Semantics for Locking Specifications

TL;DR

This paper formalizes the semantics of locking annotations like @GuardedBy in Java, clarifying ambiguities and aiding the development of tools to verify concurrency safety in programs.

Contribution

It provides two formal semantics for @GuardedBy annotations and identifies conditions under which they guarantee data race prevention.

Findings

Formal semantics for @GuardedBy annotations

Clarification of ambiguities in locking specifications

Guidelines for when annotations guarantee data race freedom

Abstract

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.