{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:08:06Z","timestamp":1755839286521,"version":"3.41.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,5,27]],"date-time":"2022-05-27T00:00:00Z","timestamp":1653609600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["FMitF-2018915"],"award-info":[{"award-number":["FMitF-2018915"]}]},{"name":"National Science Foundation and VMware","award":["CNS-1700521"],"award-info":[{"award-number":["CNS-1700521"]}]},{"DOI":"10.13039\/100000879","name":"Alfred P. Sloan Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100000879","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Google Faculty Fellowship"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2022,6,30]]},"abstract":"<jats:p>Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, state-machine-based semantics, Armadagives developers the flexibility to choose arbitrary memory layout and synchronization primitives so that they are never constrained in their pursuit of performance. To reduce developer effort, Armadaleverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and pointer analysis. All of these techniques are proven sound, and Armadacan be soundly extended with additional strategies over time. Using Armada, we verify five concurrent case studies and show that we can achieve performance equivalent to that of unverified code.<\/jats:p>","DOI":"10.1145\/3502491","type":"journal-article","created":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T22:19:11Z","timestamp":1646432351000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility"],"prefix":"10.1145","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7269-2769","authenticated-orcid":false,"given":"Jacob R.","family":"Lorch","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8659-8493","authenticated-orcid":false,"given":"Yixuan","family":"Chen","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}]},{"given":"Manos","family":"Kapritsos","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2155-4809","authenticated-orcid":false,"given":"Haojun","family":"Ma","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]},{"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[{"name":"Calibra, Bellevue, WA, USA"}]},{"given":"Upamanyu","family":"Sharma","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"given":"James R.","family":"Wilcox","sequence":"additional","affiliation":[{"name":"Certora, Seattle, WA, USA"}]},{"given":"Xueyuan","family":"Zhao","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, PA, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,5,27]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_1_3_2","first-page":"2","volume-title":"Proceedings of International Symposium on Computer Architecture (ISCA\u201990)","author":"Adve Sarita V.","year":"1990","unstructured":"Sarita V. Adve and Mark D. Hill. 1990. Weak ordering\u2014a new definition. In Proceedings of International Symposium on Computer Architecture (ISCA\u201990). 2\u201314."},{"key":"e_1_3_1_4_2","article-title":"Boogie: A modular reusable verifier for object-oriented programs","author":"Barnett Mike","year":"2005","unstructured":"Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of Formal Methods for Components and Objects (FMCO\u201905). 364\u2013387.","journal-title":"Proceedings of Formal Methods for Components and Objects (FMCO\u201905)."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480930"},{"key":"e_1_3_1_7_2","first-page":"306","volume-title":"Proceedings of Symposium on Operating Systems Design and Implementation (OSDI\u201918)","author":"Chajed Tej","year":"2018","unstructured":"Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, and Nickolai Zeldovich. 2018. Verifying concurrent software using movers in CSPEC. In Proceedings of Symposium on Operating Systems Design and Implementation (OSDI\u201918). 306\u2013322."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"Concurrency Theory (CONCUR\u201998)","author":"Cohen Ernie","year":"1998","unstructured":"Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In Concurrency Theory (CONCUR\u201998). 317\u2013331."},{"key":"e_1_3_1_12_2","first-page":"207","volume-title":"Proceedings of European Conference on Object-Oriented Programming (ECOOP\u201914)","author":"Pinto Pedro da Rocha","year":"2014","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In Proceedings of European Conference on Object-Oriented Programming (ECOOP\u201914). 207\u2013231."},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480885"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007543"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_1_19_2","first-page":"653","volume-title":"Proceedings of USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916). 653\u2013669."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_1_21_2","article-title":"Market share of the x86 architecture","author":"Hardware Tom\u2019s","year":"2021","unstructured":"Tom\u2019s Hardware. 2021. Market share of the x86 architecture. Retrieved March 15, 2022 from https:\/\/www.tomshardware.com\/news\/amds-cpu-market-share-and-revenue-jump-as-apples-m1-arm-chips-rise.","journal-title":"https:\/\/www.tomshardware.com\/news\/amds-cpu-market-share-and-revenue-jump-as-apples-m1-arm-chips-rise"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"issue":"20","key":"e_1_3_1_24_2","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28, e20 (2018).","journal-title":"Journal of Functional Programming"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_29_2","first-page":"37:1\u201337:31","article-title":"Go with the flow: Compositional abstractions for concurrent data structures","author":"Krishna Siddharth","year":"2018","unstructured":"Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. 2018. Go with the flow: Compositional abstractions for concurrent data structures. Proceedings of the ACM Symposium on Programming Languages 2 (POPL\u201918). 37:1\u201337:31.","journal-title":"Proceedings of the ACM Symposium on Programming Languages 2 (POPL\u201918)."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103711"},{"key":"e_1_3_1_32_2","article-title":"LFDS 7.11 queue implementation","year":"2019","unstructured":"LibLFDS. 2019. LFDS 7.11 queue implementation. Retrieved March 15, 2022 from https:\/\/github.com\/liblfds\/liblfds7.1.1\/tree\/master\/liblfds7.1.1\/liblfds71\\1\/src\/lfds711_queue_bounded_singleproducer_singleconsumer. (Nov. 2019).","journal-title":"https:\/\/github.com\/liblfds\/liblfds7.1.1\/tree\/master\/liblfds7.1.1\/liblfds71\\1\/src\/lfds711_queue_bounded_singleproducer_singleconsumer"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_1_36_2","first-page":"267","volume-title":"Proceedings of ACM Symposium on Principles of Distributed Computing (PODC\u201906)","author":"Michael Maged M.","year":"2006","unstructured":"Maged M. Michael and Michael L. Scott. 2006. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of ACM Symposium on Principles of Distributed Computing (PODC\u201906). 267\u2013275."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_1_41_2","unstructured":"Shaz Qadeer. 2019. Private communication. (2019)."},{"key":"e_1_3_1_42_2","article-title":"Noninterference, Transitivity, and Channel-control Security Policies","author":"Rushby John","year":"1992","unstructured":"John Rushby. 1992. Noninterference, Transitivity, and Channel-control Security Policies. Technical Report CSL-92-02, SRI International. (1992).","journal-title":"Technical Report CSL-92-02, SRI International"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3436808"},{"key":"e_1_3_1_44_2","first-page":"403","volume-title":"Proceedings of Interactive Theorem Proving (ITP\u201910)","author":"Schirmer Norbert","year":"2010","unstructured":"Norbert Schirmer and Ernie Cohen. 2010. From total store order to sequential consistency: A practical reduction theorem. In Proceedings of Interactive Theorem Proving (ITP\u201910). 403\u2013418."},{"key":"e_1_3_1_45_2","first-page":"287","volume-title":"Proceedings of USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201918)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A framework for design and verification of information flow control systems. In Proceedings of USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201918). 287\u2013305."},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_1_47_2","first-page":"43","volume-title":"Proceedings of ACM Symposium on Principles of Programming Languages (POPL\u201911)","author":"\u0160ev\u010d\u00edk Jaroslav","year":"2011","unstructured":"Jaroslav \u0160ev\u010d\u00edk, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. 2011. Relaxed-memory concurrency and verified compilation. In Proceedings of ACM Symposium on Principles of Programming Languages (POPL\u201911). 43\u201354."},{"key":"e_1_3_1_48_2","article-title":"SLOCCount","author":"Wheeler David A.","year":"2004","unstructured":"David A. Wheeler. 2004. SLOCCount. Software distribution. (2004). Retrieved March 15, 2022 from http:\/\/www.dwheeler.com\/sloccount\/.","journal-title":"Software distribution"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3502491","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3502491","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:12:00Z","timestamp":1750191120000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3502491"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,27]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6,30]]}},"alternative-id":["10.1145\/3502491"],"URL":"https:\/\/doi.org\/10.1145\/3502491","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2022,5,27]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}