## Waitfree linearization of an arbirary 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.

Comments and questions are welcome.

Back to my home page.

Wim H. Hesselink

Last modified: Tue Apr 16 20:52:07 CEST 2024