Doctoral Thesis Oral Defense - Myra Lily Sun Dotzel
August 17, 2026 2:00PM—4:00PM
Location:
4405 and Zoom
-
Gates and Hillman Centers
Speaker:
MYRA LILY SUN DOTZEL,
Ph.D. Candidate, Computer Science Department, Carnegie Mellon University
https://www.andrew.cmu.edu/user/mdotzel/
Intermittent computing enables applications to thrive in energy-scarce and inaccessible environments, where manual device maintenance is infeasible. Instead of relying on batteries, devices in these applications are instead powered by energy from the environment. They harvest energy from the environment into a rechargeable buffer, compute when energy is available, and power off when energy is depleted, halting program execution until more energy can be retrieved. To enable correct program re-execution despite these potentially frequent and arbitrary power failures, runtime support is needed to save and restore necessary state.
This thesis lays a logical foundation for intermittent computing by building type systems and runtime systems to guarantee correct program execution across diverse features and behaviors, including sequential and concurrent execution, as well as inputs and effectful outputs. First, we explore sequential, intermittent computing and model checkpoint, crash, restore, and re-execute operations as computation on crash types. We draw inspiration from adjoint logic and define crash types by introducing two adjoint modality operators to model operations on nonvolatile and volatile memories. 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. Throughout this thesis, we extend crash types to consider more realistic program and system behaviors, such as more flexible checkpointing policies, common logging styles, I/O and branching.
Lastly, we provide the first provably-correct system for concurrent, intermittent program execution, which is needed for supporting hardware-triggered interrupts and accesses to shared memory which are common to many embedded systems applications. We present a co-designed runtime system and type system that together support the provably correct intermittent execution of concurrent programs running on shared memory. This system promotes a more flexible programming model and supports a broader spectrum of task re-execution behaviors than is considered by prior work. We provide the first formal definition and proofs of correctness for concurrent, intermittent execution.
Thesis Committee:
Limin Jia (Co-Chair)
Farzaneh Derakhshan (Co-Chair)
Frank Pfenning
Jan Hoffmann
Brigitte Pientka (McGill University)
In-person & Zoom
Contact
Matt Stewart