Search for: All records

We present Metis, a model-checking framework designed for versatile, thorough, yet configurable file system testing in the form of input and state exploration. It uses a nondeterministic loop and a weighting scheme to decide which system calls and their arguments to execute. Metis features a new abstract state representation for file-system states in support of efficient and effective state exploration. While exploring states, it compares the behavior of a file system under test against a reference file system and reports any discrepancies; it also provides support to investigate and reproduce any that are found. We also developed RefFS, a small, fast file system that serves as a reference, with special features designed to accelerate model checking and enhance bug reproducibility. Experimental results show that Metis can flexibly generate test inputs; also the rate at which it explores file-system states scales nearly linearly across multiple nodes. RefFS explores states 3–28x faster than other, more mature file systems. Metis aided the development of RefFS, reporting 11 bugs that we subsequently fixed. Metis further identified 12 bugs from five other file systems, five of which were confirmed and with one fixed and integrated into Linux. 

We present Metis, a model-checking framework designed for versatile, thorough, yet configurable file system testing in the form of input and state exploration. It uses a nondeterministic loop and a weighting scheme to decide which system calls and their arguments to execute. Metis features a new abstract state representation for file-system states in support of efficient and effective state exploration. While exploring states, it compares the behavior of a file system under test against a reference file system and reports any discrepancies; it also provides support to investigate and reproduce any that are found. We also developed RefFS, a small, fast file system that serves as a reference, with special features designed to accelerate model checking and enhance bug reproducibility. Experimental results show that Metis can flexibly generate test inputs; also the rate at which it explores file-system states scales nearly linearly across multiple nodes. RefFS explores states 3–28× faster than other, more mature file systems. Metis aided the development of RefFS, reporting 11 bugs that we subsequently fixed. Metis further identified 12 bugs from five other file systems, five of which were confirmed and with one fixed and integrated into Linux. 

Manipulating gene expression in the host genome with high precision is crucial for controlling cellular function and behavior. Here, we present a precise, non-invasive, and tunable strategy for controlling the expression of multiple endogenous genes both in vitro and in vivo, utilizing ultrasound as the stimulus. By engineering a hyper-efficient dCas12a and effector under a heat shock promoter, we demonstrate a system that can be inducibly activated through thermal energy produced by ultrasound absorption. This system allows versatile thermal induction of gene activation or base editing across cell types, including primary T cells, and enables multiplexed gene activation using a single guide RNA array. In mouse models, localized temperature elevation guided by high-intensity focused ultrasound effectively triggers reporter gene expression in implanted cells. Our work underscores the potential of ultrasound as a clinically viable approach to enhance cell and gene-based therapies via precision genome and epigenome engineering. 

We study equilibrium configurations of double-stranded DNA in a cylindrical viral capsid. The state of the encapsidated DNA consists of a disordered inner core enclosed by an ordered outer region, next to the capsid wall. The DNA configuration is described by a unit helical vector field, tangent to an associated centre curve, passing through properly selected locations. We postulate an expression for the energy of the encapsulated DNA based on that of columnar chromonic liquid crystals. A thorough analysis of the Euler–Lagrange equations yields multiple solutions. We demonstrate that there is a trivial, non-helical solution, together with two solutions with non-zero helicity of opposite sign. Using bifurcation analysis, we derive the conditions for local stability and determine when the preferred coiling state is helical. The bifurcation parameters are the ratio of the twist versus the bend moduli of DNA and the ratio between the sizes of the ordered and the disordered regions.