Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models
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 OctDisplayed time zone: Beirut change
11:00 - 12:30
|Efficient Lock-Free Durable Sets|
Yoav Zuriel Technion - Israel, Michal Friedman Technion - Israel, Gali Sheffi Technion - Israel, Nachshon Cohen Amazon, Erez Petrank Technion - IsraelDOI
|Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models|
Azalea Raad MPI-SWS, Germany, John Wickerson Imperial College London, Viktor Vafeiadis MPI-SWS, GermanyDOI
|Verifying Safety and Accuracy of Approximate Parallel Programs via Canonical Sequentialization|
Vimuth Fernando University of Illinois at Urbana-Champaign, Keyur Joshi University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-ChampaignDOI
|Dependence-Aware, Unbounded Sound Predictive Race Detection|
Kaan Genç Ohio State University, Jake Roemer Ohio State University, Yufan Xu Ohio State University, Michael D. Bond Ohio State UniversityDOI Pre-print