Batteryless energy-harvesting devices enable computing in harsh or inaccessible environments, at a cost to programmability and correctness. These devices operate intermittently as energy is available, requiring a recovery system to save and restore program state. Complicating matters, some program tasks must execute atomically w.r.t. power failures, re-executing if power fails before completion. Such a re-execution should typically be idempotent—its behaviour should not differ from the behaviour of a single execution. Thus, a key aspect to correct intermittent execution is identifying and recovering state causing undesired non-idempotence. Unfortunately, past intermittent systems take an ad-hoc approach to identifying this set, using potentially unsound dataflow analyses or conservatively recovering all written state. Moreover, no prior work allows the programmer to specify idempotence requirements.

We present Curricle, the first type system approach to safe intermittence, based on Rust. Type level reasoning allows programmers to express requirements and retains crucial alias information necessary for sound analyses. Curricle uses information flow and type-state reasoning to rule out programs that cause unintentional non-idempotence. We implement Curricle’s type system on top of the Rust compiler, evaluating the prototype on benchmarks from prior work, finding that Curricle benefits recovery system designers and application programmers. Targeting Curricle allows designers to write simpler, more performant systems. Using Curricle allows programmers to express idempotence requirements, having assurance that the program will execute correctly.