A concurrent data object

The design of a linearization of a concurrent data object

The proof is made with the theorem prover NQTHM-1992 of Boyer and Moore, which can be obtained from nqthm-request@cli.com, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas 78703, USA.

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

The event files that can be read and submitted for NQTHM-1992 to yield a formal proof, at least of safety, are

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