TitleSemantics for locking specifications
Publication TypeConference Paper
Year of Publication2016
AuthorsErnst MD, Macedonio D, Merro M, Spoto F
Conference NameNFM 2016: 8th NASA Formal Methods Symposium
Pagination355-372
Date or Month PublishedJune
Conference LocationMinneapolis, MN, USA
AbstractLock-based synchronization disciplines, like Java's \texttt@GuardedBy, are widely used to prevent concurrency errors. However, their semantics is often expressed informally and is consequently ambiguous. This article highlights such ambiguities and overcomes them by formalizing two possible semantics of \texttt@GuardedBy, using a reference operational semantics for a core calculus of a concurrent Java-like language. It also identifies when such annotations are actual guarantees against data races. Our work aids in understanding the annotations and supports the development of sound tools that verify or infer them.
Downloadshttps://checkerframework.org/ checking implementation https://homes.cs.washington.edu/~mernst/pubs/locking-semantics-nfm2016.pdf PDF
Citation KeyErnstMMS2016