Thanks to the research group of MIT’s Computer Science and Artificial Intelligence Lab (CSAIL) who claimed to have created a computer that will never lose data in the event of a crash. The team from MIT’s CSAIL said that the new system is “mathematically guaranteed’ not to lose information by accident, such as though a system crash or other failure. MIT researchers will present the first file system at the ACM Symposium on Operating Systems Principles in October, which will show that the system is mathematically guaranteed not to lose track of data during crashes. Although the system is slow, the researchers admit, the same principles could be applied to more “sophisticated designs.” In the end, formal verification could make it much easier to develop reliable, efficient file systems. Nickolai Zeldovich, co-author of the paper and CSAIL principal investigator, said: “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.” “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. 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.” To test and confirm the computer’s abilities, the research team went through a process known as formal verification, which mathematically describes the limits of operation for a computer program, before proving the program cannot go beyond those limits. While the computer can still crash, but it can save data in the process. “It’s not like people haven’t proven things in the past,” Ulfar Erlingsson, the lead manager for security research at Google, who had observed the MIT team at work, said. “But usually the methods of 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. “This is stuff that’s going to get built on and applied in many different domains. That’s what’s so exciting.” In the course of writing the file system, they repeatedly went back and retooled the system specifications, and vice versa. The team at MIT is hopeful that their new system safeguard design will be utilized in many different sectors in the IT and business industries. The paper will be presented at the ACM Symposium on Operating Systems Principles
