Quasi-Linearizability is Undecidable

Quasi-linearizability is a quantitative relaxation of linearizability. It preserves the intuition of the standard notion of linearizability and permits more flexibility. The decidability of quasi-linearizability has been remaining open in general for a bounded number of processes. In this paper we show that the problem of whether a library is quasi-linearizable with respect to a regular sequential specification is undecidable for a bounded number of processes. This is proved by reduction from the k-Z decision problem of a k-counter machine, a known undecidable problem. The key idea of the proof is to establish a correspondence between the quasi-sequential specification of quasi-linearizability and the set of all unadmitted runs of the k-counter machines.