Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation

TL;DR

The paper tackles verifying linearizability and progress properties of concurrent objects, a task traditionally handled by PSPACE-hard trace refinement. It proposes divergence-sensitive branching bisimulation (DSBB) to relate an abstract atomic specification $\Theta$ to a concrete object $O$, enabling polynomial-time verification for finite systems and preserving progress properties via next-free LTL equivalence. By proving that $O\sim_{\cal B}^{div}\Theta$ implies linearizability (and, when $\Theta$ is wait-free, that $O$ is wait-free as well), the authors offer a unified framework to verify both correctness and liveness. Through experiments on Treiber’s lock-free stacks (with and without hazard pointers) using CADP, they show DSBB is significantly more scalable than trace refinement, can automatically yield counterexamples, and even uncover a bug where a revised hazard-pointer scheme loses wait-freedom, illustrating the practical impact of the approach.

Abstract

The verification of linearizability -- a key correctness criterion for concurrent objects -- is based on trace refinement whose checking is PSPACE-complete. This paper suggests to use \emph{branching} bisimulation instead. Our approach is based on comparing an abstract specification in which object methods are executed atomically to a real object program. Exploiting divergence sensitivity, this also applies to progress properties such as lock-freedom. These results enable the use of \emph{polynomial-time} divergence-sensitive branching bisimulation checking techniques for verifying linearizability and progress. We conducted the experiment on concurrent lock-free stacks to validate the efficiency and effectiveness of our methods.

Figures (7)

• Figure 1: Abstract counter $(i)$ and concrete counter $(ii)$.
• Figure 2: Different progress properties of methods $\texttt{dec}()$.
• Figure 3: Divergence-sensitivity of bisimulation for object systems.
• Figure 4: Treiber's lock-free stack push/pop and the lock-free stack with hazard pointers push_HP/pop_HP, where the implementation of Retire_Node(o) can be found in Michael04.
• Figure 5: The linearizable specification of concurrent stacks.

Theorems & Definitions (12)

• Example 1
• Example 2
• Definition 2.1: Object systems
• Definition 3.1: Linearizability relation between histories
• Definition 3.2: Linearizability of object systems
• Theorem 3.3
• Definition 4.1
• Theorem 4.2
• Definition 5.1
• Definition 5.2