Intermittent Computing with Peripherals, Formally Verified.

Gautier Berthou, Pierre-Évariste Dagand, Delphine Demange, Rémi Oudin, Tanguy Risset.

Paper accepted at LCTES20

Presentation and slides

Companion Coq development

Browsable Coq development

Main results

Auxiliary definitions, and intermediate refinements

Our proof is organized as a series of refinements, modulo some subtrace relations. The global refinement chain is

PLF ⊆sub PLFO ⊆ PL ⊆sub PLO ⊆ SPEC

PLFO and PLO are intermediate checkpointing schemes where non-determinism related to checkpointing failures (PLFO), and power-interrupts during power-continuous sections (PLO) are removed, thanks to oracles. We prove the existence of those oracles, and that they progressively lead to a corresponding trace in SPEC.

Corresponding definitions and proofs are in the following files: