Dataflow architectures have gained renewed interest due to their balance between energy efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, which greatly improves data locality and parallelism. However, compiling to dataflow architectures remains an error-prone process, due to the difficulty of maintaining determinacy while enabling pipelining . Determinacy means that the result of a dataflow program is deterministic and independent of the schedule of operator execution, and pipelining is an important optimization in spatial dataflow that enables parallelism across loop iterations. In this work, we present Wavelet, the first effort to formally verify a compiler for asynchronous dataflow. We use a mix of techniques to achieve this goal. Our frontend uses a novel capability type system with fences to synchronize conflicting memory accesses and enable pipelining . We then verify a Lean formalization of two core compiler passes that translate elaborated programs from the type checker to dataflow graphs, proving important properties of forward simulation and determinacy . Notably, our formalization semantically propagates the soundness guarantees of the frontend type system, ensuring modularity between simulation and determinacy proofs. In our evaluation, we show that dataflow graphs compiled by Wavelet have comparable quality to those produced by unverified dataflow compilers from RipTide and LLVM CIRCT.

Programs are executed intermittently on devices that experience arbitrary power failures such as Energy Harvesting Devices (EHDs). 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 accommodate 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.

Abstract Intermittent computing is gaining traction in application domains such as Energy Harvesting Devices (EHDs) that experience arbitrary power failures during program execution. To make progress, programs require system support to checkpoint state and re-execute after power failure by restoring the last saved state. This re-execution should becorrect, 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. We define a Crash type system for a core calculus. We prove the correctness of intermittent systems by defining a novel logical relation for Crash types.

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 re-execution 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 non-idempotence). 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.

Energy-harvesting devices eliminate batteries, instead collecting their operating energy from environmental sources. A device stores energy into a capacitor, drawing energy to perform tasks and powering off to recharge when the energy is exhausted. State-of-the-art charge management systems for these devices aim to avoid power failure during task execution by reasoning about task energy cost. We identify that the innate equivalent series resistance (ESR) in energy storage capacitors breaks energy-based systems’ guarantees; running high current load on a high-ESR capacitor causes a substantial voltage drop that rebounds once the load is removed. This voltage drop is disregarded by systems that only reason about energy. If the drop lowers the voltage below the system’s operating threshold, however, the device powers off while stored energy remains. Though ESR is well understood in hardware design, this is the first work to argue that software for batteryless devices must also be aware of ESR.This work presents Culpeo, a hardware/software mechanism and architectural interface to relay the effect of ESR in the power system to software. We develop static and dynamic implementations of Culpeo and demonstrate on real batteryless devices that considering ESR restores correctness guarantees broken by energy-only charge management. We then demonstrate how to integrate Culpeo’s safe voltage into state-of-the-art schedulers, restoring task deadline guarantees for applications with predictable energy harvesting. Finally, we propose an on-chip Culpeo hardware implementation that allows for runtime monitoring of the effects of ESR to respond to changes in harvestable power.

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.

Intermittently powered devices enable new applications in harsh or inaccessible environments, such as space or in-body implants, but also introduce problems in programmability and correctness. Researchers have developed programming models to ensure that programs make progress and do not produce erroneous results due to memory inconsistencies caused by intermittent executions. As the technology has matured, more and more features are added to intermittently powered devices, such as I/O. Prior work has shown that all existing intermittent execution models have problems with repeated device or sensor inputs (RIO). RIOs could leave intermittent executions in an inconsistent state. Such problems and the proliferation of existing intermittent execution models necessitate a formal foundation for intermittent computing. In this paper, we formalize intermittent execution models, their correctness properties with respect to memory consistency and inputs, and identify the invariants needed to prove systems correct. We prove equivalence between several existing intermittent systems. To address RIO problems, we define an algorithm for identifying variables affected by RIOs that need to be restored after reboot and prove the algorithm correct. Finally, we implement the algorithm in a novel intermittent runtime system that is correct with respect to input operations and evaluate its performance.

Intermittently-powered, energy-harvesting devices operate on energy collected from their environment and must operate intermittently as energy is available. Runtime systems for such devices often rely on checkpoints or redo-logs to save execution state between power cycles, causing arbitrary code regions to re-execute on reboot. Any non-idempotent program behavior—behavior that can change on each execution—can lead to incorrect results. This work investigates non-idempotent behavior caused by repeating I/O operations, not addressed by prior work. If such operations affect a control statement or address of a memory update, they can cause programs to take different paths or write to different memory locations on re-executions, resulting in inconsistent memory states. We provide the first characterization of input-dependent idempotence bugs and develop IBIS-S, a program analysis tool for detecting such bugs at compile time, and IBIS-D, a dynamic information flow tracker to detect bugs at runtime. These tools use taint propagation to determine the reach of input. IBIS-S searches for code patterns leading to inconsistent memory updates, while IBIS-D detects concrete memory inconsistencies. We evaluate IBIS on embedded system drivers and applications. IBIS can detect I/O-dependent idempotence bugs, giving few (IBIS-S) or no (IBIS-D) false positives and providing actionable bug reports. These bugs are common in sensor-driven applications and are not fixed by existing intermittent systems.

The use of end-user programming, such as if-this-then-that (IFTTT), is becoming increasingly common. Services like IFTTT allow users to easily create new functionality by connecting arbitrary Internet-of-Things (IoT) devices and online services using simple if-then rules, commonly known as recipes. However, such convenience at times comes at the cost of security and privacy risks for end users. To gain an in-depth understanding of the potential security and privacy risks, we build an information-flow model to analyze how often IFTTT recipes involve potential integrity or secrecy violations. Our analysis finds that around 50% of the 19,323 unique recipes we examined are potentially unsafe, as they contain a secrecy violation, an integrity violation, or both. We next categorize the types of harm that these potentially unsafe recipes can cause to users. After manually examining a random selection of potentially unsafe recipes, we find that recipes can not only lead to harms such as personal embarrassment but can also be exploited by an attacker, e.g., to distribute malware or carry out denial-of-service attacks. The use of IoT devices and services like IFTTT is expected only to grow in the near future; our analysis suggests users need to be both informed about and protected from these emerging threats to which they could be unwittingly exposing themselves.