CCSpec: A Correctness Condition Specification Tool

Concurrent libraries provide data structures whose operations appear to execute atomically when invoked individually. Although these libraries guarantee safety for the data structure operations, the composition of operations may be vulnerable to undefined behavior. The difficulty of reasoning about safety properties in a concurrent environment has led to the development of tools to verify that a concurrent data structure meets a correctness condition. The disadvantage of these tools is that they cannot verify that the composition of concurrent data structure operations respects the intended semantics of the algorithm. Formal logic has been proposed to enable the verification of correctness specifications for a concurrent algorithm. However, a large amount of manual labor is required to fully mechanize the correctness proofs of the concurrent algorithm and each concurrent data structure invoked in the algorithm. In this research, we propose Correctness Condition Specification (CCSpec), the first tool that automatically checks the correctness of a composition of concurrent multi-container operations performed in a non-atomic manner. In addition to checking the correctness of a composition of data structure operations in a concurrent algorithm, CCSpec also checks the correctness of each concurrent data structure utilized in the algorithm. A reference to a container is associated with each method called in a concurrent history to enable the evaluation of correctness for a composition of multiple containers. We develop a lightweight custom specification language that allows the user to define a correctness condition associated with the concurrent algorithm and a correctness condition associated with the concurrent data structures. We demonstrate the practical application of CCSpec by checking the correctness of a concurrent depth-first search utilizing a non-blocking stack, a concurrent breadth-first search utilizing a non-blocking queue, a concurrent shortest path algorithm utilizing a non-blocking priority queue, and a concurrent adjacency list utilizing non-blocking sets.