{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:37:39Z","timestamp":1743071859571,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030449131"},{"type":"electronic","value":"9783030449148"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Multithreaded programs generally leverage efficient and thread-safe <jats:italic>concurrent objects<\/jats:italic> like sets, key-value maps, and queues. While some concurrent-object operations are designed to behave atomically, each witnessing the atomic effects of predecessors in a linearization order, others forego such strong consistency to avoid complex control and synchronization bottlenecks. For example, contains (value) methods of key-value maps may iterate through key-value entries without blocking concurrent updates, to avoid unwanted performance bottlenecks, and consequently overlook the effects of some linearization-order predecessors. While such <jats:italic>weakly-consistent<\/jats:italic> operations may not be atomic, they still offer guarantees, e.g.,\u00a0only observing values that have been present.<\/jats:p><jats:p>In this work we develop a methodology for proving that concurrent object implementations adhere to weak-consistency specifications. In particular, we consider (forward) simulation-based proofs of implementations against <jats:italic>relaxed-visibility specifications<\/jats:italic>, which allow designated operations to overlook some of their linearization-order predecessors, i.e.,\u00a0behaving as if they never occurred. Besides annotating implementation code to identify <jats:italic>linearization points<\/jats:italic>, i.e.,\u00a0points at which operations\u2019 logical effects occur, we also annotate code to identify <jats:italic>visible operations<\/jats:italic>, i.e.,\u00a0operations whose effects are observed; in practice this annotation can be done automatically by tracking the writers to each accessed memory location. We formalize our methodology over a general notion of transition systems, agnostic to any particular programming language or memory model, and demonstrate its application, using automated theorem provers, by verifying models of Java concurrent object implementations.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_11","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"280-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verifying Visibility-Based Weak Consistency"],"prefix":"10.1007","author":[{"given":"Siddharth","family":"Krishna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dejan","family":"Jovanovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991)","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"11_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 for highly concurrent data structures. STTT 19(5), 549\u2013563 (2017)","DOI":"10.1007\/s10009-016-0415-4"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: CAV. Lecture Notes in Computer Science, vol.\u00a04590, pp. 477\u2013490. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The vercors tool set: Verification of parallel and concurrent software. In: IFM. Lecture Notes in Computer Science, vol. 10510, pp. 102\u2013110. Springer (2017)","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On reducing linearizability to state reachability. Inf. Comput. 261(Part), 383\u2013400 (2018)","DOI":"10.1016\/j.ic.2018.02.014"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Mutluergil, S.O.: Proving linearizability using forward simulations. In: CAV (2). Lecture Notes in Computer Science, vol. 10427, pp. 542\u2013563. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types: specification, verification, optimality. In: POPL. pp. 271\u2013284. ACM (2014)","DOI":"10.1145\/2578855.2535848"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. Logical Methods in Computer Science 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"11_CR9","unstructured":"Delbianco, G.A., Sergey, I., Nanevski, A., Banerjee, A.: Concurrent data structures linked in time. In: ECOOP. LIPIcs, vol.\u00a074, pp. 8:1\u20138:30. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Derrick, J., Dongol, B., Schellhorn, G., Tofan, B., Travkin, O., Wehrheim, H.: Quiescent consistency: Defining and verifying relaxed linearizability. In: FM. Lecture Notes in Computer Science, vol.\u00a08442, pp. 200\u2013214. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_15"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Dongol, B., Jagadeesan, R., Riely, J., Armstrong, A.: On abstraction and compositionality for weak-memory linearisability. In: VMCAI. Lecture Notes in Computer Science, vol. 10747, pp. 183\u2013204. Springer (2018)","DOI":"10.1007\/978-3-319-73721-8_9"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Dragoi, C., Gupta, A., Henzinger, T.A.: Automatic linearizability proofs of concurrent objects with cooperating updates. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 174\u2013190. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_11"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Emmi, M., Enea, C.: Weak-consistency specification via visibility relaxation. PACMPL 3(POPL), 60:1\u201360:28 (2019)","DOI":"10.1145\/3290373"},{"key":"11_CR14","unstructured":"Haas, A., Henzinger, T.A., Holzer, A., Kirsch, C.M., Lippautz, M., Payer, H., Sezgin, A., Sokolova, A., Veith, H.: Local linearizability for concurrent container-type data structures. In: CONCUR. LIPIcs, vol.\u00a059, pp. 6:1\u20136:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. Logical Methods in Computer Science 6(3) (2010)","DOI":"10.2168\/LMCS-6(3:6)2010"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: CAV (2). Lecture Notes in Computer Science, vol.\u00a09207, pp. 449\u2013465. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kirsch, C.M., Payer, H., Sezgin, A., Sokolova, A.: Quantitative relaxation of concurrent data structures. In: POPL. pp.317\u2013328. ACM (2013)","DOI":"10.1145\/2480359.2429109"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","DOI":"10.1145\/78969.78972"},{"key":"11_CR19","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress. pp. 321\u2013332. North-Holland\/IFIP (1983)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Khyzha, A., Dodds, M., Gotsman, A., Parkinson, M.J.: Proving linearizability using partial orders. In: ESOP. Lecture Notes in Computer Science, vol. 10201, pp. 639\u2013667. Springer (2017)","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-gries reasoning for weak memory models. In: ICALP (2). Lecture Notes in Computer Science, vol.\u00a09135, pp. 311\u2013323. Springer (2015)","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR (Dakar). Lecture Notes in Computer Science, vol.\u00a06355, pp.348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI. pp. 459\u2013470. ACM (2013)","DOI":"10.1145\/2499370.2462189"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995)","DOI":"10.1006\/inco.1995.1134"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC. pp. 267\u2013275. ACM (1996)","DOI":"10.1145\/248052.248106"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Moskal, M., Lopuszanski, J., Kiniry, J.R.: E-matching for fun and profit. Electr. Notes Theor. Comput. Sci. 198(2), 19\u201335 (2008)","DOI":"10.1016\/j.entcs.2008.04.078"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a03170, pp. 49\u201367. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: Anaxiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976)","DOI":"10.1145\/360051.360224"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Grasshopper - complete heap verification with mixed specifications. In: TACAS. Lecture Notes in Computer Science, vol.\u00a08413, pp. 124\u2013139. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Raad, A., Doko, M., Rozic, L., Lahav, O., Vafeiadis, V.: On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models. PACMPL 3(POPL), 68:1\u201368:31 (2019)","DOI":"10.1145\/3290381"},{"key":"11_CR32","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55\u201374. IEEE Computer Society (2002)"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: How to prove algorithms linearisable. In: CAV. Lecture Notes in Computer Science, vol.\u00a07358, pp.243\u2013259. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_21"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI. pp. 77\u201387. ACM (2015)","DOI":"10.1145\/2813885.2737964"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A., Delbianco, G.A.: Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In: OOPSLA. pp. 92\u2013110. ACM (2016)","DOI":"10.1145\/3022671.2983999"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: CADE. Lecture Notes in Computer Science, vol.\u00a03632, pp. 219\u2013234. Springer (2005)","DOI":"10.1007\/11532231_16"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: VMCAI. Lecture Notes in Computer Science, vol.\u00a05403, pp. 335\u2013348. Springer (2009)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: CAV. Lecture Notes in Computer Science, vol.\u00a06174, pp. 450\u2013464. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Rgsep action inference. In: VMCAI. Lecture Notes in Computer Science, vol.\u00a05944, pp. 345\u2013361. Springer (2010)","DOI":"10.1007\/978-3-642-11319-2_25"},{"key":"11_CR40","unstructured":"Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods. p.\u00a0561. North-Holland (1990)"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Zhu, H., Petri, G., Jagannathan, S.: Poling: SMT aided linearizability proofs. In: CAV (2). Lecture Notes in Computer Science, vol.\u00a09207, pp.3\u201319. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_1"}],"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-44914-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:10:05Z","timestamp":1656609005000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","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":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"87","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":"27","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":"31% - 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,3","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":"11-12","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 conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}