Half-time seminar: 'Efficient Linearizability Monitoring'

Abstract: We present efficient and novel algorithms for checking the linearizability of executions of concurrent data structure libraries such as stacks queues and sets. Linearizability is the standard correctness condition for such concurrent objects, and is routinely taught at the undergraduate level. Despite the simplicity of the concept, designing linearizability algorithms has shown to be notoriously difficult. In fact, it is so difficult that we have found that all previous works on polynomial-time algorithms either (i) are unsound, (ii) have unsound correctness proofs, or (iii) are missing correctness arguments altogether. Furthermore, the algorithms in (ii) or (iii) have cubic complexity.

We present a new family of algorithms with better time complexity, as well as provide proofs of their correctness. For stacks, we construct a linearization recursively by detecting patterns that correspond to intervals of time during which the stack is populated or may be empty, and obtain an algorithm that is quadratic in the length of the input. For queues, we have proven a small-model theorem, from which we can extract an algorithm that is O(n log n). For (multi)sets, we show that it is sufficient to count certain events at each step, and thus obtain an algorithm that is O(n).

We have implemented these algorithms in a tool, LiMo (LInearizability MOnitor). In this talk, I will present these algorithms, and relay the key ideas in their correctness proofs.

Reviewer: Tobias Wrigstad
Supervisors: Parosh Abdulla, Bengt Jonsson