Nickolai Zeldovich表示,确保文件系统可以从系统崩溃中恢复比较棘手,因为有这么多不同的地方需要考虑和处理,你必须考虑每个指令或每个磁盘操作,发现系统崩溃原因,找出处理方式,找出系统崩溃时文件系统中的海量错误,并且随时试图纠正这些错误。因此即使是在非常行之有效的文件系统,确保文件系统可以从系统崩溃中恢复不仅棘手而且耗时。
Nickolai Zeldovich相信他们开发的这套文件系统可应用到其他设计当中,他们这个项目历经了10次改写,他们花费90%的时间来定义组件,以及它们之间的关系和实际的形式证明。他们可能没有太多的时间优化这套文件系统。该小组在开发过程中使用Coq证明助手。
MIT研究小组的工作已经引起行业一些成员关注。 谷歌首席安全经理 lfar Erlingsson表示,说,现有正式设计主要针对特定的文件系统,在重复使用上变化不大。与此相反,MIT的工作可以被用作许多不同应用程序的基础。
该小组将在10月份举行的操作系统原则ACM研讨会上展示他们的研究成果。