Waitfree linearization was introduced by Herlihy in ACM TOPLAS in 1991. As I was not convinced of the correctness of the implementation Herlihy proposed, I developed a variation of his implementation together with a proof supported by the mechanical theorem prover NQTHM. The report about this work appeared in Distributed Computing in 1995. It described how I learned to use the prover, but it did not describe the logic of the proof. Moreover, my implementation assumed that the data object to be linearized was deterministic.
I am now (2024) redoing this work for an arbitrary (possibly nondeterministic) data object. A report is in preparation. It will describe the proofs in great detail. The proofs have been developed now with the proof assistant PVS. The PVS proof script is available. The assertion that the concurrent data object is linearizable, means that it has a simulation or refinement function towards the corresponding abstract atomic data object. This is incorporated in the new PVS proof script.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink