Slashdot Mirror
MIT's New File System Won't Lose Data During Crashes
jan_jes sends news that MIT researchers will soon present a file system they say is mathematically guaranteed not to lose data during a crash. While building it, they wrote and rewrote the file system over and over, finding that the majority of their development time was spent defining the system components and the relationships between them. "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." The file system is slow compared to other modern examples, but the researchers say their formal verification can also work with faster designs. Associate professor Nickolai Zeldovich said, "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.”
Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth
If the hard drive firmware is not proven, this FS won't be any better than ZFS and others.
Writing safe file systems is the easy part (even trivial using synchronous writes, when you consider their design is "slow").
The impossible part is dealing with firmwares that are known to lie (including pretending than a write is synchronous): how could you not lose data if the drive didn't ever write the data to the platters in the first place ?
I have discovered a truly marvelous proof of killer sig, which this margin is too narrow to contain.
> When write is complete, signal application.
How do you know the write was complete? Most storage hardware lies about completing the write. The ZFS folks found this out the hard way: their filesystem was supposed to survive arbitrary power failures, and on a limited set of hardware that was true. In reality, most drives/controllers say they've committed the write to disk when it's still in their cache.
Any filesystem that claims to survive crashes needs to take into account that any write confirmation could be a lie, and that any data it has written in the past may still be in a volatile cache.
However, considering how many firmware bugs there are in modern SSDs and HDs which cause out-of-order writes, shorn writes, and various other random corruptions and bad behaviour during a power failure or system reset, what would be more interesting is how the file system could cope with one of those.
Many consumer devices generally conform to an unwritten standard, not a written one. That unwritten standard is "do whatever is needed to make it work on Windows". This means that mandatory commands might not be fully tested, or sometimes not even implemented. And because these are consumer devices, the manufacturers generally aren't concerned about rare end-user problems, since whoever bought the flash thumb drive on sale isn't going to complain, and the margins are way too small to waste time on reliability. All that matters is getting it to work for most people most of the time.