In a computer operating system, the file system is the part that writes data to disk and tracks where the data is stored. If the computer crashes while it’s writing data, the file system’s records can become corrupt. Hours of work could be lost, or programs could stop working properly. At the ACM Symposium on Operating Systems Principles in October, MIT researchers will present the first file system that is mathematically guaranteed not to lose track of data during crashes. Although the file system is slow by today’s standards, the techniques the researchers used to verify its performance can be extended to more sophisticated designs. Ultimately, formal verification could make it much easier to develop reliable, efficient file systems.
Nickolai Zeldovich, an associate professor of computer science and engineering and his colleagues — Frans Kaashoek, the Charles A. Piper Professor in MIT’s Department of Electrical Engineering and Computer Science (EECS); associate professor of computer science Adam Chlipala; Haogang Chen, a graduate student in EECS; and Daniel Ziegler, an undergraduate in EECS — established the reliability of their file system through a process known as formal verification. Read the full article at the MIT News Office