{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:51:44Z","timestamp":1773193904730,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100010418","name":"Institute for Information and communications Technology Promotion","doi-asserted-by":"publisher","award":["2019-0-00118"],"award-info":[{"award-number":["2019-0-00118"]}],"id":[{"id":"10.13039\/501100010418","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454027","type":"proceedings-article","created":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T13:51:32Z","timestamp":1624024292000},"page":"16-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3685-2320","authenticated-orcid":false,"given":"Kyeongmin","family":"Cho","sequence":"first","affiliation":[{"name":"KAIST, South Korea"}]},{"given":"Sung-Hwan","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2115-0871","authenticated-orcid":false,"given":"Jeehoon","family":"Kang","sequence":"additional","affiliation":[{"name":"KAIST, South Korea"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2020. The Coq Proof Assistant. https:\/\/coq.inria.fr\/  2020. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_3_2_1_2_1","volume-title":"A Formal Hierarchy of Weak Memory Models. Form. Methods Syst. Des., 41, 2","author":"Alglave Jade","year":"2012","unstructured":"Jade Alglave . 2012. A Formal Hierarchy of Weak Memory Models. Form. Methods Syst. Des., 41, 2 ( 2012 ). Jade Alglave. 2012. A Formal Hierarchy of Weak Memory Models. Form. Methods Syst. Des., 41, 2 (2012)."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_4_1","unstructured":"Arm. 2020. Arm architecture reference manual Armv8 for Armv8-A architecture profile (DDI 0487F.b). https:\/\/static.docs.arm.com\/ddi0487\/fb\/DDI0487F_b_armv8_arm.pdf  Arm. 2020. Arm architecture reference manual Armv8 for Armv8-A architecture profile (DDI 0487F.b). https:\/\/static.docs.arm.com\/ddi0487\/fb\/DDI0487F_b_armv8_arm.pdf"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_41"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374506"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660224"},{"key":"e_1_3_2_1_9_1","unstructured":"Kyeongmin Cho Sung-Hwan Lee Azalea Raad and Jeehoon Kang. 2021. Appendix for Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8. https:\/\/cp.kaist.ac.kr\/pmem  Kyeongmin Cho Sung-Hwan Lee Azalea Raad and Jeehoon Kang. 2021. Appendix for Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8. https:\/\/cp.kaist.ac.kr\/pmem"},{"key":"#cr-split#-e_1_3_2_1_10_1.1","doi-asserted-by":"crossref","unstructured":"Kyeongmin Cho Sung-Hwan Lee Azalea Raad and Jeehoon Kang. 2021. Artifact for Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8. https:\/\/doi.org\/10.1145\/3410292 10.1145\/3410292","DOI":"10.1145\/3410292"},{"key":"#cr-split#-e_1_3_2_1_10_1.2","doi-asserted-by":"crossref","unstructured":"Kyeongmin Cho Sung-Hwan Lee Azalea Raad and Jeehoon Kang. 2021. Artifact for Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8. https:\/\/doi.org\/10.1145\/3410292","DOI":"10.1145\/3410292"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629589"},{"key":"e_1_3_2_1_12_1","unstructured":"CCIX Consortium. [n.d.]. Cache Coherent Interconnect for Accelerators. https:\/\/www.ccixconsortium.com\/  CCIX Consortium. [n.d.]. Cache Coherent Interconnect for Accelerators. https:\/\/www.ccixconsortium.com\/"},{"key":"e_1_3_2_1_13_1","unstructured":"CXL Consortium. [n.d.]. Compute Express Link. https:\/\/www.computeexpresslink.org\/  CXL Consortium. [n.d.]. Compute Express Link. https:\/\/www.computeexpresslink.org\/"},{"key":"e_1_3_2_1_14_1","volume-title":"Formal Methods \u2013 The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N","author":"Derrick John","unstructured":"John Derrick , Simon Doherty , Brijesh Dongol , Gerhard Schellhorn , and Heike Wehrheim . 2019. Verifying Correctness of Persistent Concurrent Data Structures . In Formal Methods \u2013 The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N . Oliveira (Eds.). Springer International Publishing , Cham . 179\u2013195. John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. 2019. Verifying Correctness of Persistent Concurrent Data Structures. In Formal Methods \u2013 The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N. Oliveira (Eds.). Springer International Publishing, Cham. 179\u2013195."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178490"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/325096.325102"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192367"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629619"},{"key":"e_1_3_2_1_19_1","unstructured":"Intel. 2015. Persistent Memory Programming. https:\/\/pmem.io\/  Intel. 2015. Persistent Memory Programming. https:\/\/pmem.io\/"},{"key":"e_1_3_2_1_20_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 Order Number: 325462-069US.  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 Order Number: 325462-069US."},{"key":"e_1_3_2_1_21_1","unstructured":"Intel. 2019. Intel\u00ae Optane\u2122 Persistent Memory. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/optane-dc-persistent-memory.html  Intel. 2019. Intel\u00ae Optane\u2122 Persistent Memory. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/optane-dc-persistent-memory.html"},{"key":"e_1_3_2_1_22_1","unstructured":"Intel. 2020. Intel\u00ae Optane\u2122 Persistent Memory 200 Series Product Specifications. https:\/\/ark.intel.com\/content\/www\/us\/en\/ark\/products\/series\/203877\/intel-optane-persistent-memory-200-series.html  Intel. 2020. Intel\u00ae Optane\u2122 Persistent Memory 200 Series Product Specifications. https:\/\/ark.intel.com\/content\/www\/us\/en\/ark\/products\/series\/203877\/intel-optane-persistent-memory-200-series.html"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_3_2_1_24_1","volume-title":"Zixuan Wang, Yi Xu, Subramanya R. Dulloor, Jishen Zhao, and Steven Swanson.","author":"Izraelevitz Joseph","year":"2019","unstructured":"Joseph Izraelevitz , Jian Yang , Lu Zhang , Juno Kim , Xiao Liu , Amirsaman Memaripour , Yun Joon Soh , Zixuan Wang, Yi Xu, Subramanya R. Dulloor, Jishen Zhao, and Steven Swanson. 2019 . Basic Performance Measurements of the Intel Optane DC Persistent Memory Module . arxiv:1903.05714. Joseph Izraelevitz, Jian Yang, Lu Zhang, Juno Kim, Xiao Liu, Amirsaman Memaripour, Yun Joon Soh, Zixuan Wang, Yi Xu, Subramanya R. Dulloor, Jishen Zhao, and Steven Swanson. 2019. Basic Performance Measurements of the Intel Optane DC Persistent Memory Module. arxiv:1903.05714."},{"key":"e_1_3_2_1_25_1","unstructured":"Erik Jensen G. W. Hagensen and J. Broughton. 1987. A new approach to exclusive data access in shared memory multiprocessors.  Erik Jensen G. W. Hagensen and J. Broughton. 1987. A new approach to exclusive data access in shared memory multiprocessors."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830805"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434328"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434324"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080229"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872381"},{"key":"e_1_3_2_1_32_1","volume-title":"Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21, 7","author":"Lamport Leslie","year":"1978","unstructured":"Leslie Lamport . 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21, 7 ( 1978 ), July. Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21, 7 (1978), July."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037714"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304015"},{"key":"e_1_3_2_1_37_1","volume-title":"2017 USENIX Annual Technical Conference (USENIX ATC 17)","author":"Lu Youyou","year":"2017","unstructured":"Youyou Lu , Jiwu Shu , Youmin Chen , and Tao Li . 2017 . Octopus: an RDMA-enabled Distributed Persistent Memory File System . In 2017 USENIX Annual Technical Conference (USENIX ATC 17) . USENIX Association, Santa Clara, CA. 773\u2013785. isbn:978-1-93 1971-38-6 https:\/\/www.usenix.org\/conference\/atc17\/technical-sessions\/presentation\/lu Youyou Lu, Jiwu Shu, Youmin Chen, and Tao Li. 2017. Octopus: an RDMA-enabled Distributed Persistent Memory File System. In 2017 USENIX Annual Technical Conference (USENIX ATC 17). USENIX Association, Santa Clara, CA. 773\u2013785. isbn:978-1-931971-38-6 https:\/\/www.usenix.org\/conference\/atc17\/technical-sessions\/presentation\/lu"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851504"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.14778\/3137628.3137629"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Scott Owens Susmit Sarkar and Peter Sewell. 2009. A Better X86 Memory Model: X86-TSO. In TPHOL.  Scott Owens Susmit Sarkar and Peter Sewell. 2009. A Better X86 Memory Model: X86-TSO. In TPHOL.","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_42_1","volume-title":"Memory Persistency. In Proceeding of the 41st Annual International Symposium on Computer Architecuture (ISCA \u201914)","author":"Pelley Steven","unstructured":"Steven Pelley , Peter M. Chen , and Thomas F. Wenisch . 2014 . Memory Persistency. In Proceeding of the 41st Annual International Symposium on Computer Architecuture (ISCA \u201914) . IEEE Press, 265\u2013276. isbn:9781479943944 Steven Pelley, Peter M. Chen, and Thomas F. Wenisch. 2014. Memory Persistency. In Proceeding of the 41st Annual International Symposium on Computer Architecuture (ISCA \u201914). IEEE Press, 265\u2013276. isbn:9781479943944"},{"key":"e_1_3_2_1_43_1","volume-title":"POPL","author":"Pulte Christopher","year":"2017","unstructured":"Christopher Pulte , Shaked Flur , Will Deacon , Jon French , Susmit Sarkar , and Peter Sewell . 2017. Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8. 2 , POPL ( 2017 ), Dec.. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2017. Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8. 2, POPL (2017), Dec.."},{"key":"e_1_3_2_1_44_1","volume-title":"Promising-ARM\/RISC-V: A Simpler and Faster Operational Concurrency Model. In PLDI","author":"Pulte Christopher","year":"2019","unstructured":"Christopher Pulte , Jean Pichon-Pharabod , Jeehoon Kang , Sung-Hwan Lee , and Chung-Kil Hur . 2019 . Promising-ARM\/RISC-V: A Simpler and Faster Operational Concurrency Model. In PLDI 2019. Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur. 2019. Promising-ARM\/RISC-V: A Simpler and Faster Operational Concurrency Model. In PLDI 2019."},{"key":"e_1_3_2_1_45_1","volume-title":"Proc. ACM Program. Lang., 3, OOPSLA","author":"Raad Azalea","year":"2020","unstructured":"Azalea Raad , Ori Lahav , and Viktor Vafeiadis . 2020 . Persistent Owicki-Gries Reasoning . Proc. ACM Program. Lang., 3, OOPSLA (2020). Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2020. Persistent Owicki-Gries Reasoning. Proc. ACM Program. Lang., 3, OOPSLA (2020)."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_3_2_1_49_1","volume-title":"Francesco Zappa Nardelli, and Magnus O. Myreen","author":"Sewell Peter","year":"2010","unstructured":"Peter Sewell , Susmit Sarkar , Scott Owens , Francesco Zappa Nardelli, and Magnus O. Myreen . 2010 . X86-TSO: A Rigorous and Usable Programmer\u2019s Model for X86 Multiprocessors. Commun. ACM , 53, 7 (2010). Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. X86-TSO: A Rigorous and Usable Programmer\u2019s Model for X86 Multiprocessors. Commun. ACM, 53, 7 (2010)."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127479.3128610"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/NVMSA.2018.00015"},{"key":"e_1_3_2_1_52_1","volume-title":"Enabling Efficient RDMA-based Synchronous Mirroring of Persistent Memory Transactions. CoRR, abs\/1810.09360","author":"Tavakkol Arash","year":"2018","unstructured":"Arash Tavakkol , Aasheesh Kolli , Stanko Novakovic , Kaveh Razavi , Juan G\u00f3mez-Luna , Hasan Hassan , Claude Barthels , Yaohua Wang , Mohammad Sadrosadati , Saugata Ghose , Ankit Singla , Pratap Subrahmanyam , and Onur Mutlu . 2018. Enabling Efficient RDMA-based Synchronous Mirroring of Persistent Memory Transactions. CoRR, abs\/1810.09360 ( 2018 ), arxiv:1810.09360. arxiv:1810.09360 Arash Tavakkol, Aasheesh Kolli, Stanko Novakovic, Kaveh Razavi, Juan G\u00f3mez-Luna, Hasan Hassan, Claude Barthels, Yaohua Wang, Mohammad Sadrosadati, Saugata Ghose, Ankit Singla, Pratap Subrahmanyam, and Onur Mutlu. 2018. Enabling Efficient RDMA-based Synchronous Mirroring of Persistent Memory Transactions. CoRR, abs\/1810.09360 (2018), arxiv:1810.09360. arxiv:1810.09360"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950379"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360554"}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454027","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454027","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:07Z","timestamp":1750197787000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":55,"alternative-id":["10.1145\/3453483.3454027","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454027","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}