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.
Semantics for Locking Specifications
MACEDONIO, Damiano;MERRO, Massimo
;SPOTO, Nicola Fausto
2016-01-01
Abstract
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.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
paper_28.pdf
accesso aperto
Descrizione: Articolo definitivo.
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
547.18 kB
Formato
Adobe PDF
|
547.18 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.