## Waitfree linearization of an arbitrary data object

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

Last modified: Wed Jun 26 11:13:57 CEST 2024