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.
翻译:断断续续的电动装置能够在严酷或无法进入的环境中进行新的应用,如空间或体内植入,但也会造成编程和正确性方面的问题。研究人员开发了程序模型,以确保程序取得进展,并且不会因间歇处决造成的记忆不一致而产生错误结果。随着技术的成熟,间歇动力装置(如I/O)增加了越来越多的特征。先前的工作表明,所有现有的间歇性执行模型都存在重复的装置或传感器输入(RIO)的问题。RIO可能使间歇性处决处于不一致的状态。这类问题和现有间歇性执行模型的扩散要求间歇性计算有一个正式的基础。在本文件中,我们正式确定了间歇性执行模型,它们对于记忆一致性和输入的正确性,并确定了证明系统正确性所需的变异性。我们证明现有的若干间歇系统是等效的。为了解决RIO问题,我们定义了一种算法,用以确定受RIO系统影响、在重新启用后需要恢复的变量,并证明算法正确性。最后,我们在一个新的间运行时制系统中执行算法,该算法对输入操作正确无误。