Automated Verification of Linearizability for a B-Bounded Queue

This repository contains the implementation of the final project in the course "Automatic Verification of Systems" in TAU. The projects aims to use CBMC in order to verify the linearizability of a B-Bounded queue.

Method

In order to verify the linearizability of the algorithem we check that is it linearizable for N threads where each thread performs exactly one action. The verification is done by dispatching N threads via CBMC and recording their start and end time (using a global clock) their actions and their results. We then try every possible permutation of execution order of the different N actions in a single thread and make sure that at least one will result in the resulting trace we got.

Execution

You must first install cryptominisat5. Inside the code directory there is a verify.sh bash file, it can be executed using the following command line:

./verify.sh <N_THREADS> <B>

The code will then generate all possible permutation and execute CBMC with the given amount of threads and will set the queue size according to B.

Interesting results.

We have gathered three interesting traces in the cleverly named interesting_traces folder:

1. verify_4_1.txt - A counter example for linearizability with 4 threads and a queue of size 1
2. verify_4_2.txt - A counter example for linearizability with 4 threads and a queue of size 2
3. verify_5_2.txt - A counter example for linearizability with 5 threads and a queue of size 2

Reading the traces

The traces are quite long and complex, in order to read them one has got to look at the op_start and op_end of each thread in the trace and then look at the in_v, in_op (the type of operation) and out_r.

Example Parsed Trace - 4 threads with a bounded size of 2

Running threads	Memory status	Running Thread	Executed actions	Result
${T_1}$	Q = [] Count = 0	$T_1$	$T_1$: enqueue(1) n = Count FAA(Count, 1)
${T_1, T_2}$	Q = [] Count = 1	$T_2$	$T_2$: dequeue() n = Count FAA(Count, -1) r = Queue.dequeue() (returns $\bot$)
${T_1, T_2}$	Q = [] Count = 0	$T_1$	r = Queue.enqueue(1) return r	OK
${T_2, T_3}$	Q = [1] Count = 0	$T_3$	$T_3$: dequeue() n = Count (reads 0) return $\bot$	$\bot$
${T_2, T_4}$	Q = [1] Count = 0	$T_2$	n = FAA(Count, 1) + 1
${T_2, T_4}$	Q = [1] Count = 1	$T_4$	$T_4$: dequeue() n = Count FAA(Count, -1) r = Queue.dequeue() return r	1
${T_2}$	Q = [] Count = 0	$T_2$	Go through dequeue loop and exit failing return r	$\bot$