Thu 8 Nov 2018 11:15 - 11:37 at Studio 1 - Weak Memory and Refactoring Chair(s): Richard Jones

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 semantics of such persistency models in the context We demonstrate that the two characterisations of PTSO are equivalent. We then formulate the notion of persistent linearisability to establish the correctness of library implementations in the context of persistent memory. To showcase our formalism, we develop two persistent implementations of a queue library, and apply persistent linearisability to show their correctness.

Thu 8 Nov
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

10:30 - 12:00: OOPSLA - Weak Memory and Refactoring at Studio 1
Chair(s): Richard JonesUniversity of Kent
splash-2018-OOPSLA10:30 - 10:52
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Bengt JonssonUppsala University, Tuan Phong NgoUppsala University
splash-2018-OOPSLA10:52 - 11:15
Peizhao OuUniversity of California, Irvine, Brian DemskyUniversity of California, Irvine
splash-2018-OOPSLA11:15 - 11:37
Azalea RaadMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany
splash-2018-OOPSLA11:37 - 12:00