间歇计算的形式化基础
Towards a Formal Foundation of Intermittent Computing
摘要：
间歇供电设备使新的应用在恶劣或难以接近的环境中，如空间或体内植入，但也引入了可编程性和正确性的问题。研究人员开发了编程模型，以确保程序取得进展，并且不会由于间歇执行引起的内存不一致而产生错误的结果。随着技术的成熟，越来越多的功能被添加到间歇供电的设备中，例如I/O。先前的工作表明，所有现有的间歇执行模型都存在重复设备或传感器输入（RIO）的问题。RIO可能会使间歇性的执行处于不一致的状态。这些问题和现有的间歇性执行模型的扩散需要一个正式的间歇性计算的基础。在本文中，我们形式化间歇执行模型，其正确性方面的内存一致性和输入，并确定所需的不变量来证明系统的正确性。我们证明几个现有的间歇性系统之间的等价性。为了解决RIO问题，我们定义了一个算法，用于识别受RIO影响的变量，这些变量需要在重启后恢复，并证明该算法是正确的。最后，我们实现了一个新的间歇运行时系统，是正确的输入操作，并评估其性能的算法。
英文摘要：
Intermittently powered devices enable new applications in harsh or inaccessible environments, such as space or in-body implants, but also introduce problems in programmability and correctness. Researchers have developed programming models to ensure that programs make progress and do not produce erroneous results due to memory inconsistencies caused by intermittent executions. As the technology has matured, more and more features are added to intermittently powered devices, such as I/O. Prior work has shown that all existing intermittent execution models have problems with repeated device or sensor inputs (RIO). RIOs could leave intermittent executions in an inconsistent state. Such problems and the proliferation of existing intermittent execution models necessitate a formal foundation for intermittent computing. In this paper, we formalize intermittent execution models, their correctness properties with respect to memory consistency and inputs, and identify the invariants needed to prove systems correct. We prove equivalence between several existing intermittent systems. To address RIO problems, we define an algorithm for identifying variables affected by RIOs that need to be restored after reboot and prove the algorithm correct. Finally, we implement the algorithm in a novel intermittent runtime system that is correct with respect to input operations and evaluate its performance.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
