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.
展开▼
