{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:21Z","timestamp":1776305061881,"version":"3.50.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["CCF-2008633 and CCF-2315363"],"award-info":[{"award-number":["CCF-2008633 and CCF-2315363"]}]},{"name":"Agence Nationale de la Recherche","award":["SCEPROOF"],"award-info":[{"award-number":["SCEPROOF"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Concurrent objects form the foundation of many applications that exploit multicore architectures and their importance has lead to informal correctness arguments, as well as formal proof systems. Correctness arguments (as found in the distributed computing literature) give intuitive descriptions of a few canonical executions or \"scenarios\" often each with only a few threads, yet it remains unknown as to whether these intuitive arguments have a formal grounding and extend to arbitrary interleavings over unboundedly many threads.<\/jats:p>\n          <jats:p>We present a novel proof technique for concurrent objects, based around identifying a small set of scenarios (representative, canonical interleavings), formalized as the commutativity quotient of a concurrent object. We next give an expression language for defining abstractions of the quotient in the form of regular or context-free languages that enable simple proofs of linearizability. These quotient expressions organize unbounded interleavings into a form more amenable to reasoning and make explicit the relationship between implementation-level contention\/interference and ADT-level transitions.<\/jats:p>\n          <jats:p>We evaluate our work on numerous non-trivial concurrent objects from the literature (including the Michael-Scott queue, Elimination stack, SLS reservation queue, RDCSS and Herlihy-Wing queue). We show that quotients capture the diverse features\/complexities of these algorithms, can be used even when linearization points are not straight-forward, correspond to original authors' correctness arguments, and provide some new scenario-based arguments. Finally, we show that discovery of some object's quotients reduces to two-thread reasoning and give an implementation that can derive candidate quotients expressions from source code.<\/jats:p>","DOI":"10.1145\/3649857","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"1294-1323","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Scenario-Based Proofs for Concurrent Objects"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"first","affiliation":[{"name":"LIX - CNRS - \u00c9cole Polytechnique, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7363-634X","authenticated-orcid":false,"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, Hoboken, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, Xavier Rival (Ed.) (Lecture Notes in Computer Science","volume":"83","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla, Bengt Jonsson, and Cong Quy Trinh. 2016. Automated Verification of Linearization Policies. In Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, Xavier Rival (Ed.) (Lecture Notes in Computer Science, Vol. 9837). Springer, 61\u201383. https:\/\/doi.org\/10.1007\/978-3-662-53413-7_4 10.1007\/978-3-662-53413-7_4"},{"key":"e_1_2_1_2_1","volume-title":"20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, Aarti Gupta and Sharad Malik (Eds.) (Lecture Notes in Computer Science","volume":"413","author":"Berdine Josh","year":"2008","unstructured":"Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, and Shmuel Sagiv. 2008. Thread Quantification for Concurrent Shape Analysis. In Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, Aarti Gupta and Sharad Malik (Eds.) (Lecture Notes in Computer Science, Vol. 5123). Springer, 399\u2013413. https:\/\/doi.org\/10.1007\/978-3-540-70545-1_37 10.1007\/978-3-540-70545-1_37"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005","author":"Bornat Richard","year":"2005","unstructured":"Richard Bornat, Cristiano Calcagno, Peter W. O\u2019Hearn, and Matthew J. Parkinson. 2005. Permission accounting in separation logic. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. 259\u2013270. https:\/\/doi.org\/10.1145\/1040305.1040327 10.1145\/1040305.1040327"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_6_1","volume-title":"CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 16\u201334","author":"Brookes Stephen D.","year":"2004","unstructured":"Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 16\u201334. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2 10.1007\/978-3-540-28644-8_2"},{"key":"e_1_2_1_7_1","unstructured":"Tej Chajed M. Frans Kaashoek Butler W. Lampson and Nickolai Zeldovich. 2018. Verifying concurrent software using movers in CSPEC. In OSDI. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/chajed"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"e_1_2_1_9_1","volume-title":"10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, Alan J. Hu and Moshe Y. Vardi (Eds.) (Lecture Notes in Computer Science","volume":"158","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla. 1998. Symmetry Reductions in Model Checking. In Computer Aided Verification, 10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, Alan J. Hu and Moshe Y. Vardi (Eds.) (Lecture Notes in Computer Science, Vol. 1427). Springer, 147\u2013158. https:\/\/doi.org\/10.1007\/BFb0028741 10.1007\/BFb0028741"},{"key":"e_1_2_1_10_1","volume-title":"TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings. 207\u2013231","author":"da Rocha Pinto Pedro","year":"2014","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings. 207\u2013231. https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9 10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_1_11_1","volume-title":"14th International Conference, DISC 2000, Toledo, Spain, October 4-6, 2000, Proceedings, Maurice Herlihy (Ed.) (Lecture Notes in Computer Science","volume":"73","author":"Detlefs David","unstructured":"David Detlefs, Christine H. Flood, Alex Garthwaite, Paul Alan Martin, Nir Shavit, and Guy L. Steele Jr.. 2000. Even Better DCAS-Based Concurrent Deques. In Distributed Computing, 14th International Conference, DISC 2000, Toledo, Spain, October 4-6, 2000, Proceedings, Maurice Herlihy (Ed.) (Lecture Notes in Computer Science, Vol. 1914). Springer, 59\u201373. https:\/\/doi.org\/10.1007\/3-540-40026-5_4 10.1007\/3-540-40026-5_4"},{"key":"e_1_2_1_12_1","volume-title":"The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913","author":"Dinsdale-Young Thomas","year":"2013","unstructured":"Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 287\u2013300. https:\/\/doi.org\/10.1145\/2429069.2429104 10.1145\/2429069.2429104"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_14_1","volume-title":"SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures","author":"Doherty Simon","year":"2004","unstructured":"Simon Doherty, David Detlefs, Lindsay Groves, Christine H. Flood, Victor Luchangco, Paul Alan Martin, Mark Moir, Nir Shavit, and Guy L. Steele Jr.. 2004. DCAS is not a silver bullet for nonblocking algorithm design. In SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, June 27-30, 2004, Barcelona, Spain, Phillip B. Gibbons and Micah Adler (Eds.). ACM, 216\u2013224. https:\/\/doi.org\/10.1145\/1007912.1007945 10.1145\/1007912.1007945"},{"key":"e_1_2_1_15_1","volume-title":"Henzinger","author":"Dragoi Cezara","year":"2013","unstructured":"Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In CAV \u201913 (LNCS, Vol. 8044). Springer, 174\u2013190."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Tayfun Elmas Shaz Qadeer and Serdar Tasiran. 2009. A calculus of atomic actions. In POPL. https:\/\/doi.org\/10.1145\/1480881.1480885 10.1145\/1480881.1480885","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_2_1_17_1","unstructured":"Constantin Enea Parisa Fathololumi and Eric Koskinen. 2023. Scenario-Based Proofs for Concurrent Objects [Extended Version]. arxiv:2301.05740."},{"key":"e_1_2_1_18_1","volume-title":"CION: Concurrent Trace Reductions. https:\/\/github.com\/quotientprovers\/cion","author":"Enea Constantin","year":"2024","unstructured":"Constantin Enea, Parisa Fathololumi, and Eric Koskinen. 2024. CION: Concurrent Trace Reductions. https:\/\/github.com\/quotientprovers\/cion"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_1_20_1","volume-title":"16th International Conference, DISC 2002, Toulouse, France, October 28-30, 2002 Proceedings, Dahlia Malkhi (Ed.) (Lecture Notes in Computer Science","volume":"279","author":"Harris Timothy L.","unstructured":"Timothy L. Harris, Keir Fraser, and Ian A. Pratt. 2002. A Practical Multi-word Compare-and-Swap Operation. In Distributed Computing, 16th International Conference, DISC 2002, Toulouse, France, October 28-30, 2002 Proceedings, Dahlia Malkhi (Ed.) (Lecture Notes in Computer Science, Vol. 2508). Springer, 265\u2013279. https:\/\/doi.org\/10.1007\/3-540-36108-1_18 10.1007\/3-540-36108-1_18"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Chris Hawblitzel Erez Petrank Shaz Qadeer and Serdar Tasiran. 2015. Automated and Modular Refinement Reasoning for Concurrent Programs. In CAV. https:\/\/doi.org\/10.1007\/978-3-319-21668-3_26 10.1007\/978-3-319-21668-3_26","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"e_1_2_1_23_1","volume-title":"SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures","author":"Hendler Danny","year":"2004","unstructured":"Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A scalable lock-free stack algorithm. In SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, June 27-30, 2004, Barcelona, Spain, Phillip B. Gibbons and Micah Adler (Eds.). ACM, 206\u2013215. https:\/\/doi.org\/10.1145\/1007912.1007944 10.1145\/1007912.1007944"},{"key":"e_1_2_1_24_1","volume-title":"The Art of Multiprocessor Programming","author":"Herlihy Maurice","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. isbn:0123705916, 9780123705914"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_26_1","volume-title":"Specification and Design of (Parallel) Programs. In IFIP Congress. 321\u2013332","author":"Jones Cliff B.","year":"1983","unstructured":"Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In IFIP Congress. 321\u2013332."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_28_1","volume-title":"Proc. ACM Program. Lang., 4, POPL","author":"Jung Ralf","year":"2020","unstructured":"Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang., 4, POPL (2020), 45:1\u201345:32. https:\/\/doi.org\/10.1145\/3371113 10.1145\/3371113"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Eric Koskinen. 2024. quotientprovers\/cion: oopsla2024-artifact: Version used in evaluation for the OOPSLA\u201924 paper \"Scenario-Based Proofs for Concurrent Objects\". https:\/\/doi.org\/10.5281\/zenodo.10814650 10.5281\/zenodo.10814650","DOI":"10.5281\/zenodo.10814650"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020","author":"Kragl Bernhard","year":"2020","unstructured":"Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. 2020. Inductive sequentialization of asynchronous programs. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 227\u2013242. isbn:978-1-4503-7613-6 https:\/\/doi.org\/10.1145\/3385412.3385980 10.1145\/3385412.3385980"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Bernhard Kragl and Shaz Qadeer. 2018. Layered Concurrent Programs. In CAV. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_5 10.1007\/978-3-319-96145-3_5","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.21"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_2_1_36_1","volume-title":"The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913","author":"Ley-Wild Ruy","year":"2013","unstructured":"Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. 561\u2013574. https:\/\/doi.org\/10.1145\/2429069.2429134 10.1145\/2429069.2429134"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of an Advanced Course","volume":"324","author":"Mazurkiewicz Antoni W.","year":"1986","unstructured":"Antoni W. Mazurkiewicz. 1986. Trace Theory. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg (Eds.) (Lecture Notes in Computer Science, Vol. 255). Springer, 279\u2013324. https:\/\/doi.org\/10.1007\/3-540-17906-2_30 10.1007\/3-540-17906-2_30"},{"key":"e_1_2_1_39_1","volume-title":"Scott","author":"Michael Maged M.","year":"1996","unstructured":"Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC \u201996. ACM, 267\u2013275."},{"key":"e_1_2_1_40_1","volume-title":"Proc. ACM Program. Lang., 3, OOPSLA","author":"Nanevski Aleksandar","year":"2019","unstructured":"Aleksandar Nanevski, Anindya Banerjee, Germ\u00e1n Andr\u00e9s Delbianco, and Ignacio F\u00e1bregas. 2019. Specifying concurrent programs in separation logic: morphisms and simulations. Proc. ACM Program. Lang., 3, OOPSLA (2019), 161:1\u2013161:30. https:\/\/doi.org\/10.1145\/3360587 10.1145\/3360587"},{"key":"e_1_2_1_41_1","volume-title":"Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 49\u201367","author":"O\u2019Hearn Peter W.","year":"2004","unstructured":"Peter W. O\u2019Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 49\u201367. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_4 10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010","author":"O\u2019Hearn Peter W.","year":"2010","unstructured":"Peter W. O\u2019Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2010. Verifying linearizability with hindsight. In Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010, Zurich, Switzerland, July 25-28, 2010, Andr\u00e9a W. Richa and Rachid Guerraoui (Eds.). ACM, 85\u201394. isbn:978-1-60558-888-9 https:\/\/doi.org\/10.1145\/1835698.1835722 10.1145\/1835698.1835722"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007","author":"Parkinson Matthew J.","year":"2007","unstructured":"Matthew J. Parkinson, Richard Bornat, and Peter W. O\u2019Hearn. 2007. Modular verification of a non-blocking stack. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007. 297\u2013302. https:\/\/doi.org\/10.1145\/1190216.1190261 10.1145\/1190216.1190261"},{"key":"e_1_2_1_46_1","volume-title":"ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 710\u2013735","author":"Raad Azalea","year":"2015","unstructured":"Azalea Raad, Jules Villard, and Philippa Gardner. 2015. CoLoSL: Concurrent Local Subjective Logic. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 710\u2013735. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_29 10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_1_47_1","volume-title":"CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. 243\u2013259","author":"Schellhorn Gerhard","year":"2012","unstructured":"Gerhard Schellhorn, Heike Wehrheim, and John Derrick. 2012. How to Prove Algorithms Linearisable. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. 243\u2013259."},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 147\u2013156","author":"William N","year":"2006","unstructured":"William N Scherer III, Doug Lea, and Michael L Scott. 2006. Scalable synchronous queues. In Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 147\u2013156."},{"key":"e_1_2_1_49_1","volume-title":"ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 333\u2013358","author":"Sergey Ilya","year":"2015","unstructured":"Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 333\u2013358. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_14 10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_1_50_1","volume-title":"Systems Programming: Coping with Parallelism","author":"Treiber R. K.","year":"1986","unstructured":"R. K. Treiber. 1986. Systems Programming: Coping with Parallelism. IBM Almaden Research Center."},{"key":"e_1_2_1_51_1","volume-title":"ACM SIGPLAN International Conference on Functional Programming, ICFP\u201913","author":"Turon Aaron","year":"2013","unstructured":"Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In ACM SIGPLAN International Conference on Functional Programming, ICFP\u201913, Boston, MA, USA - September 25 - 27, 2013. 377\u2013390. https:\/\/doi.org\/10.1145\/2500365.2500600 10.1145\/2500365.2500600"},{"key":"e_1_2_1_52_1","volume-title":"Modular fine-grained concurrency verification. Ph. D. Dissertation","author":"Vafeiadis V.","unstructured":"V. Vafeiadis. 2008. Modular fine-grained concurrency verification. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_2_1_53_1","volume-title":"Proc. 10th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (LNCS","volume":"348","author":"Vafeiadis Viktor","year":"2009","unstructured":"Viktor Vafeiadis. 2009. Shape-Value Abstraction for Verifying Linearizability. In VMCAI \u201909: Proc. 10th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (LNCS, Vol. 5403). Springer, 335\u2013348."},{"key":"e_1_2_1_54_1","volume-title":"22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.) (Lecture Notes in Computer Science","volume":"464","author":"Vafeiadis Viktor","year":"2010","unstructured":"Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.) (Lecture Notes in Computer Science, Vol. 6174). Springer, 450\u2013464. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40 10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_2_1_56_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. 3\u201319","author":"Zhu He","year":"2015","unstructured":"He Zhu, Gustavo Petri, and Suresh Jagannathan. 2015. Poling: SMT Aided Linearizability Proofs. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. 3\u201319."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649857","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649857","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:07Z","timestamp":1750287247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649857"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":56,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649857"],"URL":"https:\/\/doi.org\/10.1145\/3649857","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}