Model Checking a Lazy Concurrent List-Based Set Algorithm

Concurrent objects are notoriously difficult to design correctly, and high performance algorithms that make little or no use of locks even more so. In this paper, we present a formal verification of a lazy concurrent list-based set using model checking techniques. The algorithm supports insertion, removal, and membership testing of a list entry under optimistic locking scheme. The algorithm has nonfixed linearization points and is highly non-trivial. We have proved that the algorithm satisfies linearizability, by showing a trace refinement relation from the concrete implementation to its abstract specification. These models are specified in CSP# and verified automatically using our home grown model checker PAT.