In this post I describe the Asynchronous Computability Theorem, which uses tools from Algebraic Topology to show whether a task is solvable in a distributed system. The theorem yields quite readily to intuition, however we will take care to make our statements as precise as possible without getting too caught up in the details. Loosely speaking, the theorem states that a task is solvable with a distributed system if its input space maps continuously into its output space. In particular, a continuous mapping fails to exist when the spaces at hand are incompatible with respect to holes within them. The beauty of the theorem lies in that it provides a geometric interpretation of the execution of a distributed protocol, allowing us to draw on our innate intuition for space to tame the combinatorial explosion of states in concurrent computations. In what follows, we shall answer the following questions: What is a task? What does it mean for a task to be solvable with a distributed system? What are input and output spaces? What is a continuous map? Finally, we shall state the Asynchronous Computability theorem and use it to demonstrate the impossibility of consensus.
To gain intuition for tasks and solvability, we start with a well known impossibility result — Impossibility of Distributed Consensus with One Faulty Process. Known colloquially as the FLP result, it states that processes communicating over an asynchronous network can’t all agree on a proposal if even one of the processes fails. An asynchronous network is one where communication delays can be arbitrarily long. The task in this case is consensus. Solvability corresponds to whether there exists a terminating algorithm which the participating processes can run to come to consensus. Since it is impossible to distinguish between a communication delay and a failed process, any consensus algorithm may not be able to terminate if a process fails. More generally, k-set agreement refers to tasks where processes must agree on at most k distinct values. The consensus task in FLP is 1-set agreement. It has been shown that as long as k < n, the k-set agreement task is unsolvable with a wait-free protocol [8]. That the algorithm is deterministically terminating is a key stipulation of this impossibility result. In the next section, we discuss solutions to consensus wherein the termination property is relaxed.
In the analysis of distributed algorithms, we make assertions about the correctness of system states — safety properties, and the temporality of system states — liveness properties. Safety ensures that nothing bad happens, and liveness ensures that something eventually happens. The problem revealed by the FLP result is that of liveness — due to arbitrary timing delays, we can’t assert that a consensus algorithm will eventually terminate. Consensus protocols such as Paxos and Raft overcome this limitation through elaborate use of quorums and timeouts, or more generally, failure detectors [4]. Indeed, one can decompose the problem of consensus along safety and liveness properties — the alpha and omega of consensus [3]. Alpha captures the safety properties of consensus — agreement, validity, and integrity, whereas omega captures liveness properties — the eventual termination of the algorithm. It is this latter component of consensus that does not admit a wait-free protocol.
Consensus is solvable, but as demonstrated by FLP and the Asynchronous Computability Theorem, it is not wait-free solvable. Wait freedom is a particular type of progress condition:
No process can be prevented from completing an operation by undetected halting failures of other processes, or by arbitrary variations in their speed. [6]
In this way, wait-freedom gives us a type of fault-tolerance particularly important in a distributed system where components fail independently. This is a remarkable global reasoning property that ensures that each non-faulty process of a distributed protocol will make progress regardless of failures of other processes, and do so in a bounded number of steps. It should be noted that the wait freedom property is perhaps too strong — the absence of a wait-free protocol for a task does not mean it can’t be solved with weaker progress guarantees. For example, an achievable progress property for consensus is anon-blocking guarantee which states that eventually progress can be made — albeit slowed arbitrarily by retries in case of collision.
The system model used in defining the Asynchronous Computability Theorem is based on I/O automata. An I/O automaton is defined as a set of states, events and a transition relation. Individual processes are represented as automatons — Turing machines — with well-defined start and finish events, as well as events corresponding to interaction with a shared memory object. The shared memory object is a linearizable atomic read/write memory, represented as an automaton with events corresponding to read and write operations. Processes have exclusive write access to their memory cell, but may read the contents of memory cells belonging to other processes. A protocol is defined as a set of processes and a shared memory object.
Interestingly, the methodology used to establish the result in this post has been used to unify the synchronous and asynchronous message passing models.
Informally, a task is a problem in a distributed system. Formally, a task is a tuple ⟨I,O,Δ⟩ where I is a set of input vectors, O a set of output vectors and Δ a specification relation mapping inputs to outputs. An input vector represents a possible assignment of input values to the processes of a distributed system. Similarly, an output vector represents process outputs at the end of execution. Components of input and output vectors correspond to processes, such that I[i] represents the input to the i-th process and O[i] its output. If I[i] = ⊥ then process i does not participate in the execution. If a process i fails, then O[i]=⊥. ****The task specification relation Δ maps input vectors to sets of allowable output vectors.
Take for example the binary consensus task. Each process starts with an input value of 0 or 1 and at the end of execution, chooses 0 or 1 such that they all agree and the chosen value was some processes’s input. A task specification for a two process binary consensus task is shown in Figure 1 bellow:
| I | Δ(I) | I | Δ(I) |
|--------|-------------|-------|--------------|
| (0,⊥) | (0,⊥) | (1,⊥) | (1,⊥) |
| (⊥,0) | (⊥,0) | (⊥,1) | (⊥,1) |
| (0,0) | (0,0) | (1,1) | (1,1) |
| (0,1) | (0,0), (1,1) | (1,0) | (0,0), (1,1) |
Figure 1: Task specification for the 2 process binary consensus task.
Recall that a protocol is a collection of processes interacting through shared memory to solve a task. A protocol solves a task if 1) no process takes a infinite number of steps to finish, and 2) the output value of a process is consistent with the task specification Δ. A protocol wait-free solves a task if it solves the task even if all but one of the processes fail.