Intermittent Computing with Peripherals, Formally Verified
Intermittent Computing with Peripherals, Formally Verified
复制标题
外设间歇计算，已正式验证
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
T. Risset
中科院分区：
文献类型：
--
作者：
Gautier Berthou;Pierre;Delphine Demange;Rémi Oudin;T. Risset
具有非易失性存储器和外围设备的瞬态供电系统可实现新型低功耗传感器应用的开发。然而，作为程序员，我们没有能力推理断电是常态而不是例外的系统。第一个挑战在于能够捕获应用程序的所有易失状态（包括外围设备）以确保进度。第二个更根本的挑战在于指定电源故障如何与外围设备操作相互作用。在本文中，我们提出了外围设备间歇计算的正式规范、基于中断的检查点的公理模型及其正确性证明，并在 Coq 证明助手中进行了机器检查。我们还用文献中提出的几个系统来说明我们的模型。
Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application -- external peripherals included -- to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In this paper, we propose a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. We also illustrate our model with several systems proposed in the literature.
登录
查看更多内容
影响因子：
--
作者：
Milijana Surbatovich;Limin Jia;Brandon Lucia
通讯作者：
Milijana Surbatovich;Limin Jia;Brandon Lucia
验证持久并发数据结构的正确性：一种健全且完整的方法
影响因子：
1
作者：
Derrick J
通讯作者：
Derrick J
DOI：
10.1145/3314221.3314583
发表时间：
2019-06
期刊：
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
E. Ruppel;Brandon Lucia
通讯作者：
E. Ruppel;Brandon Lucia
使用 Perennial 验证并发、防碰撞系统
DOI：
10.1145/3341301.3359632
发表时间：
2019
期刊：
Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP
影响因子：
--
作者：
Chajed, Tej;Tassarotti, Joseph;Kaashoek, Frans;Zeldovich, Nickolai
通讯作者：
Zeldovich, Nickolai