Waitfree Linearization of an Arbitrary Data Object
Waitfree linearization of data objects was introduced by Herlihy in 1991. The present article proposes an algorithm for waitfree linearization of a possibly nondeterministic data object in bounded memory, together with a complete proof of correctness supported by the proof assistant PVS. The project is exceptional in that the proofs of 70 invariants are recorded systematically, and that waitfree progress is quantified in waitfree complexity and is formally proved.
Authors
- Wim H. Hesselink (ORCID: https://orcid.org/0000-0002-1413-4320)
Institutions
- University of Groningen (NL)
Publication Details
- Journal
- Formal Aspects of Computing
- Published
- 2025-04-03
- DOI
- https://doi.org/10.1145/3725535
- Primary Topic
- Distributed systems and fault tolerance
- Type
- article
- Field-Weighted Citation Impact
- 0.00