Computer Science Department
School of Computer Science, Carnegie Mellon University
GLINDA: Natural Language Text Generation in the Oz Interactive Fiction Project
This paper presents a library of concurrent objects of different data types: FIFO queues, priority queues, semiqueues, stuttering queues, sets, multiple sets, and registers. For each different kind of concurrent object, we provide a (sequential) specification written in Larch, an implementation in C, and a proof of correctness. We use linearizability as our basic correctness condition.