This is work done together with Jan Friso Groote of the CWI, from March to June 1998. It culminated in the paper W.H. Hesselink, J.F. Groote: Waitfree concurrent memory management by Create, and Read until Deletion (CaRuD). Dist. Comput. 14 (2001) 31-39.
The events files for the Nqthm proof of this
distributed algorithm are as follows.
The file
crud0.events contains the modelling, the program, and
the semantic lemmas.
The file
crud1.events contains the constituent invariants.
The file
crud2.events contains the construction of the global
invariant, its proof of invariance, and the proof of its
satisfiability, i.e. the initialization.
See the sibling directories for the methods used to handle
sequential and distributed algorithms with Nqthm.