{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:14Z","timestamp":1773193514156,"version":"3.50.1"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            There is an increasing body of literature proposing new and efficient \npersistent versions of concurrent data structures ensuring that a consistent \nstate can be recovered after a power failure or a crash. \nTheir correctness is typically stated in terms of\n            <jats:italic>durable linearizability<\/jats:italic>\n            (DL), \nwhich requires that individual library operations appear to be executed \natomically in a sequence consistent with the real-time order and, moreover, \nthat recovering from a crash return a state corresponding to a prefix of that \nsequence. \nSadly, however, there are hardly any formal DL proofs, and those that do exist \ncover the correctness of rather simple persistent algorithms on specific \n(simplified) persistency models. \n \nIn response, we propose a general, powerful, modular, and incremental proof technique that \ncan be used to guide the development and establish DL. \nOur technique is \n(1)\n            <jats:italic>general<\/jats:italic>\n            , in that it is not tied to a specific persistency and\/or consistency model, \n(2)\n            <jats:italic>powerful<\/jats:italic>\n            , in that it can handle the most advanced persistent algorithms in the literature, \n(3)\n            <jats:italic>modular<\/jats:italic>\n            , in that it allows the reuse of an existing linearizability argument, and \n(4)\n            <jats:italic>incremental<\/jats:italic>\n            , in that the additional requirements for establishing DL \ndepend on the complexity of the algorithm to be verified. \nWe illustrate this technique on various versions of a persistent set, \nleading to the link-free set of Zuriel et al.\n          <\/jats:p>","DOI":"10.1145\/3571219","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"748-774","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["The Path to Durable Linearizability"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9179-5827","authenticated-orcid":false,"given":"Emanuele","family":"D'Osualdo","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-3242","authenticated-orcid":false,"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Aguilera and Svend Frolund","author":"Marcos","year":"2003","unstructured":"Marcos K. Aguilera and Svend Frolund . 2003 . Strict Linearizability and the Power of Aborting . https:\/\/www.hpl.hp.com\/ techreports\/2003\/HPL-2003-241.html Marcos K. Aguilera and Svend Frolund. 2003. Strict Linearizability and the Power of Aborting. https:\/\/www.hpl.hp.com\/ techreports\/2003\/HPL-2003-241.html"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-012-0161-5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3210377.3210400"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00541-8"},{"key":"#cr-split#-e_1_2_1_8_1.1","unstructured":"Emanuele D'Osualdo Azalea Raad and Viktor Vafeiadis. 2022. The Path to Durable Linearizability (Extended Version). CoRR arxiv:2211.07631 ( 2022 ). https:\/\/doi.org\/10.48550\/arxiv.2211.07631 10.48550\/arxiv.2211.07631"},{"key":"#cr-split#-e_1_2_1_8_1.2","unstructured":"Emanuele D'Osualdo Azalea Raad and Viktor Vafeiadis. 2022. The Path to Durable Linearizability (Extended Version). CoRR arxiv:2211.07631 ( 2022 ). https:\/\/doi.org\/10.48550\/arxiv.2211.07631"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386031"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454105"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45414-4_21"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_14_1","unstructured":"Intel. 2015. Persistent Memory Programming. http:\/\/pmem.io\/  \t\t\t\t  Intel. 2015. Persistent Memory Programming. http:\/\/pmem.io\/"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.MICROREL.2011.09.028"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555758"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853222"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629496"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_28_1","unstructured":"Storage Networking Industry Association (SNIA). 2017. NVM Programming Model (NPM). SNIA Technical Position. https:\/\/www.snia.org\/sites\/default\/files\/technical_work\/final\/NVMProgrammingModel_v1.2.pdf Version 1.2.  \t\t\t\t  Storage Networking Industry Association (SNIA). 2017. NVM Programming Model (NPM). SNIA Technical Position. https:\/\/www.snia.org\/sites\/default\/files\/technical_work\/final\/NVMProgrammingModel_v1.2.pdf Version 1.2."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/IOLTS.2019.8854427"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508436"},{"key":"e_1_2_1_31_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\/3571219","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571219","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571219"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":32,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571219"],"URL":"https:\/\/doi.org\/10.1145\/3571219","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}