A Mechanized Proof of the Chase-Lev Deque Using a Proof System
Published in International Conference on Networked Systems (NETYS), 2016
Recommended citation: Suha Mutluergil and Serdar Tasiran. " A Mechanized Proof of the Chase-Lev Deque Using a Proof System." Proceedings of 4th International Conference on Networked Systems (NETYS), 2016.
This paper is about verification of a non-trivial concurrent double ended queue using the Boogie assistant.
Abstract. We present a linearizability proof for the Chase-Lev work-stealing queue (WSQ) on sequentially consistent (SC) memory. We used the CIVL proof system for verifying refinement of concurrent programs. The lowest-level description of the WSQ is the data structure code described in terms of fine-grained actions whose atomicity is guaranteed by hardware. Higher level descriptions consist of increasingly coarser action blocks obtained using a combination of Owicki-Gries (OG) annotations and reduction and abstraction. We believe that the OG annotations (location invariants) we provided to carry out the refinement proofs at each level provide insight into the correctness of the algorithm. The top-level description for the WSQ consists of a single atomic action for each data structure operation, where the specification of the action is tight enough to show that the WSQ data structure is linearizable.