Write a Blog >>
Wed 22 Jan 2020 15:35 - 15:56 at Ile de France III (IDF III) - Concurrency / Memory Chair(s): Susmit Sarkar

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. However, the persistency semantics of the ubiquitous x86 architecture remains unexplored to date. To close this gap, we develop the Px86 (‘persistent x86’) model, formalising the persistency semantics of x86 for the first time. We formulate Px86 both operationally and declaratively, and prove that the two characterisations are equivalent. To demonstrate the application of Px86 and to make persistent programming accessible to the uninitiated programmer, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael-Scott queue library. We further showcase the application of Px86 by encoding it in Alloy and generating persistency litmus tests automatically.

Wed 22 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: Research Papers - Concurrency / Memory at Ile de France III (IDF III)
Chair(s): Susmit SarkarUniversity of St. Andrews
POPL-2020-Research-Papers15:35 - 15:56
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany
Link to publication DOI Media Attached
POPL-2020-Research-Papers15:56 - 16:18
Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto
Link to publication DOI Media Attached
POPL-2020-Research-Papers16:18 - 16:40
Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWS
Link to publication DOI Media Attached