-
- Azalea Raad
- MPI-SWS, Germany
-
- John Wickerson
- Imperial College London, UK
-
- Gil Neiger
- Intel Labs, USA
-
- Viktor Vafeiadis
- MPI-SWS, Germany
抄録
<jats:p>Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of RAM. To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. 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 Intel-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, we develop two persistent libraries over Px86: a persistent transactional library, and a persistent variant of the Michael–Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.</jats:p>
収録刊行物
-
- Proceedings of the ACM on Programming Languages
-
Proceedings of the ACM on Programming Languages 4 (POPL), 1-31, 2019-12-20
Association for Computing Machinery (ACM)
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1362825895163012096
-
- DOI
- 10.1145/3371079
-
- ISSN
- 24751421
-
- データソース種別
-
- Crossref