Featherweight Scribble

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.

We thank the reviewers for their comments. This work is par- tially supported by EPSRC projects EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1 and EP/N028201/1. The first author was supported by an EPSRC Doctoral Prize Fellowship.

Authors and Affiliations

1. Brunel University London, London, UK

   Rumyana Neykova

2. Imperial College London, London, UK

   Nobuko Yoshida

Corresponding author

Correspondence to Nobuko Yoshida .

Editors and Affiliations

1. Department of Statistics, Computer Science, Applications, University of Florence, Florence, Italy

   Michele Boreale

2. School of Science and Technology, University of Camerino, Camerino, Italy

   Flavio Corradini

3. School of Science and Technology, University of Camerino, Camerino, Italy

   Michele Loreti

4. Department of Statistics, Computer Science, Applications, University of Florence, Florence, Italy

   Rosario Pugliese

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. 1.

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

2. 2.

   (inductive case) if then such that .

   1. (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

   2. (b)

      By

      By IH s.t

      By Lemma 4.5

      

      Thus, s.t

      By

      By Lemma 4.5

   3. (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. 1.

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

2. 2.

   (inductive case) if then such that .

   1. (a)

      can do or \(\ell \) by or respectively.

      Then follows by the IH and by the definition of encoding

   2. (b)

      From IH:

      Thus, if

      then s.t

      From rule:

   3. (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. 1.

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

2. 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. 1.

   then both and then no rules can be applied.

2. 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. 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. 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. 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. 1.

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

2. 2.

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

   1. (a)

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

      by \({\scriptstyle \lfloor {\textsc {LSel}}\rfloor }\)

   2. (b)

      if by

      by \({\scriptstyle \lfloor {\textsc {LBra}}\rfloor }\)

   3. (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 }\)

   4. (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. 1.

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

2. 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. (1*)

     We have that , where .

  2. (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.

Reprints and permissions

© 2019 Springer Nature Switzerland AG

Policies and ethics