In file systems as in life, the last mile is always the hardest. So hard, in fact, that it has taken a full sixty years from the advent of the first hierarchical data access scheme until the announcement of the first fully crash-tolerant file system this week, much to the delight of consumers and business continuity professionals everywhere.

The credit for the breakthrough goes to a team of computer scientists from the Massachusetts Institute of Technology (MIT), three of them professors, who have painstakingly constructed a proof-of-concept that is mathematically guaranteed to avoid data loss. That was accomplished by individually checking that each and every last bit is being handled reliably.

That’s a lot less straightforward than it sounds. The researchers had to apply the so-called formal verification techniques used in the software world to test the function of high-level algorithms at the most fundamental system level, where there are far too many variables to examine by hand, which required producing a custom simulation from scratch to verify the file system.

The work started with the basics, by feeding definitions of the individual components that make up a computer – from bits to disks – into the proof engine used for the experiment, a piece of open-source software called Coq. That involved distilling more than a century of pioneering work into programmatic abstractions that can be understood by its specialized compiler.

The task accounted for 90 percent of the time that the group dedicated to the project, according to Nickolai Zeldovich, an associate professor of computer science and engineering at MIT and one of the three lecturers who took part. The rest was spent mostly on perfecting the file system itself, which he said took about 10 rewrites.

After all the pieces were put in place, Coq was able to perform the heavylifting on its own, automatically checking every single operation performed by the system against every loss scenario from power outages to hardware errors in order to verify its integrity. The researchers will demonstrate the successful results at the upcoming ACM Symposium on Operating Systems Principles in October.

The file system itself is hardly ready for use outside the lab. But now that MIT has proven it can be done – and more specifically, that there exists a reproducible way of doing it – guaranteed loss prevention is now within the reach of consumers and enterprises. The only question left is how long it will take the industry to bring the lessons of the project to production.

Photo via IBM