Towards a Formal Foundation of Intermittent Computing
Thu 19 Nov 2020 22:00 - 22:20 at SPLASH-I - R-2 Chair(s): Sheng Chen, John Peter Campora
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
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.
Thu 19 NovDisplayed time zone: Central Time (US & Canada) change
21:00 - 22:20
R-2OOPSLA at SPLASH-I
Chair(s): Sheng Chen University of Louisiana at Lafayette, John Peter Campora University of Louisiana at Lafayette
|Automatic and Efficient Variability-Aware Lifting of Functional Programs|
Ramy Shahin University of Toronto, Marsha Chechik University of TorontoLink to publication DOI Pre-print Media Attached
|Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs|
Alejandro Gómez-Londoño Chalmers University of Technology, Johannes Åman Pohjola Data61 at CSIRO / UNSW, Hira Taqdees Syeda Chalmers University of Technology, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Carnegie Mellon UniversityLink to publication DOI Media Attached
|Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell|
Yiyun Liu University of Maryland at College Park, James Parker University of Maryland at College Park, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Michael Hicks University of Maryland at College Park, Niki Vazou IMDEA Software InstituteLink to publication DOI Media Attached
|Towards a Formal Foundation of Intermittent Computing|
Milijana Surbatovich Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, Limin Jia Carnegie Mellon UniversityLink to publication DOI Media Attached