Future filesystems: mechanized specification, validation, implementation and verification of filesystems

文件系统非常重要。用户每次点击“保存”按钮时，都依赖于文件系统来存储他们的文件。企业依赖数据库来安全地存储数据，而这些数据库反过来又依赖于文件系统。现代文件系统的设计是为了满足许多复杂的需求。其结果是，实现被各种问题所困扰。实现代码极其复杂，几乎不可避免地包含错误。这些错误可能并且确实会导致数据损坏和丢失。开发时间非常长。测试也是非常漫长和昂贵的，并且不能保证消除所有的错误。应用程序开发人员通常不清楚文件系统提供什么保证，因此为给定的文件系统编写正确的应用程序变得极其困难，更不用说跨不同文件系统可移植的应用程序了。甚至NASA也受到了糟糕的文件系统设计的不利影响。2004年1月21日，任务控制中心与火星探索漫游者（MER）精神号失去了联系。幸运的是，勇气号配备了“残废模式能力”来应对不可预见的错误，在运营团队的广泛努力下，勇气号在16天后的2月6日恢复了运行状态。官方报告称：“异常的根本原因是提供文件系统服务的软件模块的设计错误。”如果没有残废模式的能力，“MER任务很可能已经失败了”。该特派团的费用估计超过8亿美元。如何解决这些问题？几十年来，计算机科学家一直在开发生产可靠系统的技术。验证和正确性是当前备受关注的一种方法，即根据其规格证明软件是正确的数学证明。数字经济中对可靠和可靠系统的广泛需求意味着这一领域的研究越来越重要。2003年，Tony Hoare提出了接下来15年的验证大挑战：一个经过验证的编译器。在NASA的MER异常之后，NASA的两位研究科学家Rajeev Joshi和Gerard Holzmann提出了一个更容易处理的挑战：建立一个可验证的文件系统。我们将接受这个挑战，指定并构建一个经过验证的文件系统。这项工作本质上是基础性的，但处理的是现实世界系统的复杂性。我们将使用非常复杂和高级的逻辑技术，结合最先进的软件开发技术来解决现实世界系统的全部复杂性。经过验证的文件系统有可能影响技术高度复杂的组织（如NASA）和互联网巨头（如b谷歌、Amazon和Facebook），同时也为最终用户带来好处。经过验证的文件系统可以对数字经济的许多领域产生重大影响。例如，超可靠的文件系统是追求超可靠计算基础设施的关键部分，这反过来又有助于实现将信息技术作为实用工具交付的目标。最后，除了对现实世界的影响之外，这项研究还将为进一步研究和验证使用文件系统功能的关键应用程序（如数据库和持久消息队列）提供坚实的数学基础。

Filesystems are extremely important. Users depend on filesystems to store their files whenever they hit "save". Businesses rely on databases to store their data safely, and these databases in turn rely on the filesystem.Modern filesystems are designed to satisfy many complicated requirements. As a result, implementations are beset with problems. The implementation code is extremely complex, and almost inevitably contains bugs. These bugs can and do lead to data corruption and loss. Development time is very lengthy. Testing is also very lengthy and costly, and does not guarantee to eliminate all bugs. It is often unclear to application developers what guarantees a filesystem provides, so that it becomes extremely difficult to write correct applications for a given filesystem, let alone applications that are portable across different filesystems.Even NASA was adversely affected by poor filesystem design. On January 21 2004, mission control lost contact with the Mars Exploration Rover (MER) Spirit. Fortunately Spirit had been equipped with a "crippled mode capability" to cope with unforeseen errors, and together with extensive efforts by the operations team, Spirit was returned to operational status 16 days later on February 6. The official report states: "the root cause of the anomaly was a design error in the software module that provides file system services". Without crippled mode capability, "the MER mission may well have been lost". The cost of the mission was estimated at over US$ 800 million.What can be done to tackle these problems? For many decades, computer scientists have been developing techniques for producing dependable systems. One approach that is receiving much current interest is verification and correctness i.e. mathematical proof that software is correct according to its specification. The widespread need in the digital economy for reliable and dependable systems means that research in this area is increasingly important.In 2003, Tony Hoare proposed a verification grand challenge for the following 15 years: a verified compiler. Following the NASA MER anomaly, two NASA research scientists, Rajeev Joshi and Gerard Holzmann, proposed a more tractable challenge: to build a verifiable filesystem. We will take up this challenge, and specify and build a verified filesystem.This work is foundational in nature, but tackles the complexities of real-world systems. We will use very sophisticated and high-level logical techniques combined with state-of-the-art software development techniques to address the full complexity of real-world systems. The verified filesystem has the potential to impact both technologically highly sophisticated organizations such as NASA and internet giants such as Google, Amazon and Facebook, whilst also delivering benefits to end users. A verified filesystem can have a significant impact on many areas of the digital economy. For example, an ultra-reliable filesystem is a key part of the quest for ultra-reliable computing infrastructure, which in turn contributes to the goal of delivering information technology as a utility. Finally, in addition to real-world impact, this research will provide a solid mathematical foundation for further research and verification of critical applications that make use of filesystem functionality, such as databases and persistent message queues.