The algorithm, its design, and the construction of its proof are described in

- The design of a linearization of a concurrent data object. In: D. Gries, W.-P. de Roever (eds.): Programming Concepts and Methods, Proceedings PROCOMET '98, Chapman & Hall, IFIP 1998, pp. 205--224.
- Progress under bounded fairness. In preparation (24 pages), September 1998
- Progress for memory management of a concurrent data object, 11 pages, September 1998

- linproc0m.events contains the algorithm and the semantic lemmas
- linproc1m.events contains the invariants
- linproc2m.events contains the construction of the initial state that satisfies the invariants
- linproc3m.events contains some results used for the proof of progress

Comments are welcome, September 29, 1998