Communications of the ACM
Crash-Tolerant Data Storage
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