Featherweight Scribble

Abstract

This paper gives a formal definition of the protocol specification language Scribble. In collaboration with industry, Scribble has been developed as an engineering incarnation of the formal multiparty session types. In its ten years of development, Scribble has been applied and extended in manyfold ways as to verify and ensure correctness of concurrent and distributed systems, e.g. type checking, runtime monitoring, code generation, and synthesis. This paper introduces a core version of Scribble, Featherweight Scribble. We define the semantics of Scribble by translation to communicating automata and show a behavioural-preserving encoding of Scribble protocols to multiparty session type.

1 Introduction

The computational model, Klaim, introduced by De Nicola and others [8] advocates a hybrid (dynamic and static) approach for access control against capabilities (policies) to support static checking integrated within a dynamic access-control procedure. Their capabilities can specify crucial operations for mobile computation such as read, write and execute of processes in relation to the various localities, as types. Around the same period, (binary) session types [14, 27] were proposed to describe a sequence of read (output), write (input) and choice operations for channel passing protocols. Later binary session types were extended to multiparty session types [7, 15], as a model of abstract choreographies of Web Services Choreography Description Language [6]. See [16, §1] for more historical backgrounds.

Scribble [13, 26] is a protocol description language, formally based on the multiparty session type theory. A protocol in Scribble represents an agreement on how participating systems interact with each other. It specifies a format and a predefined order for messages to be exchanged. The name of the language embodies the motivation for its creation, as explained by the following quote from the inventor of the Scribble language Kohei Honda:

The name (Scribble) comes from our desire to create an effective tool for architects, designers and developers alike to quickly and accurately write down protocols.

The development of Scribble is a result of a persistent dialogue between researchers and industry partners. Currently Scribble tools are applied to verification of main stream languages such as Java [18, 19], Python [9, 17], MPI [24], Go [5], F# [22], Erlang [23].

All great ideas of architectural construction come from that unconscious moment, when you do not realise what it is, when there is no concrete shape, only a whisper which is not a whisper, an image which is not an image, somehow it starts to urge you in your mind, in so small a voice but how persistent it is, at that point you start scribbling

Although Scribble is often referred as “the practical incarnation of multiparty session types (MPST)” [13, 26], a formal correspondence between the two is not proven in the literature. In this paper we present the semantics of Scribble protocols, given by translation to communicating automata, and show a behavioural-preserving encoding of Scribble protocols to multiparty session type.

Section 2 gives an overview of Scribble and explains the Scribble framework. Section 3 presents the formal semantics of the Scribble language. Section 4 proves the encoding of Scribble local and global protocols to global and local session types to be behaviour-preserving. Section 5 gives the translation between local Scribble protocols and Communicating Finite State machines (CFSMs) [10]. Section 6 concludes. Appendix contains omitted proofs.

Fig. 1.

Scribble development methodology

2 Scribble Overview

Scribble protocols describe an abstract structure of message exchanges between roles: roles abstract from the actual identity of the endpoints that may participate in a run-time conversation instantiating the protocol. Scribble enables the description of abstract interaction structures including asynchronous message passing, choice, and recursion.

Here we demonstrate the basic Scribble constructs via an example of an online payment service. Figure 2 (left) shows the global Scribble protocol . The first line declares, under the name , the Scribble global protocol and the two participating roles. The protocol has a recursion at thetop-level. In each iteration, the sends the the current balance and the overdraft limit for client’s account. The message has an payload; similarly for the . then can choose to either make a payment, close the account or quit this session.

Figure 1 gives an abstract overview of the Scribble verification process. From a global Scribble protocol, the toolchain produces (1) a set of local protocols or (2) a set of finite state machines (FSMs). We outline the tasks performed by the Scribble toolchain.

Fig. 2.

A global (left) and local (right) Scribble protocol

Well-Formedness Check: A global Scribble protocol is verified for correctness to ensure that the protocol is well-formed, which intuitively represents that a protocol describes a meaningful interaction, beyond the basic syntax defined by the language grammar. This well-formed checking is necessary because some of the protocols are unsafe or inconsistent even if they follow the grammar. For example, two choice branches from the same sender to the same receiver with the same message signature lead to ambiguity at the receiver side. A protocol is well-formed if local protocols can be generated for all of its roles, i.e., the projection function is defined for all roles. The formal definition of projection is given in Definition 4.10. Here we give intuition as to what the main syntactic restrictions are. First, in each branch of a choice the first interaction (possibly after a number of unfoldings) is from the same sender (e.g., ${\mathtt {A}}$) and to the same set of receivers. Second, in each branch of a choice the labels are pair-wise distincs (i.e., protocols are deterministic).

Projection: A global Scribble protocol is projected to a set of local protocols. More precisely, a local Scribble protocol is generated per each role declared in the definition of the global protocol. Local protocols correspond to local (MPST) types, they describe interactions from the viewpoint of a single entity. They can be used directly by a type checker to verify that an endpoint code implementation complies to the interactions prescribed by a specification. Figure 2 (right) lists the Scribble local protocol projected for role .

FSM Generation: An alternative representation of a local protocol can be given in the form of a communicating finite state machine (FSM). This representation is useful for runtime verification. Specifically, at runtime the traces emitted by a program are checked against the language accepted by the FSM.

An implementation of Java and Python based Scribble tools for projection and validation [26], as well as static verification for various languages can be found in [1].

3 Syntax and Semantics of Scribble

3.1 Scribble Global Protocols

We now define the syntax of Scribble global protocols. The grammar is given below.

Definition 3.1

(Scribble Global Protocols)

Protocol names are ranged over by pro. A (global) specification declares a protocol with name $\mathtt {pro}$, involving a list ($\mathtt {A_1}, .. \mathtt {A_n}$) of roles, and prescribing the behaviour in . The other constructs are explained below:

• An interaction specifies that a message $\mathtt {a}(\mathtt {\mathtt {S}})$ should be sent from role ${\mathtt {A}}$ to role ${\mathtt {B}}$ and that the protocol should then continue as prescribed by the continuation . Messages are of the form $\mathtt {a}(\mathtt {\mathtt {S}})$ with $\mathtt a$ being a label and $\mathtt {S}$ being the constant type of exchanged messages (such as and ).

• A choice specifies a branching where role ${\mathtt {A}}$ chooses to engage in the interactions prescribed by one of the options . The decision itself is an internal process to role ${\mathtt {A}}$, i.e. how ${\mathtt {A}}$ decides which scenario to follow is not specified by the protocol.

• A recursion defines a scope with a name $\mathtt{{t}}$ and a body . Any call executes another recursion instance (if is not in an appropriate scope than it remains idle).

Formal Semantics of Global Protocols. The formal semantics of global protocols characterises the desired/correct behaviour of the roles in a multiparty protocol. We give the semantics for Scribble protocols as a Labelled Transition System (LTS). The LTS is defined over the following set of transition labels:

$$\begin{aligned} \ell {:}{:}={\mathtt {A}}{\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}}) \ | \ {\mathtt {A}}{\mathtt {B}}? \mathtt {a}(\mathtt {\mathtt {S}}) \end{aligned}$$

Label ${\mathtt {A}} {\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$ is for a send action where role ${\mathtt {A}}$ sends to role ${\mathtt {B}}$ a message $\mathtt {a}(\mathtt {\mathtt {S}})$. Label ${\mathtt {A}}{\mathtt {B}} ? \mathtt {a}(\mathtt {\mathtt {S}})$ is for a receive action where ${\mathtt {B}}$ receives (i.e., collects from the queue associated to the appropriate channel) message $\mathtt {a}(\mathtt {\mathtt {S}})$ that was previously sent by ${\mathtt {A}}$. We define the subject of an action, modelling the role that has the responsibility of performing that action, as follows:

$$\begin{aligned} subj({\mathtt {A}} {\mathtt {B}} ! \mathtt {a}(\mathtt {\mathtt {S}})) = {\mathtt {A}} \qquad subj({\mathtt {A}} {\mathtt {B}} ? \mathtt {a}(\mathtt {\mathtt {S}})) = {\mathtt {B}} \qquad \end{aligned}$$

As, due to asynchrony, send and receive are two distinct actions, the LTS shall also model the intermediate state where a message has been sent but it has not been yet received. To model these intermediate states we introduce the following additional global Scribble interaction:

to describe the state in which a message $\mathtt {a}(\mathtt {\mathtt {S}})$ has been sent by ${\mathtt {A}}$ but not yet received by ${\mathtt {B}}$. We call runtime global protocol a protocol obtained by extending the syntax of Scribble with these intermediate states.

The transition rules are given in Fig. 3. Rule ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ models a sending action; it produces a label ${\mathtt {A}} {\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$. The sending action yields a state in which the global protocol is in an intermediate state.

Rule ${\scriptstyle \lfloor {\textsc {recv}}\rfloor }$ models the dual receive action, from an intermediate state to a continuation . Rule ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ continues the execution of the protocol as a continuation of one of the branches. Rule ${\scriptstyle \lfloor {\textsc {rec}}\rfloor }$ is standard and unfolds recursive protocols.

We explain the remaining rules with more detailed illustration.

Due to asynchrony and distribution, in a particular state of a Scribble global protocol it may be possible to trigger more than one action. For instance, the protocol in (1) allows two possible actions: ${\mathtt {A}}{\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$ or ${\mathtt {C}}{\mathtt {D}}! \mathtt {a}(\mathtt {\mathtt {S}})$.

(1)

This is due to the fact that the two send actions are not causally related as they have different subjects (which are independent roles). We want the semantics of Scribble to allow, in the state with protocol (1), not only the first action that occurs syntactically (e.g., ${\mathtt {A}}{\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$) but also any action that occurs later, syntactically, but it is not causally related with previous actions in the protocol (e.g., ${\mathtt {C}}{\mathtt {D}}! \mathtt {a}(\mathtt {\mathtt {S}})$). Rule ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$ captures this asynchronous feature. ${\mathtt {C}}{\mathtt {D}}! \mathtt {a}(\mathtt {\mathtt {S}})$, which occurs syntactically later than ${\mathtt {A}}{\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$ to possibly occur before. In fact, the LTS allows (1) to take one of these two actions: either ${\mathtt {A}}{\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$ by rule ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ or ${\mathtt {C}}{\mathtt {D}}! \mathtt {a}(\mathtt {\mathtt {S}})$ is allowed by ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$. Rule ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }$ is similar to ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$ but caters for intermediate states, and is illustrated by the protocol in (2).

(2)

The protocol in (2) is obtained from (1) via transition ${\mathtt {A}}{\mathtt {B}}! \mathtt {a}(\mathtt {\mathtt {S}})$ by rule ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$. The above protocol can execute either ${\mathtt {A}}{\mathtt {B}}? \mathtt {a}(\mathtt {\mathtt {S}})$ by rule ${\scriptstyle \lfloor {\textsc {recv}}\rfloor }$, or ${\mathtt {C}}{\mathtt {D}}! \mathtt {a}(\mathtt {\mathtt {S}})$ by rule ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }$.

Fig. 3.

Labelled transitions for global protocols.

Fig. 4.

Labelled transitions for local protocols (from ${\mathtt {A}}$’s point of view)

Fig. 5.

Syntax for global and local types

Fig. 6.

(adapted from [11])

Labelled transitions for global types

Fig. 7.

(adapted from [11])

LTS for local session types

3.2 Scribble Local Protocols

Scribble local protocols describe a session from the perspective of a single participant. The syntax of Scribble local protocols is given below.

Definition 3.2

(Scribble Local Protocols)

The construct models a send action from ${\mathtt {A}}$ to ${\mathtt {B}}$; the dual local protocol is that models a receive action of ${\mathtt {A}}$ from ${\mathtt {B}}$. The other protocol constructs are similar to the corresponding global protocol constructs. Recursive variables are guarded in the standard way, i.e. they only occur under a prefix. For convenience we will, sometimes, use the notation to denote protocols of the form with $n>1$, or of the form when $n=1$.

Decomposing global protocols into a set of local protocols is called projection. Projection is a key mechanism to enable distributed enforcement of global properties. Projection preserves the interaction structures and message exchanges required for the target role to fulfil his/her part in the conversation. The formal definition of projection, for a normal (canonical) form of global protocols, is given by Definition 4.10.

Formal Semantics of Local Protocols. The LTS for local protocols is defined by the rules in Fig. 4, and uses the same labels as the global semantics in Fig. 3. The rules $\scriptstyle \lfloor {\textsc {send}}\rfloor$, $\scriptstyle \lfloor {\textsc {recv}}\rfloor$, $\scriptstyle \lfloor {\textsc {choice}}\rfloor$, $\scriptstyle \lfloor {\textsc {rec}}\rfloor$ are similar to the respective rules for global protocols. No rules for asynchrony are required as each participant is assumed to be single threaded.

Formal Semantics of Configurations. The LTS in Fig. 4 describes the behaviour of each single role in isolation. In the rest of this section we give the semantics of systems resulting from the composition of Scribble local protocols and communication channels. Given a set of roles $\{1,\ldots ,n\}$ we define configurations where are unidirectional, possibly empty (denoted by $\epsilon$), unbounded FIFO queues with elements of the form $\mathtt {a}(\mathtt {\mathtt {S}})$.

Definition 3.3

(Semantics of configurations).

In (1) the configuration makes a send action given that one of the participants can perform that send action. Case (1) has the effect of adding a message, that is sent, to the corresponding queue. In (2) the configuration makes a receive action given that one of its participant can perform such an action and that the message being received is currently stored in the corresponding queue. Thus, (2) has the effect of removing the message received from the queue.

4 Correspondence Between Scribble and MPST

In this section we show that a trace of a global protocol corresponds exactly to a trace of its projected local protocols. Correspondence is important as it ensures that the composition of processes, each implementing some local protocol, will behave as prescribed by the original global specification. In the context of MPST, this property is known as soundness of the projection (Theorem 3.1, [11]) and has already been proven for global types as defined in [11]. As explained in Sect. 4.1 a translation of this result to Scribble, however, is not obvious.

Figure 8 gives a high level overview of the results presented in this section. First, we discuss the (syntactic) differences between global types and global protocols. We present a normal form for global protocols such that a Scribble global protocol in a normal form can be encoded into (MPST) global types and it preserves semantics. We then prove a similar correspondence between Scribble local protocols and (MPST) local types. The soundness of the projection of global protocols then follows from soundness of the projection of MPST global types (Theorem 3.1 from [11]).

Fig. 8.

Workflow of proving soundness of the projection

4.1 Scribble Normal Form

We recall the syntax of global types from [11] in Fig. 5. It is very similar to the syntax of Scribble global protocols in Sect. 3 except: (1) Scribble does not cater for delegation and higher order protocols whereas global types do; and (2) the choice and interaction protocols are two separated constructs in Scribble while they are modelled as a unique construct in global types and (3) differently than MPST, Scribble allows unguarded choice. The case of (2) is a consequence of the specific focus of Scribble as a protocol design language directed at practitioners that are familiar with e.g., Java notation, who proved to find this notation friendlier [12, 13, 26, 28]. Regarding (3) the choice construct in Scribble directly supports recursion and choice while in MPST the choice is always directly followed by an interaction. In the following section we explain that these differences are indeed syntactic and do not affect the soundness of the language.

Definition 4.1

(Scribble Normal Form (SNF))

First, we observe that a Scribble syntax with a guarded and a singleton choice directly corresponds to MPST. We refer to a Scribble protocol, where all choices are guarded, as a Scribble Normal Form (SNF). Later we show that there is a behaviour preserving translation between a well-formed Scribble protocol and its normal form. The Scribble Normal Form (SNF) for global protocols is given below.

Fig. 9.

Scribble protocol (left), and its flatten form (right)

Fig. 10.

Scribble protocol (left), and its normal form (right)

The encoding of Scribble global protocols to SNF requires two auxiliary functions: and . The latter collects top level global types from a choice type, and is utilised in the encoding as to remove nested choice. The former performs one unfolding of a recursion. We demonstrate $\mathtt {flatten(G)}$ in the example in Fig. 9.

Definition 4.2

(Flatten). Given a Scribble protocol then is defined as . In all other cases, is homomorphic,

Definition 4.3

(Unfold). Given a global Scribble protocols then is defined as and homomrhic otherwise

Thus for any recursive type, unfold is the result of repeatedly unfolding the top level recursion until a non-recursive type constructor is reached. Unfold terminates given the assumption that recursive types are contractive, as in our case. Intuitively, a protocol is translated to a normal form after first unfolding all recursions once and then flattening nested choice. Figure 10 shows a Scribble protocol and its translation to its normal form, and the encoding is given in Definition 4.4.

Definition 4.4

(Encoding $\langle \rangle$ of Global Protocols to SNF)

Trace Equivalence. The definition of trace equivalence, denoted by $\approx$ is standard. We write if where is the set of traces obtained by reducing

We assume is closed, i.e does not contain free type variables, where a type variable $\mathtt{{t}}$ is bound in , and free otherwise. We extend the definition of traces for local protocols, global and local types, and we also extend $\approx$ and $\lesssim$ to local protocols, as well as global and local types, and configuration of local protocols.

Lemma 4.5

Given a global protocol then: (1) (2) ; and (3)

Proposition 4.6

(SNF Translation). Let be a Scribble local protocol, then .

4.2 From Global Protocols to Global Types

Definition 4.7

(Encoding of Global Protocols to Global Types). The encoding $\llbracket \rrbracket$   from SNF to global types is given below:

For convenience, we recall the semantics of global types in Fig. 6. The semantics of global protocols and global types are similar except that the one for MPSTs from [11] have no rule ${\scriptstyle \lfloor {\textsc {Choice}}\rfloor }$ as choice is handled directly in the rule for send/selection and branch/receive. To match Scribble global protocols and MPST step by step we extend the definition of encoding to account for intermediate steps:

Proposition 4.8

(Correspondence of Global Protocols and Global Types). Let be a Scribble global protocol, then .

4.3 From Local Protocols to Local Types

The syntactic differences between Scribble local protocols and local types (given in Fig. 5) reflect the difference between Scribble global protocols and MPST global types. We define an encoding of local protocols (Definition 3.2) to local types on the normal form of a Scribble local protocol (Definition 4.9).

Definition 4.9

(Local Scribble Normal Form (LSNF))

Local types are generated from global types following a syntactic procedure, called projection. In a similar way we define projection on global protocols. The definition of projection is given in Definition 4.10. We denote by the set of roles in a protocol .

Definition 4.10

(Projection). The projection of onto , written , is defined by induction on as follows:

If no side condition applies then is not projectable on $\mathtt {A}$ and the global protocol is not well-formed. The case for uses the merge operator to ensure that (1) the locally projected behaviour is independent of the chosen branch (i.e , for all $i, j \in I$), or (2) the chosen branch is identifiable by ${\mathtt {A}}$ via a unique label. The merge operator [11] is defined as a partial commutative operator over two types s.t.

$\textit{where for each } k \in I \cap J, \mathtt {a_k} = \mathtt {a'_k}, \mathtt {S}_k=\mathtt {S}'_k$ Merge is homomorphic for all other types (i.e , where $\mathscr {E}$ is a context for local protocols.). We say that is well-formed if for all , is defined. Note that a normal form is preserved during projection, i.e a Sribble global protocol in a normal form is projected to a Scribble local protocol in a normal form. Next we give the encoding between Scribble local protocols and MPST local types. Hereafter we write Scribble local protocol when referring to LSNF protocols.

Definition 4.11

(Encoding of Local Protocols to Local Types). The encoding from (Scribble) local protocols to MPST local types is given below:

Proposition 4.12

(Correspondence of Local Protocols and Local Types). Let be a Scribble local protocol, then .

Proposition 4.13

(Correspondence of Configurations). Let be a configuration of Scribble local protocols, then .

4.4 Correspondence of Global and Local Protocols

Theorem 4.14 gives the correspondence between the traces produced by a global protocol and those produced by the configuration that consists of the composition of the projections of .

Theorem 4.14

(Soundness of projection). Let be a Scribble global protocol and be the set of its projections, then

Theorem 4.14 directly follows by: (i) the correspondence between (Scribble) global protocols and MPSTs global types given in Sect. 4; (ii) trace equivalence between global types and configuration of projected global types (Theorem 3.1 in [11]); (iii) the correspondence between configurations of MPSTs local types and configurations of Scribble local protocols given in Sect. 4.

5 From Scribble to CFSMs

This section gives the translation of local protocols to CFSMs [4]. First, we start from some preliminary notations. $\epsilon$ is the empty word. $A$ is a finite alphabet and $A^*$ is the set of all finite words over $A$. |x| is the length of a word x and x.y or xy the concatenation of two words x and y. Let $\mathscr {P}$ be a set of participants fixed throughout the section: $\mathscr {P}=\{{\mathtt {A, B, C}},\ldots {\mathtt {p,q}},\ldots \}$.

Definition 5.1

(CFSM). A communicating finite state machine is a finite transition system given by a 5-tuple $M=(Q, C, q_0, A, \delta )$ where (1) $Q$ is a finite set of states; (2) $C\ = \{ {\mathtt {A}}{\mathtt {B}} \in \mathscr {P}^2 | {\mathtt {A}} \ne {\mathtt {B}}\}$ is a set of channels; (3) $q_0\in Q$ is an initial state; (4) $A$ is a finite alphabet of message labels, and (5) $\delta = Q\times (C\times \{!,?\}\times {A}) \times Q$ is a finite set of transitions.

Final State is a state $q \in Q$, which does not have any outgoing transitions. If all states in $Q$ are final, $\delta$ is the empty relation. A (communicating) system $\textit{S}$ is a tuple $\textit{S}=(M_{p})_{p \in \mathscr {P}}$ of CFSMs such that $M_p=(Q_p, C, q_{0_{p}}, A, \delta _p)$. We define

a configuration for $M_p$ to be a tuple where and where $w= (w_{{\mathtt {pq}}})_{p \ne q \in \mathscr {P}}$ with $w_{pq} \in A^*$.

A path in M is a finite sequence of $q_0, \ldots , q_n (n \ge 0)$ such that $(q_i, \ell , q_{i+1}) \in \delta (0 \le i \le n-1)$ and we write $q \xrightarrow {\ell } q'$ if $(q, \ell , q') \in \delta$.

Definition 5.2 gives the translation of local Scribble protocols to CFSMs. For convenience, we do not separate a label from a payload and we write $\texttt {msg}$ instead of $\mathtt {a}(\mathtt {S})$. Without loss of generality we assume all nested recursive types are given as , where . , then .

We use the auxiliary function to denote the body of a recursive term. Hence ; in all other cases . We remind that recursive variables are guarded in the standard way, i.e. they only occur under a prefix and therefore cannot be .

Definition 5.2

(Translation from local types to CFSMs). We write occurs in . Let be the normal form of the local type of participant projected from . The automaton corresponding to is where: (1) ; (2) (3) ; (4) is the set of labels in ; and (5) $\delta$ is defined below:

• 1. if , then

  

• 2. if , then

  

• 3. if , then:

  • (a)
    
  • (b)
    

Examples. We illustrate the translation with two examples, in Figs. 11 and 12. The CFSM for the local protocol from Fig. 11 (left) is . We first generate the states Q of from the suboccurrences of the initial local protocol . The states are denotes as $s_1$ and $s_2$ where and . is defined as the 5-tuple: 1) $Q = \{s_1, s_2\}$; 2) ; 3) $q_0$ = $s_1$; 4) A = ; 5) .

Fig. 11.

Scribble protocol (left) and corresponding CFSM (right)

Fig. 12.

Scribble protocol (left) and corresponding CFSM (right)

Next we consider the local type , given on Fig. 12 (left). From the suboccurrences of the local protocol we generate three states $s_1$, $s_2$, and $s_3$, where ; ; and  Then the corresponding automaton is the 5-tuple $(Q, C, A, q_0, \delta )$ where 1) $Q = \{s_1, s_2, s_3 \}$; 2) ; 3) $q_0$ = $s_1$ 4) ; 5) .

We proceed by proving operational correspondence between a local type and its corresponding . We use an auxiliary function to map recursive variables to types.

Definition 5.3

(Unfold mapping). We define a function , where is a type and is a mapping from recursive variables to types

We assume all recursive variables are distinct and also . Hence, can contain and we apply the substitution without $\alpha$-renaming.

Lemma 5.4

(Suboccurrences). Given a local protocol , with a suboccurrence and a substitution s.t ,then

Theorem 5.5

(Soundness of translation). Given a local protocol , then .

6 Conclusion and Related Work

De Nicola is the first person who proposed a location-based distributed model with rich capability types, and implemented that model in Java as to demonstrate a practical use of formal foundations for mobile computing. Following his spirits, this paper gave a formal definition of a practical protocol description language, Scribble. We proved a correspondence between Scribble and MPST and showed that a global protocol corresponds to a system of CFSMs.

The work [10] is the first to explore the connection of MPST and CFSMs. [10] gives a sound and complete characterisation of a class of communicating automata that can be expressed by the language of multiparty session types. The presented work is closely based on the translation of session types to CFSMs presented in [10], and hence we adhere to the same conditions as theirs, namely the CFSM is deterministic and directed without mixed states (each state is either sending or receiving to the same participant with distinct labels). Lange et al. [20] presents an algotithm for synthesising global graphs from local multiparty specifications, given as CFSMs, that allows more general constructs, such as fork and join. Scribble currently does not support such constructs. The correspondence of MPST and CFSMs with time constraints is further explored in [2, 3]. The work [21] uses the result in [3] to implement a runtime monitor based on an extension of Scribble with time annotations, but the work does not prove formal correspondence between timed Scribble and timed automata.

The encoding of Scribble protocols to CFSMs presented in this article is an important basis when building and verifying distributed systems. It guarantees that global safety properties can be ensured through local, i.e, decentralised verification. The setting defined by CFSMs does not require synchronisation at runtime. Therefore our approach is more efficient to implement than a centralised approach. In [9, 17], we rely on this result to design and build a sound Scribble-based framework for runtime and hybrid verification.

Several implementation works use the Scribble toolchian and the local CFSM representation to generate APIs for programming distributed protocols [18, 22]. In recent years, Scribble-based code generation has been extended with various contructs, e.g. parameterised role [5] for distributed Go programming, delegation in Scala [25], time constarints in Python [3], explicit connections [19] for dynamic joining of roles in Java, and payload constraints in F# [22]. The above mentioned works are either practical (hence no formal semantics nor operational correspondence results are given) and/or informally rely on the correspondence between MPST and Scribble as to justify the soundness of their respective implementations and extensions.

Future work includes formalisations of extended Scribble in the literature explained above. In particular, there exists no operational semantics of multiple multiparty session types with delegations and higher-order code mobility since a single system of CFSMs corresponds to a single multiparty session type with fixed participants. We plan to tackle this problem first extending CFSM models from a fixed set to a family of participants.

Appendices

A Scribble Normal Form

Proposition 4.6 (SNF Translation): Let be a Scribble local protocol, then .

Proof. First we consider . The proof is mechanical and is done by induction on the transition rules applied for closed terms of .

• 1. (base case) If then both and produce an empty set of traces and no rules can be applied.

• 2. (inductive case) if then such that .

  • (a) if

    can do ${\mathtt {A}}{\mathtt {B}}!\texttt {msg}$ or $\ell$ by ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ or ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$ respectively.

    Then follows by the induction hypothesis (IH) and by the definition of encoding

  • (b)

    By

    By IH s.t

    By Lemma 4.5

    

    Thus, s.t

    By

    By Lemma 4.5

  • (c)

    From with

    From IH s.t From it follows that

    s.t

    From ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ it follows

Now we consider . The proof is by induction on the definition of encoding of closed terms of .

• 1. (base case) If then both and produce an empty set of traces and no rules can be applied.

• 2. (inductive case) if then such that .

  • (a)

    can do or $\ell$ by or respectively.

    Then follows by the IH and by the definition of encoding

  • (b)

    From IH:

    Thus, if

    then s.t

    From rule:

  • (c) = From with

    By Lemma 4.5 it follows that

    s.t

    From IH it follows that s.t .

B From Global Protocols to Global Types

Proposition 4.8 (Correspondence of Global Protocols and Global Types): Let be a Scribble global protocol, then .

Proof. First, we consider . The proof is done by induction (on the depth of the tree) on the transition rule applied.

• 1. (Base case) If then both and produce an empty set of traces.

• 2. (Inductive case) if and we have to prove that .

• if then we either have a send action by ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ or $\ell$ transition by ${\scriptstyle \lfloor {\textsc {ASYNC1}}\rfloor }$

  • 

    By (1) and

    (2) and

    (3) :

    we have

  • 

    By (1) and By (2) , which follows from the premise of the ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$ and by IH and (3) , which follows from the premise of ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$:

    we can apply the ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }_{MPST}$ rule:

• if

  We proceed as in the above case. We either have a receive action by the rule ${\scriptstyle \lfloor {\textsc {recv}}\rfloor }$ or $\ell$ transition by the rule ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }$.

  • where

    By (1) and and

    (3) ${\scriptstyle \lfloor {\textsc {branch}}\rfloor }_{MPST}$:

    therefore

  • where

    By (1) and By (2) , which follows from the premises of the ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$ and by the induction hypothesis and

    (3) ${\mathtt {A}}, {\mathtt {B}} \not \in subj(\ell )$, which follows from the premise of ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }$:

    we can apply the ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }_{MPST}$ rule:

• if

  By ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ we have where by the rule premise we have for that

  which brings us back to the first case.

• if the thesis directly follows by induction since

  (1) by where

  (2)

  By

  (3) From IH, and therefore

Now we consider .

The proof is done by induction on transition rules applied to the encoding of .

• 1. then both and then no rules can be applied.

• 2. if , then we either have a send action by ${\scriptstyle \lfloor {\textsc {select}}\rfloor }_{MPST}$ or $\ell$ transition by ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$.

  • 

    By and and it follows that

  • where

    and

    By (1) the rule premise and by (2) IH it follows that .

    Given also that ${\mathtt {A}}, {\mathtt {B}} \not \in subj(\ell )$, we can apply ${\scriptstyle \lfloor {\textsc {async1}}\rfloor }$. Thus,

• 3. if

  Then by ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ we have that when for $i \in I$.

  Thus, we have to prove that

  if then , which follows from a).

• 4. if can do a receive action by ${\scriptstyle \lfloor {\textsc {branch}}\rfloor }_{MPST}$ or $\ell$ transition by ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }$.

  • 

    By and

    and it follows that

  • where

    and

    By (1) the rule premise and by (2) IH it follows that .

    Given also that ${\mathtt {A}}, {\mathtt {B}} \not \in subj(\ell )$, we can apply ${\scriptstyle \lfloor {\textsc {async2}}\rfloor }$. Thus,

• 5. if the thesis directly follows by induction.

C From Local Protocols to Local Types

Proposition 4.12 (Correspondence of Local Protocols and Local Types): Let be a Scribble local protocol, then .

Proof.

First, we consider .

The proof is done by induction (on the depth of the tree) on the transition rule applied.

• 1. (Base case) If then both and produce an empty set of traces.

• 2. (Inductive case) and we have to prove that . We proceed by case analysis on the structure of

  • (a) if by ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$

    by ${\scriptstyle \lfloor {\textsc {LSel}}\rfloor }$

  • (b) if by

    by ${\scriptstyle \lfloor {\textsc {LBra}}\rfloor }$

  • (c) if

    Depending on the structure of , this case folds back to previous cases a) and b).

    if then by

    if then by ${\scriptstyle \lfloor {\textsc {LBra}}\rfloor }$

  • (d) if the thesis directly follows by induction.

Now we consider .

The proof is done by induction on transition rules applied to the encoding.

• 1. (Base case) If then both and produce an empty set of traces.

• 2. (Inductive case) and we have to prove that . We proceed by case analysis on the structure of

• if

  by ${\scriptstyle \lfloor {\textsc {LSel}}\rfloor }$

  by ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$

• if

  by ${\scriptstyle \lfloor {\textsc {Lbra}}\rfloor }$

  by ${\scriptstyle \lfloor {\textsc {recv}}\rfloor }$

• if

  

  By ${\scriptstyle \lfloor {\textsc {recv}}\rfloor }$ and the structure of we have that and therefore we can apply ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$

  Thus,

• if the case is analogical to the previous one.

• if the thesis directly follows by induction.

Proposition 4.13 (Correspondence of Configurations): Let be a configuration of Scribble local protocols, then .

Proof. The proof is by induction on the number of transition steps.

Inductive hypothesis:

Now we want to prove that if then

We do a case analysis on the transition label $\ell$:

(1) if $\ell = {\mathtt {A}}{\mathtt {B}} ! \mathtt {a}\langle \mathtt {S}\rangle$

By and Proposition 4.12 it follows:

By definition of configuration of local protocols:

.

(2) if $\ell = {\mathtt {A}}{\mathtt {B}} ? \mathtt {a}\langle \mathtt {S}\rangle$

By

By definition of configuration of local protocols:

$w'_{{\mathtt {A}}{\mathtt {B}}}=w_{{\mathtt {A}}{\mathtt {B}}}\cdot \mathtt {a}(\mathtt {\mathtt {S}})\wedge (\Rightarrow w_{ij}=w'_{ij})_{ij\not = {\mathtt {A}}{\mathtt {B}}}$

In (1) and (2) we have by definition that , which by the inductive hypothesis implies that

Then by the definition of configuration of local protocols (from (1) and (2)) it follows that .

D From Sribble to CFSM

Lemma 5.5 (Soundness of the translation). Given a local protocol , then .

Proof. In the proof we assume . Also we assume . When the lemma is trivially true since produces an empty set of traces, is an empty relation and $q_0$, the initial state, is also a final state.

First, we consider . Next we prove that if then such that and , and .

The proof is by induction on the transition relation for local types. In all cases we assume that .

• ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ if the reduction is by ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ we have

  .

  Thus, where $\ell = \texttt {msg}!{\mathtt {A}}{\mathtt {B}}$.

  Since we proceed by case analysis on .

  Case 1:

  By Definition 5.2(1-2) and .

  Case 2:

  We have that , where .

  By ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ we have .

  By Definition 5.2(1-1) and it follows that

  with .

  By Lemma 5.4 we have and we conclude the case.

• ${\scriptstyle \lfloor {\textsc {recv}}\rfloor }$ is similar to Case ${\scriptstyle \lfloor {\textsc {send}}\rfloor }$ and thus we omit.

• ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ if the reduction is by ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ we have

  .

  Case 1: if has the shape

  then we have for some $j \in I$ with $\ell = \texttt {msg}_j!{\mathtt {A}}{\mathtt {B}}$.

  Since = , we proceed by case analysis on .

  Case 1.1:

  By Definition 5.2(3-a-2) and = we have .

  Case 1.2:

  • (1*) We have that , where .

  • (2*) By ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$ we have .

    By Definition 5.2(3-a-2) and

    with .

    By Lemma 5.4 we have .

  Applying the IH to (1*) and (2*) we conclude the case.

  Case 2: if has the shape

  this case is similar to Case 1 and thus we omit.

  Note that since the normal form of local types does not allow for unguarded choice, hence, all possible transitions of are the transitions from Case 1 and Case 2.

• ${\scriptstyle \lfloor {\textsc {rec}}\rfloor }$ if the reduction is by ${\scriptstyle \lfloor {\textsc {rec}}\rfloor }$ we have then . We note that does not contain the term since unguarded recursive variables are not allowed. Hence, is either send, receive or choice and by IH and , , we conclude this case.

We next consider . We prove that given a local protocol if then s.t. and and with . We proceed by case analysis on the transitions in $\delta$.

Case 1: and $\ell = \texttt {msg}?{\mathtt {A}}{\mathtt {B}}$.

Then and we have by .

Case 1.1: if

The hypothesis follows from .

Case 1.2: if

By Definition 5.2 .

By Definition 5.3 and Lemma 5.4 we have .

From IH and we conclude the case.

Case 2: and $\ell = \texttt {msg}!{\mathtt {A}}{\mathtt {B}}$.

Proceeds in a similar way as Case 2 and thus we omit.

Case 3:

Then we have by ${\scriptstyle \lfloor {\textsc {choice}}\rfloor }$

for some $j \in I$.

Case 3.1: if

From IH and we conclude the case.

Case 3.2: if

By Definition 5.2

By Definition 5.3 and Lemma 5.4 we have s.t. .

We have that , hence we conclude the case.

Case 4:

Proceeds in a similar way as Case 3 and thus we omit.

Case 5:

Note that the is either message send or message receive. Hence, By applying the IH and Case 1, 2 we conclude the case.