Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 16:40 - 16:50 at POPL-B - Concurrency (Shared Memory)

We study the formal semantics of non-volatile memory in the x86-TSO architecture. We show that while the recent model of Raad et al. from POPL’20 has asynchronous explicit persist operations, it is equivalent, in terms of reachable states, to a (novel) model with synchronous operations, which is much closer to common developers’ understanding of persistency semantics. We further introduce a simpler and stronger sequentially consistent persistency model, develop a sound mapping from the this stronger model to x86, and establish a data-race-freedom guarantee providing programmers with a safe programming discipline. Our operational models are accompanied with equivalent declarative formulations, which facilitate our formal arguments, and may prove useful for program verification under x86 persistency.

Thu 21 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Concurrency (Shared Memory)POPL at POPL-B
16:00
10m
Talk
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Roy Margalit Tel Aviv University, Israel, Ori Lahav Tel Aviv University
Link to publication DOI
16:10
10m
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin Arora CMU, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
Link to publication DOI
16:20
10m
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. Muller Illinois Institute of Technology, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
16:30
10m
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40
10m
Talk
Taming x86-TSO Persistency
POPL
Artem Khyzha Tel Aviv University, Ori Lahav Tel Aviv University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL