An Algorithmic Approach to the Asynchronous Computability Theorem

TL;DR

This paper provides the first complete description and proof of correctness for the convergence algorithm, an alternative, algorithmic proof of the asynchronous computability theorem in distributed computing.

Contribution

It offers the first comprehensive description and validation of the convergence algorithm, complementing the combinatorial proof of the ACT.

Findings

Complete description of the convergence algorithm

Proof of correctness for the convergence algorithm

Bridges combinatorial and algorithmic proofs of the ACT

Abstract

The asynchronous computability theorem (ACT) uses concepts from combinatorial topology to characterize which tasks have wait-free solutions in read-write memory. A task can be expressed as a relation between two chromatic simplicial complexes. The theorem states that a task has a protocol (algorithm) if and only if there is a certain chromatic simplicial map compatible with that relation. While the original proof of the ACT relied on an involved combinatorial argument, Borowsky and Gafni later proposed an alternative proof that relied on a algorithmic construction, termed the "convergence algorithm". The description of this algorithm was incomplete, and presented without proof. In this paper, we give the first complete description, along with a proof of correctness.

Figures

Equations

$$\Gamma :\mathcal{K}\to 2^{\mathcal{L}},$$

$$y=\sum _{i=0}^n{t}_i\cdot x_i,$$

$$\mathrm{S}{\mathrm{t}}^{\circ }(\sigma )=\bigcup _{\tau \supseteq \sigma }\mathrm{Int}\tau .$$

$$f(\mathrm{Int}|\alpha |)\subseteq \bigcap _{a\in \alpha }\mathrm{S}{\mathrm{t}}^{\circ }(\phi (a))=\mathrm{S}{\mathrm{t}}^{\circ }(\phi (\alpha )),$$

$$\mu :\mathrm{Div}(\mathcal{I})\to \mathcal{O}$$

$$\varphi :{\mathrm{Ch}}^N\mathcal{I}\to \mathrm{Div}\mathcal{I},$$

$${\mathrm{Ch}}^N\mathcal{I}\stackrel{\varphi }{\to }\mathrm{Div}\mathcal{I}\stackrel{\mu }{\to }\mathcal{O}.$$

$$c_p^r=\bigcap _{j\in J}{w}_{p_j}^r,$$

$${\bar{c}}_p^r=\bigcap _{k\in K}{c}_{p_k}^r$$

$${\mathcal{C}}_p^r=\mathrm{Lk}(\bigcap _{k\in K}{c}_{p_k}^r,\bigcup _{k\in K}{P}_{p_k}^r).$$

$$w_p^r=\bigcup _{i\in I}{s}_{p_i}^r\cup \bigcap _{i\in I}{\bar{c}}_{p_i}^r-\{u_p^r\}$$

$$w_p^{r+1}=\bigcup _{i\in I}{s}_{p_i}^{r+1}\cup \bigcap _{i\in I}{\bar{c}}_{p_i}^{r+1}-\{u_p^{r+1}\}$$

$$\bigcup _{i\in I}{s}_{p_i}^{r+1}=s_{p_{\ell }}^{r+1}$$

$$\bigcap _{i\in I}{\bar{c}}_{p_i}^{r+1}\subseteq {\bar{c}}_{p_{\ell }}^{r+1}$$

$$w_p^{r+1}=\bigcup _{i\in I}{s}_{p_i}^{r+1}\cup \bigcap _{i\in I}{\bar{c}}_{p_i}^{r+1}-\{u_p^{r+1}\}\subseteq s_{p_{\ell }}^r\cup {\bar{c}}_{p_{\ell }}^{r+1}.$$

$$w_{p^{\prime }}^{r+1}=\bigcup _{i\in I}{s}_{p_i}^{r+1}\cup \bigcap _{i\in I}{\bar{c}}_{p_i}^{r+1}-\{u_{p^{\prime }}^r\}.$$

$$u\in \bigcap _{i\in I}{\bar{c}}_{p_i}^{r+1}\subseteq w_{p^{\prime }}^{r+1}$$

$$\Delta (V)\times \mathrm{Bary}(\mathrm{Div}(\mathcal{I}))\times \mathrm{Bary}(\mathcal{I}),$$

$$f:|\mathcal{A}|\to |\mathcal{B}|$$

$$f^m:|{\mathrm{skel}}^m(\mathcal{A})|\to |\mathcal{B}|$$

$$f^{m+1}:|{\mathrm{skel}}^{m+1}(\mathcal{A})|\to |\mathcal{B}|.$$

$${\overline{c}}_i=\bigcap _j{c}_{ij}\text{and }{\overline{P}}_i=\bigcup _j{P}_{ij}.$$

$${\mathcal{L}}_i=\mathrm{Lk}({\overline{c}}_i,{\overline{P}}_i).$$

$$f^{m+1}:|{\mathrm{skel}}^{m+1}(\mathcal{A})|\to \mathcal{B}$$

$$\bigcap _{k\le \ell }{\sigma }_{i_k}\subseteq \bigcap _{k\in K}{\sigma }_{i_k},$$

$${\tau }_r\cup {\sigma }_{r+1}\subseteq {\tau }_r\cup {\Sigma }_{r+1},$$

$$\varphi :{\mathrm{Ch}}^N(\mathcal{I})\to \mathrm{Div}\mathcal{I}$$

Full text

While the original proof of the ACT relied on an involved combinatorial argument, Borowsky and Gafni later proposed an alternative proof that relied on a algorithmic construction, termed the “convergence algorithm”. The description of this algorithm was incomplete, and presented without proof. In this paper, we give the first complete description, along with a proof of correctness.

1 Introduction

Herlihy and Shavit’s [13, 12] asynchronous computability theorem (ACT) characterizes which tasks are solvable in asynchronous shared-memory systems. Informally, this characterization employs the language of combinatorial topology: a task can be expressed as a relation between two “colored” simplicial complexes. The theorem states that a protocol (algorithm) exists if and only if there is a “color-preserving” simplicial map from one complex to the other compatible with the task’s relation. This approach replaces the usual operational model, where computations unfold in time, with a static model in which all possible protocol interleavings are captured in a single combinatorial structure.

The proof of the ACT contains one difficult step. Using the classical simplicial approximation theorem [15, p.89], it is straightforward to construct a simplicial map having all desired properties except that of being color-preserving. To make this map color-preserving required a rather long construction employing mechanisms from point-set topology, such as $\epsilon$-balls and Cauchy sequences.

Borowsky and Gafni [5] later proposed an alternative proof strategy for the ACT in which the essential chromatic property was guaranteed by an algorithm, rather than by a combinatorial construction. The description of this algorithm was sketchy, however, and no proof was provided. In this paper, we give the first complete description of their algorithm, along with its first proof of correctness.

The paper is structured as follows. In Section 2, we briefly introduce the combinatorial model and the relevant topological machinery, and we give a short exposition on the work by Borowsky and Gafni [5]. In Section 3, we describe the convergence algorithm and a subroutine used by it. In Section 4, we give a complete proof of correctness of the convergence algorithm. In Section 5, we explain how the convergence algorithm can be applied to more general tasks. In Section 6, we summarize some related work, and in Section 7, we conclude with some final remarks.

2 Combinatorial Topology

This section reviews the basic notions of combinatorial topology that will be used to describe shared-memory computation. Our basic construct, called a simplicial complex, can be defined in two complementary ways: combinatorial and geometric. Sometimes it is convenient to use one view, sometimes the other, and we will go back and forth as needed.

2.1 Abstract Simplicial Complexes

Given a finite set $V$, and a family ${\cal K}$ of finite subsets of $V$, we say that ${\cal K}$ is an abstract simplicial complex on $V$ if the following hold:

1. (1)

if $X\in{\cal K}$, and $Y\subseteq X$, then $Y\in{\cal K}$; 2. (2)

$\{v\}\in{\cal K}$, for all $v\in V$.

Each set in ${\cal K}$ is called a simplex, usually denoted by lower-case Greek letters $\sigma$ and $\tau$. A subset of a simplex is a face of that simplex. The dimension $\dim\sigma$ is one less than the number of elements of $\sigma$, or $|\sigma|-1$. We use “$n$-simplex” as shorthand for “$n$-dimensional simplex”, and similarly for “$n$-face”. A simplex $\phi$ in ${\cal K}$ is a facet of ${\cal K}$ if $\phi$ is not contained in any other simplex. A complex is pure if all its facets have the same dimension. The $n$-skeleton of a complex ${\cal K}$, $\operatorname{skel}^{n}{\cal K}$, is the complex formed by all simplexes of ${\cal K}$ of dimension $n$ or less. If ${\cal K}$ and ${\cal L}$ are complexes with ${\cal K}\subseteq{\cal L}$, we say ${\cal K}$ is a subcomplex of ${\cal L}$.

We use $\Delta^{n}$ to denote the complex consisting of a single $n$-simplex and its faces. A labeling is a map $\lambda:V\rightarrow D$, where $D$ is an arbitrary domain, such as the natural numbers. A map $\phi$ carrying vertexes of ${\cal K}$ to vertexes of ${\cal L}$ is a simplicial map if it also carries simplexes of ${\cal K}$ to simplexes of ${\cal L}$. A simplicial map $\chi:\mathcal{K}\rightarrow\mathcal{L}$ is a coloring if for each simplex $\sigma$ of ${\cal K}$, the vertexes of $\sigma$ are mapped to distinct vertexes. Most complexes considered here are endowed with a coloring $\chi$, and such complexes are called chromatic. A simplicial map $\phi:{\cal K}\to{\cal L}$ is color-preserving if $\chi(v)=\chi(\phi(v))$ for vertexes $v\in{\cal K}$.

For complexes ${\cal K}$ and ${\cal L}$, a carrier map, written

[TABLE]

maps each simplex $\sigma\in{\cal K}$ to a subcomplex $\Gamma(\sigma)$ of ${\cal L}$, such that if $\tau\subseteq\sigma$, then $\Gamma(\tau)\subseteq\Gamma(\sigma)$. A simplicial map $\gamma$ is carried by a carrier map $\Gamma$ if $\gamma(\sigma)\subseteq\Gamma(\sigma)$ for every simplex in their domain. In this case, $\gamma$ is said to be carrier-preserving.

The star of a simplex $\sigma\in{\cal C}$, written $\operatorname{St}(\sigma,{\cal C})$, or $\operatorname{St}(\sigma)$ when ${\cal C}$ is clear from context, is the complex that consist of every simplex $\tau$ which contains $\sigma$, and every simplex contained in such $\tau$.

2.2 Geometric Complexes

In the alternative geometric view, we embed a complex in a Euclidean space $\mathbb{R}^{d}$ of sufficiently high dimension.

Given a set $X=\left\{x_{0},\ldots,x_{n}\right\}$ of points in $\mathbb{R}^{d}$, their convex hull, written $\operatorname{conv}X$, is the set of points $y$ that can be expressed as

[TABLE]

where the coefficients $t_{i}$ satisfy $0\leq t_{i}\leq 1$, and $\sum_{i=0}^{n}t_{i}=1$. The $t_{i}$ are called the barycentric coordinates of $y$ with respect to $X$. The set $X$ is affinely independent if no point in the set can be expressed as a weighted sum of the others.

A (geometric) vertex is a point in $\mathbb{R}^{d}$, and a (geometric) $n$-simplex is the convex hull of $(n+1)$ affinely-independent geometric vertexes. A geometric simplicial complex ${\cal K}$ in $\mathbb{R}^{d}$ is a collection of of geometric simplexes, such that

1. (1)

any face of a $\sigma\in{\cal K}$ is also in ${\cal K}$; 2. (2)

for all $\sigma,\tau\in{\cal K}$, their intersection $\sigma\cap\tau$ is a face of each of them.

We use $|{\cal K}|$ to denote the point-set occupied by the geometric complex ${\cal K}$.

Given a geometric simplicial complex ${\cal K}$, we can define the underlying abstract simplicial complex ${\cal C}({\cal K})$ as follows: take the union of all the sets of vertexes of the simplexes of ${\cal K}$ as the vertexes of ${\cal C}({\cal K})$, then for each simplex $\sigma=\operatorname{conv}\{v_{0},\dots,v_{n}\}$ of ${\cal K}$ take the set $\{v_{0},\dots,v_{n}\}$ to be a simplex of ${\cal C}({\cal K})$.

In the opposite direction, given an abstract simplicial complex ${\cal A}$ with finitely many vertexes, there exist many geometric simplicial complexes ${\cal K}$, such that ${\cal C}({\cal K})={\cal A}$.

The open star, denoted $\operatorname{St^{\circ}}(\sigma)$, is the union of the interiors of the simplexes that contain $\sigma$:

[TABLE]

Note that $\operatorname{St^{\circ}}(\sigma)$ is not an abstract or geometric simplicial complex, but just a open point-set in ${\cal C}$.

2.3 Subdivisions

If ${\cal A}$ and ${\cal B}$ are geometric complexes, a continuous map $f:|{\cal A}|\to|{\cal B}|$ is carried by a carrier map $\Phi:{\cal A}\to 2^{{\cal B}}$ if, for every simplex $\sigma\in{\cal A}$, $f(\sigma)\subseteq|\Phi(\sigma)|$.

Informally, a subdivision of a complex ${\cal K}$ is constructed by “dividing” the simplexes of ${\cal K}$ into smaller simplexes, to obtain another complex ${\cal L}$. Subdivisions can be defined for both geometric and abstract complexes.

Definition 2.1*.*

A geometric complex ${\cal B}$ is called a subdivision of a geometric complex ${\cal A}$ if the following two conditions are satisfied:

1. (1)

$|{\cal A}|=|{\cal B}|$; 2. (2)

each simplex of ${\cal A}$ is the union of finitely many simplexes of ${\cal B}$.

Figure 1 shows a geometric complex and a subdivision of that complex.

Subdivisions can be defined for abstract simplicial complexes as well.

Definition 2.2*.*

Let ${\cal A}$ and ${\cal B}$ be abstract simplicial complexes. We say that ${\cal B}$ subdivides the complex ${\cal A}$ if there exists a homeomorphism $h:|{\cal A}|\rightarrow|{\cal B}|$ and a carrier map $\Phi:{\cal A}\rightarrow 2^{{\cal B}}$, such that for every simplex $\sigma\in{\cal A}$, the restriction $h|_{|\sigma|}$ is a homeomorphism between $|\sigma|$ and $|\Phi(\sigma)|$.

A subdivision $\operatorname{Div}({\cal K})$ is chromatic, if $\operatorname{Div}({\cal K})$ is chromatic, and for every simplex $\sigma\in{\cal K}$, $\operatorname{Div}(\sigma)$ and $\sigma$ have the same colors.

Let $\operatorname{Div}{\cal K}$ be a subdivision. The carrier of a simplex $\sigma$, $\operatorname{Car}(\sigma)$, is the smallest simplex $\kappa\in\operatorname{Div}{\cal K}$ such that $\sigma\in\operatorname{Div}({\cal K})$.

2.3.1 Barycentric Subdivision

In classical combinatorial topology, the following barycentric subdivision is perhaps the most widely used.

Definition 2.3*.*

Let ${\cal K}$ be an abstract simplicial complex. Its barycentric subdivision $\operatorname{Bary}{\cal K}$ is the abstract simplicial complex whose vertexes are the non-empty simplexes of ${\cal K}$. A $(k+1)$-tuple $(\sigma_{0},\dots,\sigma_{k})$ is a simplex of $\operatorname{Bary}{\cal K}$ if and only if the tuple can be indexed so that $\sigma_{0}\subset\cdots\subset\sigma_{k}$.

2.3.2 Standard Chromatic Subdivision

The standard chromatic subdivision $\operatorname{Ch}({\cal K})$ is the chromatic analog to the barycentric subdivision. (See Figure 2.)

Definition 2.4*.*

Let $({\cal A},\chi)$ be a chromatic abstract simplicial complex. Its standard chromatic subdivision $\operatorname{Ch}({\cal A})$ is the abstract simplicial complex whose vertexes have the form $(i,\sigma_{i})$, where $i\in\{0,...,n\}$, $\sigma_{i}$ is a non-empty face of $\sigma$, and $i\in\chi(\sigma_{i})$. A $(k+1)$-tuple $(\sigma_{0},\dots,\sigma_{k})$ is a simplex of $\operatorname{Ch}({\cal A})$ if and only if

• •

the tuple can be indexed so that $\sigma_{0}\subseteq\cdots\subseteq\sigma_{k}$.

• •

for $0\leq i,j\leq n$, if $i\in\chi(\sigma_{j})$ then $\sigma_{i}\subseteq\sigma_{j}$.

Finally, to make the subdivision chromatic, we define the coloring $\chi:\operatorname{Ch}({\cal K})$ to be $\chi(i,\sigma)=i$.

This subdivision extends to complexes in the obvious way, and it can be iterated to produce subdivisions $\operatorname{Ch}^{N}(\sigma)$, for $N>0$.

2.4 Links and Connectivity

Subdivided simplexes exhibit an important property called link-connectivity. We provide the necessary definitions below.

Definition 2.5*.*

The link of a $\sigma$ in complex ${\cal K}$, denoted $\operatorname{Lk}(\sigma,{\cal K})$, is the subcomplex of ${\cal K}$ consisting of all simplexes $\tau$ disjoint from $\sigma$ such that $\tau\cup\sigma\in{\cal K}$.

One can think of the link of $\sigma$ as a simplicial neighborhood that encompasses $\sigma$. Next, we present the concept of connectivity as taken from algebraic topology.

Definition 2.6*.*

Let $S^{k}$ denote the $k$-dimensional sphere. A complex ${\cal K}$ is $k$-connected if, for all $0\leq m\leq k$, any continuous map $f:~{}S^{m}~{}\to~{}|{\cal K}|$ can be extended to a continuous $F:~{}D^{m+1}~{}\to~{}|{\cal K}|$, where the sphere $S^{m}$ is the boundary of the disk $D^{m+1}$.

One way to think about this property is that any map $f$ of the $k$-sphere that cannot be “filled in” represents a $k$-dimensional “hole” in the complex.

Definition 2.7*.*

A pure $n$-dimensional complex ${\cal K}$ is link-connected if for all $\sigma\in{\cal K}$, $\operatorname{Lk}(\sigma,{\cal K})$ is $(n-\dim(\sigma)-2)$-connected.

Informally, link-connectivity ensures that a complex cannot be “pinched” too thinly. All subdivided simplexes are link-connected, which is an important property for proving the main theorem.

2.5 Useful Theorems

We will need the following pasting lemma from point-set topology.

Lemma 2.8*.*

Let $X_{1}$ and $X_{2}$ be closed sets of a common space, with continuous $f_{i}:X_{i}\rightarrow Y$ that coincide on the intersection $X_{1}\cap X_{2}$. Then the function $f:X_{1}\cup X_{2}\rightarrow Y$, defined in terms of the $f_{i}$, is a continuous function.

We will also need the following version of the classical simplicial approximation theorem.

Definition 2.9*.*

Let ${\cal A}$ and ${\cal B}$ be abstract simplicial complexes, let $f:~{}|{\cal A}|~{}\to~{}|{\cal B}|$ be a continuous map, and let $\varphi:~{}{\cal A}~{}\to~{}{\cal B}$ be a simplicial map. The map $\varphi$ is called a simplicial approximation to $f$, if for every simplex $\alpha$ in ${\cal A}$ we have

[TABLE]

where $\operatorname{Int}|\alpha|$ denotes the interior of $|\alpha|$.

Theorem 2.10*.*

Let ${\cal A}$ and ${\cal B}$ be simplicial complexes. Given a continuous map $f:|{\cal A}|~{}\to~{}|{\cal B}|$, there is an $N>0$ such that $f$ has a simplicial approximation $\varphi:~{}\operatorname{Ch}^{N}({\cal A})~{}\to~{}{\cal B}$.

This theorem remains true if we replace the standard chromatic subdivision $\operatorname{Ch}(\cdot)$ with the barycentric subdivision $\operatorname{Bary}(\cdot)$.

3 Read-Write Memory

In this section we describe and motivate our model of computation. A distributed system is a collection of sequential computing entities, called processes, that cooperate to solve a problem, called a task. The processes communicate by reading and writing a shared memory. Each process runs a program that defines how and when it communicates with other processes. Collectively these programs define a concurrent algorithm, or protocol.

The theory of distributed computing is largely about what is computable in the presence of timing uncertainty and failures. Here, we assume processes are subject to crash failures, in which a faulty process simply halts and falls silent. We focus on wait-free protocols that solve particular tasks when any proper subset of the of processes may fail. We adopt an asynchronous timing model, where processes run at arbitrary, unpredictable speeds, and there is no bound on process step time. Note that a failed process cannot be distinguished from a slow process.

3.1 Processes

As stated, a process is an automaton. Each process has a unique name. In a computation, it starts with an input value, takes a finite number of steps, and halts with an output value. The task specification defines which values can be assigned as inputs, and which can be accepted as outputs.

A process state is modeled as a vertex, labeled with both that process’s name and its state. A system state is a simplex, where each vertex represents a process and its state, and the vertexes represent mutually compatible states. Such is simplex colored by process names, and labeled with process states. An initial system state is represented as a simplex whose set of vertexes represent the simultaneous states of distinct processes. The set of all possible states forms a chromatic complex, colored by process names, and labeled with process states. Henceforth, we speak of a vertex’s color as shorthand for the name of the corresponding process.

3.2 Tasks

To reduce computation to its simplest form, we consider a fundamental unit of computation called a task. An input to a task is distributed: only part of the input is given to each process. The output from a task is also distributed: only part of the output is computed by each process. The task specification states which outputs can be produced in response to each inputs.

A task is a triple $({\cal I},{\cal O},\Gamma)$, where ${\cal I}$ is the input complex that defines all possible initial configurations, ${\cal O}$ is the output complex that defines all possible final configurations, and $\Gamma$ is a carrier map carrying each $m$-simplex of ${\cal I}$ to a subcomplex of $m$-simplexes of ${\cal O}$, for $0\leq m\leq n$. $\Gamma$ has the following interpretation: for each $\sigma\in{\cal I}$, if the $(\dim\sigma+1)$ processes in $\sigma$ start with the designated input values, and the remaining $n-\dim\sigma$ processes fail without taking any steps, then each simplex in $\Gamma(\sigma)$ corresponds to a legal final state of the non-faulty processes.

A task has the following interpretation. For each simplex $\sigma\in{\cal I}$, if the $(\dim\sigma+1)$ processes in $\sigma$ each starts on the unique vertex colored with its name, taking as input that vertex’s labeled value, and the remaining $n-\dim\sigma$ processes fail without taking any steps, then each simplex in $\Gamma(\sigma)$ corresponds to a legal final state of the non-faulty processes, where each process halts on the unique vertex colored with its name, taking as output that vertex’s labeled value.

The most common task considered in this paper is a convergence task. We are given a input complex ${\cal I}$ colored by process names, and a chromatic subdivision of ${\cal I}$. In the task $({\cal I},\operatorname{Div}({\cal I}),\operatorname{Div})$, the $n+1$ processes start on vertexes of an $n$-simplex $\sigma$ of ${\cal I}$, where each process’s input vertex is colored by that process’s name. The processes halt on a single simplex of $\operatorname{Div}(\sigma)$, and each process halts on an vertex is colored by that process’s name.

In some circumstances, we relax the requirement that each processes halt on an output vertex labeled with its own name. A colorless task is also defined by a triple $({\cal I},{\cal O},\Gamma)$, but there is no requirement that the decision map be color-preserving.

3.3 Protocols

A protocol is a concurrent algorithm to solve a task: initially each process knows its own part of the input, but not the others’. Each process communicates with the others by reading and writing a shared memory, and eventually halts with its own output value. Collectively, the individual output values form the task’s output.

Here, we are concerned with protocols where processes communicate by reading and writing shared memory. Without loss of generality, we consider full-information protocols in which each process repeatedly writes its current state to the shared memory, and constructs its new state by taking a snapshot of (instantaneously reading) the states written by other processes. After a finite number of such communication rounds, each process applies a decision map to its state to choose an output value.

All possible executions of a protocol can be modeled as a chromatic simplicial complex. We think of the protocol executions as a chromatic carrier map $\Xi$ from the input complex ${\cal I}$ to ${\cal P}$, the chromatic protocol complex. The carrier map $\Xi$ carries each input simplex $\sigma\in{\cal I}$ to a subcomplex $\Xi(\sigma)$ of the protocol complex. $\Xi$ carries each $\sigma\in{\cal I}$ to the executions in which the processes in $\sigma$ do not hear from any other process.

The protocol complex is related to the output complex by the decision map $\delta$, a chromatic simplicial map that sends each vertex $v$ in the protocol complex to a vertex $w$ in the output complex, colored with the same process name. The decision value labeling $w$ is the value which the corresponding process takes as its output value. A protocol with carrier map $\Xi$ solves the task if the carrier map obtained by composing $\delta$ with $\Xi$ is carried by $\Delta$.

3.4 Read-Write Memory

In the most natural shared-memory model, the processes share an ordered sequence of registers, memory units that can hold values from an arbitrary domain. A process can read a register, returning its current contents, or it can write a new value to that register, obliterating that register’s prior value.

There are many variations of the asynchronous read-write model, all computationally equivalent in the sense that one model can simulate the others with overhead polynomial in the number of processes. Here, we will use two distinct alternatives. In the snapshot model, each process can write atomically to a single register, but it can atomically read any set of registers, an operation called a snapshot.

It is also sometimes convenient to use a variation known as the immediate snapshot model [4, 16] An immediate snapshot takes place in two contiguous steps. In the first step, a process writes its view to a word in memory, possibly concurrently with other processes. In the very next step, it takes a snapshot of some or all of the memory, possibly concurrently with other processes. It is important to understand that that in an immediate snapshot, the snapshot step takes place immediately after the write step.

Although, modern multicores do not support either the snapshot or the immediate snapshot model directly, either model can be simulated by more conventional models, and vice-versa [11, Ch. 14]. The snapshot model is convenient for expressing specific algorithms, while the immediate snapshot model is convenient because the protocol complex generated by an $N$-round immediate snapshot execution is the subdivision $\operatorname{Ch}^{N}({\cal I})$ of the input complex [11, Ch. 4]. (Using individual reads and writes, the protocol complexes are not subdivisions, although the can be retracted to subdivisions.)

4 The Asynchronous Computability Theorem

The ACT states that a task $T=({\cal I},{\cal O},\Gamma)$ has a wait-free protocol in read-write memory exactly when there is a chromatic, simplicial map from a chromatic subdivision of ${\cal I}$ to ${\cal O}$ carried by $\Gamma$.

Theorem 4.1*.*

A task $({\cal I},{\cal O},\Gamma)$ has a wait-free read-write protocol if and only if there is a chromatic subdivision $\operatorname{Div}(\mathcal{I})$ and a color-preserving simplicial map

[TABLE]

carried by $\Gamma$.

In one direction, the claim is relatively easy. If there exists a read-write protocol, then there exists an immediate snapshot protocol whose protocol complex is $\operatorname{Ch}^{N}({\cal I})$ for some $N>0$. The color-preserving simplicial decision map $\delta:~{}\operatorname{Ch}^{N}({\cal I})~{}\to~{}{\cal O}$ is the desired map.

The other direction is more difficult: we must show that given a chromatic map $\mu:~{}\operatorname{Div}{\cal I}~{}\to~{}{\cal O}$ carried by $\operatorname{Div}$, for some $N>0$. A protocol can be constructed by solving the convergence task on $\operatorname{Ch}^{n}({\cal I})$, and then using $\phi$ as the decision map.

The most straightforward strategy is to show there exists a color-preserving simplicial map

[TABLE]

for some $N>0$, such that for all $\sigma\in{\cal I}$, $\phi(\operatorname{Ch}^{N}\sigma)\subseteq\operatorname{Div}\sigma$. These maps compose as follows:

[TABLE]

These maps can used to construct a protocol. From an input simplex $\sigma$, each process performs the following three steps:

1. step 1.

execute an $N$-layer immediate snapshot protocol, halt on a vertex $x$ of the simplicial complex $\operatorname{Ch}^{N}\sigma$, 2. step 2.

compute $y=\phi(x)$, yielding a vertex in $\operatorname{Div}\sigma$, 3. step 3.

compute $z=\mu(y)$, yielding an output vertex.

It is easy to check that all processes halt on the vertexes of a single simplex in $\Gamma(\sigma)$. Moreover, because all maps are color-preserving, each process halts on an output vertex of matching color.

In prior work, the map $\phi:~{}\operatorname{Ch}^{N}{\cal I}~{}\to~{}\operatorname{Div}{\cal I}$ was constructed in the following combinatorial way. The continuous identity map $|\operatorname{Ch}^{N}{\cal I}|\to|\operatorname{Div}{\cal I}|$ has a simplicial approximation $\psi:~{}\operatorname{Ch}^{N}~{}{\cal I}~{}\to~{}\operatorname{Div}~{}{\cal I}$, carried by $\Delta$. The bulk of the proof is concerned with “perturbing” $\psi$ to make it color-preserving, a somewhat long and delicate construction.

Borowsky and Gafni suggested an alternative approach: treat this problem as a task, $({\cal I},\operatorname{Div}{\cal I},\operatorname{Div})$, in which processes start on vertexes of matching color on a simplex $\sigma$ of ${\cal I}$, and halt on vertexes of matching color on a single simplex of $\operatorname{Div}(\sigma)$. An explicit protocol that solves this chromatic simplex agreement (CSA) task induces the desired map. As noted, the original paper lacked a complete description of the algorithm and a proof, both of which are presented here.

4.1 Chromatic Simplex Agreement

Borowsky and Gafni first consider a more simple task, called non-chromatic simplex agreement (NCSA), in which processes start on the same input complex $\mathcal{I}$ and must converge to any simplex of $\operatorname{Div}(\mathcal{I})$. Processes do not have to land on vertexes of any specified color, though they must remain where they are if they run solo.

NCSA can be solved provided that $\mathcal{I}$ is sufficiently connected. Borowsky and Gafni present a sketch of an inductively constructed protocol, which can be made rigorous via combinatorial topology. While we do not give an explicit protocol here, in the next section we give an explicit protocol for a similar task called link-based NCSA, or LNCSA, which is directly used in the construction of the convergence algorithm.

Algorithm 1 shows the Chromatic Simplex Agreement (CSA) protocol, which is round-based. Recall that participating processes begin on a simplex of ${\cal I}$. In the first round, the processes to run a simplex agreement protocol on $\operatorname{Bary}(\operatorname{Div}{\cal I})$, so that they collectively choose a nested sequence of simplexes in $\operatorname{Div}{\cal I}$. Each process writes its simplex to shared memory and takes an immediate snapshot of the simplexes written by the others. If a process sees a vertex of its color in all simplexes in its snapshot, then the process returns that vertex and finishes. Otherwise, it computes its view111 Borowsky and Gafni called the view the “core”. as the union of all simplexes it saw, minus the vertex of its own color, if it exists. The process proceeds to the next round.

A process entering round $r>1$ has already computed a view. Each process begins round $r$ by writing its view to shared memory and taking immediate snapshots of the shared memory from this round as well as the first round. By retaking a snapshot of the first round, a process updates the participating set of processes it observes running the protocol. By taking a snapshot of the views from the current round, the process computes its core222 Borowsky and Gafni called this the “intersection of cores”., defined to be the intersection of the views from the current round’s snapshot. Using these two snapshots, the process computes its convergence complex, a simplicial neighborhood of the core (defined in the next section). Note that processes typically construct different convergence complexes, though all such complexes will be ordered by inclusion. Each process then chooses a starting vertex of its own color in its convergence complex, and runs the LNCSA protocol on the barycentric subdivision of its convergence complex. Processes collectively obtain a nested sequence simplexes, similar to the first round. Each process then replaces its core with the smallest core observed when running LNCSA. Each process writes its simplex and its new core to shared memory and takes a snapshot. If a process sees a vertex of its color in each simplex it saw, it decides on that vertex and finishes. Otherwise, it updates its view and proceeds to the next round.

See Algorithm 1 for pseudocode. In the next section, we give more detailed explanations about how each piece of data is computed.

5 Correctness of the Convergence Algorithm

5.1 Preliminaries

If each process executes Protocol 1, it will decide on a vertex of its color in a simplex on $\operatorname{Div}({\cal I})$, thus solving CSA over ${\cal I}$. In this section we show that the protocol terminates, and that processes choose valid outputs.

Here is some notation useful to prove correctness of the convergence algorithm. Let $p_{1},\ldots,p_{n+1}$ be the processes participating in the convergence algorithm. Let $p$ be any such process. For each round $r>1$, $p$’s state consists of the following: its participating set $P^{r}_{p}$, its core $c^{r}_{p}$, its convergence complex ${\cal C}^{r}_{p}$, its starting vertex $v^{r}_{p}$, its simplex $s^{r}_{p}$, and its view $w^{r}_{p}$.

Here is how each component is computed during round $r$ of the convergence algorithm:

The participating set $P^{r}_{p}$ is the set of processes and corresponding input vertexes that process $p$ sees when it takes a snapshot of the first round’s shared memory. 2. 2.

The core $c^{r}_{p}$ is the set of vertexes that may be decision values of processes other than $p$ that have finished the protocol. It is defined to be

[TABLE]

where $J$ is the index set of processes seen by $p$ in its snapshot of views from the current round $r$. When running LNCSA, the process may see smaller cores, in which case $p$ recomputes its core as

[TABLE]

where $I$ is the index set of processes seen by $p$ during LNCSA. 3. 3.

The convergence complex ${\cal C}^{r}_{p}$ is the complex on which $p$ runs the LNCSA protocol to choose a new simplex consistent with current decision values. It is computed as

[TABLE] 4. 4.

The starting vertex $v^{r}_{p}$ is the vertex on which $p$ begins running the LNCSA protocol. Any vertex from ${\cal C}^{r}_{p}$ with the same color as $p$ may be chosen. 5. 5.

The simplex $s^{r}_{p}$ is the simplex in ${\cal C}^{r}_{p}$ which $p$ chooses as a result of running the LNCSA protocol. They collectively represent the domain of values from which processes may choose decision values in round $r$. 6. 6.

The view $w^{r}_{p}$ is the set of vertexes that $p$ sees in round $r$. It is computed as

[TABLE]

where $I$ is the index set of processes seen by $p$ in its snapshot of simplexes and cores, and $u^{r}_{p}$ is the vertex with the same color as $p$, if it exists.

5.2 Link-based non-chromatic simplex agreement

Before we can define LNCSA, we need a few technical lemmas.

Lemma 5.1*.*

All views and cores are simplexes.

Proof.

By induction. It is clear that views from round $1$ are simplexes, since they are all subsets of the largest simplex chosen during simplex agreement. The cores computed in round $2$ are also simplexes, since they are intersections of the views from round $1$.

Inductively assume that all views from round $r$ are simplexes. Clearly all cores $c^{r+1}_{p}$ in round $r+1$ are simplexes as well, since they are intersections of views from round $r$. Views in round $r+1$ are computed as

[TABLE]

Fix process $p$. We know that

[TABLE]

for some $\ell\in I$, since the simplexes are ordered by inclusion. Then $s^{r+1}_{p_{\ell}}$ is the largest simplex seen by $p$ in its snapshot. Furthermore, we know that $s^{r+1}_{p_{\ell}}\cup\bar{c}^{r+1}_{p_{\ell}}$ is a simplex, by definition of the link of a simplex. But

[TABLE]

so

[TABLE]

By downward closure, we conclude that $w^{r+1}_{p}$ is a simplex.

By induction, all views and cores are simplexes. ∎

The next lemma states that the convergence complexes of the processes are ordered by inclusion, ensuring that the NCSA tasks solved by different processes are coherent, even though they may have different convergence complexes.

Lemma 5.2*.*

The convergence complexes of participating processes for any given round are ordered by inclusion.

Proof.

Fix round $r$. If exactly one or fewer processes have not decided, then the claim is trivial. So let $p_{1}$ and $p_{2}$ be distinct processes that have not decided. Let ${\cal C}_{i}$ denote the convergence complex for $p_{i}$. We must show ${\cal C}_{1}$ and ${\cal C}_{2}$ are comparable. Without loss of generality, suppose $p_{1}$ takes a snapshot of the view arrays for rounds $1$ and $k$ before $p_{2}$. Then $p_{2}$ sees more views than $p_{1}$, so it computes a larger intersection for its core, meaning that $c_{2}\subseteq c_{1}$, where $c_{i}$ is the core of $p_{i}$ in the current round. Furthermore, if $Q_{i}$ is the set of processes that $p_{i}$ sees in round $1$, then $Q_{1}\subseteq Q_{2}$. Since the link operator is order reversing in the first argument, and order preserving in the second, we have $\operatorname{Lk}(c_{1},Q_{1})\subseteq\operatorname{Lk}(c_{2},Q_{2})$. We conclude that ${\cal C}_{1}\subseteq{\cal C}_{2}$, which proves the lemma. ∎

Since convergence complexes are ordered by inclusion, cores and participating sets are ordered in the same way.

The next lemma allows each process to pick a vertex of its own color in its convergence complex when it starts LNCSA.

Lemma 5.3*.*

If process $p$ has not decided by round $r$, then there is at least one vertex of its color in ${\cal C}^{r}_{p}$.

Proof.

It suffices to show that no vertex in $c^{r}_{p}$ has the same color as $p$. The core $c^{r}_{p}$ is computed as the intersection of views that $p$ sees in its snapshot of the view array in round $r$. This includes $w^{r-1}_{p}$. But $w^{r-1}_{p}$ cannot contain a vertex of color $p$, since any such vertex is explicitly removed in the computation of $w^{r-1}_{p}$. Since $w^{r-1}_{p}$ does not contain a vertex of color $p$, neither does $c^{r}_{p}$. since ${\cal I}$ is chromatic, ${\cal C}^{r}_{p}$ must contain at least one vertex of color $p$. ∎

The next lemma states that a decision value reached in a given round is contained in all cores and views of subsequent rounds.

Lemma 5.4*.*

If a process decides on a vertex, then that vertex is contained in the views and cores of all processes in all subsequent rounds.

Proof.

Suppose process $p$ decides on vertex $u$ in round $r_{p}$. We proceed by induction. As the base case, we show that every view computed in round $r_{p}$ contains $u$. Let $p^{\prime}$ be any other process that does not decide this round. There are two cases: when $p^{\prime}$ computes its new view, either $p^{\prime}$ sees the simplex that $p$ wrote, or $p^{\prime}$ does not. In the first case, $p^{\prime}$ sees what $p$ wrote, which is a simplex $\sigma$ that must contain $u$, otherwise $p$ could not decide this round, since $p$ must have seen $u$ in its own simplex. So $p^{\prime}$ includes $\sigma$ in the computation of its view, so the view of $p^{\prime}$ contains $u$. Now consider the second case, where $p^{\prime}$ does not see the simplex that $p$ wrote. But for $p$ to decide on $u$, $u$ must have been contained in all previously written simplexes, including the simplex of $p^{\prime}$. Since this simplex contains $u$, the view of $p^{\prime}$ will also contain $u$. In either case, the view of $p^{\prime}$ contains $u$.

Now, inductively assume that all views from round $r\geq r_{p}$ contain vertex $u$. We want to show that all views from round $r+1$ also contain $u$. First, consider the cores computed in round $r+1$. As intersections of views from round $r$, all cores computed in round $r+1$ also contain $u$. Furthermore, each process $p^{\prime}$ computes its view in round $r+1$ as

[TABLE]

Since each core contains $u$, we have

[TABLE]

so the view of $p^{\prime}$ computed in round $r+1$ also contains $u$. Therefore all views in round $r+1$ also contain $u$. By induction, all views in all rounds after $r_{p}$ contain $u$. Since cores are computed as intersections of views, all cores in rounds $r>r_{p}$ also contain $u$. ∎

We formally define LNCSA and give a protocol similar to that of NCSA.

Lemma 5.5*.*

Fix round $r$, and suppose processes have computed their cores. Then there is a wait-free immediate-snapshot protocol for converging to a simplex on $\operatorname{Lk}(\bigcap_{k\in K}c^{r}_{p_{k}},\bigcup_{k\in K}P^{r}_{p_{k}})$.

Proof.

Let $({\cal I},\operatorname{Div}({\cal I}),\operatorname{Div})$ be the chromatic simplex agreement task we want to solve via the convergence algorithm. Fix round $r$, and suppose the processes have just computed their links. They will next collectively converge to a simplex that is consistent with the smallest core among them. That is, they will converge on the largest link among the processes. This is the LNCSA task.

We formally define the task. Each process’s state is defined by its core $c$, its participating set $p$, and the starting vertex $v$ it chooses in its link (which by Lemma 5.3 it can do), so the input complex ${\cal A}$ of LNCSA has vertex set consisting of triples $(v,c,P)$ such that $v\in P$ and $\operatorname{Car}(c,{\cal I})\subseteq P$. A set of triples $\{(v_{i},c_{i},P_{i})\}$ is a simplex in ${\cal A}$ if the $v_{i}$ all have distinct colors and $\{c_{i}\}$ and $\{P_{i}\}$ are ordered by inclusion. We require the $v_{i}$ to have different colors since each process chooses a vertex of its own color, and we require $\{c_{i}\}$ and $\{P_{i}\}$ to be ordered in the same way by inclusion, since they were computed using snapshots.

So ${\cal A}$ is a subcomplex of

[TABLE]

where $V$ is the vertex set of ${\cal I}$. The output complex of LNCSA is ${\cal B}=\operatorname{Bary}(\operatorname{Div}({\cal I}))$, since each process chooses a simplex on $\operatorname{Div}({\cal I})$. Processes that execute in isolation stay where they are. Otherwise, processes converge to a simplex in the largest link they see, so if $\sigma=\{(v_{i},c_{i},P_{i})\}$ is a simplex in ${\cal A}$, then we have $\Gamma(\sigma)=\{v\}$ if $\sigma=\{(v,c,P)\}$, and $\Gamma(\sigma)=\operatorname{Lk}(\bigcap c_{i},\bigcup P_{i})$. By Lemma 5.2, $\Gamma$ is monotonic, so it is a carrier map.

Thus LNCSA is the task $({\cal A},{\cal B},\Gamma)$. We show that this task is solvable by constructing a continuous

[TABLE]

carried by $\Gamma$. We induct on skeletons to construct an such an $f$ by defining carrier-preserving

[TABLE]

for each $m$. As base case, we define $f^{0}$ as $f^{0}((v,c,P))=v$ for each vertex $(v,c,P)$ of ${\cal A}$. The function $f^{0}$ is clearly continuous and carried by $\Gamma$. Now inductively assume we have defined $f^{m}$. We want to define

[TABLE]

Let $\{\sigma_{i}\}$ be the facets of $\operatorname{skel}^{m+1}({\cal A})$, and for each $i$, let $\sigma_{i}=\{(v_{ij},c_{ij},P_{ij})\}_{j\leq m+2}$. Let

[TABLE]

By the inductive hypothesis, $f^{m}$ is carried by $\Gamma$, which implies that the image of $f^{m}$ is contained in

[TABLE]

We also know that $\dim({\cal L}_{i})\geq\dim(\sigma_{i})=m$, since each $v_{ij}\in{\cal L}_{i}$, each $v_{ij}$ has different color, and ${\cal L}_{i}$ is chromatic. Suppose $\dim(\overline{P}_{i})=n$. We know that ${\cal L}_{i}$ a link in the subdivided simplex $\operatorname{Bary}(\operatorname{Div}(\overline{P}_{i}))$, which is link-connected, so since $\dim({\cal L}_{i})\geq m$, we conclude that ${\cal L}_{i}$ is at least $n-2-(n-m-1)$ = $(m-1)$-connected. Using this, along with the fact that $\operatorname{Im}(f^{m})\subseteq{\cal L}_{i}$, we can extend $f^{m}|_{\partial\sigma_{i}}$ to a function $f^{m+1}_{i}:|\sigma_{i}|\rightarrow|{\cal L}_{i}|$. Next, using the pasting lemma, we can glue the $f^{m+1}_{i}$ together to obtain a map

[TABLE]

extending $f^{m}$. By construction, $f^{m+1}$ is carried by $\Gamma$. By induction, we have obtained a continuous function $f:|{\cal A}|\rightarrow|{\cal B}|$. By the simplicial approximation theorem, the task $({\cal A},{\cal B},\Gamma)$ is wait-free solvable using immediate snapshots. ∎

5.3 Termination and Validity

Next, we show that all processes eventually decide.

Theorem 5.6*.*

All processes participating in the convergence algorithm eventually decide.

Proof.

We show that at least one process decides each round. Fix a round, and let $\{p_{0},\ldots,p_{\ell}\}$ be the set of participating processes. The processes each run LNCSA protocols over barycentric subdivisions of the convergence complexes, and by Lemma 5.5, they converge to a simplex $\tau$ on the largest subcomplex, say $\operatorname{Bary}({\cal C})$. By definition of $\operatorname{Bary}$, the simplex $\tau\in\operatorname{Bary}({\cal A}_{i_{k}})$ corresponds to a chain of simplexes $\sigma_{i_{0}}\subseteq\cdots\subseteq\sigma_{i_{\ell}}$. Their intersection is $\sigma_{i_{0}}$, which is clearly nonempty, so choose a vertex $\hat{v}\in\sigma_{i_{0}}$. The color of $\hat{v}$, denoted as $\chi(\hat{v})$, cannot be the color of any nonparticipating process, because all subcomplexes $\operatorname{Bary}({\cal C})$ are all subcomplexes of the processes’ carrier, which contains only vertexes whose colors are those of the participating processes, since ${\cal I}$ is chromatic. Neither can $\chi(\hat{v})$ be the color of a process that decided in a previous round. Supposing not, this means the largest convergence complex contains vertexes of color $\chi(\hat{v})$, meaning that the corresponding core could not contain a vertex of color $\chi(\hat{v})$, since the link contains vertexes of color exactly those not in the corresponding core. This contradicts Lemma 5.4, since decided vertexes must be contained in all cores.

Let $\hat{p}\in P$ be the process whose color is $\chi(\hat{v})$, and let $K\subseteq\{0,\ldots,\ell\}$ be the index set of processes that $\hat{p}$ saw during its snapshot of the simplex array. Then

[TABLE]

so $\hat{v}\in\bigcap_{k\in K}\sigma_{i_{k}}$. Since $\hat{p}$ sees $\hat{v}$ in all simplexes in its snapshot, $\hat{p}$ decides on $\hat{v}$. It follows that at least one process decides in each round, so all processes decide in at most $n+1$ rounds. ∎

Theorem 5.7*.*

Participating processes converge to a simplex in their carrier.

Proof.

We show that for each round $r$, the set of vertexes that processes have decided form a simplex. We argue by induction, starting at round $1$. In round $1$, it is clear that decision values form a simplex, since processes decide on vertexes from the largest simplex chosen by running LNCSA. All decision values in round $1$ must be contained in this largest simplex, hence they must form a simplex.

Fix round $r$, and inductively assume that the vertexes which processes decided during the rounds up to $r$ form a simplex, which we call $\tau_{r}$. Consider round $r+1$. Processes in this round choose vertexes on a simplex of the barycentric subdivision of the largest convergence complex, $\operatorname{Bary}({\cal C})$, which is determined by the smallest core. So vertexes on which processes decide this round are contained in an ascending chain of simplexes in ${\cal C}$. Call the largest such simplex $\Sigma_{r+1}$. Let $c_{r+1}$ be the smallest core, corresponding to the largest convergence complex. Then by definition of the link, $c_{r+1}\cup\Sigma_{r+1}$ is a simplex in ${\cal C}$, since the largest link is determined by simplex $c_{r}$. From Lemma 5.4, we must have $\tau_{r}\subseteq c_{r+1}$, so $\tau_{r}\cup\Sigma_{r+1}$ is also a simplex in ${\cal C}$, by downward closure of simplicial complexes. Let $\sigma_{r+1}\subseteq\Sigma_{r+1}$ be the set of all vertexes that processes on decide during round $r+1$. Again by downward closure,

[TABLE]

so $\tau_{r}\cup\sigma_{r+1}$ is a simplex. But by definition of $\tau_{r}$, $\tau_{r+1}=\tau_{r}\cup\sigma_{r+1}$, where $\tau_{r+1}$ is exactly the set of vertexes on which processes have decided up to round $r+1$. So $\tau_{r+1}$ is also a simplex. By induction, it follows that the processes’ decision values form a simplex.

Processes can choose decision only values in their carrier, since all links are computed relative to the observed participating set, and all decision values are chosen from these links. This completes the proof of the theorem, and the proof of correctness of the convergence algorithm. ∎

6 Application to more general tasks

Recall that CSA over a chromatic subdivision $\operatorname{Div}(\mathcal{K})$ is defined as the task $(\mathcal{K},\operatorname{Div}(\mathcal{K}),\operatorname{Div})$. The proof of the convergence algorithm shows that this task has a wait-free read-write protocol. To make the convergence algorithm work, we required that $\operatorname{Div}(\mathcal{K})$ be link-connected so that processes can iteratively converge over ever smaller subcomplexes. Phrased in a different way, the convergence algorithm allows us to find a chromatic simplicial map

[TABLE]

carried by $\operatorname{Div}$, Given the continuous (identity) map $\mathrm{id}:|{\cal I}|\rightarrow|\operatorname{Div}({\cal I})|$ also carried by $\operatorname{Div}$. In fact, link-connectivity is the essential property of the output complex. In particular, the the convergence algorithm may be applied to more general continuous functions $f:|{\cal I}|\rightarrow|{\cal O}|$ carried by some $\Gamma$. Given the assumption that $\Gamma(\sigma)$ is link-connected for all $\sigma\in{\cal I}$, we can use the convergence algorithm to obtain a chromatic simplicial map $\phi:\operatorname{Ch}^{N}({\cal I})\rightarrow{\cal O}$ also carried by $\Gamma$. We state this observation as a theorem.

Theorem 6.1*.*

Let $f:|{\cal I}|\rightarrow|{\cal O}|$ be a continuous map between chromatic complexes and let $\Gamma:{\cal I}\rightarrow{\cal O}$ be a carrier map such that $\Gamma(\sigma)$ is link-connected for each $\sigma\in{\cal I}$. Suppose $f$ is carried by $\Gamma$. Then there exists a chromatic, carrier-preserving simplicial map $\phi:\operatorname{Ch}^{N}({\cal I})\rightarrow{\cal O}$.

7 Related work

A more complete treatment of topological models for concurrent computing can be found in the textbook of Herlihy, Kozlov, and Rajsbaum [11].

The original ACT [13, 12] used combinatorial arguments to construct the color-preserving map required by the theorem. Borowsky and Gafni [5] proposed the alternative algorithmic approach to constructing this map, but without complete definitions or a proof of correctness. Guerraoui and Kuznetsov [10] compare the two approaches. Gafni et al. [9] recently generalized the ACT to encompass infinite executions and other models.

The first application of the ACT was to prove the impossibility of the $k$-set agreement task [7], a result also proved, using other techniques, by Borowsky and Gafni [4], and by Saks and Zaharoglou [16]. These results generalize the classic proofs of the impossibility of consensus due to Fischer et al. [8] and Biran et al. [3].

Castaneda and Rajsbaum [6] use the ACT to show that the renaming task [1] for $n+1$ processes has no wait-free read/write protocol with $2n$ output names when $n+1$ is a prime power, but that a protocol does exist when $n+1$ is not a prime power. Attiya et al. [2] and Kozlov [14] give upper bounds on the running times of such protocols.

8 Remarks

The heart of the ACT is the construction of a chromatic map from a chromatic subdivision of the input complex to the output complex. While it is easy to construct a non-chromatic map using the well-known simplicial approximation theorem [15, p.89], the only prior construction [11, 12] was long and complex. The algorithmic approach proposed by Borowsky and Gafni [4] was intuitively appealing, but lacked a complete statement of the algorithm and a proof. Here, we have given such a statement and proof, and we believe the result, while far from simple, is easier to follow, and yields new insight into this key construction.