SHF: Small: Practical and Formal Foundations for Intermittent Computer Systems

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Intermittent, energy-harvesting, battery-less devices are cheap, small, and low-maintenance devices for building computing, sensing, and communicating systems that will serve as the foundation for future internet of things, edge computing and sensing, and cyber physical systems. However, intermittent software execution can make a device unreliable, due to the device's hard-to-predict power failure and recharge cycles, complicating deployment to high-assurance applications. This project defines the first formal models to precisely characterize the behavior of intermittent systems, formalizes desired correctness properties, designs and implements new sophisticated intermittent systems that are correct, and constructs benchmarks representative of real-world applications of intermittent systems. This project's impacts are that its technical developments make intermittent systems capable of complex tasks, and at the same time, safer and more reliable, thereby allowing wider deployment into cyber-physical and internet-of-things applications. The key technical contributions of this project are in its formal models of intermittent computing, starting with a sequential model, then extending to concurrent operations in the presence of peripheral devices with timing requirements. These models characterize system behavior precisely, allowing for correctness proofs of deployed systems. Adapting these models to scheduling, this project develops the first provably correct energy collection and computation scheduler for intermittent systems. The project establishes rules for verifying feasibility of a set of computing tasks with respect to energy constraints, and allows for graceful degradation when no schedule is feasible. Benchmarks produced by this project aggregate and thoroughly characterize independently developed applications, enabling direct comparison between systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.