Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems

TL;DR

This paper introduces Ocelot, a tool that automatically enforces freshness and temporal consistency constraints on inputs in intermittently powered systems, ensuring robustness without significant performance overhead.

Contribution

It formalizes input constraints for intermittent systems and develops Ocelot, an LLVM-based tool that automatically enforces these constraints in Rust programs.

Findings

Ocelot effectively enforces input constraints with minimal performance impact.

Formalization of freshness and temporal consistency properties for intermittent systems.

Ocelot requires only annotations and infers atomic regions automatically.

Abstract

Intermittently powered energy-harvesting devices enable new applications in inaccessible environments. Program executions must be robust to unpredictable power failures, introducing new challenges in programmability and correctness. One hard problem is that input operations have implicit constraints, embedded in the behavior of continuously powered executions, on when input values can be collected and used. This paper aims to develop a formal framework for enforcing these constraints. We identify two key properties -- freshness (i.e., uses of inputs must satisfy the same time constraints as in continuous executions) and temporal consistency (i.e., the collection of a set of inputs must satisfy the same time constraints as in continuous executions). We formalize these properties and show that they can be enforced using atomic regions. We develop Ocelot, an LLVM-based analysis and transformation tool targeting Rust, to enforce these properties automatically. Ocelot provides the programmer with annotations to express these constraints and infers atomic region placement in a program to satisfy them. We then formalize Ocelot's design and show that Ocelot generates correct programs with little performance cost or code changes.