# Relaxed Data Types as Consistency Conditions +
## 6 Placing New Consistency Conditions
An overwriter \(OP\) is an operation such that every sequence \(\pi.op\), \(op\in OP\), is equivalent to the singleton sequence \(op\)[5; 30]. This means that the set of next operation instances which result in a legal sequence is determined entirely by the last previous mutator. In addition to a \(Read/Write\) register, this class includes other data types whose mutators are all overwriters, but which have accessors that return only parts of the state. StutteringCC(\(k\)) and \(k\)-Atomicity both allow us to ignore some recent mutator instances. The difference, which makes the two consistency conditions distinct, is that a stuttering instance must be ignored by all subsequent operation instances, while in \(k\)-Atomicity, instances may be ignored by some subsequent instances, but seen by others. If all mutators in a data type \(T\), which has no mixed operations, are overwriters, then for all \(k\geq 1\), StutteringCC(\(k\)) on \(T\) is stronger than \((k-1)\)-Atomicity on \(T\). Proof. : We show that any schedule which is legal under StutteringCC(\(k\)) is also legal under \((k-1)\)-Atomicity. Consider an arbitrary schedule \(E\). Let \(\Pi\) be an ordering of all instances in \(E\), which respects the schedule partial order of non-overlapping instances, as specified by the definition of StutteringCC(\(k\)). Let \(\Pi=op_{1}.op_{2}.\)... For each \(\pi^{\prime}_{i}\) specified by the definition of StutteringCC(\(k\)), let \(m_{i}\) be the last mutator instance in \(\pi^{\prime}_{i}\). Because all mutators are overwriters, \(\pi^{\prime}_{i}\equiv m_{i}\). For each \(op_{i}\in\Pi\), there cannot be more than \((k-1)\) mutator instances in \(\Pi\) strictly between \(m_{i}\) and \(op_{i}\), by the definition of \(\pi^{\prime}_{i}\) and \(m_{i}\). Thus, by deleting up to \((k-1)\) of the last previous mutator instances before \(op_{i}\) in \(\pi\), \(m_{i}\) will be the last mutator instance, and because it is a mutator, \(op_{1}...m_{i}\equiv m_{i}\equiv\pi^{\prime}_{i}\), so \(op_{1}...op_{i}\) is legal under \(k\)-Atomicity. Thus, \(\Pi\) is legal under \(k\)-Atomicity. Finally, we show that the three new consistency conditions corresponding to data type relaxations we introduced in this paper are incomparable to one another. We no longer restrict the set of data types considered, since these relaxations are defined for all data types. **Theorem 8**. : _Considered on all data types and for all \(k\geq 1\) and \(l,m\geq 2\), OutofOrderCC\((k)\), LatenessCC\((l)\), and StutteringCC\((m)\) are all incomparable to one another._  
Proof. :
1. First, we compare OutofOrderCC\((k)\) and LatenessCC\((l)\), showing that neither condition contains the other. * On a FIFO queue, the sequential schedule \[Enqueue(1)...Enqueue(l+2).Dequeue(2)...Dequeue(l+2)\] is legal under OutofOrderCC\((k)\), because \(Enqueue(1)...Enqueue(l+2)\) is legal in the base type, and for each instance \(Dequeue(x)\), we can obtain a \(\pi^{\prime}\) such that \(\pi^{\prime}.Dequeue(x)\) is legal by deleting \(Enqueue(1)\) from the minimal-length equivalent sequence to the preceding sequence, which consists of all \(Enqueue\) instances whose argument has not yet been returned. The schedule is not legal under LatenessCC\((l)\) because there are \(l\) consecutive \(Dequeue(x)\) instances, for none of which is \(\pi^{\prime}.Dequeue(x)\) legal in a FIFO queue, when \(\pi^{\prime}\) is a minimal-length equivalent sequence to the prior history, since all minimum-length sequences equivalent to a prefix of this schedule start with \(Enqueue(1)\). * On a FIFO queue, the sequential schedule \[Enqueue(1)...Enqueue(k+2).Dequeue(k+2)\] is legal under LatenessCC\((l)\), but not under OutofOrderCC\((k)\). In the base type, the prefix \(Enqueue(1)...Enqueue(k+2)\) is legal and of minimum length among equivalent sequences. By deleting a finite number, \(k+1\), of consecutive mutators from the preceding sequence, we have \(Enqueue(k+2).Dequeue(k+2)\) which is legal in the base type.