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

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.
Concurrent Java
Data race detection
Semantics of programming languages
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/944791
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact