Carnegie Mellon University
curricle_long_version.pdf (2.81 MB)
Download file

Technical Report: A Type System for Safe Intermittent Computing

Download (2.81 MB)
posted on 2023-06-21, 19:50 authored by Milijana SurbatovichMilijana Surbatovich, Naomi Spargo, Limin JiaLimin Jia, Brandon LuciaBrandon Lucia

The long version of the Curricle  Programming Language Design and Implementation (PLDI) 23 paper that includes the appendix. 

 Batteryless energy-harvesting devices enable computing in inaccessible environments, at a cost to programmability and correctness. These devices operate intermittently as energy is available, using a recovery system to save and restore state. Some program tasks must execute atomically w.r.t. power failures, re-executing if power fails before completion. Any reexecution should typically be idempotent—its behavior should match the behavior of a single execution. Thus, a key aspect of correct intermittent execution is identifying and recovering state causing undesired non-idempotence. Unfortunately, past intermittent systems take an ad-hoc approach, using unsound dataflow analyses or conservatively recovering all written state. Moreover, no prior work allows the programmer to directly specify idempotence requirements (including allowable nonidempotence).

We present Curricle, the first type system approach to safe intermittence, for Rust. Type level reasoning allows programmers to express requirements and retains alias information crucial for sound analyses. Curricle uses information flow and type qualifiers to reject programs causing undesired non-idempotence. We implement Curricle’s type system on top of Rust’s compiler, evaluating the prototype on benchmarks from prior work. We find that Curricle benefits application programmers by allowing them to express idempotence requirements that are checked to be satisfied, and that targeting programs checked with Curricle allows intermittent system designers to write simpler recovery systems that perform better.


Usage metrics