COLLECT is a tool for verifying concurrent collections.
A concurrent collection implements a standard collection interface, such as set, queue, stack, or priority queue, and can be safely accessed by multiple threads simultaneously.
COLLECT uses model checking techniques to verify a concurrent collection implementation within a small scope. It is built on top of the CIVL Model Checker. Given a concurrent collection implemented in the CIVL-C language, along with small bounds on the number of threads, number of method calls, and other parameters, COLLECT explores the reachable states of the program. It is able to check standard consistency properties within these bounds, such as sequential consistency, linearizability, or quiescent consistency.
This web site also presents the results of an on-going case study applying COLLECT to the data structures from the widely-used text, The Art of Multiprocessor Programming, by Maurice Herlihy, Nir Shavit, Victor Luchangco, and Michael Spear. At this point, we have analyzed all 20 structures in the chapters on Lists, Queues, Hash Sets, and Priority Queues (chapters 9, 10, 13, and 15). We have verified many of these structures within various small scopes, and found several subtle and previously unknown defects in others.
This website has been anonymized for review purposes.