{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T17:02:58Z","timestamp":1761930178219,"version":"3.37.3"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,5,17]],"date-time":"2021-05-17T00:00:00Z","timestamp":1621209600000},"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\/R032351\/1"],"award-info":[{"award-number":["EP\/R032351\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R032556\/1"],"award-info":[{"award-number":["EP\/R032556\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R019045\/2"],"award-info":[{"award-number":["EP\/R019045\/2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["WE 2290\/12-1"],"award-info":[{"award-number":["WE 2290\/12-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RE 828\/13-2"],"award-info":[{"award-number":["RE 828\/13-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Non-volatile memory (NVM), aka persistent memory, is a new memory paradigm that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of\n            <jats:italic>persistent<\/jats:italic>\n            concurrent data structures, together with associated notions of correctness. In this paper, we present a formal proof technique for\n            <jats:italic>durable linearizability<\/jats:italic>\n            , which is a correctness criterion that extends linearizability to handle crashes and recovery in the context ofNVM.Our proofs are based on refinement of Input\/Output automata (IOA) representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification and prove that this transformation is both sound and complete. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistentmemory queue that builds on Michael and Scott\u2019s lock-free queue. To support the proofs, we describe an automated translation procedure from code to IOA and a thread-local proof technique for verifying correctness of invariants.\n          <\/jats:p>","DOI":"10.1007\/s00165-021-00541-8","type":"journal-article","created":{"date-parts":[[2021,5,17]],"date-time":"2021-05-17T11:02:55Z","timestamp":1621249375000},"page":"547-573","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Verifying correctness of persistent concurrent data structures: a sound and complete method"],"prefix":"10.1145","volume":"33","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Department of Computing, University of Sheffield, Sheffield, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Doherty","sequence":"additional","affiliation":[{"name":"Department of Computing, University of Sheffield, Sheffield, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Surrey, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Augsburg, Institut f\u00fcr Informatik, 86135, Augsburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Paderborn, Institut f\u00fcr Informatik, 33098, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"39","volume-title":"FORTE, vol 12136 of LNCS","author":"Bila E","year":"2020"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Cohen N Aksun DT Larus JR (2018) Object-oriented recovery for non-volatile memory. PACMPL 2(OOPSLA):153:1\u2013153:22","DOI":"10.1145\/3276523"},{"key":"e_1_2_1_2_3_2","unstructured":"Cepeda D Chowdhury S Li N Lopez R Wang X Golab W (2019) Toward linearizability testing for multi-word persistent synchronization primitives. In: Felber P Friedman R Gilbert S Miller A (eds) OPODIS vol 153 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik pp 19:1\u201319:17"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Chajed T Tassarotti J Kaashoek MF Zeldovich N (2019) Verifying concurrent crash-safe systems with perennial. In: Brecht T Williamson C (eds) SOSP. ACM pp 243\u2013258","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Chen H Ziegler D Chajed T Chlipala A Kaashoek MF Zeldovich N (2015) Using crash hoare logic for certifying the FSCQ file system. In: Miller EL Hand S (eds) SOSP. ACM pp 18\u201337","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Dongol B Derrick J (2015) Verifying linearisability: a comparative survey. ACM Comput Surv 48(2):19:1\u201319:43","DOI":"10.1145\/2796550"},{"key":"e_1_2_1_2_7_2","unstructured":"Doherty S Dongol B Derrick J Schellhorn G Wehrheim H (2016) Proving opacity of a pessimistic STM. In: OPODIS vol 70 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik pp 35:1\u201335:17"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/978-3-030-30942-8_12","volume-title":"Formal methods\u2013the next 30 years-third world congress, FM 2019, Porto, Portugal, October 7\u201311, 2019, Proceedings","author":"Derrick J","year":"2019"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal techniques for networked and distributed systems\u2013FORTE 2004","author":"Doherty S","year":"2004"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Denny JE Lee S Vetter JS (2016) NVL-C: static analysis techniques for efficient correct programming of non-volatile main memory systems. In: Nakashima H Taura K Lange J (eds) HPDC. ACM pp 125\u2013136","DOI":"10.1145\/2907294.2907303"},{"key":"e_1_2_1_2_11_2","unstructured":"de\u00a0Roever WP de\u00a0Boer FS Hannemann U Hooman J Lakhnech Y Poel M Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional methods vol. 54 of Cambridge tracts in theoretical computer science. Cambridge University Press"},{"key":"e_1_2_1_2_12_2","first-page":"323","volume-title":"FM 2011","author":"Derrick J","year":"2011"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Ernst G Pf\u00e4hler J Schellhorn G Haneberg D Reif W KIV\u2014overview and verifythis competition. Softw Tools Technol Transf STTT) 17(6):677\u2013694 2015","DOI":"10.1007\/s10009-014-0308-3"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.009"},{"key":"e_1_2_1_2_15_2","first-page":"28","volume-title":"ACM SIGPLAN symposium on principles and practice of parallel programming","author":"Friedman M","year":"2018"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/3019225"},{"key":"e_1_2_1_2_17_2","unstructured":"Huang Y Pavlovic M Marathe VJ Seltzer M Harris T Byan S (2018) Closing the performance gap between volatile and persistent key-value stores using cross-referencing logs. In USENIX annual technical conference. USENIX Association pp 967\u2013979"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_2_19_2","first-page":"313","volume-title":"Distributed computing\u201330th international symposium, DISC","author":"Izraelevitz J","year":"2016"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Iiboshi H Ugawa T (2018) Towards model checking library for persistent data structures. In: IEEE 7th non-volatile memory systems and applications symposium NVMSA 2018 Hakodate Sapporo Japan August 28\u201331 2018. IEEE pp 119\u2013120","DOI":"10.1109\/NVMSA.2018.00032"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Joshi A Nagarajan V Cintra M Viglas S (2018) DHTM: durable hardware transactional memory. In: ISCA. IEEE Computer Society pp 452\u2013465","DOI":"10.1109\/ISCA.2018.00045"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_2_23_2","unstructured":"KIV proofs for the durable linearizable queue 2020. https:\/\/kiv.isse.de\/projects\/Durable-Queue.html"},{"key":"e_1_2_1_2_24_2","first-page":"137","volume-title":"PODC","author":"Lynch NA","year":"1987"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Liu S Wei Y Zhao J Kolli A Khan SM (2019) Pmtest: a fast and flexible testing framework for persistent memory programs. In: Bahar I Herlihy M Witchel E Lebeck AR (eds) ASPLOS. ACM pp 411\u2013425","DOI":"10.1145\/3297858.3304015"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Michael MM Scott ML (1996) Simple fast and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings 15th ACM symposium on principles of distributed computing pp 267\u2013275","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Oukid I Booss D Lespinasse A Lehner W (2016) On testing persistent-memory-based software. In: DaMoN. ACM pp 5:1\u20135:7","DOI":"10.1145\/2933349.2933354"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Pavlovic M Kogan A Marathe VJ Harris T (2018) Brief announcement: persistent multi-word compare-and-swap. In: PODC. ACM pp 37\u201339","DOI":"10.1145\/3212734.3212783"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Raad A Vafeiadis V (2018) Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. PACMPL 2(OOPSLA):137:1\u2013137:27","DOI":"10.1145\/3276507"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Raad A Wickerson J Neiger G Vafeiadis V (2020) Persistency semantics of the intel-x86 architecture. Proc ACM Program Lang 4(POPL):11:1\u201311:31","DOI":"10.1145\/3371079"},{"key":"e_1_2_1_2_32_2","unstructured":"Sigurbjarnarson H Bornholt J Torlak E Wang X (2016) Push-button verification of file systems via crash refinement. In: Keeton K Roscoe T (eds) OSDI. USENIX Association pp 1\u201316"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Derrick J Wehrheim H (2014) A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans Comput Log 15(4):31:1\u201331:37","DOI":"10.1145\/2629496"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/11591191_33","volume-title":"Logic for programming, artificial intelligence, and reasoning","author":"Tuch H","year":"2005"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00541-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00541-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00541-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00541-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:24:14Z","timestamp":1641486254000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00541-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":34,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-021-00541-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00541-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"3 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 January 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 February 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 May 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}