title: Amortized Constant Round Atomic Snapshot in Message-Passing Systems
authors: Vijay Garg Saptaparni Kumar Lewis Tseng Xiong Zheng
text: 
  
  Argo Lite: Open-Source Interactive Graph Exploration and Visualization in Browsers
      Siwei Li, Zhiyan Zhou, Anish Upadhayay, Omar Shaikh, Scott Freitas, Haekyu Park, Zijie J. Wang, Susanta Routray, Matthew Hull, Duen Horng Chau
      Aug. 2020
  ==================================================================================================================================================
  
  
  
  
  
   We study the lattice agreement (LA) and atomic snapshot problems in asynchronous message-passing systems where up to f nodes may crash. Our main result is a crash-tolerant atomic snapshot algorithm with amortized constant round complexity. To the best of our knowledge, the best prior result is given by Delporte et al. [TPDS, 18] with amortized O(n) complexity if there are more scans than updates. Our algorithm achieves amortized constant round if there are Ω(√(k)) operations, where k is the number of actual failures in an execution and is bounded by f. Moreover, when there is no failure, our algorithm has O(1) round complexity unconditionally.
   
   To achieve amortized constant round complexity, we devise a simple early-stopping lattice agreement algorithm and use it to “order” the update and scan operations for our snapshot object. Our LA algorithm has O(√(k)) round complexity. It is the first early-stopping LA algorithm in asynchronous systems. 
   
  
  
  
  
  
   
   
   
   
   
  
   
   
   
   
       
       
       
       
       
       
       
  
   
   
  
   
  
  
   
   
   
   
   
   
  
  
  
  
  
  
  § INTRODUCTION
  
  
  The lattice agreement (LA) problem <cit.> and atomic snapshot object (ASO) problem <cit.> are two closely related problems in the literature. In the LA problem, given input values from a lattice, nodes have to decide output values that lie on a chain of the input lattice and satisfy some non-trivial validity property. The atomic snapshot object is a concurrent object well studied in shared memory, e.g.,  <cit.>. An atomic snapshot object is partitioned into segments. Node i can either update the i-th segment (single-writer model), or instantaneously scan all segments of the object. In shared memory, Attiya et al. <cit.> showed how to apply algorithms for one problem to solve the another problem. 
  
  
  
  
  
  
  
  
  
  Both LA algorithms and atomic snapshot objects have a wide spectrum of applications. For example, LA algorithms can be used to implement an update-query state machines <cit.> and linearizable conflict-free replicated data types (CRDT) <cit.>.
  Atomic snapshot objects can be used for solving approximate agreement <cit.>, randomized consensus <cit.>, and implementing wait-free data structures in shared memory <cit.>. 
  
  
  In message-passing systems, atomic snapshot objects can be used for
  
  creating self stabilizing memory, and detecting  stable properties to debug distributed programs. In essence, ASO simplify the design and verification of many distributed and concurrent algorithms (example applications  can be found in <cit.>,<cit.> and <cit.>). 
  Recently, Guerraoui et al. <cit.> also demonstrated a mechanism to use ASO for cryptocurrency.
  
  
  
  
  
  
  
  
  
  
  
      
      
          
          
          
      
      
     
       
      
      
      
      
      
      
      
      
      
      
      
  
  
      
      
  
  
  
  
  
  
  
  
  Contribution:  
  Our main contribution and closely-related works in message-passing networks are summarized in the table below. 
  
  All of our algorithms are proven correct when up to f < n/2 nodes may crash. Our LA algorithm is early-stopping in the sense that the round complexity depends only on k (k ≤ f), the actual number of failures in an execution.
  
  We also present a general transformation to implement ASO from any LA algorithm. Combined with the O(log n) LA algorithm in <cit.>, we obtain an ASO implementation that takes O(log n) rounds for both  and Scan. Our primary contribution is an ASO algorithm which has amortized constant round complexity when there are Ω(√(k)) operations for each node and incurs only constant message size overhead. As a byproduct, we obtain a linearizable update-query state machines <cit.> implementation that takes amortized O(1) rounds for each update and query operation and O(1) message size overhead. 
  
  
  
  
  
  
  
  
  
  
  
  Related Work: Lattice Agreement  
  The lattice agreement (LA) problem is well studied both in synchronous (e.g., <cit.>) and asynchronous (e.g., <cit.>) message-passing systems with crash failures. 
  Mavronicolasa et al. <cit.> give an early-stopping algorithm with round complexity of O(min{h, √(f)}), where h is the height of the input lattice. This is the only early-stopping LA algorithm that we know before our work. 
  In asynchronous systems, the lattice agreement problem cannot be solved when f ≥n/2. All existing work assume that f < n/2. Faleiro et al. <cit.> give the first algorithm for this problem which takes O(n) rounds. Xiong et al <cit.> present an algorithm with round complexity of O(log f).
  LA in the Byzantine fault model is also studied recently. Algorithms for both synchronous systems and asynchronous have been proposed <cit.>.  The equivalence quorum technique for our LA algorithm is quite different from the techniques in these papers.
  
  
  
  Related Work: Atomic Snapshot  
  ASO is well studied in shared memory, e.g., <cit.>. Due to space constraint, we focus our discussion in message-passing networks.
  In message-passing systems, there are many algorithms for implementing atomic read/write registers in the presence of crash faults <cit.>. 
  A simple way to implement an atomic snapshot object is to first build n SWMR (single-writer/multi-reader) atomic registers, and then use a shared-memory ASO algorithm, e.g., <cit.>. 
  
  Delporte et al. <cit.> present the first algorithm for directly implementing an ASO in crash-prone asynchronous message-passing systems. In their implementation, each  operation takes two rounds and O(n) messages, and each operation takes O(n) rounds and O(n^2) messages. 
  A recent preprint by Attiya et al. <cit.> implement a store-collect object in dynamic networks with continuous churn. They also show how to use the store-collect object to build an ASO. These two algorithms and the read/write-register-based algorithms have worse round complexity than our ASO algorithm. In terms of techniques, our ASO algorithm is inspired by <cit.>. We will discuss in more details in Section <ref>.
  
  
  
  
  
  System Model:  
  We consider an asynchronous message-passing system composed of n nodes with unique identifiers from {1,2,...,n}. 
  
  Nodes do not have clocks and cannot determine the current time nor directly measure how much time has elapsed since some event. Each node has exactly one server thread and at most one client thread. Client threads invoke or  operations. Each client thread can have at most one or  operation at any time, i.e., each process is sequential. 
  Server threads handle incoming messages (i.e., event-driven message handlers).
  Local computation is negligible compared to the message delay (or network latency). At most f nodes may fail by crashing in the system. We use k, where k≤ f, to denote the actual number of failures in a given execution. 
  
  
  
  
  
  
  Each pair of nodes can communicate with each other by sending messages along point-to-point channels. Channels are reliable and FIFO (First-In, First-Out). “Reliable” means that a message m sent by node i to node j is eventually received by node j if j has not already crashed. That is, once the command “send m to j” is completed at node i, then the network layer is responsible for delivering m to j. The delivery will occur even if node i crashes after completing the “send” command. Such a channel can be implemented by a reliable broadcast primitive in practical networks <cit.>. 
  FIFO means that if message m_1 is sent before message m_2 by node i to node j, then m_1 is delivered  before m_2 at node j.
  
  
  
  
  
  
      
      
      
      
      
      
      
      
      
      
      
      
      
  
  
  
  
  
  
  
  
  Lattice Agreement (LA):  
  
  Let (X, ≤, ⊔) be a finite join semi-lattice with a partial order ≤ and join ⊔. Two values u and v in X are comparable iff u ≤ v or v ≤ u. The join of u and v is denoted as ⊔{u, v}. X is a join semi-lattice if a join exists for every non-empty finite subset of X. In this paper, we use the term lattice instead of
  join semi-lattice for simplicity. More background on join semi-lattices can be found in <cit.>.
  
  In the lattice agreement problem <cit.>, each node i proposes a value x_i ∈ X and must decide on some output y_i ∈ X such that the following properties are satisfied: 
  
  
      
    * Downward-Validity: For all i ∈ [1..n], x_i ≤ y_i. 
      
      
    * Upward-Validity: For all i ∈ [1..n], y_i ≤⊔{x_1,...,x_n}.
      
      
    * Comparability: For all i ∈ [1..n] and j 
  ∈ [1..n], either y_i ≤ y_j or y_j ≤ y_i.
  
  
  
  
  
  
  
  
  
  
   §.§ The Byzantine Lattice Agreement Problem
  
  
  As per discussion with Xiong, we will remove Byzantine part from this paper so that we have enough room to present main results and focus on the crash faults.
  
  The Byzantine lattice agreement problem (BLA) <cit.> is similar to the lattice agreement problem. Each node has an input value from a lattice and needs to output a value from the lattice such that all output values of correct processes are comparable. The difference lies on the validity condition. The Upward-Validity is modified as follows to prevent Byzantine nodes introducing arbitrary number of values into the outputs of correct nodes. 
  
  
      
    * Upward-Validity: ⊔{y_i   |   i ∈ C}≤⊔({x_i   |   i ∈ C}∪ B), where B ⊂ X and |B| ≤ k.  
  
  
  
  
  
  
  Atomic Snapshot Object (ASO):  
  The snapshot object is made up of n segments (one per node), and provides two operations:  and Scan. Node i invokes (v) to write value v into the i-th segment of the snapshot object. We adopt the single-writer semantics, i.e., only i can write to the i-th segment.  The operation allows a node to obtain an instantaneous view of the snapshot object. The returns a vector Snap, where Snap[i] is a value of the i-th segment.   
  
  
  
  
  
  Intuitively, a snapshot object is atomic  
  (or linearizable) <cit.> if every operation appears to happen instantaneously at some point in time between its invocation and response events. 
  More formally, for each execution, there exists a sequence or ordering σ that contains all and  operations in the execution and satisfies the following properties: 
  
      
    * Real-time order: If operation Op_1 completes before operation Op_2 starts in the execution, then Op_1 appears before Op_2 in σ.
      
    * Sequential specification: If a operation returns the vector Snap, then for every i∈{1 ,⋯, n}, Snap[i] is the value written by the  operation by node i  that precedes the operation in σ or the initial value if no such  exists.
  
  
  
  
  
  
  
  
      
      
      
      
      
      
         
      
  
  
  
  
  
  § EARLY-STOPPING LATTICE  AGREEMENT ALGORITHM
  
  
  
  ++++++
  
  
   §.§ Model: Same as above
  
  
      
    * We do one shot lattice agreement
      
    * Assume FIFO message delivery per node.
      
    * Sequential computing at each node
      
    * Assume Reliable Broadcast (See Bracha)
      
  
  ++++++++
  
  
  
  
  We first present ELA (Early-stopping Lattice Agreement) in Algorithm <ref>. 
  Our constant amortized round atomic snapshot implementation uses a variation of ELA to “order” and , which will be discussed in the next section. The ELA algorithm is inspired by the stable vector algorithm by Attiya et al. <cit.> and Mendes et al. <cit.>. One of our key contributions is the formal abstraction of the equivalence quorum condition and its application to lattice agreement and atomic snapshot objects implementations.
  
  Each node i
  is given an input x, and at all times, i maintains a vector of sets, V_i[1]⋯ V_i[n], where V_i[j] (j i) stores the set of values received from node j. We denote that a variable v belongs to node i by attaching to it the subscript i, for example v_i. When the node identity is clear from the context, we often omit the subscript. 
  
  
  
  
  
  
  
  
  The ELA algorithm has two main parts: exchange all values known so far, and determine when it is “safe” to output a value using a decision rule.
  One key challenge is to identify the decision rule to enable the early-stopping property. Our decision rule  is based on the existence of 
  an equivalence quorum. Let V be a vector of size n and i∈{1, ⋯,n}. We define the predicate (V,i) as follows. 
   
  
  (V,i) is true iff ∃ Q ⊆{1, ⋯,n} s.t. |Q| ≥ n - f ∧ V[j] = V[i], ∀ j ∈ Q. When the predicate is true, we call  Q as the equivalence quorum. 
  
  
  In ELA, node i decides when the predicate (V_i,i) becomes true for the first time. Intuitively, 
  (V_i, i) becomes true when node i learns about ≥ n-f nodes (including i) with identical sets of values. 
  Then, node i decides on the join of all values in V_i[i]. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  [!hptb]
  
  ELA (Early-stopping Lattice Agreement): Code for node i
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  Correctness of ELA:  
  Consider any execution of Algorithm <ref>. We show that the outputs of correct nodes satisfy the three properties defined in Section <ref>. Due to space constraint, proofs are presented in Appendix <ref>. 
  Downward-validity and upward-validity are straightforward from the code. 
  Lemmas <ref> is key for proving comparability in Lemma <ref>.
  For any two sets U and V, we say U and V are comparable if either U ⊆ V or V ⊆ U.
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  lemmacompViewsForSameNode 
  For any two nodes i and j, fix time t and t', and then the set V_i[s] at time t and the set V_j[s] at time t' are comparable for each node s.
  
  
  
  
  
  
  
  
  By applying Lemma <ref> and the decision rule, we have the following lemma. 
  lemmacomparabilityELA[Comparability] 
  For any two nodes i and j, y_i and y_j are comparable.  
  
  
  
  
  
  
  
  
  
  
  
  Round Complexity:  
  Given an execution of ELA, let D be the maximum message delay. That is, if both the sender and the receiver are nonfaulty, then the sender's message will be received by the receiver within time D. We divide time into intervals of length D and each interval is called a round. 
  For simplicity, we assume that every node initiates the ELA algorithm at the same time. 
  
  
  The analysis can be generalized to the case when nodes invoke ELA within constant number of rounds. 
  We begin with a useful definition. 
  
  
  
  [Exposed value in an interval] 
  We say a value v is an exposed value in interval [t, t + D) if some nonfaulty node receives v in interval [t, t+D), and no nonfaulty node has received v before time t. 
  
  
  Note that by definition, any exposed value for t > D must be the input of some faulty node. We have the following lemma, which guarantees the termination of our algorithm.
  
  
  lemmaterminationELA[Termination] 
  For an arbitrary interval [t, t + 2D). If there does not exist any exposed value in this interval, then all undecided nonfaulty nodes decide by time t + 2D. 
  
  
  Lemma <ref> follows from the observation that if there is no exposed value in the [t, t + 2D) interval, then at the end of the interval, for each node i, we must have V_i[j] = V_i[i] for each nonfaulty j. Now we introduce the notion of failure chain of an exposed value. 
  
   
   
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  A sequence of nodes p_1,p_2,...,p_m is said to form a failure chain of an exposed  value v if (i) p_1, p_2, …, p_m -1 are faulty, and p_m is correct; (ii) the input value of p_1 is v; (iii) p_i receives value v from p_i-1; and (iv) For 1 ≤ i < m - 1, p_i crashes while sending (v,p_i) to other nodes, i.e., p_1 crashes when executing line 1 and p_2,...,p_m-2 crash when executing line <ref>. 
  
  
  
  
  lemmafailureChainLength 
  If value v is an exposed value in interval [t, t + D), then value v has a failure chain with length at least t/D + 1.
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  The following lemma can be derived from condition (iv) of Definition <ref>. 
  
  lemmauniqueFailureChain 
  For any two exposed values v and u with failure chain P_v and P_u respectively. Then, the first |P_v| - 2 nodes in P_v and the first |P_u| - 2 nodes in P_u are disjoint.
  
  
  
  
  
  
  
  
  lemmaroundComplexityELA 
  If an execution has k≤ f crash failures, then ELA takes at most 2 √(k) rounds. 
  
  
  Since there are at most k failures in the execution, and an exposed value in interval [t, t + D) is associated with ≥t/D - 1 unique faulty nodes by Lemma <ref> and <ref>, we cannot have > 2√(k) distinct intervals with exposed values. Lemma <ref> then implies that ELA takes at most 2√(k) rounds.  
  
  
  
  
  
  
  
  
  § ATOMIC SNAPSHOT OBJECT
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  In this section, we present two algorithms for implementing an atomic snapshot object in crash-prone asynchronous message-passing systems with f < n/2. 
  
  
  
  
  
  
  
  
  
  
   §.§ General Transformation
  
   Attiya et al. <cit.> gave an elegant algorithm that transforms any wait-free lattice agreement algorithm to a wait-free atomic snapshot object in the shared memory systems. Their key idea is to invoke a sequence of lattice agreement instances to obtain comparable snapshots. 
  
  
  
  
  
  
  To adapt the algorithm in <cit.> for  message-passing systems, we need to make two main modifications: (i) Replace each read or write step in shared memory by sending a read or write message to all nodes and waiting for n - f acknowledgements; and (ii) Add another write step (sending the input to at least n - f nodes) before invoking a lattice agreement instance. Since the algorithm is similar to the algorithm in <cit.> except for these two changes,  we present the algorithm, TS-ASO, and its proof in Appendix <ref>.
  Using the O(log n)-round lattice agreement algorithm by Xiong et al. <cit.> in our transformation gives an implementation of atomic snapshot objects that take O(log n) rounds for both  and operations.[Note that the algorithm in <cit.> actually has round complexity O(log f); however, if we plug in the original version, our transformation becomes O(n) rounds. We need to make a simple modification of the algorithm in <cit.> to get O(log n) round complexity. Please refer to Appendix <ref> for more details.] 
  
  
  
  
  
  
      
  
  
  
  
  
  
  
  
  
  One drawback of our transformation is that it does not necessarily “preserve” the round complexity of the lattice agreement algorithm. This is because the round complexity analysis of some lattice agreement algorithms depends on the assumption that each node starts around the same time and different nodes might participate in the same lattice agreement instance at different times in TS-ASO. Therefore, directly using our ELA algorithm in the transformation gives a round complexity of O(n).[The round complexity guarantee of the O(log n) rounds algorithm in <cit.> does not depend on the assumption that all nodes start the algorithm around the same time.] To address this issue, we propose our second atomic snapshot algorithm. 
  
  
  
   
   
   
   
  
  
  
  
  
  
   §.§ Algorithm with Constant Amortized Round Complexity
  
  
  
  Our second atomic snapshot algorithm,  (amortized constant atomic snapshot object), uses the equivalence quorum technique and a novel mechanism of invoking lattice agreement instances
  to ensure amortized round complexity.
  In addition, TS-ASO requires message size overhead of O(n), because each node needs to collect the states of at least a quorum of nodes before participating in a particular lattice agreement instance.  only incurs O(1) message size overhead. As a byproduct, we obtain a linearizable update-query state machines <cit.> that take amortized O(1) rounds for each update and query command and O(1) message size overhead, shown in Appendix <ref>. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
    §.§.§ Main Techniques of 
  
  
  
  Our algorithm  is inspired by <cit.>, i.e., invoking a sequence of lattice agreement instances to implement atomic snapshot. The key technical contribution is to identify how to tightly glue different components together to obtain amortized constant round complexity. We first discuss two goals that need to be achieved for  correctness. Then we introduce a new mechanism of invoking lattice operations, namely LatticeRenewal(), and discuss how we achieve the desired round complexity. Finally, we compare TS-ASO and AC-ASO.
  
  In our discussion below, we call an instance of lattice agreement a lattice operation for brevity.
  Following <cit.>, we will use a tag (or a logical timestamp) to distinguish different lattice operations in . Hence by “nodes participate in lattice operation with the same tag,” we mean that these nodes are in the same instance of the lattice agreement algorithm. Due to the property of lattice agreement, these nodes are guaranteed to obtain comparable outputs.
  Each value written by the  is also assigned a tag as well. Later in Definition <ref>, we  formally define the tag for operations and values.
  
  
  
  
  
  Goals for ensuring correctness:  
  
  In our design, when a or  operation completes, it obtains a “view.”
  Roughly speaking, a view represents a set of values that are observed by the operation and are “safe” to return (to be introduced formally later in Definition <ref>).
  Inspired by <cit.>, we want to achieve the following two goals in our algorithm: (G1) views obtained by all and  operations are comparable; and (G2) once an  completes, its written value is “visible” to any subsequent operations. These two goals allow us to use a natural mechanism to construct a linearization for a given execution. 
  
  It is simple to achieve goal (G2).  ensures that once an  completes, a quorum of nodes have seen the update. 
  For goal (G1), we require each node to participate in lattice operation(s) to complete its and  operations.  
  Intuitively, an operation is completed if it obtains a view, which could be an output of a lattice operation invoked by this operation, or an output borrowed from another lattice operation invoked by some other operation. 
   achieves goal (G1) by maintaining the following invariant:
  
  
  
  
  
  In , the views returned by lattice operations are comparable.
  
  
  
  
  
  
  
  Lattice Renewal:  
  
  
  We introduce the LatticeRenewal() procedure to guarantee Invariant <ref>.
  We stress that even though the usage of borrowed view is not new, we are not aware of any prior work that achieves amortized constant rounds for atomic snapshot objects. 
  LatticeRenewal() is a mechanism to invoke a sequence of lattice operations to provide the following desirable properties:
  
  
  
      
    (P1) LatticeRenewal() invokes at most three lattice operations in a row.
      
      
      
      
      
      
      
    (P2) If any of the lattice operations does not observe a higher tag, then LatticeRenewal() returns the view obtained by that particular lattice operation, namely direct view.
      
      
    (P3) If all three lattice operations observe a larger tag, then LatticeRenewal() fails to find a direct view. It  will then wait to borrow a view from a lattice operation invoked by other nodes, namely indirect view. 
      
      
    (P4) Views returned by LatticeRenewal() are comparable with each other.
  
   
   
  
   
  
  
  
  
  
  
  
  
  
  
  
  (P1) is mainly for correctness and improved round complexity as we will explain next. (P2) to (P4) jointly guarantee Invariant <ref>. Due to the properties of lattice agreement, views returned by the lattice operation with the same tag are comparable. For lattice operations with different tags, we rely on (P2) and (P3). (P2) implies that a lattice operation returns a view iff it does not observe a lattice operation with a higher tag. 
  This together with our approach of obtaining tags ensure that the view returned by a lattice operation with a smaller tag must be known by a lattice operation with a larger tag.
  Therefore, when the lattice operation with a larger tag starts, its view is at least as large as the view of any lattice operation with a smaller tag.
  This allows later lattice operations to learn older views.
  
  Due to message delays and concurrent s, it is possible that all three lattice operations fail to return a view. In this case, we rely on (P3) to ensure that LatticeRenewal() is able to obtain an indirect view. Moreover, our design guarantees that such an indirect view can be borrowed within a constant amount of rounds. In Lemma <ref>, we formally prove that properties (P2) to (P4) are enough to maintain Invariant <ref>.
  
  
  In , a and  operation invokes LatticeRenewal() (after some preprocessing) and the operation is completed when LatticeRenewal() obtains a view. Invariant <ref> can be used to prove (P4), which then guarantees goal (G1) – views obtained by all and  operations are comparable (as formally proved in Lemma <ref>). 
  Later in our correctness proof, this allows us to construct a linearization of operations.
   
  
  
  
  
  
  
  Round Complexity:  
   ensures amortized constant round complexity, and each operation takes O(√(k)) rounds in the worst case. 
  On a high level,  uses the equivalence quorum technique to implement the underlying lattice operation. 
  Worst case round complexity roughly follows the analysis for ELA (Algorithm <ref>) as presented in Section <ref>.
  For amortized constant round, the main property we rely on is the early-stopping property which ensures that if no node fails, then the lattice operation completes in a constant number of rounds.  By assumption, a crashed node does not participate in the algorithm anymore; hence, if we have enough number of and  operations,  achieves amortized constant round complexity. 
  
  Recall that the round complexity analysis of ELA depends on the notion of exposed values (Definition <ref>) and the time interval these values appear. Unlike the (single-shot) lattice agreement problem, atomic snapshot is long-living; thus, it is possible that s attempt to write values with the same tag consecutively in a way that these values are all treated as the input to a particular lattice operation, which eventually “slow down” the progress of that lattice operation, and hence the  operation. This is also the reason that if we plug ELA into our transformation algorithm in Appendix <ref>, we get O(n) round complexity.
  
  Our idea to address this issue is in fact simple: increment tags and invoke lattice operation(s) in a way that “late”  does not prevent the progress of existing
  lattice operations. More concretely, 
  consider a lattice operation with tag T, say Lattice(T), starts at time t. Fix a constant D (which will become clear in Lemma <ref>). We need to ensure that (i) All values from  operations that start after time t + D must have tag strictly greater than T; and (ii) “slow writers” that participate in Lattice(T) after time t+D do not introduce any exposed value with tag T. 
  These two properties ensure that the lattice operation in  completes in O(√(k)) rounds in the worst case, and has a constant amortized round complexity. This observation together with the design that LatticeRenewal() invokes at most three lattice operations give the desired round complexity.
  
  
  
  TS-ASO vs AC-ASO:  
  
  
  Recall that TS-ASO is our general transformation algorithm adapted from <cit.> (presented in Appendix <ref>). We present high-level comparison between  and TS-ASO here, and details in Appendix <ref>. 
  
  
      
    (D1) TS-ASO participates in the first lattice operation using the largest tag read from a quorum, whereas  adds 1 to obtain a new tag for the first lattice operation.
      
    (D2)  has an initial lattice operation in addition to the ones in LatticeRenewal().
      
    (D3) TS-ASO collects the states of at least a quorum and writes the join of the states collected to at least a quorum, and participates in at most two lattice operations to obtain a view. , instead, directly uses at most three lattice operations to obtain a view.
  
  
  Roughly speaking, (D1) allows nodes to invoke a lattice operation with the same tag around the same time. (D2) ensures property (P3) of LatticeRenewal(), particularly, some node without obtaining a direct view can always borrow a view. (D3) ensures property (P4) of LatticeRenewal() and constant message size overhead.
  The details of the necessity of three lattice operations are presented in Lemma <ref>, and the round complexity analysis can be found in Lemma <ref>. 
  
  
  
  
  
  
  
  
  
  
  ++++++ Lewis: Let's follow Xiong's suggestion to remove discussion on Invariant. +++++
  
  
  Concretely, we achieve the following invariant.
  
  
  
  Suppose a lattice operation with tag T starts at time t. All values from  operations that start after time t + D must have tag strictly greater than T for some constant D. 
  
  
  Additionally, we also make sure that before an  invokes the first lattice operation, it already introduces its value (along with a tag) to other nodes. Therefore, even if a “slow” node invokes a lattice operation with the same tag at a later time, no value will be exposed; hence, such a slow behavior will not affect the progress of this lattice operation.
  
  
  
  In order to “preserve” the round complexity of ELA, we need to guarantee that lattice operations with the same tag are invoked at roughly the same time (i.e., within a constant round of each other). this is not completely right. As I said in the email, nodes can participate the lattice operation with the same tag at different times but the node which joins quite late does not introduce any new value This guarantee together with Property 1 and 2 of LatticeRenewal() lead to amortized constant rounds given enough number of operations.
  While the “similar starting time guarantee” might seem trivial, it is subtle to achieve. For example, if we plug in ELA (the only early-stopping lattice agreement algorithm that we know of) into our transformation presented in Appendix XXX (based on Algorithm in <cit.>), the resulting algorithm does not have the same round complexity, because in the transformation algorithm, different nodes may invoke the same instance of the lattice operation at very different time. In the worse case, a single node invokes an  operation in a n consecutive rounds, which will in turn force the lattice operation to complete in Ω(n) rounds.[In comparison, algorithm in <cit.> completes in O(log n) rounds even if nodes invoke it at different time.]
  
   addresses this issue by ensuring the following invariant:
  
  Lewis: check the following invariant
  
  
  
  
  If there is a lattice operation with tag T starting at time t, then all values from  operations that start after time t + D must have tag strictly greater than T. 
  
  
  Actually, I think we are making things more complicated. The following invariant is too technical. We just need to briefly state the high level ideas. When I read the following invariant, I am already lost. 
  
  
  If there are exactly k active nodes in a period of c rounds Find out what is c?, then at most k lattice operations will be invoked with the same tag.
  
  
   achieves Invariant <ref> using the following approaches to handle . We do not care about here, since it does not introduce new values.
  
  
      
      
    * Each node contacts a quorum of nodes to figure out the current tag, say r.
      
      
      
      
    * Each node uses r+1 as the tag, and  sends out its value-tag pair to all nodes before invoking its initial lattice operation with tag r. 
      
      
    * After the initial lattice operation, the node invokes LatticeRenewal(r') where r' is the maximum of r+1 and the largest tag known by the node so far.
      
      
    * Each LatticeRenewal(r) invokes at most three lattice operation with varying tags. The first lattice operation always starts with tag r.
  
  
  
  These approaches together ensures that (i) at most k values would be exposed during c rounds; and (ii) after c rounds (before the first LatticeRenewal(T)), all  will read a tag strictly larger than T. These two properties allow  to maintain Invariant <ref>.
  
  ++++++ Lewis: Old Text that gets too complicated +++++
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
   
   
   
  
  
  
  
  
  
  
  
  
  
      
      
      
      
      
      
      
      
      
      
      
      
  
      
  
  
  
  
  
  
   
  
  
  
  
  [!hptb]
  
  ASO: Code for node i
  
  
  
  
  
  
    §.§.§  Description and Pseudocode
  
  
  
  The pseudocode of  is presented in Algorithm <ref>. We first describe key variables used, followed by the procedures and message handlers. 
  
  
  
  
  Variables:  
  
  
  Each value (written by an  operation) is associated with a timestamp of the form r, j, where r is the tag and j is the ID of the writer who initiates the . The exact value of the tag in the timestamp is determined in the  operation.
  For brevity, we often use value to denote a value-timestamp pair.
  For a set of values H, we use H^≤ r to denote the set of values with tag at most r. 
  
  At all time, each node i keeps track of a vector V_i of size n, which represents the vector of “view” at node i. 
  
  Formally, for j ∈ [n], V_i[j] is the set of written and/or forwarded values that i has received from node j. In our design, each node i needs to forward a value it receives for the first time. In this case, we say a value is forwarded by i. 
  Two other variables are related to V_i: (i) V_i^≤ r is the vector of views with tag at most r, i.e., V^≤ r = [V[1]^≤ r, V[2]^≤ r, …, …, V[n]^≤ r]; and (ii) D_i[j] is a particular view borrowed from node j that can be “safely” returned. 
  The meaning of “safe” will become clear when we discuss the lattice operation.
  
  Each node also keeps track of a variable maxTag, which represents the largest tag it has ever received via writeTag messages or echoTag messages. Note that it is possible that there are some values with tag larger than maxTag in V_i.
  
  
  
  
  
  
  
  Procedures:  
  We explain two helper procedures, Lattice(r) and LatticeRenewal(r), and two interface procedures, (v) and Scan(). Other procedures are fairly straightforward from the pseudocode.
  
  
  Lattice(r): 
  Each node uses the Lattice(r) procedure to run the r-th instance of lattice agreement, or in our terminology, lattice operation with tag r. 
  The goal of a lattice operation is to solve lattice agreement, except that it is associated with an input tag r and the termination condition depends on r and the messages received, especially those with tag ≤ r. 
  
  Consider a Lattice(r) invocation at node i. Node i first writes the input tag r to at least n - f nodes. Then it waits until the equivalence quorum predicate (Definition <ref>) becomes true for the first time. After that if the maxTag value is strictly larger than r, then the lattice operation returns false, ∅. Otherwise, it returns true, V^* where V^* = V^≤ r is the vector that satisfies the equivalence quorum predicate. In this case, Lattice(r) is said to be a good lattice operation, as defined next.
  An important design choice here is that line 16 to 21 are executed atomically. Therefore, once V^* satisfies the equivalence quorum predicate for the first time, no other value is added to V^*.
  
   We call each execution of the Lattice(r) procedure as a lattice operation with tag r. A lattice operation is good if it returns true at line <ref>.
  
  
  LatticeRenewal(r): The LatticeRenewal(r) procedure is also given a parameter r. 
  It contains at most three lattice operations. If some lattice operation is good, it returns the view obtained by the good lattice operation, i.e., direct view. If the first two lattice operation are not good, then by definition, it means that node i has observed a larger tag, i.e., condition at line <ref> returns false. Therefore, node i initiates the next lattice operation with tag equal to maxTag.
  If the third lattice operation is also not good, then node i  waits for a goodLA message from some other node j to obtain a view from j's good lattice operation. In this case, the view is called an indirect view or a borrowed view. 
  
  It is fairly straightforward to see that our design satisfies the (P1) to (P3) stated earlier in Section <ref>. (P4) and the round complexity are less obvious, and depend on how we combine different components together.
  Both  and operations use the LatticeRenewal() procedure to obtain a view. This approach works owing to (P4).
  Intuitively, the moment that  and obtains a view is the synchronization point.
  
  
  
  Update(v): To write value v,  node i first obtains a tag by reading from at least n - f nodes. Let r denote the largest tag in the received readAck messages. Then, i constructs the timestamp of value v as the r + 1, i tuple. It sends value v with its timestamp to all nodes. Then, a lattice operation with tag r is invoked. This step is called the phase 0 lattice operation of the  operation.
  
  After the phase 0 lattice operation, the  obtains a new tag r' and executes LatticeRenewal(r').
  The view returned by LatticeRenewal(r') is not used; and hence discarded.
  Node i returns the ACK to complete the .
  
  In addition to the LatticeRenewal() procedure, another subtle point is to execute the phase 0 lattice operation before invoking LatticeRenewal().
  The way we devise them ensures that
  for each tag,
  there is a good lattice operation. Recall that a lattice operation is good if it returns true at line 17.
  Lemma <ref> presented later explains this statement in more details.
  
  
      
  Scan(): The code for a operation is quite simple. It first obtains a tag r similarly.
  Then, it executes the LatticeRenewal(r). After LatticeRenewal(r) returns a view scanView, the node takes the most recent value by each node in scanView by executing the extract(scanView) procedure.
  
  
  
  
  
  
  
  Message Handlers:  
  All the handlers execute in the background; hence, even if a node does not have a pending  or operation, it still processes messages. Moreover, all the handlers are executed atomically, i.e., during the period that a handler is executing, no other part of the code can take step. All the handlers should be clear from the code. One subtle part to note is that a node does not update its maxTag variable when it receives a value with a larger tag from a value message. The maxTag variable is only updated when a node receives a writeTag message or echoTag message. This design helps  achieve the desired round complexity. Especially, we rely on it to prove Lemma <ref>. For completeness, we also present detailed description of message handlers is in Appendix <ref>. 
  
  
  
  
  
  
  
      
  
      
  
      
  
      
  
      
  
  
  
  
  
  
  
  
  
   
  
  
  
  
  
  
  
   §.§ Proof of Correctness
  
  
  For correctness, we need to  prove termination and construct a linearizable sequence of  and operations for any execution. We first discuss important definitions and properties of our algorithm to facilitate the proof. Then, we prove termination and show the linearization construction.
  
  
  
  Useful Definitions: Tags and Views:  
  We say an  or is direct if its LatticeRenewal() procedure returns at line <ref>; otherwise, it is indirect. Intuitively, an operation is direct if it there is a good lattice operation during LatticeRenewal(). 
  
  We define the tag of an operation and value as following.
  
    The tag of an  or operation is the tag of its last lattice operation.
  
  
   The timestamp of a value is the r+1, i (tag-ID tuple) at line <ref> in the (v) procedure. The tag of a value is defined as the tag contained in its timestamp. For value v, we use ts_v to denote its timestamp.
  
  
  
  Now we introduce an important concept, view, that is used throughout our proof. 
  
  
   
  
  We define the views for a node and operations as below:
  
  
  
      
    * For a node i, its view is defined as the set V_i[i].
      
    * For a good lattice operation with tag T (Lattice(T)) at node i, its view is defined as the set of values with tag at most T in V_i[i] right after completing line <ref>, i.e., V_i[i]^≤ T.
      
    * For an  or operation, its view is defined as the set returned by its LatticeRenewal() procedure.
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  We present two lemmas on properties of the tags. Lemma <ref> follows directly from line <ref>.
  
   
  The tags of values are non-skipping, i.e., if there is a value with tag T ≥ 1, then there is also a value with tag T - 1. 
  
  
  
  
  
  
  
  The proof of the following lemma explains why we need the phase 0 lattice operation.
  
  
  
  
  
  lemmaconsecutiveGoodLA 
  If the largest tag in the system is T at time t, i.e., max_i ∈ [n] maxTag_i = T at time t, then for each 1 ≤ z ≤ T - 1, there is a good lattice operation with tag z before time t.
  
  
  
  To prove the lemma, we first prove the following claim. 
  
  
  
  If the largest tag in the system is T at time t, then there exists a good lattice operation with tag T - 1 that completes before t. 
  
  
  
  Observe that a value with tag T must be sent by some node, since we consider only crash failures. 
  Let node i be the first node that sends tag T to all other nodes inside the writeTag procedure in operation Op.
  Since Op is the first operation to send tag T, 
  Op must be an   operation. Let L_0 denote the phase 0 lattice operation inside Op. 
  When Op executes line <ref>, we have maxTag_i < T, 
  and r_i = T when line <ref> completes. This implies that r_i = T-1 at line <ref>.  Thus, the phase 0 lattice operation L_0 of Op at line <ref> must have tag T - 1.
  That is, node i invokes Lattice(T-1) as the phase 0 lattice operation.
  
  Since by assumption, Op is the first operation that proposes tag T and it proposes tag T after line <ref> (through the writeTag step at line <ref>), no node has proposed tag T before the execution of line <ref>.
  Hence, during the execution of the phase 0 lattice operation L_0 at line <ref>, we have maxTag_i ≤ T - 1 . Recall that the tag of L_0 is T - 1.  
  This implies that at line <ref> inside L_0, we have maxTag_i ≤ T-1 = r_i. 
  
  Thus, L_0 is a good lattice operation. Moreover, by assumption, L_0 completes before time t. This proves Claim <ref>.
  
  
  Since tags are non-skipping by Lemma <ref>, applying Claim  <ref> inductively gives us that for each 1 ≤ z ≤ T - 1, there exists a good lattice operation with tag r before time z.
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  Termination:  We show that each operation eventually terminates if each lattice operation terminates. We will show that each lattice operation takes O(√(k)) rounds later. 
  
  
  lemmaterminationASOLemma[Termination] 
  If each lattice operation eventually terminates, then  and operations in Algorithm <ref> eventually terminate.
  
  
  
  We show that each LatticeRenewal() eventually terminates. The only blocking part is line <ref>. Lemma <ref> implies that if a node observes a tag T, then it must be able to borrow a good view for some tag smaller than T. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  ++++++ Lewis: remove for the sake of space.
  
  Since the only blocking code that can prevent an operation from terminating is line <ref> in an  and line <ref> in a operation that calls LatticeRenewal(). 
  The only two return statements in LatticeRenewal() are on line numbers <ref> (if the call to the lattice operation is good) when termination is straightforward and line <ref> where termination is proved in Lemma <ref>. 
  
  ++++++++
  
  
  
  
  
  
  
  
  
  
  Useful Lemmas: Comparable Views:  
  Next we prove Invariant <ref>, which is formally stated in Lemma <ref>.
  
  lemmaviewFromGoodLattice 
  The view of each  or operation is the same as the view of some good lattice operation. 
  
  
  
  Similar to Lemma <ref>, we obtain the following lemma on the views (bounded by tag T) at node i and j due to our assumption on FIFO channel. Its proof is in Appendix <ref>.
  
  lemmacomparableTagViewsSameNode 
  For any two nodes i and j and tag T, fix any time t and t', the set V_i[s]^≤ T at time t and the set V_j[s]^≤ T at time t' are comparable for each node s.
  
  
  
  
  
  
  
  
  
  
  Next, we prove an important lemma which shows our key usage of lattice operation and the equivalence quorum technique. Lemma <ref> is a formal statement of Invariant <ref>. We put its full proof in Appendix <ref>.
  
  lemmalaComparableViews 
  The views returned by all good lattice operations are comparable. 
  
  
  For any two lattice operations Op_i and Op_j with tag T_i and T_j, if T_i = T_j, then Lemma <ref> and the equivalence quorum predicate imply that their views must be comparable. Otherwise, assume w.l.o.g T_i < T_j. Our algorithm guarantees that the view of Op_i must be a subset of the view of Op_j. Intuitively, the fact that Op_i does not observe T_j at line <ref> implies that Op_j must complete its line <ref> step after Op_i has completed. This ensures that Op_j must have received all values in the view of Op_i when Op_j starts line <ref>. 
  
  
  
  
  
  
  
  
      
  
  
      
  
  
  
      
  
      
  
  
          
  
          
  
          
  
          
  
  
  
          
  
  
  
  
  Lemma <ref> immediately follows from Lemma <ref>  and <ref>. Lemma <ref> allows us to construct a linearization of and  operations later. 
  
  
   
  The views returned by all  and operations are comparable. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  Useful Lemma: Visible Views:  
  To respect the atomicity semantics, we also need to ensure that (i) once an  is completed, then its value is visible to subsequent 's; and (ii) once a reads certain set of values, these values are also visible to subsequent 's. We prove these two through the usage of views and tags. 
  
  The lemma below is straightforward from the code. Refer Definition <ref> for view definition. 
  
  
  
  
  
   
  For a good lattice operation Op by node i with tag T, let H denote the view of node i right before Op execute  line <ref> and H_Op denote the view of Op. Then, H^≤ T⊆ H_Op. 
   
  
  The next lemma is the main reason that we need to have three lattice operations in the LatticeRenewal() procedure.
  
  lemmaoutputDomiInput
  
  Let Op be an  or operation by node i with tag T. Let H_Op denote its view. Let H denote the view of node i right before Op executes its LatticeRenewal() invocation. Then, H^≤ T⊆ H_Op. 
  
  
  
  We assume that Op is an  operation. The proof for the other case is similar. 
  If Op is an  with a direct view, the claim follows from Lemma <ref>, since by definition of a direct view, Op obtains a view from its good lattice operation.  
  Now, consider the case when Op completes with an indirect view. By construction,
  Op must continue to phase 3. Let R_1, R_2 and R_3 denote the tags for each of the three lattice operations in Op's invocation of LatticeRenewal(), respectively. Then, by Definition <ref>, T = R_3, the tag of the last lattice operation in Op.
  Moreover, Op must have received (goodLA, R_3) message 
  from some other node j. Let L_j denote this particular lattice operation by node j. By construction, L_j is a good lattice operation with tag R_3.  Then, we prove the following claim.
  
  
  
  Tag R_3 was not known by node i during its phase 1 lattice operation.
  
  
  
  First observe that R_1 < R_2 < R_3, since none of the lattice operation in i's LatticeRenewal() is good.
  The fact that Op obtains tag R_2 such that R_2 < R_3 during phase 2 implies that when Op completes its phase 1, it has not learned R_3; otherwise, it would not proceed to phase 2 with tag R_2, since R_2 < R_3.
  
  
  Let L_i denote the lattice operation by Op in phase 1 at node i. Consider the writeTag procedure in L_i and L_j. Let Q_i and Q_j denote the set of nodes that sent the writeAck messages in responding to the writeTag message of L_i and L_j, respectively. Since both set of nodes are of size at least n-f, there exists a nonfaulty node s ∈ Q_i ∩ Q_j such that node s must have received the writeTag message from L_j after sending writeAck message in responding to the writeTag message of L_i. Otherwise, Op would obtain tag R_3 for phase 2, a contradiction to Claim <ref>. 
  
  
  
  Since communication is reliable and FIFO, and node i sends all values in H before sending the writeTag message in lattice operation L_i, node s must receive all values in H and sends out to all other nodes before sending the writeAck message in responding to the writeTag message of L_j. Thus, node j must have received all values in H before it completes line <ref> of L_j.
  
  Let H_j denote the view of lattice operation L_j. Since L_j is a good lattice operation, Lemma <ref> implies that H^≤ R_3⊆ H_j. 
  
  
  By assumption, node i borrows j's view after it has received the (goodLA, R3) at line <ref>. Thus, H_j ⊆ H_Op. Therefore, H^≤ R_3 = H^≤ T⊆ H_j ⊆ H_Op. 
  
  
  
  
  
  
  The above lemma immediately implies that the value of an  operation must belong to the view obtained by the  operation. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  Following the convention, we say that Op → Op' iff the response (or completion) time of Op occurs before the invocation time of Op'. The following Lemma immediately follows from the usage of writeTag and readTag procedures.
  
   
  For any two operations Op_i with tag T_i and Op_j with tag T_j, respectively. If Op_i → Op_j, then T_i ≤ T_j. 
  
  
  
  
  
  
  Now we prove the important lemma on views being “visible” to subsequent operations.
  
  lemmaviewOrder 
  For any two operations Op_i of node i and Op_j of node j with views H_i and H_j, respectively. If Op_i → Op_j, then H_i ⊆ H_j. 
  
  
  Let T_i and T_j denote the tag of Op_i and Op_j, respectively. 
  Consider the following two cases. 
  Let H denote the view of node j right before Op_j invokes LatticeRenewal(). Lemma <ref> implies that H^≤ T_j⊆ H_j. To prove the lemma, we need to show that H_i ⊆ H^≤ T_j. 
  
  
      
    * Case 1: Op_i obtains a direct view. 
      
      Consider Op_i's last lattice operation L_i. Then L_i is a good lattice operation with tag T_i. By definition, H_i is also the view of L_i. 
      Let Q_i denote the equivalence quorum for L_i. Then, we have H_i = V_i[w]^≤ T_i⊆ V_w[w]^≤ T_i for each node w ∈ Q_i when L_i completes. Let Q_j denote the set of nodes which send readAck for the first readTag message of Op_j. Since Op_j starts after Op_i completes, there exists a nonfaulty node s ∈ Q_i ∩ Q_j such that node s sends out all the values in its current view, which must include all the values in H_i, to all the other nodes before sending the readAck message for Op_j's first readTag message. By FIFO channels, node j must have received all the values in H_i before it completes the writeTag procedure of Op_j. Lemma <ref> implies that T_j ≥ T_i. This together with the observation that the largest tag in H_i is T_i,  we have H_i ⊆ H^≤ T_j. 
      
      
      
      
      
    * Case 2: Op_i obtains an indirect view. 
      
      The view H_i of Op_i is the same as the view of some good lattice operation L and Op_i must have received the goodLA message sent by L. Thus, when Op_i completes, L have completed its execution of line <ref>. Then, by a similar argument in case 1, H_i ⊆ H^≤ T_j.
  
  
  
  
  
  Construction of a linearization:  
  
  For a given execution, we construct a sequence σ of all  and operations in the execution such that σ preserves the semantics of atomic snapshot object. The construction is similar to one from <cit.>, and presented below.
  
  
      
    * Insert operations: First, we construct a sequence σ' which includes all operations. The operations are ordered in σ' according to the order of their associated views. Specifically, for any two operations Sc_i and Sc_j that have view H_i and H_j, respectively, if H_i < H_j, then Sc_i appears before Sc_j in σ'. If H_i = H_j and Sc_i → Sc_j, then Sc_i appears before Sc_j in σ'. Otherwise, Sc_i and Sc_j are ordered arbitrarily. 
      
      
    * Insert  operations:
      Second,
      we insert all  operations into σ'. Consider an  operation Op that writes v with timestamp ts_v. We insert Op after all operations whose view do not include v, ts_v and before all operations whose view contains v, ts. That is, Op is inserted just before the first operation in σ' such that its view contains v, ts. For any two  operations Op_1 and Op_2 that fit between the same pair of operations. If Op_1 → Op_2, then we insert Op_1 before Op_2 in sequence σ. Otherwise, Op_1 and Op_2 are ordered arbitrarily. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
     
  
      
  
     
  
      
  
      
  
      
  
  
  
  
  Similar to the proof given in <cit.>, the proof of the following theorem uses Lemma <ref>.  <ref> and <ref> to show that σ is a linearizable sequence. We put it in Appendix <ref>
  
  theoremmainTheoremASO 
   (Algorithm <ref>) implements an atomic snapshot object.
  
  
  
  
  
  
  
   §.§ Round Complexity
   
  
  
  
  
  
  Now we analyze the round complexity of our algorithm. We assume the local computation time is negligible compared with the message delay. 
  We show that each lattice operation takes O(√(k)) rounds. The proofs of the two lemmas below are in Appendix <ref> and <ref>.
  
  
  lemmalaterOperationBiggerTag  
  Suppose there exists a lattice operation that starts at time t with tag T, then any  operation starting after time t + D must assign a tag > T for its value.  Thus, all values with tags at most T must have been sent out by time t + D. 
  
  
  
  
  
  lemmaknownToAllAfterD 
  Let Op denote (v) operation. If Op completes before time t, then for each nonfaulty node i, v, ts_v ∈ V_i[j] for each nonfaulty node j by the end of time t + 2D. 
  
  
  
  
  
  
  Recall that the exposed value is introduced in Definition <ref>. 
  
  lemmaroundComplexityASO 
  Each lattice operation takes O(√(k)) message delays in the worst case. 
  
  
  Let L_i be a lattice operation at node i. 
  Suppose L_i starts at time t with tag T. According to the condition at line <ref>, the termination of L_i only depends on values with tags at most T.  Thus, we do not need to consider the values from  operations that start after time t + D by Lemma <ref>. That is, for the termination of L_i, we only need to consider  operations that start before time t + D.  Now, we prove an important claim.
  
  
  
  There are at most k exposed values with tag ≤ T in intervals after time t + 4D.
  
  
  By Lemma <ref>, all values with tags at most T from  operations that have completed before t + D must be contained in V_i[j] for each pair of nonfaulty nodes i and j by time t + 3D, i.e., known by all nonfaulty nodes. Thus, by definition of the exposed values, we have that values from  operations that have completed before time t + D cannot be exposed values in intervals after time t + 3D. Since the values from  operations that start after time t + D must have tag greater than T, only values from  operations that start before time t + D and have not completed by time t + D can be exposed values in intervals after time t + 3D. 
  Let U denote the set of these values.
  Moreover, by definition, there can at most one such  operation per node. 
  
  
  Consider an arbitrary value v ∈ U and the (v) operation. We show that if (v) is from a nonfaulty node, then value v cannot be an exposed value for intervals after time t + 3D. Consider lines <ref> to <ref> of (v), since local computation takes negligible time, and line <ref> takes at most 2D time, value v must be sent to all other nodes at line <ref> before time t + 3D. Thus, by time t + 4D, value v must be known by all nodes that have not crashed at this time, including all the nonfaulty nodes. Therefore, v cannot be an exposed value in intervals after time t + 4D. 
  Thus, a value in v ∈ U can be an exposed value for intervals after time t + 4D iff (v) is from a faulty node. This proves the claim. 
  
  
  
  The above Claim implies that after time t + 4D, if we only consider values with tag at most T, Lemma <ref>, <ref> and <ref> still hold. Thus, similar to the proof in Lemma <ref>, l_p must terminate in O(√(k)) rounds.
  
  
  
  The proof of Claim <ref> also explains why we need to put line <ref> before the initial lattice operation at line <ref>. If we switch the order of line <ref> and line <ref>, then we cannot guarantee that value v is sent to all the other nodes before time t + 3D, even though (v) starts before time t + D. 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
   
  
  
  
  
  
  
  
  
  
  
  
  § LINEARIZABLE UPDATE-QUERY STATE MACHINES
   
  In this section, we show how to implement a linearizable update-query state machine using our atomic snapshot algorithm. A update-query state machine only supports two types of operations: update and query. It does not support update and query mixed operations. It also assume that all updates are commutable, so the order of updates does not matter. Many data structures such as sets,
  sequences, certain types of key-value tables, and graphs <cit.>
  can be designed with commuting updates. 
  
  The implementation, shown in Algorithm <ref>, is almost same as the atomic snapshot implementation in Algorithm <ref>, except that we let the operation return its view, i.e., the set obtained at line <ref>. The view is a set of update commands from clients. Each element in the vector V_p is a command. For an update command up from a client, node p invokes (up). When receiving a query command from a client, node p invokes the modified () to return a set of commands and then apply these commands and return responses accordingly. 
  
  [!hptb]
  
  Linearizable UQ State Machines
  
  
  
  The following theorem implies that each command takes O(1) rounds if there is no crash fault. O(1) message size overhead means that if we assume that the size of each command is O(1), then each message in the implementation has size O(1). 
  
  
  There exists an implementation of linearizable update/query state machines such that each command takes O(√(k)) message delays and O(1) message size overhead, where k is the actual number of crash failures in the system. 
  
  
  
  
  § PROOFS FOR THE ELA ALGORITHM
   
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
  The value of set V_i[s] is modified only when i receives a message from node s. Since s is a non-faulty node and the communication is FIFO, the set V_i[s] at time t must be the same as the set V_s[s] at some time t_i and the set V_j[s] at time t' must be the same as the set V_s[s] at some time t_j. The set V_s[s] is non-decreasing. Thus, V_i[s] at time t must be comparable with V_j[s] at time t'. 
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
  Let V_i denote the vector at node i and V_j denote the vector at node j when nodes i and j decide. The statement of the lemma is proved if we show that V_i[i] and V_j[j] are comparable. 
  
  The decision condition on line <ref> states that there exists a set Q_i of size at least n - f such that V_i[i] = V_i[s] for each s ∈ Q_i and a set Q_j of size at least n - f such that V_j[j] = V_j[s] for each s ∈ Q_j. Since f < n/2, there exists a correct process s ∈ Q_i ∩ Q_j. Lemma <ref> implies that V_i[s] and V_j[s] are comparable. This leads to the conclusion that V_i[i] (which is equal to V_i[s]) is comparable to V_j[j] (which is equal to V_j[s])
  
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  *
  
  
  Let C denote the set of correct nodes in an execution. Let node i be an undecided node at time t that does not crash by t+2D.
  We show that by time t+2D, we have V_i[j] = V_i[i] for each j ∈ C.
  As a result, the predicate  at line number <ref> becomes true, and node i decides at Line <ref>.
  
  Proof by contradiction. Suppose there exists a value v ∈ V_i[i] - V_i[j] at time t+2D. Since by assumption, value v is not an exposed value in this interval, it must be received by some correct node s (or it is the input value of node s) at some time t_s < t.
  Thus, value v must be sent to all by node s at time t_s and received by all correct nodes  
  by time t_s+D < t+D, including node j. By the algorithm, node j must send value v to all the other nodes before time t+D. 
  Thus, node i must receive value v from node j by  
   time t+2D, and add v into V_i[i] and V_i[j], a contradiction to the assumption that v ∈ V_i[i] - V_i[j].   
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
   Recall the definition of an exposed value v occurring in an interval 
   (t,t+D]: there has to be a failure chain ending with a correct process that receives value v in interval (t, t + D]. Let p_1,⋯,p_m-1, p_m denote such a failure chain for value v, where p_1⋯ p_m-1 are faulty and node p_m is non-faulty. 
  
  
  
  
  Assume by contradiction that the length of this failure chain is l ≤t/D. Since D is the message delay in the execution, node p_i (in the failure chain) hears about v at time t_i ≤ i· D. Thus if l ≤t/D, the correct node p_m hears about v at time t_m ≤t/D· D = t making v an exposed value occurring in an interval prior to (t,t+D). This contradicts the assumption in the statement of the lemma that v is an exposed value in interval (t,t+D].
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
  Let V and U denote the set of the first |P_v| - 2 nodes in P_v and the first |P_u| - 2 nodes in P_u. Suppose node i ∈ V ∩ U for contradiction. By condition (iv) of Definition <ref>, node i crashes while sending v to other nodes on line <ref> of ELA. Since lines <ref> to <ref> of ELA are executed atomically, node i cannot crash while sending value u to other nodes at line <ref>, a contradiction. 
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
  Let us assume that the algorithm takes 2 √(k) + 1 rounds for contradiction. By Lemma <ref>,  we know that to prevent the algorithm from terminating, there has to be at least one exposed value every two rounds. Lemma <ref> gives us the length of any failure chain and Lemma <ref> states that a faulty node (except for the last 2 nodes in a failure chain) can be a part of only one failure chain. 
  
  Thus if the algorithm terminates in round 2 √(k) + 1,  the number of faulty nodes
  must be at least 1 + 3 + … + 2√(k) - 1 > k, leading to a contradiction. 
  
  
  
  
  § GENERAL TRANSFORMATION IN MESSAGE PASSING SYSTEMS
   
  
  In this section, we show how to adapt the transformation given by Attiya et al. in <cit.> for shared memory systems to work in message passing systems. The transformation algorithm, TS-ASO, is shown in Algorithm <ref>. 
  
  In the algorithm, each node p keeps track of a vector Snap of size n, which is the local view  of the shared object, i.e., Snap[q] stores the most recent value written by node q known by node p. The variable V is a map from tag number to snapshot. V[r] is the snapshot vector obtained for tag r. Variable r denotes the tag number of the last lattice agreement instance that node p has completed. maxTag keeps track of the largest tag ever seen by a node. ts is a sequence number for values, which is increased by one when a new value needs to be written. Each value is associated with a timestamp. For any value v, we use ts_v to denote its associated timestamp. If a variable belongs to node i, we use the subscript i to denote it. For example, maxTag_i denotes the value of variable maxTag at node i. 
  
  Scan() operation: a operation invokes at most two lattice operations to obtain a view. We call the two for loops as its two phases. At each phase, it first decides which lattice agreement instance to run by reading the largest tag from at least n - f nodes at line <ref>. Then, it writes the tag obtained to at least n - f nodes at line <ref>. At line <ref>, it reads the local state from at least n - f nodes and the join of all states received will be used as input for its lattice agreement. At line <ref>, it writes the join of all states read at line <ref> to at least n - f nodes. Then, it invokes the lattice agreement instance with the tag obtained at line <ref> and the vector obtained at line <ref> as input parameters. After completion of the lattice agreement, if it does not observe a higher tag number, then it directly returns the view obtained from its lattice agreement invocation. If it does not return a view after lattice agreement invocation, it borrows a view from some other node, which is guaranteed to exist. 
  
  Update(v) operation: To write value v, node p increases ts_p by one and assign it to be the timestamp of v. It writes value v with its timestamp to at least n - f nodes. Then, it executes a operation. The view returned by the operation is not used. The operation acts as a synchronization point.  
      
  
  
  [!hptb]
  
  TS-ASO: code for node p.
  
  
  
  
  
   §.§ Proof of Correctness
   
  In this section, we show that atomic object implementation is linearizable by explicitly constructing a linearization of all update and scan operations. We can first obtain the following lemma regarding to the views returned by all operations. We say a view returned by an operation is a direct view if this view is returned in the first phase of the scan procedure. Otherwise, we call this view as an indirect view. We can readily see that a direct view of p_i is obtained from an execution of lattice agreement of p_i. An indirect view of node i is direct view of some other node j. We call an invocation of a lattice agreement with tag r as a lattice operation with tag r. 
  
  
   
  Consider a lattice operation op by node p with tag r, suppose op returns V_op at time t. Then, for each j, there exists a set of nodes Q_j with size at least n - f such that V_op[j] ≤ Snap_i[j] for each i ∈ Q_j at time t. 
  
  Let P denote the set of nodes which invokes the lattice operation op before or at time t. By Upward-Validity, we have that V_op[j] = input_p[j] for some node p ∈ P. By line <ref>, there exists a set of nodes Q_j with size at least n - f such that input_p ≤ Snap_q for each i ∈ Q_j. Therefore, V_op[j] = input_p[j] ≤ Snap_i[j] for any i ∈ Q_j.  
  
  
  
  
  If two operations return view_i and view_j, then view_i and view_j are comparable. 
  
  We only need to show that view_i and view_j are comparable if they are direct views. Let op_i and op_j denote the two operations that return view_i and view_j, respectively. We have the following cases. 
  
  Case 1. view_i and view_j are obtained from the same lattice operation. By comparability of lattice agreement, view_i and view_j are comparable. 
  
  Case 2. view_i are obtained from lattice operation with tag r_i and view_j is obtained from lattice operation with round r_j. Assume that r_j > r_i, w.l.o.g. Assume that op_i obtains view_i in first phase. The case that op_i returns view_i in second phase is symmetric. Then, in line op_i finds no nodes with tag number greater than r_i. Therefore, op_i obtains view_i before op_j completes line <ref>. Then, when op_j starts to read states of at least n - f nodes at line <ref>, it must be able to read view_i[j] for each j, by Lemma <ref> and quorum intersection. Thus, view_i is less that or equal to the input of op_j for the lattice operation with tag r_j. By Downward-Validity of lattice agreement, we have view_i ≤ view_j. 
   
  
  
  
  Now, we associate an view with the beginning of an operation. For operation op, the view associated with the beginning of op is view view' such that view'[j] is the largest value written by p_j which is contained in the local state of at least n - f nodes. 
  
    
  Assume operation op returns view and let view' denote the view associated with the beginning of op, then view' ≤ view.
  
  Consider the following two cases. 
  
  Case 1. op return view directly from lattice operation with tag r. W.l.o.g, assume that op returns view in the first phase. The case where op returns view in the second phase is symmetric. Let input denote the input of op for the lattice operation with tag r at line <ref>. By definition of view', when op executes line <ref>, it must be able to read all values in view'. Since nodes write increasing values to the snapshot object, view' ≤ input. By Downward-Validity of lattice agreement, we have input ≤ view. Thus, view' ≤ view. 
  
  Case 2. op returns view indirectly. Then, op must continue to phase 2. Let r_1 and r_2 denote the tag number op obtains at line <ref> of phase 1 and phase 2, respectively. We have r_1 < r_2. Consider the second phase, the condition at line <ref> is satisfied and op borrows a view of some other nodes for tag r_2. view must be a direct view of some operation op' for tag r_2. W.l.o.g, assume that op' returns view in the first phase. The case where op' returns view in the second phase is symmetric. Since r_1 < r_2, op' must start line <ref> after op starts. Otherwise, op would obtain tag number r_2 instead of r_1 for its first phase. By the definition of the view associated with an operation, op' must be able to read all values in view' at line <ref>. Downward-Validity of lattice agreement implies that view' ≤ view. 
  
  
  
  
  Consider two operations op_i and op_j that return view_i and view_j, respectively. If op_i → op_j, then view_i ≤ view_j. 
  
  
  Let view be the view associated with the beginning of op_j. By Lemma <ref>, view ≤ view_j. Since op_i obtains view_i before the beginning of op_j, Lemma <ref> implies that view_i ≤ view. Thus, view_i ≤ view_j. 
  
  
  
  
  Let up be an  operation by node p that writes value v, and returns view_p. Then, v, ts_v≤ view_p[p].
  
  Let view be the view associated with the beginning of the operation embedded in up. Since up writes v, ts_v to at least n - f nodes before its embedded operation, then v, ts≤ view[p]. By Lemma <ref>, we have view ≤ view_p. Thus, v, ts_v≤ view_p[p].  
  
  
  
  The linearization sequence of the scan and update operations is constructed in the same way as the one given in <cit.>. First, we construct a sequence σ' which only includes all scan operations. The sequence also includes the scan operations embedded in the update operations. The scan operations are ordered in σ' according to the order of the views returned by them. Specifically, for any two scan operations sc_i and sc_j that return view_i and view_j, respectively, if view_i < view_j, then sc_i appears before sc_j in σ'. If view_i = view_j and sc_i → sc_j, then sc_i appears before sc_j in σ'. Otherwise, sc_i and sc_j are ordered arbitrarily. 
  
  Now we create a linearization sequence σ from σ' by inserting all update operations into σ'. Consider an operation op_i that writes value v. We insert op after all scan operations that return a value strictly smaller than v and before all scan operations that return a value greater than or equal to v. That is, op is inserted  just before the first scan operation that returns a view which contains v. For any two operations op_1 and op_2 that fit between the same pair of scan operations. If op_1 → op_2, then we put op_1 before op_2 in sequence σ. Otherwise, op_1 and op_2 are ordered arbitrarily. 
  
  As long as we have the above lemmas, the proof which shows that σ is a linearization is the same as the proof in <cit.>. 
  
  
  There exists an atomic snapshot object implementation in asynchronous crash-prone message passing systems, which requires O(log n) message delays per update or scan operation, where f < n/2 is the maximum number of crash failures in the system. 
  The paper <cit.> presents an O(log f) rounds algorithm for the lattice agreement problem in asynchronous crash-prone message passing systems. Directly plugging in their algorithm into our transformation result in O(n) rounds complexity for update and scan operations, since their algorithm requires all nodes to start around the same time. Their algorithm can be simply modified to run in O(log n) rounds even if nodes start at different times. 
  
  
  
  
  
  § COMPARISON BETWEEN TS-ASO AND AC-ASO
   
  Let TS-ASO denote the general transformation in Appendix <ref>. We list the two primary differences between TS-ASO and AC-ASO here. 
  
  1) In both TS-ASO and AC-ASO, to write a new value (in an  operation), a node needs to first read the largest tag from a quorum of nodes. Let r denote the tag obtained. In TS-ASO, a node directly participates in the lattice operation with tag r (This design ensures that there is good lattice operation for each tag). This design is also the main reason why TS-ASO cannot preserve the round complexity of our ELA algorithm, since the round complexity of our ELA algorithm depends on the assumption that each node starts the algorithm around the same time and nodes can join the lattice operation with the same tag at quite different times. To solve this problem, our idea is to let a node participate a lattice operation with a strictly greater tag than the tag it reads from a quorum. That is, if a node observes a tag r, then it participates the lattice operation with tag r + 1. This ensures that all nodes participate the lattice operation with same tag around the same time (at most constant round apart). If we only have the above modification, we cannot guarantee that there exists a good lattice operation for each tag, then when some lattice operation needs to borrow a view from a good lattice operation, the existence of such a good lattice operation is not guaranteed. Thus, to tackle this problem, our idea is to use a dummy lattice operation whose only purpose is to ensure the existence of a good lattice operation for each tag. Specifically, we let each  operation executes an initial lattice operation with tag r but without introducing a new value with tag r. This initial lattice operation guarantees the existence of a good lattice operation for each tag but does not prevent the termination of existing lattice operations with the same tag due to the reason below. Our lattice operation has the following properties: the termination of a lattice operation with tag T depends on only the values with tags at most T. Since the initial lattice operation with tag r does not introduce a new value with tag r, it does not prevent progress of other existing lattice operations with tag at most r. This is also the reason why our design is not a general transformation that preserves the round complexity of any lattice agreement algorithm. 
  
  2) In TS-ASO, before participating a lattice operation, a node needs to collect the states of at least a quorum of nodes and use their join as input for the lattice operation. In TS-ASO, such a read step is important in ensuring the correctness. (First, it ensures that a lattice operation with a bigger tag must be able to read the view obtained by a lattice operation with a smaller tag. Second, it ensures that a later  or operation must be able to read the view obtained by previous (completed)  or operation.) Each state read from other nodes is a vector of n values. Thus, each message in the lattice operation has O(n) overhead in size (it contains at least n values). In our design, we would like to remove such overhead in message size. Note that our ELA algorithm has constant message size overhead. In AC-ASO, when a node participates a lattice operation, it does not collect the states of at least a quorum of nodes and use that as input for lattice operation. Without the reading step, two lattice operations are not sufficient to guarantee correctness. To ensure correctness, we will show that three lattice operations are sufficient. 
  
  
  
  § PROOFS FOR THE  ALGORITHM
   
   
  
  
   §.§ Mesage Handlers of 
   
  
  
  
  
      
    * Upon receiving a writeTag message: node i updates its maxTag to be the maximum of its current maxTag and the received tag. Then, it responds a writeAck. 
      
      
      
      
    * Upon receiving a echoTag message: node i updates its maxTag to be the maximum of its current maxTag and the received tag. 
      
      
    * Upon receiving a value message from node j: node i adds the value into V_i[i] and V_i[j]. It then forwards this value to all other nodes if it has never done so before. It is important to note that a node does not update its maxTag variable when it receives a value with a larger tag from a value message. The maxtTag variable is only updated when a node receives a writeTag message or echoTag message. 
      
      
    * Upon receiving a readTag message: node i responds a readAck message along with the largest tag it has ever seen via writeTag messages. 
      
      
    * Upon receiving a goodLA message with tag r from node j: node i borrows the view from node j by recording V_i[j]^≤ r. Our design ensures that the borrowed view is identical to the view from j's good lattice operation.
      By assumption the communication is FIFO, and node j sends the message (goodLA, r) right after its view satisfies the equivalence predicate at line <ref>; thus, V_i[j]^≤ r must be the same as the view of the particular good lattice operation at node j. We formally prove this claim in Lemma <ref>.
  
  
  
  
  
  
   §.§ Proof of Lemma <ref>
   
  
  *
  
  
  We show that each LatticeRenewal() invocation terminates. 
  Let Op denote the LatticeRenewal() procedure at node i. 
  We only need to show that the condition at line <ref> is eventually satisfied if Op has not returned earlier, since the condition is the only blocking code inside Op. Consider the phse 3 lattice operation L_3. Since Op continues to line <ref> with phase = 3, L_3 is not a good lattice operation. This means that the for loop of Op breaks at line <ref>; hence, r_i at line <ref> is equal to the tag used by L_3. Since L_3 is not a good lattice operation, and it returns false, we have maxTag_i > r_i at line <ref>. In other words, at this point of time, the largest tag in the system is at least maxTag_i. Lemma <ref> implies that a good lattice operation with tag r_i must be completed before L_3 executes line <ref>. By assumption of the reliable communication channel, node i is able to receive a (completed, r_i) message from the good lattice operation.
  After receiving the message, condition at line <ref> is satisfied, and hence, LatticeRenewal() terminates.
  
  
  
  
   §.§ Proof of Lemma <ref>
   
  
  *
  
  
  If the operation is direct, then by definition, its view is the view of its final lattice operation in LatticeRenewal() procedure. Otherwise, the operation borrows the view from some other node j at line <ref>, which must be the view of j's good lattice operation. This is because only a good lattice operation sends a goodLA message. 
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
  
  The value of set V_i[s]^≤ T is modified only when i receives a new value with tag ≤ T from node s. Since the communication is FIFO, the set V_i[s]^≤ T at time t must be the same as the set V_s[s]^≤ T at some time t_i and the set V_j[s]^≤ T at time t' must be the same as the set V_s[s]^≤ T at some time t_j. The set V_s[s]^≤ T is non-decreasing. Thus, V_i[s]^≤ T at time t must be comparable with V_j[s]^≤ T at time t'. 
  
  
  
  
  
  
  
  
  
  
  
  
   §.§ Proof of Lemma <ref>
   
  
  *
  
  
  Consider two good lattice operations Op_i with tag T_i by node i  and Op_j with tag T_j by node j. Let H_i and H_j denote node i and j's view, respectively, after they complete line <ref>. Recall that by Definition <ref>, H_i = V_i^* = V_i[i]^≤ T_i and H_j = V_j^* = V_j[j]^≤ T_j right after the equivalence quorum predicate is satisfied.
  
  To prove the lemma, we need to show that either H_i ⊆ H_j or H_j ⊆ H_i. Assume without loss of generality T_i ≤ T_j. Then consider two following cases. 
  
      
    * Case 1: T_i = T_j = T. 
      Intuitively, both nodes participate in the same instance of lattice agreement, and thus, they will obtain  comparable outputs (views).
      
      Formally, 
      let W_i and W_j denote the equivalence quorum of lattice operation Op_i and Op_j, respectively. Thus, there exists a nonfaulty node s ∈ W_i ∩ W_j such that H_i = V_i[i]^≤ T = V_i[s]^≤ T and H_j = V_j[j]^≤ T = V_j[s]^≤ T. Lemma <ref> implies that V_i[s]^≤ T and V_j[s]^≤ T are comparable. Thus, H_i must be comparable with H_j, since to satisfy the equivalence quorum predicate, H_i = V_i[i]^≤ T = V_i[s]^≤ T and H_j = V_j[j]^≤ T = V_j[s]^≤ T.
      
      
    * Case 2: T_i < T_j. In this case, we show that H_i ⊆ H_j.
      Roughly speaking, we want to show that lattice operation with a larger tag start with a view that is  at least as large as the view of any lattice operation with a smaller tag.
      we rely on Property 2 of LatticeRenewal() and the way we update maxTag's to prove the claim. 
      
      We make the following observations:
      
      
          
    * Obs. 1: the tag T_j is not known by node i when Op_i completes line <ref>.
          
          This is because (i) Op_i is a good lattice operation, and the condition maxTag_i ≤ r_i at line <ref> of Op_i must return true; and (ii) line <ref> and <ref> are executed atomically, and hence V_i^* = V_i[i]^≤ T_i does not change during this block of code. 
  
          
          
    * Obs. 2: There exists a node s such that H_i ⊆ V_s[s]^≤ T_i and V_s[s]^≤ T_i⊆ V_j[j]^≤ T_j.
          
          Let W_i denote the equivalence quorum of Op_i. Let Q_j denote the set of at least n - f nodes that sent the writeAck messages in responding to the writeTag message of Op_j. Since both set are of size at least n-f, there exists a node s ∈ W_i ∩ Q_j such that (i) H_i = V_i^* =  V_i[s]^≤ T_i (due to the equivalence predicate); and (ii) node s ∈ Q_j. 
          
          By Obs. 1, and the assumption of FIFO communication, node s must have received all values in V_i[s]^≤ T_i before receiving the writeTag message of Op_j. Otherwise, Op_i would observe tag T_j at line <ref>.  
          
          Thus, node s must send out all values in V_i[s]^≤ T_i to all before sending writeAck for the writeTag message of op_j. Then, when node j receives the writeAck from node s, it must also receive all values in V_i[s]^≤ T_i, i.e., the view of node j contains all values in V_i[s]^≤ T_i after line <ref> of op_j completes. Since H_j is the set of values with tag at most T_j > T_i in the history of node j when op_j completes line <ref>,  V_i[s]^≤ T_i⊆ H_j. Therefore, H_i ⊆ H_j.
          
          
      
      
      
      
      
      
      
      
     
  
  
  
  
  
   §.§ Proof of Theorem <ref>
    
  
  We first show the following two lemmas. 
  
  lemmasemanticsASO 
  
  The sequence σ preserves the semantics of atomic snapshot object, i.e., for any operation which returns Snap, for any i, Snap[i] must be the value written by the latest  operation of node i that appears before the operation in σ. 
  
  
  
  Assume Snap[i] = v, and let op be the (v) operation by node i. By the construction of σ, op appears before sc in σ. First, we have that any  operation by node i that writes a value strictly greater than v is ordered after sc in σ. Furthermore, any  operation by node i that writes a value strictly smaller than v is ordered before op in σ. Therefore, op is the last  operation by node i that is ordered before .
  
  
  The following lemma is implied by Lemma <ref>. 
  lemmadownwardValidity 
  Let Op be an  operation by node i that writes value v with timestamp ts and has view H_i. Then, v, ts ∈ H_i.
  
  
  lemmarealTimeOrder 
  The sequence σ respects the real-time order of operations, i.e., for any two operations Op_i and Op_j, if Op_i → Op_j, then Op_i appears before Op_j in σ.
  
  
  
  
  Let H_i and H_j be the views of op_i and op_j, respectively. Let node i and node j denote the nodes where op_i and op_j take place, respectively. Note that i may be equal to j. By Lemma <ref>, we have H_i ⊆ H_j. 
  We consider the following cases. 
  
  
      
    op_i= (v) and op_j= (u): 
     If op_i and op_j are placed between the same pair of operations, then they are ordered according to →. Hence, op_i appears before op_j in σ. Otherwise, there exists a operation sc with view H_sc between op_i and op_j in σ. Suppose, by way of contradiction, that op_j is ordered before op_i. In other words, sc appears after op_j and appears before op_i in σ. Then v, ts_v ∉H_sc and u, ts_u ∈ H_sc. Lemma <ref> implies that v, ts_v ∈ H_i. On the other hand, since op_i → op_j, we have u, ts_u ∉H_i. Thus,  H_sc and H_i are incomparable, a contradiction to Lemma <ref>.
     
      
    op_i= (v) and op_j= : 
      
      Lemma <ref> and Lemma <ref> together imply that v, ts_v∈ H_i ⊆ H_j. Thus, op_i must be ordered before op_j in σ. 
     
      
    op_i= and op_j= :
      
      If H_i ≠ H_j, which means H_i ⊂ H_j. In this case, op_i is ordered before op_j by construction. Otherwise, since two operations that return the same view are ordered according to →, op_i is ordered before op_j in σ. 
      
      
    op_i= and op_j= (v):
      
      Clearly, v, ts_v ∉H_i. Since op_j is ordered after all operations whose view does not contain v, ts_v, it follows that op_i appears before op_j in σ. 
  
  
  
  *
  
  
  Immediately follows from Lemma <ref> and <ref>. 
  
  
  
  
  
  
      
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  	
  
      
  
      
  
  
      
  
      
  
      
  
      
  
  
      
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  	
  
      
  
      
  
  
      
  
      
  
      
  
      
  
  
      
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
   §.§ Proof of Lemma <ref>
    
  
  *
  
  
  Let operation op denote such a lattice operation. Since op sends its tag T to all in the writeTag function at line 28, by time t + D, each correct node must have received tag T. Thus, any  operation that starts after time t + D must obtain a tag greater than T for its value. Thus, all values with tags at most T must come from  operations that start before time t + D. Since local computation does not take time, all such values must be sent out at line <ref> before time t + D. 
  
  
  
  
   §.§ Proof of Lemma <ref>
   
  
  *
  
  
  Since op completes before time t, v, ts_v must be sent to node q before time t and must be received by node q by time t + D. Thus, node p must receive v, ts_v from node q by the end of t+ 2D. 
  
  
  
  
  
  