Skip to main content

A verified messaging system

Author(s): Mansky, William; Appel, Andrew W; Nogin, Aleksey

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1gq6r24w
Full metadata record
DC FieldValueLanguage
dc.contributor.authorMansky, William-
dc.contributor.authorAppel, Andrew W-
dc.contributor.authorNogin, Aleksey-
dc.date.accessioned2023-12-19T20:09:34Z-
dc.date.available2023-12-19T20:09:34Z-
dc.date.issued2017-10en_US
dc.identifier.citationWilliam Mansky, Andrew W. Appel, and Aleksey Nogin. 2017. A Verified Messaging System. Proc. ACM Program. Lang. 1, OOPSLA, Article 87 (October 2017), 28 pages. https://doi.org/10.1145/3133911en_US
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1gq6r24w-
dc.description.abstractWe 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.en_US
dc.languageenen_US
dc.language.isoen_USen_US
dc.relation.ispartofProceedings of the ACM on Programming Languagesen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.subjectshared-memory communication, shared-memory concurrency, concurrent separation logicen_US
dc.titleA verified messaging systemen_US
dc.typeJournal Articleen_US
dc.identifier.doi10.1145/3133911-
dc.identifier.eissn2475-1421-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/journal-articleen_US

Files in This Item:
File Description SizeFormat 
VerifiedMessagingSystem.pdf860.74 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.