Proofs of Linearizability for the Elimination Queue

This Web page gives mechanized proofs that show linearizability for the Elimination queue algorithms as described in [MoirNussbaumShalevShavit2005]. The proof strategy used here is the complete backward simulation technique described in [TOCL2014] that was used earlier to verify Herlihy & Wing's Queue from [HW]. A description of the specifications that form the general theory for verifying linearizability by proving a backward simulation based are described here. This page only describes the instance of the theory for the concrete algorithms of the Elimination queue.

The following sections are structured as follows:

Overview over the important specifications

Before going into details, we first give a rough description of the important specifications that are accessible via the overview over the specification structure:

Encoding the algorithms as operations of a data type

The main invariants of the algorithm

The main invariant of the algorithm is HINV(gs,lsf,H) as defined in specification CINV. It consists of several parts:

The backward simulation

Proving the invariants and the backward simulation


Bibliography

[TOCL2014] A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structure
John Derrick, Gerhard Schellhorn and Heike Wehrheim ACM Trans. Comput. Logic, 2014, vol. 15, no. 4.
[MoirNussbaumShalevShavit2005] Using elimination to implement scalable and lock-free FIFO queues
M. Moir and D. Nussbaum and O. Shalev and N. Shavit SPAA 2005, ACM press, p. 253--262

[Imprint] [Data Privacy Statement] [E-Mail]