PERSEVERE: A Rigorous Foundation for Persistent Verification

PERSEVERE：持久验证的严格基础

• 批准号: MR/V024299/1
• 负责人: Azalea Raad
• 金额: $ 191.12万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=MR%2FV024299%2F1
• 关键词: PERSEVERE; Rigorous; Foundation; Persistent; Verification

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.

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

项目成果

The Path to Durable Linearizability

持久线性化之路

• DOI: 10.1145/3571219
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: D'Osualdo E

Memento: A Framework for Detectable Recoverability in Persistent Memory

• DOI: 10.1145/3591232
• 发表时间: 2023-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: K. Cho;Seungmin Jeon;Azalea Raad;Jeehoon Kang

Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8

• DOI: 10.1145/3453483.3454027
• 发表时间: 2021-06
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: K. Cho;Sung-Hwan Lee;Azalea Raad;Jeehoon Kang

Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores

• DOI: 10.1145/3498683
• 发表时间: 2022-01
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Azalea Raad;Luc Maranget;Viktor Vafeiadis

Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings

编程语言和系统 - 第 31 届欧洲编程研讨会，ESOP 2022，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2022，德国慕尼黑，2022 年 4 月 2-7 日，会议记录

• DOI: 10.1007/978-3-030-99336-8_9
• 发表时间: 2022
• 作者: Bila E