{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:26Z","timestamp":1774025786486,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"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"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>\n            The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of\n            <jats:italic>correct<\/jats:italic>\n            programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable\n            <jats:italic>verification gap<\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>\n            To address this, we study the verification of NVM programs, and present\n            <jats:italic>Persistent Owicki-Gries<\/jats:italic>\n            (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.\n          <\/jats:p>","DOI":"10.1145\/3428219","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86"],"prefix":"10.1145","volume":"4","author":[{"given":"Azalea","family":"Raad","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany \/ Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas.","author":"Abdulla Parosh Aziz","year":"2015"},{"key":"e_1_2_2_2_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_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_4_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Clarke Edmund"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629589"},{"key":"e_1_2_2_6_1","volume-title":"Formal Methods-The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N","author":"Derrick John"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_8_1","first-page":"504","volume-title":"Concurrent Abstract Predicates. In ECOOP 2010-Object-Oriented Programming, Theo D'Hondt (Ed.). Springer Berlin Heidelberg","author":"Dinsdale-Young Thomas","year":"2010"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178490"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192367"},{"key":"e_1_2_2_11_1","volume-title":"Relaxed Persist Ordering Using Strand Persistency. In 2020 ACM\/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). 652-665","author":"Gogte V."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_2_2_13_1","unstructured":"Intel. 2015. Persistent Memory Programming. http:\/\/pmem.io\/  Intel. 2015. Persistent Memory Programming. http:\/\/pmem.io\/"},{"key":"e_1_2_2_14_1","unstructured":"Intel. 2019. 3D XPoint. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/intel-optane-technology. html  Intel. 2019. 3D XPoint. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/intel-optane-technology. html"},{"key":"e_1_2_2_15_1","unstructured":"Intel. 2019. Intel 64 and IA-32 Architectures Software Developer's 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's 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_2_2_16_1","volume-title":"Scott","author":"Izraelevitz Joseph","year":"2016"},{"key":"e_1_2_2_17_1","volume-title":"Zixuan Wang, Yi Xu, Subramanya R. Dulloor, Jishen Zhao, and Steven Swanson.","author":"Izraelevitz Joseph","year":"2019"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926417"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830805"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_22_1","unstructured":"J. Kaiser Hoang-Hai Dang D. Dreyer O. Lahav and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP.  J. Kaiser Hoang-Hai Dang D. Dreyer O. Lahav and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.microrel.2011.09.028"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360599"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080229"},{"key":"e_1_2_2_27_1","volume-title":"Delegated Persist Ordering. In The 49th Annual IEEE\/ACM International Symposium on Microarchitecture","author":"Kolli Aasheesh","year":"1956"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","volume-title":"Owicki-Gries Reasoning for Weak Memory Models","author":"Lahav Ori","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"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","volume-title":"Communicating State Transition Systems for Fine-Grained Concurrent Resources","author":"Nanevski Aleksandar"},{"key":"e_1_2_2_33_1","volume-title":"Dal\u00ed: A Periodically Persistent Hash Map. In DISC.","author":"Nawab Faisal","year":"2017"},{"key":"e_1_2_2_34_1","volume-title":"Pedro da Rocha Pinto, and Philippa Gardner","author":"Ntzik Gian","year":"2015"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_2_36_1","first-page":"265","volume-title":"Memory Persistency. In Proceeding of the 41st Annual International Symposium on Computer Architecuture (Minneapolis, Minnesota, USA) ( ISCA '14). IEEE Press","author":"Pelley Steven"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","volume-title":"A Separation Logic for Fictional Sequential Consistency","author":"Sieczkowski Filip","DOI":"10.1007\/978-3-662-46669-8_30"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"D. B. Strukov G. S. Snider D. R. Stewart and R. S. Williams. 2008. The missing memristor found. Nature 453 ( 2008 ) 80-83.  D. B. Strukov G. S. Snider D. R. Stewart and R. S. Williams. 2008. The missing memristor found. Nature 453 ( 2008 ) 80-83.","DOI":"10.1038\/nature06932"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","volume-title":"A Separation Logic for a Promising Semantics","author":"Svendsen Kasper","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_2_47_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\/3428219","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428219","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428219"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":47,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428219"],"URL":"https:\/\/doi.org\/10.1145\/3428219","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}