{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:37:10Z","timestamp":1770280630462,"version":"3.49.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006831","name":"U.S. Air Force","doi-asserted-by":"publisher","award":["FA8750-12-C-0281"],"award-info":[{"award-number":["FA8750-12-C-0281"]}],"id":[{"id":"10.13039\/100006831","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0293"],"award-info":[{"award-number":["FA8750-12-2-0293"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-152160"],"award-info":[{"award-number":["CCF-152160"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100002418","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":[[2017,10,12]]},"abstract":"<jats:p>We present a concurrent-read exclusive-write buffer system with strong correctness and security properties. Our motivating application for this system is the distribution of sensor values in a multicomponent vehicle-control system, where some components are unverified and possibly malicious, and other components are vehicle-control-critical and must be verified. Valid participants are guaranteed correct communication (i.e., the writer is always able to write to an unused buffer, and readers always read the most recently published value), while invalid readers or writers cannot compromise the correctness or liveness of valid participants. There is only one writer, all operations are wait-free, and there is no extra process or thread mediating communication. We prove the correctness of the system with valid participants by formally verifying a C implementation of the system in Coq, using the Verified Software Toolchain extended with an atomic exchange operation. The result is the first C-level mechanized verification of a nonblocking communication protocol.<\/jats:p>","DOI":"10.1145\/3133911","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["A verified messaging system"],"prefix":"10.1145","volume":"1","author":[{"given":"William","family":"Mansky","sequence":"first","affiliation":[{"name":"Princeton University, USA"}]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"given":"Aleksey","family":"Nogin","sequence":"additional","affiliation":[{"name":"HRL Labs, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22969-0_6"},{"key":"e_1_2_1_3_1","unstructured":"Darren Cofer and Michael Whalen. 2013. Secure Mathematically-Assured Composition of Control Models (SMACCM). (2013). https:\/\/wiki.sei.cmu.edu\/aadl\/images\/f\/f6\/SMACCM- TA4- whalen- 42013.pdf  Darren Cofer and Michael Whalen. 2013. Secure Mathematically-Assured Composition of Control Models (SMACCM). (2013). https:\/\/wiki.sei.cmu.edu\/aadl\/images\/f\/f6\/SMACCM- TA4- whalen- 42013.pdf"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/362759.362813"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(93)90095-L"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_12_1","volume-title":"Using Promela and Spin to verify parallel algorithms. (1","author":"McKenney Paul E.","year":"2007","unstructured":"Paul E. McKenney . 2007. Using Promela and Spin to verify parallel algorithms. (1 August 2007 ). Available: http:\/\/lwn.net\/ Articles\/243851\/ . Paul E. McKenney. 2007. Using Promela and Spin to verify parallel algorithms. (1 August 2007). Available: http:\/\/lwn.net\/ Articles\/243851\/ ."},{"key":"e_1_2_1_13_1","volume-title":"Slingwine","author":"McKenney Paul E.","year":"1998","unstructured":"Paul E. McKenney and John D . Slingwine . 1998 . Read-Copy Update: Using Execution History to Solve Concurrency Problems. In Parallel and Distributed Computing and Systems. Las Vegas, NV , 509\u2013518. Paul E. McKenney and John D. Slingwine. 1998. Read-Copy Update: Using Execution History to Solve Concurrency Problems. In Parallel and Distributed Computing and Systems. Las Vegas, NV, 509\u2013518."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190261"},{"key":"e_1_2_1_17_1","volume-title":"ICRA Workshop on Open Source Software.","author":"Quigley Morgan","unstructured":"Morgan Quigley , Ken Conley , Brian P. Gerkey , Josh Faust , Tully Foote , Jeremy Leibs , Rob Wheeler , and Andrew Y. Ng . 2009. ROS: an open-source Robot Operating System . In ICRA Workshop on Open Source Software. Morgan Quigley, Ken Conley, Brian P. Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Y. Ng. 2009. ROS: an open-source Robot Operating System. In ICRA Workshop on Open Source Software."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133911","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133911","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133911","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:25Z","timestamp":1750212805000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133911"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":20,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133911"],"URL":"https:\/\/doi.org\/10.1145\/3133911","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}