Improving the Scalability of Automatic Linearizability Checking in SPINNovember 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: https://ti.arc.nasa.gov/events/nfm-2017/