{'fraction_non_alphanumeric': 0.03574554449165979, 'fraction_numerical': 0.006837064755501998, 'mean_word_length': 4.280375083724046, 'pattern_counts': {'":': 0, '<': 22, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Separation and Equivalence results for the Crash-stop and Crash-recovery Shared Memory Models

Linearizability, the traditional correctness condition for concurrent data structures is considered insufficient for the non-volatile shared memory model where processes recover following a crash. For this crash-recovery shared memory model, strict-linearizability is considered appropriate since, unlike linearizability, it ensures operations that crash take effect prior to the crash or not at all. This work formalizes and answers the question of whether an implementation of a data type derived for the crash-stop shared memory model is also strict-linearizable in the crash-recovery model. This work presents a rigorous study to prove how helping mechanisms, typically employed by non-blocking implementations, is the algorithmic abstraction that delineates linearizability from strict-linearizability. Our first contribution formalizes the crash-recovery model and how explicit process crashes and recovery introduces further dimensionalities over the standard crash-stop shared memory model. We make the following technical contributions: (i) we prove that strict-linearizability is independent of any known help definition; (ii) we then present a natural definition of help-freedom to prove that any obstruction-free, linearizable and help-free implementation of a total object type is also strict-linearizable; (iii) finally, we prove that for a large class of object types, a non-blocking strict-linearizable implementation cannot have helping. Viewed holistically, this work provides the first precise characterization of the intricacies in applying a concurrent implementation designed for the crash-stop model to the crash-recovery model, and vice-versa.


Introduction
Concurrent data structures for the standard volatile shared memory model typically adopt linearizability as the traditional safety property [15]. However, in the non-volatile shared memory model where processes recover following a crash, linearizability is considered insufficient since it allows object operations that crash to take effect anytime in the future. In the crash-recovery model [8], linearizability is strengthened to force crashed operations to take effect before the crash or not take effect at all, so-called strict-linearizability [2]. While there exists a well-studied body of linearizable data structure implementations in the crash-stop model [17], concurrent implementations in the crash-recovery model are comparatively nascent. Consequently, it is natural to ask: under what conditions is a linearizable implementation in the crash-stop also strict-linearizable in the crash-recovery model?
Non-blocking implementations in the crash-stop model employ helping: i.e., apart from completing their own operation, processes perform additional work to help linearize concurrent operations and make progress. This helping mechanism enables an operation invoked by a process p i to be linearized by the event performed of another process p j , but possibly after the crash of p i . However, strict-linearizability stipulates that the operation invoked by p i be linearized before the crash event. Intuitively, this suggests that linearizable implementations that are help-free must be strict-linearizable (also conjectured in [8]). This work formalizes and answers this precise question: whether a help-free implementation of a data type derived for the crash-stop model can be used as it is in the crash-recovery model.
Precisely answering this question necessitates the formalization of the crash-recovery shared memory model. Explicit process crashes introduces further dimensionalities to the set of executions admissible in the crash-recovery model over the well formalized crash-stop shared memory [6]. Processes may crash on an individual basis, i.e., an event in the execution corresponds to the crash of a single process (we refer to this as the individual crash-recovery model ). An event may also correspond to m (1 < m ≤ n), process crashes where n is total number of processes participating in the concurrent implementation (when m = n it is the full-system crash-recovery model ). Following a crash event in this model, the local state of the process is reset to its initial state when it recovers and restarts an operation assuming the old identifiers crash-recovery model (and resp. new identifiers crash-recovery model ) with the original process identifier (and resp. new process identifier). Our contributions establish equivalence and separation results for crash-stop and the identified crash-recovery models, thus providing a precise characterization of the intricacies in applying a concurrent implementation designed for thecrash-stop model to the crash-recovery model, and vice-versa.

Contributions
First, we define the crash-recovery model and its characteristics. We show that there exist sequential implementations of object types in the crash-stop model that as is have inconsistent sequential specifications in the old identifiers crash-recovery model.
We then consider how data structures use helping in the crash-stop model by adopting the definitions of linearization-helping [9] and universal-helping [5]. When considering an execution with two concurrent operations, the linearization of these operations dictates which operation take effect first. The definition of linearization-helping considers a specific event e, in which it is decided which operation is linearized first. In an implementation that does not have linearization-helping, e is an event by the process whose operation is decided to be the one that comes first. Universal-helping requires that the progress of some processes eventually ensures that all pending invocations are linearized, thus forcing a process to ensure concurrent operations of other processes are eventually linearized.
The first technical contribution of this paper is proving that some pairs of conditions are incomparable. That is, an implementation can satisfy exactly one of them, both, or none.
• linearization-helping vs. universal-helping • strict-linearizability vs. linearization-helping • strict-linearizability vs. universal-helping The second technical contribution is to show that under certain restrictions there is a correlation between some of the above pairs.
• Restricting the definition of linearization-helping to be prefix-respecting, we prove that linearization-help free implies strict-linearizability. More specifically, any obstruction-free implementation of a total object type that is linearizable and has no linearization-helping in the crash-stop model is also strict-linearizable in the new identifiers individual crashrecovery model (Lemma §1). • We prove that any non-blocking implementation of an order-dependent type that is strictlinearizable in the crash-recovery model has no universal-helping in the crash-stop model (Lemma §7). Roadmap. The contributions in this paper are structured as follows: §2 introduces the crashstop shared memory model and other preliminaries. §3 presents our characterization of the dimensionalities of the crash-recovery shared memory model. §4 recalls universal-helping, linearization-helping, valency-helping and presents new results on implementations satisfying these definitions. §5 discuss the correlation between strict-linearizable implementations and linearization-helping. §6 proves that help-freedom does not implies strict-linearizability in general, but under a natural definition of help-freedom it does follows. §7 proves that strictlinearizability and universal-helping are independent. However, for a large class of objects, strict-linearizability implies universal-help freedom. Finally, §8 discuss the relation between strict-linearizability and valency-helping. The paper is concluded with a short discussion in §9.

Related work
Strict-linearizability was proposed by Aguilera et al. [2] who show that it precludes wait-free implementations of multi-reader single-writer registers from single-reader single-writer registers. [8] showed that this is in fact possible with linearizability thus yielding a separation between the crash-stop and crash-recovery models. That helping mechanisms, typically employed by non-blocking implementations, is the algorithmic abstraction that may delineate linearizability from strict-linearizability was also conjectured in [8]. This is the first work to conclusively answer this question by providing the first precise characterization of the intricacies in applying a shared memory concurrent implementation designed for the crash-stop (and resp. crashrecovery) model to the crash-recovery (and resp. crash-stop) model.
Censor-Hillel et al. [9] formalized linearization-helping and showed that without it, certain objects called exact-order types lack wait-free linearizable implementations (assuming only read, write, compare-and-swap, fetch-and-add primitives) in the standard crash-stop shared memory model. Universal-helping and valency-helping were defined by Attiya et al. [5]. Informally, it was shown in [5] that a non-blocking n-process linearizable implementation of a queue or a stack with universal-helping can be used to solve n-process consensus. This result was also extended to strong-linearizability [13] which requires that once an operation is linearized, its linearization order cannot be changed in the future. The definition of strong-linearizability does bear resemblance with the proposed helping definitions in [9,5]; however, it is defined as restriction of linearizability and is incomparable to helping. Indeed, [9] makes the observation that strong-linearizability is incomparable with linearization-helping. The results in this paper study the implications of the universal, linearization and valency helping definitions for strictlinearizability in the crash-recovery, which has not been studied carefully thus far.

Crash-stop Model
This section presents the preliminaries of the standard volatile shared memory model in which processes stop participating following a crash. Processes and shared memory. We consider an asynchronous shared memory system in which a set of N processes communicate by applying operations on shared objects. Each process p i ; i ∈ N has an unique identifier and an initial state. An object is an instance of an abstract data type which specifies a set of operations that provide the only means to manipulate the object. An abstract data type τ defines a set of operations, a set of responses, a set of states, an initial state and a transition relation that determines, for each state and each operation, the set of possible resulting states and produced responses [3]. We consider only deterministic types: when an operation π is applied on an object of type τ in state q, there is exactly one state q to which the object can move to and exactly one matching response r. An object type is total if any operation of the object type applied by any process (we assume that the identifier of the process does not matter) is well-defined for every object state. An example for an object that is not total can be drawn by restricting known objects. For example, consider a stack where process p is allowed to perform P ush(i) only after completing P ush(i − 1). In such object, a process is not allowed to invoke P ush(2) as its first operation. However, to the best of our knowledge, most objects types are total.
An implementation of an object type (sometimes we just say object) τ provides a specific data-representation of τ by applying primitives on a set of shared base objects b 1 , b 2 , . . ., each of which is assigned an initial value and a set of algorithms I 1 (τ ), . . . , I n (τ ), one for each process. We assume that the primitives applied on base objects are deterministic. A primitive is a generic read-modify-write (rmw ) procedure applied to a base object [11,15]. It is characterized by a pair of functions g, h : given the current state of the base object, g is an update function that computes its state after the primitive is applied, while h is a response function that specifies the outcome of the primitive returned to the process. Let e be an event issued by some transaction that applies the rmw primitive g, h to a base object b after an execution E. Let v be the value of b after E. Now, e atomically performs the following: it updates the value of b to the value specified by the function g and returns a response specified by the function h.
Executions and configurations. An event of a process p i in the crash-stop model (sometimes we say admissible step of p i ) is an invocation or response of an operation performed by p i or a rmw primitive applied by p i to a base object along with its response. A configuration specifies the value of each base object and the state of each process. The initial configuration is the configuration in which all base objects have their initial values and all processes are in their initial states.
An execution fragment is a (finite or infinite) sequence of events. An execution of an implementation I is an execution fragment where, starting from the initial configuration, each event is issued according to I and each response of a rmw event matches the state of b resulting from all preceding events. An execution E · E , denoting the concatenation of E and E , is an extension of E and we say that E extends E. Let E be an execution fragment. For every process identifier k, E|k denotes the subsequence of E restricted to events of process p k . If E|k is non-empty, we say that p k participates in E, else we say E is p k -free. An operation π precedes another operation π in an execution E, denoted π → E π , if the response of π occurs before the invocation of π in E. Two operations are concurrent if neither precedes the other. An execution is sequential if it has no concurrent operations. Two executions E and E are indistinguishable to a set P of processes, if for each process p k ∈ P, E|k = E |k. An operation π k ∈ ops(E) is complete in E if it returns a matching response in E. Otherwise we say that it is incomplete or pending in E. We say that an execution E is complete if every invoked operation is complete in E. Well-formed executions. In the crash-stop model, we assume that executions are wellformed : no process invokes a new operation before the previous operation returns. Specifically, we assume that for all p k , E|k begins with the invocation of an operation, is sequential and there is no event between a matching response event and the subsequent following invocation. Safety property: Linearizability. A history H of an execution E is the subsequence of E consisting of all invocations and responses of operations. Histories H and H are equivalent if for every process p i , H|i = H |i. A complete history H is linearizable with respect to an object type τ if there exists a sequential history S equivalent to H such that (1) → H ⊆→ S and (2) S is consistent with the sequential specification of type τ . A history H is linearizable if it can be completed (by adding matching responses to a subset of incomplete operations in H and removing the rest) to a linearizable history [18,7].

Characterization of the Crash-recovery Model
Processes and non-volatile shared memory. We extend the crash-stop model defined in §2 by allow any process p i to fail by crashing; following a crash, process p i does not take any steps until the invocation of a new operation. Following a crash, the state of the shared objects remains the same as before the crash; however, the local state of crashed process is set to its initial state. Executions and configurations. An event of a process p i in the crash-recovery model is any step admissible in the crash-stop model as well as a special ⊥ P crash step; P is a set of process identifiers. The ⊥ P step performs the following actions: (i) for each i ∈ P, the local state of p i set to its initial state, (ii) the execution E 1 · ⊥ P · E 2 ; E 2 is P-free, is indistinguishable to every process j / ∈ P from the execution E 1 · E 2 . In other words, processes are not aware to crash events. Process crash model. We say that an execution E is admissible in the individual crashrecovery model if for any event ⊥ P in E, |P| = 1. If |P| = N, we refer to it as the system-wide crash-recovery model. We say that an implementation I is admissible in the individual crashrecovery model (resp. system-wide crash-recovery model ) if every execution of I is admissible in the individual crash-recovery model (resp. system-wide crash-recovery model ).
Safety property: Strict-Linearizability. A history H is strict-linearizable with respect to an object type τ if there exists a sequential history S equivalent to H c , a strict completion of H, such that (1) → H c ⊆→ S and (2) S is consistent with the sequential specification of τ .
A strict completion of H is obtained from H by inserting matching responses for a subset of pending operations after the operation's invocation and before the next crash step (if any), and finally removing any remaining pending operations and crash steps.
Liveness. An object implementation is obstruction-free if for any execution E and any pending operation π i by process p i , π returns a matching response in E · E or crashes where E is the complete solo-run (E only contains steps of p i executing π) execution fragment of π by p i . An object implementation is non-blocking if in every execution, at least one of the correct processes completes its operation in a finite number of steps or it crashes. An object implementation is wait-free if in every execution, every correct process completes its operation within a finite number of its own steps or crashes. Obviously, liveness in the crash-stop model is identical to the above without the option of process crashing. Old identifiers crash-recovery model. Consider an execution E and a process p i that crashes in E. We say that an execution E is admissible in the old identifiers crash-recovery model if for any process p i and any event ⊥ P in E such that i ∈ P, p i takes its first step in E after the crash by invoking a new operation. New identifiers crash-recovery model. We say that an execution E is admissible in the new identifiers crash-recovery model if for any process p i and any event ⊥ P in E such that i ∈ P, process p i no longer takes steps following ⊥ P in E. Note that even in this model, there are at most N active processes in an execution, i.e., processes that have not crashed.
As we next prove, given an implementation in the crash-stop model, using it as is in the old identifiers crash-recovery model may result a sequential execution in which a process returns an invalid response. Therefore, it is not trivial to transform an implementation from the crashstop model to the old identifiers crash-recovery model. On the other hand, any execution in the new identifier crash-recovery model with crash events is indistinguishable to all non-crashed processes from an execution in the crash-stop model in which every crashed process simply halts, and vice-versa. Thus, and by abuse of notation, we can consider the same execution in both models in the context of deriving proofs for a given implementation.
For this reason, all results in this work concern the new identifiers crash-recovery model, thus we do not state the model explicitly. We note that all impossibility results in this paper holds also for the old identifiers crash-recovery model. This stems from the fact that given an execution in the new identifiers crash-recovery model, it can be seen as an execution in the old identifiers crash-recovery model when N, the total number of processes in the system, is larger then the number of processes taking steps in the execution. Lemma 1. There exists a sequential implementation A of an object type τ in the crash-stop model providing sequential liveness, such that A is not consistent with the sequential specification of τ in the old identifiers system-wide crash-recovery model.
To prove the claim we present an implementation A of type τ , and construct an execution in the old identifiers system-wide crash-recovery model, such that process p i invokes and completes in a crash-free manner an operation σ; however σ returns a response that is not consistent with the sequential specification of τ (sequential liveness in the lemma statement simply requires that a process running sequentially will complete its operation with a matching response). Notice that the lemma holds for the more restricted system-wide crash model, hence it holds for the individual crash model as well. Moreover, the lemma holds even for the weak sequential liveness progress condition, where no concurrency is allowed. Proof. Let B be a sequential implementation of an object type τ . Assume for simplicity no operation returns the value ℵ. Implementation A is obtained by 'wrapping' each operation of B with an extra code. Each process p i has a single-writer single-reader register R[i] initialized to 0. At the beginning of each operation p i first reads R[i]. If it contains value different then 0 then p i stops and returns ℵ. Otherwise, p i writes 1 to R[i], continue with the execution of π as in implementation B, and finally before returning writes 0 back to R[i].
Clearly, algorithm A is a sequential implementation of object τ in the crash-stop model, since any process p i takes the same steps as algorithm B except for the extra reads and writes of R[i]. Since R[i] is initialized to 0, and as p i set it back to 0 before completing any operation, R[i] value is 0 at the beginning of each operation. Consider the following execution in the crash-recovery model. Process p i invokes an operation π and the system crash right after p i sets R[i] ← 1 in line 2. Next, the system recovers p i by invoking a new operation σ, and let p i complete it in a crash-free manner. Since p i crashed after setting R[i] to 1, p i reads 1 in line 1 when executing σ, and thus returns ℵ.

Process Helping
In this section we present the various variants of helping based on previous works [9,5]. We then show that linearization-helping and universal-helping are not comparable, i.e., one does not implies the other. Linearization-helping ( [9], rephrased). We say that f is a linearization function over a set of histories H, if for every H ∈ H, f (H) is a linearization of H. We say that operation π 1 is decided before π 2 in H with respect to f and a set of histories H, if there exists no S ∈ H such that H is a prefix of S and π 2 < f (S) π 1 . Throughout the paper, the binary relation < is used to denote that the linearization of one operation precedes another.
A set of executions E is linearization-help free if there exists a linearization function f over E, such that for any two operations π 1 , π 2 ∈ E and a single step γ such that E · γ ∈ E, it holds that if π 1 is decided before π 2 in E · γ and π 2 is not decided before π 1 in E, then γ is a step of π 1 by the process that invoked π 1 . We say that an implementation is linearization-help free if the set of admissible histories is linearization-help free. Universal-helping ( [5], rephrased). for simplicity and without loss of generality, for the purposes of defining universal-helping, we assume that the first step of every operation is to publish its signature (i.e., the operation type and its operands). Consider a linearizable implementation A of an object type τ and a function t : N → N. Then, A has t-universal-helping (when t is clear from the context, we leave it out) if for every finite execution E · E such that some process completes t(n) or more operations in E whose invocations are contained in E , there is a linearization of E · E satisfying the following conditions: • linearization of E · E contains every operation that is incomplete in E • for every extension E , the execution E · E · E has a linearization such that the linearization of E · E is the same Otherwise, we say that A is universal-help free.
[5] proved that universal-helping implies linearization-helping. However, a careful inspection of the proof reveals an implicit assumption on the object type was made. Roughly speaking, [5] conclude that if a pending operation needs to be linearized by steps of other process due to universal helping then this implies linearization-helping. Although it is the case for many objects, the key point to consider is that universal-helping and linearization-help free definitions requires the existence of a linearization function satisfying specific conditions. Exploiting this flexibility we prove an implementation has universal-helping using some linearization function, while proving it is also linearization-help free using a different linearization function. Claim 1. There exists a wait-free strict-linearizable implementation A of an object type τ in the individual crash-recovery model, such that A has universal-helping and it is linearization-help free in the crash-stop model.

Proof.
A k-bounded Counter τ is an object type supporting a single operation Fetch&Increment (F&I). The initial value of τ is 0. A F&I operation π applies to τ with value l changes the value of the object to l + 1 and returns l if l < k, otherwise l = k and π returns k without changing τ 's value. Algorithm §2 is a wait-free implementation of a k-bounded Counter using CAS (compare-and-swap) primitive.
Linearization-help free. To prove Algorithm §2 is linearization-help free, it is enough to present a linearization function such that each operation π is linearized at a step by the process performing it. Consider the following linearization function: for any execution E and an operation π ∈ ops(E), π is linearized at its successful CAS event, if such exists. Otherwise, if π reads the value k in line 6, this is the linearization point of π.
Universal-helping. We present a linearization function satisfying the conditions of the definition for universal-helping. An operation π performing a successful CAS operation is linearized at the point of the CAS . In addition, once some operation π changes the value of count to k, any other pending operation that is yet to be linearized, is linearized (in an arbitrary order) immediately after π. From that point on, any new invoked operation is linearized on its first step. Let π be a pending F&I operation in an execution E. The following holds -either π already have a linearization point in E; or that if any other process completes k operations starting from E then π have a linearization point. Moreover, the assignment of linearization points is the same for any extending execution.
Strict-Linearizability. The linearization function presented above to prove Algorithm §2 is linearization-help free, also proves it is strict-linearizable. Any operation π is linearized on a step by its owner. Hence, in case process p i crashes while executing an operation π, either the operation was linearized before the crash of p i , or that π has no linearization point in any extending execution. There exists an implementation of a data type that satisfies universal-helping (resp. linearization-helping), but does not satisfy linearization-helping (resp. universal-helping).
Proof sketch. The bounded counter implementation from Claim §1 gives the proof for one direction of Lemma §2. To prove the other direction, we observe that any implementation in which only a subset of the operations are getting help has linearization-helping but no universalhelping. For example, in the Binary Search Tree implementation of Ellen et al. [10] update operations help each other to complete, while find operations do not complete any incomplete update operation. Therefore, intuitively two update operations can prove linearization-helping. However, an infinite sequence of find operations do not complete any pending update operation; thus denying universal-helping since every pending operation must be eventually linearized. [5] also describes an implementation satisfying linearization-helping, but not universal-helping.
The main results in this work focus on universal and linearization-helping. However, [5] also introduced the definition of valency-helping which unlike linearization-helping and universalhelping is defined on operation responses. Since correctness conditions like strict-linearizability only care about linearization order, it is more relevant to discuss help definitions that are defined using the linearization order of operations, and not using the response values. Nonetheless, for pedagogical purposes, we also introduce the definition of valency-helping (and mention its relevance in the context of some results). Valency-helping ( [5], rephrased). Let A be an implementation of object type τ whose inputs and output responses of operations belong to the set V. Let C be a configuration of A and π an operation by process p i . We say that π is v-univalent in C if in every configuration C that is reachable from C in which π is complete, π returns v; otherwise it is multivalent.
Given an operation π by process p i , and a configuration C such that π is multivalent in C, we say that a process p j ; j = i helps process p i in C if the next step of p j results a configuration q(C) such that π is v-univalent in q(C) for some v. We say that A has valency-helping if it has a configuration C such that some process p i helps process p j in C. Otherwise we say that A is valency-help free (Note that valency-helping is incomparable to both universal-helping and linearization-helping [5]).

Strict-linearizability vs. Linearization-helping
In this section we prove that strict-linearizability and linearization-helping are not bonds together. That is, a strict-linearizable implementation in the crash-recovery model can either have or not have linearization-helping in the crash-stop model.
Claim §1 proves that an implementation can be strict-linearizable in the crash-recovery model while being linearization-help free in the crash-stop model. In Claim §2 below we prove there in fact exist linearizable object type implementations that are wait-free with both linearization-helping and universal-helping, but are also strict-linearizable. We find this result to be somewhat surprising, since intuitively helping seems to contradict strict-linearizability -an operation can be linearized by steps of other processes, thus if the owner of the operation crash the linearization point of the crashed operation may be after the crash. As we show, one can consider different linearization functions to proves the different properties of the implementation.

Double-Read-And-Fix Object Type
The type used to prove the claim is a Double-Read-And-Fix (DRAF) type object that supports Read and Write operations. Its sequential specification is as follows: Write(v) operation returns ack. The first Read operation returns an ordered pair v 1 , v 2 of the last two preceding writes (if such exists, otherwise a unique ⊥ symbol is used). Any later Read returns v 1 , v 2 as well. That is, the first Read operation fix the value of the object for the rest of the history. Algorithm 3 presents a wait-free implementation of a DRAF type using read, write and CAS primitives. The variable val is composed of four components. The first two, denoted v 1 , v 2 , represents the status of the object, i.e., the value of the last two writes (in order). The third component, named counter, is a global monotonically increasing counter, counting the number of writes performed to the object so far. The fourth component, named gate, is used to fix the status of the object after the first read operation. Once gate is set to 1 no farther changes to val are allowed. In addition, a shared boolean variable readAnn is used to announce a read operation started, so other processes can help it complete. A detailed description follows.
To perform a Write(u) operation, process p i first read the counter stored in val. Then it proceeds according to the value of readAnn. If readAnn is set, i.e. its value is 1, implying some read operation has been invoked, p i helps it to complete by iteratively attempting to atomically set the gate component of val to 1 while not changing the other components, using a CAS . Once gate is set, p i returns ack. Otherwise no read operation has started. In such case, p i iteratively attempts, using CAS , to atomically add its value u to val by setting the first component of val to u, while increasing the counter by 1. p i stops and returns ack once one of the following holds -it successfully adds its value to val in line 22; the counter was advanced by 2 or more since p i first read it; or, gate has been set.
A  operations, let π be the first Read operation to set readAnn to 1. Then π is linearized at the point where the gate component is set to 1 by some process. All other read operations are linearized at their last read of val in line 25. The correctness of the above linearization order relies on the following simple observations: (i) once readAnn is set to 1 it remains so for the rest of the execution; (ii) any operation invoked after this point, either Read or Write, must first make sure the gate component in val is set before returning. Therefore, no Write invoked after this point can change the values in val; (iii) once the gate component is set it remains so forever, since there is no CAS operation with gate = 1 as its old value.
Denote by t the time when the gate component was set to 1. Let π 1 , π 2 be the last two direct-writes by the above linearization order, if such exists. It follows that both are linearized before time t. Any Read operation π returns only after observing the gate component is set, thus π is linearized at time t or later and returns the values of π 1 , π 2 , since after time t the content of val is fixed. This also implies the first Read to set readAnn must be active at time t, thus its linearization point is within its interval.
Finally, we prove that all other writes except for π 1 , π 2 does not effect the response of other operations. Any Write observing the gate component is set is linearized after time t. Since this is not a direct-write, it does not write to val (except for maybe setting gate), and thus it does not effect other operations response. A Write observing the counter was increased by at least 2 does not write to val. However, since any direct-write increases the value of the counter by 1, this implies at least two direct-writes are linearized after π was invoked. Hence, π is linearized on its first step, and is overridden by later writes.
Wait-Freedom. A direct-write and indirect-write are wait-free -failed CAS in line 21 implies the content of val has been changed. However, any write to val either set the gate to 1, or increases counter by 1. Therefore, the while loop in line 17 can be iterated at most twice.
A Read, as well as helping-write, are wait-free for the following argument. Notice that once the gate component is set, any operation completes in a finite number of steps. Therefore, it suffice to prove the gate is set after a finite number of steps. Consider some process p i attempting to set the gate, i.e., either a Read or a helping-write operation. Any failed CAS attempt implies the value of val has been changed. If the gate was set, then we are done. Otherwise, some other process p j performed a successful direct-write. Hence, its current operation is complete. However, on its next operation, either Read or Write, it will observe readAnn is set, thus it will try to set the gate component as well. As a result, after at most N failed CAS attempts, all processes are either not active, or trying to set the gate, and at least one must succeed.
Linearization-Helping. Since DRAF is an exact-order type, by Theorem 4.18 in [9], any wait-free implementation of an exact-order type using read-write registers and CAS has also linearizationhelping.
Universal-Helping. Denote by f the linearization function used to prove linearizability. We next prove that a similar linearization function proves universal-helping. Let E be an execution, and π be an operation in it by some process p i . To prove universal-helping we prove that after a finite number of operations by any other process π has a linearization point. We consider two cases based on the type of operation.
π is a Read operation. Any other process p j completing two operations after π writes 1 to readAnn must set the gate component to 1, unless it was already set. Although f linearize Read operations on their last access to val, we can change it such that once the gate is set, all pending Read operations are linearized (in an arbitrary order), while any future Read is linearized on its first step. The correctness proof for the new linearization-order is similar to the one given for f . This implies that once the gate is set, π have a linearization point, and this linearization point remains the same for any extension.
π is a Write operation. Consider a different process p j completing two operations after π reads the counter in line 10. Denote by t the time when p j complete the second operation.
Then in any of p j operations, it either observes gate was set, or counter was incremented (by p j or some other process). Hence, at t either gate is set or that counter was incremented by 2 or more. We consider three cases: (1) at t π already written its value to val, i.e., it is a direct-write. Thus by f it has a linearization point before t ; (2) at t the gate is set. Similar to the read case, we can change f such that all non direct-write that are active at the point where the gate is set are linearized at this point (in an arbitrary order, but after the reads). Any later Write is linearized on its first step; (3) at t the counter was incremented by two or more since π first read it. Then π is linearized on its first step by f , and in particular before t ; In all cases we get that π has a linearization point in t , and it remains the same for any extension.
Strict-Linearizability. Consider some execution E in the individual crash-recovery model. Assume p i crashed while executing an operation π. Assume π is a Write operation. If π is a direct-write, meaning that it has written to val in line 21 before the crash, then π has a linearization point before the crash. In any other case, i.e., indirect-write and helping-write, π does not writes its value to val, thus we can consider it as having no linearization point at all.
Assume now π is a Read operation. If π was invoked after gate component was set, then we can consider it has having no linearization point, since it does not effect any other operation. The same can be done in case gate was not set in E. Otherwise, π was invoked before gate was set, and the gate is set in E. Denote by t the time when gate was set. If there is an active non-crashed Read operation at time t, we can linearize it at t, and all crashed Read operations can be removed from the history without effecting any other operation. Therefore, we are left with the case where all read operations are crashed before time t.
w.l.o.g. assume π is the first operation to set readAnn and it is the only Read operation invoked before time t. As we next prove, linearizing π at t does not violates strict-linearizability. Once this is done, all other crashed Read operations, if any, can be removed from the history, and strict-linearizability follow. Notice that t is after the crash point of p i , implying some other operation sets the gate. This seems to contradict strict-linearizability. Nevertheless, we next prove any operation that is linearized before t, is either pending or completed when p i crashed. Therefore, all those operations, including π itself, can be seen as having linearization points before the crash, and this concludes the proof.
Let σ be an operation by some process p j invoked after the crash of π. If σ is a Read operation, then by our simplifying assumption π is the only Read before time t, thus σ was invoked after time t, and in particular is linearized after time t. Otherwise σ is a Write operation. Notice that it can be invoked after the crash of p i and before time t. However, since π already set readAnn to 1, π j must be a helping-write. Therefore it completes only after the gate is set, that is after time t, and it is also linearized after time t. This proves that any operation that is linearized before time t is invoked before the crash of p i .

Claim 2.
There exists an implementation A of an object type τ such that A is linearizable, waitfree and has both linearization-helping and universal-helping in the crash-stop model. Moreover, A is strict-linearizable in the individual crash-recovery model.

Help-freedom vs. Strict-linearizability
In this section we prove an implementation can have no helping (both linearization and universal helping) while still being not strict-linearizable. The result is counter intuitive, since no linearization-helping seems to imply only the owner of an operation p can cause it to be linearized by its own step. Hence, in case of a crash, either the pending operation was already linearized by a step of p, or that it is yet to be linearized and p takes no more steps after the crash, thus the operation will have no linearization point. As we prove, forcing a linearization function to have no decided-before relation between two operations, even after the operations are linearized and completed, allows us to derive such a counter-example.
We then preclude such behaviours by posing a condition on the linearization function. In a nutshell, we consider only functions such that after two operations are linearized, in any extending execution the linearization function must linearized both in the same order. We note that for the best of our knowledge, any known linearizable implementation has such a linearization function. We prove that under this restriction, linearization-help free indeed implies strict-linearizability.

Sticky-Bit Object
A Sticky-Bit object type τ is the most simple form of multi-reader multi-writer register. Its value is initially 0, and it supports Set and Read operations. A Set operations returns ack, while a Read operation returns 0 if there is no Set preceding it in the history, and 1 otherwise. Algorithm §4 presents a Sticky-Bit implementation I using single bit registers, such that I is linearizable, wait-free, linearization-help free, and universal-help free in the crash-stop model. However, as we prove, I is not strict-linearizable in the system-wide crash-recovery model.
Set operation simply writes 1 to val. However, p 0 and p 1 executes Set in a different manner, by first announcing their operation by setting a bit in the ann array, and only then writing 1 to val. Two different Read implementations are provided. For clarity, we refer to it in the code as Read1 and Read2. We assume some processes use only Read1, and all others uses only Read2. As we prove, the claim holds as long as there is at least one process different then p 0 , p 1 using Read1, and at least one such process using Read2. As such, we assume it holds, and do not specify the exact set of processes using each of the different Read implementations. Wait-freedom follows directly from the code. Case I -π is a Set operation. Then, we linearize any Set operation on its write to val. As a result, any other Set is linearized after π, a Read returning 0 is linearized before π, while any Read returning 1 is linearized after π.

Algorithm 4: Sticky-Bit Object
Case II -π is a Read operation, namely, it is Read2. In such case, process p i observed both ann[0] and ann [1] are true, that is both p 0 and p 1 already invoked a Set operation. Denote these operations by Set 0 , Set 1 respectively. Since p i is the first to write to val, no Read operation returned 1 before p i writes to val. We linearized Set 0 at the write to val by π, while any other Set is linearized on the step where it writes to val. As in case I, a Read operation reading val before it was first written is linearized before Set 0 and returns 0, while any other Read operation is linearized after this point and returns 1. This concludes the linearizability proof.
Universal-help Free. Consider an execution E in which p 0 invokes a Set operation, writes 1 to ann[0] and halts. Follow that process p = p 0 performs an infinite sequence of Read1 operations. Then, all Read operations return 0, thus the Set operation is pending and has no linearization point during the entire execution. Hence Algorithm §4 is universal-help free.
Linearization-help Free. Consider some execution E of the implementation. Following the linearization points defined above, in case I any operation is linearized on a step by the process performing it, and thus E is linearization-help free. Nevertheless, in case II, a step by process p i performing Read2 operation results a linearization point for a Set operation by p 0 , while any other operation is linearized on a step by the process performing it. This seems to imply linearization-helping. However, the same argument holds for a linearization order in which we choose to linearize Set 1 instead of Set 0 at the first write to val. Notice that changing the linearization order in this manner does not effect any other operation. Therefore, we can choose a linearization function f such that if case II holds, in some extensions Set 0 is linearized first, while in others Set 1 . For example, based on the number of operations in the execution (odd or even).
Under the linearization function f , E has both an extension where Set 0 is linearize before Set 1 , and vice versa. Hence, by definition Set 0 is not decided before Set 1 at any point. Moreover, according to f , before Set 0 writes to val it can be linearized before any other operation that is yet to read or write val. Once p 0 writes to val it determines the last possible linearization point (in any extension) for Set 0 . In other words, only a step by p 0 can cause Set 0 to be decided before some other operation. The same argument applies to Set 1 . Thus, function f proves I is linearization-help free.
Strict-Linearizability. Consider the following execution E of the implementation I in the crashrecovery model. Each of p 0 , p 1 invokes a Set operation and writes to ann, followed by a systemwide crash. Upon recovery, some process p i invokes and complete a Read1 operation, thus returning 0. Follow that, some other process p j performs Read2 operation to completion and returns 1. It follows that in any linearization order for E one of the Set operations of either p 0 or p 1 (or both) must be linearized in-between the two Read operations of p i and p j , and in particular, after the crash point. This contradicts strict-linearizability.

Claim 3.
There exists a wait-free linearizable implementation I of an object type τ such that I is linearization-help free and universal-help free in the crash-stop model, while I is not strictlinearizable in the system-wide crash-recovery model.
Remark. Implementation I being not strict-linearizable in the system-wide new identifiers crash-recovery model imply I is also not strict-linearizable in all other crash-recovery models -individual (system-wide) new (old) identifiers crash-recovery model. Therefore, Lemma §?? holds for all crash-recovery models.

Lemma 4. Strict-linearizability and linearization-helping are independent
Proof sketch. Lemma 3 proves an implementation can be strict-linearizable in the crash-recovery model while having or not linearization-helping in the crash-stop model. For the not strict-linearizable case, Claim 3 proves an implementation can be not strict-linearizable in the crashrecovery model, while being linearization-help free in the crash-stop model. The last case remains is an implementation being not strict-linearizable in the crash-recovery model, while satisfy linearization-helping in the crash-stop model. This case is almost trivial, and can be proven using many known implementations with linearization-helping. For example, in the Binary Search Tree implementation of Ellen et al. [10], an update operation may mark a node, and later in the execution the operation can be completed by a different process. To prove the implementation is not strict-linearizable, consider the scenario where the process crash after the marking.

An Equivalence between Linearizability and Strict-linearizability
The formalization of linearization-helping specifies a linearization function f such that for any history H it produce its linearization order f (H). As the sticky-bit implementation demonstrates, the formalization of linearization-helping leads to executions where the decided-before order is not well-defined, and this may break the concept of helping leading to non-intuitive results. Specifically, f can linearize operations of some history H in different order for different extensions of H. For example, consider a stack implementation, and a history H where two pop operations π 1 , π 2 are executed concurrently to completion starting from the initial configuration. Both operations returns empty, and can be linearized in any order. Therefore, in different extensions of H, f may sometimes linearize π 1 before π 2 and sometimes vice versa. Thus, although both operations completed, there is no decided-before order between the two.
In this section we restrict the discussion to a more natural prefix-respecting linearization function precluding such a behaviour. We emphasize that to the best of our knowledge, any known implementation has such a linearization function. Definition 1. We say that a linearization function f is prefix-respecting if for any execution E and an execution F extending it, < f (E) ⊆< f (F ) . In other words, for any two operations π 1 , π 2 ∈ E, if π 1 < f (E) π 2 then π 1 < f (F ) π 2 .
Strong-linearizability [13] requires the linearization order of an execution E to be a prefix of the linearization order of any extension of E. Although this seems to bear similarity to prefix-respecting, strong-linearizability is a more restrict requirement. Given an execution E, strong-linearizability requires that if an operation π is linearized in f (E), then in any extending execution no operation σ that is pending in E can be linearized before π, even if σ was invoked before π and it is not linearized in f (E). On the other hand, prefix-respecting allows such a scenario, as long as you do not change the linearization order of operations that are already linearized in f (E).
A key feature of prefix-respecting linearization function is that given an execution E, if some operation π 1 is linearized before π 2 in f (E), then it holds that π 1 is decided before π 2 in E (with respect to f ). Hence, and by abuse of notation, we may say π 1 is linearized before π 2 while referring to the decided before order. Restricting our discussion to linearization-helping based on prefix-respecting linearization functions only, we prove that a linearization-help free implementation A of an object type τ in the crash-stop model is also strict-linearizable in the crash-recovery model. Roughly speaking, under this restriction, if A is linearization-help free and some operation π crashes, then either it has a linearization point before the crash, or that it has no linearization point in any extending execution, as steps by other processes can not cause it to be linearized.

Lemma 5. Let
A be an obstruction-free implementation of a total object type τ such that A is not strict-linearizable in the individual crash-recovery model. Then, any prefix-respecting linearization function f of A imply linearization-helping in the crash-stop model. Proof. In high-level, since A is not strict-linearizable there exists an execution E of A contradicting strict-linearizability. Assume towards a contradiction there exists a prefix-respecting linearization function f such that A is linearization-help free with respect to f . E does not satisfy strict-linearizability, thus there exists a crashed operation π j which is linearized after the crash of its owner process p j in f (E). Consider some operation π z by a different process p z . We prove that π j is not decided before π z when p j crash, while π j is decided before π z in E. However, after the crash of p j all steps are by processes different then p j , thus contradicting linearization-help free. A detailed proof follows.
Notation and Observations. For the rest of the proof we fix the linearization function f . Therefore, all claims are with respect to f , and we do not mention it. In addition, by abuse of notation we write π 1 < F π 2 to denote π 1 < f (F ) π 2 . Given two operations π 1 , π 2 we write π 1 F π 2 (π 1 F π 2 ) if π 1 is decided before (not decided before) π 2 in the execution F with respect to f . We say that a process p i is idle in execution F if p i has no pending operation in F . Let F be an execution, and π 1 , π 2 be operations by p 1 , p 2 respectively. The following claims hold: P1: π 1 < F π 2 imply π 1 F π 2 .
Explanation: f is prefix-respecting, thus lineatization order implies decided before order.
P2: π 1 F π 2 implies there exists an extension of F such that π 2 is linearized before π 1 .
Explanation: follows immediately from the definition of decided before order.
Detailed Proof. f (E) is a linearization of E, hence a contradiction to strict-linearizability is due to a crashed operation π j by some process p j . That is, π j is linearized after the crash of p j in f (E). Next we prove this implies π i < E π j < E π k for some operations π i , π k , by processes p i , p k respectively, such that π i was invoked after the crash of p j .
Assume towards a contradiction one of π i , π k does not exists. If no such π i exists, then any operation that is linearized before π j in f (E) was invoked before the crash of p j . As a result, all those operations, including π j , have a linearization point before the crash of p j . If no such π k exists, then no operation is linearized after π j in f (E). We consider a linearization order similar to f (E) in which π j have no linearization point. We get a linearization order for E in which π j is either linearized before the crash of p j , or have no linearization point at all, contradicting the fact that π j must be linearized after its crash.
Denote the execution up to the invocation of π i by E . Let p z be an idle process in E , and let π z be an operation by p z . We prove (1) π j E π z ; (2) π j E π z . However, the extension leading from E to E is p j -free, since p j crashed in E , contradicting P4. Figure 1 depicts the structure of the execution constructed by our proof.
For simplicity, we first prove the lemma under the following two assumptions: (i) π i , π k are completed in E; (ii) starting from E only p i and p k takes steps in E, while all other processes are idle. To prove (1) we construct an execution starting from E such that π z is linearized before π j . Consider a solo run of p z starting from E such that π z is completed and linearized. Denote the resulted execution by F . Since π i is yet to be invoked in F we get π z F π i . Notice that π j E π i , since there is an extension of E leading to E in which π i < E π j . The extension leading from E to F is p i -free, thus by P4 π j F π i . By P2 there exists an extension of F to an execution G such that π i < G π j . Since π z F π i , in any extension of F , and in particular in G, π z is linearized before π i , which is linearized before π j . We next prove (2). Since π j < E π k , by P1 π j E π k . By our assumption π k is completed in E before π z is invoked, thus π k E π z . Since is transitive, π j E π z .
Next, we prove the general case without the simplifying assumptions made above. To do so, we construct an execution in which the two assumptions holds. That is, after E only p i and p k may take steps while all other processes are idle, and both π i , π k are completed. The construction proceeds in phases.
Phase 1. Denote the execution up to the crash point of p j by E 0 . Starting from E 0 , as long as there is a pending operation π by a process p / ∈ {p i , p j , p k }, we let p perform a solo run and complete its pending operation. Denote the resulted execution by E 1 . By the construction, in E 1 all processes except maybe for p i , p j , p k are idle. Since there is an extension of E 0 such that π i < E π j < E π k , we get π j E 0 π i and π k E 0 π j . However, all steps in the extension of E 0 to E 1 are by processes different then p i , p j , p k , thus by P4 π j E 1 π i and π k E 1 π j . Phase 2. Starting from E 1 , let p i complete its pending operation, if such exists, followed by an execution of π i to completion. Denote the resulted execution by E 2 . Since all steps in the extension from E 1 to E 2 are by p i , following P4 we have π j E 2 π i and π k E 2 π j . We now prove that since π i is completed in E 2 and linearized, this implies π i E 2 π j .
Assume towards a contradiction π i E 2 π j . Since π j E 2 π i holds, by P2 there exists an extension of E 2 in which π i is linearized and decided before π j . However, π i is completed and have no more steps to take. Thus, there is a step by an operation different then π i causing π i to be decided before π j . This contradicts the fact that f is linearization-help free.
Phase 3. Finally, starting from E 2 we let p k complete any pending operation different then π k , if such exists, followed by an execution of π k to completion in a solo-run manner. Denote the resulted execution by E 3 . We prove E 3 satisfies all the required conditions. First, notice that p j crashed in E 3 . In addition, starting from the invocation step of π i , only p i and p j takes steps, while any other process is idle, and both π i , π k are completed in E 3 . It remains to prove π i < E 3 π j < E 3 π k . Since E 3 is an extension of E 2 we have π i E 3 π j . As we next prove, π j E 3 π k . Moreover, by the construction π i < E 3 π k . This proves π j must be linearized between π i and π k . This completes the proof.
To prove π j E 3 π k , we prove it holds in E 0 , and thus in any extension of E 0 . Assume towards a contradiction π j E 0 π k . Since p j crashed in E 0 , the extension leading to E is p j -free. By P4 π j E π k , contradicting the fact that π j < E π k . Corollary 1. Let A be an obstruction-free implementation of a total object type τ such that A is linearizable and linearization-help free in the crash-stop model. Then A is strict-linearizable in the individual crash-recovery model.

Strict-Linearizability vs. Universal-helping
In this section we prove that strict-linearizability and universal-helping are independent. We then prove that for a large class of object types, any strict-linearizable implementation in the crash-recovery model is universal-help free in the crash-stop model. Lemma 6. Strict-linearizability and universal-helping are independent Proof sketch. We prove an implementation being strict-linearizable or not in the crash-recovery model is independent of it having or not having universal-helping in the crash-stop model. We do so by proving that for any of the four possible combinations there exists an implementation.
Strict-linearizability + Universal-help free. This direction is intuitive, since naturally strictlinearizability seems to contradict universal-helping. Indeed, any strict-linearizable implementation we are familiar with is universal-help free in the crash-stop model. For example, consider the well-known Harris linked-list [14]. It is strict-linearizable in the crash-recovery model since any operation is linearized on a step by its owner process. However, it is universal-help free in the crash-stop model since processes do not help each other (except for physical removal of nodes), thus an insert operation will never be completed if its owner halts before adding the key to the list.
not Strict-linearizable + Universal-helping. This direction is intuitive as well, since in most cases universal-helping contradicts strict-linearizability. Consider Herlihy universal-construction [16] applied to a stack object type. It has universal-helping in the crash-stop model. However, it is not strict-linearizable in the crash-recovery model, since a process may crash after announcing a pop operation, and later that operation can be completed by a different process. This may result a return value of a push operation which was invoked after the crash. This implies the linearization point of the pop operation must be after the crash.
not Strict-linearizable + Universal-help free. Follows from Claim 3

Equivalence between Strict-linearizability and Universal-help Freedom
Notation. Given a sequential history H and an operation π, we denote by H + π the set of all sequential histories obtained by including π (i.e., its invocation and response) in H. The same is defined for more than one operation. Two sequential histories H 1 , H 2 are distinct if there exists an operation π in both such that its response is different. If π is in some (common) sub-history H, we say that H 1 , H 2 are distinct for an operation in H.
Order-dependant types include many known objects, such as queue and stack. In a nutshell, an order-dependent type have two operations such that adding exactly one of them or both changes the response of some other operation. Moreover, the order in which both operations are performed (starting from the initial configuration) effects the response of some other operation.
Claim 7.1.1. A queue is an order-dependent type.
Proof. Let π 1 = Enqueue(1), π 2 = Enqueue(2), and H be an infinite sequence of Dequeue operations. Assuming the queue is initially empty, all operations in H returns empty. Adding only one of π 1 , π 2 cause a single operation in H to return a value different then empty, while adding both effects the response of two operations in H. In addition, the first Dequeue operation in H returns different response in the histories π 1 · π 2 · H and π 2 · π 1 · H. Claim 7.1.2. A stack is an order-dependent type.
Proof. Let π 1 = P ush(1), π 2 = P ush (2), and H be an infinite sequence of P op operations. Assuming the stack is initially empty, all operations in H returns empty. Adding only one of π 1 , π 2 cause a single operation in H to return a value different then empty, while adding both effects the response of two operations in H. In addition, the first P op operation in H returns different response in the histories π 1 · π 2 · H and π 2 · π 1 · H.

Separating Exact-Order and Order-Dependent types
Order-dependant are closely related to exact-order types [9]. Roughly speaking, exact-order types are types in which operations are non-commutative, that is, switching the order of two operations changes the response of future operations. [9] proved that an exact-order type precludes a linearizable wait-free and linearization-help free implementation using read, write, compare-and-swap and fetch-and-add primitives. We next prove that order-dependant type and exact-order type are incomparable. For convenience, we present the definition and results for exact-order type as appears in [9]. For more details, we refer the reader to [9].
Notation. Let S be a sequential history. We denote by S(n) the first n operations in S, and by S n the n-th operation in S. We denote by (S + π?) all sequential histories that contains S and possibly also the operation π. In other words, (S + π?) is a set of sequential histories that contains S, and also all sequential histories that are similar to S, except that a single operation π is inserted in somewhere between (or before or after) the operations of S.
Definition 3 (Exact-Order Type. Definition 4.1 [9]). An exact order type τ is a type for which there exists an operation π, an infinite sequential history of operations W , and a (finite or an infinite) sequential history of operations R, such that for every integer n ≥ 0 there exists an integer m ≥ 1, such that for at least one operation in R(m), the result it returns in any history in W (n + 1) · (R(m) + π?) differs from the result it returns in any history in W (n) · π · (R(m) + W n+1 ?).
Theorem 1 (Theorem 4.18 [9]). A wait-free linearizable implementation of an exact order type using read, write, compare-and-swap and fetch-and-add primitives cannot be linearization-help free.
Order-Dependent does not imply Exact-Order A Double-Write-Register type is a variant of a multi-reader-multi-writer register supporting exactly two writes. The sequential specification is as follows: a Write(v) operation returns ack ; a Read operation returns the pair of values written by the first two Write operations in the history (if such exists, otherwise a unique symbol ⊥ is used). In other words, all Write operations after the first two writes do not effect any other operation.
Order-Dependent Type. To satisfy the conditions of Definition 2, we define H to be an infinite sequence of Read operations, and π 1 , π 2 to be Write(1), Write(2) operations, respectively. The proof is simple and straightforward, and is left to the reader.
Exact-Order Type. An exact-order type requires an infinite sequence of operations W , and an operation π, such that for any i, π and W i are non-commutative after W (i − 1). However, this implies any operation in W must be a Write operation, since Read operation does not effect any other operation. As a result, after the history W 1 · W 2 the value of the register is set, and no operation effects the result of any future operation. This contradicts the requirement of π and W 3 being non-commutative after the history W 1 · W 2 . Hence, no such sequence of operations W exists, and a Double-Write-Register is not an exact-order type.
Exact-Order does not imply Order-Dependent We prove that the Double-Read-And-Fix object type presented in Section §?? is an exact-order type but not an order-dependent type. By Claim 2 there exists an implementation of a DRAF object using registers and CAS only such that it is wait-free, linearizable and has both linearization-helping and universal-helping in the crash-stop model, while it is strict-linearizable in the crash-recovery model. This proves that Lemma 7 does not apply to exact-order types. Notice that one can find a type for which Lemma 7 can be applied, although it is not order-dependent. Nonetheless, as DRAF type demonstrate, defining the exact set of objects for which Lemma 7 can be applied is not a trivial task, as known sets of objects are not suffice.
Exact-Order Type. Let W be an infinite sequence of alternating Write(0) and Write (1) operations. Let π be a Write(2) operation, and R = σ a single Read operation. Consider a finite prefix of W , denoted by H. w.l.o.g. assume the last operation in H is Write(0) (the other case is symmetric). That is, the next operation in W is Write(1).
Order-Dependent Type. Assume towards a contradiction DRAF is an order-dependant type. Let H be an infinite sequence of operations, π 1 , π 2 two operations, as in Definition 2. If H contains a Read operation, then adding either π 1 or π 2 after the first Read does not effect any operation, thus contradicting condition 1 of Definition 2. Otherwise, H is a sequence of Write operations. However, Write always returns ack, thus condition 2 of Definition 2 does not hold. This is a contradiction. Hence, DRAF is not an order-dependent type.
Order-dependent type plus Strict-Linearizability implies Universal-help Freedom Lemma 7. Let A be a non-blocking implementation of an order-dependent total type τ , such that A is strict-linearizable in the system-wide crash-recovery model. Then A is linearizable and universal-help free in the crash-stop model.
Proof. Consider an implementation A as in the lemma. Notice that A is linearizable in the crashstop model, since applying strict-linearizability correctness condition to crash-free executions only implies linearizability.
Assume towards a contradiction A has universal-helping. Since τ is an order-dependent type there exists an infinite history H and two operations π 1 , π 2 satisfying the conditions of Definition §2. Consider a system with 3 processes p 1 , p 2 , p 3 . Starting from the initial configuration, let p 1 invoke π 1 and publish its signature, followed by p 2 invoke and publish π 2 signature. Denote the resulted execution by D. From D we let p 3 performs the sequence of operations H in a solo-run manner. Denote the resulted execution by E. Since A is total and non-blocking such an execution exists. In high-level, since A has universal-helping, after a finite number of operations by p 3 both π 1 , π 2 are linearized. Since A is strict-linearizable, adding a system-wide crash at D guarantees both operations must be linearized before the crash. Order-dependant ensures both operation must be linearized in a specific order. w.l.o.g. π 1 is linearized before π 2 . We then consider a similar execution, in which p 2 publish its signature first and crash. For the same reasons, π 2 must be linearized after π 1 , that is, after the crash of p 2 , contradicting strict-linearizability. A detailed proof follows.
By our assumption, A has universal-helping, thus after a finite number of complete operations by p 3 both π 1 , π 2 have linearization points, that is, in lin(E) both π 1 and π 2 are linearized. Consider an equivalent execution in the system-wide crash-recovery model, where the system crash at D. Notice this does not effect the steps of p 3 . By abuse of notation, we denote both executions by E. Since A is strict-linearizable, there exists a linearization slin(E) in which each of π 1 , π 2 is either linearized before the crash, or not linearized at all. By OD1 both operations must be linearized in slin(E), since they affected some operation in H. In other words, there exists no linearization of E such that exactly one of π 1 , π 2 , or none of them, is linearized. Following OD2, there exists a single linearization order for π 1 , π 2 in slin(E). This is so since a different order effects the response of some operation in H. Assume w.l.o.g. slin(E) = π 1 ·π 2 ·H.
Crashes are not visible to processes, thus we can construct a similar execution as follows: first p 2 invokes and publishes the signature of π 2 , followed by a system crash. Then p 1 invokes π 1 and publishes its signature, followed by a solo run of p 3 executing operations according to H. Since p 3 is executing the same steps as in E, and following the same argument as above, in the resulted execution π 2 must be linearized after π 1 in any linearization function. However, this implies π 2 must be linearized after the crash of p 2 , thus contradicting strict-linearizability.
Corollary 2. Let A be a non-blocking implementation of an order-dependent total object τ such that A has universal-helping in the crash-stop model. Then A is not strict-linearizable in the system-wide crash-recovery model.
Remark. An implementation I that is not strict-linearizable in the system-wide new identifiers crash-recovery model imply I is also not strict-linearizable in all other crash-recovery modelsindividual (system-wide) new (old) identifiers crash-recovery model. Therefore, Lemma §7 and Corollary §2 holds for all crash-recovery models.

Strict-Linearizability vs. Valency-helping
In this section we prove that strict-linearizability and valency-helping are not bonds together. That is, an implementation being strict-linearizable in the crash-recovery model is independent of it having valency-helping in the crash-stop model. We note that we prove a slightly stronger result -strict-linearizability can co-exist with valency-helping and linearization-helping, or with none of the helping definitions.

Claim 4.
There exists a strict-linearizable wait-free implementation A of an object τ in the individual crash-recovery model, such that A is linearizable and satisfies both linearization-helping and valency-helping in the crash-stop model.
The proof of the lemma involves constructing a modified version of the wait-free Snapshot implementation of Attiya et al. [1]. For simplicity of presentation, we present the original snapshot implementation of [1] and then discuss the required modifications. The code appears in Algorithm §5.
Modifications. (i) Each shared register contains the entire history written to it. That is, whenever a process writes to a register Segment it simply appends the new value to the content of the register. Therefore, Segment[i] contains a list of triplets ts, data, view written to it along the execution. Since all registers in the implementation are single-writer, this can be done in a safe and atomic manner. Proof. In the following we assume all initial values are 0.
Strict-Linearizability. Scan is a read-only operation, and thus clearly satisfy strict-linearizability -a crashed Scan is considered to not have a linearization point. An Update operation is linearized when p i writes to Segment[i]. Hence, if a crash occurs before this write then the operation has no linearization point in any extension, otherwise it has a linearization point before the crash.
Linearization-helping. Consider the following execution. Process p 3 invokes a Scan operation, collects the copy of a, starts collecting the copy of b by reading Segment [1], and halts. Process p 1 then completes Update 1 (S, 1) operation, followed by p 2 invocation of Update 2 (S, 2), where p 2 completes the Scan and halts just before writing to Segment [2]. Denote the resulted execution by E.
Starting from E, a solo-run of p 3 completes collecting the copy b, and since a = b (all values are the initial values), p 3 returns 0, 0, 0 . This implies the Scan of p 1 is linearized before Update 1 of p 1 . On the other hand, if p 2 takes its next step after E and writes to Segment [2], then any future Update operation will observe the Update 1 (S, 1) operation. Thus, in any extension, p 3 's Scan will return a snapshot which observe Update 1 (S, 1) or a later update by p 1 . Hence, in any extension the linearization point of Update 1 (S, 1) is before the Scan of p 3 , i.e., p 1 's Update 1 operation is decided before p 3 's Scan operation due to a step by p 2 . This proves linearization-helping.
Valency-helping. To prove valency-helping, consider the following execution. Process p 3 executes a Scan operation and stops after collecting the first copy of a. Process p 1 then completes an Update 1 (S, 1) operation, starts a new Update 1 (S, 2) operation in which it completes the Scan and halts just before the write to Segment [1]. Denote the resulted execution by E, and the next step of p 1 by e.
A step by p 1 results the execution E · e, such that in any extension of it p 3 's Scan returns the view written by p 1 in the step e, that is, the view 1, 0, 0 . The timestamp associated with this view is greater by 2 then then timestamp p 1 read and stored in c [1]. Following the selection rule for indirect view, even in case more Update operations are executed after this point, p 3 will always choose to return this view. This implies p 3 's Scan is univalent after the step e. On the other hand, if starting from E p 2 completes an Update 2 (S, 1) operation, followed by a solo run of p 3 , the Scan operation completes and returns 1, 1, 0 . This implies p 3 's Scan is multivalent in E. This proves valency-helping.
Remark. Algorithm §5 is also strict-linearizable in the more restricted system-wide crashrecovery model. Moreover, a careful analysis of the strict-linearizability proof suggests it also holds for the old identifiers crash-recovery model. Hence, Claim §4 holds for all crash-recovery models.
Lemma 8. An implementation being strict-linearizable in the crash-recovery model is independent of it satisfying valency-helping in the crash-stop model.
Proof sketch. By Claim §4, there exists a strict-linearizable implementation in the crash-recovery model that has also valency-helping in the crash-stop model. On the other hand, take for example the well-known Harris linked-list [14]. It is strict-linearizable in the crash-recovery model since any operation is linearized on a step by its owner process. However, it is valency-help free in the crash-stop model since processes do not help each other (except for physical removal of nodes). We note that Harris linked-list does not satisfy any of the helping definitions.

Discussion
The correctness condition considered in this paper is strict-linearizability. However, weaker conditions have been proposed for the crash-recovery model, including durable-linearizability [19] and recoverable-linearizability [8]. Helping mechanisms seemingly delineate linearizability from strict-linearizability since crashed operations may be linearized anytime in the future. However, this is not the case with durable-and recoverable-linearizability: a pending operation can be linearized anytime in the future, thus intuitively, it does not preclude any kind of helping. Moreover, any linearizable implementation in the crash-stop model is also durable-and recoverable-linearizable in the new identifiers crash-recovery model. Correctness conditions, such as detectability [12] and nesting-safe-recoverable-linearizability [4] has been proposed for a different model in which processes are aware to crash events. More precisely, upon recovery from a crash, processes execute a special recovery function responsible to fix any inconsistencies in the data-structure before proceeding with their normal execution.
The model presented in this paper is an abstract model in which all writes are immediately persistent. This is useful for exploring the limitations of the crash-recovery model, and derive lower-bounds and impossibility results. However, real-world machines introduce another layer of complexity, since caches are volatile. In such machines, a data that has been written to main memory but is yet to be persisted is lost in case of a crash. Therefore, there is a need to carefully and manually regulate eviction of cache lines to main memory in order to avoid critical data loss. Izraelevitz et al. [19] defined and studied such a model, called explicit epoch persistency. In addition, [19] proposed a general durability transformation to transform any implementation from the abstract model to the more realistic model with volatile cache. Although the transformation has been proven to satisfy durable-linearizability, a similar transformation can be used for strict-linearizability. Therefore, our algorithmic results holds also for the explicit epoch persistency model.