任意高度无限长Skiplists的判定理论
A Decidable Theory of Skiplists of Unbounded Size and Arbitrary Height
摘要：
本文给出了任意高度跳跃者的理论，并证明了无量词公式的可满足性问题的可判定性。跳跃列表是一种命令式软件数据结构，它通过在内存中维护几个级别的有序单链表来实现集合，其中每个级别是其较低级别的子列表。Skiplist在实践中被广泛使用，因为它们提供了与平衡二叉树相当的性能，并且可以更有效地实现。为了实现此性能，大多数实现都会动态增加高度（级别数）。由于动态大小（节点数量）和不同层之间的共享，很难对Skiplist进行推理。此外，关于动态高度的推理增加了处理任意多个水平的挑战。本文的第一个贡献是理论TSL，允许表示堆内存布局的跳跃列表的任意高度。第二个贡献是无量词TSL公式的可满足性问题的判定过程。最后的贡献是说明了形式化验证的实际skiplist实现使用此决策过程。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
