MIT researchers have built a filesystem that won't lose data to a crash

[Ekpyrosis]

Illustration: Christine Daniloff/MIT

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.

“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.”

[...]

“We’ve written file systems many times over, so we know exactly what it’s going to look like,” Zeldovich says. “Whereas with all these logics and proofs, there are so many ways to write them down, and each one of them has subtle implications down the line that we didn’t really understand.”

“No one had done it,” Kaashoek adds. “It’s not like you could look up a paper that says, ‘This is the way to do it.’ But now you can read our paper and presumably do it a lot faster.”

“It’s not like people haven’t proven things in the past,” says Ulfar Erlingsson, lead manager for security research at Google, who has observed the new work from a distance. “But usually the methods and technologies, the formalisms that were developed for creating the proofs, were so esoteric and so specific to the problem that there was basically hardly any chance that there would be repeat work that built up on it. But I can say for certain that Adam’s stuff with Coq, and separation logic, this is stuff that’s going to get built on and applied in many different domains. That’s what’s so exciting.”

Source: http://news.mit.edu/2015/crash-tolerant-data-storage-0824 (Highlighting by me)

This filesystem won't lose any data to a crash, it won't corrupt and that is formally proven. You can look up the technical details in the article, basically they achieve 100% certainty by using the same "language" for the proof and the filesystem itself, unlike exitisting proofs for other filesystems that only apply to an ivory tower abstraction instead of an actual implementation.

It will take a whole while before we can see any real-world benefit from this, but I still think it is exciting news, as filesystems can be a pain to deal with sometimes and this will matter eventually.

[blackadder]

This isn't news you hear about often but, should effect us all if it happens. This seems cool for mission critical stuff.

[Aytex]

microsoft r u there? can u buy dis 4 me pls

[Knaj]

Sorta off topic, but I love how that's a windows popup on a macbook

[Kherm]

NTFS 2.0

[SleathX1]

Sorta off topic, but I love how that's a windows popup on a macbook

Dual boot for the win

[Yummychickenblue]

And Microsoft will stick with NTFS. The filesystem they developed in the late 90's and still use today.

[patrickjp93]

Can't wait to get this paper and find the flaw like I found in their proof that Subgraph Isomorphism is NP-HARD. MIT's been slipping lately. That was embarrassing for them like little ever has been.

[Ekpyrosis]

Can't wait to get this paper and find the flaw like I found in their proof that Subgraph Isomorphism is NP-HARD. MIT's been slipping lately. That was embarrassing for them like little ever has been.

Wouldn't such a flaw be found by Coq, though?

[patrickjp93]

Wouldn't such a flaw be found by Coq, though?

Coq doesn't actually prove that a program is bug-free with a gap in the logic needed. It's highly limited in what it can detect, and there's a huge disclaimer bundled with it saying just that in more technical speak. It's not a valid proof of an air-tight program to have it pass Coq's tests. That's why no proof paper in IEEE or ACM uses it as the only proof provided. That said, it is useful to have Coq's overall analysis of the logic.

 

If there's anything out of scope or improperly represented in the logic, Coq won't catch it. IBM's working on a much more sophisticated system right now actually.

[TrigrH]

NTFS 2.0

 

aka Not This Fucking Shit again