PERSEVERE: A Rigorous Foundation for Persistent Verification

当你的电脑电源被切断，或者你的移动的手机电池耗尽，你当时正在工作的任何东西（例如纸牌游戏）都将永远丢失。这是因为RAM，您的设备用于临时存储数据的内存，在断电时会被擦除。然而，当您的设备重新开机时，您保存在PC上的文档或您在手机上拍摄的照片仍然在您的设备上。这是因为它们保存在硬盘驱动器中，硬盘驱动器是永久存储器，即使断电也会保留其数据。最近，技术公司制造了一种新型RAM，非易失性存储器或NVM，当断电时不会丢失其数据。这意味着当设备在断电或发生灾难性事件（如崩溃）后重新打开时，其数据仍然可以在NVM上使用;我们说它的数据仍然存在。这意味着通过仔细的工程设计，我们可以恢复数据而不会丢失我们的工作。然而，这并不那么简单。现代设备的速度非常快，为了做到这一点，它们使用聪明的方法来有效地完成工作。例如，它们一次完成多项任务，或者以不同的顺序完成一系列任务。有时这意味着让您的数据暂时处于不好的状态，稍后再进行修复，例如在保存新版本之前删除旧数据。如果我们在一个坏的临时状态下断电（例如，在删除旧数据之后，但在保存其替换之前），那么当我们重新启动设备时，我们可能会恢复坏数据。我的研究项目将从硬件（例如手机）、软件（例如手机应用程序）和理论分析的角度研究NVM的使用，从而解决这些问题。我将开发新的工具和技术，帮助我们构建持久的技术，然后使用形式化（数学）方法来证明这些工具和技术是安全和正确的。我提议的研究有三个关键组成部分。首先，我将创建NVM的“持久模型”，这是严格的方式来描述NVM可以/不能做什么，具有数学精度。然后，我将使用专门的工具来测试英特尔和ARM微芯片（在我们的PC和手机）对我的模型，看看他们如何使用NVM时的行为。确保真实世界的硬件按预期运行是迈向安全可靠的NVM的重要一步，因为它为在其上编写软件提供了安全的基础。其次，我将扩展现代编程语言，使编写的程序（软件）能够控制数据如何持久存储到NVM，这反过来又使恢复NVM数据变得更容易和更安全。目前，写这样的程序是不可能的，因为NVM是一个新的概念，持久性控制不是现代编程语言的一部分。我将扩展这些语言并提供示例程序和测试。然后，我将证明这些扩展是正确的，以便软件公司可以依靠它们来构建他们未来的产品。最后，我将开发测试和验证程序安全恢复NVM数据的方法。测试是硬件和软件开发的重要组成部分，但测试NVM持久性目前是不可行的：目前唯一的方法是运行数千次测试，每次在不同的时间切断电源。然而，强制这种频繁的功率损耗既不切实际又效率低下。我将开发新的方法来测试NVM的持久性，这是广泛采用NVM的最后一个关键步骤。NVM每年可以节省无数的数据，金钱和时间。数据丢失不仅是每天使用计算机的人面临的问题，也是全球数据中心和安全关键技术面临的问题。NVM可以使数据丢失成为过去，但需要建立一个严格、安全的基础，以避免一种不可预测性变成另一种不可预测性。这项研究项目将确保这一基础，并释放这项新技术的潜力。

When your PC power is cut off, or your mobile phone runs out of battery, anything you were working on at the time (e.g. a game of Solitaire) is lost forever. This is because the RAM, the memory your device uses to store data temporarily, is wiped clean whenever it loses power. However, documents you saved on your PC or the photos you took on your phone are still on your device when it switches back on. This is because they are saved to the hard drive, which is permanent storage that keeps its data even if it loses power.Recently, technology companies have manufactured a new type of RAM, non-volatile memory or NVM, that does not lose its data when it loses power. This means that when a device switches back on after losing power or something catastrophic like a crash, its data is still available on NVM; we say that its data persists. This means that with careful engineering we may recover the data and not lose our work.However, this is not quite so straightforward. Modern devices are very fast, and to do this they use clever methods to get work done efficiently.For example, they do multiple tasks all at once or do a list of tasks in a different order. Sometimes this means leaving your data in a bad state temporarily and fixing it later, e.g. deleting your old data before saving a new version. If we lose power during a bad temporary state (e.g. after deleting old data but before saving its replacement), then when we restart the device we may recover bad data. This has many unfortunate consequences, from simply losing data to causing errors in our software.My research project will solve these problems, by studying NVM use from the perspective of hardware (e.g. our phones), software (e.g. our phone apps), and theoretical analysis. I will develop new tools and techniques that will help us build persistent technology, and then use formal (mathematical) methods to prove that these tools and techniques are safe and correct.My proposed research has three key components. First, I will create NVM 'persistency models', which are rigorous ways of describing exactly what NVM can/cannot do, with mathematical precision. I will then use specialised tools to test Intel and ARM microchips (in our PCs and phones) against my models, and see how they behave when using NVM. Verifying that real-world hardware behaves as expected is an important step towards safe and reliable NVM, as it provides a safe foundation to write software on top of.Second, I will extend modern programming languages to enable writing programs (software) that can control how data persists to NVM, which in turn makes it easier and safer to recover NVM data. Currently it is impossible to write such programs, because NVM is such a new concept that persistence control is not a part of modern programming languages. I will extend these languages and provide example programs and tests. I will then prove that these extensions are correct so that software companies can rely on them to build their future products.Finally, I will develop ways to test and verify that programs safely recover NVM data. Testing is an important part of hardware and software development, but testing NVM persistency is currently infeasible: the only way to do this currently is to run thousands of tests, each time cutting the power at different times. However, forcing such frequent power losses is both impractical and inefficient. I will develop new ways to test NVM persistency, which is the final key step for widespread NVM adoption.NVM could save untold amounts of data, money and time every year. Data loss is faced by not only people who use computers every day, but also data centres and safety-critical technologies worldwide. NVM can make data loss a thing of the past, but requires a rigorous, safe foundation to be built on, to avoid trading one kind of unpredictability for another. This research project will ensure that foundation, and unleash the potential of this new technology.