According to Sky News, the researchers have developed a file system, the part of a computer’s operating system that writes data to disk and tracks where it is stored, that they claim is “mathematically guaranteed” not to lose information.
The team from the university’s Computer Science and Artificial Intelligence Laboratory went through an exhaustive process known as formal verification to prove this.
This involves describing the acceptable bounds of operation for a programme, and then proving it will not exceed them.
Nickolai Zeldovich, part of the team that carried out the research, 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.
“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.”
While the researchers admit the file system they have developed is slow by today’s standards, the team says the methods they used can be applied to more sophisticated designs.
“Ultimately, formal verification could make it much easier to develop reliable, efficient file systems,” the department said in a press release.
The researchers’ work will be presented at a symposium later this year.
