Model-Checking of Correctness Conditions for Concurrent Objects

The notions of serializability, linearizability and sequential consistency are used in the specification of concurrent systems. We show that the model checking problem for each of these properties can be cast in terms of the containment of one regular language in another regular language shuffled using a semi-commutative alphabet. The three model checking problems are shown to be, respectively, in Pspace, in Expspace, and undecidable. 1 Introduction A common way of specifying concurrent systems is to describe the desired sequential behavior of the system, and then to allow the implementation to execute certain operations in parallel, provided the appearance of sequential behavior is maintained for a suitable observer. The earliest such notion of correctness was serializability (see, for instance, [EGLT76, Pap86, BHG87]), which requires that a collection of transactions that are scheduled in parallel must produce the same result as the same transactions scheduled in some sequential ord..