Designing Formally Correct Intermittent Systems

Batteryless energy harvesting devices (EHDs) enable computing in environments that are too harsh, remote, or inaccessible to support the required maintenance of a battery, opening the door to new applications in domains such as health wearables, disaster monitoring, and smart infrastructure. Instead of using a battery, an EHD harvests energy from its environment into a buffer and operates intermittently, only as energy is available. This operational cycle causes the device to experience frequent, arbitrary power failures that make correct programming difficult. To make progress, software relies on intermittent system support to save execution state before power failure and restore it after the device reboots. Mistakes in determining which state must be saved and where a save point should be made cause software to exhibit memory and timing bugs that would not occur on continuously powered program executions. As EHDs are envisioned to be remotely deployed, low-maintenance devices that run sensitive applications, software must execute reliably, without memory consistency or timing violations that could corrupt results or render the device inoperable. Unfortunately, existing intermittent systems rely on informal, undefined correctness notions that preclude proving such necessary correctness properties. 

This dissertation lays the foundation for designing formally correct intermittent systems by providing formal models and correctness definitions along with practical enforcement tools. First, we confirm the need for formal reasoning by showing how existing correctness notions are insufficient and lead to unaddressed bugs. We then present a formal model of intermittent execution and a correctness theorem, using these to design a runtime system that is provably correct with respect to memory state. Next, we show how reasoning about safe intermittent execution at the language level via types gives application programmers more control over how their applications execute on these unusual new devices and moreover leads to simpler, more modular system design. Finally, we address timing violations caused by intermittent execution. To that end, we create language abstractions a programmer can use to specify important timing properties and develop a compiler toolchain that generates correct-by-construction executables with respect to the specified timing constraints. Together, the contributions of this dissertation allow the development of intermittent systems that meet specified guarantees of time and memory consistency, improving programmability and reliability