Output details

A simple abstraction for complex concurrent indexes

<10>This paper demonstrated the usefulness of modular reasoning based on concurrent abstract predicates, by applying CAP to several realistic index algorithms. In comparison to Krishnaswami, this paper radically simplifies and generalises the interface presented to clients. Furthermore, this paper verifies a real-world index implementation, the widely-used B-Link tree. As a demonstration of the significance of this approach, it uncovered an apparently-unknown bug in this algorithm. This paper also introduced the idea of using separation-logic style reasoning to express epistemic uncertainty, an idea later developed in Fictional Separation Logic by Jensen et al and Subjective Auxiliary State by Ley-Wild et al.