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.
@inproceedings{vechev2009experience, title={Experience with model checking linearizability}, author={Vechev, Martin and Yahav, Eran and Yorsh, Greta}, booktitle={International SPIN Workshop on Model Checking of Software}, pages={261--278}, year={2009}, organization={Springer}}