Towards a Formal Foundation of Intermittent Computing
summary
Provides a formal correctness definition: an intermittent execution is correct if it is observationally equivalent to some continuous execution, and it proves a theorem that checkpointing all right-after-read locations plus an exclusive may-write set (and allowing must-first-write variables) guarantees that equivalence. Implements two EMW collectors (all-branch and taint-optimized EMW) in LLVM and integrates them into Alpaca, and evaluates on prior benchmarks showing low runtime overhead—taint-optimized EMW gives the best tradeoff—while prior IBIS bug finder remains only a detector.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:13Batteryless Energy-harvesting Devices (EHDs) enable computing in inaccessible environments
- 1:00Intermittent execution in energy harvesting devices
- 2:51Input re-executions are not handled correctly
- 3:33The need to formalize intermittent execution
- 4:09Correct intermittent execution Continuous execution specifies correct program behaviour
- 4:31Difficulty of reasoning about equivalence
- 5:11Memory can be different at many points
- 6:38Outline
- 6:57Any differences must resolve on re-execution
- 7:37Must-first-write set
- 7:55Defining allowable differences
- 8:55Only checkpointing WAR variables is incorrect
- 9:32Collecting Exclusive May-Writes
- 10:40Correctness Theorem
- 11:05Implementation
- 11:27Goal of evaluation
- 11:45EMW has little performance penalty
- 12:35EMW needs little to no programmer effort
- 13:35Connection to related work
- 14:28Summary
related talks
01h 03mPrinciples of Persistent Programming
17mA Difference World: High-performance, NVM-invariant, Software-only Intermittent...
27mRecurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
16mModel Checking for a Multi-Execution Memory Model
16mMemory-Efficient Fixpoint Computation
25mMultiple Resumptions and Local Mutable State, Directly
14mA Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
15mIncremental Certified Programming