CIVL Verification of The Art of Multiprocessor Programming

This repository contains implementations of data structures from The Art of Multiprocessor Programming in CIVL-C for model checking with CIVL.

Installation directions:

A recent installation of the CIVL model checker is required. Installation directions can be found here: http://vsl.cis.udel.edu:8080/civl/index.html.

To tell AMPVer where to find your CIVL installation, make a copy of config/config_default.mk called config/config.mk and set the CIVL_ROOT and VSL_DEPS arguments appropriately.

Once your CIVL installation is set up and you've configured AMPVer to point to that installation, you can verify any of the implemented data structures using our Makefile rules, which use various preset bounds as described in the paper. The Makefile includes rules to run all the experiments in the paper.

The core experiments are divided into four categories: (hash) sets, lists, queues, and priority queues. Each category has multiple sets of limits, which are the parameters for the experiments passed to the AMPVer tool. The limits are defined in the variables HASHSET_LIMITS_n, LIST_LIMITS_n, QUEUE_LIMITS_n, and PQUEUE_LIMITS_n, where n is the number of the limit set. For example, HASHSET_LIMITS_1 is the limit set for the first and smallest core set experiment. To run all of the core experiments for a particular category and size, make the corresponding target.

Below is a list of the targets for each category:

• Sets: hashset_1, hashset_2, hashset_3, hashset_4
• Lists: list_1, list_2, list_3, list_4
• Queues: queue_1, queue_2, queue_3
• Priority Queues: pqueue_1, pqueue_2, pqueue_3, pqueue_4

For an example, to verify all lists using the second set of limits, one would run:

make list_2

The output of each experiment is stored in the out/ directory. The summary output for each data structure is stored in a file named out/DS_n.out, where DS is the name of the data structure and n is the limit set. The outputs for each schedule are stored in separate files in under a directory named out/DS_n.dir, following the same naming convention. For example, the output for the CoarseHashSet data structure using the first set of limits is stored in out/CoarseHashSet_1.out, and the output for the first schedule is stored in out/CoarseHashSet_1.dir/schedule_1.out, along with the CIVL schedule configuration file as schedule_1.cvl. To run just one data structure and limit set combination, one can run the corresponding target. For example, to run just the CoarseHashSet data structure using the first set of limits, one would run:

make out/CoarseHashSet_1.out

Some data structures have additional variants that can also be verified. The variant names are appended to the data structure name. The available variants are listed and described below. These variants are included in the core experiment targets described above.

LockFreeList: LockFreeListOriginal

• Original: uses the original version of the LockFreeList data structure as presented in the 1st edition of the book, which contains a bug in the remove method corrected in later editions and the errata.

FineGrainedHeap: FineGrainedHeapFair, FineGrainedHeapNoCycles

• Fair: uses a fair ReentrantLock instead of the original ReentrantLock. Also passes the -fair flag to AMPVer, which indicates thread scheduling must be fair.
• NoCycles: removes the -checkTermination flag from AMPVer, which means AMPVer will not check for cycle violations.

SkipQueue: SkipQueuePatched

• Patched: uses a patched version of the SkipQueue data structure that fixes the cycle bug in FindAndMarkMin as described in the paper.

In addition to the core experiments above, the Makefile also includes targets for running particular individual schedules of interest. These targets are described below. Currently, the only schedules of interest are for priority queues.

• PQUEUE_SCHED_1: a schedule that reveals the non-linearizable behavior in SkipQueuePatched.
• PQUEUE_SCHED_2: a schedule that reveals the cycle violation in SkipQueue.
• PQUEUE_SCHED_3: same as PQUEUE_SCHED_2, but one fewer pre-add and one fewer thread.
• PQUEUE_SCHED_4: a schedule of similar size to the above that reveals no defect in SkipQueue or SkipQueuePatched.

Individual schedules can be run using a target of the form out/DS_Sn, where DS is the name of the data structure, including any variants, and n is the number of the schedule. Note the use of the letter S before the schedule number to indicate that it is a schedule rule. The output of the schedule is stored in out/DS_Sn. For example, to run the first schedule for SkipQueuePatched, one would run:

make out/SkipQueuePatched_S1

All schedules for all priority queues can be run using the target pqueue_schedules:

make pqueue_schedules

Concurrent data structures implemented:

All page numbers taken from the 2nd Edition.

Lists (Ch. 9)

CoarseList:

• src/list/CoarseList.cvl
• A linked list which uses a single lock to control access to the entire list.
• AMP Chapter 9.4, page 206

FineList:

• src/list/FineList.cvl
• A linked list which uses one lock for each node of the list.
• AMP Chapter 9.5, page 207

OptimisticList:

• src/list/OptimisticList.cvl
• A linked list which allows searching the list without locking, locks when the nodes are found, and then checks that the locked nodes are correct. If a synchronization conflict causes the wrong node to be locked, the locks are released and the process restarts.
• AMP Chapter 9.6, page 211

LazyList:

• src/list/LazyList.cvl
• A linked list, similar to the optimistic list, which implements a non-blocking contains and a two-step lazy remove method which uses a boolean mark field on each node.
• AMP Chapter 9.7, page 215

LockFreeList:

• src/list/LockFreeList.cvl
• A linked list which uses atomic markable references with compare-and-set for a non-blocking synchronization strategy.
• AMP Chapter 9.8, page 220

Queues (Ch. 10)

BoundedQueue:

• src/queue/BoundedQueue.cvl
• A queue implementation with two locks and two condition variables to synchronize, with bounded partial behavior, meaning threads attempting to remove from an empty queue or add to a full queue will block until the queue status changes.
• AMP Chapter 10.3, page 230

UnboundedQueue:

• src/queue/UnboundedQueue.cvl
• A queue implementation with a simple two-lock synchronization approach.
• AMP Chapter 10.4, page 235

LockFreeQueue:

• src/queue/LockFreeQueue.cvl
• A queue implementation which uses atomic compare and swap operations to maintain correctness, with a lazy/two-step add/remove process.
• AMP Chapter 10.5, page 236

Sets (Ch. 13)

CoarseHashSet:

• src/hashset/CoarseHashSet.cvl
• A closed-address hash set which uses a single lock to control access.
• AMP Chapter 13.2.1, page 308

StripedHashSet:

• src/hashset/StripedHashSet.cvl
• A closed-address hash set which uses a fixed number of locks which each control access to a disjoint subet of the set's buckets.
• AMP Chapter 13.2.2, page 310

StripedCuckooHashSet:

• src/hashset/StripedCuckooHashSet.cvl
• An open-address hash set which combines the approaches of the cuckoo hash set and the striped hash set.
• AMP Chapter 13.4.3, page 329

Priority Queues (Ch. 15)

FineGrainedHeap:

• src/pqueue/FineGrainedHeap.cvl
• A priority queue implementation which uses a fine-grained locking approach for synchronization of the underlying heap structure.
• AMP Chapter 15.4, page 363

SkipQueue:

• src/pqueue/SkipQueue.cvl
• A lock-free priority queue using atomic markable references and a skiplist structure.
• AMP Chapter 15.5, page 371

Barriers (Ch. 18)

Note that barrier verification is performed using a separate driver and Makefile found under src/barrier.

Sense-reversing Barrier

• src/barrier/sense_barrier/sense_barrier.cvl
• A simple barrier with one global sense and thread-local Boolean senses
• AMP Chapter 18.3, page 433

Combining Tree Barrier

• src/barrier/combining_tree_barrier/combining_tree_barrier.cvl
• A tree barrier in which each node is a barrier between two threads, and all threads are assigned in pairs to leaf nodes. Similar to a tournament barrier.
• AMP Chapter 18.4, page 434

Static Tree Barrier

• src/barrier/static_tree_barrier/static_tree_barrier.cvl
• A tree barrier in which each thread is a assigned a node, and each node waits for its children to complete.
• AMP Chapter 18.5, page 436

Reverse Tree Barrier

• src/barrier/reverse_tree_barrier/reverse_tree_barrier.cvl
• A tree barrier similar to the combining tree barrier except that barrier completion starts at the root rather than at the leaves, and notifications come back to the root from the leaves. Presented as an exercise for the reader to check correctness.
• AMP Chapter 18.8, Exercise 18.7, page 447

TODO:

• SimpleBarrier
• Termination Detection Barrier?