Conference Publication

Improving the Scalability of Automatic Linearizability Checking in SPIN
November 2016

Concurrency in data structures is crucial to the performance of multithreaded programs in shared-memory multiprocessor environments. However, greater concurrency also increases the difficulty of verifying correctness of the data structure. Model checking has been used for verifying concurrent data structures satisfy the correctness condition ‘linearizability’. In particular, ‘automatic’ tools achieve verification without requiring user-specified linearization points. This has several advantages, but is generally not scalable. We examine the automatic checking used by Vechev et al. in [VYY09] to understand the scalability issues of automatic checking in SPIN. We then describe a new, more scalable automatic technique based on these insights, and present the results of a proof-of-concept implementation.

Authors: Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan

Venue: NASA Formal Methods Symposium:


Hardware and Software, Engineered to Work Together