A General Class of Reductions and Extension-Based Proofs

The way of composing multiple protocols in [10] can be generalized to a larger class of reductions. Note that these protocols are assumed to be transparent which means that the entity that tries to compose the protocols knows everything about these protocols. We present some properties of this composition that are necessary for discussions of the construction of an extension-based prover in both this paper and in [10], but are missing in the previous work. For example, a protocol in an extension-based proof is not a transparent protocol as assumed in the composition of multiple protocols, as the prover can only learn information about it by submitting queries to it. The usage of this composition in the discussions about extension-based proofs must be inspected in a more rigid way.

Next, we prove that if the task $𝒯$ reduces to the task $𝒮$ using multiple instances of $𝒮$ and $𝒯$ has an augmented extension-based proof that it is impossible to solve in the NIIS model, then $𝒮$ has a multiple-instance extension-based proof that it is impossible to solve in the NIIS model. Our proof is not a trivial generalization of the proof in [10]. A technical difference here is that when the reduction from $𝒯$ to $𝒮$ involves more than one instance of $𝒮$, we have to discuss a new version of extension-based proofs, called multiple-instance extension-based proofs, where the prover interacts with multiple instances of the protocol (instead of only one instance of the protocol in the original definition). Then, similar to the approach in [10], we describe how to construct a multiple-instance extension-based prover ${𝒫}_S$ from an extension-based prover ${𝒫}_T$. Given a protocol that claims to solve the task $𝒮$, the prover ${𝒫}_S$ simulates an interaction between the composed protocol and ${𝒫}_T$. ${𝒫}_S$ decides which queries it will submit in its interaction with multiple instances of the protocol that claims to solve $𝒮$, based on the queries it sees in this simulation. We will show that ${𝒫}_S$ wins in the interaction since ${𝒫}_T$ wins in its interaction with $𝒯$ by assumption.

A snapshot object consists of an array of elements and supports two types of operation: write and read. In a write operation, a process with id $i$ writes a value to the $i$-th cell of the array. In a snapshot operation, a process atomically reads the contents of all the cells of the array. Similarly, the immediate snapshot (IS) object was introduced by Borowsky and Gafni in [8]. An IS object consists of an array of elements and provides writeread operations, where a process with id $i$ writes a value to the $i$-th element of the array and returns a snapshot of the array immediately after this write. The writeread operations on a single IS object by multiple processes are said to be concurrent if all their snapshot operations happen after all their writes to the array are finished.

IS objects are the basic building blocks of the iterated immediate snapshot (IIS) model. The IIS model consists of $n$ processes $\mathrm{\Pi }=\{u_1,u_2\mathrm{\dots }{u}_n\}$ and a bounded sequence of IS objects $\{I{S}_1,I{S}_2\mathrm{\dots }I{S}_e\}$. In the execution of a protocol in the IIS model, each process will terminate after performing a writeread operation on each IS object in ascending order in the sequence. The IIS model has been shown to have computational power equivalent to that of the standard shared memory model in [1, 8].

Hoest and Shavit [15] introduced a new model called the non-uniform iterated snapshot (NIIS) model, a variant of the iterated immediate snapshot (IIS) model. The NIIS model consists of $n$ processes $\mathrm{\Pi }=\{u_1,u_2\mathrm{\dots }{u}_n\}$ and an unbounded sequence of IS objects $\{I{S}_1,I{S}_2\mathrm{\dots }\}$. Each process starts with a process id $i$ and its input value $v_i$, and performs a writeread operation on each IS object sequentially. By definition, each NIIS protocol is determined by a decision map $\delta$ from a local state to output values (or a special value $⟂$). In the execution of an NIIS protocol $\delta$, each time a process completes a writeread operation, it checks whether it has reached a final state by applying $\delta$ to its local state variable. If $\delta$ returns $⟂$, the process continues to access the next IS object. Otherwise, the process uses the return value of $\delta$ as its output and terminates. An NIIS protocol is said to be transparent to some entity if this entity knows everything about the function $\delta$. In this paper, we consider full-information NIIS protocols in which each process uses its current state as an argument to perform a writeread operation. After a writeread operation, its new state consists of its process id $i$ and the result of the writeread operation. Note that unlike the IIS model, the NIIS model allows different processes to terminate after accessing a different number of IS objects.

A configuration of a protocol consists of the state of each process and the contents of each IS object. Since each process remembers its entire history and only process $p_i$ can write to the $i$-th component of each IS object, the state of each IS object is included in states of the processes, which means that a configuration is fully determined by the states of processes. A process is active in a configuration if it is not terminated. A configuration is final if it has no active processes. If $C$ is a configuration and $U$ is a set of processes that are poised to perform writeread operations on the same IS object, then $C\{U\}$ is the configuration that results from $C$ when the processes in $U$ concurrently take a step in the protocol. A schedule of a protocol from $C_0$ is a finite or infinite sequence of sets of processes $\gamma =U_1,U_2\mathrm{\dots }$ such that there is a sequence of configurations $C_0,C_1\mathrm{\dots }$ where processes in $U_i$ is active in $C_{i-1}$ and $C_i=C_{i-1}{U}_i$ for all $U_i$ in $\gamma$. A $U$-only schedule from $C$ is a schedule in which only processes in $U$ appear. Each finite schedule from an initial configuration results in a reachable configuration. A protocol is wait-free if each process is terminated after a finite number of steps.

A task $𝒯$ consists of a finite set of input vectors, $I$, a finite set of output vectors, $O$, and a map $T:I\to 2^O$ that represents the task specification. For each input vector $x\in I$, $T$ maps $x$ to a non-empty set $T(x)\subseteq O$ of output vectors. Suppose that $A$ is a wait-free protocol that has an initial configuration with input vector $x$ for each $x\in I$. We say that a protocol $A$ solves $𝒯$ if, for each $x\in I$, every final configuration that is reached from the initial configuration of $A$ that has input vector $x$ has output vector $y$ and $y\in T(x)$. If $𝒯$ and ${𝒯}^{{}^{\prime }}$ are tasks with maps $T$ and $T^{{}^{\prime }}$, respectively, their composition $𝒯\circ {𝒯}^{{}^{\prime }}$ is a task that has the same set of input vectors as $𝒯$ and the same set of output vectors as ${𝒯}^{{}^{\prime }}$. The map of the composed protocol is defined by $T^{{}^{\prime }}\circ T(x)=\cup \{T^{{}^{\prime }}(y)|y\in T(x)\}$.

In [3], Alistarh, Aspnes, Ellen, Gelashvili and Zhu formally defined the class of extension-based proofs that generalizes the impossibility proof technique used in the FLP impossibility result. The proof of impossibility is modeled as an interaction between a prover and a wait-free NIIS protocol that claims to solve the task. The protocol is defined by a map $\delta$ from the process states to the output values or a special value $⟂$. The prover asks queries to learn information about the protocol, such as the $\delta$ values of states of processes in some reached configuration, in an effort to find a violation of the task specification, or construct an infinite execution.

If there exists a prover that can defeat any protocol that claims to solve the task, we say that the task has an extension-based impossibility proof. But if for each prover, an adversary can adaptively design a protocol based on the queries made by the prover such that the prover cannot win in the interaction, there is no extension-based proof for the impossibility of the task. The adaptive protocol constructed by the adversary will be referred to as an adversarial protocol as in [3].

Three classes of extension-based proofs are defined in [3, 10]. We will first introduce restricted extension-based proofs. The interaction between the prover and a protocol proceeds in phases. In each phase $\phi$ the prover starts with a finite schedule $\alpha (\phi )$ and a set of configurations $𝒜(\phi )$ reached from some initial configurations of the task by $\alpha (\phi )$ which only differ in the input values of processes that are not in the schedule $\alpha$. For $\phi =1$, the schedule $\alpha (1)$ is the empty schedule and $𝒜(1)$ contains all initial configurations. The set of configurations reached in phase $\phi$ is denoted by ${𝒜}^{{}^{\prime }}(\phi )$ which is empty at the beginning of phase $\phi$. The prover queries the protocol by choosing a configuration $C\in 𝒜(\phi )\bigcup {𝒜}^{{}^{\prime }}(\phi )$ and a set of processes $U$ that are poised to perform writeread operations on the same IS object in $C$. The protocol replies with the value of $\delta$ of each process in $U$ in the configuration $C^{{}^{\prime }}$ resulting from the processes in $U$ concurrently performing writeread operations, and the prover adds the configuration $C^{{}^{\prime }}$ to ${𝒜}^{{}^{\prime }}(\phi )$. A chain of queries is a (finite or infinite) sequence of queries such that if $(C_i,U_i)$ and $(C_{i+1},U_{i+1})$ are consecutive queries in the chain, then $C_{i+1}$ is the configuration resulting from scheduling $U_i$ from $C_i$. The prover is allowed to construct finitely many chains of queries in a phase.

When the output values from the response of a query are not allowed output values for the task, we say that the prover finds a violation of the task specification. Similarly, if a prover can construct an infinite chain of queries, the protocol must admit that it is not wait-free. If the prover does not find a violation or construct an infinite execution after a finite number of queries or chains of queries, it must end the current phase and choose some configuration $C^{{}^{\prime }}\in {𝒜}^{{}^{\prime }}(\phi )$. Let ${\alpha }^{{}^{\prime }}$ be the schedule such that $C^{{}^{\prime }}$ is reached via ${\alpha }^{{}^{\prime }}$ from some configuration in $𝒜(\phi )$. The schedule $\alpha (\phi ){\alpha }^{{}^{\prime }}$ will be used as the initial schedule $\alpha (\phi +1)$ in the next phase. Suppose that the configuration $C^{{}^{\prime }}$ is reached from an initial configuration $C_{ini}$. Then $𝒜(\phi +1)$ consists of all configurations reached by the schedule $\alpha (\phi +1)$ from initial configurations that only differ from $C_{ini}$ by the input values of the processes that do not appear in $\alpha (\phi +1)$.

Extension-based proofs allow for an additional type of query. The prover performs an output query by choosing a configuration $C\in 𝒜(\phi )\bigcup {𝒜}^{{}^{\prime }}(\phi )$, a set of processes $U$ that are poised to access the same IS object, and a value $y\in \{0,1,\mathrm{\dots },k\}$. If there is a $U$-only schedule from $C$ that results in a configuration in which a process in $U$ outputs $y$, the protocol will return some such schedule. Otherwise, the protocol returns $NULL$. Augmented extension-based proofs provide a more general query, called an assignment query. An assignment query consists of a configuration $C\in 𝒜(\phi )\bigcup {𝒜}^{{}^{\prime }}(\phi )$, a set of processes $U$, and an assignment function $f$ from a subset $U^{{}^{\prime }}$ of $U$ to the output values. If there is a $U$-only schedule from $C$ that results in a configuration in which the output value of each process $u$ in $U^{{}^{\prime }}$ is $f(u)$, the protocol will return some such schedule. Otherwise, the protocol will return $NULL$. It is shown that an output query $(C,U,y)$ can be simulated by a sequence of assignment queries $(C,U,f_u)$ for each process $u$ in [10]. Therefore, we will discuss only augmented extension-based proofs in subsequent sections.

The tasks which have been proved to have no extension-based proofs of the impossibility are still quite limited. It is proved in [3, 2] that the $(n,k)$-set agreement task does not have extension-based proofs of the impossibility in the NIIS and NIS models. Some similar results on the approximate agreement task are proved in [4, 16]. Shi and Liu [18] gave a topological characterization of a colorless task to have no extension-based proofs of impossibility.

Attiya, Castañeda, and Rajsbaum [5] studied the limitations of valency arguments in the IIS model. Note that in the IS and IIS models, extension-based proofs are too powerful. They define the class of local valency impossibility proofs, that cannot show there is no wait-free protocol for $(n,n-1)$-set agreement, weak symmetry breaking or $(2n-2)$-renaming in the IIS model. Attiya, Fraigniaud, Paz and Rajsbaum [6] introduced an FLP-style impossibility proof which is a simple case of extension-based proofs and local valency impossibility proofs, and showed that there are no FLP-style proofs of the impossibility of any 1-dimensional colorless task if it is not wait-free solvable.

If a task $𝒯$ reduces to a task $𝒮$, then there exists a protocol $A_{l+1}^{{}^{\prime }}\circ A_l\circ A_l^{{}^{\prime }}\mathrm{\cdots }{A}_1\circ A_1^{{}^{\prime }}$ that solves the task $𝒯$ where each $A_i$ is a protocol to solve the task $𝒮$ and each $A_i^{{}^{\prime }}$ is an NIIS protocol for some task ${ℛ}_i$. We assume that the number of instances of the protocol to solve $𝒮$ is a constant. We say that $({ℛ}_1,{ℛ}_2,\mathrm{\dots }.{ℛ}_l,{ℛ}_{l+1})$ is a reduction from a task $𝒯$ to a task $𝒮$.

Previous work[10] used a restricted version of this definition in which only one instance in this composition is a protocol that solves the task $𝒮$. The restricted version of reductions in their paper is enough to prove the non-existence of extension-based proofs for many tasks. But some reductions use multiple instances of $𝒮$, such as the reduction given by [13] from weak symmetry breaking to $(n-1)$-set agreement, which uses two instances of $(n-1)$-set agreement.

The composition of NIIS protocols is much more complicated than the composition of IIS protocols, as processes can terminate after different rounds during the execution of some NIIS protocol. To compose IIS protocols, we can simply have each process execute IIS protocols sequentially. Since each process ends the execution of a protocol after the same round, the information used in the execution of different IIS protocols will not be mixed together. But this is not true for NIIS protocols, since processes accessing the same IS object in the composed protocol may be running different NIIS protocols. We need a mechanism to separate information from different NIIS protocols.

Let $A_1$ and $A_2$ be NIIS protocols such that each output from $A_1$ is a possible input for $A_2$. We temporarily assume that everything about $A_1$ and $A_2$ is known (this is not true in the construction of ${𝒫}_S$). In [10], Brusse and Ellen provided an implementation of the composed protocol $A_2\circ A_1$ in the NIS model using estimate vectors introduced by Borowsky and Gafni [9]. The composition of two NIIS protocols in our paper can use almost identical techniques. But since this is quite important in this paper, we have to explain it in detail. Let $I{S}_h^{{}^{\prime }}$, $I{S}_h^{{}^{\prime \prime }}$ and $I{S}_h$ denote the $h$-th IS object accessed by processes in the schedules of $A_1$, $A_2$, and $A_2\circ A_1$, respectively. Each process $u_i$ simulates the steps of $u_i$ in protocol $A_1$ followed by the steps of $u_i$ in protocol $A_2$. The result of a writeread operation in simulation of $A_1$ can be obtained from some writeread operation of the composed protocol. Since different processes may terminate after different rounds in $A_1$, the result of a writeread operation in the simulation of $A_2$ cannot be easily obtained. Each process locally maintains an infinite sequence of estimate vectors, each with $n$ components. The $h$-th estimate vector of process $u_i$ is a potential output of the writeread operation on $I{S}_h^{{}^{\prime \prime }}$ in the simulation of $A_2$.

Let $\gamma$ be a schedule of the composed protocol $A_2\circ A_1$ from some initial configuration $C_{ini}$. Each process updates its estimate vectors during this schedule of the composed protocol $A_2\circ A_1$, and finalizes its $i$-th estimate vector after collecting enough information. This estimate vector can be proved to be equivalent to the return value of the writeread operation to $I{S}_i^{{}^{\prime \prime }}$ by the same process in some schedule of the second NIIS protocol. We can call this schedule the restriction of $\gamma$ to $A_2$. A process will apply the function $\delta$ that specifies the second protocol to the finalized estimate vector to decide whether it should end the simulation of $A_2$ (and which value to output if so).

We give some pseudocode in Algorithm 1. The process $u_i$ performs writeread operations to $I{S}_1,I{S}_2\mathrm{\cdots }$ sequentially, with $h_i$ indicating the next IS object to be accessed. The value written to $I{S}_i$ by a process consists of three parts: r (round number), state1 (state in the simulation of $A_1$) and state2 (state in the simulation of $A_2$). The round number is 0 when the process is simulating $A_1$, is $r$ when simulating the $r$-round of $A_2$. The attribute $state2$ is a sequence of estimate vectors.

When a process simulates $A_1$, it computes the result of the writeread operation on $I{S}_i^{{}^{\prime }}$ from the result of the writeread operation on $I{S}_i$ by ignoring the attribute $state2$. However, a process $u_i$ will update its estimate vectors using the result as described in Algorithm 2. $u_i$ updates the $k^{{}^{\prime }}$-th component of its $k$-th estimate vector when this component is blank and the result of a writeread operation on $I{S}_{h_i}$ contains some estimate vectors from some other process, where the $k^{{}^{\prime }}$-th component of its $k$-th estimate vector is not blank. After a process $u_i$ has finished simulating $A_1$, it modifies its first estimate vector to include its output of $A_1$ as the input for $A_2$ and then tries to finalize it. To finalize its $r_i$-th estimate vector, for any $r_i\ge 1$, the process repeatedly performs a writeread operation on the next IS object $I{S}_{h_i}$ (to contain its first $r_i$ estimate vectors). The process updates its estimate vectors just as it does when simulating $A_1$. The process does not finalize its $r_i$-th estimate vector in two cases. The first case is that it sees some other process $u_i^{{}^{\prime }}$ accessing $I{S}_{h_i}$ when that process was simulating $A_1$ or an earlier round of $A_2$. This is to avoid process $u_i^{{}^{\prime }}$, which is simulating an earlier round, from missing the finalized $r_i$-th estimate vector of process $u_i$. The other case is that it changes its $r_i$-th estimate vector using information from $I{S}_{h_i}$.

Otherwise, the process finalizes its $r_i$-th estimate vector. When a process finalizes its $r_i$-th estimate vector, this vector will be used as the output of its writeread operation on $I{S}_{r_i}^{{}^{\prime \prime }}$ in the simulation of $A_2$. Note that it may take many rounds of the composed protocol for a process to finalize its current estimate vector, i.e. to take a step in the simulated execution. Based on the return values of its $r_i$-th estimate vector, the process terminates its simulation of $A_2$ or modifies its $(r_i+1)$-th estimate vector to include its new state in the simulation of $A_2$ and continues to finalize its $(r_i+1)$-th estimate vector.

Now we present some properties that are necessary in Section 4. The first property was shown in [10].

The second property is about restrictions. Given an initial configuration $C_{ini}$ of $A_2\circ A_1$, the composed protocol simulates a schedule of $A_1$ from $C_{ini}$, followed by a schedule of $A_2$, where the output of the first schedule serves as input to the second schedule. Let $\gamma$ be a schedule of $A_2\circ A_1$ from $C_{ini}$. The restriction of $\gamma$ to $A_1$ is defined as the schedule ${\gamma }_1$ obtained from $\gamma$ by removing all the occurrences of each process after simulating $A_1$. Each process $u_i$ finishes its simulation of $A_1$ with output $y_i$ during the schedule $\gamma$ of $A_2\circ A_1$ from $C_{ini}$ if and only if $u_i$ terminates with output $y_i$ during the schedule ${\gamma }_1$ of $A_1$ from $C_{ini}$.

Let $U$ be the set of processes that complete their simulation of $A_1$ during $\gamma$ and, for each $u_i\in U$, let $y_i$ be its simulated output from $A_1$. Let $C_2$ be any initial configuration of $A_2$ in which each process $u_i\in U$ has input $y_i$. We have to prove that, for each $l$, the $l$-th estimate vectors that have been finalized by the processes in $U$ correspond to the responses of the writeread operations in some $U$-only schedule ${\gamma }_2$ of $A_2$ from $C_2$. Each process $u_i$ finishes its simulation of $A_2$ with output $z_i$ during the schedule $\gamma$ of $A_2\circ A_1$ from $C_{ini}$ if and only if $u_i$ terminates with output $z_i$ during the schedule ${\gamma }_2$ of $A_2$ from $C_2$. The restriction of $\gamma$ to $A_2$ is defined as the schedule ${\gamma }_2$. Note that we are using the same definition as in [10] except that we are using the NIIS model rather than the NIS model.

The composition of multiple NIIS protocols $A_m\mathrm{\cdots }{A}_2\circ A_1$ can be derived from the composition of two NIIS protocols. Inductively, $A_m\mathrm{\cdots }{A}_2\circ A_1$ is the composition of $A_1$ and $A_m\mathrm{\cdots }{A}_3\circ A_2$. Let $\gamma$ be a schedule of $A_m\mathrm{\cdots }{A}_2\circ A_1$ from some initial configuration $C$. Let $\gamma (1)$ denote the restriction of $\gamma$ to $A_1$, $\gamma (2)$ denote the restriction of $\gamma$ to $A_m\mathrm{\cdots }{A}_3\circ A_2$. The restriction of $\gamma$ to $A_j$, where $2\le j\le m$, can be defined inductively as the restriction of $\gamma (2)$ to $A_j$. The properties proved in Section 3.2 also apply to the composition of multiple NIIS protocols.

In the following sections, we extend the proof in [10] to more general reductions. Suppose that $𝒯$ reduces to $𝒮$ and ${𝒫}_T$ is an augmented extension-based prover that can win against any protocol that claims to solve $𝒯$. Our goal is to construct an augmented extension-based prover ${𝒫}_S$ for task $𝒮$ that can also win against any protocol $A$ that claims to solve $S$.

${𝒫}_S$ will simulate an interaction between ${𝒫}_T$ and the composed protocol $A_{l+1}^{{}^{\prime }}\circ A_l\circ A_l^{{}^{\prime }}\mathrm{\cdots }{A}_1\circ A_1^{{}^{\prime }}$, and will use restrictions to interact with multiple copies of $A$, as shown in Figure 1. There is an interaction between ${𝒫}_T$ and the composed protocol in Figure 1. But at the same time, if we regard the elements within the black frame as a prover ${𝒫}_S$, the interaction can be seen to happen between ${𝒫}_S$ and multiple instances of $A$.

If the prover ${𝒫}_T$ submits a query in the simulation, the prover ${𝒫}_S$ will reinterpret this query as queries to some instances of $A$ and will use the responses of the instances of the protocol $A$ and its knowledge about the protocols $A_1^{{}^{\prime }},\mathrm{\cdots }{A}_l^{{}^{\prime }},A_{l+1}^{{}^{\prime }}$ to generate a response to the original query. The most important idea of this section is that during the interaction between ${𝒫}_T$ and the composed protocol, ${𝒫}_S$ interacts with each instance $A_i$ to resume the logical executions of the NIIS protocols. Since the prover ${𝒫}_T$ is going to win against the composed protocol, there must be something wrong within the workflow. This can only happen in interactions between ${𝒫}_S$ and some copy of $A$, which means that ${𝒫}_S$ wins in the interaction with some copy.

The prover ${𝒫}_S$ will independently interact with a constant number of instances of the protocol $A$. Note that we are using a different definition of prover here. In the standard definition, an extension-based prover interacts with a single instance of the protocol. A multiple-instance extension-based prover interacts with multiple instances of the same protocol $A$ and maintains a separate set of arguments (i.e. all arguments an extension-based prover will maintain during its interaction with a protocol) recording its interaction with each instance of $A$. For example, ${\varphi }_i$ and ${\varphi }_j$, representing the current phases of interactions with $A_i$ and $A_j$ can be different.

A multiple-instances prover submits queries to each instance individually. It can use the response from any query to decide what to do next (such as how to submit a query in the interaction with another instance of $A$). But we do not allow a multiple-instance prover to use responses from different instances to produce a conflict even when the protocol $A$ responds with different output values for a single schedule in its interaction with different instances. A multiple-instance prover wins if it can win in the interaction with some instance using only the information obtained from this instance. Otherwise, the protocol wins. It is easy to see that a multiple-instance extension-based prover is at least as powerful as an extension-based prover since a multiple-instance extension-based prover can choose to interact with one instance only.

Let $\gamma$ be a schedule of the composed protocol $A_{l+1}^{{}^{\prime }}\circ A_l\circ A_l^{{}^{\prime }}\mathrm{\cdots }{A}_1\circ A_1^{{}^{\prime }}$ from some initial configuration $C_{ini}$ to some configuration $C$. The restriction of $\gamma$ to a protocol $A_i^{{}^{\prime }}$ or $A_i$ is defined in Section 3.3, denoted by ${\gamma }_i^{{}^{\prime }}$ and ${\gamma }_i$. By Lemma 3, given a schedule $\gamma$ of the composed protocol, the prover ${𝒫}_S$ can compute the restriction of $\gamma$ to any $A_i^{{}^{\prime }}$ or $A_i$.

An initial configuration $C_i$ of $A_i$ is defined as compatible with some configuration $C_i^{{}^{\prime }}{\gamma }_i^{{}^{\prime }}$ of $A_i^{{}^{\prime }}$ if the output value of every process terminated in $C_i^{{}^{\prime }}{\gamma }_i^{{}^{\prime }}$ is the input value of the same process in $C_i$. An initial configuration $C_{i+1}^{{}^{\prime }}$ of $A_{i+1}^{{}^{\prime }}$ is defined to be compatible with some configuration $C_i{\gamma }_i$ of $A_i$ if the output value of every process terminated in $C_i{\gamma }_i$ is the input value of the same process in $C_{i+1}^{{}^{\prime }}$.

In the simulation, ${𝒫}_S$ maintains the following invariant. Suppose that ${𝒫}_T$ has reached the configuration $C=C_{ini}\gamma$ of the composed protocol $A_{l+1}^{{}^{\prime }}\circ A_l\circ A_l^{{}^{\prime }}\mathrm{\cdots }{A}_1\circ A_1^{{}^{\prime }}$. Then there exist initial configurations $C_1^{{}^{\prime }},C_1,C_2^{{}^{\prime }},\mathrm{\dots },C_l,C_{l+1}^{{}^{\prime }}$ of the protocols $A_1^{{}^{\prime }},A_1,A_2^{{}^{\prime }},\mathrm{\dots }{A}_l,A_{l+1}^{{}^{\prime }}$ such that, for all $1\le i\le l$, $C_i$ is compatible with $C_i^{{}^{\prime }}{\gamma }_i^{{}^{\prime }}$, $C_{i+1}^{{}^{\prime }}$ is compatible with $C_i{\gamma }_i$, and ${𝒫}_S$ has reached configuration $C_i{\gamma }_i$ in its interaction with $A_i$. Let $\psi$ denote the current phase of the simulated interaction, and let ${\varphi }_i$ denote the current phase of $A_i$ for each $1\le i\le l$. ${\alpha }_i({\varphi }_i)$ is a prefix of ${\gamma }_i$ for each $1\le i\le l$.

At the beginning of the simulation, ${𝒫}_T$ starts with an empty schedule and has reached the initial configurations of the composed protocol $A_{l+1}^{{}^{\prime }}\circ A_l\circ A_l^{{}^{\prime }}\mathrm{\cdots }{A}_1\circ A_1^{{}^{\prime }}$. For each $1\le i\le l$, the interaction between ${𝒫}_S$ and $A_i$ also starts with an empty schedule and has reached the initial configurations of $A_i$. Since every initial configuration of $A_i^{{}^{\prime }}$ is compatible with every initial configuration of $A_i$, the invariant holds at the start of phase 1 of the simulated interaction. We will discuss the strategy that the prover ${𝒫}_S$ will use in interactions with these instances of $A$ when ${𝒫}_T$ submits a query, submits an assignment query, or ends a phase in the simulation.