Experience with Model Checking Linearizability

Martin Vechev, Eran Yahav, Greta Yorsh

In Proc. SPIN Workshop on Model Checking of Software (SPIN 2009)

Non-blocking concurrent algorithms offer significant performance advantages, but are very difficult to construct and verify. In this paper, we describe our experience in using SPIN to check linearizability of non-blocking concurrent data-structure algorithms that manipulate dynamically allocated memory. In particular, this is the first work that describes a method for checking linearizability with non-fixed linearization points.