Stone Duality Proofs for Colorless Distributed Computability Theorems

For the purposes of this paper, we will consider a simplicial complex $𝒞$ over a finite set of vertices $V$ to be a down-set in the poset $(𝒫(V)\setminus \{\mathrm{\varnothing }\},\subseteq )$. This is a simple reformulation of the classical definition of simplicial complexes. Elements $\sigma \in 𝒞$ are called simplices, minimal elements are called vertices and downsets $A\subseteq 𝒞$ are called subcomplexes. We denote by $V_{𝒞}$ the set of vertices of $𝒞$, and by $𝒟(𝒞)$ its lattice of subcomplexes. We denote by $dim(\sigma ):=|\sigma |-1$ the dimension of $\sigma$, and by $dim(𝒞)=\max \{dim(\sigma )\mid \sigma \in 𝒞\}$ the dimension of a complex $𝒞$. A simplex of dimension $k$ will sometimes be referred to as a $k$-simplex.

A simplicial map $f:𝒞\to {𝒞}^{\prime }$ is given by a map $g:V_{𝒞}\to V_{{𝒞}^{\prime }}$ such that $f=g_{\ast }$. Note that the dimension of $f(\sigma )$ may be of smaller than that of $\sigma$. We say that $f$ is rigid when it preserves dimension. The category of simplicial complexes with simplicial maps is denoted by $\mathrm{𝐬𝐂𝐨𝐦𝐩}$.

In the topological approach to distributed computing, another type of map is often also considered. Given two simplicial complexes $𝒞,{𝒞}^{\prime }$, a carrier map from $𝒞$ to ${𝒞}^{\prime }$ is a map $\varphi :𝒞\to 𝒟({𝒞}^{\prime })$, such that for $\sigma \subseteq \tau$ in $𝒞$, we have $\varphi (\sigma )\subseteq \varphi (\tau )$. A carrier map is rigid when it preserves dimension, i.e. for a simplex $\sigma$ of dimension $d$, $\varphi (\sigma )$ is a subcomplex of ${𝒞}^{\prime }$ of dimension $d$. We say that it is strict if it preserves intersections, i.e. $\varphi (\sigma \cap \tau )=\varphi (\sigma )\cap \varphi (\tau )$. However, note that when $\varphi$ is not strict, we still have $\varphi (\sigma \cap \tau )\subseteq \varphi (\sigma )\cap \varphi (\tau )$.

Finally, we endow these structures with a topology. It is well known [12, Section 2.2] that finite posets can be endowed with a topology given by up- and down-sets. This is known as the Alexandrov topology. Since simplicial complexes are a special kind of poset, we will consider them as finite topological spaces endowed with this topology. Explicitly, we consider the topology on $𝒞$ in which open sets are up-sets $U\in 𝒰(𝒞)$ and closed sets are down-sets $D\in 𝒟(𝒞)$. With this topology, $𝒞$ is a finite $T_0$ space.

Finite $T_0$ spaces are examples of special topological spaces called spectral or Stone spaces, see [8] for a very complete presentation of these spaces and associated results. Recall that in a topological space $X$, a subset $A\subseteq X$ is said to be compact if any open cover of $A$ can be refined to a finite open cover¹¹1Note that we do not require $X$ to be Hausdorff.. In non-Hausdorff spaces, a compact set is not necessarily closed. For this reason, in such spaces we may consider the set $𝒦𝒪(X)$ of compact-open subsets of $X$, i.e. those which are compact and open. A $T_0$, compact and sober topological space $X$ is a spectral space when $𝒦𝒪(X)$ is closed under finite intersections and is in addition a basis for its topology, i.e. its open sets are generated under arbitrary unions of elements of $𝒦𝒪(X)$. A spectral map is a continuous function $f:X\to Y$ between spectral spaces, such that for every $U\in 𝒦𝒪(Y)$, $f^{-1}[U]\in 𝒦𝒪(X)$. The category of spectral spaces and spectral maps is denoted by $\mathrm{𝐒𝐩𝐞𝐜}$. In the case of a finite spectral space, which corresponds precisely to a poset $P$ endowed with the Alexandrov topology, we have $𝒦𝒪(P)=𝒰(P)$, and spectral maps are simply order-preserving maps [12, Section 2.2]. In other words, the category ${\mathrm{𝐏𝐨𝐬}}_f$ of finite posets and order-preserving maps is a full sub-category of $\mathrm{𝐒𝐩𝐞𝐜}$.

In this paper we will make extensive use of Stone duality, which establishes a useful connection between distributive lattices and spectral spaces. Given a lattice $L$, recall that a filter $F\subseteq L$ is a non-empty up-set which is closed under meets. A filter $P$ is proper when $P\ne L$ and is prime if it is proper and if, for all $a,b\in L$, $a\vee b\in P$ implies that $a\in P$ or $b\in P$. We denote by $\mathrm{𝑝𝐹𝑖𝑙𝑡}(L)$ the set of prime filters of $L$. Endowing $\mathrm{𝑝𝐹𝑖𝑙𝑡}(L)$ with the topology generated by the sets $\widehat{a}=\{F\in X\mid a\in F\},$ for $a\in L$, we obtain a spectral space $\mathrm{𝑆𝑡}(L)$. Denoting by $\mathrm{𝐃𝐋}$ the category of distributive lattices and lattice homomorphisms, and by $\mathrm{𝐒𝐩𝐞𝐜}$ the category of spectral spaces and spectral maps, we have a pair of contravariant functors between $\mathrm{𝐃𝐋}$ and $\mathrm{𝐒𝐩𝐞𝐜}$:

establishing a duality between $\mathrm{𝐃𝐋}$ and $\mathrm{𝐒𝐩𝐞𝐜}$. Concretely, this means that, given a spectral map $f:X\to X^{\prime }$ between spectral spaces, we obtain a lattice homomorphism $f^{-1}:𝒦𝒪(X^{\prime })\to 𝒦𝒪(X)$ given by inverse image. Conversely, a lattice homomorphism $h:L\to L^{\prime }$ yields a spectral map $\mathrm{𝑆𝑡}(h):\mathrm{𝑆𝑡}(L^{\prime })\to \mathrm{𝑆𝑡}(L)$, and these assignments are mutually inverse. For a more in-depth treatment of Stone duality, see [12].

As mentioned above, a finite spectral space $X$ is isomorphic to a poset $P$ endowed with the Alexandrov topology, and we have $𝒦𝒪(X)\cong 𝒰(P)$. Conversely, given a finite distributive lattice $L$, there is a bijection between $\mathrm{𝑝𝐹𝑖𝑙𝑡}(L)$ and the set $𝒥(L)$ of join-prime elements of $L$. Summing this up, in the finite case, Stone duality specializes to a duality between ${\mathrm{𝐏𝐨𝐬}}_f$ and ${\mathrm{𝐃𝐋}}_f$, the category of finite distributive lattices. This is called Birkhoff duality, see [12] for more information. Note however that since $𝒟(P)$ is order-dual to $𝒰(P)$, this duality also applies to down-set lattices.

Given some number of processes, a chromatic distributed system is the given of a set of possible local views or states for each process, along with subsets thereof describing global states. In the pioneering work of Herlihy and Shavit [19], the authors established a simplicial semantics for task-solvability. Indeed, considering not only global states, but also their subsets, we obtain a simplicial complex. For example, given two processes $p$ and $q$, each of which can have the possible local state $0$ or $1$, we obtain the chromatic simplicial complex pictured below on the right, in which the local views of $p$ (resp. $q$) are colored red (resp. blue). This encoding of a distributed system thus not only contains all global states, but also encodes their indistinguishability for each local state. Indeed, when the red process has value $1$, it cannot tell whether it is in a global state in which blue has $0$ or $1$. Uncertainty here is encoded simplicially by it being a member of two distinct $1$-simplices.

Chromatic distributed systems are thus encoded as simplicial complexes decorated with colors representing process identities. However, in many cases of interest in distributed computing, the specification of which process has which view is unimportant; only the values present in the system are considered. The identifiers can thus be projected out of the system, resulting in a regular (achromatic) simplicial complexes. Therefore, in the achromatic case, the interpretation of a simplex $\{v_1,\mathrm{\dots },v_k\}$ is that there exists a global state in which each value $v_i$ is the local view of at least one process in the system. The simplicial complex corresponding to the chromatic example described above is pictured just below it.

In order to provide a faithful semantics of task-solvability, we also simplicially describe tasks, i.e. distributed program specifications. For a sequential program, a specification is simply a relation between a set of input values and a set of output values. Since a distributed algorithm outputs a value at each process, a distributed task must relate a collection of inputs with sets of (legal) collections of outputs. A task is said to be colorless [17, Chap. 4.1] if for any input with set of values $I$, any input formed with a subset $I^{\prime }\subset I$ of values is also a possible input, and, symmetrically, for any legal output for a given $I$ with set of values $O$, an output with set of values $O^{\prime }\subset O$ is also legal for $I$. This means its specification does not depend of the multiplicity of values in the distributed system, we only have to encode the values present in the system, rather than also keeping track of process identifiers. So, in a colorless task specification, we must relate a complex $ℐ$ of input values to a complex $𝒪$ of output values. Recall that a relation $R\subseteq X\times Y$ is equivalent, via currying, to a map $f_R^X:X\to 𝒫(Y)$, defined by $f_R^X(x)=\{y\in Y\mid xRy\}$. In the case of a relation between simplicial complexes, respecting the simplicial structure means that the associated map is of the form $\mathrm{\Delta }:ℐ\to 𝒟(𝒪)$ and is required to be monotone. As recalled above in Section 2.1, this is known as a carrier map. In the simplicial semantics, this map is interpreted as the specification that, starting with values in $\sigma \in ℐ$, valid outputs are in the sub-complex $\mathrm{\Delta }(\sigma )\in 𝒟(𝒪)$. Such a carrier map is called a (colorless) task. As an example, we have illustrated the binary consensus task above on the left. This is the distributed specification in which processes start with values $0$ or $1$ and must collectively agree on one of them. The specification $\mathrm{\Delta }$ for binary consensus is pictured in blue; when all processes have value $0$ (resp. $1$), they must decide on that value, corresponding to the assignment $\{0\}\mapsto \{\{0\}\}$ (resp. $\{1\}\mapsto \{\{1\}\}$). However, when at least one process has $0$ and at least on other has $1$, they can choose either value, corresponding to the assignment $\{0,1\}\mapsto \{\{0\},\{1\}\}$. Note that simplices, sets of values, are distinguished from sub-complexes, which are sets of sets of values.

As recalled previously, distributed computability is concerned with determining which tasks can be solved in a given communication protocol. Above we defined colorless tasks in the simplicial semantics. Here, we describe how achromatic protocols are encoded. For the definition of colorless task-solvability in the simplicial semantics, see Section 5.1 below.

Note that we employ the term colorless (resp. achromatic) to describe tasks (resp. protocols) which can be encoded via (achromatic) simplicial complexes. As mentioned in the introduction, the precise semantic relationship between colored and colorless task-solvability with respect to chromatic or achromatic models is not well understood. For this reason we choose to terminologically distinguish tasks and protocols with respect to (achromatic) simplicial encoding. Henceforth we will consider exclusively colorless tasks and achromatic protocols, and will thus often omit the qualifications “colorless” and “achromatic”.

Broadly speaking, a protocol consists of a set of valid communication scenarios along with their epistemic effect on the input states. Since the order of communications will affect the knowledge of each process, these protocols are inherently non-deterministic. As above, we glue these possible reachable states along common local states to obtain a simplicial complex. For example, consider a system in which at least two processes, starting with either $0$ or $1$, send each other their local value, and in which at most one message may be lost. The carrier map describing this communication protocol is pictured below on the right.

Indeed, when all processes start with $0$ (resp. $1$), the only value they can see is $0$ (resp. $1$), regardless of how many messages are lost. However, when at least one process starts with $0$ and another with $1$, corresponding to the input simplex $\{0,1\}$, there are several possibilities. If no message is lost, all processes see both values, corresponding to the subcomplex $\{\{01\}\}$. If however at least one process having $0$ (resp. $1$) has not received a message containing a different value than it already has, it sees only $0$ (resp. 1), while other processes see $01$, corresponding to the sub-complex $\{\{0\},\{0,01\},\{01\}\}$ (resp. $\{\{1\},\{1,01\},\{01\}\}$). Note that if all messages can be lost, we must add an extra simplex to $𝒫$, namely $\{0,1\}$ and include it in the image of $\pi (\{0,1\})$.

Summing up, an (achromatic) distributed protocol is given by an input complex $ℐ$ encoding input states, a protocol complex $𝒫$ encoding reachable states, and a carrier map $\pi :ℐ\to 𝒟(𝒫)$. In [17], carrier maps associated to protocols are required to satisfy additional properties, namely

• $\mathrm{■}$

  $\forall {\sigma }_1,{\sigma }_2\in ℐ$, $\pi ({\sigma }_1\cap {\sigma }_2)=\pi ({\sigma }_1)\cap \pi ({\sigma }_2)$ (strictness),

• $\mathrm{■}$

  ${\bigvee }_{\sigma \in ℐ}{\pi }_{ℐ}(\sigma )=𝒫$ (effective surjectivity).

For this reason, we refer to carrier maps which satisfy these conditions as protocol maps.

The first contribution of this paper is in identifying these conditions as precisely those needed to lift a protocol map to a homomorphism of lattices from $𝒟(ℐ)$ to $𝒟(𝒫)$. Recall that given an order preserving map $f:P\to 𝒟(Q)$, where $P$ and $Q$ are posets, we obtain a union-preserving map, called the join-lift of $f$:

It is routine to check that strictness and effective surjectivity imply that the join-lift of a protocol map $\pi$ not only preserves unions, but is in fact a lattice homomorphism ${\pi }^{\vee }:𝒟(ℐ)\to 𝒟(𝒫)$. Applying Birkhoff duality, we can thus conclude that a protocol map is equivalent to a monotone map $\rho :𝒫\to ℐ$. This insight naturally leads to spectral spaces as the generalization of the simplicial semantics of distributed computability, as is described in Section 4.

The above is a very general definition of a protocol, in the sense that the protocol complex $𝒫$ can represent any reachable configuration of distributed knowledge. In this paper, we consider round-based protocols. This means that we have a collection of protocol complexes $({𝒫}^r,{\pi }^r)$ for every round $r$. However, due to the fact that these protocols perform the same actions each round, in certain cases such protocols can be understood as functorial transformations of the input complex. We describe this construction in the following sub-section.

For round-based, content-neutral, full-information models, the protocol complex is simply defined and appears as a functorial construction describing how the simplices (i.e. global states) of the input complex are modified by the action of the protocol in one round. The full scope of the correspondence between protocols and functors is not fully known, but we describe the functorial construction for our protocols in Appendix A.5. More precisely, we consider protocols that are

• $\mathrm{■}$

  Round-based: the communication scheme is temporally organized into rounds, the information only flows inside a given round.

• $\mathrm{■}$

  Full-information: the distributed system can be described by the tuple of the local states and a process has no limit on the size of information it can share. This implies that it is possible to “store and forward” all information received (doing this repeatedly is called full information algorithm in distributed computing).

• $\mathrm{■}$

  Content-neutral: the way information is transmitted (or not) does not depend on the actual content of this information.

For the purposes of this paper, a protocol is a pair $(\mathrm{\Pi },\pi )$ where $\mathrm{\Pi }:\mathrm{𝐬𝐂𝐨𝐦𝐩}\to \mathrm{𝐬𝐂𝐨𝐦𝐩}$ is a functor and $\pi$ is a natural transformation between $U:\mathrm{𝐬𝐂𝐨𝐦𝐩}\to {\mathrm{𝐏𝐨𝐬}}_f$, the forgetful functor, and $V\circ 𝒟\circ \mathrm{\Pi }:\mathrm{𝐬𝐂𝐨𝐦𝐩}\to {\mathrm{𝐏𝐨𝐬}}_f$, where $V:{\mathrm{𝐃𝐋}}_f\to {\mathrm{𝐏𝐨𝐬}}_f$ is the forgetful functor. Given a simplicial complex $𝒞$, we require the component ${\pi }_{𝒞}:𝒞\to 𝒟(\mathrm{\Pi }(𝒞))$ to be a protocol map. Furthermore, due to the full-information hypothesis, the join-lifts of the ${\pi }_{𝒞}$ are assumed to be injective maps, see Appendix A.5. Due to this naturality condition, we may consider the components ${\pi }_{{\mathrm{\Pi }}^n(𝒞)}$ for each $n\in \mathbb{N}$, which to simplify notation below we denote by ${\pi }_n$, obtaining a sequence of maps in the category $\mathrm{𝐃𝐋}$:

For $n\le n^{\prime }$, we denote by ${\pi }_{n,n^{\prime }}^{\vee }:𝒟({\mathrm{\Pi }}^n(𝒞))\to 𝒟({\mathrm{\Pi }}^{n^{\prime }}(𝒞))$ the composition ${\pi }_n^{\vee }\circ \mathrm{\cdots }\circ {\pi }_{n^{\prime }-1}^{\vee }$. We also denote by ${\rho }_{𝒞}$ the dual map associated to ${\pi }_{𝒞}^{\vee }$, thereby obtaining a natural transformation $\rho :U\circ \mathrm{\Pi }\to U$. This is called the dual natural transformation associated to $\pi$. Since duality sends monos to epis and the ${\pi }_{𝒞}^{\vee }$ are injective, the maps ${\rho }_{𝒞}$ are surjective.

This functorial definition of protocol maps has also been proposed in [15, Section 4], but without the associated natural transformation. Moreover, it is consistent with the description of many well-studied distributed protocols. For example, the Immediate Iterated Snapshot ($IIS$) protocol corresponds functorially to the barycentric subdivision, and its carrier maps can be defined as natural transformations, see Section A.4.

Applying Birkhoff duality to the sequence (1), or equivalently using the dual natural transformation associated to $\pi$, we deduce the existence of order-preserving maps ${\rho }_n:{\mathrm{\Pi }}^{n+1}(ℐ)\to {\mathrm{\Pi }}^n(ℐ)$ on the underlying simplicial complexes. This gives rise to a projective limit system

in the category of spectral spaces, since each ${\mathrm{\Pi }}^n(ℐ)$ is a spectral space when endowed with the Alexandrov topology. The theory of spectral spaces [20] tells us that the limit of this diagram, which we denote by ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$, is a spectral space. We denote by ${\rho }_{n^{\prime },n}:{\mathrm{\Pi }}^{n^{\prime }}\to {\mathrm{\Pi }}^n$ the composition ${\rho }_{n^{\prime }}\circ \mathrm{\cdots }\circ {\rho }_{n-1}$, i.e. the dual of ${\pi }_{n,n^{\prime }}^{\vee }$, and by ${\lambda }_n:{\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)\to {\mathrm{\Pi }}^n(ℐ)$ the canonical projections associated with the limit construction. Note that since each ${\rho }_n$ is surjective, so are the ${\lambda }_n$.

Moreover, since we consider up-sets as open sets, the colimit of the dual diagram (1) which we denote by ${𝒟}^{\mathrm{\infty }}(ℐ)$, is the lattice of closed sets of ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ whose complements are compact, which generate its closed sets under arbitrary intersections and finite unions. We denote by $i_n:𝒟({\mathrm{\Pi }}^n(ℐ))\to {𝒟}^{\mathrm{\infty }}(ℐ)$ the canonical maps associated with the colimit, which by duality are injective, see Remark 2. Summing this up, we obtain our first theorem.

Here we describe the spectral space ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ concretely. Indeed, we show that points in ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ correspond to certain sequences of simplices and explicitly describe its topology. This will lead us nicely to our main result, namely that the topology on ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ characterizes task solvability, see Theorem 6 below. To this end, we consider sequences ${({\sigma }_n)}_n$ of simplices such that for all $n$,

• $\mathrm{■}$

  ${\sigma }_n\in {\mathrm{\Pi }}^n(ℐ)$,

• $\mathrm{■}$

  ${\sigma }_{n+1}\in {\pi }_n(\downarrow {\sigma }_n)$, or equivalently, ${\rho }_n({\sigma }_{n+1})={\sigma }_n$.

We call these protocol sequences. Since ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ is the limit of the sequence (2), we have [8, Section 2.3.9] that the underlying set of ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ is $\{(\sigma )\in \prod {\mathrm{\Pi }}^n(ℐ)\mid {\rho }_n({\sigma }_{n+1})={\sigma }_n\},$ that is, the set of protocol sequences. By [8], the specialization order $⪯$ on ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$ is determined point-wise. More explicitly, given protocol sequences $(\sigma )$ and $(\tau )$, we have $(\sigma )⪯(\tau )$ if, and only if, for all $n$ ${\sigma }_n{⪯}_n{\tau }_n$, where ${⪯}_n$ is the specialization order in the finite $T_0$ space ${\mathrm{\Pi }}^n(ℐ)$. The latter is given by ${\sigma }_n{⪯}_n{\tau }_n\iff \uparrow {\sigma }_n\subseteq \uparrow {\tau }_n,$ whereby we deduce $(\sigma )⪯(\tau )$ if, and only if, ${\sigma }_n\ge {\tau }_n$ for all $n$. Finally, we have the following characterization of ${\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)$. See also Appendix A.4 for a full description of the spectral space associated to the $IIS$ protocol.

We say that a protocol solves a task $(ℐ,𝒪,\mathrm{\Delta })$ if there exists an $n\in \mathbb{N}$ and a simplicial map $\delta :{\mathrm{\Pi }}^n(ℐ)\to 𝒪$, such that for all $\sigma \in {\mathrm{\Pi }}^n(ℐ)$, ${\delta }_{\ast }({\pi }_{0,n}(\sigma ))\subseteq \mathrm{\Delta }(\sigma )$. Remarking that in full information models, distributed algorithms have a canonical presentation as full information algorithms, this is the classical definition of the simplicial semantics of distributed computing (see e.g. [17]), which we reformulate exclusively in terms of down-set lattices. Unwinding the definitions of the join-lift of a map and using the adjunction between inverse and direct images, one easily proves that the diagram on the left sub-commutes if, and only if, the diagram on the right sub-commutes, i.e. for $A\in 𝒟(ℐ)$, ${\pi }_{0,n}^{\vee }[A]\le {\delta }^{-1}[{\mathrm{\Delta }}^{\vee }[A]$. Note that the right-hand diagram is not in $\mathrm{𝐃𝐋}$ since ${\mathrm{\Delta }}^{\vee }$ only preserves joins in general.

Given a task $(ℐ,𝒪,\mathrm{\Delta })$ and a protocol $(\mathrm{\Pi },\pi )$, we say that a spectral map $f:{\mathrm{\Pi }}^{\mathrm{\infty }}(ℐ)\to 𝒪$ is carried by $\mathrm{\Delta }$ provided that $i_0[A]\le f^{-1}[{\mathrm{\Delta }}^{\vee }[A]]$.

Finally, we recall that the geometric realization $𝒞$ of a simplicial complex $𝒞$ is, roughly speaking, the interpretation of each $n$-simplex as the convex hull of $n+1$ linearly independent points in ${ℝ}^{n+1}$, glued along common sub-simplices, see [14, p. 7] for a more detailed account. As above for spectral maps, we say that a continuous map $f:ℐ\to 𝒪$ is carried by $\mathrm{\Delta }$ provided that, for all $\sigma \in ℐ$, $f(\sigma )\subseteq \mathrm{\Delta }(\sigma )$. In [17, Thm. 4.2.3], the authors show that for the $IIS$ protocol, task-solvability is equivalent to the existence of a continuous map $ℐ\to 𝒪$ carried by $\mathrm{\Delta }$, see Theorem 8 in the Appendix. The goal of this section is to generalize this groundbreaking topological characterization of task-solvability.

Before formulating our main result, we first prove the following lemma: