  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.
