Model Checking Unbounded Concurrent Lists

We present a model checking based method for verifying list-based concurrent data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification community. These data structures are unbounded in two dimensions: the list size is unbounded and an unbounded number of threads access them. Thus, their model checking requires abstraction to a model bounded in both the dimensions.

In previous work, we showed how the unbounded number of threads can be model checked by reduction to a finite model. In that work, we used the CMP (CoMPositional) method which abstracts the unbounded threads by keeping one thread as is (concrete) and abstracting all the other threads to a single environment thread. Next, this abstraction was iteratively refined by the user in order to prove correctness. However, in that work we assumed that the number of list elements was bounded by a fixed value. In practice this fixed value was small; model checking could only complete for small sized lists.

In this work, we overcome this limitation and model check the unbounded list as well. While it is possible to show correctness for unbounded threads by keeping one concrete thread and abstracting others, this is not directly possible in the list dimension as the nodes pointed to by the threads change during list traversal. Our method addresses this challenge by constructing an abstraction for which the concrete nodes can change with program execution and allowing for refinement of this abstraction to prove invariants. We show the soundness of our method and establish its utility by model checking challenging concurrent listbased data structure examples.