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系统影响、在重新启用后需要恢复的变量,并证明算法正确性。最后,我们在一个新的间运行时制系统中执行算法,该算法对输入操作正确无误。

0
下载
关闭预览

相关内容

专知会员服务
50+阅读 · 2021年6月30日
【MIT-ICML2020】图神经网络的泛化与表示的局限
专知会员服务
42+阅读 · 2020年6月23日
【微众银行】联邦学习白皮书_v2.0,48页pdf,
专知会员服务
165+阅读 · 2020年4月26日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
计算机类 | PLDI 2020等国际会议信息6条
Call4Papers
3+阅读 · 2019年7月8日
计算机 | IUI 2020等国际会议信息4条
Call4Papers
6+阅读 · 2019年6月17日
计算机 | ICDE 2020等国际会议信息8条
Call4Papers
3+阅读 · 2019年5月24日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | 中低难度国际会议信息6条
Call4Papers
7+阅读 · 2019年5月16日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
人工智能 | NIPS 2019等国际会议信息8条
Call4Papers
7+阅读 · 2019年3月21日
Arxiv
0+阅读 · 2021年8月30日
Arxiv
0+阅读 · 2021年8月27日
Arxiv
30+阅读 · 2021年8月18日
AutoML: A Survey of the State-of-the-Art
Arxiv
69+阅读 · 2019年8月14日
VIP会员
相关资讯
计算机类 | PLDI 2020等国际会议信息6条
Call4Papers
3+阅读 · 2019年7月8日
计算机 | IUI 2020等国际会议信息4条
Call4Papers
6+阅读 · 2019年6月17日
计算机 | ICDE 2020等国际会议信息8条
Call4Papers
3+阅读 · 2019年5月24日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | 中低难度国际会议信息6条
Call4Papers
7+阅读 · 2019年5月16日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
人工智能 | NIPS 2019等国际会议信息8条
Call4Papers
7+阅读 · 2019年3月21日
Top
微信扫码咨询专知VIP会员