SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 10:00 - 10:20 at SPLASH-I - R-2 Chair(s): Adrian Sampson, Sheng Chen
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
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.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: R-2OOPSLA at SPLASH-I +12h
Chair(s): Adrian SampsonCornell University, Sheng ChenUniversity of Louisiana at Lafayette
09:00 - 09:20
Talk
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
09:20 - 09:40
Talk
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
09:40 - 10:00
Talk
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
10:00 - 10:20
Talk
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached
21:00 - 22:20: R-2OOPSLA at SPLASH-I
Chair(s): Sheng ChenUniversity of Louisiana at Lafayette, John Peter CamporaUniversity of Louisiana at Lafayette
21:00 - 21:20
Talk
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
21:20 - 21:40
Talk
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
21:40 - 22:00
Talk
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
22:00 - 22:20
Talk
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached