Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Fri 25 Oct 2019 11:22 - 11:45 at Olympia - Concurrency Chair(s): Sophia Drossopoulou

Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM).
To describe the persistency guarantees of NVM, several memory persistency models
have been proposed in the literature.
However, the formal persistency semantics of mainstream hardware is unexplored to date.
To close this gap, we present a formal declarative framework for describing concurrency models in the NVM context, and then develop the PARMv8 persistency model as an instance of our framework, formalising the persistency semantics of the ARMv8 architecture for the first time.
To facilitate correct persistent programming, we study transactions as a simple abstraction for concurrency and persistency control.
We thus develop the PSER (persistent serialisability) persistency model, formalising transactional semantics in the NVM context for the first time,
and demonstrate that PSER correctly compiles to PARMv8.
This then enables programmers to write correct, concurrent and persistent programs, without having to understand the low-level architecture-specific persistency semantics of the underlying hardware.

Fri 25 Oct

splash-2019-oopsla
11:00 - 12:30: OOPSLA - Concurrency at Olympia
Chair(s): Sophia DrossopoulouImperial College London
splash-2019-oopsla11:00 - 11:22
Talk
Yoav ZurielTechnion - Israel, Michal FriedmanTechnion - Israel, Gali SheffiTechnion - Israel, Nachshon CohenAmazon, Erez PetrankTechnion - Israel
DOI
splash-2019-oopsla11:22 - 11:45
Talk
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Viktor VafeiadisMPI-SWS, Germany
DOI
splash-2019-oopsla11:45 - 12:07
Talk
Vimuth FernandoUniversity of Illinois at Urbana-Champaign, Keyur JoshiUniversity of Illinois at Urbana-Champaign, Sasa MisailovicUniversity of Illinois at Urbana-Champaign
DOI
splash-2019-oopsla12:07 - 12:30
Talk
Kaan GençOhio State University, Jake RoemerOhio State University, Yufan XuOhio State University, Michael BondOhio State University
DOI Pre-print