{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:15Z","timestamp":1780994655808,"version":"3.54.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000005","name":"US Department of Defense","doi-asserted-by":"crossref","award":["NDSEG"],"award-info":[{"award-number":["NDSEG"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100008299","name":"Dartmouth College","doi-asserted-by":"publisher","award":["James Frank Family Professorship"],"award-info":[{"award-number":["James Frank Family Professorship"]}],"id":[{"id":"10.13039\/100008299","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            We introduce simple,\n            <jats:italic toggle=\"yes\">universal<\/jats:italic>\n            ,\n            <jats:italic toggle=\"yes\">sound<\/jats:italic>\n            , and\n            <jats:italic toggle=\"yes\">complete<\/jats:italic>\n            proof methods for producing machine-verifiable proofs of linearizability and strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the TLA+ Proof System).\n          <\/jats:p>","DOI":"10.1145\/3632924","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2456-2484","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8930-3467","authenticated-orcid":false,"given":"Prasad","family":"Jayanti","sequence":"first","affiliation":[{"name":"Dartmouth College, Hanover, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2681-1632","authenticated-orcid":false,"given":"Siddhartha","family":"Jayanti","sequence":"additional","affiliation":[{"name":"Google Research, Cambridge, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6218-2466","authenticated-orcid":false,"given":"Ugur Y.","family":"Yavuz","sequence":"additional","affiliation":[{"name":"Boston University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1823-9990","authenticated-orcid":false,"given":"Lizzie","family":"Hernandez","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0415-4"},{"key":"e_1_3_1_4_1","unstructured":"M. K. Aguilera and S. Fr\u00f8lund. Strict linearizability and the power of aborting. Technical Report HPL-2003-241 Hewlett-Packard Labs 2003."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"e_1_3_1_6_1","first-page":"2:1","volume-title":"33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary, volume 146 of LIPIcs","author":"Attiya H.","year":"2019","unstructured":"H. Attiya and C. Enea. Putting strong linearizability in context: Preserving hyperproperties in programs that use concurrent objects. In J. Suomela, editor, 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary, volume 146 of LIPIcs, pages 2:1\u20132:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2019."},{"key":"e_1_3_1_7_1","first-page":"7:1","volume-title":"35th International Symposium on Distributed Computing, DISC 2021, October 4-8, 2021, Freiburg, Germany (Virtual Conference) , volume 209 of LIPIcs","author":"Attiya H.","year":"2021","unstructured":"H. Attiya, C. Enea, and J. L. Welch. Impossibility of strongly-linearizable message-passing objects via simulation by single-writer registers. In S. Gilbert, editor, 35th International Symposium on Distributed Computing, DISC 2021, October 4-8, 2021, Freiburg, Germany (Virtual Conference) , volume 209 of LIPIcs, pages 7:1\u20137:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021."},{"key":"e_1_3_1_8_1","first-page":"20:1","volume-title":"19th International Conference on Principles of Distributed Systems, OPODIS 2015, December 14-17, 2015, Rennes, France, volume 46 of LIPIcs","author":"Berryhill R.","year":"2015","unstructured":"R. Berryhill, W. M. Golab, and M. Tripunitara. Robust shared objects for non-volatile main memory. In E. Anceaume, C. Cachin, and M. G. Potop-Butucaru, editors, 19th International Conference on Principles of Distributed Systems, OPODIS 2015, December 14-17, 2015, Rennes, France, volume 46 of LIPIcs, pages 20:1\u201320:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2015."},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","unstructured":"V. Bloemen A. Laarman and J. van de Pol. Multi-core on-the-fly SCC decomposition. In Proceedings of the 21st ACM SIGPLAN symposium on Principles and practice of parallel programming PPoPP '16 page to appear 2016.","DOI":"10.1145\/2851141.2851161"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"e_1_3_1_12_1","unstructured":"D. Y. C. Chan V. Hadzilacos X. Hu and S. Toueg. An impossibility result on strong linearizability in message-passing systems. CoRR abs\/2108.01651 2021."},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"Automated Reasoning","author":"Chaudhuri K.","year":"2010","unstructured":"K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz. Verifying safety properties with the TLA+ Proof System. In J. Giesl and R. H\u00e4hnle, editors, Automated Reasoning, pages 142\u2013148, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg."},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2005.49"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_44"},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","unstructured":"L. Dhulipala C. Hong and J. Shun. ConnectIt: A framework for static and incremental parallel graph connectivity algorithms 2020.","DOI":"10.14778\/3436905.3436923"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676963"},{"key":"e_1_3_1_18_1","unstructured":"S. Doherty. Modelling and verifying non-blocking algorithms that use dynamically allocated memory. In Victoria University of Wellington 2003."},{"key":"e_1_3_1_19_1","unstructured":"B. Dongol and J. Derrick. Verifying linearizability: A comparative survey. CoRR abs\/1410.6268 2014."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993636.1993687"},{"key":"e_1_3_1_21_1","unstructured":"Google-Graph-Mining-Team. Google graph-mining. https:\/\/github.com\/google\/graph-mining 2023."},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645959.676137"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11795490_3"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2332432.2332508"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA200584"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","unstructured":"C. Hong L. Dhulipala and J. Shun. Exploring the design space of static and incremental graph connectivity algorithms on GP Us. Proceedings of the ACM International Conference on Parallel Architectures and Compilation Techniques September 2020.","DOI":"10.1145\/3410463.3414657"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060590.1060697"},{"key":"e_1_3_1_32_1","first-page":"25:1","volume-title":"37th International Symposium on Distributed Computing (DISC 2023), volume 281 of Leibniz International Proceedings in Informatics (LIPIcs)","author":"Jayanti P.","year":"2023","unstructured":"P. Jayanti, S. Jayanti, and S. Jayanti. Durable algorithms for writable LL\/SC and CAS with dynamic joining. In R. Oshman, editor, 37th International Symposium on Distributed Computing (DISC 2023), volume 281 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1\u201325:20, Dagstuhl, Germany, 2023a. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik."},{"key":"e_1_3_1_33_1","doi-asserted-by":"crossref","unstructured":"P. Jayanti S. Jayanti U. Y. Yavuz and L. Hernandez Videa. Artifact for \u201cA Universal Sound and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability\u201d POPL 2024 Oct. 2023b.","DOI":"10.1145\/3632924"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293611.3331593"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933108"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-020-00388-x"},{"key":"e_1_3_1_37_1","unstructured":"M. Jones. What really happened to the software on the Mars Pathfinder spacecraft\u0152 https:\/\/www.rapitasystems.com\/blog\/what-really-happened-software-mars-pathfinder-spacecraft July 2013."},{"key":"e_1_3_1_38_1","first-page":"361","volume-title":"Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989, Proceedings, volume 430 of Lecture Notes in Computer Science","author":"Jonsson B.","year":"1989","unstructured":"B. Jonsson. On decomposing and refining specifications of distributed systems. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989, Proceedings, volume 430 of Lecture Notes in Computer Science, pages 361\u2013385. Springer, 1989."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54430-5_99"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/69624.357207"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492545"},{"key":"e_1_3_1_45_1","doi-asserted-by":"crossref","unstructured":"N. Leveson and C. Turner. An investigation of the Therac-25 accidents. Computer 1993.","DOI":"10.1109\/MC.1993.274940"},{"key":"e_1_3_1_46_1","unstructured":"J. Lim. An engineering disaster: Therac-25 1998."},{"key":"e_1_3_1_47_1","volume-title":"Distributed Algorithms","author":"Lynch N. A.","year":"1996","unstructured":"N. A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996."},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498694"},{"key":"e_1_3_1_50_1","doi-asserted-by":"crossref","DOI":"10.1145\/3571231","article-title":"A compositional theory of linearizability","volume":"7","author":"Vale A. Oliveira","year":"2023","unstructured":"A. Oliveira Vale, Z. Shao, and Y. Chen. A compositional theory of linearizability. Proc. ACM Program. Lang., 7(POPL), Jan. 2023.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_1_52_1","unstructured":"K. Poulsen. Software bug contributed to blackout. SecurityFocus 2004."},{"key":"e_1_3_1_53_1","doi-asserted-by":"crossref","unstructured":"W. Reif G. Schellhorn K. Stenzel and M. Balser. Structured specifications and interactive proofs with KIV. Automated Deduction\u2014A Basis for Applications: Volume II: Systems and Implementation Techniques pages 13\u201339 1998.","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"e_1_3_1_54_1","first-page":"99","volume-title":"Eighteenth International Symposium on Temporal Representation and Reasoning, TIME 2011, L\u00fcbeck, Germany, September 12-14, 2011","author":"Schellhorn G.","year":"2011","unstructured":"G. Schellhorn, B. Tofan, G. Ernst, and W. Reif. Interleaved programs and rely-guarantee reasoning with I TL. In C. Combi, M. Leucker, and F. Wolter, editors, Eighteenth International Symposium on Temporal Representation and Reasoning, TIME 2011, L\u00fcbeck, Germany, September 12-14, 2011, pages 99\u2013106. IEEE, 2011."},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629496"},{"key":"e_1_3_1_56_1","volume-title":"Technical Report UCAM-CL-TR-726","author":"Vafeiadis V.","year":"2008","unstructured":"V. Vafeiadis. Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory, July 2008."},{"key":"e_1_3_1_57_1","first-page":"335","volume-title":"Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings, volume 5403 of Lecture Notes in Computer Science","author":"Vafeiadis V.","year":"2009","unstructured":"V. Vafeiadis. Shape-value abstraction for verifying linearizability. In N. D. Jones and M. M\u00fcller-Olm, editors, Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings, volume 5403 of Lecture Notes in Computer Science, pages 335\u2013348. Springer, 2009."},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632924","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632924","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:37Z","timestamp":1751659537000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632924"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632924"],"URL":"https:\/\/doi.org\/10.1145\/3632924","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}