{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:45Z","timestamp":1779074685612,"version":"3.51.4"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572661","type":"print"},{"value":"9783031572678","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a general framework for specifying and verifying <jats:italic>persistent libraries<\/jats:italic>, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persistent library specifications ranging from hardware architectural specifications to correctness conditions such as durable linearizability. As case studies, we specify the  and  libraries, verify their implementations over \"Image missing\", and use them to build higher-level durably linearizable libraries, all within our framework. We also specify and verify a persistent transaction library that highlights some of the technical challenges which are specific to persistent memory compared to weak memory and how they are handled by our framework.\n<\/jats:p>","DOI":"10.1007\/978-3-031-57267-8_8","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:01Z","timestamp":1712246521000},"page":"185-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Specifying and Verifying Persistent Libraries"],"prefix":"10.1007","author":[{"given":"L\u00e9o","family":"Stefanesco","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"8_CR1","unstructured":"Aguilera, M.K., Frolund, S.: Strict linearizability and the power of aborting. Tech. Rep. HPL-2003-241 (2013)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-based owicki\u2013gries reasoning for persistent x86-tso. In: Sergey, I. (ed.) Programming Languages and Systems. pp. 234\u2013261. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bodenm\u00fcller, S., Derrick, J., Dongol, B., Schellhorn, G., Wehrheim, H.: A fully verified persistency library. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 26\u201347. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-50521-8_2"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Chakrabarti, D.R., Boehm, H.J., Bhandari, K.: Atlas: Leveraging locks for non-volatile memory consistency. SIGPLAN Not. 49(10), 433\u2013452 (Oct 2014). https:\/\/doi.org\/10.1145\/2714064.2660224, http:\/\/doi.acm.org\/10.1145\/2714064.2660224","DOI":"10.1145\/2714064.2660224"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Cho, K., Lee, S.H., Raad, A., Kang, J.: Revamping hardware persistency models: View-based and axiomatic persistency models for Intel-X86 and Armv8. p. 16-31. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021)","DOI":"10.1145\/3453483.3454027"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Condit, J., Nightingale, E.B., Frost, C., Ipek, E., Lee, B., Burger, D., Coetzee, D.: Better I\/O through byte-addressable, persistent memory. In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles. pp. 133\u2013146. SOSP \u201909, ACM, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1629575.1629589, http:\/\/doi.acm.org\/10.1145\/1629575.1629589","DOI":"10.1145\/1629575.1629589"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Dang, H.H., Jung, J., Choi, J., Nguyen, D.T., Mansky, W., Kang, J., Dreyer, D.: Compass: Strong and compositional library specifications in relaxed memory separation logic. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2022 (2022)","DOI":"10.1145\/3519939.3523451"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verifying correctness of persistent concurrent data structures. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods \u2013 The Next 30 Years. pp. 179\u2013195. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-30942-8_12"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Friedman, M., Herlihy, M., Marathe, V., Petrank, E.: A persistent lock-free queue for non-volatile memory. In: Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. p. 28-40. PPoPP \u201918, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3178487.3178490, https:\/\/doi.org\/10.1145\/3178487.3178490","DOI":"10.1145\/3178487.3178490"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Friedman, M., Petrank, E., Ramalhete, P.: Mirror: making lock-free data structures persistent. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921. pp. 1218\u20131232 (2021)","DOI":"10.1145\/3453483.3454105"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Gogte, V., Diestelhorst, S., Wang, W., Narayanasamy, S., Chen, P.M., Wenisch, T.F.: Persistency for synchronization-free regions. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 46\u201361. PLDI 2018, ACM, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3192366.3192367, http:\/\/doi.acm.org\/10.1145\/3192366.3192367","DOI":"10.1145\/3192366.3192367"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Gorjiara, H., Xu, G.H., Demsky, B.: Yashme: Detecting persistency races. In: Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. p. 830-845. ASPLOS 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3503222.3507766, https:\/\/doi.org\/10.1145\/3503222.3507766","DOI":"10.1145\/3503222.3507766"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X.N., Weng, S., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: POPL (2015)","DOI":"10.1145\/2676726.2676975"},{"key":"8_CR14","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2008)"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Hermida, C., Reddy, U.S., Robinson, E.P.: Logical relations and parametricity - a reynolds programme for category theory and programming languages. Electronic Notes in Theoretical Computer Science 303, 149\u2013180 (2014), proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)","DOI":"10.1016\/j.entcs.2014.02.008"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Izraelevitz, J., Mendes, H., Scott, M.L.: Linearizability of persistent memory objects under a full-system-crash failure model. In: Gavoille, C., Ilcinkas, D. (eds.) DISC. Lecture Notes in Computer Science, vol.\u00a09888, pp. 313\u2013327 (2016)","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jagadeesan, R., Petri, G., Pitcher, C., Riely, J.: Quarantining weakness. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. pp. 492\u2013511. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_27"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Khyzha, A., Lahav, O.: Taming x86-tso persistency. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021)","DOI":"10.1145\/3434328"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Kaysin, I., Raad, A., Vafeiadis, V.: Persevere: Persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5(POPL) (jan 2021). https:\/\/doi.org\/10.1145\/3434324, https:\/\/doi.org\/10.1145\/3434324","DOI":"10.1145\/3434324"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Kolli, A., Gogte, V., Saidi, A., Diestelhorst, S., Chen, P.M., Narayanasamy, S., Wenisch, T.F.: Language-level persistency. In: Proceedings of the 44th Annual International Symposium on Computer Architecture. pp. 481\u2013493. ISCA \u201917, ACM, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3079856.3080229, http:\/\/doi.acm.org\/10.1145\/3079856.3080229","DOI":"10.1145\/3079856.3080229"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in c\/c++11. SIGPLAN Not. 52(6), 618-632 (jun 2017). https:\/\/doi.org\/10.1145\/3140587.3062352, https:\/\/doi.org\/10.1145\/3140587.3062352","DOI":"10.1145\/3140587.3062352"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28(9), 690\u2013691 (Sep 1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439, http:\/\/dx.doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Pelley, S., Chen, P.M., Wenisch, T.F.: Memory persistency. In: Proceeding of the 41st Annual International Symposium on Computer Architecuture. pp. 265\u2013276. ISCA \u201914, IEEE Press, Piscataway, NJ, USA (2014), http:\/\/dl.acm.org\/citation.cfm?id=2665671.2665712","DOI":"10.1109\/ISCA.2014.6853222"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Pelley, S., Chen, P.M., Wenisch, T.F.: Memory persistency. In: Proceeding of the 41st Annual International Symposium on Computer Architecuture. p. 265-276. ISCA \u201914, IEEE Press (2014)","DOI":"10.1109\/ISCA.2014.6853222"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Raad, A., Doko, M., Ro\u017ei\u0107, L., Lahav, O., Vafeiadis, V.: On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models. POPL (2019)","DOI":"10.1145\/3291635"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Raad, A., Lahav, O., Vafeiadis, V.: Persistent owicki-gries reasoning: A program logic for reasoning about persistent programs on intel-x86. Proc. ACM Program. Lang. 4(OOPSLA) (nov 2020). https:\/\/doi.org\/10.1145\/3428219, https:\/\/doi.org\/10.1145\/3428219","DOI":"10.1145\/3428219"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Raad, A., Maranget, L., Vafeiadis, V.: 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 (2022)","DOI":"10.1145\/3498683"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Raad, A., Vafeiadis, V.: Persistence semantics for weak memory: Integrating epoch persistency with the tso memory model. Proc. ACM Program. Lang. 2(OOPSLA), 137:1\u2013137:27 (Oct 2018). https:\/\/doi.org\/10.1145\/3276507, http:\/\/doi.acm.org\/10.1145\/3276507","DOI":"10.1145\/3276507"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Raad, A., Wickerson, J., Neiger, G., Vafeiadis, V.: Persistency semantics of the intel-x86 architecture. Proc. ACM Program. Lang. 4(POPL), 11:1\u201311:31 (2020)","DOI":"10.1145\/3371079"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Raad, A., Wickerson, J., Vafeiadis, V.: Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang. 3(OOPSLA), 135:1\u2013135:27 (Oct 2019)","DOI":"10.1145\/3360561"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: X86-TSO: A rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (Jul 2010). https:\/\/doi.org\/10.1145\/1785414.1785443, http:\/\/doi.acm.org\/10.1145\/1785414.1785443","DOI":"10.1145\/1785414.1785443"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Singh, A.K., Lahav, O.: An operational approach to library abstraction under relaxed memory concurrency. Proc. ACM Program. Lang. 7(POPL) (jan 2023). https:\/\/doi.org\/10.1145\/3571246, https:\/\/doi.org\/10.1145\/3571246","DOI":"10.1145\/3571246"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Stefanesco, L., Raad, A., Vafeiadis, V.: Specifying and verifying persistent libraries (with appendix). CoRR abs\/2306.01614 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2306.01614, https:\/\/doi.org\/10.48550\/arXiv.2306.01614","DOI":"10.48550\/ARXIV.2306.01614"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Wei, Y., Ben-David, N., Friedman, M., Blelloch, G.E., Petrank, E.: Flit: a library for simple and efficient persistent algorithms. In: Lee, J., Agrawal, K., Spear, M.F. (eds.) PPoPP \u201922. pp. 309\u2013321 (2022)","DOI":"10.1145\/3503221.3508436"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Zuriel, Y., Friedman, M., Sheffi, G., Cohen, N., Petrank, E.: Efficient lock-free durable sets. Proc. ACM Program. Lang. 3(OOPSLA) (Oct 2019). https:\/\/doi.org\/10.1145\/3360554, https:\/\/doi.org\/10.1145\/3360554","DOI":"10.1145\/3360554"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57267-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:04:27Z","timestamp":1712246667000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57267-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572661","9783031572678"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57267-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}