{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:29:54Z","timestamp":1784255394515,"version":"3.55.0"},"reference-count":83,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2008633"],"award-info":[{"award-number":["2008633"]}],"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,10,31]]},"abstract":"<jats:p>\n            There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions (\n            <jats:italic>e.g.<\/jats:italic>\n            , concurrent objects, transactional memory, etc.) simplify matters, but still involve intricate engineering. We argue that some difficulty of multicore programming can be meliorated through a declarative programming style in which programmers directly express the independence of fragments of sequential programs.\n          <\/jats:p>\n          <jats:p>In our proposed paradigm, programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments sequentially commute. Putting such commutativity conditions into source code offers a new entry point for a compiler to exploit the known connection between commutativity and parallelism. We give a semantics for the programmer\u2019s sequential perspective and, under a correctness condition, find that a compiler-transformed parallel execution is equivalent to the sequential semantics. Serializability\/linearizability are not the right fit for this condition, so we introduce scoped serializability and show how it can be enforced with lock synthesis techniques.<\/jats:p>\n          <jats:p>We next describe a technique for automatically verifying and synthesizing commute conditions via a new reduction from our commute blocks to logical specifications, upon which symbolic commutativity reasoning can be performed. We implemented our work in a new language called Veracity, implemented in Multicore OCaml. We show that commutativity conditions can be automatically generated across a variety of new benchmark programs, confirm the expectation that concurrency speedups can be seen as the computation increases, and apply our work to a small in-memory filesystem and an adaptation of a crowdfund blockchain smart contract.<\/jats:p>","DOI":"10.1145\/3563349","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1726-1756","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Veracity: declarative multicore programming with commutativity"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5159-6532","authenticated-orcid":false,"given":"Adam","family":"Chen","sequence":"first","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8602-2862","authenticated-orcid":false,"given":"Parisa","family":"Fathololumi","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7363-634X","authenticated-orcid":false,"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6708-5262","authenticated-orcid":false,"given":"Jared","family":"Pincus","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2014. Multicore OCaml.  https:\/\/github.com\/ocaml-multicore\/ocaml-multicore \t\t\t\t  2014. Multicore OCaml.  https:\/\/github.com\/ocaml-multicore\/ocaml-multicore"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508273"},{"key":"e_1_2_1_3_1","first-page":"116","article-title":"The Fortress language specification","volume":"139","author":"Allen Eric","year":"2005","unstructured":"Eric Allen , David Chase , Joe Hallett , Victor Luchangco , Jan-Willem Maessen , Sukyoung Ryu , Guy L Steele Jr , Sam Tobin-Hochstadt , Joao Dias , and Carl Eastlund . 2005 . The Fortress language specification . Sun Microsystems , 139 , 140 (2005), 116 . Eric Allen, David Chase, Joe Hallett, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L Steele Jr, Sam Tobin-Hochstadt, Joao Dias, and Carl Eastlund. 2005. The Fortress language specification. Sun Microsystems, 139, 140 (2005), 116.","journal-title":"Sun Microsystems"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258967"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_7"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09573-w"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1639989"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010 . The smt-lib standard: Version 2.0 . In Proceedings of the 8th international workshop on satisfiability modulo theories ( Edinburgh, England). 13, 14. Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England). 13, 14."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/PGEC.1966.264565"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025876"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.180621"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835703"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_68"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/76263.76326"},{"key":"e_1_2_1_18_1","volume-title":"Veracity: Declarative Multicore Programming with Commutativity. https:\/\/doi.org\/10.48550\/ARXIV.2203.06229","author":"Chen Adam","year":"2022","unstructured":"Adam Chen , Parisa Fathololumi , Eric Koskinen , and Jared Pincus . 2022 . Veracity: Declarative Multicore Programming with Commutativity. https:\/\/doi.org\/10.48550\/ARXIV.2203.06229 10.48550\/ARXIV.2203.06229 Adam Chen, Parisa Fathololumi, Eric Koskinen, and Jared Pincus. 2022. Veracity: Declarative Multicore Programming with Commutativity. https:\/\/doi.org\/10.48550\/ARXIV.2203.06229"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7058421"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375619"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699681"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087835"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_16"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594322"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810295.1810454"},{"key":"e_1_2_1_26_1","volume-title":"ScaleFS: A multicore-scalable file system. Ph. D. Dissertation","author":"Eqbal Rasha","unstructured":"Rasha Eqbal . 2014. ScaleFS: A multicore-scalable file system. Ph. D. Dissertation . Massachusetts Institute of Technology . Rasha Eqbal. 2014. ScaleFS: A multicore-scalable file system. Ph. D. Dissertation. Massachusetts Institute of Technology."},{"key":"#cr-split#-e_1_2_1_27_1.1","unstructured":"Gidon Ernst. 2020. A Complete Approach to Loop Verification with Invariants and Summaries. https:\/\/doi.org\/10.48550\/ARXIV.2010.05812 10.48550\/ARXIV.2010.05812"},{"key":"#cr-split#-e_1_2_1_27_1.2","unstructured":"Gidon Ernst. 2020. A Complete Approach to Loop Verification with Invariants and Summaries. https:\/\/doi.org\/10.48550\/ARXIV.2010.05812"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_4"},{"key":"e_1_2_1_29_1","volume-title":"10th $USENIX$ Symposium on Networked Systems Design and Implementation ($NSDI$ 13). 371\u2013384. https:\/\/doi.org\/10.5555\/2482626.2482662","author":"Fan Bin","unstructured":"Bin Fan , David G Andersen , and Michael Kaminsky . 2013. Memc3: Compact and concurrent memcache with dumber caching and smarter hashing . In 10th $USENIX$ Symposium on Networked Systems Design and Implementation ($NSDI$ 13). 371\u2013384. https:\/\/doi.org\/10.5555\/2482626.2482662 10.5555\/2482626.2482662 Bin Fan, David G Andersen, and Michael Kaminsky. 2013. Memc3: Compact and concurrent memcache with dumber caching and smarter hashing. In 10th $USENIX$ Symposium on Networked Systems Design and Implementation ($NSDI$ 13). 371\u2013384. https:\/\/doi.org\/10.5555\/2482626.2482662"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_18"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2688500.2688511"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19595-2_16"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345233"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949340"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555283"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62684"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/872035.872048"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/165123.165164"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290387"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993561"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/322358.322363"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_5"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_10"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993562"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346311"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250759"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2592798.2592820"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.80122"},{"key":"e_1_2_1_52_1","unstructured":"2013. libcuckoo: A high-performance concurrent hash table.  http:\/\/efficient.github.io\/libcuckoo\/ \t\t\t\t  2013. libcuckoo: A high-performance concurrent hash table.  http:\/\/efficient.github.io\/libcuckoo\/"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1248648.1248657"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54016"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2611462.2611495"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2911151.2911160"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229442"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708046.1708053"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454112"},{"key":"e_1_2_1_63_1","unstructured":"Raghu Prabhakar and Rohit Kumar. 2011. Concurrent programming with Go. Citeseer. \t\t\t\t  Raghu Prabhakar and Rohit Kumar. 2011. Concurrent programming with Go. Citeseer."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993500"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561927_10"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269969"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1123001"},{"key":"#cr-split#-e_1_2_1_68_1.1","unstructured":"Vikram Saraph and Maurice Herlihy. 2019. An empirical study of speculative concurrency in ethereum smart contracts. arXiv preprint arXiv:1901.01376 https:\/\/doi.org\/10.48550\/arXiv.1901.01376 10.48550\/arXiv.1901.01376"},{"key":"#cr-split#-e_1_2_1_68_1.2","unstructured":"Vikram Saraph and Maurice Herlihy. 2019. An empirical study of speculative concurrency in ethereum smart contracts. arXiv preprint arXiv:1901.01376 https:\/\/doi.org\/10.48550\/arXiv.1901.01376"},{"key":"e_1_2_1_69_1","unstructured":"2018. Servois: Synthesizing Commutativity Conditions.  https:\/\/github.com\/kbansal\/servois \t\t\t\t  2018. Servois: Synthesizing Commutativity Conditions.  https:\/\/github.com\/kbansal\/servois"},{"key":"e_1_2_1_70_1","unstructured":"2022. Servois2: An Extended Commutativity Condition Synthesizer.  https:\/\/github.com\/veracity-lang\/servois2 \t\t\t\t  2022. Servois2: An Extended Commutativity Condition Synthesizer.  https:\/\/github.com\/veracity-lang\/servois2"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2005.34"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCSI.2021.3102618"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048085"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.68"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706338"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.9728"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806710"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2788018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563349","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563349","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563349","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:11Z","timestamp":1750178291000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563349"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":83,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563349"],"URL":"https:\/\/doi.org\/10.1145\/3563349","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}