# Relaxed Data Types as Consistency Conditions +
## 2 Model  
### Data Types  
An _Abstract Data Type_ specifies an interface for interacting with data, and defines how a data object instantiating that type will behave. Data type specifications consist of the possible operations which a process may invoke and a set of sequences of operation invocation-response pairs, called _instances_, which specify all possible return values an operation response may have, given a sequence of past operations and an invocation. We here consider only objects with sequential specifications, as relaxation of tasks without sequential specifications (see, e.g., [23; 24]) has not been defined. Definition 1: An _Abstract Data Type consists of_  
1. _A set_ \(OPS\) _of operations and the sets_ \(args(OP)\) _of valid arguments and_ \(rets(OP)\) _of valid return values for each_ \(OP\in OPS\)_. An_ instance _of an operation_ \(OP\)_, denoted_ \(OP(arg,ret)\)_, contains the argument(s)_ \(arg\) _and the value(s) returned, ret. In a sequential environment, instances are indivisible, but we will consider them as a distinct invocation and matching response in the distributed setting._ _When either_ \(args(OP)\) _or_ \(rets(OP)\) _contains only a null value (_\(\bot\)_), we condense the notation to_ \(OP(arg)\) _or_ \(OP(ret)\)_, as appropriate._
2. _A set_ \(\mathcal{L}\) _of sequences of operation instances, called_ legal sequences_, which satisfies two properties:_ 1. _Prefix Closure:_ _If a sequence_ \(\rho\) _is in_ \(\mathcal{L}\)_, then every prefix of_ \(\rho\) _is also in_ \(\mathcal{L}\)_._ 2. _Completeness:_ _If a sequence_ \(\rho\) _is in_ \(\mathcal{L}\)_, then for every operation_ \(OP\in OPS\) _and every argument_ \(arg\) _for_ \(OP\)_, there is a response ret such that_ \(\rho.OP(arg,ret)\) _is in_ \(\mathcal{L}\)_, where \".\" represents concatenation of sequences._  
The intuitive notion of the state of a shared object is determined by the sequence of past operation instances on that object. We say that two such, not necessarily equal, sequences \(\pi\) and \(\rho\) are _equivalent_, denoted \(\pi\equiv\rho\), if for any sequence \(\sigma\) where either \(\pi.\sigma\) or \(\rho.\sigma\) is legal, then \(\rho.\sigma\) or \(\pi.\sigma\) is also legal, respectively. We classify operations by whether they change a shared object's state, return information about it, or both. Definition 2: An _operation_ \(OP\) _of an abstract data type_ \(T\) _is a_ mutator _if there exists a legal sequence \(\rho\) of instances of operations of \(T\) and an instance op of \(OP\) such that \(\rho\
ot\equiv\rho.op\). An operation \(OP\) is an_ accessor _if there exist legal sequences \(\rho,\rho^{\prime}\) of instances of operations of \(T\) and an instance aop of \(OP\) such that \(\rho.\emph{ap}\) is legal, but \(\rho^{\prime}.\emph{ap}\) is not legal._  
_An operation which is both an accessor and a mutator is a_ mixed _operation_. An operation which is a mutator but not an accessor, or an accessor but not a mutator, is a_ pure _mutator or accessor, respectively._  
For example, in an RMW register, _Read_ is a pure accessor, \(Write\) is a pure mutator, and \(Read\)-\(Modify\)-\(Write\) is a mixed operation. In a FIFO queue augmented with _Peek_, _Enqueue_ is a pure mutator, _Dequeue_ is a mixed operation, and _Peek_ is a pure accessor. A data type does not need to have all three kinds, as seen in a \(Read/Write\) register or classic queue without _Peek_. Note that removing all instances of pure accessors from a sequence of operation instances \(\pi\) does not change the state represented, so we denote this equivalent sequence containing only mutator instances as \(\pi|_{m}\). We next give two example definitions of classic data types we will use in this paper. Definition 3 (\(Read/Write\) Register):
1. \(OPS=\{Read,Write\}\)_,_ \(args(Read)=\{\bot\}\)_,_ \(rets(Read)=\mathbb{Z}\)_,_ \(args(Write)=\mathbb{Z}\)_, and_ \(rets(Write)=\{\bot\}\)_._2.