{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:47Z","timestamp":1779074687988,"version":"3.51.4"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"VeTSS"},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/X037142\/1"],"award-info":[{"award-number":["EP\/X037142\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The advent of non-volatile memory technologies has spurred intensive research interest in correctness and programmability. This paper addresses both by developing and verifying a durable (aka persistent) transactional memory (TM) algorithm, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\text {dTML}_{\\text {Px86}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>dTML<\/mml:mtext>\n                    <mml:mtext>Px86<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Correctness of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\text {dTML}_{\\text {Px86}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>dTML<\/mml:mtext>\n                    <mml:mtext>Px86<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is judged in terms of <jats:italic>durable opacity<\/jats:italic>, which ensures both <jats:italic>failure atomicity<\/jats:italic> (ensuring memory consistency after a crash) and <jats:italic>opacity<\/jats:italic> (ensuring thread safety). We assume a realistic execution model, Px86, which represents Intel\u2019s persistent memory model and extends the <jats:italic>Total Store Order<\/jats:italic> memory model with instructions that control persistency. Our TM algorithm, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\text {dTML}_{\\text {Px86}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>dTML<\/mml:mtext>\n                    <mml:mtext>Px86<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, is an adaptation of an existing software transactional mutex lock, but with additional synchronisation mechanisms to cope with Px86. Our correctness proof is operational and comprises two distinct types of proofs: (1) proofs of invariants of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\text {dTML}_{\\text {Px86}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mtext>dTML<\/mml:mtext>\n                    <mml:mtext>Px86<\/mml:mtext>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and (2) a proof of refinement against an operational specification that guarantees durable opacity. To achieve (1), we build on recent Owicki\u2013Gries logics for Px86, and for (2) we use a simulation-based proof technique, which, as far as we are aware, is the first application of simulation-based proofs for Px86 programs. Our entire development has been mechanised in the Isabelle\/HOL proof assistant.<\/jats:p>","DOI":"10.1007\/s10703-024-00462-1","type":"journal-article","created":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T19:03:15Z","timestamp":1722452595000},"page":"237-282","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A verified durable transactional mutex lock for persistent x86-TSO"],"prefix":"10.1007","volume":"64","author":[{"given":"Eleni","family":"Vafeiadi\u00a0Bila","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,31]]},"reference":[{"issue":"POPL","key":"462_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434337","volume":"5","author":"PA Abdulla","year":"2021","unstructured":"Abdulla PA, Atig MF, Bouajjani A et al (2021) Deciding reachability under persistent x86-TSO. Proc ACM Program Lang 5(POPL):1\u201332. https:\/\/doi.org\/10.1145\/3434337","journal-title":"Proc ACM Program Lang"},{"key":"462_CR2","first-page":"50","volume-title":"FORTE, LNCS","author":"A Armstrong","year":"2017","unstructured":"Armstrong A, Dongol B, Doherty S (2017) Proving opacity via linearizability: a sound and complete method. In: Bouajjani A, Silva A (eds) FORTE, LNCS, vol 10321. Springer, pp 50\u201366"},{"key":"462_CR3","doi-asserted-by":"publisher","unstructured":"Attiya H, Gotsman A, Hans S, et\u00a0al (2013) A programming language perspective on transactional memory consistency. In: Fatourou P, Taubenfeld G (eds) PODC \u201913. ACM, pp 309\u2013318. https:\/\/doi.org\/10.1145\/2484239.2484267","DOI":"10.1145\/2484239.2484267"},{"key":"462_CR4","unstructured":"Beillahi SM, Bouajjani A, Enea C (2021) Robustness against transactional causal consistency. Log Methods Comput Sci 17(1). URL https:\/\/lmcs.episciences.org\/7149"},{"key":"462_CR5","doi-asserted-by":"publisher","unstructured":"Bila E, Doherty S, Dongol B, et\u00a0al (2020) Defining and verifying durable opacity: Correctness for persistent software transactional memory. In: Gotsman A, Sokolova A (eds) FORTE, LNCS, vol 12136. Springer, pp 39\u201358. https:\/\/doi.org\/10.1007\/978-3-030-50086-3_3","DOI":"10.1007\/978-3-030-50086-3_3"},{"key":"462_CR6","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:7)2022","author":"E Bila","year":"2022","unstructured":"Bila E, Derrick J, Doherty S et al (2022) Modularising verification of durable opacity. Log Methods Comput Sci. https:\/\/doi.org\/10.46298\/lmcs-18(3:7)2022","journal-title":"Log Methods Comput Sci"},{"key":"462_CR7","unstructured":"Bila EV, Dongol B (2024) Isabelle\/HOL files for \u201cA verified durable transactional mutex lock for persistent x86-TSO\u201d. URL https:\/\/figshare.com\/articles\/thesis\/DTML_correctness_proof\/25037312"},{"key":"462_CR8","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-030-99336-8_9","volume-title":"ESOP, LNCS","author":"EV Bila","year":"2022","unstructured":"Bila EV, Dongol B, Lahav O et al (2022) View-based Owicki\u2013Gries reasoning for persistent x86-tso. In: Sergey I (ed) ESOP, LNCS, vol 13240. Springer, pp 234\u2013261. https:\/\/doi.org\/10.1007\/978-3-030-99336-8_9"},{"key":"462_CR9","doi-asserted-by":"publisher","unstructured":"B\u00f6hme S, Nipkow T (2010) Sledgehammer: judgement day. In: Giesl J, H\u00e4hnle R (eds) Automated reasoning, 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, LNCS, vol 6173. Springer, pp 107\u2013121. https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"462_CR10","doi-asserted-by":"crossref","unstructured":"Chajed T, Tassarotti J, Kaashoek MF, et\u00a0al (2019) Verifying concurrent, crash-safe systems with perennial. In: Proceedings of the 27th ACM symposium on operating systems principles, pp 243\u2013258","DOI":"10.1145\/3341301.3359632"},{"key":"462_CR11","doi-asserted-by":"publisher","unstructured":"Chakrabarti DR, Boehm H, Bhandari K (2014) Atlas: leveraging locks for non-volatile memory consistency. In: Black AP, Millstein TD (eds) OOPSLA. ACM, pp 433\u2013452. https:\/\/doi.org\/10.1145\/2660193.2660224","DOI":"10.1145\/2660193.2660224"},{"key":"462_CR12","doi-asserted-by":"publisher","unstructured":"Cho K, Lee SH, Raad A, et\u00a0al (2021) Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8. In: Freund SN, Yahav E (eds) PLDI. ACM, pp 16\u201331. https:\/\/doi.org\/10.1145\/3453483.3454027","DOI":"10.1145\/3453483.3454027"},{"key":"462_CR13","doi-asserted-by":"publisher","unstructured":"Coburn J, Caulfield AM, Akel A, et\u00a0al (2011) Nv-heaps: making persistent objects fast and safe with next-generation, non-volatile memories. In: Gupta R, Mowry TC (eds) ASPLOS. ACM, pp 105\u2013118. https:\/\/doi.org\/10.1145\/1950365.1950380","DOI":"10.1145\/1950365.1950380"},{"key":"462_CR14","doi-asserted-by":"crossref","unstructured":"Correia A, Felber P, Ramalhete P (2018) Romulus: efficient algorithms for persistent transactional memory. In: SPAA, pp 271\u2013282","DOI":"10.1145\/3210377.3210392"},{"key":"462_CR15","doi-asserted-by":"crossref","unstructured":"Dalessandro L, Dice D, Scott M, et\u00a0al (2010) Transactional mutex locks. In: Euro-Par, Springer, pp 2\u201313","DOI":"10.1007\/978-3-642-15291-7_2"},{"issue":"OOPSLA2","key":"462_CR16","doi-asserted-by":"publisher","first-page":"1817","DOI":"10.1145\/3563352","volume":"6","author":"S Dalvandi","year":"2022","unstructured":"Dalvandi S, Dongol B (2022) Implementing and verifying release-acquire transactional memory in C11. Proc ACM Program Lang 6(OOPSLA2):1817\u20131844. https:\/\/doi.org\/10.1145\/3563352","journal-title":"Proc ACM Program Lang"},{"issue":"5","key":"462_CR17","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/s00165-017-0433-3","volume":"30","author":"J Derrick","year":"2018","unstructured":"Derrick J, Doherty S, Dongol B et al (2018) Mechanized proofs of opacity: a comparison of two techniques. Formal Asp Comput 30(5):597\u2013625. https:\/\/doi.org\/10.1007\/s00165-017-0433-3","journal-title":"Formal Asp Comput"},{"issue":"4\u20135","key":"462_CR18","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/s00165-021-00541-8","volume":"33","author":"J Derrick","year":"2021","unstructured":"Derrick J, Doherty S, Dongol B et al (2021) Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput 33(4\u20135):547\u2013573. https:\/\/doi.org\/10.1007\/s00165-021-00541-8","journal-title":"Formal Aspects Comput"},{"key":"462_CR19","doi-asserted-by":"crossref","unstructured":"Dice D, Shalev O, Shavit N (2006) Transactional locking II. In: International symposium on distributed computing, Springer, pp 194\u2013208","DOI":"10.1007\/11864219_14"},{"key":"462_CR20","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1007\/s00165-012-0225-8","volume":"25","author":"S Doherty","year":"2013","unstructured":"Doherty S, Groves L, Luchangco V et al (2013) Towards formally specifying and verifying transactional memory. Form Aspect Comput 25:769\u2013799","journal-title":"Form Aspect Comput"},{"key":"462_CR21","unstructured":"Doherty S, Dongol B, Derrick J, et\u00a0al (2016) Proving opacity of a pessimistic STM. In: Fatourou P, Jim\u00e9nez E, Pedone F (eds) OPODIS, LIPIcs, vol\u00a070. Schloss Dagstuhl\u2013Leibniz\u2013Zentrum f\u00fcr Informatik, pp 35:1\u201335:17"},{"issue":"2","key":"462_CR22","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/2796550","volume":"48","author":"B Dongol","year":"2015","unstructured":"Dongol B, Derrick J (2015) Verifying linearisability: a comparative survey. ACM Comput Surv 48(2):19:1-19:43. https:\/\/doi.org\/10.1145\/2796550","journal-title":"ACM Comput Surv"},{"key":"462_CR23","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-030-92124-8_13","volume-title":"SEFM, LNCS","author":"B Dongol","year":"2021","unstructured":"Dongol B, Le-Papin J (2021) Checking opacity and durable opacity with FDR. In: Calinescu R, Pasareanu CS (eds) SEFM, LNCS, vol 13085. Springer, pp 222\u2013242. https:\/\/doi.org\/10.1007\/978-3-030-92124-8_13"},{"issue":"POPL","key":"462_CR24","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1145\/3571219","volume":"7","author":"E D\u2019Osualdo","year":"2023","unstructured":"D\u2019Osualdo E, Raad A, Vafeiadis V (2023) The path to durable linearizability. Proc ACM Program Lang 7(POPL):748\u2013774. https:\/\/doi.org\/10.1145\/3571219","journal-title":"Proc ACM Program Lang"},{"key":"462_CR25","doi-asserted-by":"crossref","unstructured":"Dziuma D, Fatourou P, Kanellou E (2014) Consistency for transactional memory computing. Bull EATCS 113","DOI":"10.1007\/978-3-319-14720-8_1"},{"key":"462_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3126-2","volume-title":"On a method of multiprogramming. Monographs in computer science","author":"WHJ Feijen","year":"1999","unstructured":"Feijen WHJ, van Gasteren AJM (1999) On a method of multiprogramming. Monographs in computer science. Springer. https:\/\/doi.org\/10.1007\/978-1-4757-3126-2"},{"key":"462_CR27","doi-asserted-by":"crossref","unstructured":"Felber P, Gramoli V, Guerraoui R (2009) Elastic transactions. In: DISC, Springer, pp 93\u2013107","DOI":"10.1007\/978-3-642-04355-0_12"},{"key":"462_CR28","doi-asserted-by":"publisher","unstructured":"Friedman M, Ben-David N, Wei Y, et\u00a0al (2020) Nvtraverse: in NVRAM data structures, the destination is more important than the journey. In: Donaldson AF, Torlak E (eds) PLDI. ACM, pp 377\u2013392. https:\/\/doi.org\/10.1145\/3385412.3386031","DOI":"10.1145\/3385412.3386031"},{"key":"462_CR29","doi-asserted-by":"publisher","unstructured":"Friedman M, Petrank E, Ramalhete P (2021) Mirror: making lock-free data structures persistent. In: Freund SN, Yahav E (eds) PLDI. ACM, pp 1218\u20131232. https:\/\/doi.org\/10.1145\/3453483.3454105","DOI":"10.1145\/3453483.3454105"},{"key":"462_CR30","doi-asserted-by":"publisher","unstructured":"Giles E, Doshi KA, Varman PJ (2015) Softwrap: a lightweight framework for transactional support of storage class memory. In: IEEE MSST. IEEE Computer Society, pp 1\u201314. https:\/\/doi.org\/10.1109\/MSST.2015.7208276","DOI":"10.1109\/MSST.2015.7208276"},{"key":"462_CR31","doi-asserted-by":"publisher","unstructured":"Gorjiara H, Luo W, Lee A, et\u00a0al (2022) Checking robustness to weak persistency models. In: Jhala R, Dillig I (eds) PLDI. ACM, pp 490\u2013505. https:\/\/doi.org\/10.1145\/3519939.3523723,","DOI":"10.1145\/3519939.3523723"},{"key":"462_CR32","unstructured":"Gu J, Yu Q, Wang X, et\u00a0al (2019) Pisces: a scalable and efficient persistent transactional memory. In: Malkhi D, Tsafrir D (eds) USENIX ATC. USENIX Association, pp 913\u2013928"},{"key":"462_CR33","doi-asserted-by":"publisher","unstructured":"Guerraoui R, Kapalka M (2010) Principles of transactional memory. synthesis lectures on distributed computing theory, Morgan & Claypool Publishers. https:\/\/doi.org\/10.2200\/S00253ED1V01Y201009DCT004","DOI":"10.2200\/S00253ED1V01Y201009DCT004"},{"issue":"3","key":"462_CR34","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy M, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3):463\u2013492. https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans Program Lang Syst"},{"key":"462_CR35","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2012.04.037","volume":"444","author":"D Imbs","year":"2012","unstructured":"Imbs D, Raynal M (2012) Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations). Theor Comput Sci 444:113\u2013127. https:\/\/doi.org\/10.1016\/j.tcs.2012.04.037","journal-title":"Theor Comput Sci"},{"key":"462_CR36","unstructured":"Intel (2022) Persistent memory development kit, libpmemobj library. URL https:\/\/pmem.io\/pmdk\/libpmemobj\/"},{"key":"462_CR37","unstructured":"Intel Corporation (2021) Intel 64 and IA-32 architectures optimization reference manual"},{"key":"462_CR38","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-662-53426-7_23","volume-title":"DISC, LNCS","author":"J Izraelevitz","year":"2016","unstructured":"Izraelevitz J, Mendes H, Scott ML (2016) Linearizability of persistent memory objects under a full-system-crash failure model. In: Gavoille C, Ilcinkas D (eds) DISC, LNCS, vol 9888. Springer, pp 313\u2013327. https:\/\/doi.org\/10.1007\/978-3-662-53426-7_23"},{"key":"462_CR39","doi-asserted-by":"crossref","unstructured":"Jeong J, Hong J, Maeng S, et\u00a0al (2020) Unbounded hardware transactional memory for a hybrid dram\/nvm memory system. In: MICRO, IEEE, pp 525\u2013538","DOI":"10.1109\/MICRO50266.2020.00051"},{"key":"462_CR40","doi-asserted-by":"publisher","unstructured":"Joshi A, Nagarajan V, Viglas S, et\u00a0al (2017) ATOM: atomic durability in non-volatile memory through hardware logging. In: HPCA. IEEE computer society, pp 361\u2013372. https:\/\/doi.org\/10.1109\/HPCA.2017.50","DOI":"10.1109\/HPCA.2017.50"},{"key":"462_CR41","doi-asserted-by":"crossref","unstructured":"Joshi A, Nagarajan V, Cintra M, et\u00a0al (2018) Dhtm: durable hardware transactional memory. In: ISCA, IEEE, pp 452\u2013465","DOI":"10.1109\/ISCA.2018.00045"},{"key":"462_CR42","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung R, Krebbers R, Jourdan JH et al (2018) Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J Funct Program 28:e20","journal-title":"J Funct Program"},{"key":"462_CR43","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller F, Wenzel M, Paulson LC (1999) Locales a sectioning concept for isabelle. In: TPHOLs, Springer, pp 149\u2013165","DOI":"10.1007\/3-540-48256-3_11"},{"issue":"POPL","key":"462_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434328","volume":"5","author":"A Khyzha","year":"2021","unstructured":"Khyzha A, Lahav O (2021) Taming x86-TSO persistency. Proc ACM Program Lang 5(POPL):1\u201329. https:\/\/doi.org\/10.1145\/3434328","journal-title":"Proc ACM Program Lang"},{"key":"462_CR45","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-030-99336-8_10","volume-title":"ESOP, LNCS","author":"A Khyzha","year":"2022","unstructured":"Khyzha A, Lahav O (2022) Abstraction for crash-resilient objects. In: Sergey I (ed) ESOP, LNCS, vol 13240. Springer, pp 262\u2013289. https:\/\/doi.org\/10.1007\/978-3-030-99336-8_10"},{"key":"462_CR46","doi-asserted-by":"publisher","unstructured":"Kolli A, Pelley S, Saidi AG, et\u00a0al (2016) High-performance transactions for persistent memories. In: Conte T, Zhou Y (eds) ASPLOS. ACM, pp 399\u2013411. https:\/\/doi.org\/10.1145\/2872362.2872381","DOI":"10.1145\/2872362.2872381"},{"key":"462_CR47","doi-asserted-by":"crossref","unstructured":"Krishnan RM, Kim J, Mathew A, et\u00a0al (2020) Durable transactional memory can scale with timestone. In: ASPLOS, pp 335\u2013349","DOI":"10.1145\/3373376.3378483"},{"issue":"9","key":"462_CR48","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport L (1979) How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans Comput 28(9):690\u2013691. https:\/\/doi.org\/10.1109\/TC.1979.1675439","journal-title":"IEEE Trans Comput"},{"key":"462_CR49","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-662-45174-8_27","volume-title":"DISC, LNCS","author":"M Lesani","year":"2014","unstructured":"Lesani M, Palsberg J (2014) Decomposing opacity. In: Kuhn F (ed) DISC, LNCS, vol 8784. Springer, pp 391\u2013405. https:\/\/doi.org\/10.1007\/978-3-662-45174-8_27"},{"key":"462_CR50","unstructured":"Lesani M, Luchangco V, Moir M (2012) Putting opacity in its place. In: Workshop on the theory of transactional memory, pp 137\u2013151"},{"key":"462_CR51","doi-asserted-by":"publisher","unstructured":"Liu M, Zhang M, Chen K, et\u00a0al (2017) Dudetm: Building durable transactions with decoupling for persistent memory. In: Chen Y, Temam O, Carter J (eds) ASPLOS. ACM, pp 329\u2013343.https:\/\/doi.org\/10.1145\/3037697.3037714","DOI":"10.1145\/3037697.3037714"},{"key":"462_CR52","volume-title":"Distributed algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch NA (1996) Distributed algorithms. Morgan Kaufmann"},{"issue":"3","key":"462_CR53","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk D, Murray T, Wenzel M (2016) Eisbach: a proof method language for Isabelle. J Autom Reason 56(3):261\u2013282. https:\/\/doi.org\/10.1007\/s10817-015-9360-2","journal-title":"J Autom Reason"},{"key":"462_CR54","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki SS, Gries D (1976) An axiomatic proof technique for parallel programs I. Acta Inform 6:319\u2013340. https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Inform"},{"issue":"4","key":"462_CR55","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou CH (1979) The serializability of concurrent database updates. J ACM (JACM) 26(4):631\u2013653","journal-title":"J ACM (JACM)"},{"issue":"POPL","key":"462_CR56","doi-asserted-by":"publisher","first-page":"68:1","DOI":"10.1145\/3290381","volume":"3","author":"A Raad","year":"2019","unstructured":"Raad A, Doko M, Rozic L et al (2019) On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. Proc ACM Program Lang 3(POPL):68:1-68:31. https:\/\/doi.org\/10.1145\/3290381","journal-title":"Proc ACM Program Lang"},{"issue":"OOPSLA","key":"462_CR57","doi-asserted-by":"publisher","first-page":"135:1","DOI":"10.1145\/3360561","volume":"3","author":"A Raad","year":"2019","unstructured":"Raad A, Wickerson J, Vafeiadis V (2019) Weak persistency semantics from the ground up: formalising the persistency semantics of armv8 and transactional models. Proc ACM Program Lang 3(OOPSLA):135:1-135:27. https:\/\/doi.org\/10.1145\/3360561","journal-title":"Proc ACM Program Lang"},{"issue":"OOPSLA","key":"462_CR58","doi-asserted-by":"publisher","first-page":"151:1","DOI":"10.1145\/3428219","volume":"4","author":"A Raad","year":"2020","unstructured":"Raad A, Lahav O, Vafeiadis V (2020) Persistent Owicki\u2013Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc ACM Program Lang 4(OOPSLA):151:1-151:28. https:\/\/doi.org\/10.1145\/3428219","journal-title":"Proc ACM Program Lang"},{"issue":"POPL","key":"462_CR59","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/3371079","volume":"4","author":"A Raad","year":"2020","unstructured":"Raad A, Wickerson J, Neiger G et al (2020) Persistency semantics of the Intel-x86 architecture. Proc ACM Program Lang 4(POPL):11:1-11:31. https:\/\/doi.org\/10.1145\/3371079","journal-title":"Proc ACM Program Lang"},{"issue":"POPL","key":"462_CR60","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498683","volume":"6","author":"A Raad","year":"2022","unstructured":"Raad A, Maranget L, Vafeiadis V (2022) Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. Proc ACM Program Lang 6(POPL):1\u201331. https:\/\/doi.org\/10.1145\/3498683","journal-title":"Proc ACM Program Lang"},{"key":"462_CR61","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-031-57267-8_6","volume-title":"ESOP, LNCS","author":"A Raad","year":"2024","unstructured":"Raad A, Lahav O, Wickerson J et al (2024) Intel PMDK transactions: Specification, validation and concurrency. In: Weirich S (ed) ESOP, LNCS, vol 14577. Springer, pp 150\u2013179. https:\/\/doi.org\/10.1007\/978-3-031-57267-8_6"},{"key":"462_CR62","doi-asserted-by":"publisher","unstructured":"Ramalhete P, Correia A, Felber P, et\u00a0al (2019) Onefile: a wait-free persistent transactional memory. In: DSN. IEEE, pp 151\u2013163. https:\/\/doi.org\/10.1109\/DSN.2019.00028","DOI":"10.1109\/DSN.2019.00028"},{"key":"462_CR63","doi-asserted-by":"publisher","unstructured":"Ren J, Zhao J, Khan SM, et\u00a0al (2015) ThyNVM: enabling software-transparent crash consistency in persistent memory systems. In: Prvulovic M (ed) MICRO. ACM, pp 672\u2013685. https:\/\/doi.org\/10.1145\/2830772.2830802","DOI":"10.1145\/2830772.2830802"},{"issue":"7","key":"462_CR64","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell P, Sarkar S, Owens S et al (2010) x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun ACM 53(7):89\u201397","journal-title":"Commun ACM"},{"issue":"3","key":"462_CR65","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/s00446-022-00420-2","volume":"35","author":"K Siek","year":"2022","unstructured":"Siek K, Wojciechowski PT (2022) Last-use opacity: a strong safety property for transactional memory with prerelease support. Distribut Comput 35(3):265\u2013301. https:\/\/doi.org\/10.1007\/s00446-022-00420-2","journal-title":"Distribut Comput"},{"issue":"POPL","key":"462_CR66","doi-asserted-by":"publisher","first-page":"1542","DOI":"10.1145\/3571246","volume":"7","author":"AK Singh","year":"2023","unstructured":"Singh AK, Lahav O (2023) An operational approach to library abstraction under relaxed memory concurrency. Proc ACM Program Lang 7(POPL):1542\u20131572. https:\/\/doi.org\/10.1145\/3571246","journal-title":"Proc ACM Program Lang"},{"key":"462_CR67","doi-asserted-by":"publisher","unstructured":"Sun L, Lu Y, Shu J (2015) $$\\text{Dp}^{2}$$: reducing transaction overhead with differential and dual persistency in persistent memory. In: Napoli CD, Salapura V, Franke H, et\u00a0al (eds) CF. ACM, pp 24:1\u201324:8. https:\/\/doi.org\/10.1145\/2742854.2742864","DOI":"10.1145\/2742854.2742864"},{"key":"462_CR68","doi-asserted-by":"crossref","unstructured":"Vindum SF, Birkedal L (2022) Spirea: a mechanized concurrent separation logic for weak persistent memory","DOI":"10.1145\/3622820"},{"key":"462_CR69","doi-asserted-by":"publisher","unstructured":"Volos H, Tack AJ, Swift MM (2011) Mnemosyne: lightweight persistent memory. In: Gupta R, Mowry TC (eds) ASPLOS. ACM, pp 91\u2013104. https:\/\/doi.org\/10.1145\/1950365.1950379","DOI":"10.1145\/1950365.1950379"},{"key":"462_CR70","doi-asserted-by":"publisher","unstructured":"Wei Y, Ben-David N, Friedman M, et\u00a0al (2022) Flit: a library for simple and efficient persistent algorithms. In: Lee J, Agrawal K, Spear MF (eds) PPoPP. ACM, pp 309\u2013321. https:\/\/doi.org\/10.1145\/3503221.3508436","DOI":"10.1145\/3503221.3508436"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00462-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00462-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00462-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:03:40Z","timestamp":1735409020000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00462-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,31]]},"references-count":70,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["462"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00462-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,31]]},"assertion":[{"value":"5 November 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 July 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}