Semantics for locking specifications

Download: PDF, slides (PDF), slides (PowerPoint), checking implementation.

“Semantics for locking specifications” by Michael D. Ernst, Damiano Macedonio, Massimo Merro, and Fausto Spoto. In NFM 2016: 8th NASA Formal Methods Symposium, (Minneapolis, MN, USA), June 2016, pp. 355-372.
A previous version appeared as University of Washington Department of Computer Science and Engineering technical report UW-CSE-15-09-01, (Seattle, WA, USA), Sep. 2015.


Lock-based synchronization disciplines, like Java's @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 @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.

Download: PDF, slides (PDF), slides (PowerPoint), checking implementation.

BibTeX entry:

   author = {Michael D. Ernst and Damiano Macedonio and Massimo Merro and
	Fausto Spoto},
   title = {Semantics for locking specifications},
   booktitle = {NFM 2016: 8th NASA Formal Methods Symposium},
   pages = {355-372},
   address = {Minneapolis, MN, USA},
   month = jun,
   year = {2016}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.