{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:10Z","timestamp":1775790730805,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000879","name":"Alfred P. Sloan Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000879","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Google Faculty Fellowship"},{"name":"National Science Foundation and VMware","award":["CNS-1700521"],"award-info":[{"award-number":["CNS-1700521"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3385971","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"197-210","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Armada: low-effort verification of high-performance concurrent programs"],"prefix":"10.1145","author":[{"given":"Jacob R.","family":"Lorch","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Yixuan","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Michigan, USA \/ Yale University, USA"}]},{"given":"Manos","family":"Kapritsos","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}]},{"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[{"name":"Calibra, USA"}]},{"given":"Upamanyu","family":"Sharma","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}]},{"given":"James R.","family":"Wilcox","sequence":"additional","affiliation":[{"name":"Certora, USA"}]},{"given":"Xueyuan","family":"Zhao","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_1_2_1","volume-title":"Proc. International Symposium on Computer Architecture (ISCA). 2\u2013 14","author":"Sarita","unstructured":"Sarita V. Adve and Mark D. Hill. 1990. Weak ordering\u2014a new definition. In Proc. International Symposium on Computer Architecture (ISCA). 2\u2013 14."},{"key":"e_1_3_2_1_3_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Mike","year":"2006","unstructured":"Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006."},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of Formal Methods for Components and Objects (FMCO)","author":"Boogie","year":"2006","unstructured":"Boogie: A modular reusable verifier for PLDI \u201920, June 15\u201320, 2020, London, UK J. R. Lorch, Y. Chen, M. Kapritsos, B. Parno, S. Qadeer, U. Sharma, J. R. Wilcox, X. Zhao object-oriented programs. Proceedings of Formal Methods for Components and Objects (FMCO) (2006)."},{"key":"e_1_3_2_1_5_1","unstructured":"Sandrine Blazy Zaynah Dargaye and Xavier Leroy. 2006."},{"key":"e_1_3_2_1_6_1","volume-title":"Proc. International Symposium on Formal Methods (FM). 460\u2013475","author":"Formal","unstructured":"Formal verification of a C compiler front-end. In Proc. International Symposium on Formal Methods (FM). 460\u2013475."},{"key":"e_1_3_2_1_7_1","unstructured":"G\u00e9rard Boudol and Gustavo Petri. 2009."},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. ACM Symposium on Principles of Programming Languages (POPL). 392\u2013403","author":"Relaxed","unstructured":"Relaxed memory models: An operational approach. In Proc. ACM Symposium on Principles of Programming Languages (POPL). 392\u2013403."},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. USENIX Symposium on Operating Systems Design and Implementation (OSDI). 306\u2013322","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 Proc. USENIX Symposium on Operating Systems Design and Implementation (OSDI). 306\u2013322."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_11_1","volume-title":"Schneider","author":"Clarkson Michael R.","year":"2010","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2010."},{"key":"e_1_3_2_1_12_1","volume-title":"Journal of Computer Security 18, 6","year":"2010","unstructured":"Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157\u20131210."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In Concurrency Theory (CONCUR). 317\u2013331.","DOI":"10.1007\/BFb0055631"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_1_17_1","volume-title":"Deny-Guarantee Reasoning. In Proc. European Symposium on Programming (ESOP). 363\u2013377","author":"Dodds Mike","year":"2009","unstructured":"Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. 2009. Deny-Guarantee Reasoning. In Proc. European Symposium on Programming (ESOP). 363\u2013377."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480885"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007543"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. USENIX Conference on Operating Systems Design and Implementation (OSDI). 653\u2013669","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 Proc. USENIX Conference on Operating Systems Design and Implementation (OSDI). 653\u2013669."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_1_23_1","unstructured":"Chris Hawblitzel Erez Petrank Shaz Qadeer and Serdar Tasiran. 2015."},{"key":"e_1_3_2_1_24_1","volume-title":"Proc. Computer Aided Verification (CAV). 449\u2013465","author":"Automated","unstructured":"Automated and modular refinement reasoning for concurrent programs. In Proc. Computer Aided Verification (CAV). 449\u2013465."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_1_28_1","unstructured":"Jieung Kim Vilhelm Sj\u00f6berg Ronghui Gu and Zhong Shao. 2017."},{"key":"e_1_3_2_1_29_1","volume-title":"Proc. Asian Symposium on Programming Languages and Systems (APLAS). 273\u2013297","author":"Safety","unstructured":"Safety and liveness of MCS lock\u2014layer by layer. In Proc. Asian Symposium on Programming Languages and Systems (APLAS). 273\u2013297."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_34_1","unstructured":"Hongjin Liang Xinyu Feng and Ming Fu. 2012."},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. ACM Symposium on Principles of Programming Languages (POPL). 455\u2013468","author":"A","unstructured":"A rely-guaranteebased simulation for verifying concurrent program transformations. In Proc. ACM Symposium on Principles of Programming Languages (POPL). 455\u2013468."},{"key":"e_1_3_2_1_36_1","unstructured":"LibLFDS. 2019."},{"key":"e_1_3_2_1_37_1","unstructured":"LFDS 7.11 queue implementation. https: \/\/github.com\/liblfds\/liblfds7.1.1\/tree\/master\/liblfds7.1.1\/liblfds711\/ src\/lfds711_queue_bounded_singleproducer_singleconsumer."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_2_1_40_1","volume-title":"Proc. ACM Symposium on Principles of Distributed Computing (PODC). 267\u2013275","author":"Maged","unstructured":"Maged M. Michael and Michael L. Scott. 2006. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proc. ACM Symposium on Principles of Distributed Computing (PODC). 267\u2013275."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.024"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"e_1_3_2_1_43_1","unstructured":"Scott Owens Susmit Sarkar and Peter Sewell. 2009."},{"key":"e_1_3_2_1_44_1","volume-title":"Proc. Theorem Proving in Higher Order Logics (TPHOLs). 391\u2013407","author":"A","unstructured":"A better x86 memory model: x86-TSO. In Proc. Theorem Proving in Higher Order Logics (TPHOLs). 391\u2013407."},{"key":"e_1_3_2_1_45_1","unstructured":"Shaz Qadeer. 2019. Private Communication."},{"key":"e_1_3_2_1_46_1","unstructured":"John Rushby. 1992. Noninterference Transitivity and Channel-control Security Policies. Technical Report CSL-92-02 SRI International."},{"key":"e_1_3_2_1_47_1","volume-title":"Proc. Interactive Theorem Proving (ITP). 403\u2013418","author":"Schirmer Norbert","year":"2010","unstructured":"Norbert Schirmer and Ernie Cohen. 2010. From total store order to sequential consistency: A practical reduction theorem. In Proc. Interactive Theorem Proving (ITP). 403\u2013418."},{"key":"e_1_3_2_1_48_1","volume-title":"Proc. USENIX Symposium on Operating Systems Design and Implementation (OSDI). 287\u2013305","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 Proc. USENIX Symposium on Operating Systems Design and Implementation (OSDI). 287\u2013305."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_2_1_50_1","volume-title":"Proc. ACM Symposium on Principles of Programming Languages (POPL). 43\u201354","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 Proc. ACM Symposium on Principles of Programming Languages (POPL). 43\u201354."},{"key":"e_1_3_2_1_51_1","unstructured":"David A. Wheeler. 2004."}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385971","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3385971","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:14Z","timestamp":1750200074000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385971"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":51,"alternative-id":["10.1145\/3385412.3385971","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3385971","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}