A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes

Alejandro Sánchez and César Sánchez
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.
Download: BIB PDF