SoylentNews

AnonTechie [soylentnews.org] writes:

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 [ucsc.edu], 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.

“What many people worry about is building these file systems to be reliable, both when they’re operating normally but also in the case of crashes, power failure, software bugs, hardware errors, what have you,” says Nickolai Zeldovich, an associate professor of computer science and engineering and one of three MIT computer-science professors on the new paper. “Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash. You literally have to consider every instruction or every disk operation and think, ‘Well, what if I crash now? What now? What now?’ And so empirically, people have found lots of bugs in file systems that have to do with crash recovery, and they keep finding them, even in very well tested file systems, because it’s just so hard to do.”

https://www.eecs.mit.edu/news-events/media/crash-tolerant-data-storage [mit.edu]

[Also Covered By]: MIT researchers create file system guaranteed not to lose data even if a PC crashes [computerworld.com]

[Related]: Hoare logic [wikipedia.org]

Original Submission