# Relaxed Data Types as Consistency Conditions +
## 5 Consistency Condition to Relaxation
#### k-Atomicity  
[PERSON] et al. defined \(k\)-Atomicity [25]. However, their definition only discusses registers and has, to our knowledge, not been generalized to other types. Since we are interested in arbitrary ADTs, we would like a more general definition. To do this, we generalize _Reads_ to all pure accessors and _Writes_ to all pure mutators. It is not well-defined how mixed operations should behave under \(k\)-Atomicity. They should be allowed to return a value as if they were out of order, but then the mutations they cause could seemingly cause previous operation instances to be illegal. Given these issues, we will limit our definition of \(k\)-Atomicity to data types which have only pure operations. **Definition 13** (\(k\)-Atomicity). : _A schedule \(E\) on a data type \(T\) with only pure operations is \(k\)-atomic, for \(k\geq 0\), if there exists a permutation \(\Pi\) of all operation instances in \(E\), respecting the schedule order of non-overlapping instances, such that, for every accessor instance \(op\), with \(\Pi=\pi.op.\rho\), there exists a sequence \(\pi^{\prime}\) obtained by removing up to \(k\) consecutive instances from the end of \(\pi|_{m}\) such that \(\pi^{\prime}.op\) is legal in \(T\)._  
We can now split this condition into two pieces. The first is the core of Linearizability, that there is an ordering of all operation instances in the schedule that respects the schedule order. The second condition expands the set of legal sequences beyond the set of legal sequences specified by \(T\). The consistency condition requires that the sequence of all instances from the first part is in the set defined by the second part. By moving the second part into the data type, relaxing the data type specification, we are left with Linearizability for the consistency condition, and have the desired equivalence. **Definition 14** (\(k\)-Atomic-Equiv Relaxed ADT). : _Given any ADT \(T\) with no mixed operations and \(k\geq 0\), a \(k\)-Atomic-Equiv relaxation of \(T\) is defined as follows:_  
1. \(OPS(T^{\prime})=OPS(T)\)_._
2. \(\mathcal{L}_{\mathcal{T^{\prime}}}\) _is the set of sequences_ \(\Pi\)_, where for each accessor instance_ \(op\)_, with_ \(\Pi=\pi.op.\rho\)_, there exists a sequence_ \(\pi^{\prime}\) _such that_ \(\pi^{\prime}.op\) _is legal in_ \(T\)_, where_ \(\pi^{\prime}\) _is obtained by removing up to_ \(k\) _consecutive instances from the end of_ \(\pi|_{m}\)_._  
**Theorem 4**. : _For \(k\geq 0\), the set of schedules legal on a \(k\)-Atomic-Equiv relaxation of any ADT \(T\) with no mixed operations under Linearizability is the same as the set of schedules legal on \(T\) under \(k\)-Atomicity._Theorem 4 holds by construction. Definition 14 is very similar to that of \(k\)-Out-of-Order, but they are not equivalent. Because it uses minimal equivalent sequences, a \(k\)-Out-of-Order relaxed data type cannot return a value which has been \"deleted\" from the data structure. For example, consider the following sequence:  
\[Enqueue(1).Enqueue(2).Enqueue(3).Dequeue(1).Dequeue(x)\]  
In a 2-Out-of-Order queue, \(x\) could be either 2 or 3. On the other hand, a \(k\)-Atomic type can return historical values that have been deleted or overwritten, so if the sequence in the previous example were executed on a 2-Atomic-Equiv queue, \(x\) could also be 1. It is interesting to note that \(k\)-Regularity and \(k\)-Safety, other conditions from [25] very similar to \(k\)-Atomicity which we define below, cannot be directly converted into relaxed data types. This is because they allow operation instances to have different behaviors when they overlap with one or more mutators than when they do not overlap with any mutators. A sequential specification has no notion of concurrency, or overlapping operation instances, so cannot differentiate these two possibilities. Recent work (e.g., [24; 26; 27]) has begun exploring the concept of tasks or objects which do not have sequential specifications.