A mechanized refinement proof of the Chase–Lev deque using a proof system

Abstract

We present a linearizability proof for the concurrent Chase–Lev work-stealing queue (WSQ) implementation on sequentially consistent memory. We used the CIVL proof system to carry out the proof. 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.