{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:30:33Z","timestamp":1770291033532,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R006865\/1"],"award-info":[{"award-number":["EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ERC","award":["683289"],"award-info":[{"award-number":["683289"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, the formal persistency semantics of mainstream hardware is unexplored to date. To close this gap, we present a formal declarative framework for describing concurrency models in the NVM context, and then develop the PARMv8 persistency model as an instance of our framework, formalising the persistency semantics of the ARMv8 architecture for the first time. To facilitate correct persistent programming, we study transactions as a simple abstraction for concurrency and persistency control. We thus develop the PSER (persistent serialisability) persistency model, formalising transactional semantics in the NVM context for the first time, and demonstrate that PSER correctly compiles to PARMv8. This then enables programmers to write correct, concurrent and persistent programs, without having to understand the low-level architecture-specific persistency semantics of the underlying hardware.<\/jats:p>","DOI":"10.1145\/3360561","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models"],"prefix":"10.1145","volume":"3","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":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994593"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"e_1_2_2_4_1","unstructured":"ARM. 2018. ARM architecture reference manual ARMv8 for ARMv8-A architecture profile (DDI 0487D.a). https: \/\/static.docs.arm.com\/ddi0487\/da\/DDI0487D_a_armv8_arm.pdf  ARM. 2018. ARM architecture reference manual ARMv8 for ARMv8-A architecture profile (DDI 0487D.a). https: \/\/static.docs.arm.com\/ddi0487\/da\/DDI0487D_a_armv8_arm.pdf"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_41"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2926697.2926704"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872406"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660224"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.14778\/2735479.2735483"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192373"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950380"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629589"},{"key":"e_1_2_2_14_1","unstructured":"Harold Cooper. 2008. Persistent collections. https:\/\/pcollections.org\/  Harold Cooper. 2008. Persistent collections. https:\/\/pcollections.org\/"},{"key":"e_1_2_2_15_1","unstructured":"Niall Douglas. 2018. P1026R0: A call for a data persistence (iostream v2) study group. http:\/\/www.open- std.org\/jtc1\/sc22\/ wg21\/docs\/papers\/2018\/p1026r0.pdf  Niall Douglas. 2018. P1026R0: A call for a data persistence (iostream v2) study group. http:\/\/www.open- std.org\/jtc1\/sc22\/ wg21\/docs\/papers\/2018\/p1026r0.pdf"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/325096.325102"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192367"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_19_1","unstructured":"Intel. 2014. Intel architecture instruction set extensions programming reference. https:\/\/software.intel.com\/sites\/default\/ files\/managed\/07\/b7\/319433- 023.pdf  Intel. 2014. Intel architecture instruction set extensions programming reference. https:\/\/software.intel.com\/sites\/default\/ files\/managed\/07\/b7\/319433- 023.pdf"},{"key":"e_1_2_2_20_1","unstructured":"Intel. 2015. Persistent memory programming. http:\/\/pmem.io\/  Intel. 2015. Persistent memory programming. http:\/\/pmem.io\/"},{"key":"e_1_2_2_21_1","unstructured":"Intel. 2019. Intel 64 and IA-32 architectures software developer\u2019s manual (Combined volumes). https:\/\/software.intel.com\/ sites\/default\/files\/managed\/39\/c5\/325462- sdm- vol- 1- 2abcd- 3abcd.pdf  Intel. 2019. Intel 64 and IA-32 architectures software developer\u2019s manual (Combined volumes). https:\/\/software.intel.com\/ sites\/default\/files\/managed\/39\/c5\/325462- sdm- vol- 1- 2abcd- 3abcd.pdf"},{"key":"e_1_2_2_22_1","unstructured":"ITRS. 2011. Process integration devices and structures. http:\/\/www.maltiel- consulting.com\/ITRS_2011- Process- IntegrationDevices- Structures.pdf International technology roadmap for semiconductors.  ITRS. 2011. Process integration devices and structures. http:\/\/www.maltiel- consulting.com\/ITRS_2011- Process- IntegrationDevices- Structures.pdf International technology roadmap for semiconductors."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872410"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_2_2_25_1","volume-title":"Software abstractions \u2013 Logic, language, and analysis (revised ed.)","author":"Jackson Daniel"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2018.00035"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830805"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.microrel.2011.09.028"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080229"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2954679.2872381"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2016.7783761"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555758"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304015"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2017.37"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_2_39_1","unstructured":"PCJ. 2016. Persistent collections for Java. https:\/\/github.com\/pmem\/pcj  PCJ. 2016. Persistent collections for Java. https:\/\/github.com\/pmem\/pcj"},{"key":"e_1_2_2_40_1","volume-title":"41st Annual International Symposium on Computer Architecuture (ISCA","author":"Pelley Steven","year":"2014"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_33"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_1"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/NVMSA.2018.00015"},{"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\/3009837.3009838"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2063384.2063436"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2540708.2540744"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360561","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360561","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360561"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":53,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360561"],"URL":"https:\/\/doi.org\/10.1145\/3360561","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}