The following shows experimental results on embedded examples in CSP module to demonstrate the strength of PAT of handling various kinds of fairness constraints and verifying linearizability of concurrent data structure implementations.

LTL Checking under Various Kinds of Fairness Assumptions

This part shows verification statistics to show power of PAT to handle fairness in comparison to SPIN. The verified benchmark systems consist of dining philosopher problem, Milner’s cyclic scheduler algorithm and Peterson’s mutual exclusive algorithm.

Because of the deadlock state, the dining philosophers model (dp(N) for N philosophers and forks) does not guarantee that a philosopher always eventually eats ([]<> eat0) whether under no fairness or the strongest fairness. This experiment shows PAT takes little extra time for handling the fairness assumption. Notice that SPIN finds a counterexample (under no fairness) quickly. This is due to the particular order of exploration as well as its nested depth-first-search algorithm. Milner’s cyclic scheduler algorithm (ms(N) for N processes) is a showcase for the effectiveness of partial order reduction. We apply fairness in two different ways, i.e., one applying strong local fairness to the whole system (slf-whole) and the other applying only to inter-process communications (slf-action). In the latter case, partial order reduction allows us to prove the property over a much larger number of processes (e.g., 200 vs 12). Peterson’s mutual exclusive algorithm (peterson(N)) requires process-level weak fairness to guarantee bounded by-pass. The property is verified under weak fairness in PAT and process-level weak fairness in SPIN. PAT outperforms SPIN in this setting. The experiment data is available here.

Linearizability Checking

The experiment includes a number of
concurrent data structure algorithms, including a K-valued single-writer register, a
concurrent stack, mailbox problem and scalable non-zero indicator. The following table summarizes
part of our experiments, where ‘#Processes’ means the number of interleaving
processes, ‘#Operations’ means the number of operations a process performs, ‘N/A’ means out of memory or more than two hours, and ‘Unlimited’ means a process executes operations in a loop.

In the experiments, the number of states
and the running time increase rapidly with increasing data size or the number
of processes, e.g., 3 processes (in the Register or Stack) vs. 2
processes. Compared with the results in other method, our solution is
much more scalable to handle all the possible interleaving of operations. In
summary, PAT is effective and can handle millions of states in hours. The experiment data is available here.

However, the checking process still suffers from state space explosion problem.
We further address the challenge of state space reduction
of model checking linearizability by incorporating both symmetry
reduction and partial order reduction techniques. Our insight
emerged from our observation about characteristics of concurrent
object algorithms. First, concurrent objects are often designed
for a number of classes of similar threads. Such similarity or symmetry
often induces equivalent portions of the state space during
model checking process. Symmetry reduction targets at eliminating
such redundant equivalent states. Second, concurrent threads
are loosely coupled and different execution orders of transitions of
different threads may result in the same global state. Partial order
reduction is used to take advantage of this fact and restricts
model checking to explore only one of the equivalent execution
orders. Therefore, the features of concurrent data structures potentially
enable effective symmetry and partial order reductions, and
furthermore, we prove that these two techniques can be combined
for linearizability checking.

The new method has also been implemented in our model checker PAT
and applied to a number of real-world concurrent object algorithms,
including register-the K-valued multi-reader single-writer register, stack-a concurrent stack algorithm, buggy queue-an
incorrect queue algorithm, fixed queue-the modified correct
queue proposed, SNZI-recently-proposed complicated scalable
Non-Zero indicators espectively. For each algorithm, any
thread is constructed as a most general user to non-deterministically
execute one operation. The experiment data are presented in the following table
. In the table, ‘T’ is the total number of interleaving threads,
‘Res’ is the verification result, ‘Time’ is the running time in seconds
and ‘States’ is the number of stored states respectively for checking
with specific options (SR-symmetry reduction, POR-partial order
reduction). ‘Gain’ shows the percentage of reduced states and time
by applying two reduction techniques. ‘-’ denotes out of memory
or more than one hour.

From the table, it is shown that symmetry reduction and/or partial
order reduction reduce both memory and time consumption as
expected, and the combination of both techniques works best in
most cases. The computational overhead stems from two aspects.
One is dependency analysis between transitions of different threads
at each exploration step for partial order reduction; the other is
checking whether any equivalent state of a visiting state has been
explored for symmetry reduction. The experiment shows that our
approach can significantly save time and space for demonstrating
absence of errors and at the same time it does not sacrifice the capability
of detecting bugs.