Download: PDF.
“Semantics for locking specifications” by Michael D. Ernst, Damiano Macedonio, Massimo Merro, and Fausto Spoto. University of Washington Department of Computer Science and Engineering technical report UW-CSE-15-09-01, (Seattle, WA, USA), Sep. 2015.
To prevent concurrency errors, programmers need to obey a locking
discipline. Annotations that specify that discipline, such as Java's
@GuardedBy
, are already widely used. Unfortunately, their
semantics is 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.
BibTeX entry:
@techreport{ErnstMMS2015, author = {Michael D. Ernst and Damiano Macedonio and Massimo Merro and Fausto Spoto}, title = {Semantics for locking specifications}, institution = {University of Washington Department of Computer Science and Engineering}, number = {UW-CSE-15-09-01}, address = {Seattle, WA, USA}, month = sep, year = {2015} }
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.