How Exhaustive Does an Extension-Based Proof Need to Be?

In the iterated immediate snapshot model, there are $n\ge 2$ processes, $p_1,\mathrm{\dots },p_n$, that communicate using an infinite sequence, $S_1,S_2,\mathrm{\dots }$, of shared snapshot objects. Each snapshot object has $n$ components, which are all initially blank (denoted by $-$), and supports two operations, $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}(v)$, for values $v\ne -$, and $\mathrm{𝗌𝖼𝖺𝗇}()$. An $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}(v)$ operation by $p_i$ sets the $i$th component of the object to have value $v$. A $\mathrm{𝗌𝖼𝖺𝗇}()$ operation returns a vector containing the value of each component of the object.

A (full-information) protocol is described using a function $\delta$ from the set of possible process states to $O\cup \{\perp \}$, where $O$ is a set of possible output values that does not include $\perp$. The initial state of each process $p_i$ is a pair, $(i,x_i)$, which consists of its identifier, $i$, and its input, $x_i$. The $t$’th time that $p_i$ is scheduled, it performs an $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ to $S_t$ with its current state as the value and then performs a $\mathrm{𝗌𝖼𝖺𝗇}$ on $S_t$. The new state of $p_i$ is the pair $(i,r_{i,t})$, where $r_{i,t}$ is the result of this $\mathrm{𝗌𝖼𝖺𝗇}$. If $\delta$ returns an output value for this state, then $p_i$ outputs that value and terminates. Otherwise, $\delta$ returns $\perp$. In this case, $p_i$ remains active and will access the next snapshot object, $S_{t+1}$, when it is next scheduled.

A configuration (of a protocol) consists of the states of each process and the contents of each snapshot object at some point during an execution when each process is either poised to perform an $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ or has already terminated. In an initial configuration, each process is in an initial state and the contents of all snapshot objects are blank. An important property of the iterated immediate snapshot model is that the contents of the snapshot objects in a configuration can be inferred from the states of the processes, so a configuration is often described by its set of process states.

An execution of a protocol is an alternating sequence $\alpha =C_0,Q_1,C_1,Q_2,C_2,\mathrm{\dots }$ of configurations and nonempty subsets of processes. For $t\ge 1$, the processes in $Q_t$ are all poised to $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ the same snapshot object in $C_{t-1}$. Configuration $C_t=C_{t-1}{Q}_t$ results from configuration $C_{t-1}$ when the processes in $Q_t$ perform their pending $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$s (in any order), immediately followed by their pending $\mathrm{𝗌𝖼𝖺𝗇}$s (in any order, after processes in $Q_t$ have all performed their $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾𝗌}$). The execution is finite if it ends with a configuration and is terminating if it ends with a configuration in which every process is terminated. It is $P$-only, for some set of processes $P$, if $Q_t\subseteq P$ for all $t\ge 1$. A configuration $C^{\prime }$ is reachable from another configuration $C$ if there is an execution $\alpha$ that starts with $C$ and ends with $C^{\prime }$. This is denoted by $C^{\prime }=C\alpha$. Configuration $C^{\prime }$ is reachable if it is reachable from an initial configuration.

Given any execution $\alpha$ from an initial configuration, there is an execution ${\alpha }^{\prime }$ from the same initial configuration that is indistinguishable from $\alpha$ to all processes, such that all operations on each snapshot object $S_t$ occur before any operation on snapshot object $S_{t^{\prime }}$, for all . This is because operations on different snapshot objects commute with one another.

A t-round execution of a protocol is an execution from an initial configuration in which each process appears in exactly $t$ subsets of processes within the execution (i.e. it has performed exactly one $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ and $\mathrm{𝗌𝖼𝖺𝗇}$ operation on each of the first $t$ snapshot objects) or it has terminated after performing fewer than $t$ $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ and $\mathrm{𝗌𝖼𝖺𝗇}$ operations. A configuration is round-based if it is reachable via a $t$-round execution, for some $t\ge 0$. If $C$ is a round-based configuration, then a 1-round execution from $C$ is an execution starting from $C$ in which each process that is not terminated in $C$ performs exactly one $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ and one $\mathrm{𝗌𝖼𝖺𝗇}$ on the same snapshot object. More generally, if $C$ is a configuration in which each process in $P$ is poised to $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ the same snapshot object or has terminated before accessing that snapshot object, then a t-round, P-only execution from $C$ is a $P$-only execution from $C$ in which each process in $P$ appears in exactly $t$ subsets or has terminated before performing $t$ $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ and $\mathrm{𝗌𝖼𝖺𝗇}$ operations.

For each $n\ge 2$ and each $1\le x\le n$, a protocol among $n$ processes is $x$-obstruction-free if, for each subset $P$ consisting of at most $x$ processes and for each configuration $C$ reachable via some initial configuration, all $P$-only executions starting from $C$ are finite. A protocol among $n$ processes is wait-free if it is $n$-obstruction-free.

An(abstract) simplex $\sigma$ is a non-empty finite subset of some universe. Each element of $\sigma$ is a vertex of $\sigma$ and each non-empty subset of $\sigma$ is a face of $\sigma$. An (abstract) simplicial complex $ℂ$ is a collection of simplices that is closed under subset: if $\sigma \in ℂ$ and ${\sigma }^{\prime }$ is a face of $\sigma$, then ${\sigma }^{\prime }\in ℂ$. A simplex is a facet of $ℂ$ if it is not a face of any other simplex in $ℂ$. The set $V(ℂ)$ of vertices of $ℂ$ is the union $\cup \{\sigma \mid \sigma \in ℂ\}$ of the vertices of simplices in $ℂ$. A subcomplex of $ℂ$ is any subset of $ℂ$ that is itself a simplicial complex. Given a set of vertices $V\subseteq V(ℂ)$, the subcomplex of $ℂ$ induced by $V$ is the set of all simplices $\sigma \in ℂ$ such that $\sigma \subseteq V$. Notice that a simplex $\sigma$ together with all its faces form a simplicial complex. The boundary of $\sigma$, denoted by $\partial \sigma$, is the subcomplex consisting of all proper faces ${\sigma }^{\prime }⊊\sigma$.

Let $G$ be the graph with vertex set $V(ℂ)$ whose edges are the 2-vertex simplices in $ℂ$. Two vertices of $ℂ$ are adjacent (or neighbours) if they are adjacent in $G$. The distance between two vertices of $ℂ$ is the length of a shortest path between them in $G$. A vertex is adjacent to (or is a neighbour of) a subcomplex $𝔸\subseteq ℂ$ if the vertex is not in $V(𝔸)$, but is adjacent to some vertex in $V(𝔸)$.

A task $𝕋$ may be formalized in the language of combinatorial topology as a triple $𝕋=(𝕀,𝕆,\mathrm{\Delta })$, where $𝕀$ and $𝕆$ are simplicial complexes, called the input and output complexes of the task, and $\mathrm{\Delta }:𝕀\to 2^{𝕆}$ is a task specification map from $𝕀$ to the set of all subcomplexes of $𝕆$. Additionally, $\delta$ is required to be a carrier map. This means that $\mathrm{\Delta }({\sigma }^{\prime })\subseteq \mathrm{\Delta }(\sigma )$ for all ${\sigma }^{\prime }\subseteq \sigma \in 𝕀$.

The input complex $𝕀$ represents the set of initial configurations of any protocol for $𝕋$. Each simplex in $𝕆$ represents a correct (partial) assignment of outputs to processes. $\mathrm{\Delta }$ encodes the input/output specifications of the task. A task is finite if its input complex is finite.

Let $\delta$ be a protocol in the iterated immediate snapshot model. For $t\ge 0$, it is also possible to represent the set of all configurations of $\delta$ reachable via $t$-round executions as a simplicial complex, ${ℂ}^t$. Specifically, each such configuration $C$ is represented by an $n$-vertex simplex $\sigma \subseteq {ℂ}^t$ whose vertices are the states of the processes in $C$. The color of a vertex is the identifier of the process whose state it represents. We say that a vertex is terminated if it represents the state of a terminated process. Otherwise, we say that it is unterminated.

Given a simplex $\sigma \in {ℂ}^t$ with no terminated vertices, its chromatic subdivision, $\chi (\sigma ,\delta )$, is the the subcomplex of ${ℂ}^{t+1}$ induced by the vertex set $V(\chi (\sigma ,\delta ))=\{(i,\tau )\mid \tau \subseteq \sigma \text{ is a face that contains a vertex with color }i\}$. The simplices of $\chi (\sigma ,\delta )$ are the nonempty subsets of $V(\chi (\sigma ,\delta ))$ with the property that, for any two vertices $(i,\tau )$ and $(j,{\tau }^{\prime })$ that belong to the same subset, $i\ne j$ and either $\tau \subseteq {\tau }^{\prime }$ or ${\tau }^{\prime }\subseteq \tau$.

More generally, suppose $\sigma$ is an arbitrary simplex in ${ℂ}^t$. Let $W=\{s\in V(\sigma )\mid \delta (s)\ne \perp \}$ be the terminated vertices in $\sigma$ and let $\tau \subseteq \sigma$ be the simplex induced by the unterminated vertices of $\sigma$. If $W\ne \mathrm{\varnothing }$, then $\chi (\sigma ,\delta )$ is the simplicial complex whose vertex set is $W\cup V(\chi (\tau ,\delta ))$ and whose faces are of the form $W^{\prime }\cup \rho$, where $W^{\prime }\subseteq W$ and $\rho \in \chi (\tau ,\delta )$ is a simplex.

Note that, if ${\sigma }^{\prime }\subseteq \sigma$, then $\chi ({\sigma }^{\prime },\delta )\subseteq \chi (\sigma ,\delta )$. Moreover, if $\sigma$ represents a round-based configuration, $C$, and $Q=\{p_i\mid i\text{ is the first component}$ $\text{of some vertex in }{\sigma }^{\prime }\}$, then each facet of $\chi ({\sigma }^{\prime },\delta )$ is the set of states of processes in $Q$ at the end of some 1-round, $Q$-only execution from $C$. (The processes in $Q$ that are terminated in $C$ do not take steps in this execution.) In particular, each $n$-vertex simplex of $\chi (\sigma ,\delta )$ represents a configuration obtained from $C$ via a 1-round execution.

For each subcomplex $𝔸\subseteq {ℂ}^t$, we define $\chi (𝔸,\delta )=\cup \{\chi (\sigma ,\delta )|\sigma \in 𝔸$ is a simplex$\}\subseteq ℂ{}^{t+1}$. Note that, if ${𝔸}^{\prime }\subseteq 𝔸$ is a subcomplex, then $\chi ({𝔸}^{\prime },\delta )\subseteq \chi (𝔸,\delta )$. Hoest and Shavit [18] showed that ${ℂ}^{t+1}=\chi ({ℂ}^t,\delta )$, for all $t\ge 0$. Given a subcomplex $𝔸\subseteq {ℂ}^t$, we use ${\chi }^0(𝔸,\delta )$ to denote $𝔸$ and, for $k\ge 0$, we use ${\chi }^{k+1}(𝔸,\delta )$ to denote $\chi ({\chi }^k(𝔸,\delta ),\delta )\subseteq {ℂ}^{t+k+1}$. In particular, for all $t\ge 0$, ${ℂ}^t={\chi }^t(𝕀,\delta )$. For any $k\ge 0$ and any $n$-vertex simplex $\sigma \subseteq {ℂ}^t$ representing a configuration $C$ reachable via a $t$-round execution, the set of all configurations reachable from $C$ via $k$-round executions is represented by ${\chi }^k(\sigma ,\delta )$.

For any $n$-vertex simplex $\sigma \in 𝕀$, each $(n-1)$-vertex simplex $\tau \in {\chi }^t(\sigma ,\delta )$ is a face of at most two $n$-vertex simplices in ${\chi }^t(\sigma ,\delta )$ (see [16], Chapter 9). If $\tau$ is a face of exactly one $n$-vertex simplex in ${\chi }^t(\sigma ,\delta )$, then we say that $\tau$ is on the boundary of ${\chi }^t(\sigma ,\delta )$. Otherwise, we say that $\tau$ is in the interior of ${\chi }^t(\sigma ,\delta )$.

A protocol $\delta$ for $𝕋$ is safe if the outputs of the terminated processes in each execution from an initial configuration represented by $\sigma$ are represented by a simplex contained in $\mathrm{\Delta }(\sigma )$. Note that a safe protocol is not necessarily wait-free. In particular, a protocol in which no process terminates is safe. Finally, $\delta$ is uniform if there is a constant $M$ such that, in every execution, every process terminates after performing exactly $M$ $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ operations and $\mathrm{𝗌𝖼𝖺𝗇}$ operations.

In a colorless protocol, processes make decisions ignoring all information about process identifiers and the number of times the same information appears in a $\mathrm{𝗌𝖼𝖺𝗇}$. The colorless states of processes are defined inductively from their states: If the initial state of process $p_i$ is $(i,x_i)$, then its initial colorless state is simply its input value, $x_i$. Assume that each process that has not terminated after its $(t-1)$’th step has a well-defined colorless state. Then, for each such process $p_i$, its new colorless state after obtaining a $\mathrm{𝗌𝖼𝖺𝗇}$ result $r$ from snapshot object $S_t$ is the set $\{c_j\mid r[j]\ne -\text{ and }{c}_j\text{ is the colorless state of }r[j]\}$. In particular, a colorless state does not record the number of times each colorless state at the end of the previous round occurs in the result of a $\mathrm{𝗌𝖼𝖺𝗇}$. In general, it is not possible to determine the previous colorless states of a process from its current colorless state. Thus, colorless protocols are not full-information protocols.

Given a configuration $C$ of $\delta$, its colorless configuration, $D$, is the set of colorless states of the process states in $C$. A colorless configuration $D^{\prime }$ is reachable from $D$ if there exists a configuration reachable from $C$ whose colorless configuration is $D^{\prime }$. A colorless configuration is reachable if it is reachable from an initial colorless configuration.

Executions of a colorless protocol have a simpler combinatorial representation using simplicial complexes. For each $t\ge 0$, the simplicial complex, ${𝔹}^t$ represents the set of all colorless configurations of $\delta$ reachable via $t$-round executions. Specifically, each such colorless configuration is a facet of ${𝔹}^t$. If $\sigma$ contains no terminated vertex, then the barycentric subdivision, $\beta (\sigma ,\delta )$, of $\sigma$ is a simplicial complex whose vertices are the non-empty subsets of $V(\sigma )$. Its simplices are the nonempty subsets of $V(\beta (\sigma ,\delta ))$ with the property that, for any two vertices $\tau$ and ${\tau }^{\prime }$ that belong to the same subset, either $\tau \subseteq {\tau }^{\prime }$ or ${\tau }^{\prime }\subseteq \tau$. The barycenter of $\beta (\sigma ,\delta )$ is the vertex $V(\sigma )$. If $𝔸$ is a simplicial complex such that $\delta (v)=\perp$ for all $v\in V(𝔸)$, then the barycentric subdivision, $\beta (𝔸,\delta )$, of $𝔸$ is the union of $\beta (\sigma ,\delta )$ for all simplices $\sigma \subseteq 𝔸$. For uniform colorless protocols, $\delta$, it is known that ${𝔹}^{t+1}=\beta ({𝔹}^t,\delta )$. (See Chapter 4 of [16].)

More generally, suppose $\sigma$ is a simplex representing an arbitrary colorless configuration reachable via a $t$-round execution. Let $W=\{s\in V(\sigma )|\delta (s)\ne \perp \}$ be the terminated vertices in $\sigma$ and let $\tau \subseteq \sigma$ be the simplex induced by the unterminated vertices of $\sigma$. If $W\ne \mathrm{\varnothing }$, then $\beta (\sigma ,\delta )$ is the simplicial complex whose vertex set is $W\cup V(\beta (\tau ,\delta ))$ and whose faces are of the form $W^{\prime }\cup \rho$, where $W^{\prime }\subseteq W$ and $\rho \subseteq \beta (\tau ,\delta )$ is a simplex. Using essentially the same argument as in Hoest and Shavit [18], it is possible to show that ${𝔹}^{t+1}=\beta ({𝔹}^t,\delta )$, for all $t\ge 0$. Furthermore, $\beta$ maps every subcomplex $𝔸\subseteq {𝔹}^t$ to a subcomplex $\beta (𝔸,\delta )\subseteq {𝔹}^{t+1}$. Given a subcomplex $𝔸\subseteq {𝔹}^t$, we use ${\beta }^0(𝔸,\delta )$ to denote $𝔸$ and, for $k\ge 0$, we use ${\beta }^{k+1}(𝔸,\delta )$ to denote $\beta ({\beta }^k(𝔸,\delta ),\delta )\subseteq {𝔹}^{t+k+1}$.

Consider any task $T=(𝕀,𝕆,\mathrm{\Delta })$ among $n\ge 2$ processes that has no wait-free solution in the iterated immediate snapshot model. An extension-based proof of (the impossibility of) $T$ is an interaction between a prover and a protocol $\delta$ that claims to solve $T$. The goal of the prover is to find a bad execution of the protocol: an execution that is either infinite in length or one that where processes output values that violate the task specification. The interaction proceeds in phases.

At the start of each phase $\phi \ge 1$, the prover has a set, $A(\phi )$, of reachable configurations of protocol $\delta$. These configurations differ from one another only in the states of processes that are still in their initial states. (In other words, the prover has committed to an execution and a set of initial configurations that are indistinguishable from the first configuration in the execution to all processes that appear in the execution.) $A(1)$ is the set of all initial configurations of $\delta$. Throughout phase $\phi$, the prover maintains a set of configurations, $A^{\prime }(\phi )$, that it has reached from configurations in $A(\phi )$. This set is empty at the start of phase $\phi$.

In each phase $\phi$, the prover can ask queries to find out information about the protocol. For a single-step query, the prover specifies a configuration $C\in A(\phi )\cup A^{\prime }(\phi )$ and a nonempty set $Q$ of processes that are poised to $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ the same snapshot object in configuration $C$. The protocol responds to this query with information about the configuration $C^{\prime }=CQ$. More specifically, for each process in $Q$, the protocol returns $\delta (v)$, where $v$ is the state of that process in configuration $C^{\prime }$. This is sufficient information for the prover to know everything about configuration $C^{\prime }$. Then the prover adds $C^{\prime }$ to $A^{\prime }(\phi )$. If the outputs in configuration $C^{\prime }$ do not satisfy the specifications of $T$, then the prover wins, since it has demonstrated that $\delta$ is incorrect.

A chain of (single-step) queries is a (finite or infinite) sequence of consecutive single-step queries $(C_1,Q_1),(C_2,Q_2),\mathrm{\dots }$ such that $C_1,Q_1,C_2,Q_2,\mathrm{\dots }$ is an execution from $C_1$. If the prover constructs an infinite chain of queries, it wins, since it has demonstrated that $\delta$ is not wait-free.

For an output query, the prover specifies a configuration $C\in A(\phi )\cup A^{\prime }(\phi )$, a set $Q$ of processes that are poised to $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ the same snapshot object in configuration $C$, and an output value $y$. If there is a $Q$-only execution from $C$ that ends in a configuration in which some process in $Q$ outputs $y$, then the protocol responds with the sequence of sets of processes scheduled in some such execution. Otherwise, the protocol says that no such execution exists.

An assignment query is a generalization of an output query. Instead of specifying an output value $y$, the prover now needs to specify a function $f:Q^{\prime }\to V(𝕆)$, where $Q^{\prime }$ is some non-empty subset of $Q$. Similar to an output query, if there is a $Q$-only execution from $C$ that ends in a configuration in which every process $p\in Q^{\prime }$ outputs $f(p)$, then the protocol responds with the sequence of sets of processes scheduled in some such execution. Otherwise, the protocol says that no such execution exists.

The prover must end the current phase after asking a finite number of output queries and chains of queries. To end phase $\phi$, the prover chooses a configuration $C\in A^{\prime }(\phi )$. If all processes are terminated in configuration $C$, then the prover loses. Otherwise, phase $\phi +1$ begins, with $A(\phi +1)$ consisting of $C$ and any configuration that differs from $C$ only in the states of processes that are still in their initial states.

The prover wins if there are an infinite number of phases in the interaction, since it has demonstrated that the protocol is not wait-free. It also wins if the protocol gives it inconsistent responses.

For a length query, the prover specifies a configuration $C\in A(\phi )\cup A^{\prime }(\phi )$ and a nonempty set $Q$ of processes that are poised to $\mathrm{𝗎𝗉𝖽𝖺𝗍𝖾}$ the same snapshot object in configuration $C$. The protocol responds with an upper bound on the length of a longest $Q$-only execution from $C$, or $\mathrm{\infty }$, if there is an infinite $Q$-only execution from $C$.

A $k$-exhaustive extension-based proof is a generalization of an (augmented) extension-based proof that allows the prover to ask length queries for sets of processes of size at most $k$, in addition to chains of queries and assignment queries.

It is easy to obtain an $n$-exhaustive extension-based proof of the impossibility of any task among $n\ge 2$ processes that has a finite input complex, but no deterministic, wait-free solution. For each initial configuration $C$, the prover performs a length query for $C$ and the set of all processes. If the protocol’s response to this query is $\mathrm{\infty }$, then a length query for some one-round extension of $C$ and the set of all processes must also return $\mathrm{\infty }$. In this case, the prover will be able to inductively construct an infinite execution of the protocol, which demonstrates that the protocol is not wait-free. If the protocol’s response is $r$, the prover performs all possible chains of queries from $C$. If any of these chains continues for more than $r$ steps, the prover wins, since the protocol has provided inconsistent information. For each configuration reached in which some processes are terminated, the prover checks that the outputs of these processes satisfy the specifications of the task. If not, the prover wins, since the protocol is incorrect. If at any point during this interaction the prover receives conflicting information (for example, a process producing different outputs in two configurations that are indistinguishable to this process), the prover wins. Since the protocol is not a deterministic, wait-free solution to the task, one of these conditions must eventually happen.

Consider the 2-set agreement task among $n=3$ processes. Let $𝕀$ denote the input complex for this task and let $\delta$ be an arbitrary protocol with input complex $𝕀$. Note that a round-based configuration is represented by a triangle and its boundary assignment (if it has one) can be obtained by performing chromatic subdivisions on its edges.

For the 2-set agreement task, we call an edge in a boundary assignment special if one of its endpoints is assigned output 0 by $\delta$ and its other endpoint is assigned output 1 by $\delta$. Let $B$ be the property such that, for any $n$-vertex simplex $\sigma$ representing a round based configuration $C$ that has a boundary assignment under $\delta$, $B(\partial (\sigma ,\delta ))$ is true if and only if some output of $\partial (\sigma ,\delta )$ does not satisfy validity or $\partial (\sigma ,\delta )$ has an odd number of special edges.

Consider the initial configuration $C$ represented by the simplex $\sigma =\{v_0,v_1,v_2\}$, where $v_i=(p_i,i)$ represents process $p_i$ with input value $i$, for each $i\in \{0,1,2\}$. Suppose that $C$ has a boundary assignment $\partial (\sigma ,\delta )$ that satisfies validity. Vertices in $\partial (\sigma ,\delta )$ that represent states of processes in terminating $\{p_i,p_j\}$-only executions are assigned either $i$ or $j$ as outputs. It follows that all special edges in $\partial (\sigma ,\delta )$ lie on the subdivision of the edge $\{v_0,v_1\}$ of $\sigma$. The two vertices at the ends of this subdivided edge represent solo-executions by $p_0$ and by $p_1$, which must output 0 and 1, respectively. It follows that the outputs of the vertices along this subdivided edge switch between 0 and 1 an odd number of times, which gives an odd number of special edges.

In the full version of the paper, we show that any non-terminal round-based configuration whose boundary assignment satisfies $B$ has a one-round extension whose boundary assignment also satisfies $B$. This is proved via a cancellation argument similar to the proof of two-dimensional Sperner’s lemma [6].

Finally, if a configuration $C^{\prime }$ is terminal, then its boundary assignment defines the outputs of its three vertices. Notice that if ${\sigma }^{\prime }$ is the simplex representing $C^{\prime }$, then it is impossible for ${\sigma }^{\prime }$ to have three special edges. Furthermore, in the case that ${\sigma }^{\prime }$ has exactly one special edge, the set of outputs produced by the processes must be $\{0,1,2\}$, which violates agreement. Hence, if $B(\partial ({\sigma }^{\prime },\delta ))$ is true, then the outputs of processes in configuration $C^{\prime }$ violate either validity or agreement.

More generally, for $(n-1)$-set agreement with $n\ge 2$, we can define $B$ to be the predicate such that the boundary assignment of a round-based configuration satisfies $B$ if and only if its outputs do not satisfy validity for $(n-1)$-set agreement or it contains an odd number of $(n-1)$-vertex simplices whose vertices are assigned different values in $\{0,1,\mathrm{\dots },n-2\}$ by $\delta$.

In the weak symmetry breaking task, processes do not have inputs. Each process that does not crash must output either 0 or 1, with the restriction that, if no processes crash, at least one process must output 0 and at least one process must output 1. It is known that weak symmetry-breaking has a wait-free protocol from registers when the number of processes, $n$, is not a prime power [10].

The class of zero-one exclusion tasks was introduced by Gafni [14]. Each of the tasks in this class further restricts the outputs when some of the processes do not participate (i.e. take no steps). Thus, any solution to a zero-one exclusion task is a solution to weak symmetry breaking. More specifically, a zero-one exclusion task among $n\ge 2$ processes is specified by a sequence of $n-1$ bits $b(1),b(2),\mathrm{\dots },b(n-1)$. In any execution where exactly processes participate, the task requires that not all $k$ processes output $b(k)$. Gafni gave a reduction from any zero-one exclusion task to set agreement and proved that some zero-one exclusion tasks are strictly weaker than set agreement. Gafni and Herlihy [15] gave a characterization of zero-one exclusion tasks that have wait-free protocols from registers using combinatorial topology.

We consider the zero-one exclusion tasks among 3 processes. The input complex $𝕀$ consists of a single triangle, ${\sigma }_0=\{p_0,p_1,p_2\}$, where each vertex represents an inputless process. For $b(1)=b(2)=0$, the task ${𝔼}_{00}=(𝕀,{𝕆}_{00},{\mathrm{\Delta }}_{00})$ requires that at least one process output 1 in any execution and, if all 3 processes participate, then at least one process must also output 0. In other words, a process must output 1 in a solo-terminating execution, if 2 processes run by themselves, they cannot both output 0, and if all 3 processes produce output values, both 0 and 1 are output. The task ${𝔼}_{01}=(𝕀,{𝕆}_{01},{\mathrm{\Delta }}_{01})$ is defined similarly. A process must output 1 in a solo-terminating execution, if 2 processes run by themselves, they cannot both output 1, and if all 3 processes participate, both 0 and 1 are output. There are two other zero-one exclusion tasks among 3 processes that can be obtained from ${𝔼}_{00}$ and ${𝔼}_{01}$ by interchanging 0 and 1 and are computationally equivalent to them.

Let $\delta$ be an arbitrary protocol with input complex $𝕀$ and binary output values. For each vertex $v$ that represents the state of a terminated process $p_i$, define its label (with respect to $\delta$) to be the quantity $i+\delta (v)mod3$. We call an edge of a boundary assignment special if one of its endpoints has label 0 and its other endpoint has label 1. Define the property $B_{00}$ to be such that, for any $n$-vertex simplex $\sigma$ representing a round-based configuration $C$ that has a boundary assignment under $\delta$, $B_{00}(\partial (\sigma ,\delta ))$ is true if and only if the output values in $\partial (\sigma ,\delta )$ do not satisfy the specification of the task ${𝔼}_{00}$ or $\partial (\sigma ,\delta )$ has an odd number of special edges.

Suppose that ${\sigma }_0$ has a boundary assignment $\partial ({\sigma }_0,\delta )$ that satisfies specification of ${𝔼}_{00}$. Each edge $\{p_i,p_j\}$ of ${\sigma }_0$ is subdivided into an odd number of edges in the protocol complex. This is because the vertices along the subdivided edge must alternate between states of $p_i$ and states of $p_j$, where the vertices on the ends of the path represent states of $p_i$ and $p_j$ at the end of their solo-executions. From the specification of $E_{00}$, these two vertices both output 1. Furthermore, no edge in $\partial ({\sigma }_0,\delta )$ has output 0 at both of its endpoints. Hence, if there is an edge $\{u,v\}$ in the subdivision of $\{p_i,p_j\}$ such that $\delta (u)=0$ and $\delta (v)=1$, then there is an another edge $\{u,w\}$ in this subdivision such that $\delta (w)=1$. The remaining edges in the subdivision of $\{p_i,p_j\}$ are assigned output 1 at both endpoints. There are an odd number of such edges.

In the subdivision of $\{p_0,p_1\}$, an edge is special if and only if both endpoints output 0, which does not occur. In the subdivision of $\{p_1,p_2\}$, an edge is special if and only if the endpoint corresponding to $p_2$ outputs 1 and the endpoint corresponding to $p_1$ outputs 0. As above, such a special edge is adjacent to another special edge in the subdivision of $\{p_1,p_2\}$. This gives an even number of special edges in the subdivision of $\{p_1,p_2\}$. In the subdivision of $\{p_0,p_2\}$, an edge is special if and only if both processes output 1. As above, there are an odd number of such edges. In total, this gives an odd number special edges in $\partial ({\sigma }_0,\delta )$.

The argument used for set-agreement can also be applied here to show that any non-terminal round-based configuration whose boundary assignment satisfies $B_{00}$ has a 1-round extension whose boundary assignment also satisfies $B_{00}$.

Finally, if ${\sigma }^{\prime }$ is the triangle that represents a terminal configuration, then it is impossible for ${\sigma }^{\prime }$ to have three special edges. In the case that ${\sigma }^{\prime }$ has exactly one special edge, the set of labels on its vertices must be $\{0,1,2\}$. This is only possible if all three processes output 0 or if all three processes output 1, which violates the task specification, as it fails to break symmetry.

We now generalize the constructions described in Section 3.1 and Section 3.2 to arbitrary tasks with no deterministic wait-free solutions.

Given a task $𝕋=(𝕀,𝕆,\mathrm{\Delta })$, a boundary property of $𝕋$ is a predicate $B$ that maps each boundary assignment $\partial (\sigma ,\delta )$ to true or false, where $\delta$ is any protocol with input complex $𝕀$ and $\sigma$ is any $n$-vertex simplex $\sigma$ that represents a round-based configuration of the protocol $\delta$. For proving impossibility results about tasks, we need a bad boundary property, $B$, which means that for any protocol $\delta$ with input complex $𝕀$, $B$ is initially bad, extendable, and dangerous, where

• $\mathrm{■}$

  $B$ is initially bad if there is an initial configuration that either has no boundary assignment or has a boundary assignment that satisfies $B$,

• $\mathrm{■}$

  $B$ is extendable if every boundary assignment of a non-terminal round-based configuration that satisfies $B$ has a one-round extension that either has no boundary assignment or has a boundary assignment that satisfies $B$, and

• $\mathrm{■}$

  $B$ is dangerous if, for every boundary assignment of a terminal configuration that satisfies $B$, the outputs of its processes violate the specification of $𝕋$.

We prove that, for any finite task $𝕋=(𝕀,𝕆,\mathrm{\Delta })$ among $n\ge 2$ processes with no deterministic, wait-free solution, there is a bad boundary property $B_{𝕋}$ for $𝕋$. Then Theorem 4 follows from the proof strategy described at the beginning of Section 3.

Consider an arbitrary finite task $𝕋=(𝕀,𝕆,\mathrm{\Delta })$ among $n\ge 2$ processes. If $\delta$ is a protocol with input complex $𝕀$ and $C$ is a round-based configuration reachable from some initial configuration of $\delta$, then we say that $\delta$ locally solves $𝕋$ from $C$ if $\delta$ has no infinite execution starting from $C$ and the outputs produced in all executions starting from $C$ satisfy the specification of $𝕋$. We define the canonical bad boundary property $B_{𝕋}$ of $𝕋$ to be the predicate such that, for each protocol $\delta$ with input complex $𝕀$ and for each $n$-vertex simplex $\sigma$ that represents a round-based configuration $C$ of $\delta$ that has a boundary assignment, $B_{𝕋}(\partial (\sigma ,\delta ))$ is true if and only if

• $\mathrm{■}$

  the outputs in $\partial (\sigma ,\delta )$ do not satisfy the specification of $𝕋$ or

• $\mathrm{■}$

  the outputs in $\partial (\sigma ,\delta )$ satisfy the specification of $𝕋$, but there is no protocol ${\delta }^{\prime }$ that locally solves $𝕋$ from $C$ for which $\partial (\sigma ,{\delta }^{\prime })=\partial (\sigma ,\delta )$.

In particular, if $\sigma$ represents a configuration consisting of only terminated processes, then $B_{𝕋}(\partial (\sigma ,\delta ))$ is true if and only if the outputs of the vertices of $\sigma$ do not satisfy the specification of $𝕋$. Thus, $B_{𝕋}$ is dangerous, by definition.

The next lemma shows that, if the boundary assignments of a finite set of round-based configurations of $\delta$ do not satisfy $B_{𝕋}$, then there exists a protocol that locally solves $𝕋$ simultaneously from all these configurations.

In particular, if $D$ is the set of all initial configurations and each of them has a boundary assignment that does not satisfy $B_{𝕋}$, then there is a wait-free protocol for $𝕋$.

The next lemma shows that $B_{𝕋}$ is extendable.

Our main result in this section follows from Corollary 2, Lemma 3, and the fact that canonical bad boundary properties are dangerous.

The property $B$ defined for 2-set agreement in Section 3.1 implies the canonical bad boundary property for 2-set agreement. To see why, let $\sigma$ be a triangle representing a round-based configuration $C$ in a protocol $\delta$. If the boundary assignment of $\sigma$ has an odd number of 0-1 edges, then, by a generalization of Sperner’s lemma, any wait-free protocol ${\delta }^{\prime }$ that agrees with $\delta$ on the boundary assignment of $\sigma$ must have at least one execution starting from $C$ that leads to a configuration in which three different values are output by the three processes. In other words, there is no protocol that locally solves 2-set agreement from $C$ that also agrees with $\delta$ on the boundary assignment of $C$.

In general, to show that a finite task has no deterministic, wait-free solution, it suffices to define an explicit boundary property for the task and prove that this boundary property is initially bad, extendable, and dangerous. In the examples for set-agreement and zero-one exclusion tasks, the bad boundary properties we gave are computable. However, this is not the case for the canonical bad boundary properties defined in this section. Furthermore, a bad canonical boundary property is shown to be bad under the assumption that the task is impossible. Thus, the results we presented in this section do not immediately yield impossibility results for arbitrary tasks.

The argument by Alistarh, Aspnes, Ellen, Gelashvili and Zhu [1, 2] that there is no extension-based proof for $(n-1)$-set agreement among $n$ processes constructed a partially defined protocol $\delta$ while maintaining the invariant that states which output different values are sufficiently far away from one another. This is not possible for $\mathrm{\ell }$-exhaustive extension-based proofs when $\mathrm{\ell }\ge 2$. For example, the prover can ask length queries for all sets of 2 processes from all initial configurations and then perform all possible chains of queries involving at most 2 process from all initial configurations. The set of states reached form a single connected component of the protocol complex and include states in which each of the values in $\{0,1,\mathrm{\dots },n-1\}$ is output.

For simplicity, we will construct $\delta$ so that it is colorless. This is without loss of generality, as the prover must be able to handle arbitrary protocols. As we respond to the prover’s queries during the first phase, we update $\delta$ while maintaining a number of invariants.

First, we ensure that $\delta$ is defined for every colorless state $s$ in every colorless configuration that the prover has reached, i.e., $\delta (s)$ is either set to $\perp$ or an output value. If $\delta (s)$ is defined for some colorless state $s$ reachable via an $r$-round execution, then $\delta (s^{\prime })$ is defined for every colorless state $s^{\prime }$ reachable via an $(r-1)$-round execution. Moreover, if $\delta (s)=\perp$, then $\delta (s^{\prime })$ is defined for every colorless state $s^{\prime }$ reachable via an $r$-round execution. Hence, there is an integer $t\ge 0$ such that $\delta$ is defined on all colorless states reachable via $r$-round executions, for all , and $\delta$ is only defined on terminated colorless states reachable via $t$-round executions.

More formally, let ${𝔹}^0$ be the simplicial complex representing the set of all initial colorless configurations of the $k$-set agreement task, i.e., ${𝔹}^0$ consists of an $n$-vertex simplex with one vertex corresponding to each of the possible inputs, as well as all faces of this simplex.

In the first phase, we ensure that $\delta$ appears to be solving $k$-set agreement, from the perspective of the prover. In particular, we ensure that, in any colorless configuration reached by the prover, there are at most $k$ different output values, each of which is valid. Additionally, if a colorless configuration reached by the prover has at least one non-terminated colorless state, then there are at most $k-1$ different output values. This is crucial when we fully define $\delta$, at the end of the first phase.

Now consider colorless configurations reachable via $t$-round executions that each contains a colorless state on which $\delta$ is undefined and another colorless state on which $\delta$ outputs a value. We further ensure that it is possible to assign valid output values to the undefined colorless states in these configurations so that at most $k-1$ values are output in any of these configurations. Note that this will still leave many parts of the protocol undefined.

More formally, let $t\ge 0$ be the integer in Invariant 1, and let $U$ be an arbitrary set of vertices in ${𝔹}^t$ on which $\delta$ is undefined. The extension of $\delta$ by a function $\gamma :U\to \{0,1,\mathrm{\dots },n-1\}$ is the protocol ${\delta }^{\prime }$ such that ${\delta }^{\prime }(u)=\gamma (u)$, for each vertex in $u\in U$, and ${\delta }^{\prime }(v)=\delta (v)$, for each vertex $v\notin U$ on which $\delta (v)$ is defined. We say ${\delta }^{\prime }$ is good if, in every colorless configuration represented by a simplex $\sigma \in {𝔹}^t$, the protocol outputs at most $k$ different values, each of which is valid, and furthermore, if $\sigma$ has at least one unterminated vertex, then the protocol outputs at most $k-1$ different values.

At any point during the interaction, we can prolong the protocol by setting $\delta (v)=\perp$, for every undefined vertex $v\in {𝔹}^t$. It is one way of responding to a query and sometimes it is the only thing we can do. Intuitively, it provides us more room to assign outputs in future rounds, similar to how it was used in [2].

Finally, we describe our strategy for responding to queries so that the invariants are maintained. Initially, before any queries are made, $\delta (s)=\perp$ for every initial colorless state $s$ and is undefined for every other colorless state. The invariants hold with $t=1$. In particular, Invariant 2 is vacuously true.

Now suppose that the invariants hold immediately before a query by the prover. Recall that each query involves a previously reached configuration $C$ and a set of (at most $k-1$) processes $Q$ that are all poised to access the same snapshot object $S_{r+1}$ in $C$, for some $r\ge 0$ (so all processes in $Q$ have taken exactly $r$ steps). Let $\sigma$ be the set of colorless states of processes in $Q$ in configuration $C$. Then $\sigma$ is a simplex in ${𝔹}^r$. Let $t\ge 0$ be the integer in Invariant 1 immediately before the query. Since every process in $Q$ is poised to access the same snapshot object, $\delta (v)=\perp$ for every $v\in V(\sigma )$, which implies that . We consider step queries, length queries, and assignment queries separately.

Since the prover does not win in the first phase, it must eventually end the first phase and commit to a non-empty execution $\alpha$.

By Invariant 1, there is an integer $t\ge 0$ such that $\delta$ is defined on every vertex in ${𝔹}^r$ for all and $\delta (v)\ne \perp$ for any vertex $v$ in ${𝔹}^t$. We first prolong the protocol twice to create ${𝔹}^{t+2}$, so that each terminated vertex in ${𝔹}^{t+2}$ is a terminated vertex in ${𝔹}^t$. Let $N$ be the set of undefined neighbours of the terminated vertices in ${𝔹}^{t+2}$. By Invariant 2, there is a good extension ${\delta }^{\prime }$ of $\delta$ by a function $\gamma :N\to \{0,1,\mathrm{\dots },n-1\}$. For each vertex $v\in N$, set $\delta (v)={\delta }^{\prime }(v)$. Since ${\delta }^{\prime }$ is good, for every reachable configuration that has an unterminated process, the processes output at most $k-1$ different output values, each of which is valid.

Let $x$ be the input value of any process that is scheduled in the first step of $\alpha$. Notice that $x$ is a valid output value for every process in any extension that extends $\alpha$. Consider any colorless state $s$ reachable by a $t$-round execution that begins with $\alpha$. If $\delta (s)$ is undefined, then set $\delta (s)=x$. Then every extension of $\alpha$ is finite. This fully defines $\delta$ for every colorless configuration the prover can reach from the second phase onwards. Note that at most $k$ different output values are produced in any such reachable configuration. In the full version of the paper, we extend this partially defined protocol, which only appears to be wait-free to the prover, into a correct $k$-obstruction-free protocol solving $k$-set agreement.