{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T05:27:38Z","timestamp":1770269258052,"version":"3.49.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1942711"],"award-info":[{"award-number":["1942711"]}],"id":[{"id":"10.13039\/100000001","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":[[2022,4,29]]},"abstract":"<jats:p>Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods\u2014the property known as linearizability\u2014and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls\u2014or serializability.<\/jats:p>\n          <jats:p>\n            We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of\n            <jats:italic>transactional predication<\/jats:italic>\n            ; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on\n            <jats:italic>interaction trees<\/jats:italic>\n            \u2014i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.\n          <\/jats:p>","DOI":"10.1145\/3527324","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["C4: verified transactional objects"],"prefix":"10.1145","volume":"6","author":[{"given":"Mohsen","family":"Lesani","sequence":"first","affiliation":[{"name":"University of California at Riverside, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2673-4400","authenticated-orcid":false,"given":"Li-yao","family":"Xia","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"given":"Anders","family":"Kaseorg","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Christian J.","family":"Bell","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7839-1636","authenticated-orcid":false,"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","volume-title":"Shared memory consistency models: A tutorial. computer, 29, 12","author":"Adve Sarita V","year":"1996","unstructured":"Sarita V Adve and Kourosh Gharachorloo . 1996. Shared memory consistency models: A tutorial. computer, 29, 12 ( 1996 ), 66\u201376. Sarita V Adve and Kourosh Gharachorloo. 1996. Shared memory consistency models: A tutorial. computer, 29, 12 (1996), 66\u201376."},{"key":"e_1_2_1_3_1","unstructured":"Timos Antonopoulos Paul Gazzillo Eric Koskinen and Zhong Shao. 2016. Vertical Composition of Reversible Atomic Objects.  Timos Antonopoulos Paul Gazzillo Eric Koskinen and Zhong Shao. 2016. Vertical Composition of Reversible Atomic Objects."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60225-7_4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374514"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131360"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429099"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835703"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Andrea Cerone Alexey Gotsman and Hongseok Yang. 2014. Parameterised linearisability. In International Colloquium on Automata Languages and Programming. 98\u2013109.  Andrea Cerone Alexey Gotsman and Hongseok Yang. 2014. Parameterised linearisability. In International Colloquium on Automata Languages and Programming. 98\u2013109.","DOI":"10.1007\/978-3-662-43951-7_9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473599"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15291-7_2"},{"key":"e_1_2_1_14_1","volume-title":"Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects. In Asian Symposium on Programming Languages and Systems. 313\u2013331","author":"Dickerson Thomas","year":"2019","unstructured":"Thomas Dickerson , Eric Koskinen , Paul Gazzillo , and Maurice Herlihy . 2019 . Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects. In Asian Symposium on Programming Languages and Systems. 313\u2013331 . Thomas Dickerson, Eric Koskinen, Paul Gazzillo, and Maurice Herlihy. 2019. Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects. In Asian Symposium on Programming Languages and Systems. 313\u2013331."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0225-8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3301491"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_30"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Xinyu Feng. 2009. Local rely-guarantee reasoning. In POPL \u201909.  Xinyu Feng. 2009. Local rely-guarantee reasoning. In POPL \u201909.","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462172"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_19"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/218607.218611"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345233"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065952"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555283"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345237"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/165123.165164"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2901318.2901348"},{"key":"e_1_2_1_33_1","unstructured":"Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP.  Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601339"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.03.001"},{"key":"e_1_2_1_36_1","unstructured":"Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In Information Processing 83. 9 321\u2013332.  Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In Information Processing 83. 9 321\u2013332."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_38_1","volume-title":"Iris: Monoids and Invariants As an Orthogonal Basis for Concurrent Reasoning. In POPL \u201915. 637\u2013650. isbn:978-1-4503-3300-9","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 POPL \u201915. 637\u2013650. isbn:978-1-4503-3300-9 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 POPL \u201915. 637\u2013650. isbn:978-1-4503-3300-9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_14"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3303084.3309491"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3380536.3380543"},{"key":"e_1_2_1_43_1","volume-title":"Concurrent programming in Java: design principles and patterns","author":"Lea Douglas","unstructured":"Douglas Lea . 2000. Concurrent programming in Java: design principles and patterns . Addison-Wesley Professional . Douglas Lea. 2000. Concurrent programming in Java: design principles and patterns. Addison-Wesley Professional."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_36"},{"key":"e_1_2_1_45_1","volume-title":"Workshop on the theory of transactional memory. 137\u2013151","author":"Lesani Mohsen","year":"2012","unstructured":"Mohsen Lesani , Victor Luchangco , and Mark Moir . 2012 . Putting opacity in its place . In Workshop on the theory of transactional memory. 137\u2013151 . Mohsen Lesani, Victor Luchangco, and Mark Moir. 2012. Putting opacity in its place. In Workshop on the theory of transactional memory. 137\u2013151."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_37"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6342476"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491435"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660217"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_7"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1402227.1402235"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.01.002"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.024"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3148964"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_21"},{"key":"e_1_2_1_61_1","unstructured":"Michael Scott. 2006. Sequential specification of transactional memory semantics.  Michael Scott. 2006. Sequential specification of transactional memory semantics."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048073"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/224964.224987"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908112"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_2_1_68_1","unstructured":"Viktor Vafeiadis and Matthew Parkinson. 2007. A Marriage of Rely\/Guarantee and Separation Logic. In CONCUR.  Viktor Vafeiadis and Matthew Parkinson. 2007. A Marriage of Rely\/Guarantee and Separation Logic. In CONCUR."},{"key":"e_1_2_1_69_1","volume-title":"Parkinson","author":"Windsor Matt","year":"2017","unstructured":"Matt Windsor , Mike Dodds , Ben Simner , and Matthew J . Parkinson . 2017 . Starling : Lightweight Concurrency Verification with Views. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham. 544\u2013569. isbn:978-3-319-63387-9 Matt Windsor, Mike Dodds, Ben Simner, and Matthew J. Parkinson. 2017. Starling: Lightweight Concurrency Verification with Views. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 544\u2013569. isbn:978-3-319-63387-9"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373813"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209690"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527324","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527324","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527324"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":72,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527324"],"URL":"https:\/\/doi.org\/10.1145\/3527324","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}