I am a...
I want to...
Sign In/Register for Account
External Research Office
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.
Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan
Oracle Labs on OTN
Want to try out some of the cool technology being built at Oracle Labs?
Email to a friend
Integrated Cloud Applications and Platform Services
Oracle RSS Feed