The awesome people at the Massachusetts Institute of Technology (MIT) have come up with a way to create an “uncrashable” computer, which means the pain of losing data to a crashing system could soon be ended, for good.
The work is still slow, but it is a major breakthrough, says V3, quoting the researchers in the university’s Computer Science and Artificial Intelligence Laboratory.
Nickolai Zeldovich, a principal investigator at CSAIL, who co-authored the new paper, explained the system.
“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?’" he said.
"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."
The key difference in the research lied in Coq, a “proof assistant”, which provided “a formal language for describing aspects of a computer system and the relationships between them".
By focusing on the final code instead of on a “high-level schema”, these problems were skipped.
“We implement the file system in the same language where we’re writing the proofs. And the proofs are checked against the actual file system, not some whiteboard idealisation that has no formal connection to the code,” he said.
The research drew attention of a couple of big players, Google included.
“I can say for certain that Adam’s stuff with Coq, and separation logic, is stuff that’s going to get built on and applied in many different domains. That’s what’s so exciting,” said Ulfar Erlingsson, lead manager for security research at Google.