Towards a Formal Foundation of Intermittent Computing

TL;DR

This paper establishes a formal foundation for intermittent computing, addressing correctness issues caused by power interruptions, and proposes algorithms and a runtime system to ensure reliable operation in such environments.

Contribution

It formalizes intermittent execution models, proves their correctness, and introduces an algorithm and runtime system to handle repeated device inputs and ensure system reliability.

Findings

Proved equivalence between existing intermittent systems.

Developed an algorithm to identify variables affected by RIOs.

Implemented a runtime system that maintains correctness with respect to inputs.

Abstract

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.