Modal Crash Types for WAR-Aware Intermittent Computing

Programs are executed intermittently on devices such as Energy Harvesting Devices (EHDs) that experience arbitrary power failures. To ensure progress, intermittent systems need runtime support to checkpoint state and re-execute after power failure by restoring the last saved state. Such re-execution should be correct, i.e., simulated by a continuously-powered execution. We study the logical underpinning of intermittent computing and model checkpoint, crash, restore, and re-execution operations as computation on Crash types. We draw inspiration from adjoint logic and define Crash types by introducing two adjoint modality operators to model persistent and transient memory values of partial (re-)executions and the transitions between them caused by checkpoints and restoration. Our formalism is general enough to accomodate a variety of checkpointing policies. We define a Crash type system for a core calculus. To prove the correctness of intermittent systems, we define a novel logical relation for Crash types.