{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T22:39:30Z","timestamp":1767998370306,"version":"3.49.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030993351","type":"print"},{"value":"9783030993368","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study abstraction for crash-resilient concurrent objects using non-volatile memory (NVM). We develop a library-correctness criterion that is sound for ensuring contextual refinement in this setting, thus allowing clients to reason about library behaviors in terms of their abstract specifications, and library developers to verify their implementations against the specifications abstracting away from particular client programs. As a semantic foundation we employ a recent NVM model, called Persistent Sequential Consistency, and extend its language and operational semantics with useful specification constructs. The proposed correctness criterion accounts for NVM-related interactions between client and library code due to explicit persist instructions, and for calling policies enforced by libraries. We illustrate our approach on two implementations and specifications of simple persistent objects with different prototypical durability guarantees. Our results provide the first approach to formal compositional reasoning under NVM.<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_10","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"262-289","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Abstraction for Crash-Resilient Objects"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6781-9665","authenticated-orcid":false,"given":"Artem","family":"Khyzha","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"10_CR1","unstructured":"C++ reference (std::list::pop_front explanation), https:\/\/www.cplusplus.com\/reference\/list\/list\/pop_front\/ [Accessed Jan-2022]"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: TACAS. pp. 324\u2013338. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"10_CR3","unstructured":"Aguilera, M.K., Fr\u00f8lund, S.: Strict linearizability and the power of aborting. Technical Report HPL-2003-241 (2003)"},{"key":"10_CR4","unstructured":"ARM: ARM architecture reference manual: ARMv8, for ARMv8-A architecture profile (2021), https:\/\/developer.arm.com\/documentation\/ddi0487\/latest\/ [Accessed July-2021]"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C\/C++ concurrency. In: POPL. pp. 235\u2013248. ACM, New York, NY, USA (2013)","DOI":"10.1145\/2429069.2429099"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Boehm, H.J.: Can Seqlocks get along with programming language memory models? In: MSPC. pp. 12\u201320. ACM, New York, NY, USA (2012), http:\/\/doi.acm.org\/10.1145\/2247684.2247688","DOI":"10.1145\/2247684.2247688"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL. p. 651\u2013662. ACM, New York, NY, USA (2015), https:\/\/doi.org\/10.1145\/2676726.2677002","DOI":"10.1145\/2676726.2677002"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: ESOP. pp. 87\u2013107. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"10_CR9","unstructured":"Chajed, T., Tassarotti, J., Theng, M., Jung, R., Kaashoek, M.F., Zeldovich, N.: Gojournal: a verified, concurrent, crash-safe journaling system. In: OSDI. pp. 423\u2013439. USENIX Association (Jul 2021), https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"10_CR10","doi-asserted-by":"publisher","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. In: PLDI. p. 16\u201331. ACM, New York, NY, USA (2021), https:\/\/doi.org\/10.1145\/3453483.3454027","DOI":"10.1145\/3453483.3454027"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: A logic for time and data abstraction. In: ECOOP. pp. 207\u2013231. Springer (Jul 2014), https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Wehrheim, H.: Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects of Computing pp. 1\u201327 (2021)","DOI":"10.1007\/s00165-021-00541-8"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theoretical Computer Science 411(51), 4379\u20134398 (2010), https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397510005001","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Friedman, M., Herlihy, M., Marathe, V., Petrank, E.: A persistent lock-free queue for non-volatile memory. In: PPoPP. pp. 28\u201340. ACM, New York, NY, USA (2018), http:\/\/doi.acm.org\/10.1145\/3178487.3178490","DOI":"10.1145\/3178487.3178490"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Gorjiara, H., Xu, G.H., Demsky, B.: Jaaru: Efficiently model checking persistent memory programs. In: ASPLOS. p. 415\u2013428. ACM, New York, NY, USA (2021), https:\/\/doi.org\/10.1145\/3445814.3446735","DOI":"10.1145\/3445814.3446735"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Yang, H.: Liveness-preserving atomicity abstraction. In: ICALP. pp. 453\u2013465. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22012-8_36"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Yang, H.: Linearizability with Ownership Transfer. Logical Methods in Computer Science Volume 9, Issue 3 (Sep 2013), https:\/\/lmcs.episciences.org\/931","DOI":"10.2168\/LMCS-9(3:12)2013"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X.N., Weng, S.C., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: POPL. p. 595\u2013608. ACM, New York, NY, USA (2015), https:\/\/doi.org\/10.1145\/2676726.2676975","DOI":"10.1145\/2676726.2676975"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Levy, R.R.: Robust emulations of shared memory in a crash-recovery model. In: ICDCS. p. 400\u2013407. IEEE Computer Society, USA (2004)","DOI":"10.1109\/ICDCS.2004.1281605"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: CAV. pp. 449\u2013465. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (Jul 1990), http:\/\/doi.acm.org\/10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"10_CR22","unstructured":"Intel: Persistent Memory Programming (2015), http:\/\/pmem.io\/"},{"key":"10_CR23","unstructured":"Intel: Intel 64 and ia-32 architectures software developer\u2019s manual (combined volumes) (May 2019), https:\/\/software.intel.com\/sites\/default\/files\/managed\/39\/c5\/325462-sdm-vol-1-2abcd-3abcd.pdf, order Number: 325462-069US"},{"key":"10_CR24","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: DISC. pp. 313\u2013327. Springer, Berlin, Heidelberg (2016)","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Khyzha, A., Lahav, O.: Taming x86-TSO persistency. Proc. ACM Program. Lang. 5(POPL), 47:1\u201347:29 (Jan 2021), https:\/\/doi.org\/10.1145\/3434328","DOI":"10.1145\/3434328"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36(1) (Mar 2014), https:\/\/doi.org\/10.1145\/2576235","DOI":"10.1145\/2576235"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Lorch, J.R., Chen, Y., Kapritsos, M., Parno, B., Qadeer, S., Sharma, U., Wilcox, J.R., Zhao, X.: Armada: Low-effort verification of high-performance concurrent programs. In: PLDI. p. 197\u2013210. ACM, New York, NY, USA (2020), https:\/\/doi.org\/10.1145\/3385412.3385971","DOI":"10.1145\/3385412.3385971"},{"key":"10_CR28","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. Proc. ACM Program. Lang. 3(POPL), 68:1\u201368:31 (Jan 2019), http:\/\/doi.acm.org\/10.1145\/3290381","DOI":"10.1145\/3290381"},{"key":"10_CR29","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","DOI":"10.1145\/3428219"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Raad, A., Wickerson, J., Neiger, G., Vafeiadis, V.: Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang. 4(POPL) (Jan 2020), https:\/\/doi.org\/10.1145\/3371079","DOI":"10.1145\/3371079"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Modular reasoning about separation of concurrent data structures. In: ECOOP. pp. 169\u2013188. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Zuriel, Y., Friedman, M., Sheffi, G., Cohen, N., Petrank, E.: Efficient lock-free durable sets. Proc. ACM Program. Lang. 3(OOPSLA), 128:1\u2013128:26 (Oct 2019), http:\/\/doi.acm.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-030-99336-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:08:31Z","timestamp":1731647311000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/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":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","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":"21","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":"0","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":"33% - 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.5","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":"7","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)"}}]}}