Doctoral Thesis Proposal - Myra Dotzel
— 2:00pm
Location:
In Person
-
Reddy Conference Room, Gates Hillman 4405
Speaker:
MYRA DOTZEL
,
Ph.D. Student
Computer Science Department
Carnegie Mellon University
https://www.andrew.cmu.edu/user/mdotzel/
Intermittent computing is gaining popularity in applications that rely on batteryless energy-harvesting devices which experience frequent and arbitrary power failures. To enable correct program re-execution despite these potentially frequent and arbitrary power failures, runtime support is needed to save and restore necessary state.
In this talk, we study the formal foundations of intermittent computing by use of type systems to guarantee the correctness of programs prior to their deployment, and runtime systems to facilitate correct program execution, including support for sequential and concurrent models of execution.
First, we explore the logical underpinning of sequential, intermittent computing and model checkpoint, crash, restore, and re-execution operations as computation on crash types. We draw inspiration from adjoint logic to reason about the relationship between persistent and transient memories through (re-)execution, checkpointing, and restoration. Using crash types, we show that any correct intermittent execution can be simulated by a continuously-powered execution.
Second, we present the first provably-correct system for concurrent, intermittent program execution, which is needed as many embedded applications rely on interactions with hardware-triggered interrupts and accesses to shared memory. Prior work on concurrent, intermittent execution has only provided restrictive programming models with no formal correctness guarantees. In this talk, we present a co-designed runtime system and type system that together support the provably correct intermittent execution of task-based concurrent programs with 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, Illinois Institute of Technology)
Frank Pfenning
Jan Hoffmann
Brigitte Pientka (McGill University)
For More Information:
matthewstewart@cmu.edu