{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:48:54Z","timestamp":1768006134570,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,7,28]],"date-time":"2022-07-28T00:00:00Z","timestamp":1658966400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/R032556\/1"],"award-info":[{"award-number":["EP\/R032556\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/R032351\/1"],"award-info":[{"award-number":["EP\/R032351\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Non-volatile memory (NVM), also known as persistent memory, is an emerging\nparadigm for memory that preserves its contents even after power loss. NVM is\nwidely expected to become ubiquitous, and hardware architectures are already\nproviding support for NVM programming. This has stimulated interest in the\ndesign of novel concepts ensuring correctness of concurrent programming\nabstractions in the face of persistency and in the development of associated\nverification approaches.\n  Software transactional memory (STM) is a key programming abstraction that\nsupports concurrent access to shared state. In a fashion similar to\nlinearizability as the correctness condition for concurrent data structures,\nthere is an established notion of correctness for STMs known as opacity. We\nhave recently proposed durable opacity as the natural extension of opacity to a\nsetting with non-volatile memory. Together with this novel correctness\ncondition, we designed a verification technique based on refinement. In this\npaper, we extend this work in two directions. First, we develop a durably\nopaque version of NOrec (no ownership records), an existing STM algorithm\nproven to be opaque. Second, we modularise our existing verification approach\nby separating the proof of durability of memory accesses from the proof of\nopacity. For NOrec, this allows us to re-use an existing opacity proof and\ncomplement it with a proof of the durability of accesses to shared state.<\/jats:p>","DOI":"10.46298\/lmcs-18(3:7)2022","type":"journal-article","created":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T13:10:00Z","timestamp":1659100200000},"source":"Crossref","is-referenced-by-count":6,"title":["Modularising Verification Of Durable Opacity"],"prefix":"10.46298","volume":"Volume 18, Issue 3","author":[{"given":"Eleni","family":"Bila","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Doherty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2022,7,28]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9851\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9851\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:18:44Z","timestamp":1687292324000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6941"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,28]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(3:7)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2011.15013v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2011.15013v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2011.15013v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2011.15013","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2011.15013","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,28]]},"article-number":"6941"}}