A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
This paper presents a theory of skiplists with a decidable
satisfiability problem, and shows its applications to the
verification of concurrent skiplist implementations. A skiplist is
a data structure used to implement sets by maintaining several
ordered singly-linked lists in memory, with a performance comparable
to balanced binary trees. We define a theory capable of expressing
the memory layout of a skiplist and show a decision procedure for
the satisfiability problem of this theory. We illustrate the
application of our decision procedure to the temporal verification
of an implementation of concurrent lock-coupling skiplists.
Concurrent lock-coupling skiplists are a particular version of
skiplists where every node contains a lock at each possible level,
reducing granularity of mutual exclusion sections.
The first contribution of this paper is the theory \TSLK. \TSLK is
a decidable theory capable of reasoning about list reachability,
locks, ordered lists, and sublists of ordered lists. The second
contribution is a proof that \TSLK enjoys a finite model property
and thus it is decidable. Finally, we show how to reduce the
satisfiability problem of quantifier-free \TSLK formulas to a
combination of theories for which a many-sorted version of
Nelson-Oppen can be applied.
In Proceedings of the Third International Symposium on NASA Formal Methods (NFM'11), Pasadena, CA, USA, April 18-20, 2011. vol 6617 of Lecture Notes in Computer Science, pp343--358, Springer 2011.