{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:51:43Z","timestamp":1773193903137,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["683289"],"award-info":[{"award-number":["683289"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/R006865\/1"],"award-info":[{"award-number":["EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<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 (\u2018persistent x86\u2019) 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\u2013Scott queue. Finally, we encode our declarative Px86 model in Alloy and use it to generate persistency litmus tests automatically.<\/jats:p>","DOI":"10.1145\/3371079","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Persistency semantics of the Intel-x86 architecture"],"prefix":"10.1145","volume":"4","author":[{"given":"Azalea","family":"Raad","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Gil","family":"Neiger","sequence":"additional","affiliation":[{"name":"Intel Labs, USA"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_41"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2926697.2926704"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660224"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.14778\/2735479.2735483"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192373"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950380"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629589"},{"key":"e_1_2_2_9_1","volume-title":"https:\/\/pcollections.org\/","author":"Cooper Harold","year":"2008"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178490"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/325096.325102"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192367"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_14_1","unstructured":"Intel. 2014. Intel architecture instruction set extensions programming reference. (2014). https:\/\/software.intel.com\/sites\/ default\/files\/managed\/07\/b7\/319433- 023.pdf  Intel. 2014. Intel architecture instruction set extensions programming reference. (2014). https:\/\/software.intel.com\/sites\/ default\/files\/managed\/07\/b7\/319433- 023.pdf"},{"key":"e_1_2_2_15_1","unstructured":"Intel. 2015. Persistent Memory Programming. (2015). http:\/\/pmem.io\/  Intel. 2015. Persistent Memory Programming. (2015). http:\/\/pmem.io\/"},{"key":"e_1_2_2_16_1","volume-title":"https:\/\/www.intel.com\/content\/www\/us\/en\/architecture- and- technology\/intel- optanetechnology.html","author":"Point D","year":"2019"},{"key":"e_1_2_2_17_1","volume-title":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (Combined Volumes). (May","year":"2019"},{"key":"e_1_2_2_18_1","unstructured":"ITRS. 2011. Process Integration devices and structures. (2011). http:\/\/www.maltiel- consulting.com\/ITRS_2011- ProcessIntegration- Devices- Structures.pdf International technology roadmap for semiconductors.  ITRS. 2011. Process Integration devices and structures. (2011). http:\/\/www.maltiel- consulting.com\/ITRS_2011- ProcessIntegration- Devices- Structures.pdf International technology roadmap for semiconductors."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872410"},{"key":"e_1_2_2_20_1","volume-title":"Scott","author":"Izraelevitz Joseph","year":"2016"},{"key":"e_1_2_2_21_1","volume-title":"Software Abstractions \u2013 Logic, Language, and Analysis (revised edition ed.)","author":"Jackson Daniel"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2018.00035"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830805"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.microrel.2011.09.028"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360599"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080229"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2954679.2872381"},{"key":"e_1_2_2_29_1","volume-title":"Delegated Persist Ordering. In The 49th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO-49)","author":"Kolli Aasheesh","year":"1956"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555758"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304015"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.77"},{"key":"e_1_2_2_36_1","volume-title":"Dal\u00ed: A Periodically Persistent Hash Map. In DISC.","author":"Nawab Faisal","year":"2017"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884011"},{"key":"e_1_2_2_38_1","unstructured":"PCJ. 2016. Persistent Collections for Java. (2016). https:\/\/github.com\/pmem\/pcj  PCJ. 2016. Persistent Collections for Java. (2016). https:\/\/github.com\/pmem\/pcj"},{"key":"e_1_2_2_39_1","volume-title":"Memory Persistency. In Proceeding of the 41st Annual International Symposium on Computer Architecuture (ISCA \u201914)","author":"Pelley Steven"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"key":"e_1_2_2_41_1","volume-title":"On Parallel Snapshot Isolation and Release\/Acquire Consistency","author":"Raad Azalea"},{"key":"e_1_2_2_42_1","volume-title":"On the Semantics of Snapshot Isolation","author":"Raad Azalea"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/NVMSA.2018.00015"},{"key":"e_1_2_2_47_1","volume-title":"The SPARC Architecture Manual: Version 8","author":"SPARC."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature06932"},{"key":"e_1_2_2_49_1","volume-title":"Enabling Efficient RDMA-based Synchronous Mirroring of Persistent Memory Transactions. CoRR abs\/1810.09360","author":"Tavakkol Arash","year":"2018"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2248487.1950379"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2063384.2063436"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2540708.2540744"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360554"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371079","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371079","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371079"],"URL":"https:\/\/doi.org\/10.1145\/3371079","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}