Decomposable relaxation for concurrent data structures

Abstract

We propose a relaxation scheme for defining specifications of relaxed data structures. It can produce a relaxed specification parameterized with a specification of a standard data structure, a transition cost function and a relaxation strategy represented by a finite automaton. We show that this relaxation scheme can cover the known specifications of typical relaxed queues and stacks. We then propose a method to reduce a relaxed specification defined under the relaxation scheme into a finite number of finite automata called witness automata. By applying this method we prove that the specifications of typical relaxed queues and stacks can be equivalently characterized by a finite number of witness automata. Thus, the problem whether a relaxed queue or stack is linearizable with respect to its relaxed specification can be efficiently checked through automata-theoretic approaches. Moreover, all these witness automata can be generated automatically. In this way, our relaxation scheme can well balance the expressiveness of relaxation strategies with the complexity of verification.