Taming x86-TSO Persistency (Extended Version)
Artem Khyzha, Ori Lahav

TL;DR
This paper provides a formal analysis of x86-TSO persistency models, introducing a simpler, stronger model closer to developers' intuition, along with a safe programming discipline and verification tools.
Contribution
It introduces a new, more intuitive persistency model for x86-TSO, along with a formal mapping and data-race-freedom guarantees for safer programming.
Findings
Explicit persist operations enforce order between writes.
The new model is closer to developers' understanding.
A safe programming discipline is established.
Abstract
We study the formal semantics of non-volatile memory in the x86-TSO architecture. We show that while the explicit persist operations in the recent model of Raad et al. from POPL'20 only enforce order between writes to the non-volatile memory, it is equivalent, in terms of reachable states, to a model whose explicit persist operations mandate that prior writes are actually written to the non-volatile memory. The latter provides a novel model that 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 this 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Distributed systems and fault tolerance · Advanced Data Storage Technologies
