Branching Bisimulation and Concurrent Object Verification
Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, Hao Wu · 2018
Linearizability and progress properties are key correctness notions for concurrent objects. This paper presents novel verification techniques for both property classes. The key of our techniques is based on the branching bisimulation equivalence. We first show that it suffices to check linearizability on the quotient object program under branching bisimulation. This is appealing, as it does not rely on linearization points. Further, by exploiting divergence-sensitive branching bisimilarity, our approach proves progress properties (e.g., lock-, wait-freedom) by comparing the concurrent to-be-verified object program against an abstract program consisting of atomic blocks. Our work thus enables the usage of well-known proof techniques for branching bisimulation to check the correctness of concurrent objects. The potential of our approach is illustrated by verifying linearizability and lock-freedom of 14 benchmark algorithms from the literature. Our experiments confirm one known bug and reveals one new bug.