Contextual trace refinement for concurrent objects: Safety and progress

TL;DR

This paper explores how safety and progress properties of concurrent objects relate to client program behaviors, establishing that linearizability with minimal progress guarantees ensures contextual trace refinement, unlike weaker consistency models.

Contribution

It demonstrates that linearizability combined with minimal progress guarantees suffices for contextual trace refinement, clarifying the guarantees provided to client programs.

Findings

Linearizability plus minimal progress guarantees contextual trace refinement.

Sequential and quiescent consistency are too weak for this refinement.

The action systems framework is extended to handle non-atomic operations.

Abstract

Correctness of concurrent objects is defined in terms of safety properties such as linearizability, sequential consistency, and quiescent consistency, and progress properties such as wait-, lock-, and obstruction-freedom. These properties, however, only refer to the behaviours of the object in isolation, which does not tell us what guarantees these correctness conditions on concurrent objects provide to their client programs. This paper investigates the links between safety and progress properties of concurrent objects and a form of trace refinement for client programs, called contextual trace refinement. In particular, we show that linearizability together with a minimal notion of progress are sufficient properties of concurrent objects to ensure contextual trace refinement, but sequential consistency and quiescent consistency are both too weak. Our reasoning is carried out in the action systems framework with procedure calls, which we extend to cope with non-atomic operations.