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

Abstract

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.