Verifying Linearizability via Optimized

Refinement Checking

Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang and Jin Song Dong

Overview
This page contains supplementary material for our paper:”Verifying Linearizability via Optimized Refinement Checking”.

This page is maintained by Shao Jie Zhang

.

Please contact with us if you have any question about this webpage or these experiments. We will reply your enquiries as soon as possible.

Abstract
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. Our method relies on refinement checking of finite state systems specified as concurrent processes with shared variables. In order to tackle state space explosion, a combination of state reduction techniques are applied, dynamic partial order reduction, symmetry reduction, etc. The approach is built into the PAT model checker. PAT has been used to automatically check a variety of implementations of concurrent objects, including the first algorithms for the mailbox problem and scalable NonZero indicators. Our system is able to find all known and injected bugs in these implementations.

Supplementary Material
The primary purpose of this page is to host the data used in our experiments, which consist of:

1. Experimental results

2. All model files in this experiment

Our linearizability checking method has been implemented in PAT model checker and applied to a number of concurrent algorithms, including register---the K-valued register algorithm in [1], stack---a concurrent stack algorithm [2], queue---a concurrent non-blocking queue algorithm [3], buggy queue---an incorrect queue algorithm [4], and SNZI---the first algorithm for scalable Non-Zero indicators [5], respectively. The following table summarizes part of our experiments, where `-' means out of memory.

Our data archive can be downloaded as a single zip file:

exps.zip

References

1. H. Attiya and J. Welch. Distributed Computing: Fundamentals, Simulations, and Advanced Topics. John Wiley & Sons, Inc., Publication,2nd edition, 2004.

2. R. K. Treiber. Systems Programming: Coping with Parallelism. Technical Report RJ 5118, IBM Almaden Research Center, 1986.

3. M. M. Michael and M. L. Scott. Nonblocking Algorithms and Preemption-Safe Locking on Multiprogrammed Shared Memory Multiprocessors. Journal of Parallel and Distributed Computing, 51:1–26, 1998.

4. C. H. Shann, T. L. Huang, and C. Chen. A Practical Nonblocking Queue Algorithm Using Compare-and-Swap. In Proceedings of the Seventh International Conference on Parallel and Distributed Systems (ICPADS’00), pages 470–475. IEEE, 2000.

5. F. Ellen, Y. Lev, V. Luchangco, and M. Moir. SNZI: Scalable NonZero Indicators. In Proceedings of the 26th Annual ACM Symposium on Principles of Distributed Computing (PODC’07), pages 13 – 22. ACM, 2007.