Intermittent Computing with Peripherals, Formally Verified.

Paper accepted at LCTES20

• Abstract: Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application -- external peripherals included -- to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In this paper, we propose a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. We also illustrate our model with several systems proposed in the literature.
• Paper at publisher's: [.pdf]

Presentation and slides

• Virtual LCTES presentation: [video]
• Slides: [.pdf]

Companion Coq development

• Download the Coq formalization: [.tar.gz]
• Read the README.md first.

Browsable Coq development

Main results

• [device.v] DEV_Sig: devices formalized using request and responses. Concrete instanciations of devices:
  • [device_temp.v] Temperature sensor (Example 3)
  • [device_smclk.v] Sub-main clock (Example 4)
  • [device_cc2500.v] CC2500 radio link (Example 5)
  • [device_msp430.v] Sytare device model (Example 7)
• [specification.v] MCU, DEV, SPEC: specification of intermittent computing with peripherals, run in a continuous-power environment.
• [plf.v] LOG, CHKPT, PLF: interrupt-based checkpointing with failures.
• [PLF_SPEC.v] Final correctness theorem, and subtrace relation : ∀ t. PLF.sem t -> ∃ t', SPEC.sem t' ∧ t ≥ t'
• [PLF_SPEC_op.v] Alternative, operational characterization of the final correctness theorem, with explicit subtrace:
  ∀ t. PLF.sem t -> SPEC.sem (filter t).

Auxiliary definitions, and intermediate refinements

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

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:

• [util.v] Semantic definitions common to whole development
• [PLFO.v] PLFO: interrupt-based checkpointing with failures. A checkpointing oracle dictates the success/failure of the next checkpoint, just before transiting to OFF.
• [PLF_PLFO.v] Relation ≥chk, and proof of the following refinement PLF.sem t -> ∃ o t', PLFO.sem o t' ∧ t ≥chk t'.
• [PL.v] PL: interrupt-based checkpointing without checkpointing failures. Non-deterministic in the occurrence of power-interrupts during power-continuous sections.
• [PLFO_PL.v] Refinement proof PLFO.sem o ⊆ PL.sem.
• [PLO.v] PLO: interrupt-based checkpointing without checkpointing failures. A logging oracle dictates power-loss interrupts occurring during power-continuous sections.
• [PL_PLO.v] Relation ≥log, and proof of the refinement PL.sem t -> ∃ o t', PLO.sem o t' ∧ ∃ t ≥log t'.
• [PLO_SPEC.v] Refinement proof PLO.sem o ⊆ SPEC.sem.