Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
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. 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 show that these properties can be enforced using atomic regions. We develop Ocelot, an LLVM-based analysis and transformation tool targeting Rust, to automatically enforce these properties. Ocelot provides the programmer with annotations to express these constraints and infers atomic region placement in a program to satisfy them. We formalize these properties and Ocelot’s design and show that Ocelot enables correct execution at little performance cost and low programmer effort.
Thu 21 OctDisplayed time zone: Central Time (US & Canada) change
15:40 - 17:00 | |||
15:40 15mTalk | Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems SIGPLAN Papers Milijana Surbatovich Carnegie Mellon University, Limin Jia Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, USA | ||
15:55 15mTalk | IOOpt- Automatic Derivation of I/O complexity bounds for affine programs SIGPLAN Papers Auguste Olivry Inria, France, Guillaume Iooss Inria, Nicolas Tollenaere Inria, Atanas Rountev Ohio State University, Saday Sadayappan University of Utah, USA, Fabrice Rastello Inria, France | ||
16:10 15mTalk | Integration Verification Across Software and Hardware for a Simple Embedded System SIGPLAN Papers Andres Erbsen MIT, Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, USA, Clark Wood Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology | ||
16:25 15mTalk | Execution reconstruction: Harnessing failure reoccurrences for failure reproduction SIGPLAN Papers Gefei Zuo University of Michigan, Jiacheng Ma University of Michigan, Andrew Quinn University of Michigan, Pramod Bhatotia University of Edinburgh, Pedro Fonseca Purdue University, Baris Kasikci University of Michigan, USA | ||
16:40 20mLive Q&A | Discussion, Questions and Answers SIGPLAN Papers |