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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 10mTalk | Verifying Observational Robustness Against a C11-style Memory Model POPL Link to publication DOI | ||
16:10 10mTalk | Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper POPL Link to publication DOI | ||
16:20 10mTalk | Modeling and Analyzing Evaluation Cost of CUDA Kernels POPL Link to publication DOI | ||
16:30 10mTalk | 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 10mTalk | Taming x86-TSO Persistency POPL Link to publication DOI Pre-print | ||
16:50 10mBreak | Break POPL |