acm-header
Sign In

Communications of the ACM

ACM TechNews

Crash-Tolerant Data Storage


A formally verified working file system could lead to computers guaranteed never to lose data.

Researchers at the Massachusetts Institute of Technoloy have developed a computer file system which, they says, mathematically ensures no loss of data should the system crashes.

Credit: Christine Daniloff/MIT

Massachusetts Institute of Technology (MIT) researchers will detail the first computer file system that mathematically ensures no loss of data when the system crashes at the ACM Symposium on Operating Systems Principles in October.

MIT professors Nickolai Zeldovich, Frans Kaashoek, and Adam Chlipala, along with students Haogang Chen and Daniel Ziegler, used formal verification to establish the file system's reliability. Formal verification entails mathematically defining acceptable bounds of operation for a computer program and then proving the program will never surpass them.

The MIT researchers' work is unique in that they demonstrate attributes of the file system's final code instead of a high-level schema, using a proof assistant called Coq to supply a formal language for describing elements of a computer system and the relationships between them.

Chlipala notes they deploy the file system in the same language in which they are writing the proofs, which are checked against the actual file system. The next step was a formal description of the relationships between the behavior of the different system components under crash conditions.

Although the file system was rewritten numerous times, Kaashoek says the researchers spent 90 percent of their time describing system aspects and the relationships between them and on the proof.

From MIT News
View Full Article

 

Abstracts Copyright © 2015 Information Inc., Bethesda, Maryland, USA


 

No entries found

Sign In for Full Access
» Forgot Password? » Create an ACM Web Account