ACM通信
研究突出了
技术角度:证明文件系统符合预期
50多年来，文件系统一直是计算机系统的标准组成部分。我们经常(大多数是不假思索地)使用它们来存储和检索持久数据。但它们到底有多持久呢?
这个问题的答案比乍看起来要复杂得多，原因如下。持久存储介质比非持久存储器(如处理器寄存器或随机访问存储器)慢几个数量级。它们的组织方式也不同:持久媒体以块的形式进行读写，其大小为千字节，但也可高达兆字节。弥合速度和粒度差距需要复杂的数据缓冲逻辑、实现高效查找和重新排序慢操作以获得最佳性能。其中一些由操作系统执行，另一些在存储设备的固件中执行，操作系统控制有限。
文件系统将这种复杂性隐藏在一个简单的读写接口后面，承诺写入持久媒体的数据可以在以后正确地检索(前提是存储媒体本身不被销毁)。
使实现这一承诺变得棘手的是计算机系统是(仍然不可靠，他们会坠毁。这样的崩溃可能是物理故障(缺乏电力)的结果，但更常见的是软件故障的结果，尤其是操作系统，甚至文件系统实现本身。除非非常小心，否则这样的失败可能会导致本应持久的数据的丢失或损坏。例如，一个写操作可能已经更新了一个内部缓冲区，但还没有到达持久介质，从而导致数据丢失。重新排序可能会导致违反因果关系，其中稍后在计算中产生的数据是持久的，而之前在逻辑上产生的数据不是。在极端情况下，元数据(例如查找数据结构)的损坏可能会导致之前已持久化的数据的丢失。
不同的文件系统在防止这种损失方面采取了不同的措施，从根本不提供任何保证，到保证元数据的完整性，再到保证在显式或隐式同步屏障之前写入的所有数据的持久性和完整性。但是，当这些“保证”在几乎肯定有bug的复杂软件中实现时，它们的真正含义是什么?
具体来说，文件系统是“崩溃安全的”是什么意思?
经验表明，这些都是严重的问题，如果在特别不恰当的时刻发生崩溃，即使是“成熟的”文件系统也无法实现它们的承诺。理想情况下，人们希望有证据证明承诺在任何情况下都能得到遵守。但如果你不能清楚地定义碰撞安全的真正含义，你甚至无法开始这样的证明。
下面的论文展示了朝着现实世界中严格意义上的崩溃安全的文件系统迈出的一大步。它发展了一种被称为崩溃霍尔逻辑的形式主义，它扩展了传统的霍尔逻辑，广泛用于程序的推理，通过崩溃条件。这样，当执行过程中任意时间发生崩溃时，作者就可以推断文件系统的一致性。它甚至可以处理在恢复过程中发生的崩溃，当文件系统在崩溃后试图从持久介质上找到的任何内容重新构建一致状态时，在最坏的情况下不会发生任何进展(这种情况可能是由于文件系统本身的错误触发的崩溃引起的)。
这确实是一项了不起的工作，它将一种新形式主义的发展及其在实际系统中的应用结合起来，以证明非常复杂的性质。
作者展示了如何将此逻辑应用于实际的文件系统，包括一些困难，如对文件系统代码执行异步的读写操作。然后，他们使用这种形式来指定和实现一个实际的、功能齐全的文件系统，并生成一个机器检查的、基本自动化的证明，以证明该文件系统实际上是安全的。
这确实是一项了不起的工作，它将一种新形式主义的发展及其在实际系统中的应用结合起来，以证明非常复杂的性质。正是这种性质的形式证明是最强大的，因为任何像碰撞安全属性那样复杂和相互关联的东西都是出了名的难以在实现中得到正确的。经验表明，它几乎从来没有被毫无道理的正式证明过。
证明自动化是非常重要的，使这样的技术规模到现实世界，高性能的系统。在这篇论文中，作者已经迈出了减少人工工作量的第一步，他们的工作已经引发了这种证明自动化的进一步进展。其他工作已经证明了自动化一些底层基础设施的可行性，本工作假设这是正确的，无需证明。所有这些都意味着，拥有功能正确性的完整证明的完整操作系统，可能比我们两年前所认为的更接近现实。
数字图书馆是由计算机协会出版的。版权所有©2017 ACM股份有限公司
没有发现记录