# Relaxed Data Types as Consistency Conditions +
## 2 Model
### Consistency Conditions  
We consider an asynchronous, shared-memory model of computation among \(n\) processes. We split operation instances into separate invocations and responses. Processes interact by invoking operations, with arguments, on shared objects. Some time after an invocation, the object responds, giving the process a return value. Computation takes the form of _schedules_. A schedule of a data type \(T\) is a collection of sequences, one per process, of alternating invocations and responses of operations of \(T\), each occurring at some real time and with each response being of the same operation as the previous invocation, so that they together form an instance of that operation. Each process' sequence is either infinite or ends in an operation response. In a schedule, we call two operation instances at different processes _overlapping_ if the real time of one instance's invocation is between the real times of the invocation and response of the other instance. Ordering non-overlapping instances by their start times produces a partial order on all operation instances, called the _schedule order_.  
Since data type specifications are inherently sequential, we need some way to relate a schedule of a distributed system, which is inherently concurrent, to those specifications. A consistency condition specifies what concurrent schedules are _legal_ on a given data type.  
**Definition 5**.: _A consistency condition \(C\) is a set of schedules defined to be legal on any data type \(T\) under \(C\)._  
When discussing a consistency condition in conjunction with a particular data type, we implicitly consider only the subset of schedules for that type. This definition overloads the term \"legal\" to refer to schedules which correspond, by the consistency condition, to legal sequences on the given data type. Equality of consistency conditions is set equality between sets of legal schedules [7].  
As an example, we define _Linearizability_, which is used throughout the literature in combination with relaxed data types, as it is the most intuitive consistency guarantee.  
**Definition 6** (Linearizability).: _A schedule \(E\) on a data type \(T\) is legal under Linearizability if there exists a permutation \(\Pi\) of all operation instances in \(E\) such that: (1) if an instance op precedes another instance op\({}^{\prime}\) in the schedule order, then op precedes op\({}^{\prime}\) in \(\Pi\); and (2) \(\Pi\) is legal, according to the sequential specification of \(T\)._  
Weaker consistency conditions may allow some reordering with respect to the schedule order. For example, \(k\)-Atomicity for \(\mathit{Read}/\mathit{Write}\) registers, introduced in [25], allows _Read_ operations to get a \"stale\" value, possibly missing some updates which overlap or even immediately precede the _Read_ instance in the schedule order. This staleness is bounded by the constant \(k\), ensuring that the behavior is not arbitrary. In practice, the values \"missed\" can reflect \(\mathit{Write}\) instances which the process invoking the _Read_ has not yet heard about. That work gives probabilistic results showing that only requiring \(k\)-Atomicity can lead to implementations with higher proportions of operations which succeed, meaning that processes do not need to retry as often, improving performance.