Pubblicazioni

Semantics for Locking Specifications  (2015)

Autori:
Ernst, Michael D.; Macedonio, Damiano; Merro, Massimo; Spoto, Nicola Fausto
Titolo:
Semantics for Locking Specifications
Anno:
2015
Tipologia prodotto:
Rapporti di ricerca
Tipologia ANVUR:
Altro
Lingua:
Inglese
Formato:
Elettronico
Parole chiave:
Concurrent Java, Data race protection, formal semantics
Breve descrizione dei contenuti:
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.
Pagina Web:
http://arxiv.org/abs/1501.05338
Dipartimento:
Id prodotto:
91264
Handle IRIS:
11562/937559
ultima modifica:
28 settembre 2020
Citazione bibliografica:
Ernst, Michael D.; Macedonio, Damiano; Merro, Massimo; Spoto, Nicola Fausto, Semantics for Locking Specifications, Dipartimento Informatica,  N°  , 2015

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

Progetti Collegati
Titolo Dipartimento Responsabili
Static Analysis for Multithreading - Joint Project 2011 Dipartimento Informatica Massimo Merro
<<indietro

Attività

Strutture