Towards a formal foundation of intermittent computing
Towards a formal foundation of intermittent computing
复制标题
为间歇性计算奠定正式基础
DOI：
10.1145/3428231
复制
发表时间：
2020
影响因子：
--
通讯作者：
Jia, Limin
中科院分区：
文献类型：
--
作者：
Surbatovich, Milijana;Lucia, Brandon;Jia, Limin
间歇性供电的设备可以在恶劣或难以接近的环境中实现新的应用，例如太空或体内植入，但也会带来可编程性和正确性方面的问题。研究人员开发了编程模型，以确保程序取得进展，并且不会因间歇执行导致的内存不一致而产生错误结果。随着技术的成熟，间歇性供电的设备中添加了越来越多的功能，例如 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.
登录
查看更多内容
一个小挑战：构建一个可验证的文件系统
影响因子：
1
作者：
Rajeev Joshi;G. Holzmann
通讯作者：
G. Holzmann
闪烁：无电池物联网的快速原型设计
DOI：
10.1145/3131672.3131674
发表时间：
2017
期刊：
Proceedings of the 15th ACM Conference on Embedded Network Sensor Systems
影响因子：
--
作者：
Josiah D. Hester;Jacob M. Sorber
通讯作者：
Jacob M. Sorber
影响因子：
2
作者：
Hester, Josiah;Tobias, Nicole;Sorber, Jacob
通讯作者：
Sorber, Jacob
DOI：
10.1145/2429069.2429100
发表时间：
2013-01
期刊：
--
影响因子：
--
作者：
Ganesan Ramalingam;K. Vaswani
通讯作者：
Ganesan Ramalingam;K. Vaswani
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor