Das Kapitel stellt einen bahnbrechenden Ansatz zur Verwaltung von Mehrparteiensitzungen in verteilten Systemen durch den Einsatz isorekursiver Mehrparteiensitzungstypen vor. Im Gegensatz zu herkömmlichen equi-rekursiven Methoden, die ineffizient und schwer umzusetzen sein können, bieten die vorgeschlagenen iso-rekursiven Methoden eine praktikablere und überprüfbarere Lösung. Der Text beginnt mit der Diskussion der Beschränkungen aktueller Theorien über Sitzungstypen, insbesondere ihrer Abhängigkeit von equi-rekursiven Typen, die für nicht faule Programmiersprachen nicht gut geeignet sind. Dann wird ein neuartiges System eingeführt, das die Freiheit von Blockaden kompositorisch berechnet und sicherstellt, dass diese Umgebungen frei von Kommunikationsfehlern und Blockaden sind. Das Kapitel enthält eine detaillierte Erläuterung der Syntax und Semantik von Mehrparteiensitzungen sowie ein formales System zur Typprüfung. Es bietet auch eine Implementierung in OCaml, die mittels automatisierter deduktiver Tools verifiziert wurde, und enthält Beispiele wie eine rekursive Variante des OAuth 2.0-Protokolls. Das Kapitel schließt mit einer Diskussion über die diesbezügliche Arbeit und die zukünftige Richtung, wobei das Potenzial für weitere Fortschritte in diesem Bereich hervorgehoben wird. Diese umfassende Untersuchung isorekursiver Sitzungstypen bietet Forschern und Praktikern im Bereich verteilter Systeme und formaler Verifikation wertvolle Erkenntnisse und praktische Werkzeuge.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Most works on session types take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. This becomes more important in recent type systems which do not require global types, also known as generalised multiparty session types (GMST). In GMST, in order to establish properties as deadlock-freedom, the environments which type processes are assumed to satisfy extensional properties holding in all infinite sequences. This is a problem because: (1) the mechanisation of GMST and equi-recursion in proof assistants is utterly complex and eventually requires co-induction; and (2) the implementation of GMST in type checkers relies on model checkers for environment verification, and thus the program analysis is not self-contained.
In this paper, we overcome these limitations by providing an iso-recursive typing system that computes the behavioural properties of environments. The type system relies on a terminating function named compliance that computes all final redexes of an environment, and determines when these redexes do not contain mismatches or deadlocks: compliant environments cannot go wrong. The function is defined theoretically by introducing the novel notions of deterministic LTS of environments and of environment closure, and can be implemented in mainstream programming languages and compilers. We showcase an implementation in OCaml by using exception handling to tackle the inherent non-determinism of synchronisation of branching and selection types. We assess that the implementation provides the desired properties, namely absence of mismatches and of deadlocks in environments, by resorting to automated deductive verification performed in tools of the OCaml ecosystem relying on Why3.
1 Introduction
Session types [32, 33, 51] are an effective method to control the behaviour of software components that run in message-passing distributed systems. Multiparty session types (MPST) [34, 35] enhance session types by providing support for sessions involving multiple participants, thus representing more expressive scenarios. Various theories of MPST have been deployed in programming languages [55] allowing verification of industrial code at compile or run-time [21].
In most works on session types, recursive types follow an equi-recursive view [47] and represent infinite trees that are manipulated co-inductively. This representation does not have a direct counterpart in non-lazy programming languages, which typically resort to iso-recursive types [1, 47] that are manipulated inductively. Moreover, lazy evaluation of predicates on equi-recursive trees might not terminate, and is thus not effective for static program analysis. In practice, MPST are embedded in non-lazy languages by encoding equi-recursive types; for instance, [37] defines infinite sequence of types as polymorphic lenses [20] by using OCaml generalised algebraic data types.
Anzeige
Our proposal to overcome this problem consists in introducing a theory of iso-recursive multiparty session types relying on a type system that computes the deadlock-freedom of type environments.
Lately, there have been several advances in MPST that can establish deadlock-freedom without using global types, e.g. [5, 7, 24, 30, 38, 46, 49, 50]: this bottom-up approach is known as generalised multiparty session types (GMST). However, the price to pay in GMST is that environments must satisfy extensional predicates requiring that a certain property holds for all infinite sequences. This is a non-integrated feature in GMST, which resort to external tools as model checkers to assess these predicates. Moreover, mechanising equi-recursive GMST in proof assistants is quite complex, and eventually relies on co-induction [17]. Specifically, formulations based on GMST are difficult to implement in programming languages because of the interplay among equi-recursive types and the verification of the semantic properties of environments. Another possibility is to proceed top-down by using global types and ensure deadlock freedom without verifying environments, while the analysis’ expressiveness is affected by projectability [52].
In this paper, we propose a formal system to compute the deadlock-freedom of type environments compositionally at the typing of parallel processes, and we provide an implementation that is automatically verified by using automated deductive tools of the OCaml ecosystem [9, 44, 45] relying on Why3 [19].
1.1 Equi-recursive vs Iso-recursive Types: SSH/OAuth2 Example
We illustrate our methodology using a recursive variant of the OAuth 2.0 protocol (cf. [49]) which provides support for ssh [10]. Let us indicate send to and receive from participant
as the types
and
, respectively, where l is a label indicating the nature of the communication, S is the sort of the payload, and T is the type of the continuation. Selection among (branching on) different output (input) types is done by means of the binary operator \(+\). Recursion is provided by the construct \(\mu X.T\), which binds the type variable X in T. Termination is represented by type \({\textsf{end}} \). Sorts describe the types of string, boolean, and unit values. The session types of the service (
), of the client (
), and of the authorisation server (
) are:
The protocol says that the service (
) sends to the client (
) either a request to login, or cancel; in the first case,
continues by sending the password (pwd, carrying a string), or by sending ssh, to
, who in turn sends authentication to
(auth, with a boolean, telling whether the client is authorised), and the session restarts; in the second case,
sends quit to
, and the session ends.
Anzeige
A problem of equi-recursive GMST, e.g. [49], is that types are defined co-inductively (cf. [17]). Recursive types can be infinitely folded and unfolded: for instance, we have the following equi-recursive equations:
This is particularly relevant when establishing the properties of the typing system, e.g. safety [49, Definition 4.1], which are based on a notion of transition of session environments. To illustrate, the idea is to interpret types as processes, cf. [41], and consider transitions of session environments mapping participants
to types T. The environment
can fire an output action
and reach
, or can fire an output action
and reach
. The environment
can fire an input action
and reach
, where
, or can fire an input action
and reach
. The environment \(\varGamma _1,\varGamma _2\) can fire two synchronisation actions: (1)
, which indicates a synchronisation on the label login by the input participant
and the output participant
, and reach the environment
; and (2)
, and reach the environment
.
In particular, the rule for recursive types in [49, Definition 2.8] states that a recursive type \(\mu X.T\) inherits the transitions from its unfolding, that is the type \(T\{\mu X.T/X\}\). For instance, the rule can be instantiated with type
as
and allows for inferring the following transitions:
We note that this elegant approach is appropriate for the theory, but less suited for mechanising GMST in theorem provers, and for automated verification.
More specifically, the approach introduced in [49] and followed in many subsequent papers on GMST, e.g. [5, 7, 24, 30, 38, 46, 49], requires to type check sessions with environments having certain extensional properties. Crucially, such properties must be established before typing by analysing all possible infinite transitions of session environments. To illustrate, the paper [49] provides a companion artefact by using mCRL2 [29] featuring \(\mu \)-calculus formulae that represent the safety and deadlock freedom properties of environments [49, Figure 5], which are defined by least and greatest fixed points.
Our solution.In this paper, we compute the semantic properties of the session environment in the rule for type checking the session composition, hence achieving decidable type checking. This is possible because our types are iso-recursive and have a finite structure.
In our setting, the types
, and
are all different, but isomorphic. A recursive type \(\mu X.T\) can only be used to type-check a recursive process, or a type variable. To type check an input or output process, we need to unfold \(\mu X.T\) by applying the substitution \(\mu X.T /X\) to type T, denoted as \(T\{\mu X.T /X\}\). That is, we have the following iso-recursive equations:
For instance, consider the authorisation process
below, whose syntax mirrors the one of its type
, but that the payload of input and output are (bound) variables and expressions, respectively, and that there is a process variable \(\chi \):
In order to type check the recursive process
we use the typing judgement:
Now consider the process obtained by substituting \(\chi \) in
with
, that is process
, and the parallel execution of
with
and
, where
are recursive processes implementing the service
typed by
, and the client
typed by
, respectively. This session should be accepted by the type system, since at runtime it behaves correctly, independently of the fact that the authorisation service
has been “unrolled” once.
That is, we want to infer the following judgement by using the rule for session composition of the typing system for sessions, denoted \(\Vdash \):
The predicate \({\textsf{comp}} (\varDelta )\) establishes compliance by using the computable function\({\textsf{comp}} \). The goal is to calculate all possible final environments that are reachable from \(\varDelta \), and verify that they are not errors. Intuitively, an environment is final when is stuck, or when it has already been encountered, reaching a fixed point.
Since we are interested in mechanising compliance, the calculation should be achieved by relying on the novel notion of deterministic transition, denoted \(\rightarrow _d\), such that \(\varDelta \overset{{\alpha _1}}{\rightarrow _d} \varDelta _1\) and \(\varDelta \overset{\alpha _2}{\rightarrow _d}\ \varDelta _2\) imply \(\alpha _1=\alpha _2\) and \(\varDelta _1=\varDelta _2\). The key point is that a deterministic transition system can be encoded as a computable function that can be deployed in type checkers and compilers. Moreover, the properties of the function can be verified with automated deductive verification tools as Why3 [19]. In particular, we propose the idea of closure of an environment\(\varDelta \): the function receives \(\varDelta \) in input and returns in output a finite set of final environments reachable from \(\varDelta \) by multiple applications of \(\rightarrow _d\).
The compliance function decides when in all final environments reached by transitions starting from \(\varDelta \), there is not a communication mismatch or a deadlock. A communication mismatch arises when a participant
has a single I/O type receiving from/sending to participant
, and
has a single I/O type receiving from/sending to participant
, and one of the following cases arise: (i) both
and
are sending or receiving; (ii) the intersection among the labels used by
and
is empty; (iii)
and
agree on a label but disagree on the label’s sort. A deadlock arises when the environment \(\varDelta \) cannot fire any transition and there is at least a participant
s.t.
.
To see an example of environment rejected by the compliance function comp, consider \(\varDelta ''\) below. An authorisation server typed by
only allows two subsequent attempts for ssh authentication: after that, it ends. Conversely, a client typed by
performs an infinite number of requests of ssh authentication: for this very reason, a system typed by \(\varDelta ''\) can deadlock and must be rejected.
The closure of \(\varDelta ''\) does return a set of environments containing the deadlocked environment \(\varDelta _{\texttt {lock}}\), which depicts the scenario discussed above. Since \(\varDelta _{\texttt {lock}}\in {\textsf{closure}} (\varDelta '')\) and \(\varDelta _{\texttt {lock}}\) is a deadlock, we have \(\lnot \,{\textsf{comp}} (\varDelta '')\):
Outline§2 introduces the syntax and semantics of multiparty sessions. §3 presents the non-deterministic labelled transition semantics of session environments (cf. §3.1), and its deterministic counterpart (cf. §3.2): the former is used to define deadlocks and to prove subject reduction; the latter is used in §3.3 to define closure and in turn to mechanise compliance. §4 introduces the typing system. We first analyse the typing rules for processes. Second, we analyse the rule for typing sessions, which relies on a computable function calculating compliance that is defined in §4.1. Last, in §4.2 we provide the proof of subject reduction and we state a progress result. §5 is devoted to the automated deductive verification of compliance. We start in §5.1 by outlining few details of the implementation of compliance and of closure of deterministic transitions in OCaml. §5.2 verifies the behavioural specification of the implementation in automated deductive verification tools of the OCaml ecosystem relying on Why3. §6 concludes by presenting related work and next directions. The full proofs and omitted definitions can be found in [27] and the accompanying artefact can be found at https://doi.org/10.5281/zenodo.14621028.
2 Multiparty Sessions
The syntax of types and processes is in Definition 1. We consider iso-recursive types of the form \(\mu X.T\) where \(\mu X.T\) and its unfolding are not equal, but isomorphic. We stress that types have a finite representation rather than abstract infinite trees (cf. equi-recursive types).
Definition 1
(Syntax of types and processes).
We require all terms to be contractive, i.e. \(\mu X_1.\mu X_2. \dots \mu X_n.X_1\) is not allowed as a sub-term for any \(n\ge 1\) [47, p. 300], which can be alternatively stated as type variables occur guarded (by input or output prefixes) [14].1
We use
to range over participants, l to range over labels, and i, j to range over indexes (natural numbers). X, Y range over type variables, \(e, e'\) range over expressions, v, w range over values, x, y range over variables, and \(\chi \) range over process variables. Sessions\(\mathcal M\) belong to the set \(\mathbb M\). A single session or thread is a process P indexed by a participant, denoted
. A multiparty session is a composition of all threads, denoted
or
.
The constructor \(\mu \) is a binder in types and processes, respectively: we let X be bound in \(\mu X.T\) and free in T; similarly, \(\chi \) is bound in \(\mu \chi .P\) and free in P. The remaining binder for processes is input: variable x is bound in
and free in P. Closed terms are those without free variables.
We assume the substitution of free occurrences of a type variable X in a type \(T_1\) with a closed type \(T_2\), written \(T_1\{T_2/X\}\). We assume the substitution of free occurrences of a process variable \(\chi \) in process \(P_1\) with a closed process \(P_2\), written \(P_1\{P_2/\chi \}\), and the substitution of free occurrences of variable x in process P with a value v, written \(P\{v/x\}\). A type R is \(\mu \)-guarded (guarded, for short) if it is a sub-term of T in the definition \(\mu X.T\).
The symbol \(=\) is reserved for Leibniz equality.
Definition 2
(Session notation).
The next step towards the definition of the typing system is to identify well-formed types that correctly abstract multiparty sessions. The definition is in the technical report [27]. We collect the labels of types in multi-sets, and the polarities and the participants of types in sets. Intuitively, a sum type \(T_1 + T_2\) is well-behaved when it has not duplicated labels, \(T_1\) and \(T_2\) have the same unique polarity, and the same unique participant. These assumptions eliminate ill-types of the form e.g.
or of the form e.g.
with
, as well as mixed choice types, e.g.
. A type T is well-formed, denoted \(\text {WF}(T)\), when it is well-behaved, contractive, and closed.
Operational semantics of multiparty sessions. We assume an evaluation function \(\downarrow \) transforming expressions e into boolean, integer and unit values v, written \(e\downarrow v\). The operational semantics of multiparty sessions are defined modulo a structural congruence relation over sessions \(\mathcal M\), denoted
. We let
be the least reflexive relation that satisfies the axiom
The labelled transition rules are defined in Figure 1; we just present the left rules. A computation is a sequence of \(\alpha \)-transitions,
, or reductions\(\mathcal{M}_1\overset{\alpha }{\rightarrow }\mathcal{M}_2\overset{\alpha }{\rightarrow }\cdots \). We are mainly interested in analysing computations of well-typed sessions (cf. § 4).
Fig. 1.
Labelled transition rules for multiparty sessions (we omit R-IfF)
Rule R-Inp says that a participant
waiting for a value from
on the label l can do a transition labelled by
and instantiate the formal parameter x with the value v in the continuation P, noted as \(P\{v/x\}\). Rule R-Out allows a participant
sending to
on label l an expression e that can be evaluated as v to do a transition labelled by
and continue as P. Non-deterministic reductions are allowed by means of rule R-Sum-L, which says that a participant
non-deterministically choosing among process P and Q, denoted \(P + Q\), can do a transition labelled by \(\alpha \) and reach
whenever
can fire the same transition and reach the same redex.
Communication among two participants
and
is performed by means of rule R-Com. Whenever
can do a transition labelled by the input action
and reach the redex
, and
can do a transition labelled by the output action
and reach the redex
, we can infer a transition labelled with
from the composition of
and
and a session
to the composition of
and
and
. Rule R-Rec allows a participant
recursively defined as \(\mu \chi .P\) and running in parallel with a session
, to do an internal transition \(\tau \) and unfold the body P while instantiating the occurrences of \(\chi \) in P with \(\mu \chi .P\), thus reaching the redex
. Rule R-IfT (R-IfF) says that a participant
with the body \({\textsf{if}} \; e \; {\textsf{then}} \; P\; {\textsf{else}} \; Q\) and running in parallel with a session
, can do a \(\tau \)-transition and reach the redex
(
) whenever the expression e evaluates to true (false). Rule R-Str rearranges processes with structural congruence.
Example 1
Consider the authorisation protocol in § 1.1 and
where process
implements the (unfolding of the) authorisation server
, and processes
and
implement the service
and the client
, respectively. We analyse transitions of the session introduced in § 1.1 and composing the service
, the client
, and the server
, here referred as \(\mathcal M\).
We want to analyse a communication of the server
with the client
depicting a login transaction. A first application of rule R-Rec unfolds the service
:
where
.
The next step consists in unfolding the client
. Since the client thread does not occur in the left, we need to first apply R-Rec and then apply structural congruence in rule R-Str:
where
. Now we apply rule R-Com to infer a communication among the service
and the client
on the label login, followed by R-Str:
where
, and
As you can see, in session \(\mathcal{M}_3\) the client
is ready to communicate the password, or to send a ssh request, to the authorisation server
. \(\square \)
3 Session Environment Reduction, Algorithmically
A central notion of multiparty session types is the interaction among parties. We model this abstraction by depicting the behaviour of session environments\(\varDelta \) assigning types T to participants
.
Our aim is to define a function that decides at compile-time when it is safe to type-check a group of participants running in parallel and willing to communicate with each other. This is reminiscent of the notion of type duality in binary session types (e.g. [22, 26]), but encompasses multiple participants. We will use the function in the typing system introduced in § 4.
Definition 3
(Labelled transition system). A labelled transition system (LTS) is a tuple \((\tilde{A}, \mathcal{S}_1,\mathcal{A}, \mathcal{S}_2,\rightarrow )\), noted as \(\tilde{A}\triangleright \sigma _1\overset{\alpha }{\rightarrow }\ \sigma _2\), whenever \(\sigma _1\in \mathcal{S}_1\) and \(\sigma _2\in \mathcal{S}_2\) and \(\alpha \in \mathcal A\), where \(\tilde{A}\) is a (possibly empty) tuple of parameters, \(\mathcal{S}_i\) are set of states, \(i=1,2\), \(\mathcal A\) is a set of actions, and \(\rightarrow \) is a transition relation s.t. \(\rightarrow \subseteq \tilde{A}\times \mathcal{S}_1\times \mathcal{A}\times \mathcal{S}_2\). A transition relation \(\rightarrow \) is a partial function whenever \(\tilde{A}\triangleright \sigma _1\overset{\alpha '}{\rightarrow }\ \sigma '_2\) and \(\tilde{A}\triangleright \sigma _1\overset{\alpha ''}{\rightarrow }\ \sigma ''_2\) imply \(\alpha '=\alpha ''\) and \(\sigma '_2=\sigma ''_2\). A LTS is deterministic whenever its transition relation is a partial function.
3.1 Non-deterministic Transition System
We first define a non-deterministic LTS of session environments, and then in § 3.2 we outline its transformation to a deterministic LTS. Non-deterministic transitions are used in the notion of deadlock (cf. Definition 10), and in the proof of subject reduction (cf. § 4.2). In the non-deterministic setting, the parameters \(\widetilde{A}\) are empty and \(\mathcal{S}_1=\mathcal{S}_2\).
We start by defining a non-deterministic LTS of types. Since we will also use the transition system to match the actions of processes, it is practical to use the same labels of the LTS of Figure 1. The left rules for types are in Figure 2. The rules are designed for well-formed types (cf. § 2), as we discuss below (cf. rules E-Sel-L, fitsE-Bra-L). Rule E-Out says that a type doing an output to the participant
on label l with payload S and continuing as T can fire the action
and reach the redex T whenever v is a value of sort S. Dually, rule E-In allows an input type from
on label l with payload S and continuing as T to do an action
and reach the redex T, if v has sort S. Rule E-Sel-L allows a sum type \(T_1 + T_2\) to do an output action
and reach the redex \(T'\) whenever \(T_1\) can fire this action and reach \(T'\). Dually, rule E-Bra-L allows a sum type \(T_1 + T_2\) to do an input action
and reach the redex \(T'\) if \(T_1\) can fire this action and reach \(T'\). Note that input and output are the only actions that a sum type can fire. This is because types as e.g. \(T_1 + \mu X.T\) or \(T_1 + (\mu X.T + T_2)\) are not well-formed.
Fig. 2.
Labelled transition system of session environments
The non-deterministic transition rules for session environments follow in Figure 2, and are the counterpart of the non-deterministic rules of the form \(\varGamma \overset{\alpha }{\rightarrow }\varGamma \) used in GMST (cf. [49]) to analyse the safety and deadlock freedom of multiparty protocols. We consider a top-level rule of the form \( D\diamond \varDelta \overset{\alpha }{\rightarrow }\ D\diamond \varDelta \), where we refer to \(D\diamond \varDelta \) as a configuration, and use C to range over it. D is a set of type environments representing a decreasing set which is a subset of a fixed point: a step can be taken only if \(\varDelta \) is in the decreasing set D. The idea is the following: since we are interested in computing all possible redexes of session environments, we avoid to further analyse the same environment twice by removing the visited environments from the (possibly infinite) set of all possible environments.
Rule Se-Top applies to configurations and checks that an environment \(\varDelta \) is in the decreasing set D, and \(\varDelta \) can move to \(\varDelta '\) with label \(\alpha \): in such case the configuration \(D\diamond \varDelta \) moves to the configuration \(D\backslash _{\varDelta }\diamond \varDelta '\), where \(D\backslash _{\varDelta }\) notes the decreasing set D less the environment \(\varDelta \).
Rule Se-Rec applies to session environments and says that
can do an internal action \(\tau \) and reach the environment
, thus unfolding the type of the participant
. Rule Se-Com applies to session environments and depicts a communication: when a participant
has a type
that can fire an input action
and move to
, and a participant
has a type
that can fire an output action
and move to
, then
can fire a synchronisation action
and move to
.
Example 2
Consider the protocol introduced in § 1.1 and take
,
. Consider a fixed point D such that \(\varDelta \in D\). A first application of E-Rec, Se-Rec, Se-Top allows for unfolding the type of the service
, where we let
:
To continue and unfold the type of the client
, we need to verify that \(\varDelta _1\in D\backslash _{\varDelta }\): this follows indeed from the property of a fixed point, that is to be closed under transition, and from the fact \(\varDelta _1\ne \varDelta \), which holds because types are iso-recursive, and in turn
. We proceed as above and infer the following transition, where
:
Two non-deterministic transitions are available from \(\varDelta _2\), and involve the synchronisation of
and
: one over the label login and the other over the label cancel. The interaction below corresponds to the label login and is obtained by applying E-Out, E-Sel-L, E-In, E-Bra-L, Se-Com, Se-Top, where
and \(D_2\;{\mathop {=}\limits ^{\text {def}}}\;D\backslash _{\varDelta ,\varDelta _1}\) and \(D_3\;{\mathop {=}\limits ^{\text {def}}}\;D_2\backslash _{\varDelta _2}\):
The interaction over the label cancel is obtained by applying E-Out, E-Sel-R, E-In, E-Bra-R, Se-Com, Se-Top, where E-Sel-R and E-Bra-R are the right rules of E-Sel-L and E-Bra-L, respectively:
We conclude by noting that the transition system \(D\diamond \varDelta \overset{\alpha }{\rightarrow }\ D\diamond \varDelta \) is indeed non-deterministic (Definition 3) by
and \(\varDelta _3\ne \varDelta '_3\). \(\square \)
3.2 Deterministic Session Environment Transitions
In this section, we define a deterministic LTS for environments that is the basis for the definition of closure in § 3.3, and in turn for the mechanisation of compliance (cf. § 4.1) in deductive tools of the OCaml ecosystem (cf. § 5).
The transition system \(D\diamond \varDelta \overset{\alpha }{\rightarrow }\ D'\diamond \varDelta '\) is non-deterministic, for two reasons: (1) threads can reduce or interact in any order; (2) label synchronisation among two participants can occur on multiple labels and in any order.
To make the LTS deterministic (cf. Definition 3), we need four ingredients:
(i) To partition the environment into minimal environments, and invoke the LTS on each minimal environment; (ii) To collect information about discarded branches and selections in synchronisations; (iii) To pass an oracle \(\varOmega \) that given an environment \(\varDelta \) returns the next two engaging participants, or the next participant firing a \(\tau \) action, or nothing; (iv) To define a scheduling policy for labels of communicating participants.
We discuss (i) and (iii), and provide the signature of the deterministic LTS. Feature (i) relies on following definition; see [27] forall details.
Let
, \({\textsf{parties}} (\mu X.T)\;{\mathop {=}\limits ^{\text {def}}}\;{\textsf{parties}} (T)\), \({\textsf{parties}} (T_1+T_2)\;{\mathop {=}\limits ^{\text {def}}}\;{\textsf{parties}} (T_1)\cup {\textsf{parties}} (T_2)\), and \({\textsf{parties}} (T)\;{\mathop {=}\limits ^{\text {def}}}\;\emptyset \) otherwise. Let \({\textsf{parties}} (\emptyset )\;{\mathop {=}\limits ^{\text {def}}}\;\emptyset \),
. Let \(\varDelta \backslash _{\textsf{End}}\) project all non-ended participants of \(\varDelta \).
Definition 4
(Minimal partition and environments). A set \(\{\varDelta _1,\dots ,\varDelta _n\}\ne \emptyset \) is a partition of \(\varDelta _1\cup \cdots \cup \varDelta _n\) whenever \(\varDelta _i\ne \emptyset \) and \({\textsf{parties}} (\varDelta _i)\cap {\textsf{parties}} (\varDelta _j)=\emptyset \) for all \(\{i,j\}\subseteq \{1,\dots , n\}\), \(i\ne j\). Let \(\mathcal{P}_\mathcal{R}(\varDelta )\) be the set of all partitions of \(\varDelta \). We say that \(\varDelta \) is minimal if there not exists \(\mathcal{P}_\mathcal{R}(\varDelta \backslash _{\textsf{End}})\ni S\ne \{\varDelta \backslash _{\textsf{End}}\}\) s.t. \(\varDelta \backslash _{\textsf{End}}=\bigcup _{\varDelta '\in S} \varDelta '\). A partition \(\{\varDelta _1,\dots ,\varDelta _n\}\) of \(\varDelta \) is minimal, denoted as \(\textsf{minPartition}_{\varDelta }(\varDelta _1,\dots , \varDelta _n)\), whenever \(\varDelta _i\) is minimal, for all \(i\in \{1,\dots ,n\}\).
The aim of invoking the LTS on minimal environments is to avoid the non-determinism coming from sub-systems executing unrelated behaviours. The fixed point mechanism based on decreasing sets assumes that once we re-encounter the same environment twice, we can stop since we already explored all possible computations. This is no longer sound if the system contain unrelated sub-systems. For instance, if an environment contains two participants
and
communicating with each other and reaching a fixed point after few steps, and also two participants
and
communicating with each other, then, depending on the oracle (see (iii)), it might be the case that the computation finishes without analysing
and
(cf. [28]). On contrast, if we consider a minimal environment, all parties are properly parsed, because the oracle is forced to analyse all sub-processes of the interacting participants. As we shall see in § 4, the minimality assumption does not pose any limitation because we perform the compliance analysis on all environments of a minimal partition.
Feature (iii) is implemented by adding a fair oracle returning participants willing to reduce or communicate when this option is available. The top level participant of a well-formed type T, denoted \(\texttt {top}(T)\), is a partial function indicating the unguarded participant of a branching or of a selection:
Definition 5
(Oracle fairness). A oracle \(\varOmega \) is fair whenever:
1.
implies
and
2.
implies
3.
\(\varOmega (\varDelta )\) undefined implies
(a)
forall
we have
(b)
there not exists
s.t.
and
Deterministic transitions of session environments have the following form:
where \(\varDelta \) is minimal (i), \(\varOmega \) is a fair oracle (iii), we assume a label scheduling policy (iv), \(\alpha \) is a synchronisation label
or a \(\tau \) action decorated with the originating participant, denoted
, and \(\varDelta \) after the symbol \(\blacktriangleright \) is called the sum continuation and is a type environment or an environment placeholder, denoted \(\nabla ^\circ \) (ii). We note that, w.r.t. to Definition 3, we have that \(\widetilde{A}=\varOmega \), the set of states \(\mathcal{S}_1\) contains \( D\diamond \varDelta \), and the set of states \(\mathcal{S}_2\) contains \(D\diamond \varDelta \blacktriangleright \varDelta \). Moreover, \(\rightarrow _d\) is a partial function: \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha '}{\rightarrow _d}\ D'\diamond \varDelta '_1\blacktriangleright \varDelta '_2\) and \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha ''}{\rightarrow _d}\ D''\diamond \varDelta ''_1\blacktriangleright \varDelta ''_2\) imply \(\alpha '=\alpha ''\), and \(D'= D''\), \(\varDelta '_i=\varDelta ''_i\), \(i=1,2\).
Example 3
Consider \(D\diamond \varDelta \) defined in Example 2. We note that \(\varDelta \) is minimal. Take a fair oracle \(\varOmega \), and assume that the scheduling of labels follows the lexicographic order. First, we note that \(\varOmega (\varDelta )\) undefined gives rise to a contradiction, because e.g.
. Depending on the oracle \(\varOmega \), we may have
or
, because any other combination would contradict Definition 5.
Assume
. A first step let us infer the reduction of the service, where
, and \({\textsf{minimal}} (\varDelta _1)\).
Next, we assume that
, where
.
In the next round we have \({\textsf{minimal}} (\varDelta _2)\) and
, and the algorithm picks the first label in the intersection of the labels of
and
, that is cancel:
After this sequence of transitions, we have two minimal environments \(\varDelta ''\) and \(\varDelta '\) corresponding to the redex of the interaction of the service
and the client
over the label cancel, and to the environment prompt to let
and
interact over the label login, respectively. The idea is to deterministically visit all the binary trees spawned by further transitions starting from \(D_3\diamond \varDelta ''\) and from \(D_3\diamond \varDelta '\), respectively, as we discuss in the next section. \(\square \)
3.3 Closure
The aim of the deterministic LTS presented in § 3.2 is to be used by the function that computes the compliance of session environments in the typing system (cf. § 4). Compliance analyses all final environments computed by the closure of the deterministic transitions originating from a type environment.
More specifically, we consider the semireflexive-transitive closure of the deterministic lts \(\rightarrow _d\), denoted \(\Longrightarrow \). Semireflexivity means that a configuration is related with itself only if is stuck, that is it cannot fire any transition.
We are interested in applying closure to environments preserving minimality.
Definition 6
(Stuck environment). A minimal environment \(\varDelta \) is stuck w.r.t. an oracle \(\varOmega \) and a decreasing set D, denoted \(\texttt {stuck}_{\varOmega , D}(\varDelta )\), if there not exists \(\alpha , \varDelta _1\), \(\varDelta _2\) such that \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha }{\rightarrow _d}\ D'\diamond \varDelta _1\blacktriangleright \varDelta _2\).
Definition 7
(Closure). Define:
The closure of a minimal environment \(\varDelta \) w.r.t. a decreasing set D s.t. \(\varDelta \in D\) and a fair oracle \(\varOmega \) is defined by the following rule:
Given a a fair oracle \(\varOmega \), the relation \(\Longrightarrow \) associates a configuration C to a non-empty tuple of e-configurations\(E_1,\dots , E_n\), denoted as \(\widetilde{E}\), where each \(E_i\) is a configuration C or the failureerr. Given a configuration \(C = D\diamond \varDelta \), three cases may arise. If C is stuck, that is C cannot fire any transition, then we apply rule [C-Rfl] and relate C with itself, else if C is not minimal, then we we apply rule [C-Err] and relate C with err. Otherwise we have that C fires an action and reaches the redex \(\varDelta '\diamond \varDelta _1\blacktriangleright \varDelta _2\): we apply rule [C-Tra] and whenever \(\varDelta '\diamond \varDelta _1\) is related by \(\Longrightarrow \) to the e-configurations \(\widetilde{E_1}\), and \(\varDelta '\diamond \varDelta _2\) is related by \(\Longrightarrow \) to \(\widetilde{E_2}\), we let C be related by \(\Longrightarrow \) to \(\widetilde{E_1},\widetilde{E_2}\).
The closure of a session environment \(\varDelta \) is defined iff \(\Longrightarrow \) does not relate \(\varDelta \) with failures. If this is the case, then \(\Longrightarrow \) relates \(\varDelta \) with configurations \(\widetilde{C}\): the function strips off all decreasing sets and associates \(\varDelta \) to a set of minimal stuck environments. It is worth noting that closure is a terminating function, because it is deterministic and it has |D| as decreasing measure.
Example 4
We continue the analysis started in Example 3 and find a subset of \(\texttt {closure}_{\varOmega ,D}(\varDelta )\), which is defined because \(\varDelta \) and its redexes are minimal. Remember
defined in § 1.1:
. Consider \(D_3\diamond \varDelta ''\blacktriangleright \varDelta '\) defined in Example 3:
To calculate the closure of \(\varDelta \) w.r.t. D, we need to analyse the closures of \(\varDelta ''\) and \(\varDelta '\) w.r.t. \(D_3\), respectively. We have that \(\varDelta ''\) and \(\varDelta '\) are minimal: we analyse the former closure, and note that \(D_3\diamond \varDelta ''\) is not stuck, i.e. the client
and the server
can communicate on quit. Assume
. We have:
We can thus infer
. \(\square \)
Fig. 3.
Type system
4 Iso-Recursive Multiparty Type System
The typing rules for processes and sessions are defined in Figure 3; we refer to the technical report [27] for the rules for expressions.
Typing judgements for processes have the form \(\varGamma \vdash P:T\), where \(\varGamma \) maps variables to sorts and process variables to types:
Typing judgements for sessions have the form \(\varGamma \Vdash \mathcal{M}:\varDelta \), where \(\varDelta \) is the session environment introduced in § 3, that is a map from participants to types, and invoke the type system \(\vdash \). The type system for sessions \(\Vdash \) only invokes the type system for processes \(\vdash \) with well-formed types (cf. § 2): for this reason, the typing rules for processes involving type sums can be simplified (cf. rules T-Sum,T-Sum-L,T-Sum-R).
The rule depicting the essence of iso-recursive multiparty session types is T-Rec. In order to allow \(\varGamma \) to type a recursion process \(\mu \chi .P\) with a type \(\mu X.T\), it must be the case that \(\varGamma ,\chi :\mu X.T\) types the continuation P with the unfolded type \(T\{\mu X.T/X\}\). That is, in our iso-recursive setting the continuation must be typed by explicitly unfolding the recursive type. This is different from the equi-recursive approach, e.g. [23], where the type of \(\mu \chi .P\) and the type of the continuation P can be equal, because types \(\mu X.T\) and \(T\{\mu X.T/X\}\) are equal. For the same reason, in rule T-Var an environment \(\varGamma ,\chi :\mu X.T\) assigns the type \(\mu X.T\) to the process variable \(\chi \): note that it is not possible to assign a non-recursive type to process variables.
Rule T-Inp allows \(\varGamma \) to type a input process
with type
whenever \(\varGamma ,x:S\) assigns the type T to the continuation P. Dually, rule T-Out allows \(\varGamma \) to type an output process
with type
whenever the expression has sort S and \(\varGamma \) assigns the type T to the continuation P.
Rule T-Sum is used for branching and selection, that are sums containing only input types from the same participant and without duplicated labels, or output types from the same participant and without duplicated labels, respectively (cf. Well-Formed Types in § 2, and Definition 2). Note indeed that well-formed types do not contain types of the form e.g. \(T_1 + \mu X.T_2\), or \({\textsf{end}} + T\). The rule says that if \(\varGamma \) can be used to type a process \(P_1\) with type \(T_1\), and a process \(P_2\) with type \(T_2\), then \(\varGamma \) types \(P_1 + P_2\) with type \(T_1 + T_2\).
While rule T-Sum types exactly each input and output with their corresponding input and output type singletons, rule T-Sum-L allows for typing a process P having type \(T_1\) with the type \(T_1 + T_2\). For instance, if P is the branching process
then we can use T-Sum-L to assign to P the type
. Rule T-Sum-R does the same thing, on the right: if P has type \(T_2\) then we can use the rule to assign to P the type \(T_1 + T_2\).
The increased flexibility offered by rules T-Sum-L, T-Sum-R is used in the rule for if-then-else, that is T-If. In order to type process \({\textsf{if}} \; e \; {\textsf{then}} \; P\; {\textsf{else}} \; Q\) with type T we require that e has a boolean sort, and that both P and Q have type T. To allow P and Q to use different labels to communicate in input/output with a participant, we use rules T-Sum-L and T-Sum-R in the premises of T-If, thus mimicking a simple form of subtyping. The next example illustrates this idea.
Consider the variant of Figure 4 of the authorisation server
in § 1.1 such that
verifies the password sent by the client
while allowing only one attempt: if the password is wrong,
sends fail to the service
and stops. We informally discuss the typing of the authorisation server
, and omit the types of the other participants. A formal derivation is included in [27].
Let \(\varGamma \;{\mathop {=}\limits ^{\text {def}}}\;\chi :\mu X.T,x:{\textsf{str}} \), consider the two branches of
, and let
. The left branch
can be assigned to \(T_{\text {if}}\) under \(\varGamma \) by using T-Sum-L, T-Out, T-Var. The right branch
can be assigned to \(T_{\text {if}}\) under \(\varGamma \) by using T-Sum-R, T-Out, T-End. By applying T-If we thus assign \(T_{\text {if}}\) to
under \(\varGamma \) ; in turn, process \(P_1\) is assigned to
under \(\chi :\mu X.T\) by using T-Inp. We note that \(T_1 = T'\{\mu X.T/X\}\). Process \(P_2\) is assigned to
under \(\chi :\mu X.T\): we omit all details. We note that \(T_2 = T''\{\mu X.T/X\}\).
We use T-Sum to assign \(T'\{\mu X.T/X\}+ T''\{\mu X.T/X\}=T\{\mu X.T/X\}\) to \(P_1+P_2\) under \(\chi :\mu X.T\). We conclude by using T-Rec to assign \(\mu X.T\) to
under the empty environment, thus typing the authorisation server. \(\square \)
Type checking sessions. The typing rules for sessions of Figure 3 have the form \(\varGamma \Vdash \mathcal{M}:\varDelta \) and use the rules for processes \(\varGamma \vdash P:T\). The system relies on the notion of minimal partition (cf. Definition 4).
Rule T-Thr is used for single threads and says that if the type system for processes \(\vdash \) can be used to type a process P with a well-formed type T (cf. § 2), then the type system \(\Vdash \) assigns the typing
to the thread
.
Rule T-Ses is the top-level rule used to type-check the multiparty session. In order to type-check a session composing the threads
with the session environment
, we require two things:
1.
Each thread
is typed with the environment
, for \(i=1,\dots n\);
2.
Each environment \(\varDelta _j\) of the minimal partition \(\{\varDelta _1,\dots ,\varDelta _k\}\) of \(\varDelta \) satisfies compliance, denoted \({\textsf{comp}} (\varDelta _j)\).
Compliance resembles the approach based on safe contexts (e.g. [49, Definition 4.1]), although is fully computational.
4.1 Compliance
Intuitively, a session typed by a compliant environment never reaches an error, that is a deadlocked system, or a redex containing two participants
and
that are willing to communicate, e.g.
is sending an output to
, and
is receiving an input from
, or vice-versa, but they mismatch the communication label and/or the type payload, or both
and
are sending (receiving) a value to each other: that is, there is a mismatch that makes the two participants stuck.
The formal definition of compliance relies on the closure of \(\rightarrow _d\) introduced in § 3, and of the formal definition of error below. Let the tagged labels of a type T, denoted \(\mathcal{L}(T)\), be defined inductively as follows:
,
, \(\mathcal{L}(T_1 + T_2) \;{\mathop {=}\limits ^{\text {def}}}\;\mathcal{L}(T_1)\cup \mathcal{L}(T_2)\), \(\mathcal{L}(T)\;{\mathop {=}\limits ^{\text {def}}}\;\emptyset \) otherwise.
Definition 8
(Well-formed environment). A session environment \(\varDelta \) is well-formed, denoted \(\text {WF}(\varDelta )\), whenever
implies
.
Definition 9
(Communication mismatch). A well-formed session environment \(\varDelta \) is a communication mismatch whenever there exists
such that one of the following cases arise:
The notion of deadlock is insensitive to decreasing sets and determinism, and is based on the non-deterministic transition system \(\varDelta \overset{\alpha }{\rightarrow }\varDelta \) of Figure 2.
Definition 10
(Deadlock). Let
. A session environment \(\varDelta \) is a deadlock when both (1) there not exists \(\alpha , \varDelta '\) such that \(\varDelta \overset{\alpha }{\rightarrow }\varDelta '\), and (2) \(\lnot {\textsf{consumed}} (\varDelta )\).
Definition 11
(Error). A well-formed environment \(\varDelta \) is an error whenever \(\varDelta \) is a communication mismatch, or \(\varDelta \) is a deadlock.
Definition 12
(Compliance). Let \(\varDelta \) be a minimal well-formed environment. Define \({\textsf{comp}} (\varDelta )\) whenever for all fair oracles \(\varOmega \) and fixed points D including \(\varDelta \), if \(\texttt {closure}_{\varOmega ,D}(\varDelta )=\varDelta _1, \dots , \varDelta _n\) then \(\varDelta _i\) is not an error, for all \(i\in \{1,\dots ,n\}\).
Example 6
Consider the minimal well-formed environment \(\varDelta ''\) introduced at the end of § 1.1, and the claim \(\lnot {\textsf{comp}} (\varDelta '')\), which follows from \(\varDelta ''\) reaching the deadlocked environment
,
,
. We prove the claim by using a Lemma mapping non-deterministic transitions to deterministic transitions. We start by a sequence of (non-deterministic) transitions from \(\varDelta ''\) that lead to \(\varDelta _{\texttt {lock}}\), and use the result to find a fair oracle \(\varOmega \) mimicking the sequence:
(1)
(2)
(3)
The transitions in (1) correspond to a first round of the protocol, which leads the service
and the client
to re-initialise, while the authorisation server
reaches the type
. The transitions in (2) correspond to a second round of the protocol, which leads the service
and the client
to re-initialise, while the authorisation server
reaches the type \({\textsf{end}} \). The transitions in (3) correspond to the starting of the protocol where the service
sends a login request to the client
. After that, both the service and the client waits to interact with the server
, which has ended. Note that \(\texttt {stuck}_{\varOmega ,D_3}(\varDelta _{\texttt {lock}})\).
We apply a multi-step Lemma (see [27]) and infer \( \varOmega \triangleright D\diamond \varDelta ''\Longrightarrow \widetilde{C_1}, D_3\diamond \varDelta _{\texttt {lock}},\widetilde{C_2} \). By Definition 7, we have \(\varDelta _{\texttt {lock}}\in {\textsf{closure}} _{\varOmega ,D}(\varDelta '')\). To prove \(\lnot {\textsf{comp}} (\varDelta '')\), we show that \(\varDelta _{\texttt {lock}}\) is an error. In fact, \(\varDelta _{\texttt {lock}}\) is a deadlock (cf. Definition 10), because it cannot fire any action, and because there is a participant that has not finished, e.g.
. By Definition 11, \(\varDelta _{\texttt {lock}}\) is an error. \(\square \)
Example 7
Consider the minimal well-formed environment \(\varDelta \) of the authorisation protocol in § 1.1. We claim that for any fair oracle \(\varOmega \) and fixed point \(D\ni \varDelta \), the closure of \(\varDelta \) returns two environments, where
: \({\textsf{closure}} _{\varOmega ,D}(\varDelta )=\{\varDelta ,\varDelta ^{\texttt {end}}\}\). Following this claim, we have \({\textsf{comp}} (\varDelta )\). In fact, both \(\varDelta \) and \(\varDelta ^{\texttt {end}}\) are not errors. By definition, neither \(\varDelta \) nor \(\varDelta ^{\texttt {end}}\) is a mismatch: the latter case is clear; in the former case, the unique unguarded sum of prefixes is the branching of the authorisation service
below, while the type of
is guarded:
Moreover, neither \(\varDelta \) nor \(\varDelta ^{\texttt {end}}\) is a deadlock. \(\varDelta \) can indeed take a step: the environment is in the closure because it is first contained in the initial decreasing set D and then re-encountered after a sequence of interactions. The claim can be verified by using the certified implementation in § 5. \(\square \)
Remark 1
In [49] an environment is deadlock-free if for all redexes \(\varGamma \) reachable in multiple steps we have that if \(\varGamma \) does not move then its range contains only the type \({\textsf{end}} \). Conversely, Definition 10 expresses a negative property, and in turn we transform the implication \({\textsf{stuck}} (\varGamma ) \rightarrow {\textsf{consumed}} (\varGamma )\) of [49] into its negation: \({\textsf{stuck}} (\varGamma ) \wedge \lnot {\textsf{consumed}} (\varGamma )\). \(\square \)
4.2 Subject Reduction and Progress
We conclude this section by showing that the typing system satisfies subject reduction and progress. We outline the sketch of the proof of subject reduction, and refer to [27] for all details, including the proof of progress.
The purpose of the subject reduction theorem is to establish that if a session \(\mathcal M\) is well-typed and does a step \(\alpha \) and reaches the session \(\mathcal{M}'\), then \(\mathcal{M}'\) is well-typed. Assume that \(\varGamma \Vdash \mathcal{M}:\varDelta \). To assess subject reduction, we provide an environment \(\varDelta '\) s.t. \(\varGamma \Vdash \mathcal{M}':\varDelta '\). Since the step \(\mathcal{M}\overset{\alpha }{\rightarrow }\ \mathcal{M}'\) is non-deterministic, we match this step with a non-deterministic environment transition (cf. Figure 2).
A key result to establish subject reduction is that compliance (cf. Definition 12) is preserved by non-deterministic transitions of session environments.
Lemma 1
Let \(\varDelta \) be minimal. If \(D\diamond \varDelta \overset{\alpha }{\rightarrow }\ D'\diamond \varDelta '\) then there exists a fair oracle \(\varOmega \) and environment \(\varDelta ''\) s.t. \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha }{\rightarrow _d}\ D'\diamond \varDelta '\blacktriangleright \varDelta ''\).
Lemma 2
If \({\textsf{comp}} (\varDelta )\) and \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha }{\rightarrow _d}\ D'\diamond \varDelta '\blacktriangleright \varDelta ''\) then \({\textsf{comp}} (\varDelta ')\).
Corollary 1
(Compliance preservation). If \({\textsf{comp}} (\varDelta )\) and \(D\diamond \varDelta \overset{\alpha }{\rightarrow }\ D'\diamond \varDelta '\) then \({\textsf{comp}} (\varDelta ')\).
Lemma 3
If \(\varGamma \Vdash \mathcal{M}_1:\varDelta \) and
then \(\varGamma \Vdash \mathcal{M}_2:\varDelta \).
Proof
If follows from the inversion of \(\varGamma \Vdash \mathcal{M}_1:\varDelta \) and the definition of
. The result is mechanised in Coq. \(\square \)
Theorem 1
(Subject Reduction). Let \(\mathcal M\) be a closed session, and let D be a fixed point including \(\varDelta \). Assume (1) \(\varGamma \Vdash \mathcal{M}:\varDelta \) and (2) \(\mathcal{M}\overset{\alpha }{\rightarrow }\mathcal{M'}\).
We have \(\varGamma \Vdash \mathcal{M}':\varDelta \) or \(D\diamond \varDelta \overset{\alpha }{\rightarrow }\ D'\diamond \varDelta '\) and \(\varGamma \Vdash \mathcal{M'}:\varDelta '\).
Proof
By induction on (2), using value and process substitution (mechanised in Coq), Lemma 3, and Corollary 1. \(\square \)
Let
when for all \(i\in I\) we have \(P_i =\textbf{0}\).
Theorem 2
(Progress). Let \(\mathcal M\) be a closed session. If \(\varGamma \Vdash \mathcal{M}:\varDelta \) and does not exist \(\mathcal{M}'\) s.t. \(\mathcal{M}\overset{\tau }{\rightarrow }\ \mathcal{M}'\) or
, for all
, then \({\textsf{Ended}} (\mathcal M)\).
5 Automated Deductive Verification of Compliance
The typing system presented in § 4 relies on the notion of compliance, which is defined theoretically by relying on the novel definitions of deterministic session environment transitions and closure introduced in § 3. In this section, we showcase how these theoretical notions can de deployed soundly in mainstream programming languages and compilers by presenting a reference implementation of compliance and by mechanising the properties of the implementation, which are that compliant environment are mismatch-free and deadlock-free.
Our goal is to define compliance as a computable function that decides when a session environment has a “good behaviour”, and in turn can be assigned by the typing system to a session. We note that computability is an essential pre-requisite for decidable type checking while assigning non-compliant environments to sessions is unsound because it invalidates progress, and must be avoided.
Towards this aim, we need to (1) deploy the function; (2) provide a mechanised proof that the function terminates; (3) provide a mechanised proof that the function decides freedom from mismatches and deadlocks. This result is established once (by the type system designer): after that, the function can be used each time we invoke the type checker on a session process.
The proofs and their mechanisation in (2) and (3) are necessary because the designer can deploy a wrong implementation, e.g. it could have forgotten a case leading to an environment deadlock, thus allowing to type check sessions that deadlock at runtime. By providing a computer-assisted proof that the implementation rules out errors and deadlocks in environments, we can rely on Theorem 2 to obtain that sessions typed by accepted environments do not deadlock.
In the remainder of the section, we tackle the requirements (1), (2) and (3) by defining function compliance and its behavioural specification, that is the contract of the function [40]. We choose OCaml as target language and use tools of the OCaml ecosystem relying on Why3 [19] to enable automated deductive verification of behavioural specifications by using constraint solvers, e.g. [4, 16, 42], while supporting imperative features, ghost code [18], and interactive proofs.
The verification has been done by using Cameleer [44, 45], which in turn relies on [9, 19]. Proofs of lemmas requiring induction are done interactively in Why3.
5.1 Structure of the Implementation
To implement closure (cf. Definition 7) in OCaml, we use function cstep receiving a fair oracle \(\varOmega \), a decreasing set D, a (ghost) fixed point \(\mathcal W\), a session environment \(\varDelta \), and a (ghost) list of environments \(\mathcal H\) representing the history of the visited environments; the function returns an environment. Function compliance invokes cstep in order to accept or reject the environment \(\varDelta \):
The behavioural specification of the functions is described in § 5.2. Ghost parameters are used both to provide a semantics to the fixed point mechanism and to prove the soundness of the accepted environments, and do not have computational interest: all ghost code referring to such parameters should be erased from the regular code after providing the proof effort [18, 45].
In function cstep we use exceptions to tackle different behaviours of environments. In all cases but for exception Fixpoint, termination by raising an exception determines failure of establishing compliance.
Definition 13
(Positive exits). Positive exits of function cstep are listed below. A positive exit implies that the parameter \(\varDelta \) of cstep satisfies compliance.
W.r.t. the signatures of cstep and of closure in Definition 7, the non-ghost parameters are the same while the return type is different, because closure returns a set of environments. Remember that the aim of the returned set of environments is to establish compliance by verifying that all the final environments are not a communication mismatch, or a deadlock (cf. Definition 12). Function cstep achieves the same result by using exception handling and ghost parameters.
The body of cstep is recursive, and contains sub-calls of the form
\(\texttt {cstep}(\varOmega , D\backslash _{\varDelta }, \mathcal{W}, \varDelta ', (\mathcal{H},\varDelta ))\): the first parameter \(\varOmega \) is the oracle and is the same in all calls; the second parameter \(D\backslash _{\varDelta }\) corresponds to the removal of \(\varDelta \) from the decreasing set D; the third parameter \(\mathcal W\) is the fixed point and is the same in all calls; the fourth parameter \(\varDelta '\) is obtained by updating the type of one or of two participants returned by the oracle \(\varOmega \) (cf. Definition 5); the last parameter appends \(\varDelta \) to the history \(\mathcal H\): in the remainder of the section, the notation\(\mathcal{H},\varDelta \) indicates that \(\varDelta \) is the last environment visited in \(\mathcal{H}\cup \{\varDelta \}\).
5.2 Verification
The verification of function compliance relies on the behavioural specification and verification of function cstep, which in turn relies on auxiliary lemmas.
Fig. 5.
Behavioural specification of the implementation
Figure 5 presents the behavioural specification of the implementation. The column param lists the input arguments of each function. The column result lists the result returned by each function. The column variant indicates the decreasing argument of cstep; note that compliance is not recursive. The column requires indicates the pre-conditions stated in terms of the parameters. The column raises indicates the formula holding for the argument carried by the exception; in the specification of cstep we omit exceptions asserting true. The column ensures indicates the post-condition stated in terms of the result.
There are two positive exits of function cstep establishing the compliance of the environment \(\varDelta \) received in input (cf. Definition 13): termination, and raising Fixpoint. The conditions holding when cstep raises an exception (cf. keyword raises) are discussed below while illustrating the verification process. Note that exceptions Fixpoint, Deadlock, Wrongbranch, DecrNotFix and NotMinimal carry the history \(\mathcal{H}',\varDelta '\), where \(\varDelta '\) is the last visited environment.
The predicate \({\textsf{sound}} _\varOmega (\varDelta ')\) relies on the result of the oracle and on Definition 9: if the oracle receives \(\varDelta '\) and returns one (cf. rule Sd-Rec) or two (cf. rule Sd-Com) participants, and \(\varDelta '\) is not a mismatch, then \(\varDelta '\) is sound. The predicate \({\textsf{cons}} (\varDelta ')\) says that all participants in the environment \(\varDelta '\) have type \({\textsf{end}} \).
The post-condition (cf. keyword ensures) of cstep says that the returned environment is consumed: all participants have type \({\textsf{end}} \). For what concerns the pre-conditions of cstep (cf. keyword requires), the predicate \({\textsf{fair}} (\varOmega )\) implements Definition 5 by relying on constructors \({\textsf{Ret}} _2,{\textsf{Ret}} _1\) and \({\textsf{Ret}} _0\):
The predicate \({\textsf{isFix}} (\mathcal{W},\varDelta ,n)\) says that \(\mathcal{W}\) is a fixed point of \(\varDelta \) (up-to depth n). The core mechanism to analyse iso-recursive types and environments is to rely on fixed points \(\mathcal W\) of type typEnvRedexes, that is a map from participants to all type redexes up-to depth n, and on the projection of all combinations of these mappings into a set of environments, denoted \({\textsf{comb}} (\mathcal W)\). The depth n indicates how many type transitions \(T\overset{\alpha _1}{\rightarrow }\cdots \overset{\alpha _n}{\rightarrow }T'\) are considered (cf. Figure 2); these include the unfolding of iso-recursive types \(\mu X.T\) into \(T\{\mu X.T/X\}\). Given a fixed point \(\mathcal W\), we require that the decreasing set D and the history \(\mathcal H\) partition the set \({\textsf{comb}} (\mathcal W)\) (cf. Figure 5, function cstep, keyword requires, lines 3-4).
The pre-conditions of compliance mirror those of cstep, modulo the fact that there is no history. The post-condition of compliance ensures that the function returns true by exploiting (1) the post-condition of cstep and (2) the formula holding when cstep raises Fixpoint. The exceptional exit of compliance occurs when raising NonCompliant, thus rejecting the input environment \(\varDelta \).
Termination. The first result establishes that function cstep terminates. We instruct [45] to use |D| as decreasing measure, cf. the keyword variant in the function specification of Figure 5, and obtain the desired result automatically.
Absence of communication mismatches. In order to show that environments accepted by compliance are mismatch-free, we ensure that positive exits of function cstep (cf. Definition 13) carry environments that are not communication mismatches (cf. Definition 9) by inspecting cstep’s contract in Figure 5.
The first positive exit is termination: cstep returns \(\varDelta _o\). The contract’s clause with keyword ensures establishes that \(\varDelta _o\) is consumed: by definition, \(\varDelta _o\) is not a mismatch. The second positive exit corresponds to the exception Fixpoint: the exceptions carries the history \(\mathcal{H'},\varDelta '\), where \(\varDelta '\) is the last visited environment. The clause raises establishes that \(\varDelta '\in \mathcal H'\) and that \(\varDelta '\) is sound. By inversion of rules Sd-Rec, Sd-Com, we obtain that \(\varDelta '\) is not a mismatch. \(\square \)
The automated verification is performed in [45] and relies on the predicate \({\textsf{mismatch}} _2(T_1, T_2)\) (cf. Figure 5) to deal with wrong choices of sums: intuitively, the predicate follow Definition 9 by using types rather than participants.
Absence of deadlocks. Similarly, we show that positive exits of cstep of Definition 13 correspond to absence of deadlocks of Definition 10.
The first positive exit occurs when function cstep returns \(\varDelta _o\). The clause with keyword ensures establishes that \(\varDelta _o\) is consumed: by definition, \(\varDelta _o\) is not a deadlock. The second positive exit is raising exception Fixpoint; the exception carries the history \(\mathcal{H}',\varDelta '\), where \(\varDelta '\) is the last visited environment. From the contract’s clause with keyword raises, we infer that \(\varDelta '\in \mathcal H'\) and that \(\varDelta '\) is sound.
By inversion of rules Sd-Rec, Sd-Com, we obtain that two cases arise: (1) there is a participant
s.t.
and \(\varDelta '\) is not a mismatch; (2) there are participants
such that
and \(\varDelta '\) is not a mismatch. We show that in both cases (1) and (2) we have that \(\varDelta '\) can do a transition.
1.
By the fairness pre-condition of cstep, we obtain
We apply E-Rec, Se-Rec of Figure 2 and find \(\varDelta ''\) s.t. \(\varDelta '\overset{\tau }{\rightarrow }\varDelta ''\).
2.
By the fairness pre-condition of cstep, we obtain
where
and
.
By inversion of
and
(cf. Definition 5), we obtain that
or
, and
or
.
By hypothesis, \(\varDelta '\) is not a mismatch: Definition 9 ensures that two sub-cases arise:
and
and
, or
, and
and
. In both cases we apply Se-Com of Figure 2 and find \(\alpha , \varDelta ''\) s.t. \(\varDelta '\overset{\alpha }{\rightarrow }\varDelta ''\). \(\square \)
6 Related Work
To the best of our knowledge, only few works follow an iso-recursive approach to session types. [31] proposes a decentralized analysis of multiparty protocols that is based on a typed asynchronous \(\pi \)-calculus relying on the notion of router processes; deadlock-freedom is established by following the priority-based approach of session types [13]. The rule to type check recursion types the continuation by unfolding iso-recursive types and lifting priorities to a common greater highest priority. Finally, type preservation holds up to unfolding (cf. [31, Theorem 2]).
[36] studies iso-recursive and equi-recursive subtyping for binary sessions. Session types are interpreted as propositions of multiplicative/additive linear logic extended with least and greatest fixed points (cf. [8, 54]). The typing rules correspond to the proof rules in [3], and include the unfolding of least and greatest fixed points. The authors compare the two subtyping relations, and note that the relations preserve not only the usual safety properties, but also termination.
Many recent papers [39, 43, 48, 56‐59] rely on iso-recursive types for variants of the \(\lambda \)-calculus, following the seminal work on Amber rules [1]. While the setting is different from ours, these papers provide several insights on the advantage of iso-recursive types and on their algorithmic implementation and mechanised verification. Previous papers [2, 6] studied iso-recursive types for a concurrent \(\lambda \)-calculus that can be seen as the foundational theory of core \(F^\sharp \).
As mentioned above, iso-recursive types have been first studied formally in the setting of Amber rules [1]. Pierce’s book [47] further discusses the differences between iso-recursive and equi-recursive types.
Future Work. Our plans go along two directions: completing the study in the paper and extending the language model and the type analysis.
Towards completion, we plan to conclude the mechanisation of subject reduction in Coq, and to compare the performance of compliance checking in OCaml with the verification of deadlock freedom in bottom-up approaches (cf. [52]) relying on model-checking [49], eventually considering a realistic testing suite involving multiple participants and interactions (cf. [49, Table 2]).
For what concerns extensions, there are two main features we are interested in: session delegation and asynchronous subtyping for multiparty session types.
Handling session delegation in session types is challenging and might require type constructors [25] or session channel decorations [15, 22, 53] to preserve type soundness. Our plan is to enforce soundness at the type level, without affecting the programmer’s syntax.
Asynchronous subtyping (e.g. [24]) is known to be undecidable for more than two participants. We envision to overcome this obstacle to an algorithmic solution by considering a maximal depth of the search of the asynchronous outputs that can be anticipated, similarly to the bound on recursion in [12].
Acknowledgements
We thank the reviewers for detailed and helpful comments. This work is partially supported by EPSRC EP/T006544/2, EP/N027833/2, EP/T014709/2, EP/Y005244/1, EP/V000462/1, Horizon EU TaRDIS 101093006, Advanced Research and Invention Agency (ARIA), and a grant from the Simons Foundation.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Formally, contractiveness is mechanised in Coq [11] by relying on the reflexive-transitive closure of the transition system of types introduced in § 3.
as the types
and
, respectively, where l is a label indicating the nature of the communication, S is the sort of the payload, and T is the type of the continuation. Selection among (branching on) different output (input) types is done by means of the binary operator \(+\). Recursion is provided by the construct \(\mu X.T\), which binds the type variable X in T. Termination is represented by type \({\textsf{end}} \). Sorts describe the types of string, boolean, and unit values. The session types of the service (
), of the client (
), and of the authorisation server (
) are: 
) sends to the client (
) either a request to 
continues by sending the password (
, who in turn sends authentication to
(
sends 
, and the session ends.
to types T. The environment
can fire an output action
and reach
, or can fire an output action
and reach
. The environment
can fire an input action
and reach
, where
, or can fire an input action
and reach
. The environment \(\varGamma _1,\varGamma _2\) can fire two synchronisation actions: (1)
, which indicates a synchronisation on the label login by the input participant
and the output participant
, and reach the environment
; and (2)
, and reach the environment
.
as 
, and
are all different, but isomorphic. A recursive type \(\mu X.T\) can only be used to type-check a recursive process, or a type variable. To type check an input or output process, we need to unfold \(\mu X.T\) by applying the substitution \(\mu X.T /X\) to type T, denoted as \(T\{\mu X.T /X\}\). That is, we have the following iso-recursive equations: 
below, whose syntax mirrors the one of its type
, but that the payload of input and output are (bound) variables and expressions, respectively, and that there is a process variable \(\chi \): 
we use the typing judgement: 
with
, that is process
, and the parallel execution of
with
and
, where
are recursive processes implementing the service
typed by
, and the client
typed by
, respectively. This session should be accepted by the type system, since at runtime it behaves correctly, independently of the fact that the authorisation service
has been “unrolled” once.
has a single I/O type receiving from/sending to participant
, and
has a single I/O type receiving from/sending to participant
, and one of the following cases arise: (i) both
and
are sending or receiving; (ii) the intersection among the labels used by
and
is empty; (iii)
and
agree on a label but disagree on the label’s sort. A deadlock arises when the environment \(\varDelta \) cannot fire any transition and there is at least a participant
s.t.
.
only allows two subsequent attempts for 
performs an infinite number of requests of 
to range over participants, l to range over labels, and i, j to range over indexes (natural numbers). X, Y range over type variables, \(e, e'\) range over expressions, v, w range over values, x, y range over variables, and \(\chi \) range over process variables. Sessions \(\mathcal M\) belong to the set \(\mathbb M\). A single session or thread is a process P indexed by a participant, denoted
. A multiparty session is a composition of all threads, denoted
or
.
and free in P. Closed terms are those without free variables.
or of the form e.g.
with
, as well as mixed choice types, e.g.
. A type T is well-formed, denoted \(\text {WF}(T)\), when it is well-behaved, contractive, and closed.
. We let
be the least reflexive relation that satisfies the axiom 
, or reductions \(\mathcal{M}_1\overset{\alpha }{\rightarrow }\mathcal{M}_2\overset{\alpha }{\rightarrow }\cdots \). We are mainly interested in analysing computations of well-typed sessions (cf. § 4).
waiting for a value from
on the label l can do a transition labelled by
and instantiate the formal parameter x with the value v in the continuation P, noted as \(P\{v/x\}\). Rule R-Out allows a participant
sending to
on label l an expression e that can be evaluated as v to do a transition labelled by
and continue as P. Non-deterministic reductions are allowed by means of rule R-Sum-L, which says that a participant
non-deterministically choosing among process P and Q, denoted \(P + Q\), can do a transition labelled by \(\alpha \) and reach
whenever
can fire the same transition and reach the same redex.
and
is performed by means of rule R-Com. Whenever
can do a transition labelled by the input action
and reach the redex
, and
can do a transition labelled by the output action
and reach the redex
, we can infer a transition labelled with
from the composition of
and
and a session
to the composition of
and
and
. Rule R-Rec allows a participant
recursively defined as \(\mu \chi .P\) and running in parallel with a session
, to do an internal transition \(\tau \) and unfold the body P while instantiating the occurrences of \(\chi \) in P with \(\mu \chi .P\), thus reaching the redex
. Rule R-IfT (R-IfF) says that a participant
with the body \({\textsf{if}} \; e \; {\textsf{then}} \; P\; {\textsf{else}} \; Q\) and running in parallel with a session
, can do a \(\tau \)-transition and reach the redex
(
) whenever the expression e evaluates to true (false). Rule R-Str rearranges processes with structural congruence.
where process
implements the (unfolding of the) authorisation server
, and processes
and
implement the service
and the client
, respectively. We analyse transitions of the session introduced in § 1.1 and composing the service
, the client
, and the server
, here referred as \(\mathcal M\).
with the client
depicting a 
: 
.
. Since the client thread does not occur in the left, we need to first apply R-Rec and then apply structural congruence in rule R-Str: 
. Now we apply rule R-Com to infer a communication among the service
and the client
on the label 
, and 
is ready to communicate the password, or to send a 
. \(\square \)
.
on label l with payload S and continuing as T can fire the action
and reach the redex T whenever v is a value of sort S. Dually, rule E-In allows an input type from
on label l with payload S and continuing as T to do an action
and reach the redex T, if v has sort S. Rule E-Sel-L allows a sum type \(T_1 + T_2\) to do an output action
and reach the redex \(T'\) whenever \(T_1\) can fire this action and reach \(T'\). Dually, rule E-Bra-L allows a sum type \(T_1 + T_2\) to do an input action
and reach the redex \(T'\) if \(T_1\) can fire this action and reach \(T'\). Note that input and output are the only actions that a sum type can fire. This is because types as e.g. \(T_1 + \mu X.T\) or \(T_1 + (\mu X.T + T_2)\) are not well-formed.
can do an internal action \(\tau \) and reach the environment
, thus unfolding the type of the participant
. Rule Se-Com applies to session environments and depicts a communication: when a participant
has a type
that can fire an input action
and move to
, and a participant
has a type
that can fire an output action
and move to
, then
can fire a synchronisation action
and move to
.
,
. Consider a fixed point D such that \(\varDelta \in D\). A first application of E-Rec, Se-Rec, Se-Top allows for unfolding the type of the service
, where we let
: 
, we need to verify that \(\varDelta _1\in D\backslash _{\varDelta }\): this follows indeed from the property of a fixed point, that is to be closed under transition, and from the fact \(\varDelta _1\ne \varDelta \), which holds because types are iso-recursive, and in turn
. We proceed as above and infer the following transition, where
: 
and
: one over the label login and the other over the label cancel. The interaction below corresponds to the label login and is obtained by applying E-Out, E-Sel-L, E-In, E-Bra-L, Se-Com, Se-Top, where
and \(D_2\;{\mathop {=}\limits ^{\text {def}}}\;D\backslash _{\varDelta ,\varDelta _1}\) and \(D_3\;{\mathop {=}\limits ^{\text {def}}}\;D_2\backslash _{\varDelta _2}\): 
and \(\varDelta _3\ne \varDelta '_3\). \(\square \)
, \({\textsf{parties}} (\mu X.T)\;{\mathop {=}\limits ^{\text {def}}}\;{\textsf{parties}} (T)\), \({\textsf{parties}} (T_1+T_2)\;{\mathop {=}\limits ^{\text {def}}}\;{\textsf{parties}} (T_1)\cup {\textsf{parties}} (T_2)\), and \({\textsf{parties}} (T)\;{\mathop {=}\limits ^{\text {def}}}\;\emptyset \) otherwise. Let \({\textsf{parties}} (\emptyset )\;{\mathop {=}\limits ^{\text {def}}}\;\emptyset \),
. Let \(\varDelta \backslash _{\textsf{End}}\) project all non-ended participants of \(\varDelta \).
and
communicating with each other and reaching a fixed point after few steps, and also two participants
and
communicating with each other, then, depending on the oracle (see (iii)), it might be the case that the computation finishes without analysing
and
(cf. [28]). On contrast, if we consider a minimal environment, all parties are properly parsed, because the oracle is forced to analyse all sub-processes of the interacting participants. As we shall see in § 4, the minimality assumption does not pose any limitation because we perform the compliance analysis on all environments of a minimal partition.
implies
and
implies
we have
s.t.
and
or a \(\tau \) action decorated with the originating participant, denoted
, and \(\varDelta \) after the symbol \(\blacktriangleright \) is called the sum continuation and is a type environment or an environment placeholder, denoted \(\nabla ^\circ \) (ii). We note that, w.r.t. to Definition 3, we have that \(\widetilde{A}=\varOmega \), the set of states \(\mathcal{S}_1\) contains \( D\diamond \varDelta \), and the set of states \(\mathcal{S}_2\) contains \(D\diamond \varDelta \blacktriangleright \varDelta \). Moreover, \(\rightarrow _d\) is a partial function: \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha '}{\rightarrow _d}\ D'\diamond \varDelta '_1\blacktriangleright \varDelta '_2\) and \(\varOmega \triangleright D\diamond \varDelta \overset{\alpha ''}{\rightarrow _d}\ D''\diamond \varDelta ''_1\blacktriangleright \varDelta ''_2\) imply \(\alpha '=\alpha ''\), and \(D'= D''\), \(\varDelta '_i=\varDelta ''_i\), \(i=1,2\).
. Depending on the oracle \(\varOmega \), we may have
or
, because any other combination would contradict Definition 5.
. A first step let us infer the reduction of the service, where
, and \({\textsf{minimal}} (\varDelta _1)\). 
, where
. 
, and the algorithm picks the first label in the intersection of the labels of
and
, that is cancel: 
and the client
over the label cancel, and to the environment prompt to let
and
interact over the label login, respectively. The idea is to deterministically visit all the binary trees spawned by further transitions starting from \(D_3\diamond \varDelta ''\) and from \(D_3\diamond \varDelta '\), respectively, as we discuss in the next section. \(\square \)
defined in § 1.1:
. Consider \(D_3\diamond \varDelta ''\blacktriangleright \varDelta '\) defined in Example 3: 
and the server
can communicate on quit. Assume
. We have: 
. \(\square \)
with type
whenever \(\varGamma ,x:S\) assigns the type T to the continuation P. Dually, rule T-Out allows \(\varGamma \) to type an output process
with type
whenever the expression has sort S and \(\varGamma \) assigns the type T to the continuation P.
then we can use T-Sum-L to assign to P the type
. Rule T-Sum-R does the same thing, on the right: if P has type \(T_2\) then we can use the rule to assign to P the type \(T_1 + T_2\).
in § 1.1 such that
verifies the password sent by the client
while allowing only one attempt: if the password is wrong,
sends fail to the service
and stops. We informally discuss the typing of the authorisation server
, and omit the types of the other participants. A formal derivation is included in [27].
, and let
. The left branch
can be assigned to \(T_{\text {if}}\) under \(\varGamma \) by using T-Sum-L, T-Out, T-Var. The right branch
can be assigned to \(T_{\text {if}}\) under \(\varGamma \) by using T-Sum-R, T-Out, T-End. By applying T-If we thus assign \(T_{\text {if}}\) to
under \(\varGamma \) ; in turn, process \(P_1\) is assigned to
under \(\chi :\mu X.T\) by using T-Inp. We note that \(T_1 = T'\{\mu X.T/X\}\). Process \(P_2\) is assigned to
under \(\chi :\mu X.T\): we omit all details. We note that \(T_2 = T''\{\mu X.T/X\}\).
under the empty environment, thus typing the authorisation server. \(\square \)
to the thread
.
with the session environment
, we require two things:
is typed with the environment
, for \(i=1,\dots n\);
and
that are willing to communicate, e.g.
is sending an output to
, and
is receiving an input from
, or vice-versa, but they mismatch the communication label and/or the type payload, or both
and
are sending (receiving) a value to each other: that is, there is a mismatch that makes the two participants stuck.
,
, \(\mathcal{L}(T_1 + T_2) \;{\mathop {=}\limits ^{\text {def}}}\;\mathcal{L}(T_1)\cup \mathcal{L}(T_2)\), \(\mathcal{L}(T)\;{\mathop {=}\limits ^{\text {def}}}\;\emptyset \) otherwise.
implies
.
such that one of the following cases arise: 
. A session environment \(\varDelta \) is a deadlock when both (1) there not exists \(\alpha , \varDelta '\) such that \(\varDelta \overset{\alpha }{\rightarrow }\varDelta '\), and (2) \(\lnot {\textsf{consumed}} (\varDelta )\).
,
,
. We prove the claim by using a Lemma mapping non-deterministic transitions to deterministic transitions. We start by a sequence of (non-deterministic) transitions from \(\varDelta ''\) that lead to \(\varDelta _{\texttt {lock}}\), and use the result to find a fair oracle \(\varOmega \) mimicking the sequence:
The transitions in (1) correspond to a first round of the protocol, which leads the service
and the client
to re-initialise, while the authorisation server
reaches the type
. The transitions in (2) correspond to a second round of the protocol, which leads the service
and the client
to re-initialise, while the authorisation server
reaches the type \({\textsf{end}} \). The transitions in (3) correspond to the starting of the protocol where the service
sends a login request to the client
. After that, both the service and the client waits to interact with the server
, which has ended. Note that \(\texttt {stuck}_{\varOmega ,D_3}(\varDelta _{\texttt {lock}})\).
. By Definition 11, \(\varDelta _{\texttt {lock}}\) is an error. \(\square \)
: \({\textsf{closure}} _{\varOmega ,D}(\varDelta )=\{\varDelta ,\varDelta ^{\texttt {end}}\}\). Following this claim, we have \({\textsf{comp}} (\varDelta )\). In fact, both \(\varDelta \) and \(\varDelta ^{\texttt {end}}\) are not errors. By definition, neither \(\varDelta \) nor \(\varDelta ^{\texttt {end}}\) is a mismatch: the latter case is clear; in the former case, the unique unguarded sum of prefixes is the branching of the authorisation service
below, while the type of
is guarded: 
then \(\varGamma \Vdash \mathcal{M}_2:\varDelta \).
. The result is mechanised in Coq. \(\square \)
when for all \(i\in I\) we have \(P_i =\textbf{0}\).
, for all
, then \({\textsf{Ended}} (\mathcal M)\).
s.t.
and \(\varDelta '\) is not a mismatch; (2) there are participants
such that
and \(\varDelta '\) is not a mismatch. We show that in both cases (1) and (2) we have that \(\varDelta '\) can do a transition.
or
, and
or
.
and
.
and
(cf. Definition 
and
and
, or
, and
and
. In both cases we apply 
