First Computer Guaranteed to Never Lose Data to be Unveiled
Researchers from the Massachusetts Institute of Technology (MIT) have announced plans to unveil the first system ‘mathematically guaranteed’ to never lose data during crashes. While the system doesn’t prevent crashes from occurring, knowing that data is completely safe, and saving hours of work from being lost, will at least take away some of the pain involved. Could this be the end of data loss forever?
One of the authors of the discovery, 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.’ Zeldovich was joined by Frans Kaashoek, Adam Chlipala, Haogang Chen and Daniel Ziegler in authoring the paper earlier in the year.
Other work had proven that crash-proof systems were possible, however this new paper is the first to translate the proof into working code, and check it against a working file system. To achieve this, the researchers on this project worked alongside a proof assistant known as Coq, which checked at each stage that the file system they created adhered to the logical relationships they described in the proof. This involved defining every component in the file system and their behaviours, and then describing the relationships between those behaviours under crash conditions. Kaashoek estimated that 90% of the time spent on the paper was spent on working out and describing these definitions.
The system is to be unveiled at the ACM Symposium on Operating Systems Principles, a biennial conference for researchers and academics, this October. Already, people are thinking ahead, and of the implications of a crash-proof, data loss free system. Ulfar Erlingsson, lead manager for security research at Google, said regarding the work: ‘this is stuff that’s going to get built on and applied in many different domains. That’s what’s so exciting.’