Resolving Conflicts with Grace: Dynamically Concurrent Universality

Kuznetsov, Petr; Schrodt, Nathan Josia

doi:10.4230/LIPIcs.OPODIS.2025.33

Resolving Conflicts with Grace:
Dynamically Concurrent Universality

Petr Kuznetsov

LTCI, Télécom Paris, Institut Polytechnique de Paris, France Nathan Josia Schrodt

Télécom Paris, Institut Polytechnique de Paris, France
Technical University of Darmstadt, Germany

Abstract

Synchronization is the major obstacle to scalability in distributed computing. Concurrent operations on the shared data engage in synchronization when they encounter a conflict, i.e., their effects depend on the order in which they are applied. Ideally, one would like to detect conflicts in a dynamic manner, i.e., adjusting to the current system state. Indeed, it is very common that two concurrent operations conflict only in some rarely occurring states. In this paper, we define the notion of dynamic concurrency: an operation employs strong synchronization primitives only if it has to arbitrate with concurrent operations, given the current system state. We then present a dynamically concurrent universal construction.

Keywords and phrases:

Universal Construction, Consensus, Dynamic Concurrency

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Distributed algorithms

DOI:

10.4230/LIPIcs.OPODIS.2025.33

Event:

29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Editors:

Andrei Arusoaie, Emanuel Onica, Michael Spear, and Sara Tucci-Piergiovanni

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

When we design a distributed system that enables concurrent access to the shared data, we often have to face our main nemesis – synchronization. It is common that concurrent operations affect one another and, thus, cannot be executed in parallel; we say that the operations encounter a conflict. Potential conflicts are typically anticipated and resolved using consensus [10]. The processes agree on the order in which the operations are applied, as in the celebrated universal construction by Herlihy [15].

As consensus is perceived an expensive tool, a lot of efforts were invested in optimistic algorithms that avoid consensus-based synchronization in good scenarios, in particular when no contention is encountered, i.e., when an operation runs in isolation [23, 16, 4]. A step further in this direction is to avoid using consensus in the absence of conflicts, even when operations contend. Indeed, one can come up with a universal construction in which concurrent operations that do not conflict are executed in parallel without engaging in consensus to decide on their execution order [24, 6].

However, conflicts are treated here in a conservative way: two operations are considered conflicting if they do not commute in some state (but might commute in another). This can result in very inefficient implementations. Indeed, many data structures exhibit conflicts rarely, only in certain states. Consider, for example an asset-transfer system [13] that allows a set of users to execute transactions sending assets across their accounts. When two transactions $\textit{transfer}(\$100)$ and $\textit{transfer}(\$50)$ are concurrently applied on the same account holding $\$100$ , their effect depends on the order in which they are executed: the first one will be accepted, and the second one – rejected. On the other hand, if the account holds at least $\$150$ , the two transactions can be applied in any order with the same effect.

The notion of a dynamic conflict in asset-transfer systems is defined in a straightforward manner, and one can come up with a system that uses consensus only when necessary, i.e., concurrent transactions cannot all be served [32]. To the best of our knowledge, however, no attempt has been taken to define dynamic conflicts in a universal way, that would apply to any sequential object. We address this issue in the concurrent model, where processes communicate by applying operations on shared base objects, heading for a universal construction, a wait-free linearizable [17, 15] implementation of any object, given its sequential specification. We distinguish between basic read-write operations (offering consensus power $1$ [15, 10, 26]) and strong (read-modify-write) synchronization primitives that enable nontrivial consensus solutions, such as CAS or LL/SC. Our goal is a dynamically concurrent universal construction that avoids using strong synchronization if concurrent operations commute in the current system state. The goal, quite easily grasped on an intuitive level, is however evasive when it comes to formal treatment. How is the “current state” defined in an execution of a concurrent algorithm?

Indeed, consider an operation in a concurrent history. The operation’s interval may be concurrent with different operations at different moments of its execution. How do we define the state of the implemented object and decide whether the operation commutes with concurrent operations in that state? Imagine an implementation in which every operation $o p$ can be thought of taking effect at a well-defined moment between its invocation and its response, a linearization point [17]. Then, each moment during the execution of $o p$ determines a system state, consisting of the effects of operations that have already taken place and the set of operations that have been invoked but not yet linearized. Even if the actual implementation does not allow us to determine an irreversible linearization point for each operation [14], we can derive a superset of all possible system states that might have occurred. Intuitively, an implementation is said to be dynamically concurrent if it uses strong synchronization for an operation only when, in some possible system state during its execution, it does not commute with some concurrent operations (see Figure 1 for an illustration).

The canonical approach to building a universal construction is to order operations using consensus and applying the sequential specification of the object to the ordering. A natural generalization of this approach, aimed at allowing concurrency, is to replace the linear model with a directed acyclic dependency graph of operations, in which all topological orderings yield equivalent linearizations. This way commuting operations are executed in parallel, which might considerably improve performance in workloads where dynamic conflicts are rare, often argued to be the most common case.

Our dynamically concurrent universal construction builds on this idea using a shared dependency graph together with a set of active operations. The current state is obtained by topologically ordering the current version of the graph, while the set of active operations is determined by identifying those that have been invoked but not yet added to the graph. If commutativity with the concurrent operations is observed, the current operation can be appended to the graph directly; otherwise, the algorithm resorts to ordering the operations via consensus. A particular difficulty here is to ensure that conflicting operations committed via different paths (direct commitment and consensus-based) cannot bypass each other, preserving correctness. We achieve this by a variant of commit-adopt [11] that guarantees that a directly committed operation is always placed in the causal past of every concurrent operation that encounters a conflict with it.

To sum up, in this paper we:

(1)

Define the notion of a dynamically concurrent object, the one that resorts to consensus only when a dynamic conflict arises.
(2)

Describe a dynamically concurrent universal construction.

The paper is organized as follows. In Section 2, we overview the related work and in Section 3, we recall our model assumptions. In Section 4, we formally define the notion of dynamic concurrency. In Section 5, we present our protocol and analyze its correctness. Section 6 concludes the paper with the discussion of ramifications of this work and open questions. Certain proofs are delegated to the appendix.

2 Related Work

Most concurrent data structures exhibiting strong consistency and availability guarantees, such as linearizability [17, 5] and wait-freedom [15], require using of consensus or strong synchronization primitives.

As consensus often becomes an implementation’s bottleneck, a lot of effort has been invested in optimistic solutions that avoid consensus in “good runs”, in particular, when no contention is observed [8, 20, 34]. In concurrent data structures, this approach instantiated in solo-fast implementations [4], where strong synchronization is only used when step contention is observed.

Schneider [29] introduced the notion of a state-machine replication, a concurrent implementation of an object given its sequential specification. Lamport [23] discovered the first fault-tolerant state-machine replication protocol and then generalized it to account for parallel execution of non-conflicting operations [24]. In the same vein, Zielinski proposed an elegant and fast generic broadcast protocol that ensures that conflicting broadcast messages are delivered in the same order (non-conflicting ones do not have to be ordered). Both proposals assume a static definition of conflicts, where certain pairs of commands are conservatively considered as conflicting if they do not commute in some state. The static understanding of conflicts has been also considered in the Byzantine fault-tolerant setting: in Byzantine generalized Paxos [28], Byblos [6] and RedBlue [25].

Aspnes and Herlihy [3] presented a wait-free construction for objects where every operations either commutes with or overwrites any other operation in any history. Like our approach, their method uses a precedence graph to capture dependencies between operations. Requiring that every operation either commutes or overwrites any other is a major restriction, since it limits the construction to objects with consensus number one. In contrast, our construction supports arbitrary objects and detects conflicts dynamically.

The notion of dynamic (state-dependent) conflicts has also been considered by Clements et al. [7] in their work on commutativity rule, an efficient generalization of disjoint-access-parallelism by Israeli and Rappoport [18] to semantics-aware systems. Kulkarni et al. [22, 21] discuss algorithms that achieve serializability of transactions and adjust to low-level dynamic conflicts incurred by underlying base-object operations: transactions that do not encounter low-level data conflict proceed in parallel, without unnecessary lock-based synchronization. In contrast, we focus here on high-level semantics-aware dynamic conflicts and wait-free implementations that do not engage in consensus in conflict-free scenarios.

To the best of our knowledge, the only attempt to account for dynamic conflicts in this context was taken in CryptoConcurrency [32], an asset transfer protocol that processes concurrent transactions on the same account in parallel, without resorting to consensus to order them, as long as they are not exhausting the current account balance. In this paper, we generalize this idea to universal construction that allows concurrent operations to proceed in parallel, as long as they are not in conflict in the current object state.

3 Model

We consider a system of $n$ asynchronous processes. Each process can be arbitrarily fast or slow relative to the other processes and can crash fail, i.e., stop taking steps at any moment. The processes communicate through fundamental shared base objects like atomic read-write registers. Those base objects can be used to implement more complex, shared, sequential objects.

Objects.

A sequential object $X$ is defined by a tuple $(Q,q_{0},O,R,\sigma)$ where $Q$ is a set of states, $q_{0}\in Q$ is the initial state, $O$ is a set of operations, $R$ is a set of outputs, and $\sigma:O\times Q\to R\times Q$ is a sequential specification with $\sigma((o,q))=(r,q^{\prime})$ if and only if operation $o$ applied to $X$ in state $q$ returns $r$ and changes its state to $q^{\prime}$ . Since we consider only sequential objects, we will henceforth refer to them simply as objects.

Steps and Algorithms.

The behavior of a process when implementing a high-level object (as opposed to a base object) is described by a deterministic automaton that specifies how each process responds to invocations of that object. Upon receiving an invocation, the process advances by taking steps prescribed by its automaton. We refer to the descriptions of these automatons simply as implementations or algorithms. Each step consists of some terminating local computation together with a single operation on a shared base object. Infinite loops of purely local computation without any interaction with a base object are disallowed. In addition, an algorithm may invoke operations of other higher-level shared objects. Such invocations act as subautomata: control is delegated to the invoked object until its operation finishes, after which the original automaton continues. Conceptually, this recursive structure can be flattened, leaving only local computations and operations on base objects. After each step, a process updates its local state according to its transition rules and may return a response to the currently active operation of the high-level object being implemented. Crucially, a process is not allowed to start executing a new operation on this implemented object until the previous operation has terminated.

Runs and Operations.

A run is a (possibly infinite) sequence of events obtained by interleaving the steps of all processes, beginning from the initial global state. A run especially includes every taken step as well as invocations and response events of operations of every (high-level or base) object involved. For simplicity, we assume that each operation is unique, i.e., an operation is invoked at most once. This uniqueness can be ensured by assigning a caller-specific identifier and a sequence number to every operation. We denote the process executing an operation $o p$ as $o p . p$ , and refer to the invocation and response (event) of $o p$ as $o p . i n v$ and $o p . r e s$ , respectively. Invocations and responses can be uniquely associated with operations.

Histories and Linearizability.

A history is a sequence $H$ of invocations and responses without duplicates, where every response $o p . r e s$ is preceded by its unique matching invocation $o p . i n v$ , and each invocation $o p . i n v$ corresponds to at most one response. We define $op\in H$ if and only if $op.inv\in H$ . A run induces a history for a given object by listing every invocation and response of operations on that object that occur in the run, in the order in which they appear. A history is sequential if every invocation can only be followed by a corresponding response. Thus, a sequential history $S$ is a list of operations and vice versa. Whenever $S$ is finite, the last operation in $S$ might not have a response.

Operation $o p$ precedes $op^{\prime}$ in $H$ if $o p . r e s$ precedes $op^{\prime}.inv$ in $H$ . We write $op<_{H}op^{\prime}$ . If neither $op<_{H}op^{\prime}$ nor $op^{\prime}<_{H}op$ but $op,op^{\prime}\in H$ , $o p$ and $op^{\prime}$ are concurrent in $H$ . The relation $<_{H}$ is irreflexive, asymmetric and transitive and therefore forms a strict partial order. For a sequential history, $<_{H}$ is a total order. We refer to $<_{H}$ as the precedence relation of $H$ . A sequential history $S$ is legal if it satisfies the sequential specifications of the objects, i.e., for each object, starting from its initial state and sequentially applying the operations of $S$ that involve this object yields exactly the responses recorded in $S$ . An operation $o p$ is complete in $H$ if $H$ contains both the invocation and the response of $o p$ . A completion of $H$ is a history $H^{\prime}$ that only includes all complete operations of $H$ and a subset of incomplete operations of $H$ with corresponding responses. Furthermore, $H^{\prime}$ has to preserve the precedence relation of $H$ . Let us denote the history that consists of all invocations and responses of a process $p$ in a history $H$ as $H\mid p$ .

Definition 1.

Histories $H$ and $H^{\prime}$ are equivalent if we have $H\mid p=H^{\prime}\mid p$ for all processes $p$ .

Definition 2.

Let $H$ be a history. A sequential history $S$ is a linearization of $H$ if

$\blacksquare$

$S$ is equivalent to a completion of $H$ ,
$\blacksquare$

$S$ preserves the precedence relation of $H$ and
$\blacksquare$

$S$ is legal.

If there exist such $S$ for a history $H$ , we call $H$ linearizable.

An implementation (or algorithm) $I$ is linearizable if, for every run $R$ of $I$ , the history induced by $R$ is linearizable. Linearizability is a widely accepted correctness condition for concurrent objects. It requires that every operation on the object appears to take effect at a single point in time between its invocation and response, as though the object was accessed atomically.

Wait-freedom.

The gold standard for progress guarantees is wait-freedom. An implementation of an object is wait-free if, whenever a process that does not crash fail invokes an operation, that process is guaranteed to complete the operation in a finite number of its own steps, regardless of the actions or failures of other processes.

Snapshots and Consensus.

A fundamental object with a wait-free linearizable implementation using only atomic read-write registers is the snapshot object [1]. Each process has a dedicated component it can update with a write operation, and all processes can invoke $\textit{snapshot}()$ to obtain a consistent view of all components. Another key object is consensus, exporting a single operation $\textit{propose}(v)$ . Each process can propose values $v$ from a set $V$ , and all invocations must return the same value (agreement), which must be one of the proposed values (validity). We say that a consensus object stores a value $v$ , once an invocation of propose returned that value. Agreement ensures that no other propose operation on the same object can return a different value. Unlike the snapshot object, consensus cannot be implemented in a wait-free linearizable manner using only read-write registers [10]. Any base object that, together with read-write registers, enables solving wait-free consensus, such as CAS or LL/SC, is called a strong synchronization primitive.

4 Dynamic Concurrency

We now introduce the notion of a dynamically concurrent implementation. Before formalizing the notions of the system state and dynamic concurrency in Definitions 6 and 7, we define the equivalence and commutativity relations and then provide some intuition on dynamic concurrency.

4.1 Equivalences and Commutativity

In this section, we define equivalences between sequences of operations, as well as the notion of commutativity, crucial in formalizing the concept of dynamic concurrency in the next section and, accordingly, in determining whether certain operations require ordering in a dynamically concurrent universal construction. Let $s$ and $s^{\prime}$ be disjoint sequences of operations. We denote $s\cdot s^{\prime}$ as the concatenation of $s$ and $s^{\prime}$ . A single operation is interpreted as a sequence of length one.

Definition 3.

Let $s$ and $s^{\prime}$ be orderings of a set of operations $S$ . The orderings $s$ and $s^{\prime}$ are equivalent if according to the sequential specification the application of $s$ to the initial state results in the same state as the application of $s^{\prime}$ and every operation in $S$ returns the same output in both orderings. We write $s\simeq s^{\prime}$ .

If $s\simeq s^{\prime}$ , and $s$ and $s^{\prime}$ share a common prefix $p$ such that $s=p\cdot r$ and $s^{\prime}=p\cdot r^{\prime}$ for some $r$ and $r^{\prime}$ , we say that $r$ and $r^{\prime}$ are equivalent in $p$ .

We immediately see that the relation $\simeq$ of sequences of operations, defined in Definition 3, is a well-defined equivalence relation for a given set of operations, i.e., it is reflexive, symmetric and transitive.

Two states are said to be distinguishable if there exists a sequence of operations whose execution from these states yields different responses. If certain states cannot be distinguished in this way, the object’s states can be replaced by equivalence classes, where two states are equivalent if they are not distinguishable. Working with this quotient state space can increase the number of equivalent orderings and, potentially, the scenarios in which operations commute according to Definition 4.

Definition 4.

Let $o p$ be an operation and $l$ and $s$ sequences of operations with $op\notin l$ , $op\notin s$ and $l\cap s=\emptyset$ . Operation $o p$ commutes in $l$ with $s$ if $l\cdot s\cdot op\simeq l\cdot op\cdot s$ .

Let $S$ be a set of operations with $op\notin S$ and $l\cap S=\emptyset$ . Operation $o p$ commutes in $l$ with $S$ if $o p$ commutes in $l$ with every ordering of $S$ .

Lemma 5.

Let $l$ be a sequence of operations, $s=s_{1}\cdot s_{2}$ and $s^{\prime}=s_{1}^{\prime}\cdot s_{2}^{\prime}$ orderings of the same set of operations $S$ , and $o p$ an operation with $op\notin l$ , $op\notin S$ and $l\cap S=\emptyset$ .

If $l\cdot s\simeq l\cdot s^{\prime}$ and $o p$ commutes with $s_{1}$ , $s_{1}^{\prime}$ , $s$ and $s^{\prime}$ in $l$ , then it follows that $l\cdot s_{1}\cdot op\cdot s_{2}\simeq l\cdot s_{1}^{\prime}\cdot op\cdot s_{2}% ^{\prime}$ .

Proof.

The equivalence follows by transitivity of the equivalence relation.

$l\cdot s_{1}\cdot op\cdot s_{2}\simeq l\cdot op\cdot s_{1}\cdot s_{2}\simeq l% \cdot s_{1}\cdot s_{2}\cdot op\simeq l\cdot s_{1}^{\prime}\cdot s_{2}^{\prime}% \cdot op\simeq l\cdot op\cdot s_{1}^{\prime}\cdot s_{2}^{\prime}\simeq l\cdot s% _{1}^{\prime}\cdot op\cdot s_{2}^{\prime}$ $\hfill\blacktriangleleft$

A key result of Lemma 5 with $s=s^{\prime}$ , used throughout this paper, is that if an operation commutes with every subset of a set, every placement of this operation in this set is equivalent.

4.2 Definitions

The idea behind a linearization, or linearizability in general, is that each operation can be viewed as taking effect atomically at a single moment between its invocation and its response. In many cases, this perspective is straightforward, as one can identify a step where an operation takes effect. In other cases, however, this perspective serves only as an abstraction, since no single concrete point in time can be pinpointed.

Our definition uses this abstraction to define possible configurations during the execution of an operation. Suppose that a linearizable history $H$ is assigned a linearization point to each of its operations, i.e., the moment between its invocation and its response where the operation an be thought of taking effect. Then, the notion of a system state during an operation $o p$ follows naturally. Take a prefix of that enriched history that includes the invocation of $o p$ but not its linearization point. The system state consists of two elements.

1.

The sequence of operations according to their linearization points.¹¹1Note that for a given sequential specification a sequence of operations defines the state of the object.
2.

The set of all operations that have been invoked but not linearized.

Definition 6.

Let $H$ be a history and $o p$ an operation. A system state during $o p$ in $H$ is a pair $(l,O)$ , where $l$ is a sequence and $O$ a set of operations, such that:

1.

There exists a prefix $H^{\prime}$ of $H$ with $op.inv\in H^{\prime}$ and $op.res\notin H^{\prime}$ .
2.

There exists a linearization $L$ of $H$ such that $l$ is a prefix of $L$ and a linearization of $H^{\prime}$ that does not include $o p$ .
3.

The set $O$ consists precisely of those operations $op^{\prime}$ for which $op^{\prime}.inv\in H^{\prime}$ , $op^{\prime}\notin l$ , and $op^{\prime}\neq op$ .

Note that the linearization $l$ in Definition 6 may also contain operations whose responses are not included in $H^{\prime}$ , provided they precede $o p$ in $L$ .

With the definition of system states in place, the notion of dynamic concurrency can be introduced. Intuitively, a dynamically concurrent implementation of an object uses a strong synchronization primitive while executing an operation $o p$ , only when, during its execution, it could have been in a system state where $o p$ does not commute with every subset of the concurrent operations in that current state.

Definition 7.

An implementation $I$ of an object is dynamically concurrent if for every history $H$ induced by a run of $I$ and every operation $o p$ in $H$ , the following holds:

Process $o p . p$ uses a strong synchronization primitive while executing $o p$ .

\Longrightarrow

There exists a system state $(l,O)$ during $o p$ in $H$ such that there exists a subset $O^{\prime}\subseteq O$ with which $o p$ does not commute in $l$ .

While the above definitions formalize the concepts of system state and dynamic concurrency, their intuition may not be immediately apparent. The following example demonstrates how these notions manifest in a concrete execution.

4.3 Example

To illustrate the concepts of system state and dynamic concurrency, consider the history $H$ depicted in Figure 1. The history is induced by a run of $4$ processes executing operations on a shared list object. This object exports the methods $\textit{append}(v)$ , $\textit{readLast}()$ , $\textit{readAll}()$ and $\textit{swap}(i,j)$ for $v\in\{a,b,c,d\}$ and $0\leq i\leq j$ . The method $\textit{append}(v)$ appends $v$ at the end of the list and returns $o k$ ; $\textit{readLast}()$ returns the value at the last index of the list, $\bot$ for an empty list; $\textit{readAll}()$ returns the whole list; $\textit{swap}(i,j)$ swaps the values at indices $i$ and $j$ and returns $o k$ if the list has at least $j-1$ elements, otherwise it has no effect and returns $\bot$ .

Figure 1: An illustration of a history

H

with

4

processes using a shared list object. The response of

p_{2}.\textit{readAll}()

requires every linearization to order

p_{1}.\textit{append}(b)

before

p_{3}.\textit{append}(a)

. Note that

p_{3}.\textit{swap}(0,2)

commutes with

p_{2}.\textit{readLast}()

in

\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{append}(a% )\big)

. Moreover, for every system state during

p_{3}.\textit{swap}(0,2)

in

H

,

p_{3}.\textit{swap}(0,2)

commutes with every subset of concurrent operations in the respective state of the object. Dynamic concurrency forbids

p_{3}

to use a strong synchronization primitive during the execution of

p_{3}.\textit{swap}(0,2)

.

Let us now examine the system states during $op:=p_{3}.\textit{swap}(0,2)$ in $H$ . To determine these states, we consider all possible linearizations $L$ of $H$ . The response of $p_{2}.\textit{readAll}()$ requires that in every linearization, $p_{1}.\textit{append}(b)$ is ordered before $p_{3}.\textit{append}(a)$ . Hence, $\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{append}(a% )\big)$ forms a prefix of every linearization.

This constraint stems from the choice made in Definition 6 to require $l$ to be a prefix of a linearization of the entire history $H$ , rather than simply a linearization of a prefix $H^{\prime}$ . The motivation for this choice is to obtain a more refined representation of the implementation’s internal state. In particular, the definition assumes that after certain operations have terminated (such as $p_{1}.\textit{append}(b)$ and $p_{3}.\textit{append}(a)$ in our example), the internal state of the implementation has either already determined their relative order, even though this ordering is not yet externally observable, or the implementation will never establish such an order at all (in the case of equivalent orderings).

Furthermore, in every linearization $p_{2}.\textit{readLast}()$ precedes $p_{2}.\textit{readAll}()$ , which in turn precedes $p_{0}.\textit{append}(c)$ (if present) and $p_{1}.\textit{append}(d)$ . Excluding $o p$ for the moment, the possible linearizations are:

1.

$\textit{pre}\cdot\big(p_{0}.\textit{append}(c),p_{1}.\textit{append}(d)\big)$ ,
2.

$\textit{pre}\cdot\big(p_{1}.\textit{append}(d),p_{0}.\textit{append}(c)\big)$ ,
3.

$\textit{pre}\cdot\big(p_{1}.\textit{append}(d)\big)$ ,

where $\textit{pre}:=\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.% \textit{append}(a),p_{2}.\textit{readLast}(),p_{2}.\textit{readAll}()\big)$ . All $14$ linearizations that include $o p$ can be obtained by inserting it at any position after the first three operations. However, since we are only interested in those prefixes of linearizations that do not include $o p$ , we can simply omit it. According to Definition 6, we obtain the following system states during $o p$ in $H$ .

1.

$l_{1}=\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{% append}(a)\big)$ with $O_{1}=\big\{p_{2}.\textit{readLast}()\big\}$ ,
2.

$l_{2}=\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{% append}(a),p_{2}.\textit{readLast}()\big)$ with $O_{2}=\big\{\big\}$ ,
3.

$l_{3}=\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{% append}(a),p_{2}.\textit{readLast}()\big)$ with $O_{3}=\big\{p_{1}.\textit{append}(d)\big\}$ ,
4.

$l_{4}=\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{% append}(a),p_{2}.\textit{readLast}()\big)$
with $O_{4}=\big\{p_{1}.\textit{append}(d),p_{0}.\textit{append}(c)\big\}$ ,
5.

$l_{5}=\big(p_{2}.\textit{append}(a),p_{1}.\textit{append}(b),p_{3}.\textit{% append}(a),p_{2}.\textit{readLast}()\big)$
with $O_{5}=\big\{p_{1}.\textit{append}(d),p_{0}.\textit{append}(c),p_{2}.\textit{% readAll}()\big\}$ ,
6.

$l_{6}=\textit{pre}$ with $O_{6}=\big\{p_{1}.\textit{append}(d),p_{0}.\textit{append}(c)\big\}$ ,
7.

$l_{7}=\textit{pre}\cdot\big(p_{0}.\textit{append}(c)\big)$ with $O_{7}=\big\{p_{1}.\textit{append}(d)\big\}$ ,
8.

$l_{8}=\textit{pre}\cdot\big(p_{1}.\textit{append}(d)\big)$ with $O_{8}=\big\{p_{0}.\textit{append}(c)\big\}$ ,
9.

$l_{9}=\textit{pre}\cdot\big(p_{0}.\textit{append}(c),p_{1}.\textit{append}(d)\big)$ with $O_{9}=\big\{\big\}$ ,
10.

$l_{10}=\textit{pre}\cdot\big(p_{1}.\textit{append}(d),p_{0}.\textit{append}(c)\big)$ with $O_{10}=\big\{\big\}$ .

According to Definition 7, dynamic concurrency forbids $p_{3}$ to use strong synchronization primitives during the execution of $o p$ , since in every system state $(l_{i},O_{i})$ $o p$ commutes in $l_{i}$ with every subset of $O_{i}$ .²²2The condition for all $i\in[1,10]$ is equivalent to requiring it only for $i\in\{1,5\}$ . Note that this holds even though $p_{0}.\textit{append}(c)$ and $p_{1}.\textit{append}(d)$ do not commute in any state.

Similarly, $p_{2}$ cannot use strong synchronization primitives during the execution of either $p_{2}.\textit{append}(a)$ or $p_{2}.\textit{readLast}()$ .

As discussed above, the response of $p_{2}.\textit{readAll}()$ enforces that $p_{1}.\textit{append}(b)$ must be ordered before $p_{3}.\textit{append}(a)$ . Suppose, however, that $p_{2}.\textit{readAll}()$ were absent from the history. In that case, $p_{3}.\textit{append}(a)$ could instead be ordered before $p_{1}.\textit{append}(b)$ , since the response of $p_{2}.\textit{readLast}()$ would remain correct provided that $p_{3}.\textit{swap}(0,2)$ is ordered before $p_{2}.\textit{readLast}()$ . In this scenario, $p_{3}.\textit{swap}(0,2)$ no longer commutes with $p_{2}.\textit{readLast}()$ , and consequently $p_{3}$ would be permitted to use strong synchronization primitives while executing $p_{3}.\textit{swap}(0,2)$ .

5 Dynamically Concurrent Universal Construction

We now present our (wait-free and linearizable) dynamically concurrent universal construction. The universal construction takes the specification of a sequential object as a parameter and exports one method $\textit{publish}(op)$ that simulates the execution of an operation $o p$ and returns a response of $o p$ .

A typical universal construction invokes multiple instances of consensus to agree on the order in which invoked operations are linearized. The response of each operation is then computed from this order using the object’s sequential specification.

To exploit commutativity, we replace the linear ordering on operations with a shared dependency graph. Intuitively, in the graph, an operation has incoming edges from every operation that should precede it. Unrelated operations in the graph are then concurrent and commuting. A linearization is obtained by topologically ordering this dependency graph.

For this algorithm to be correct, we essentially have to ensure the following conditions. First of all, after the completion of $\textit{publish}(op)$ the operation $o p$ has to be added to the dependency graph. Secondly, this dependency graph has to be an acyclic graph to ensure that topological orderings exist. Another requirement is that the topological orderings, and therefore the dependency graph, should respect the real-time ordering of different invocations of publish, i.e., the precedence relation of the induced history. If $\textit{publish}(op)$ terminates before $\textit{publish}(op^{\prime})$ is invoked, $o p$ should precede $op^{\prime}$ in every topological ordering, i.e., there must be an edge from $o p$ to $op^{\prime}$ in the dependency graph. Furthermore, all possible topological ordering of this dependency graph should be equivalent, as stated in Definition 3. Intuitively, unrelated graph vertices should commute and, thus, no process can distinguish their different orderings. Finally, we have to guarantee that this dependency graph is stable in the sense that no response of an operation, according to any topological ordering, changes when the graph evolves. This is necessary, since such a response might have already been returned by some process as the response of that operation.

We now introduce the Announce-Book-Commit Graph, a core component of our algorithm.

5.1 Announce-Book-Commit (ABC) Graph

Before introducing the main part of the algorithm, we describe the principal underlying data structure used to implement the dependency graph. The ABC Graph composes three data structures $A$ , $B$ and $C$ into one snapshot object to allow an atomic read of all three structures.

1.

$A$ is a set of operations.
2.

$B$ is a set of tuples $(op,b)$ where $o p$ is an operation and $b$ is an integer.
3.

$C$ is a graph of operations, encoded as a set of tuples $(op,M)$ , where $o p$ is an operation and $M$ is a set of operations, interpreted as the set of operations that have outgoing edges to $o p$ .

The ABC Graph exports three methods $\textit{add}_{A}(op)$ , $\textit{add}_{B}(op,b)$ and $\textit{add}_{C}(op,M)$ used to append elements to the corresponding sets in the following way. The set $A$ is the set of all operations $o p$ with some preceding $\textit{add}_{A}(op)$ operation. The set $B$ is the set of all tuples such that $(op,b)\in B$ if and only if there exists some preceding $\textit{add}_{B}(op,b)$ and $b$ is minimal among all preceding operations $\textit{add}_{B}(op,\cdot)$ . The graph $C$ is the set of all tuples such that $(op,M)\in C$ if and only if there exists some preceding operations $\textit{add}_{C}(op,M_{j})$ and $M=\bigcup_{j}M_{j}$ for all preceding operations $\textit{add}_{C}(op,M_{j})$ . The method $\textit{read}()$ returns the current state of the three data structures. Note that, even though $\textit{add}_{B}(op,\cdot)$ and $\textit{add}_{C}(op,\cdot)$ may be called multiple times for the same operation $o p$ , the components $B$ and $C$ , as returned by $\textit{read}()$ , include at most one tuple per operation: the minimum value for $B$ and the union of all sets for $C$ .

We say that an operation is announced once it is added to $A$ , booked once it is added to $B$ , and committed once it is added to $C$ . Correspondingly, we say that a process is announcing, booking, or committing an operation while executing $\textit{add}_{A}$ , $\textit{add}_{B}$ , or $\textit{add}_{C}$ , respectively. In particular, when we say that an operation $o p$ is being committed for the first time, we mean that some process is currently executing $\textit{add}_{C}(op,\cdot)$ that adds $o p$ into $C$ for the first time. We denote by $\textit{vertices}(B)$ (resp., $\textit{vertices}(C)$ ) the set of operations that appear in $B$ (resp., $C$ ). Note that operations appear only as the first element of a tuple in $B$ but in both parts of a tuple in $C$ . Furthermore, we denote by $\textit{edges}(C)$ the set of edges of $C$ , i.e., $(op,op^{\prime})\in\textit{edges}(C)$ if and only if there exists $(op^{\prime},M)\in C$ with $op\in M$ . The value associated with an operation $o p$ in $B$ is called its $B$ -value and is denoted by $B[op]$ . If $op\not\in\textit{vertices}(B)$ , we say that $o p$ has no $B$ -value, and we define, by convention, $B[op]$ to be $\infty$ .

Given the specification of an ABC Graph, we now discuss its interpretation and use within our universal construction. Each invocation of $\textit{publish}(op)$ announces its own operation $o p$ by adding it to the set $A$ , which thus contains every operation invoked so far. For each operation $o p$ , the set $B$ records information about the recency of the ABC Graph that $\textit{publish}(op)$ has observed (namely, the size of $A$ ). In our construction, each invocation $\textit{publish}(op)$ calls $\textit{add}_{A}(op)$ and $\textit{add}_{B}(op,\cdot)$ at most once, and only for its own parameter. Consequently, the aggregation mechanism for $B$ exists solely for formal completeness and is not needed in practice. Graph $C$ is interpreted as the dependency graph described above.

Algorithm 1 Announce-Book-Commit Graph.

Algorithm 1 provides a wait-free and linearizable implementation of the ABC Graph. The proof is deferred to Appendix A. In the implementation, processes store invocations of add operations in local registers (lines 8, 11 and 14) and write them to a shared snapshot object. The read operation aggregates all invocations of add to $A$ , $B$ and $C$ as described above.

5.2 Dynamically Concurrent Universal Construction

In the following, we provide intuition for how the dynamically concurrent universal construction in Algorithm 2 operates: how it places an operation $o p$ correctly into the dependency graph, and why consensus is used only when necessary, satisfying dynamic concurrency (Definition 7). Formal proofs of linearizability, wait-freedom, and dynamic concurrency are deferred to the Appendices B, C, and D.

Algorithm 2 Dynamically Concurrent Universal Construction.

Once a process proposes an operation $o p$ (line 5), it first adds it to set $A$ (line 6) to make it visible to concurrent and future operations. Then it takes a snapshot (line 7) of the current state ( $A$ , $B$ and $C$ ). By construction, graph $C$ contains the previously committed operations. The operations in $A-\textit{vertices}(C)$ are therefore concurrent. Let us call this set CUR. Note that some operations in CUR may never be committed, as they may be issued by processes that have later crashed.

After reading the state for the first time, $o p$ is added to $B$ (line 8) together with $|A|$ , the cardinality of $A$ . Intuitively, $|A|$ indicates how many operations $\textit{publish}(op)$ has encountered at its first read, indicating the recency of its view of the system. This helps later to prioritize operations that may have missed conflicts. After announcing and booking the operation, the process reads the state again (line 9), which updates its local values for $A$ , $B$ and $C$ (and implicitly CUR). The graph $C$ is then topologically ordered (line 10). We denote this ordering by $l$ . We assume inductively that all topological orderings of $C$ are equivalent. If $o p$ is already committed (line 11), the result of the operation in $l$ (according to the sequential specification) is returned (line 12); otherwise, the process checks whether $o p$ commutes with every subset of $\textit{CUR}-\{op\}$ in $l$ (line 14). Verifying commutativity with every subset of $\textit{CUR}-\{op\}$ accounts for the possibility that some operations in CUR may never be committed due to crash failures. Moreover, Lemma 5 guarantees that, for every equivalent ordering of $\textit{CUR}-\{op\}$ in $l$ , every possible insertion point of $o p$ within those orderings is equivalent in $l$ , as formalized in Definition 3. If commutativity is verified, $\textit{publish}(op)$ commits $o p$ (line 15) and returns its response in $l\cdot(op)$ (line 16). Otherwise, ordering of concurrent operations is required and conflict resolution (lines 18-32), where consensus is used, is executed.

Conflict resolution proceeds in iterations. In each iteration, the process reads the state (line 22), selects an operation with the minimal $B$ -value (among all non-committed operations) (line 26) and proposes it to the next consensus object (line 27). The state is read again (line 28) and unless the operation $\hat{op}$ that has been returned by the consensus object is already committed (line 29), it is committed by $\textit{publish}(op)$ in line 30.

Each operation $\tilde{op}$ that is proposed to a consensus object, and therefore each operation that is committed in conflict resolution, has minimal $B$ -value, according to a version of the ABC Graph that was read by some process executing conflict resolution. In the following, we are interested in the $B$ -values according to this version of the ABC Graph. As can be easily verified, an operation is added to $B$ at most once, and only by its corresponding invocation of publish. Consequently, the $B$ -values of different versions of the ABC Graph differ only in the set of operations that have a (finite) $B$ -value. Once an operation has a (finite) $B$ -value, it is constant. Since we consider, by construction, a version of the ABC Graph where $\tilde{op}$ has a minimal $B$ -value (among all non-committed operations), there only exist operations with a higher $B$ -value or operations that do not have a $B$ value yet. Each operation that already has, or can obtain, a $B$ -value of at most that of $\tilde{op}$ has been encountered by $\textit{publish}(\tilde{op})$ in line 9.³³3Since the ABC Graph is linearizable, we can order all invocations of $\textit{add}_{A}$ . Let $op_{i}$ be the $i$ -th operation added to $A$ . Since the ABC Graph is read again after executing $\textit{add}_{A}(op_{i})$ , $op_{i}$ will have a $B$ -value of at least $i$ , once it is booked. An operation that already has, or can obtain, a $B$ -value of at most $i$ , has to be among the first $i$ operations added to $A$ , and has therefore been encountered in line 9 by an operation with a $B$ -value of $i$ .

One can notice that $\textit{publish}(\tilde{op})$ might have not encountered (in line 9) concurrent operations with higher (possibly infinite) $B$ -values. Therefore, $\textit{publish}(\tilde{op})$ might have encountered no conflict and already passed the check of commutativity (line 14). This is the reason why operations with minimal $B$ -value are prioritized in conflict resolution. Operations with no $B$ -value, i.e., operations that are not booked yet, will reread the state (line 9) before committing and therefore encounter every operation that already has a $B$ -value. Thus, an operation with no $B$ -value will either encounter a conflict too or find every conflict already resolved in $C$ . Therefore, operations that are not in $B$ , i.e. with no $B$ -value, need not to be prioritized in the conflict resolution. In summary, an operation with minimal $B$ -value (among concurrent operations) in some version of the ABC Graph has been or will be encountered in line 9 by $\textit{publish}(op^{*})$ for every non-committed operation $op^{*}$ . Such an operation can therefore be proposed to be committed in conflict resolution without risking conflicting operations to miss it.

Clearly, when an operation is proposed to $\textit{CONS}_{k}$ , every previous $\textit{CONS}_{m}$ with $m<k$ stores an operation and those operations are committed. This does not imply that an operation stored in $\textit{CONS}_{k}$ , once committed, will include all of those operations, stored in previous consensus objects, as dependencies. This is due to the fact, that operations can be concurrently committed in the conflict-free path, while being proposed to a consensus object. However, it is easy to see that if an operation $o p$ is committed in the conflict resolution path, every operation committed in the conflict resolution path using a later consensus object will include $o p$ in its dependencies.

The algorithm uses a snapshot object (line 2) that records the last completed iteration of every process, allowing processes to skip iterations that have already been completed by any process (lines 18, 19, 21 and 32). This does not affect correctness, as re-executing a completed iteration has no effect.

Sketch of Linearizability Proof.

Algorithm 2 ensures linearizability by checking commutativity among operations and resorting to consensus when conflicts arise. No two conflicting operations can proceed along the conflict-free path simultaneously, because at least one operation will detect the other. Operations that could have “missed” conflicts are prioritized, when committing operations in the conflict resolution path, to maintain a consistent view among all processes. While a conflict is being resolved, other conflicting operations also enter conflict resolution, whereas non-conflicting operations continue along the conflict-free path. The resulting dependency graph has topological orderings that are equivalent, and each such ordering serves as a linearization of the history.

Sketch of Wait-Freedom Proof.

Under the assumption that the ABC Graph is wait-free, any invocation of publish that encounters no conflict terminates trivially after a finite number of steps. For invocations that perform conflict resolution, the process skips iterations that have already been completed. Given at most $c\leq n$ concurrent processes, the corresponding operation is stored in a consensus object after at most $c+1$ iterations, unless it is concurrently committed via the conflict-free path. In all cases, publish completes after a finite number of steps.

Sketch of Dynamic Concurrency Proof.

When reading the ABC Graph (line 9), the tuple $\big(\textit{linearize}(C),A-\textit{vertices}(C)-\{op\}\big)$ essentially represents a system state. It can be shown that $l:=\textit{linearize}(C)$ is a linearization of the history induced by the current run, and that for every possible extension of the run the induced history has a linearization such that $l$ is a prefix of that linearization. Furthermore, $A-\textit{vertices}(C)-\{op\}$ consists of concurrent operations $op^{\prime}$ such that $op^{\prime}\not\in\textit{linearize}(C)$ and $op^{\prime}\neq op$ , as required by Definition 6. Note that $A-\textit{vertices}(C)-\{op\}$ might be a subset of all concurrent operations, which only restricts the cases where consensus is invoked. Therefore, the check performed in line 14 directly corresponds to the dynamic concurrency condition: consensus is used only when the operation does not commute with some subset of the concurrent operations in that system state.

As mentioned above, formal proofs of linearizability, wait-freedom, and dynamic concurrency are provided in the Appendices B, C, and D.

6 Discussion

In this paper, we settle down the very possibility of implementing a dynamically concurrent universal construction that only resorts to consensus if the concurrent operations are in conflict, given the current object state.

The next question is what the cost of detecting and resolving dynamic conflicts is. In our construction, non-conflicting operations complete in two write-read rounds. However, both the communication overhead of these rounds and the local computation can become significant. The latter is exponential in the number of concurrent operations, as commutativity must be verified for every subset of those. In contrast, consensus itself may not be particularly costly, especially in a shared-memory setting, which suggests a trade-off between minimizing synchronization through dynamic conflict detection and the total computational and communication costs associated with it. It may well be that these costs outweigh the benefits gained from avoiding consensus in conflict-free scenarios. It is therefore appealing to undertake comparative performance analysis of universal-construction algorithms, with and without dynamic conflict resolution.

It is important to note that our construction makes no assumptions about the type of operations. It is common to avoid synchronization in read-only workloads, and the same optimization is possible here. Read-only operations do not need to be added to the dependency graph, since other processes do not need to be aware of them. They can compute their responses directly based on an up-to-date version of the dependency graph, proceeding efficiently while preserving correctness.

The current definition of a concurrent operation accounts for interval contention [4] – operations are considered concurrent if their intervals overlap. A more refined definition accounts for step contention which only accounts for concurrently active (taking steps) operations [16, 4]. It is tempting to design a universal construction that uses consensus only when a concurrently active conflicting operation is detected. We conjecture, however, that this might not be possible.⁴⁴4Note that every sequential objects admits a solo-fast implementation [4], in which operations complete without using strong synchronization primitives in the absence of step contention. However, using a solo-fast consensus object implementation in our algorithm would not achieve the desired effect. Even if no conflicting operation takes steps concurrently, some commuting operations could still introduce step contention on the solo-fast consensus implementation.

This work is close in spirit to the idea of optimal concurrency [12, 2], an earlier attempt to grasp the minimal use of synchronization in concurrent data structures. By naïvely running the sequential implementation of an object in the concurrent environment, we obtain, intuitively, the throughput baseline: no implementation is likely to perform better [9]. We can turn this (most probably incorrect) sequential implementation into a correct concurrent one by introducing synchronization primitives. One can then reason about the amount of concurrency the implementation exhibits using the set of correct (linearizable) concurrent schedules it accepts. An optimally concurrent implementation [12] rejects a schedule only if it results in an incorrect (i.e., not linearizable) execution. Examples of optimally concurrent implementations of concrete data structures are given in [12, 2]. In contrast, in this paper, we rely on the sequential specification of the object, rather then on a concrete sequential implementation of it. This makes our approach more general, even though we do not argue that the use of consensus is minimal in any sense. It is intriguing to explore the issue of “optimality” further, e.g., can one argue that no algorithm can use less strong synchronization?

Finally, dynamic conflict resolution can become an important tool in Byzantine fault-tolerant universal constructions [27, 33], in particular in DAG-based blockchains [19, 31, 30].

References

[1] Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. Atomic snapshots of shared memory. J. ACM, 40(4):873–890, September 1993. doi:10.1145/153724.153741.
[2] Vitaly Aksenov, Vincent Gramoli, Petr Kuznetsov, Di Shang, and Srivatsan Ravi. Optimal concurrency for list-based sets. In Victor Malyshkin, editor, PaCT, volume 12942 of Lecture Notes in Computer Science, pages 386–401. Springer, 2021. doi:10.1007/978-3-030-86359-3_29.
[3] J. Aspnes and M. Herlihy. Wait-free data structures in the asynchronous pram model. In Proceedings of the Second Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA ’90, pages 340–349, New York, NY, USA, 1990. Association for Computing Machinery. doi:10.1145/97444.97701.
[4] Hagit Attiya, Rachid Guerraoui, Danny Hendler, and Petr Kuznetsov. The complexity of obstruction-free implementations. J. ACM, 56(4):24:1–24:33, 2009. doi:10.1145/1538902.1538908.
[5] Hagit Attiya and Jennifer L. Welch. Distributed computing - fundamentals, simulations, and advanced topics (2. ed.). Wiley series on parallel and distributed computing. Wiley, 2004.
[6] Rida Bazzi and Maurice Herlihy. Clairvoyant state machine replication. Information and Computation, 285:104701, 2022. doi:10.1016/J.IC.2021.104701.
[7] Austin T. Clements, M. Frans Kaashoek, Nickolai Zeldovich, Robert T. Morris, and Eddie Kohler. The scalable commutativity rule: designing scalable software for multicore processors. In Michael Kaminsky and Mike Dahlin, editors, SOSP, pages 1–17. ACM, 2013. doi:10.1145/2517349.2522712.
[8] James A. Cowling, Daniel S. Myers, Barbara Liskov, Rodrigo Rodrigues, and Liuba Shrira. HQ replication: A hybrid quorum protocol for byzantine fault tolerance. In Brian N. Bershad and Jeffrey C. Mogul, editors, OSDI, pages 177–190. USENIX Association, 2006. URL: http://www.usenix.org/events/osdi06/tech/cowling.html.
[9] Tudor David, Rachid Guerraoui, and Vasileios Trigonakis. Asynchronized concurrency: The secret to scaling concurrent search data structures. In ASPLOS, pages 631–644, 2015. doi:10.1145/2694344.2694359.
[10] Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. JACM, 32(2):374–382, April 1985. doi:10.1145/3149.214121.
[11] Eli Gafni. Round-by-round fault detectors (extended abstract): unifying synchrony and asynchrony. In PODC, pages 143–152, 1998.
[12] Vincent Gramoli, Petr Kuznetsov, and Srivatsan Ravi. In the search for optimal concurrency. In Jukka Suomela, editor, SIROCCO, volume 9988 of Lecture Notes in Computer Science, pages 143–158, 2016. doi:10.1007/978-3-319-48314-6_10.
[13] Rachid Guerraoui, Petr Kuznetsov, Matteo Monti, Matej Pavlovic, and Dragos-Adrian Seredinschi. The consensus number of a cryptocurrency. In PODC, 2019. URL: https://arxiv.org/abs/1906.05574.
[14] Maryam Helmi, Lisa Higham, and Philipp Woelfel. Strongly linearizable implementations: possibilities and impossibilities. In Darek Kowalski and Alessandro Panconesi, editors, PODC ’12, pages 385–394. ACM, 2012. doi:10.1145/2332432.2332508.
[15] Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124–149, 1991. doi:10.1145/114005.102808.
[16] Maurice Herlihy, Victor Luchangco, and Mark Moir. Obstruction-free synchronization: Double-ended queues as an example. In 23rd International Conference on Distributed Computing Systems (ICDCS 2003), 19-22 May 2003, Providence, RI, USA, pages 522–529. IEEE Computer Society, 2003. doi:10.1109/ICDCS.2003.1203503.
[17] Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463–492, July 1990. doi:10.1145/78969.78972.
[18] Amos Israeli and Lihu Rappoport. Disjoint-access-parallel implementations of strong shared memory primitives. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, PODC ’94, pages 151–160, 1994. doi:10.1145/197917.198079.
[19] Idit Keidar, Eleftherios Kokoris-Kogias, Oded Naor, and Alexander Spiegelman. All you need is DAG. In Avery Miller, Keren Censor-Hillel, and Janne H. Korhonen, editors, PODC ’21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021, pages 165–175. ACM, 2021. doi:10.1145/3465084.3467905.
[20] Ramakrishna Kotla, Lorenzo Alvisi, Mike Dahlin, Allen Clement, and Edmund Wong. Zyzzyva: speculative byzantine fault tolerance. In Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, pages 45–58, 2007.
[21] Milind Kulkarni, Donald Nguyen, Dimitrios Prountzos, Xin Sui, and Keshav Pingali. Exploiting the commutativity lattice. In Mary W. Hall and David A. Padua, editors, PLDI, pages 542–555. ACM, 2011. doi:10.1145/1993498.1993562.
[22] Milind Kulkarni, Dimitrios Prountzos, Donald Nguyen, and Keshav Pingali. Defining and implementing commutativity conditions for parallel execution. In Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM, 2009.
[23] Leslie Lamport. The Part-Time parliament. ACM Transactions on Computer Systems, 16(2):133–169, May 1998. doi:10.1145/279227.279229.
[24] Leslie B Lamport. Generalized paxos, apr13 2010. US Patent 7,698,465. URL: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-33.pdf.
[25] Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno M. Preguiça, and Rodrigo Rodrigues. Making geo-replicated systems fast as possible, consistent when necessary. In Chandu Thekkath and Amin Vahdat, editors, 10th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2012, Hollywood, CA, USA, October 8-10, 2012, pages 265–278. USENIX Association, 2012. URL: https://www.usenix.org/conference/osdi12/technical-sessions/presentation/li.
[26] M.C. Loui and H.H. Abu-Amara. Memory requirements for agreement among unreliable asynchronous processes. Advances in Computing Research, 4:163–183, 1987.
[27] Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system, 2008.
[28] Miguel Pires, Srivatsan Ravi, and Rodrigo Rodrigues. Generalized paxos made byzantine (and less complex). Algorithms, 11(9):141, 2018. doi:10.3390/A11090141.
[29] Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22(4):299–319, December 1990. doi:10.1145/98163.98167.
[30] Alexander Spiegelman, Balaji Arun, Rati Gelashvili, and Zekun Li. Shoal: Improving DAG-BFT latency and robustness. In Jeremy Clark and Elaine Shi, editors, Financial Cryptography and Data Security - 28th International Conference, FC 2024, Willemstad, Curaçao, March 4-8, 2024, Revised Selected Papers, Part I, volume 14744 of Lecture Notes in Computer Science, pages 92–109. Springer, 2024. doi:10.1007/978-3-031-78676-1_6.
[31] Alexander Spiegelman, Neil Giridharan, Alberto Sonnino, and Lefteris Kokoris-Kogias. Bullshark: DAG BFT protocols made practical. In Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi, editors, Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, pages 2705–2718. ACM, 2022. doi:10.1145/3548606.3559361.
[32] Andrei Tonkikh, Pavel Ponomarev, Petr Kuznetsov, and Yvonne-Anne Pignolet. Cryptoconcurrency: (almost) consensusless asset transfer with shared accounts. In Weizhi Meng, Christian Damsgaard Jensen, Cas Cremers, and Engin Kirda, editors, CCS, pages 1556–1570. ACM, 2023. doi:10.1145/3576915.3616587.
[33] Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, 151(2014):1–32, 2014.
[34] Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan-Gueta, and Ittai Abraham. Hotstuff: BFT consensus with linearity and responsiveness. In Peter Robinson and Faith Ellen, editors, PODC, pages 347–356. ACM, 2019. doi:10.1145/3293611.3331591.

Appendix A ABC Graph – Proof of Linearizability and Wait-freedom

In this section, we prove in Lemma 8 that the implementation of the ABC Graph given in Algorithm 1 is both linearizable and wait-free, assuming that the underlying snapshot object $S$ (line 6) itself is linearizable and wait-free.

Lemma 8.

Algorithm 1 is a wait-free linearizable implementation of an ABC Graph.

Proof.

Let $R$ be a run of Algorithm 1, and let $H$ be the history induced by $R$ with respect to the ABC Graph. Furthermore, let $H_{S}$ denote the history induced by $R$ with respect to the shared snapshot object $S$ , i.e., $H$ contains the invocations and responses of ABC Graph operations, while $H_{S}$ contains the invocations and responses of snapshot operations. Each ABC Graph operation accesses $S$ exactly once (lines 9, 12, 15, 17). Consequently, there is a unique mapping from operations of $S$ to the corresponding operations of the ABC Graph (lines 7, 10, 13, 16).

Let $L_{S}$ be a linearization of $H_{S}$ , and let $L$ be the sequence of ABC Graph operations obtained by mapping each operation in $L_{S}$ to its originating ABC Graph operation. We show that $L$ is a linearization of $H$ .

For each $op.res\in H$ there is a corresponding operation of $S$ in $L_{S}$ and therefore $op\in L$ . Similarly, for each operation on $S$ in $L_{S}$ there is a corresponding $o p$ with $op.inv\in H$ . Assume that there are $op,op^{\prime}\in H$ with $op<_{H}op^{\prime}$ . It follows, that the corresponding operation on $S$ of $o p$ precedes the one of $op^{\prime}$ in $H_{S}$ and therefore in $L_{S}$ and consequently $op<_{L}op^{\prime}$ . We conclude that $L$ is a sequential history that is equivalent to a completion of $H$ and preserves the precedence relation of $H$ .

It remains to show that $L$ is legal. Among the ABC Graph operations, only $\textit{read}()$ (line 16) produces a response value. This value is determined by the response value of $S.\textit{snapshot}()$ in line 17. Since $S$ is linearizable, its response value contains exactly those write operations that precede it in $L_{S}$ . Consequently, the response value of $\textit{read}()$ contains precisely the $\textit{add}_{X}$ operations ( $X\in\{A,B,C\}$ ) that precede it in $L$ . The aggregation of $A$ , $B$ , and $C$ coincides with the specification given in Section 5.1. Therefore, Algorithm 1 is a linearizable implementation of an ABC Graph.

Algorithm 1 uses a single shared object: the snapshot object $S$ (line 6). Each ABC Graph operation performs exactly one operation on $S$ along with some local computation. As a result, the number of steps required by the ABC Graph implementations matches that of the underlying snapshot object. Therefore, assuming $S$ is wait-free, the ABC Graph implementation is wait-free as well. $\hfill\blacktriangleleft$

Appendix B Universal Construction – Proof of Linearizability

In the proof of correctness for Algorithm 2, we assume discrete global time, inaccessible to any individual process. Since Algorithm 1 is a linearizable implementation of the ABC Graph (Lemma 8), the execution of operations on this object admits a well-defined total order. We start from an initial time $t=0$ . Each invocation of $\textit{add}_{A}$ , $\textit{add}_{B}$ or $\textit{add}_{C}$ produces an atomic extension, which transforms the graph at time $t$ into the graph at time $t+1$ . We denote such an atomic extension by $t\rightarrow t+1$ . The causing add operation is assigned the timestamp $t+1$ . An extension is then defined as a sequence of one or more consecutive atomic extensions, representing the evolution of the graph across time. Since the read method is state-preserving, we assign it the same timestamp as its most recent predecessor (or $t=0$ if none exists). Consequently, if the same timestamp $t$ is assigned to a read and an add operation, the read observes the new state, i.e., is scheduled after the add operation. We denote $A_{t}$ , $B_{t}$ and $C_{t}$ as the values of $A$ , $B$ and $C$ at time $t$ .

As mentioned at the beginning of Section 5, linearizability of our construction is implied by the properties introduced there, which are consolidated and slightly extended in their formal statement in Lemma 9. The remainder of this section is dedicated to proving these properties and concluding in Lemma 26 that the universal construction in Algorithm 2 is linearizable.

Lemma 9.

Each run of Algorithm 2 fulfills the following properties. Let $o p$ and $op^{\prime}$ be any two operations in that run.

$\blacksquare$

For all times $t\geq 0$ , $C_{t}$ is acyclic.
$\blacksquare$

Upon termination of $\textit{publish}(op)$ , the operation $o p$ is committed.
$\blacksquare$

If $\textit{publish}(op)$ precedes $\textit{publish}(op^{\prime})$ , then $o p$ precedes $op^{\prime}$ in every topological ordering of $C_{t}$ for every $t$ after $op^{\prime}$ has been committed.
$\blacksquare$

Let $t_{1},t_{2}\geq 0$ , and let $s_{1}$ and $s_{2}$ be topological orderings of $C_{t_{1}}$ and $C_{t_{2}}$ , respectively. For every operation $o p$ such that $op\in s_{1}$ and $op\in s_{2}$ , the sequential specification yields the same response for $o p$ in both $s_{1}$ and $s_{2}$ .
$\blacksquare$

For every time $t_{2}\geq 0$ and every operation $op\in C_{t_{2}}$ , if $o p$ has a response, then there exists a time $t_{1}$ with $0\leq t_{1}\leq t_{2}$ and a topological ordering $T$ of $C_{t_{1}}$ that contains $o p$ , such that the response of $o p$ agrees with the sequential specification applied to $T$ .

B.1 Fundamental Properties and Acyclicity

After expanding the notion of the inclusion relation to graphs in Definition 10, we establish some basic properties of Algorithm 2 through a series of Lemmata. Important insights are for example that the ABC Graph is only growing (Lemma 11), only growing by at most one node at a time (Lemma 13) and that the graph $C$ is transitive (Lemma 14) and acyclic (Lemma 15) and consequently suitable for topological ordering. Lemma 17 shows that it is always possible to select a topological ordering of a version of $C$ in which a prefix forms a topological ordering of an earlier version of $C$ .

Definition 10.

Let $G$ and $H$ be graphs. We write $G\subseteq H$ if $\textit{vertices}(G)\subseteq\textit{vertices}(H)\wedge\textit{edges}(G)% \subseteq\textit{edges}(H)$ .

Lemma 11.

The sets $A_{t}$ and $B_{t}$ , and graph $C_{t}$ satisfy the following properties for every time $t\geq 0$ :

1.

$A_{t}\subseteq\textit{vertices}(B_{t})\subseteq\textit{vertices}(C_{t})$ .
2.

Let $o p$ be an operation. No other process than the one executing $\textit{publish}(op)$ announces or books $o p$ . It is announced at most once and booked at most once.
3.

If $t\leq t^{\prime}$ , then $A_{t}\subseteq A_{t^{\prime}}$ , $B_{t}\subseteq B_{t^{\prime}}$ , and $C_{t}\subseteq C_{t^{\prime}}$ .
4.

For any finite set of times $t_{1}\leq\dots\leq t_{m}$ , we have $C_{t_{m}}=\bigcup_{j}C_{t_{j}}$ .

Proof.

Items 1-3 follow trivially from the implementation. Item 4 follows directly from item 3. $\hfill\blacktriangleleft$

Lemma 12.

The graph $C_{t}$ is irreflexive for every time $t\geq 0$ .

Proof.

The initial graph $C_{0}$ is empty and trivially irreflexive. Let $t\rightarrow t+1$ be an atomic extension of the ABC Graph. If this is the result of an invocation of $\textit{add}_{A}$ or $\textit{add}_{B}$ , we have $C_{t+1}=C_{t}$ and irreflexivity follows by induction. Assume that $t\rightarrow t+1$ is the result of an invocation of $\textit{add}_{C}(op,M)$ and therefore adds incoming edges to at most one node. To prove irreflexivity, we have to show that $op\notin M$ . The method $\textit{add}_{C}(op,M)$ is called in lines 15 and 30. In both cases, the condition $op\notin M$ has been explicitly checked previously. $\hfill\blacktriangleleft$

Lemma 13.

Let $E_{t}:=t\rightarrow t+1$ be an atomic extension of the ABC Graph and let this extension be the result of an invocation of $\textit{add}_{C}(op,M)$ . We have

1.

$M=\textit{vertices}(C_{t^{\prime}})$ for some time $t^{\prime}\leq t$ and
2.

$\textit{vertices}(C_{t+1})-\textit{vertices}(C_{t})\subseteq\{op\}$ .

We define $C(E_{t}):=C_{t^{\prime}}$ for the $C_{t^{\prime}}$ that was used to calculate $M$ .

Proof.

The method $\textit{add}_{C}(op,M)$ is called in lines 15 and 30. In both cases it is called with $M=\textit{vertices}(C^{\prime})$ for some previously read graph $C^{\prime}$ . With Lemma 11 (3) we have $M\subseteq\textit{vertices}(C_{t})$ and therefore $\textit{vertices}(C_{t+1})-\textit{vertices}(C_{t})\subseteq\{op\}$ . As multiple graphs $C_{t^{\prime}}$ might fulfill $M=\textit{vertices}(C_{t^{\prime}})$ , we define $C(E_{t})$ as the $C_{t^{\prime}}$ that was used in the actual execution of the algorithm to calculate $M$ . $\hfill\blacktriangleleft$

Lemma 13 states that, in any atomic extension, caused by an invocation of $\textit{add}_{C}(op,M)$ , in which incoming edges are added from the nodes in $M$ to the node $o p$ , the set $M$ must correspond to the nodes of a previous version of graph $C$ . Consequently, at most one operation (namely, $o p$ ) is added to graph $C$ in such an extension, since every operation in $M$ is already present in the graph. Furthermore, we can infer that for every time $t\geq 0$ and operation $op\in C_{t}$ , the exist times $t_{1}\leq\dots\leq t_{k}$ such that the set of nodes that have incoming edges to $o p$ in $C_{t}$ is the union of all $\textit{vertices}(C_{t_{i}})$ with $1\leq i\leq k$ , which equals $\textit{vertices}(C_{t_{k}})$ by Lemma 11 (4).

Lemma 14.

The graph $C_{t}$ is transitive for every time $t\geq 0$ .

Proof.

Proof by contradiction. Assume $C_{t}$ is not transitive. There exists $a,b,c\in\textit{vertices}(C_{t})$ with $(a,b),(b,c)\in\textit{edges}(C_{t})$ but $(a,c)\notin\textit{edges}(C_{t})$ . Let us denote the first time $a$ was added to $C$ as $t_{a}$ , and the first time $b$ was added to $C$ as $t_{b}$ (i.e., we have $b\notin\textit{vertices}(C_{t^{\prime}})$ for all $t^{\prime}<t_{b}$ and $b\in\textit{vertices}(C_{t^{\prime}})$ for all $t^{\prime}\geq t_{b}$ ). As we have $(b,c)\in\textit{edges}(C_{t})$ , there must exist a time $t_{\textit{read}}\geq t_{b}$ such that $C_{t_{\textit{read}}}$ was used to add $c$ (or incoming edges to $c$ ) to $C$ . With $(a,c)\notin\textit{edges}(C_{t})$ , we conclude $t_{b}\leq t_{\textit{read}}<t_{a}$ . As we have $(a,b)\in\textit{edges}(C_{t})$ there must have been a read of $C$ after (or at the same time as) $t_{a}$ that was used to add incoming edges to $b$ . Therefore, this read is after $t_{b}$ and must have read $b$ . As $C_{t}$ is irreflexive by Lemma 12, this is a contradiction. $\hfill\blacktriangleleft$

Lemma 15.

The graph $C_{t}$ is acyclic for every time $t\geq 0$ .

Proof.

The graph $C_{t}$ is irreflexive by Lemma 12 and transitive by Lemma 14. Acyclicity follows directly. $\hfill\blacktriangleleft$

Lemma 16.

Let $0\leq t_{1}\leq t_{2}$ , $a\in\textit{vertices}(C_{t_{1}})$ and $b\in\textit{vertices}(C_{t_{2}})-\textit{vertices}(C_{t_{1}})$ . Then for all $t\geq 0$ , $(b,a)\notin C_{t}$ .

Proof.

The claim is trivial for $t_{1}=t_{2}$ . Assume $t_{1}<t_{2}$ . We proceed by contradiction. Suppose that there exists $a\in\textit{vertices}(C_{t_{1}})$ and $b\in\textit{vertices}(C_{t_{2}})-\textit{vertices}(C_{t_{1}})$ , such that, for some time $t^{\prime}\geq 0$ , $(b,a)\in C_{t^{\prime}}$ . Let us call $t_{a}$ the first time when $a$ was committed and $t_{b}$ the first time when $b$ was committed. Since $a\in\textit{vertices}(C_{t_{1}})$ , it follows that $t_{a}\leq t_{1}$ and since $b\in\textit{vertices}(C_{t_{2}})-\textit{vertices}(C_{t_{1}})$ , it follows that $t_{1}<t_{b}$ and therefore $t_{a}<t_{b}$ . Since $(b,a)\in C_{t^{\prime}}$ , it follows that $a$ was committed with $C_{t_{\textit{read}}}$ as dependency with $t_{b}\leq t_{\textit{read}}$ . We conclude $t_{a}<t_{\textit{read}}$ , which contradicts acyclicity proven in Lemma 15. $\hfill\blacktriangleleft$

Lemma 17.

Let $0\leq t_{1}\leq t_{2}$ . There exists a topological ordering $r$ of $C_{t_{2}}$ such that a prefix of $r$ is a topological ordering of $C_{t_{1}}$ .

Proof.

By Lemma 15, there exists a topological ordering $s$ of $C_{t_{2}}$ . By Lemma 16, there are no edges in $C_{t_{2}}$ from nodes in $\textit{vertices}(C_{t_{2}})-\textit{vertices}(C_{t_{1}})$ to those in $\textit{vertices}(C_{t_{1}})$ . Consequently, if we define $r:=r_{1}\cdot r_{2}$ , where $r_{1}$ is the subsequence of $s$ with exactly the nodes in $C_{t_{1}}$ and $r_{2}$ is the subsequence of $s$ with exactly the nodes in $\textit{vertices}(C_{t_{2}})-\textit{vertices}(C_{t_{1}})$ , then $r$ forms a topological ordering of $C_{t_{2}}$ . By Lemma 11 (3), $r_{1}$ is a topological ordering of $C_{t_{1}}$ . $\hfill\blacktriangleleft$

B.2 Commitment and Real-time Ordering

Having established fundamental properties of the ABC Graph when used by the Algorithm 2, most notably acyclicity and, consequently, the existence of topological orderings, in this section we proceed to prove in Lemma 18 that an operation is committed before its corresponding invocation of the $p u b l i s h$ method terminates, and in Lemma 19 that the algorithm satisfies real-time ordering.

Lemma 18.

Upon termination of $\textit{publish}(op)$ , the operation $o p$ is committed.

Proof.

The method publish can return at lines 12, 16 and 24. If $\textit{publish}(op)$ returned at line 12, it had verified that $o p$ is committed in line 11. If $\textit{publish}(op)$ returned at line 16, it committed $o p$ in line 15. If $\textit{publish}(op)$ returned at line 24, it had verified that $o p$ is committed in line 23. Consequently, $o p$ is committed at return. $\hfill\blacktriangleleft$

Lemma 19.

If $\textit{publish}(op)$ precedes $\textit{publish}(op^{\prime})$ , then $o p$ precedes $op^{\prime}$ in every topological ordering of $C_{t}$ for every $t$ after $op^{\prime}$ has been committed.

Proof.

Suppose $\textit{publish}(op)$ precedes $\textit{publish}(op^{\prime})$ . By Lemma 18, $o p$ is committed upon the termination of $\textit{publish}(op)$ . By Lemma 13, there exists a graph $C_{t^{\prime}}$ whose nodes have been used as incoming edges when committing $op^{\prime}$ . Suppose that this graph $C_{t^{\prime}}$ has been read after the termination of $\textit{publish}(op)$ . We therefore have $op\in C_{t^{\prime}}$ , implying that the edge $(op,op^{\prime})$ is added to $C$ by the time $\textit{publish}(op^{\prime})$ terminates. The claim then follows directly.

It remains to show that $C_{t^{\prime}}$ was read after the termination of $\textit{publish}(op)$ . If $op^{\prime}$ was committed by $publish(op^{\prime})$ , $C_{t^{\prime}}$ was read during the execution of $\textit{publish}(op^{\prime})$ and therefore after the termination of $\textit{publish}(op)$ . Otherwise, suppose that $op^{\prime}$ was committed by another invocation $p$ of publish and thus in conflict resolution. The graph $C_{t^{\prime}}$ was read by $p$ in line 28 after some invocation of publish had proposed $op^{\prime}$ to some consensus object. This occurred after $op^{\prime}$ had been booked by $\textit{publish}(op^{\prime})$ (Lemma 11 (2)) and therefore after the termination of publish(op). $\hfill\blacktriangleleft$

B.3 Equivalence of Topological Orderings

After proving the first three claims of Lemma 9, it remains to establish the final two. Before returning to these claims in Section B.4, we first prove Lemma 22 as an intermediate result.

Recall the definition of the graph $C(E_{t})$ from Lemma 13 for an atomic extension $E_{t}$ that is the result of an invocation of $\textit{add}_{C}(op,M)$ . We have $M=\textit{vertices}(C(E_{t}))$ . If $o p$ was added to $C$ for the first time at $E_{t}$ , $C(E_{t})$ consists precisely of those operations of $C_{t}$ (equivalently, of $C_{t+1}$ ) that have an outgoing edge to $o p$ in $C_{t+1}$ .

Definition 20.

Let $E_{t}:=t\rightarrow t+1$ be an atomic extension of the ABC Graph and let this extension be the result of an invocation of $\textit{add}_{C}(op,M)$ . Let $C(E_{t})$ be defined as in Lemma 13, such that $M=\textit{vertices}(C(E_{t}))$ . Furthermore, let $op\not\in C_{t}$ .

We define $P(E_{t})\subseteq C_{t}$ as the subgraph that is disjoint from $C(E_{t})$ .

Given $P(E_{t})$ as defined in Definition 20, for all $op^{\prime}\in C_{t+1}$ , exactly one of the following holds: $op^{\prime}\in C(E_{t})$ , $op^{\prime}\in P(E_{t})$ , or $op^{\prime}=op$ . Note that we only define $P(E_{t})$ in the case of $op\notin C_{t}$ , i.e., $o p$ is committed for the first time. Intuitively, $P(E_{t})$ captures the portion of the graph that was added after $C(E_{t})$ but before $o p$ was added to $C_{t}$ .⁵⁵5The extension(s) from $C(E_{t})$ to $C_{t}$ may include additional edges within $C(E_{t})$ , as well as edges from nodes in $C(E_{t})$ to nodes in $P(E_{t})$ . This information is not represented when partitioning $C_{t}$ in $C(E_{t})$ and $P(E_{t})$ . Although edges from nodes in $C(E_{t})$ to nodes in $P(E_{t})$ may exist, the reverse is ruled out by transitivity (Lemma 14) and the definition of $P(E_{t})$ : if a node in $P(E_{t})$ had an edge to a node in $C(E_{t})$ , it would (by transitivity) also have an edge to $o p$ and thus would belong to $C(E_{t})$ , contradicting disjointness.⁶⁶6Note that $op\notin C_{t}$ by assumption and therefore $(op^{\prime},op)\in C_{t+1}$ implies $op^{\prime}\in C(E_{t})$ for every $op^{\prime}\in C_{t+1}$ .

Definition 21.

Let $G$ be a graph whose nodes are operations, and let $s$ be a sequence of operations. We write $G\cap s$ for the subgraph of $G$ induced by the set of nodes appearing in $s$ .

Lemma 22.

For each fixed $t\geq 0$ , all topological orderings of $C_{t}$ are equivalent. Moreover, this equivalence holds not only for the complete sequences but also for any pair of prefixes consisting of the same set of operations.

Proof.

Let $C_{0}$ , $\dots$ , $C_{t}$ , $C_{t+1}$ , $\dots$ be the states of graph $C$ as it evolves over time. As the induction hypothesis, assume that for all $t^{\prime}\leq t$ , any two topological orderings of $C_{t^{\prime}}$ are equivalent – not only as full sequences, but also in the sense that any pair of prefixes consisting of the same set of operations are themselves equivalent.

As the hypothesis holds trivially for the empty graph $C_{0}$ , it remains to show that this property also holds for $C_{t+1}$ . If the atomic extension $E_{t}:=t\rightarrow t+1$ is the result of an invocation of $\textit{add}_{A}$ or $\textit{add}_{B}$ , we have $C_{t+1}=C_{t}$ and the statement follows directly from the induction hypothesis. If only edges are added during $E_{t}$ , the statement also follows directly from the induction hypothesis, as every topological ordering of $C_{t+1}$ is also a valid topological ordering of $C_{t}$ .

Now suppose that a new operation $o p$ is committed (added to $C$ ) for the first time in the atomic extension $E_{t}$ . Let us consider two prefixes of topological orderings of $C_{t+1}$ that consist of the same set of operations. If $o p$ is not among these operations, the equivalence follows from the induction hypothesis. In the following, we assume that $o p$ is included in both prefixes.

We define two subgraphs to analyze the structural implications of adding $o p$ to $C_{t}$ . First, let $C(E_{t})$ , as defined in Lemma 13, denote the subgraph that has been read when $o p$ was added – that is, every node in $C(E_{t})$ has an outgoing edge to $o p$ . Note that, since $o p$ was newly added, only nodes in $C(E_{t})$ have edges to it in $C_{t+1}$ . As every node in $C(E_{t})$ has an outgoing edge to $o p$ , the nodes in $C(E_{t})$ must appear before $o p$ in any topological ordering of $C_{t+1}$ . Therefore, if a prefix of a topological ordering includes $o p$ , it must also include all nodes of $C(E_{t})$ . Hence, the presence of $o p$ in both prefixes implies that the nodes of $C(E_{t})$ are also included in both prefixes. Second, let $P(E_{t})\subseteq C_{t}$ , as defined in Definition 20, denote the subgraph that is disjoint from $C(E_{t})$ . As $op\notin C_{t}$ , $P(E_{t})$ does not contain $o p$ .

Let $o=o_{0}\cdot op\cdot o_{1}$ be a prefix of a topological ordering of $C_{t+1}$ . Since every node in $C(E_{t})$ has an edge to $o p$ , it follows that $\textit{vertices}(C(E_{t}))\subseteq o_{0}$ . By the induction hypothesis, we have $o_{0}\simeq c\cdot\tilde{o_{0}}$ , where $c$ is any topological ordering of $C(E_{t})$ , and $\tilde{o_{0}}$ is the subsequence of $o_{0}$ containing only those operations not in $C(E_{t})$ .⁷⁷7A subsequence is obtained from a sequence by removing any number of elements from it without changing the order of the remaining elements. The subsequence does not have to appear continuously in the original sequence. Trivially, $o_{0}\cdot o_{1}$ is a topological ordering of $C_{t}$ . Moreover, since there are no edges from nodes in $P(E_{t})$ to nodes in $C(E_{t})$ , we can choose $c$ , the topological ordering of $C(E_{t})$ , such that $c\cdot\tilde{o_{0}}\cdot o_{1}$ is also a topological ordering of $C_{t}$ . This allows us to decompose the topological ordering $o_{0}\cdot o_{1}$ into two parts: $c$ , a topological ordering of $C(E_{t})$ , and $\tilde{o_{0}}\cdot o_{1}$ , a topological ordering of $P(E_{t})\cap o$ . Using $o_{0}\simeq c\cdot\tilde{o_{0}}$ , we conclude $o=o_{0}\cdot op\cdot o_{1}\simeq c\cdot\tilde{o_{0}}\cdot op\cdot o_{1}$ . It remains to show that

\displaystyle c\cdot\tilde{o_{0}}\cdot op\cdot o_{1}\simeq c\cdot\tilde{o_{0}}% \cdot o_{1}\cdot op,

which implies $o\simeq o_{0}\cdot o_{1}\cdot op$ , i.e., that $o p$ can be delayed to the end of the sequence without affecting the resulting state or any response value. Once this is established, the induction hypothesis for $C_{t+1}$ follows from the induction hypothesis for $C_{t}$ and the transitivity of the equivalence relation in the following way. Consider two prefixes $o=o_{0}\cdot op\cdot o_{1}$ and $o^{\prime}=o_{0}^{\prime}\cdot op\cdot o_{1}^{\prime}$ of topological orderings of $C_{t+1}$ , and assume that both prefixes consist of the same set of operations. We conclude

\displaystyle o=o_{0}\cdot op\cdot o_{1}\simeq o_{0}\cdot o_{1}\cdot op\simeq o% _{0}^{\prime}\cdot o_{1}^{\prime}\cdot op\simeq o_{0}^{\prime}\cdot op\cdot o_% {1}^{\prime}=o^{\prime}.

The equivalence $c\cdot\tilde{o_{0}}\cdot op\cdot o_{1}\simeq c\cdot\tilde{o_{0}}\cdot o_{1}% \cdot op$ is shown by Lemma 23 below. $\hfill\blacktriangleleft$

Lemma 23.

Suppose that an operation $o p$ is committed for the first time in the atomic extension $E_{t}:=t\rightarrow t+1$ , and the statement of Lemma 22 holds for every $t^{\prime}$ with $0\leq t^{\prime}\leq t$ .⁸⁸8This is the inductive hypothesis on $C_{t}$ in the proof of the lemma above.

Let $o$ be a prefix of a topological ordering of $C_{t+1}$ that contains $o p$ and let $c$ be a topological ordering of $C(E_{t})$ that is also a prefix of some topological ordering of $C_{t}$ .

For any fixed topological ordering $w$ of $P:=P(E_{t})\cap o$ , all placements of $o p$ in $w$ after $c$ are equivalent, i.e., $c\cdot w_{1}\cdot op\cdot w_{2}\simeq c\cdot w_{1}^{\prime}\cdot op\cdot w_{2}% ^{\prime}$ for all $w_{1}\cdot w_{2}=w_{1}^{\prime}\cdot w_{2}^{\prime}=w$ .

Proof.

We analyze the two cases, depending on whether $o p$ has been committed via the conflict-free or the conflict resolution path, separately. We refer to the statement of Lemma 22 as the Outer Induction Hypothesis.

Case 1: Conflict resolution path.

Let $o p$ be committed via the conflict resolution path. There exists an iteration $\hat{k}$ such that $\textit{CONS}_{\hat{k}}$ stores $o p$ . Let $p$ be the invocation of $p u b l i s h$ that committed $o p$ . As $p$ can reach iteration $\hat{k}$ only if all iterations $k<\hat{k}$ are completed and the outcomes of $\textit{CONS}_{k}.\textit{propose}()$ are added to $C$ (lines 18 and 32), $C(E_{t})$ read by $p$ in line 28 includes all operations stored in $\textit{CONS}_{k}$ with $k<\hat{k}$ . Analogously, an operation committed in a subsequent iteration $k>\hat{k}$ will include $o p$ in its dependencies. Thus, as $P(E_{t})$ is defined as the subgraph of $C_{t}$ induced by $\textit{vertices}(C_{t})-\textit{vertices}(C(E_{t}))$ and $op\notin C_{t}$ , every $op^{\prime}\in P(E_{t})$ has been committed via the conflict-free path.

Let $\hat{p}$ be an invocation of $p u b l i s h$ that proposed $o p$ to $\textit{CONS}_{\hat{k}}$ such that no proposal on that consensus object precedes the proposal of $\hat{p}$ . Note that $\hat{p}$ could be different from $p$ . In line 26, $\hat{p}$ selected an operation, i.e., $o p$ , from $B_{\hat{t}}-\textit{vertices}(C_{\hat{t}})$ with minimal $B$ -value according to the ABC Graph at time $\hat{t}$ , the time of $\hat{p}$ ’s read in line 22.

Consider an arbitrary invocation $p^{\prime}=\textit{publish}(op^{\prime})$ such that $op^{\prime}\notin\textit{vertices}(C_{\hat{t}})$ . If $op^{\prime}\notin B_{\hat{t}}$ , then $p^{\prime}$ will encounter $op\in A$ in line 9, because $op\in\textit{vertices}(B_{\hat{t}})\subseteq A_{\hat{t}}$ . If $op^{\prime}\in B_{\hat{t}}$ , then $B[op^{\prime}]\geq B[op]$ , since $o p$ has minimal $B$ -value for time $\hat{t}$ . Hence, $p^{\prime}$ had or will encounter $op\in A$ in line 9. We conclude, that every invocation $p^{\prime}=\textit{publish}(op^{\prime})$ , such that $op^{\prime}\notin\textit{vertices}(C_{\hat{t}})$ , encounters $op\in A$ in line 9.

Since $\hat{t}$ , the time when $\hat{p}$ read in line 22, precedes $\hat{p}$ ’s proposal in line 27 and no proposal precedes $\hat{p}$ ’s proposal, the read of $C(E_{t})$ in line 28 succeeds $\hat{t}$ . By Lemma 11 (3), $C_{\hat{t}}\subseteq C(E_{t})$ follows. Let $op^{\prime}\in P(E_{t})$ be an arbitrary operation. As established above, $op^{\prime}$ was committed via the conflict-free path before $o p$ was committed. Since $op^{\prime}\in C_{\hat{t}}$ implies $op^{\prime}\in C(E_{t})$ , which is a contradiction, we have $op^{\prime}\notin C_{\hat{t}}$ . As we have shown above, $op^{\prime}$ has found $op\in A$ in line 9. Since $op^{\prime}$ could not have found $op\in C$ , we conclude that $op^{\prime}$ has found $op\in A-\textit{vertices}(C)$ in line 9 and verified commutativity in line 14.

Recall that $o$ is defined as a prefix of a topological ordering of $C_{t+1}$ that contains $o p$ , and that $c$ is defined as a topological ordering of $C(E_{t})$ that is also a prefix of some topological ordering of $C_{t}$ . Let $w$ be a topological ordering of $P:=P(E_{t})\cap o$ . In the following we are showing that all placements of $o p$ in $w$ after $c$ are equivalent. We prove this by induction over $P$ , starting with an empty set and inductively adding operations to $P$ one by one. To define the induction order, we sort the operations according to the recency of the state that the corresponding invocation of publish read in line 9, from the oldest to the most recent. Note that we insert operations in their original place in $w$ such that the relative ordering of $w$ remains the same. We introduce the following notation. Let $w^{j}$ denote the sequences of operations that consists of the first $j$ operations according to the sorting of $P$ that we just defined. Our induction hypothesis is the following:

Inner Induction Hypothesis:: For every fixed prefix $\hat{w}^{j}$ of $w^{j}$ , all placements of $o p$ in $\hat{w}^{j}$ after $c$ are equivalent.
Inner Induction Base Case:: The base case is trivial as $w^{0}$ , and therefore every prefix $\hat{w}^{0}$ , is empty.
Inner Induction Step:: Assume that the induction hypothesis holds true for $0\leq j<|P|$ . Let $\hat{w}^{j+1}$ be a prefix of $w^{j+1}$ . If $\hat{w}^{j+1}$ is also a prefix of $w^{j}$ , the inner induction hypothesis for $j$ applies and we are done. Let $\hat{w}^{j+1}=u^{j}\cdot op^{\prime}\cdot v^{j}$ such that $u^{j}\cdot v^{j}$ is a prefix of $w^{j}$ and $op^{\prime}\in P$ is the next operation, added in this inner induction step. We have to show, that all placements of $o p$ in $\hat{w}^{j+1}$ after $c$ are equivalent. This is done by showing that every placement of $o p$ is equivalent to placing it after $\hat{w}^{j+1}$ . The induction hypothesis for $j+1$ follows by transitivity.

By definition of $\hat{w}^{j+1}$ , we have $c\cdot\hat{w}^{j+1}\cdot op=c\cdot u^{j}\cdot op^{\prime}\cdot v^{j}\cdot op$ . As $c\cdot u^{j}$ is a prefix of some topological ordering of the graph $C_{t}$ we can use the Outer Induction Hypothesis.⁹⁹9By definition, $c$ is a topological ordering of $C(E_{t})$ and a prefix of some topological ordering of $C_{t}$ . It is easy to see that $c\cdot w$ is also a prefix of a topological ordering of $C_{t}$ . When removing operations from $w$ in the reverse order in which they were introduced during the induction, we always remove the operation that read the most recent state in line 9, which therefore cannot have an outgoing edge to any of the remaining operations. By induction, $c\cdot w^{j}$ is a prefix of a topological ordering of $C_{t}$ ; since $u^{j}$ is a prefix of $\hat{w}^{j}$ , which in turn is a prefix of $w^{j}$ , the same holds for $c\cdot\hat{w}^{j}$ and $c\cdot u^{j}$ . Let $c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}$ be a topological ordering of the same prefix of $C_{t}$ , where $c_{op^{\prime}}$ are the operations that $\textit{publish}(op^{\prime})$ read as $C$ in line 9. The Outer Induction Hypothesis gives us $c\cdot u^{j}\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}$ . Note that $u^{j}_{op^{\prime}}\cdot op^{\prime}\cdot v^{j}\cdot op$ is a subset of CUR (the operations in $A-\textit{vertices}(C)$ ) of $\textit{publish}(op^{\prime})$ in line 9. Lemma 5 implies that all placements of $op^{\prime}$ in this set are equivalent. It follows that

	$\displaystyle c\cdot\hat{w}^{j+1}\cdot op$	$\displaystyle=c\cdot u^{j}\cdot op^{\prime}\cdot v^{j}\cdot op$
		$\displaystyle\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}\cdot op^{\prime}% \cdot v^{j}\cdot op$
		$\displaystyle\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}\cdot v^{j}\cdot op% \cdot op^{\prime}$
		$\displaystyle\simeq c\cdot u^{j}\cdot v^{j}\cdot op\cdot op^{\prime}.$

We distinguish two cases, according to whether $o p$ should be placed in $u^{j}$ or $v^{j}$ .

Case 1.1.

To place $o p$ in $u^{j}=(u^{j})_{0}\cdot(u^{j})_{1}$ , where $(u^{j})_{0}\cdot(u^{j})_{1}$ is an arbitrary split of $u^{j}$ , we use the Inner Induction Hypothesis for $j$ in the following way. Note that $u^{j}\cdot v^{j}$ and therefore also $u^{j}$ are prefixes of $w^{j}$ .

	$\displaystyle c\cdot u^{j}\cdot v^{j}\cdot op\cdot op^{\prime}$	$\displaystyle\simeq c\cdot u^{j}\cdot op\cdot v^{j}\cdot op^{\prime}$
		$\displaystyle\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}\cdot op\cdot v^{j% }\cdot op^{\prime}$
		$\displaystyle\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}\cdot op\cdot op^{% \prime}\cdot v^{j}$
		$\displaystyle\simeq c\cdot u^{j}\cdot op\cdot op^{\prime}\cdot v^{j}$
		$\displaystyle\simeq c\cdot(u^{j})_{0}\cdot op\cdot(u^{j})_{1}\cdot op^{\prime}% \cdot v^{j}.$

Case 1.2.

Suppose that $o p$ has to be placed in $v^{j}=(v^{j})_{0}\cdot(v^{j})_{1}$ , where $(v^{j})_{0}\cdot(v^{j})_{1}$ is an arbitrary split of $v^{j}$ .

	$\displaystyle c\cdot u^{j}\cdot v^{j}\cdot op\cdot op^{\prime}$	$\displaystyle\simeq c\cdot u^{j}\cdot(v^{j})_{0}\cdot op\cdot(v^{j})_{1}\cdot op% ^{\prime}$
		$\displaystyle\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}\cdot(v^{j})_{0}% \cdot op\cdot(v^{j})_{1}\cdot op^{\prime}$
		$\displaystyle\simeq c_{op^{\prime}}\cdot u^{j}_{op^{\prime}}\cdot op^{\prime}% \cdot(v^{j})_{0}\cdot op\cdot(v^{j})_{1}$
		$\displaystyle\simeq c\cdot u^{j}\cdot op^{\prime}\cdot(v^{j})_{0}\cdot op\cdot% (v^{j})_{1}.$

We conclude that every placement of $o p$ in $w^{j+1}$ after $c$ is equivalent to placing $o p$ after $c\cdot w^{j+1}$ . Transitivity of the equivalence relation gives us the Inner Induction Hypothesis for $j+1$ . The claim follows from the Inner Induction Hypothesis for $j=|P|$ .

Case 2: Conflict-free path.

Assume now that $o p$ has been committed via the conflict-free path. Let $w$ be a topological ordering of $P$ . Recall that we have to show that every placement of $o p$ in $w$ after $c$ is equivalent. As $o p$ has been committed via the conflict-free path, commutativity with every subset of $\textit{CUR}\cap P$ has been checked. By Lemma 5, for any fixed ordering $p$ of $\textit{CUR}\cap P$ , all placements of $o p$ in $p$ after $c$ are equivalent, i.e., $c\cdot p_{0}\cdot op\cdot p_{1}\simeq c\cdot p_{0}^{\prime}\cdot op\cdot p_{1}% ^{\prime}$ for $p=p_{0}\cdot p_{1}=p_{0}^{\prime}\cdot p_{1}^{\prime}$ . We are therefore concerned about the operations that have been concurrently added and have not been encountered by $o p$ , i.e., $P-CUR$ . Consider $op^{\prime}\in P-CUR$ . By the definition of CUR, $op^{\prime}$ has not been read by $o p$ in $A$ in line 9. Therefore, $op^{\prime}$ could not have been proposed to any consensus object in conflict resolution, as $op^{\prime}$ has a higher $B$ -value than $o p$ , and $o p$ has been booked prior to $op^{\prime}$ . From this we infer that every $op^{\prime}\in P-CUR$ has been added via the conflict-free path. As $op^{\prime}$ has not been found by $o p$ in $A$ in line 9, $op^{\prime}$ has read in line 7 a (proper) superset of what $o p$ has read in line 9 (Lemma 11 (3)). In particular, $op^{\prime}$ has found $op\in A-\textit{vertices}(C)$ in line 9 and verified commutativity in line 14.

To prove that all placements of $o p$ in $w$ after $c$ are equivalent, we follow an argument analogous to that employed in the conflict resolution path case above. In contrast to the conflict resolution path case, we do not need to begin with an empty set before incrementally adding operations. As shown above, we already got the equivalence of all placements of $o p$ in the orderings of subsets of $\textit{CUR}\cap P$ . The operations in $P-CUR$ are handled as in the conflict resolution path case. We sort them according to the recency of the state they read in line 9, from the oldest to the most recent. These operations are then inserted at their original positions in $w$ , thereby preserving the relative ordering within $w$ . We introduce the following notation. Let $w^{j}$ denote the sequences of operations that consists of the operations in $\textit{CUR}\cap P$ as well as the first $j$ operations according to the sorting of $P-CUR$ that we just defined. The Inner Induction Hypothesis and step is identical to the conflict resolution path case. The base case is directly given by Lemma 5 as $o p$ commutes with every subset of $\textit{CUR}\cap P$ . The claim follows directly from the Inner Induction Hypothesis for $j=|P-CUR|$ . $\hfill\blacktriangleleft$

B.4 Proof Completion

Lemmata 15, 18 and 19 correspond exactly to the first three items of Lemma 9. Having established Lemma 22 in the last section, we proceed to show the remaining two items of Lemma 9 in Lemmata 24 and 25, thereby completing the proof of Lemma 9. Finally, we show in Lemma 26 that Algorithm 2 is linearizable.

Lemma 24.

Let $t_{1},t_{2}\geq 0$ , and let $s_{1}$ and $s_{2}$ be topological orderings of $C_{t_{1}}$ and $C_{t_{2}}$ , respectively. For every operation $o p$ such that $op\in s_{1}$ and $op\in s_{2}$ , the sequential specification yields the same return value for $o p$ in both $s_{1}$ and $s_{2}$ .

Proof.

Assume, without loss of generality, $0\leq t_{1}\leq t_{2}$ . Let $s_{1}$ and $s_{2}$ be topological orderings of $C_{t_{1}}$ and $C_{t_{2}}$ , respectively. By Lemma 17, there exists some topological ordering $r=r_{1}\cdot r_{2}$ of $C_{t_{2}}$ such that $r_{1}$ is a topological ordering of $C_{t_{1}}$ . Lemma 22 then implies $r\simeq s_{2}$ and $r_{1}\simeq s_{1}$ . Since $op\in s_{1}$ , we also have $op\in r_{1}$ . With $r_{1}\simeq s_{1}$ , the response value for $o p$ is identical in both $s_{1}$ and $r_{1}$ , and therefore also in $r$ . The claim follows because $r\simeq s_{2}$ . $\hfill\blacktriangleleft$

Lemma 25.

For every time $t_{2}\geq 0$ and every operation $op\in C_{t_{2}}$ , if $o p$ has a response, then there exists a time $t_{1}$ with $0\leq t_{1}\leq t_{2}$ and a topological ordering $T$ of $C_{t_{1}}$ that contains $o p$ , such that the response of $o p$ agrees with the sequential specification applied to $T$ .

Proof.

Since $o p$ has a response, the corresponding $\textit{publish}(op)$ terminated. If $\textit{publish}(op)$ returned at lines 12 or 24, the claim is immediate. Suppose that $\textit{publish}(op)$ returned at line 16. Let $t_{com}\rightarrow t_{com}+1$ be the atomic extension produced by $\textit{add}(op,M)$ in line 15 with $M=\textit{vertices}(C_{t_{read}})$ for some $t_{read}\leq t_{com}$ (Lemma 13). Let $l$ be the topological ordering of $C_{t_{read}}$ that $\textit{publish}(op)$ calculated in line 10.

Case 1: Suppose $op\notin C_{t_{com}}$ .

By Lemma 17, there exists a topological ordering $r=r_{1}\cdot r_{2}$ of $C_{t_{com}}$ such that $r_{1}$ is a topological ordering of $C_{t_{read}}$ , and $r_{2}$ consists of nodes from $\textit{vertices}(C_{t_{com}})-\textit{vertices}(C_{t_{read}})$ . Since $op\notin C_{t_{com}}$ , there is no edge in $C_{t_{com}+1}$ from a node in $\textit{vertices}(C_{t_{com}+1})-\textit{vertices}(C_{t_{read}})$ to $o p$ . Hence, $T:=r_{1}\cdot op\cdot r_{2}$ is a topological ordering of $C_{t_{com}+1}$ . By Lemma 22, $r_{1}$ is equivalent to $l$ , and thus $T$ is equivalent to $l\cdot op\cdot r_{2}$ . Consequently, the response of $o p$ (line 16) agrees with the sequential specification applied to $T$ .

Case 2: Suppose that $op\in C_{t_{com}}$ .

Therefore, there was a preceding commitment of $o p$ . Let $p$ be the process $\textit{publish}(op).p$ and $p^{\prime}$ the process that committed $o p$ for the first time. For the sake of the argument, in the following, we will introduce alternatives to the original run, that we denote by ORUN. For a run $R^{\prime}$ and a process $q$ that can do a step, $R^{\prime}.q$ denotes the run where $q$ makes a step after $R^{\prime}$ , and no other step is made. Since the ABC Graph is linearizable, we view each operation on it as one single step (together with local computations). Furthermore, let $C_{R^{\prime}}$ denote the graph $C$ after the run $R^{\prime}$ .

Let $R$ be the prefix of ORUN right before $p^{\prime}$ commits $o p$ . Since $p$ has not found $o p$ after executing line 9, it is also about to commit $o p$ in the next step and return in line 16. Consequently, $R . p$ , $R.p^{\prime}.p$ and ORUN are indistinguishable for $p$ at the time when $p$ terminates $\textit{publish}(op)$ . In particular, the response value of $o p$ is the same in all runs. An argument analogous to the one used in Case 1 shows that there is a topological ordering $T^{\prime}:=r_{1}\cdot op\cdot r_{2}$ of $C_{R.p}$ with $r_{1}\simeq l$ . Therefore, the response of $o p$ (line 16) agrees with the sequential specification applied to $T^{\prime}$ .

Since $R . p$ is a prefix of $R.p.p^{\prime}$ , the graphs $C_{R.p}$ and $C_{R.p.p^{\prime}}$ belong to the same run $R.p.p^{\prime}$ ¹⁰¹⁰10Let $\hat{t}\geq 2$ be the time at the end of run $R.p.p^{\prime}$ . The graph $C_{R.p}$ appears in run $R.p.p^{\prime}$ at time $\hat{t}-1$ . and therefore Lemma 24 is applicable: The sequential specification yields the same response value for $o p$ in every topological ordering of $C_{R.p}$ and $C_{R.p.p^{\prime}}$ . The same holds for $C_{R.p^{\prime}}$ and $C_{R.p^{\prime}.p}$ analogously. Furthermore, we observe that, as every two add operations on the ABC Graph commute, the graphs $C_{R.p.p^{\prime}}$ and $C_{R.p^{\prime}.p}$ are identical. We conclude that the sequential specification yields the same response for $o p$ in every topological ordering of $C_{R.p}$ and $C_{R.p^{\prime}}$ .

Since the response of $o p$ agrees with the sequential specification applied to a topological ordering of $C_{R.p}$ , namely $T^{\prime}$ , it also agrees with every topological ordering of $C_{R.p^{\prime}}$ . Since $R.p^{\prime}$ is effectively a prefix of the original run ORUN, $C_{R.p^{\prime}}$ is a version of graph $C$ in ORUN. The claim follows directly. $\hfill\blacktriangleleft$

Lemma 26.

Algorithm 2 is a linearizable universal construction. Moreover, for any run of the algorithm, every topological ordering of the final graph $C$ is a linearization of the induced history.

Proof.

To prove the claim, we have to show that, for any given sequential specification and any finite run of Algorithm 2, a topological ordering of the final graph $C$ is a linearization of the induced history.¹¹¹¹11Note that the implementation of universal construction presented in Algorithm 2 exports the method $\textit{publish}(op)$ , whereas the object specified by the sequential specification exports the method $o p$ directly. This difference does not affect correctness and can be disregarded when reasoning about equivalences of histories. Let $H$ be the history of a run $R$ of Algorithm 2. Let $C_{R}$ denote the graph $C$ at the end of run $R$ . Let $S$ be a topological ordering of $C_{R}$ . Lemma 15 guarantees the existence of such a topological ordering. As a sequence of operations, $S$ forms a sequential history. It remains to show that $S$ serves as a linearization of $H$ . By Definition 2, $S$ must be equivalent¹²¹²12Note the distinction between equivalence of histories (Definition 1) and equivalence of sequences of operations (Definition 3). to a completion of $H$ , preserve the precedence relation of $H$ and be legal.

By Lemmata 18 and 19, $S$ is equivalent to a completion of $H$ and preserves the precedence relation of $H$ . It remains to show legality, i.e., that $S$ satisfies the sequential specification. For each operation $o p$ in $S$ , the response must agree with the sequential specification applied to $S$ . For operations in $S$ that do not have a response, we can assign one according to the sequential specification applied to $S$ , which trivially satisfies legality.

Let $o p$ be an operation in $S$ that has a response. By Lemma 25, there exists a topological ordering $T$ of $C_{t}$ for some time $t\geq 0$ that contains $o p$ , such that the response of $o p$ agrees with the sequential specification applied to $T$ . By Lemma 24, the sequential specification yields the same response for $o p$ in both $T$ and $S$ , i.e., the response of $o p$ agrees with the sequential specification applied to $S$ .

Since this holds for every operation in $S$ , each operation returned the value prescribed by the sequential specification in $S$ . Hence, $S$ is legal. We conclude that $S$ is a linearization of $H$ , and therefore that Algorithm 2 is linearizable. $\hfill\blacktriangleleft$

Appendix C Universal Construction – Proof of Wait-Freedom

Having established the linearizability of Algorithm 2 in the previous section, we now address its liveness guarantees, specifically proving in Lemma 27 that it satisfies wait-freedom, assuming that the underlying shared objects itself are wait-free. The underlying objects are a snapshot object $K$ (line 2), an ABC Graph $G$ (line 3), and a sequence of consensus objects $\textit{CONS}_{j}$ for $j\geq 1$ (line 4). We showed in Section A, that Algorithm 1 is a wait-free linearizable implementation of an ABC Graph.

Lemma 27.

The universal construction given in Algorithm 2 is wait-free. Each invocation of publish terminates at most after $c+2$ iterations of conflict resolution, for the maximum level of concurrency $c\leq n$ .

Proof.

Let $p$ be a process that executes $\textit{publish}(op)$ .

Case 1.

Suppose $p$ verifies commitment of $o p$ in line 11 or the commutativity in line 14. It is immediate that the number of steps it can take before terminating $\textit{publish}(op)$ is finite.

Case 2.

Suppose $p$ fails to verify the commitment of $o p$ in line 11 and fails to verify the commutativity property in line 14. Let $k_{0}$ denote the value of $k\geq 0$ read by $p$ in line 18 and let $c\leq n$ be the maximum level of concurrency, i.e., the maximum number of processes that can propose operations concurrently. We prove by contradiction that $\textit{publish}(op)$ terminates at latest in iteration $k_{0}+c+2$ .

Assume, for the sake of contradiction, that $\textit{publish}(op)$ does not terminate by iteration $k_{0}+c+2$ . Since it did not return in iteration $k_{0}+1$ , $o p$ was not decided by any $\textit{CONS}_{k}$ with $k\leq k_{0}$ ; otherwise, $o p$ would have been committed and $\textit{publish}(op)$ would have returned at line 24 in iteration $k_{0}+1$ . From iteration $k_{0}+1$ onward, $\textit{publish}(op)$ executes the conflict resolution procedure; hence, each $k$ with $k_{0}+1\leq k\leq k_{0}+c+1$ , $\textit{CONS}_{k}$ decides on an operation different from $o p$ . Otherwise, $\textit{publish}(op)$ would terminate in iteration $k+1$ .

Let us consider the $c$ different iterations with $k_{0}+2\leq k\leq k_{0}+c+1$ and the operations stored in $\textit{CONS}_{k}$ . Since $c$ is the concurrency bound, among those $c$ operations there exists an operation $op^{\prime}$ such that $\textit{publish}(op^{\prime})$ was not active at the moment when $p$ read $k_{0}$ . Either $\textit{publish}(op^{\prime})$ terminated before $p$ read $k_{0}$ or $\textit{publish}(op^{\prime})$ was invoked afterwards.

Case 2.1.

Suppose $\textit{publish}(op^{\prime})$ was invoked after $p$ read $k_{0}$ . The $B$ -value of $op^{\prime}$ will be higher than $B[op]$ . Furthermore, every process that encounters $op^{\prime}$ in line 22 will also encounter $o p$ with a lower $B$ -value. Consequently, no process would propose $op^{\prime}$ to a consensus object $\textit{CONS}_{k}$ with $k_{0}+2\leq k\leq k_{0}+c+1$ . This contradicts the validity of $\textit{CONS}_{k}$ .

Case 2.2.

Suppose $\textit{publish}(op^{\prime})$ terminated before $p$ read $k_{0}$ . By Lemma 18, $op^{\prime}$ is committed before $p$ read $k_{0}$ and consequently before any process executed line 22 in iteration $k_{0}+2$ ; otherwise, $p$ would have read at least $k_{0}+1$ in line 18. Consequently, no process would propose $op^{\prime}\in C$ to a subsequent consensus object, contradicting validity of consensus.

We conclude that the assumption that $\textit{publish}(op)$ does not terminate by iteration $k_{0}+c+2$ leads to a contradiction. Therefore, Algorithm 2 is wait-free. $\hfill\blacktriangleleft$

Appendix D Universal Construction – Proof of Dynamic Concurrency

After proving linearizability and wait-freedom of Algorithm 2, we show in Lemma 28 that the algorithm satisfies dynamic concurrency according to Definition 7.

Lemma 28.

The universal construction given in Algorithm 2 is dynamically concurrent.

Proof.

Let $H$ be an arbitrary history induced by a run of Algorithm 2 and $\textit{publish}(op)$ an operation in $H$ . Assume that process $\textit{publish}(op).p$ used a strong synchronization primitive while executing $\textit{publish}(op)$ and, thus, executed conflict resolution for $o p$ . Therefore, the conditions in lines 11 and 14 failed for $\textit{publish}(op)$ .

Let $t^{\prime}$ be the time when $\textit{publish}(op).p$ read the ABC Graph in line 9. It remains to show that there exists a set of operations $O$ with $O^{\prime\prime}:=A_{t^{\prime}}-\textit{vertices}(C_{t^{\prime}})-\{op\}\subseteq O$ such that $(l,O)$ is a configuration during $o p$ in $H$ for $l:=\textit{linearize}(C_{t^{\prime}})$ .

Let $C_{H}$ be the graph $C$ at the end of the run that induced $H$ . By Lemma 26, every topological ordering of $C_{H}$ is a linearization of $H$ . By Lemma 16, no operation in $\textit{vertices}(C_{H})-\textit{vertices}(C_{t^{\prime}})$ has an edge to an operation in $\textit{vertices}(C_{t^{\prime}})$ . Therefore, there exists a topological ordering $\hat{l}=\hat{l}_{0}\cdot\hat{l}_{1}$ of $C_{H}$ and thus a linearization of $H$ such that $op^{\prime}\in\hat{l}_{0}$ if and only if $op^{\prime}\in C_{t^{\prime}}$ for all $op^{\prime}\in C_{H}$ . Since $\hat{l}_{0}$ is also a topological ordering of $C_{t^{\prime}}$ , we have $l\simeq\hat{l}_{0}$ by Lemma 22. Thus, $L:=l\cdot\hat{l}_{1}$ is a linearization of $H$ and $l$ a prefix of $L$ . Furthermore, since $\textit{publish}(op).p$ executed conflict resolution, it failed the condition $op\in C_{t^{\prime}}$ in line 11. We therefore have $op\notin l$ .

Let $H^{\prime}$ be the maximal prefix of $H$ such that $op^{\prime}.res\in H^{\prime}$ implies $op^{\prime}\in l$ for every operation $op^{\prime}$ . We have to show $op.inv\in H^{\prime}$ and $op.res\notin H^{\prime}$ . Since $H^{\prime}$ is maximal, it excludes $o p . i n v$ only if there exists an operation $op^{\prime}\notin l$ with $op^{\prime}.res<_{H}op.inv$ . Let $op^{\prime}$ be an operation such that $op^{\prime}.res$ precedes $o p . i n v$ in $H$ . By Lemma 18, $op^{\prime}$ is committed upon termination of $\textit{publish}(op^{\prime})$ . Therefore, we have $op^{\prime}\in C_{t^{\prime}}$ and consequently $op^{\prime}\in l$ . Thus, $op.inv\in H^{\prime}$ holds. Finally, $op.res\notin H^{\prime}$ is implied by $op\notin l$ .

Furthermore, we have to show that for all $op^{\prime}\in l$ , it holds that $op^{\prime}.inv\in H^{\prime}$ . Suppose, for the sake of contradiction, that there exists $op^{\prime}\in l$ with $op^{\prime}.inv\notin H^{\prime}$ . Since $H^{\prime}$ is maximal, $op^{\prime}.inv\notin H^{\prime}$ implies that there exists $op^{\prime\prime}\notin l$ with $op^{\prime\prime}.res<_{H}op^{\prime}.inv$ . By Lemma 19, $op^{\prime\prime}$ precedes $op^{\prime}$ in every topological ordering of $C_{t^{\prime}}$ . This contradicts $op^{\prime\prime}\notin l$ . We conclude that $op^{\prime}.inv\in H^{\prime}$ for all $op^{\prime}\in l$ .

We now have to show that $l$ is a linearization of $H^{\prime}$ . By construction, $l$ is a prefix of $L$ , where $L$ is a linearization of $H$ . Consequently, $l$ is a legal sequential history. Since $H^{\prime}$ is a prefix of $H$ , $l$ preserves the precedence relation of $H^{\prime}$ , as the precedence relation of $H^{\prime}$ is a subset of that of $H$ . It remains to show that $l$ is equivalent to a completion of $H^{\prime}$ . As established above, we have $op^{\prime}.inv\in H^{\prime}$ for all $op^{\prime}\in l$ and, by construction, $op^{\prime}\in l$ for all $op.res\in H^{\prime}$ . Hence, we can construct a completion $\hat{H^{\prime}}$ of $H^{\prime}$ such that $op^{\prime}\in\hat{H^{\prime}}$ if and only if $op^{\prime}\in l$ . It remains to show that $l$ is equivalent to $\hat{H^{\prime}}$ according to Definition 1. Suppose, for the sake of contradiction, that $l$ and $\hat{H^{\prime}}$ are not equivalent. Hence, there exist some process $p^{\prime}$ and operations $op^{\prime},op^{\prime\prime}\in\hat{H^{\prime}}\mid p^{\prime}$ such that $op^{\prime}<_{\hat{H^{\prime}}}op^{\prime\prime}$ but $op^{\prime\prime}<_{l}op^{\prime}$ . This leads to a contradiction, since $op^{\prime}<_{\hat{H^{\prime}}}op^{\prime\prime}$ implies $op^{\prime}<_{H^{\prime}}op^{\prime\prime}$ , which in turn implies $op^{\prime}<_{H}op^{\prime\prime}$ , then $op^{\prime}<_{L}op^{\prime\prime}$ , and finally $op^{\prime}<_{l}op^{\prime\prime}$ . Therefore, $l$ is equivalent to $\hat{H^{\prime}}$ , a completion of $H^{\prime}$ , and consequently, $l$ is a linearization of $H^{\prime}$ .

It remains to show that $O^{\prime\prime}=A_{t^{\prime}}-\textit{vertices}(C_{t^{\prime}})-\{op\}$ is a subset of the set $O$ of all operations $op^{\prime}$ for which $op^{\prime}.inv\in H^{\prime}$ , $op^{\prime}\notin l$ , and $op^{\prime}\neq op$ . Let $op^{\prime}\in O^{\prime\prime}$ . By definition of $O^{\prime\prime}$ , we have $op^{\prime}\neq op$ and $op^{\prime}\notin\textit{vertices}(C_{t^{\prime}})$ and therefore $op^{\prime}\notin l$ . Suppose, for the sake of contradiction, that $op^{\prime}.inv\notin H^{\prime}$ . By definition of $H^{\prime}$ , there must exist an operation $op^{\prime\prime}\notin l$ such that $op^{\prime\prime}.res$ precedes $op^{\prime}.inv$ ; otherwise, $H^{\prime}$ would not be maximal. It follows from $op^{\prime}\in O^{\prime\prime}\subseteq A_{t^{\prime}}$ that time $t^{\prime}$ , when $\textit{publish}(op).p$ read the ABC Graph in line 9, succeeds $op^{\prime}.inv$ and therefore $op^{\prime\prime}.res$ . Lemma 18 contradicts $op^{\prime\prime}\notin C_{t^{\prime}}$ , i.e., $op^{\prime\prime}\notin l$ . This contradiction proves $O^{\prime\prime}\subseteq O$ . The claim follows from Definition 7. $\hfill\blacktriangleleft$

[bib.bib1] [1] Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. Atomic snapshots of shared memory. J. ACM, 40(4):873–890, September 1993. doi:10.1145/153724.153741.

[bib.bib2] [2] Vitaly Aksenov, Vincent Gramoli, Petr Kuznetsov, Di Shang, and Srivatsan Ravi. Optimal concurrency for list-based sets. In Victor Malyshkin, editor, PaCT, volume 12942 of Lecture Notes in Computer Science, pages 386–401. Springer, 2021. doi:10.1007/978-3-030-86359-3_29.

[bib.bib3] [3] J. Aspnes and M. Herlihy. Wait-free data structures in the asynchronous pram model. In Proceedings of the Second Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA ’90, pages 340–349, New York, NY, USA, 1990. Association for Computing Machinery. doi:10.1145/97444.97701.

[bib.bib4] [4] Hagit Attiya, Rachid Guerraoui, Danny Hendler, and Petr Kuznetsov. The complexity of obstruction-free implementations. J. ACM, 56(4):24:1–24:33, 2009. doi:10.1145/1538902.1538908.

[bib.bib5] [5] Hagit Attiya and Jennifer L. Welch. Distributed computing - fundamentals, simulations, and advanced topics (2. ed.). Wiley series on parallel and distributed computing. Wiley, 2004.

[bib.bib6] [6] Rida Bazzi and Maurice Herlihy. Clairvoyant state machine replication. Information and Computation, 285:104701, 2022. doi:10.1016/J.IC.2021.104701.

[bib.bib7] [7] Austin T. Clements, M. Frans Kaashoek, Nickolai Zeldovich, Robert T. Morris, and Eddie Kohler. The scalable commutativity rule: designing scalable software for multicore processors. In Michael Kaminsky and Mike Dahlin, editors, SOSP, pages 1–17. ACM, 2013. doi:10.1145/2517349.2522712.

[bib.bib8] [8] James A. Cowling, Daniel S. Myers, Barbara Liskov, Rodrigo Rodrigues, and Liuba Shrira. HQ replication: A hybrid quorum protocol for byzantine fault tolerance. In Brian N. Bershad and Jeffrey C. Mogul, editors, OSDI, pages 177–190. USENIX Association, 2006. URL: http://www.usenix.org/events/osdi06/tech/cowling.html.

[bib.bib9] [9] Tudor David, Rachid Guerraoui, and Vasileios Trigonakis. Asynchronized concurrency: The secret to scaling concurrent search data structures. In ASPLOS, pages 631–644, 2015. doi:10.1145/2694344.2694359.

[bib.bib10] [10] Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. JACM, 32(2):374–382, April 1985. doi:10.1145/3149.214121.

[bib.bib11] [11] Eli Gafni. Round-by-round fault detectors (extended abstract): unifying synchrony and asynchrony. In PODC, pages 143–152, 1998.

[bib.bib12] [12] Vincent Gramoli, Petr Kuznetsov, and Srivatsan Ravi. In the search for optimal concurrency. In Jukka Suomela, editor, SIROCCO, volume 9988 of Lecture Notes in Computer Science, pages 143–158, 2016. doi:10.1007/978-3-319-48314-6_10.

[bib.bib13] [13] Rachid Guerraoui, Petr Kuznetsov, Matteo Monti, Matej Pavlovic, and Dragos-Adrian Seredinschi. The consensus number of a cryptocurrency. In PODC, 2019. URL: https://arxiv.org/abs/1906.05574.

[bib.bib14] [14] Maryam Helmi, Lisa Higham, and Philipp Woelfel. Strongly linearizable implementations: possibilities and impossibilities. In Darek Kowalski and Alessandro Panconesi, editors, PODC ’12, pages 385–394. ACM, 2012. doi:10.1145/2332432.2332508.

[bib.bib15] [15] Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124–149, 1991. doi:10.1145/114005.102808.

[bib.bib16] [16] Maurice Herlihy, Victor Luchangco, and Mark Moir. Obstruction-free synchronization: Double-ended queues as an example. In 23rd International Conference on Distributed Computing Systems (ICDCS 2003), 19-22 May 2003, Providence, RI, USA, pages 522–529. IEEE Computer Society, 2003. doi:10.1109/ICDCS.2003.1203503.

[bib.bib17] [17] Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463–492, July 1990. doi:10.1145/78969.78972.

[bib.bib18] [18] Amos Israeli and Lihu Rappoport. Disjoint-access-parallel implementations of strong shared memory primitives. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, PODC ’94, pages 151–160, 1994. doi:10.1145/197917.198079.

[bib.bib19] [19] Idit Keidar, Eleftherios Kokoris-Kogias, Oded Naor, and Alexander Spiegelman. All you need is DAG. In Avery Miller, Keren Censor-Hillel, and Janne H. Korhonen, editors, PODC ’21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021, pages 165–175. ACM, 2021. doi:10.1145/3465084.3467905.

[bib.bib20] [20] Ramakrishna Kotla, Lorenzo Alvisi, Mike Dahlin, Allen Clement, and Edmund Wong. Zyzzyva: speculative byzantine fault tolerance. In Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, pages 45–58, 2007.

[bib.bib21] [21] Milind Kulkarni, Donald Nguyen, Dimitrios Prountzos, Xin Sui, and Keshav Pingali. Exploiting the commutativity lattice. In Mary W. Hall and David A. Padua, editors, PLDI, pages 542–555. ACM, 2011. doi:10.1145/1993498.1993562.

[bib.bib22] [22] Milind Kulkarni, Dimitrios Prountzos, Donald Nguyen, and Keshav Pingali. Defining and implementing commutativity conditions for parallel execution. In Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM, 2009.

[bib.bib23] [23] Leslie Lamport. The Part-Time parliament. ACM Transactions on Computer Systems, 16(2):133–169, May 1998. doi:10.1145/279227.279229.

[bib.bib24] [24] Leslie B Lamport. Generalized paxos, apr13 2010. US Patent 7,698,465. URL: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-33.pdf.

[bib.bib25] [25] Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno M. Preguiça, and Rodrigo Rodrigues. Making geo-replicated systems fast as possible, consistent when necessary. In Chandu Thekkath and Amin Vahdat, editors, 10th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2012, Hollywood, CA, USA, October 8-10, 2012, pages 265–278. USENIX Association, 2012. URL: https://www.usenix.org/conference/osdi12/technical-sessions/presentation/li.

[bib.bib26] [26] M.C. Loui and H.H. Abu-Amara. Memory requirements for agreement among unreliable asynchronous processes. Advances in Computing Research, 4:163–183, 1987.

[bib.bib27] [27] Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system, 2008.

[bib.bib28] [28] Miguel Pires, Srivatsan Ravi, and Rodrigo Rodrigues. Generalized paxos made byzantine (and less complex). Algorithms, 11(9):141, 2018. doi:10.3390/A11090141.

[bib.bib29] [29] Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22(4):299–319, December 1990. doi:10.1145/98163.98167.

[bib.bib30] [30] Alexander Spiegelman, Balaji Arun, Rati Gelashvili, and Zekun Li. Shoal: Improving DAG-BFT latency and robustness. In Jeremy Clark and Elaine Shi, editors, Financial Cryptography and Data Security - 28th International Conference, FC 2024, Willemstad, Curaçao, March 4-8, 2024, Revised Selected Papers, Part I, volume 14744 of Lecture Notes in Computer Science, pages 92–109. Springer, 2024. doi:10.1007/978-3-031-78676-1_6.

[bib.bib31] [31] Alexander Spiegelman, Neil Giridharan, Alberto Sonnino, and Lefteris Kokoris-Kogias. Bullshark: DAG BFT protocols made practical. In Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi, editors, Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, pages 2705–2718. ACM, 2022. doi:10.1145/3548606.3559361.

[bib.bib32] [32] Andrei Tonkikh, Pavel Ponomarev, Petr Kuznetsov, and Yvonne-Anne Pignolet. Cryptoconcurrency: (almost) consensusless asset transfer with shared accounts. In Weizhi Meng, Christian Damsgaard Jensen, Cas Cremers, and Engin Kirda, editors, CCS, pages 1556–1570. ACM, 2023. doi:10.1145/3576915.3616587.

[bib.bib33] [33] Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, 151(2014):1–32, 2014.

[bib.bib34] [34] Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan-Gueta, and Ittai Abraham. Hotstuff: BFT consensus with linearity and responsiveness. In Peter Robinson and Faith Ellen, editors, PODC, pages 347–356. ACM, 2019. doi:10.1145/3293611.3331591.