Publications

Semantics for Locking Specifications  (2015)

Authors:
Ernst, Michael D.; Macedonio, Damiano; Merro, Massimo; Spoto, Nicola Fausto
Title:
Semantics for Locking Specifications
Year:
2015
Type of item:
Rapporti di ricerca
Tipologia ANVUR:
Altro
Language:
Inglese
Format:
Elettronico
Keyword:
Concurrent Java, Data race protection, formal semantics
Short description of contents:
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 formalizes the semantics of @GuardedBy in two alternative ways, building on an operational semantics for a small concurrent fragment of a 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 formal tools that verify or infer such annotations.
Note:
An extended abstract is currently submitted to an International Conference.
Web page:
http://arxiv.org/abs/1501.05338
Department:
Product ID:
91264
Handle IRIS:
11562/937559
Last Modified:
September 28, 2020
Bibliographic citation:
Ernst, Michael D.; Macedonio, Damiano; Merro, Massimo; Spoto, Nicola Fausto, Semantics for Locking Specifications, Department Informatica,  N°  , 2015

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Related projects
Title Department Managers
Static Analysis for Multithreading - Joint Project 2011 Department Informatica Massimo Merro
<<back

Activities

Research facilities