Formal Verification of Skiplists with Arbitrarily Many Levels

Abstract

We present an effective method for the formal verification of skiplists, including skiplists with arbitrary length and unbounded size. The core of the method is a novel theory of skiplists with a decidable satisfiability problem, which up to now has been an open problem. A skiplist is an imperative software data structure used to implement a set by maintaining several ordered singly-linked lists in memory. Skiplists are widely used in practice because they are simpler to implement than balanced trees and offer a comparable performance. To accomplish this efficiency most implementations dynamically increment the number of levels as more elements are inserted. Skiplists are difficult to reason about automatically because of the sharing between the different layers. Furthermore, dynamic height poses the extra challenge of dealing with arbitrarily many levels. Our theory allows to express the memory layout of a skiplist of arbitrary height, and has an efficient decision procedure. Using an implementation of our decision procedure, we formally verify shape preservation and a functional specification of two source code implementations of the skiplist datatype. We also illustrate how our decision procedure can also improve the efficiency of the verification of skiplists with bounded levels. We show empirically that a decision procedure for bounded levels does not scale beyond 3 levels, while our decision procedure terminates quickly for any number of levels.