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.