Manifest Deadlock-Freedom for Shared Session Types

The introduction of acquire-release, to ensure that the multiple clients of a shared process interact with the process in mutual exclusion from each other, gives rise to an obvious source of deadlocks, as acquire-release effectively amounts to a locking discipline. The typical approach to prevent deadlocks in that case is to impose a partial order on the resources and to “lock-up”, i.e., to lock the resources in ascending order. We adopted this strategy in Sect. 1 (Fig. 1) to break the cyclic dependencies among the acquires in the dining philosophers.

In Sect. 1, however, we also considered another example (Fig. 2) and discovered that cyclic acquisitions are not the only source of deadlocks, but deadlocks can also arise from interdependent acquisitions and synchronizations. In that example, we can prevent the deadlock by moving the acquire past the synchronization, in either of the two processes. Whereas in a purely linear session-typed system the sequencing of actions within a process do not affect other processes, the relative placement of acquire requests and synchronizations become relevant in a shared session-typed system.

Based on this observation, we can divide the processes in a shared-session discipline into competitors and collaborators. The former compete for a set of resources, whereas the latter do not overlap in the set of resources they acquire. For example, in the dining philosophers (Fig. 1), the philosophers \( p_0 \), \( p_1 \), and \( p_2 \) compete with each other for the set of forks \( f_0 \), \( f_1 \), and \( f_2 \), whereas the process that spawns the philosophers and the forks collaborates with either of them.

Transferring this idea to the process graph that emerges at run-time, we note that competitors are siblings whereas collaborators stand in a parent-descendant relationship. We illustrate this outcome on Fig. 3 that shows a possible run-time process graph for the dining philosophers. Linear processes are depicted as solid black circles with a white identifier and shared processes are depicted as dotted filled violet circles with a black identifier. Linear channels are depicted as black lines, shared channel references as dotted violet lines with the arrow head pointing to the shared process being acquired¹. The identifiers \(P_0\), \(P_1\), and \(P_2\) stand for the three philosophers, \(F_0\), \(F_1\), and \(F_2\) for the three forks, and T for the process that sets the table. The current run-time graph depicts the scenario in which \(P_1\) is eating, while the other two philosophers are still thinking.

Embedded in the graph is a tree that arises from the linear processes and the linear channels connecting them. For any two nodes in this tree, the parent node denotes the client process and the child node the providing process. We note that the independence principle (see Sect. 2), which precludes shared processes from depending on linear channel references, guarantees that there exists exactly one tree in the process graph, with the linear main process as its root. The shape of the tree changes when new processes are spawned, linear channels exchanged (through \(\otimes \) and \(\multimap \)), or shared processes acquired. For example, process \(P_2\) could acquire the shared fork \(F_0\), which then becomes a linear child process of \(P_2\), should the acquire succeed. As indicated by the shared channel references, the sibling nodes \(P_0\), \(P_1\), and \(P_2\) compete with each other for the nodes \(F_0\), \(F_1\), and \(F_2\), whereas the node T does not compete for any of the resources acquired by its descendants (including \(F_1\) and \(F_2\)). Our type system enforces this paradigm, as we discuss in the next section.

Invariants. Having identified the notions of collaborators and competitors, our type system must guarantee: (i) that collaborators acquire mutually disjoint sets of resources; (ii) that competitors employ a locking-up strategy for the resources they share; and, (iii) that competitors have released all acquired resources when synchronizing with other competitors. Invariant (ii) rules out cyclic acquisitions and invariants (i) and (iii) combined rule out interdependent acquisitions and synchronizations.

To express the high-level invariants above in our type system, we introduce the notion of a world – an abstract value that is equipped with a partial order – and associate such a world with every process. Programmers can create worlds, indicate the world at which a process resides at spawn time, and define an order on worlds. Moreover, we associate with each process a range of worlds that indicates the worlds of resources that the process may acquire. As a result, we obtain the following typing judgments: The typing judgments reveal that we impose worlds at the judgmental level, resulting in a hybrid system, in which the adjoint modalities for acquire-release are complemented with world modalities that occur as syntactic objects in propositions [7]. We use the notation \(x_m : A_m [{\omega _k}\updownarrow ^{\omega _n}_{\omega _l}]\) (where m stands for \(\mathsf {S}\) or \(\mathsf {L}\)) to associate worlds \(\omega _k\), \(\omega _l\), and \(\omega _n\) with a process that offers a session of type \(A_m\) along channel x. World \(\omega _k\) denotes the world at which the process resides. We refer to this world as the self world. Worlds \(\omega _l\) and \(\omega _n\) indicate the range of worlds of resources that the process may acquire, with \(\omega _l\) denoting the minimal (min) world in this range and \(\omega _n\) the maximal (max) one.

Process terms are typed relative to the order specified in \(\varPsi \) and the contexts \(\varGamma \), \(\varPhi \), and \(\varDelta \). As in Sect. 2, \(\varGamma \) is a structural context consisting of hypotheses on the typing of variables bound to shared channel references, augmented with world annotations. We find it necessary to split the linear context “\(\varDelta \)” from Sect. 2 into the two disjoint contexts \(\varPhi \) and \(\varDelta \), allowing us to separate channels that are possibly aliased (due to sharing) from those that are not, respectively. Both \(\varPhi \) and \(\varDelta \) consist of hypotheses on the typing of variables that are bound to linear channels, augmented with world annotations. \(\varPsi \) is presupposed to be acyclic and defined as: \( \varPsi \,\triangleq \,\cdot \,\mid \,\varPsi ', \; \omega _{ k } < \omega _{ l } \,\mid \,\varPsi ', \; \omega _{ o } \), where \(\omega \) stands for a concrete world \(\mathsf {w}\) or a world variable \(\delta \). We allow \(\varPsi \) to contain single worlds, to support singletons as well as to accommodate world creation prior to order declaration. We define the transitive closure \(\varPsi ^+\), yielding a strict partial order, and the reflexive transitive closure \(\varPsi ^*\), yielding a partial order.

The high-level invariants (i), (ii), and (iii) identified earlier naturally transcribe into the following invariants, which we impose on the typing judgments above. We use the notation \(\_\langle x_m \rangle ; P\) to denote a process term that currently executes an action along channel \(x_m\).

Invariants 1 and 2 ensure that, for any node in the tree, the acquired resources reside at smaller worlds than those acquired by any descendant. As a result, the two invariants guarantee high-level invariant (i). Invariant 3, on the other hand, imposes a lock-up strategy on acquires and thus guarantees high-level invariant (ii). To guarantee high-level invariant (iii), we impose Invariant 4, which forces a process to release any acquired resources before communicating along its offering channel. Since sibling nodes cannot be directly connected by a linear channel, the only way for them to synchronize is through a common parent. Finally, to guarantee that world annotations are internally consistent, we require for each annotation \([{\omega _k}\updownarrow ^{\omega _n}_{\omega _l}]\) that \(\omega _k < \omega _l \le \omega _n\).

Rules. We now present select process typing rules, a complete listing is provided in the companion technical report [4]. The only new rules with respect to the language \(\mathsf {SILL}_{\mathsf {S}}\) [2] are those pertaining to world creation and order determination. These are extra-logical judgmental rules. We allow both linear and shared processes to create and relate worlds. Rules and create a new world \(\mathsf {w}\) and make it available to the continuation \(Q_{\mathsf {w}}\). Rules and relate two existing worlds, while preserving acyclicity of the order.We now consider the typing rule for acquire, which must explicitly enforce the various low-level invariants above. Since an acquire results in the addition of a new child node to the executing process, the rule can interfere with Invariants 1 and 2. The first two premises of the rule ensure that the two invariants are preserved. Moreover, the rule has to ensure that the acquiring process is locking-up (Invariant 3), which is achieved by the third premise.The remaining shift rules are actually unchanged with respect to \(\mathsf {SILL}_{\mathsf {S}}\), modulo the world annotations. In particular, low-level Invariant 4 is already satisfied because the conclusion of rule does not have a context \(\varPhi \) and because the independence principle forces \(\varPhi \) to be empty in rule .We now consider the linear connectives, starting with \(\mathbf {1}\). Rule reveals that only processes that have never been acquired may be terminated. This restriction is important to guarantee progress because existing clients of a shared process may wait indefinitely otherwise. We impose the restriction as a well-formedness condition on a session type, giving rise to a strictly equi-synchronizing session type. The notion of an equi-synchronizing session type [2] has been defined for \(\mathsf {SILL}_{\mathsf {S}}\) and guarantees that a process that has been acquired at a type \(A_{\mathchoice{\mathsf {S}}{\mathsf {S}}{\scriptscriptstyle \mathsf {S}}{\scriptscriptstyle \mathsf {S}}}\) is released back to the type \(A_{\mathchoice{\mathsf {S}}{\mathsf {S}}{\scriptscriptstyle \mathsf {S}}{\scriptscriptstyle \mathsf {S}}}\), should it ever be released. A strictly equi-synchronizing session type additionally requires that an acquired resource must be released. The corresponding rules can be found in [4]. Linearity enforces Invariant 4 in rule , making sure that no linear channels are left behind.Next, we consider internal and external choice. Since internal and external choice cannot alter the linear process tree of a process graph, the rules are very similar to the ones in \(\mathsf {SILL}_{\mathsf {S}}\). The only differences are that we get two left rules for each connective and that the \(\varPhi \)-context of each right rule must be empty to satisfy Invariant 4. The former is merely due to the tracking of possibly aliased sessions in the \(\varPhi \) context. We only list rules for internal choice, those for external choice are dual and can be found in [4].More interesting are linear channel output and input, since these alter the linear process tree of a process graph. Moreover, additional world annotations are needed to indicate the worlds of the channel that is exchanged. For the latter we use the notation \(@{\omega _l}\updownarrow ^{\omega _r}_{\omega _p}\), indicating that the exchanged channel has the worlds \(\omega _l\), \(\omega _p\), and \(\omega _r\) for \(\mathsf {self}\), \(\mathsf {min}\), and \(\mathsf {max}\), respectively. To account for induced changes in the process graph, the rules that type an input of a linear channel must guard against any disturbance of Invariants 1 and 2. Because the two invariants guarantee that parents do not overlap with their descendants in terms of acquired resources, they prevent any exchange of acquired channels. We thus restrict \(\otimes \) and \(\multimap \) to the exchange of channels that have not yet been acquired. This is not a limitation since, as we will see below, shared channel output and input are unrestricted.

Even with the above restriction in place, we still have to make sure that a received channel satisfies Invariant 2. If we were to state a corresponding premise on the receiving rules, invertibility of the rules would be disturbed. To uphold invertibility, we impose a well-formedness condition on session types that ensures for a session of type \(A_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}@{\omega _l}\updownarrow ^{\omega _r}_{\omega _p} \otimes B_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}[{\omega _m}\updownarrow ^{\omega _v}_{\omega _u}]\) that \(\omega _v < \omega _p\) and, analogously, for a session of type \(A_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}@{\omega _l}\updownarrow ^{\omega _r}_{\omega _p} \multimap B_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}[{\omega _m}\updownarrow ^{\omega _v}_{\omega _u}]\) that \(\omega _v < \omega _p\). Session types are checked to be well-formed upon process definition. Given type well-formedness, we obtain the following rules for \(\multimap \), noting that the right rule enforces Invariant 4 by requiring an empty \(\varPhi \)-context. The rules for \(\otimes \) are dual.Since there are no invariants imposed on the shared context \(\varGamma \), the rules for shared channel output and input are identical to those in \(\mathsf {SILL}_{\mathsf {S}}\). The only differences are that we have two left rules and that the \(\varPhi \)-context of the right rule must be empty to satisfy Invariant 4. The former is merely due to the tracking of possibly aliased sessions in the \(\varPhi \) context.We finally consider the rules for forwarding and spawning. We allow a shared forward between processes that offer the same session at the same worlds. Because forwards have to be world-invariant, however, no well-typed program could ever have a linear forward. The process being forwarded to must be in either of the contexts \(\varPhi \) or \(\varDelta \), and thus satisfies Invariant 2, making it impossible for the world annotations of the forwarder and forwardee to match. We omit linear forwarding and discuss possible future extensions in Sect. 6.The rules for spawning depend on the possible modes of the spawning and spawned processes: specifies how a linear process can spawn another linear process; specifies how a shared processes can spawn another shared process. The rules are checked relative to a process definition found in the signature \(\varSigma \) and to a world substitution mapping \(\gamma : |\varPsi | \rightarrow |\varPsi '|\), such that for each \(\delta \in \varPsi '\) we have \(\varPsi \,\vdash \,\gamma (\delta )\), where \(|\varPsi |\) denotes the field of \(\varPsi \) (i.e., the union of its domain and range). As usual, we lift substitution to types \(\hat{\gamma }(A_m)\), contexts \(\hat{\gamma }(\varGamma )\), and orders \(\hat{\gamma }(\varPsi )\). Both rules ensure that, given the mapping \(\gamma \), the order \(\varPsi \) of the spawning process entails the one of the process definition (\(\varPsi \,\vdash \,\hat{\gamma }(\varPsi ')\)). The linear spawn rule further enforces Invariant 2 for the spawned child. We note that the spawned child enters the linear context \(\varDelta \) in the spawning process’ continuation since no aliases to such a process can exist at this point. In the companion technical report [4], we provide a variant of rule for the case of a linear recursive tail call. Without linear forwarding, a linear tail call can no longer be implicitly “de-sugared” into a spawn and a linear forward [2, 22, 52], but must be accounted for explicitly. In the report, we also provide the rules for checking process definitions. Those rules make sure that the process’ world order is acyclic, that the types of the providing session and argument sessions are well-formed, and that the process satisfies Invariants 1 and 2.

Having introduced our type system, we revisit the dining philosophers from Sect. 1 and show how to program the example in \(\mathsf {SILL}_{\mathsf {S}^+}\), ensuring that the program will run without deadlocks. The code is given in Fig. 4. We note the world annotations in the signature of the process definitions. For instance,

indicates that, given the order \(\delta _0< \delta _1< \delta _2 < \delta _3\), process \( thinking \) provides a session of type \(\mathsf {phil}[{\delta _0}\updownarrow ^{\delta _2}_{\delta _1}]\) and uses two shared channel references of type \(\mathsf {sfork}[{\delta _1}\updownarrow ^{\delta _3}_{\delta _3}]\) and \(\mathsf {sfork}[{\delta _2}\updownarrow ^{\delta _3}_{\delta _3}]\). The two \(\cdot \) signify that neither acquired nor linear channel references are given as arguments. The signature indicates that the two shared fork references reside at different worlds, such that the world of the first one is smaller than the one of the second.

Let’s briefly convince ourselves that the two acquires in process \( thinking \) in Fig. 4 are type-correct. For each acquire we have to show that: the world of the resource to be acquired is within the acquiring process’ range; the \(\mathsf {max}\) of the acquiring process is smaller than the \(\mathsf {min}\) of the acquired resource; and, that the \(\mathsf {self}\) of the acquired resource is larger than those of all already acquired resources. We can convince ourselves that all those conditions are readily met. We note, however, that if we were to swap the two acquires, the program would not type-check.

Let us once more set the table for three philosophers and three forks. We execute this code in a process with world annotations \([{\delta _a}\updownarrow ^{\delta _b}_{\delta _b}]\) such that \(\delta _a < \delta _b\). We first create new worlds and define their order:

We then spawn the forks, each residing at a different world, such that the \(\mathsf {max}\) world of a fork is higher than the \(\mathsf {self}\) of the highest fork, ensuring Invariant 2 for the philosopher processes that we spawn afterwards:

When we spawn the philosophers, we ensure that \(P_0\) is going to pick up fork \(F_1\) and then \(F_2\), \(P_1\) is going to pick up \(F_2\) and then \(F_3\), and \(P_2\) is going to pick up \(F_1\) and then \(F_3\).

We note that the deadlocking spawn

is type-incorrect since we would substitute both \(\mathsf {w_1}\) and \(\mathsf {w_3}\) for \(\delta _1\) and \(\mathsf {w_3}\) and \(\mathsf {w_1}\) for \(\delta _2\), which violates the ordering constraints put in place by typing.

We now give the dynamics of \(\mathsf {SILL}_{\mathsf {S}^+}\). Our current system is based on a synchronous dynamics. While this choice is more conservative, it allows us to narrow the complexity of the problem at hand.

As in \(\mathsf {SILL}_{\mathsf {S}}\), we use multiset rewriting rules [12] to capture the dynamics of \(\mathsf {SILL}_{\mathsf {S}^+}\) (see Sect. 2). Multiset rewriting rules represent computation in terms of local state transitions between configurations of processes, only mentioning the parts of a configuration they rewrite. We use the predicates \(\mathsf {proc}( a_m , \, \mathsf {{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}}, \, P_{a_m} )\) and \(\mathsf {unavail}( a_{\mathchoice{\mathsf {S}}{\mathsf {S}}{\scriptscriptstyle \mathsf {S}}{\scriptscriptstyle \mathsf {S}}} , \, \mathsf {{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}})\) to define the states of a configuration (see Sect. 5.1). The former denotes a process executing term P that provides along channel \(a_m\) at mode m with worlds \(\mathsf {w_{a_1}}\), \(\mathsf {w_{a_2}}\), and \(\mathsf {w_{a_3}}\) for \(\mathsf {self}\), \(\mathsf {min}\), and \(\mathsf {max}\), respectively. The latter acts as a placeholder for a shared process providing along channel \(a_{\mathchoice{\mathsf {S}}{\mathsf {S}}{\scriptscriptstyle \mathsf {S}}{\scriptscriptstyle \mathsf {S}}}\) with worlds \(\mathsf {w_{a_1}}\), \(\mathsf {w_{a_2}}\), and \(\mathsf {w_{a_3}}\) for \(\mathsf {self}\), \(\mathsf {min}\), and \(\mathsf {max}\), respectively, that is currently unavailable. We note that since worlds are also run-time artifacts, they must occur as part of the state-defining predicates.

Fig. 5 lists selected rules of the dynamics. Since the rules remain largely the same as those of \(\mathsf {SILL}_{\mathsf {S}}\), apart from the world annotations that are “threaded through” unchanged, we only discuss the rules that actually differ from the \(\mathsf {SILL}_{\mathsf {S}}\) rules. The interested reader can find the remaining rules in the companion technical report [4].

Noteworthy are the rules and for creating and relating worlds, respectively. Rule creates a fresh world, which will be globally available in the configuration. Rule , on the other hand, updates the configuration’s order with the pair \(\mathsf {w} < \mathsf {w}'\). Rule , lastly, substitutes actual worlds for world variables in the body of the spawned process, using the substitution mapping \(\gamma \) defined earlier. It relies on the existence of a corresponding definition predicate for each process definition contained in the signature \(\varSigma \). We note that the substitution \(\gamma \) in rule instantiates the appropriate world variables in the spawned process P.

Given the hierarchy between mode \(\mathsf {S}\) and \(\mathsf {L}\) and the fact that shared processes cannot depend on linear processes, we divide a configuration into a shared part \(\varLambda \) and a linear part \(\varTheta \). We use the typing judgment \(\varPsi ; \varGamma \vDash \varLambda ; \varTheta \; {:}\,\!{:} \; \varGamma ; \varPhi , \varDelta \) to type configurations. The judgment expresses that a well-formed configuration \(\varLambda ; \varTheta \) provides the shared channels in \(\varGamma \) and the linear channels in \(\varPhi \) and \(\varDelta \). A configuration is type-checked relative to all shared channel references and a global order \(\varPsi \). While type-checking is compositional insofar as each process definition can be type-checked separately, solely relying on the process’ local \(\varPsi \) (and \(\varGamma \)), at run-time, the entire order that a configuration relies upon is considered. We give the configuration typing rules in Fig. 10.

Our progress theorem crucially depends on the guarantee that the Invariants 1 and 2 from Sect. 3 hold for every linear process in a configuration’s tree. This is expressed by the premises and in rule , based on the Definitions 1 and 2 below that restate Invariants 1 and 2 for an entire configuration. We note that Invariant 2 is based on the set of all transitive children (i.e., descendants) of a process. We formally define the notion of a descendant inductively over a well-typed linear configuration. The interested reader can find the definition in the companion technical report [4].

Our preservation theorem states that Invariants 1 and 2 are preserved for every linear process in the configuration along transitions. Moreover, the theorem expresses that the types of the providing linear channels \(\varPhi \) and \(\varDelta \) are maintained along transitions and that new shared channels and worlds may be allocated. The proof relies, in particular, on session types being strictly equi-synchronizing, on a process’ type well-formedness and assurance that the process’ \(\mathsf {min}\) world is less than or equal to its \(\mathsf {max}\) world.

In our development so far we have distilled the two scenarios of interdependencies between processes that can lead to deadlocks: cyclic acquisitions and interdependent acquisitions and synchronizations. This has lead to the development of a type system that ingrains the notions of competitors and collaborators, such that the former compete for a set of resources whereas the latter do not overlap in the set of resources they acquire. Our type system then ties these notions to a configuration’s linear process tree such that collaborators stand in a parent-descendant relationship to each other and competitors in a sibling/cousin relationship. In this section, we prove that this orchestration is sufficient to rule out any of the aforementioned interdependencies.

To this end we introduce the notions of red and green arrows that allow us to reason about process interdependencies in a configuration’s tree. A red arrow points from a linear \(\mathsf {proc}( a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}} , \, \mathsf {{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}}, \, Q )\) to a linear \(\mathsf {proc}( b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}} , \, \mathsf {{\mathsf {w_{b_1}}}\updownarrow ^{\mathsf {w_{b_3}}}_{\mathsf {w_{b_2}}}}, \, P )\), if the former is attempting to acquire a resource held by the latter and, consequently, is waiting for the latter to release that resource. A green arrow points from a linear \(\mathsf {proc}( a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}} , \, \mathsf {{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}}, \, Q )\) to a linear \(\mathsf {proc}( b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}} , \, \mathsf {{\mathsf {w_{b_1}}}\updownarrow ^{\mathsf {w_{b_3}}}_{\mathsf {w_{b_2}}}}, \, P )\), if the former is waiting to synchronize with the latter. We define these arrows formally as follows:

It may be helpful to consult Fig. 3 at this point and note the semantic difference between the violet arrows in that figure and the red arrows discussed here. Whereas violet arrows point from the acquiring process to the resource being acquired, red arrows point from the acquiring process to the process that is holding the resource. Thus, violet arrows can go out of the tree, while red arrows stay within. Given the definitions of red and green arrows, we can define the relation \(\mathcal {W}(\varTheta )\) on the configuration’s tree, which contains all process pairs that are in some way waiting for each other:

Having defined the relation \(\mathcal {W}(\varTheta )\), we can now state the key lemma underlying our progress theorem, indicating that \(\mathcal {W}(\varTheta )\) is acyclic in a well-formed and well-typed configuration.

We focus on explaining the main idea of the proof here. The proof proceeds by induction on \(\varPsi ; \varGamma \vDash \varTheta \; {:}\,\!{:} \; \varPhi , \varDelta \), assuming for the non-empty case \(\varPsi ; \varGamma \vDash \varTheta , \mathsf {proc}( a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}} , \, \mathsf {{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}}, \, P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}} ) \; {:}\,\!{:} \; (\varPhi , \varDelta , a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}: A_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}[{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}])\) that \(\mathcal {W}(\varTheta )\) is acyclic, by the inductive hypothesis. We then know that there cannot exist any paths of green and red arrows in \(\varTheta \) that form a cycle, and we have to show that there is no way of introducing such a cyclic path by adding node \(\mathsf {proc}( a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}} , \, \mathsf {{\mathsf {w_{a_1}}}\updownarrow ^{\mathsf {w_{a_3}}}_{\mathsf {w_{a_2}}}}, \, P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}} )\) to the configuration \(\varTheta \). In particular, the proof considers all possible new arrows that may be introduced by adding the node and that are necessary for creating a cycle, showing that such arrows cannot come about in a well-typed configuration.

We illustrate the reasoning for the two selected cases shown in Fig. 11. Case (a) represents a case in which process \(P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) is waiting to synchronize with its child \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) while holding a resource a descendant of \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) or \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) itself wants to acquire. However, this scenario cannot come about in a well-typed configuration because \(P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) and \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) are collaborators and thus cannot overlap in resources they acquire. Case (b) represents a case in which process \(P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) is waiting to synchronize with its child \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) while another child, process \(P_{c_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\), is waiting to synchronize with \(P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\). Given acyclicity of \(\mathcal {W}(\varTheta )\), a necessary condition for a cycle to form is that there already must exist a red arrow \(\mathbf C \) in the configuration that connects the subtrees in which the siblings \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) and \(P_{c_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) reside. However, this scenario cannot come about in a well-typed configuration because \(P_{b_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) and \(P_{c_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) are competitors, forcing \(P_{c_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\) or any of its descendant to release a resource before synchronizing with \(P_{a_{\mathchoice{\mathsf {L}}{\mathsf {L}}{\scriptscriptstyle \mathsf {L}}{\scriptscriptstyle \mathsf {L}}}}\). These arguments are made precise in various lemmas in [4].

Given acyclicity of \(\mathcal {W}(\varTheta )\), we can state and prove the following strong progress theorem. The theorem relies on the notion of a poised process, a process currently executing an action along its offering channel, and distinguishes a configuration only consisting of the top-level, linear “main” process from one that consists of several linear processes. We use \(|\varTheta |\) to denote the cardinality of \(\varTheta \):

The theorem indicates that, as long as there exist at least two linear processes in the configuration, the configuration can always step. If the configuration only consists of the main process, then this process will become poised (i.e., ready to close), once all sub-computations are finished. The proof of the theorem relies on the acyclicity of \(\mathcal {W}(\varTheta )\) and the fact that all sessions must be strictly equi-synchronizing.