A Decidable Theory of Skiplists of Unbounded Size and Arbitrary Height

TL;DR

This paper introduces a formal theory and decision procedure for reasoning about skiplists of arbitrary height, enabling formal verification of their correctness and properties.

Contribution

It presents the first decidable theory for skiplists of unbounded size and height, facilitating formal reasoning and verification.

Findings

Decidability of satisfiability for quantifier-free formulas in the theory.

Formal verification of a practical skiplist implementation.

A decision procedure for reasoning about dynamic, multi-level skiplists.

Abstract

This paper presents a theory of skiplists of arbitrary height, and shows decidability of the satisfiability problem for quantifier-free formulas. A skiplist is an imperative software data structure that implements sets by maintaining several levels of ordered singly-linked lists in memory, where each level is a sublist of its lower levels. Skiplists are widely used in practice because they offer a performance comparable to balanced binary trees, and can be implemented more efficiently. To achieve this performance, most implementations dynamically increment the height (the number of levels). Skiplists are difficult to reason about because of the dynamic size (number of nodes) and the sharing between the different layers. Furthermore, reasoning about dynamic height adds the challenge of dealing with arbitrary many levels. The first contribution of this paper is the theory TSL that allows to express the heap memory layout of a skiplist of arbitrary height. The second contribution is a decision procedure for the satisfiability prob- lem of quantifier-free TSL formulas. The last contribution is to illustrate the formal verification of a practical skiplist implementation using this decision procedure.