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.