MAG$π$!: The Role of Replication in Typing Failure-Prone Communication
Matthew Alan Le Brun Ornela Dardha




!





M. A. Le Brun and O. Dardha

University of Glasgow, Glasgow, UK

{matthewalan.lebrun,ornela.dardha}@glasgow.ac.uk

!: The Role of Replication in Typing Failure-Prone Communication
    Matthew Alan Le Brun Ornela Dardha
    April 29, 2024
================================================================





 is a Multiparty, Asynchronous and Generalised π-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. 

Its type system guarantees that all possible message-loss is handled by timeout branches. 

In this work, we argue that the previous is unnecessarily strict. 

We present !, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). 

Replication is a standard π-calculus construct used to model infinitely available servers. 

We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. 

We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification.









§ THE TALE OF THE MAG(PIE/Π)


The magpie is a bird with deep ties to British folklore. 

The first known mention of their counting for fortune telling dates back to 1780, where John Brand writes what is thought to be one of the original versions of the magpie rhyme <cit.>:



    “One for sorrow, Two for mirth, Three for a funeral, And four for a birth.”



We can imagine that the natural reaction of a person who spots a solitary magpie is to scan the surrounding area for its companion.

Alas, if no one is immediately visible, the person desperately waits—hoping a second magpie comes their way.

But how long should one wait? 

The reality is that it is impossible to know the difference between no magpie and a magpie that has not yet arrived.

To computer scientists, this is a well known impossibility result <cit.>.

In the study of distributed systems and fault tolerance, mechanisms must be employed to approximate the impossibility result of determining whether a message has been lost or delayed— by using a timeout.

Hence, the computer scientist who spots a lonely magpie knows to only wait some fixed amount of time before assuming that no other magpie is coming and accepting their sorrowful faith.

This philosophy is the core principle of the process calculus  <cit.>, a language designed to model communication failures (via message loss) with a generic type system aiming to provide configurable runtime guarantees.


 is a Multiparty, Asynchronous and Generalised π-calculus, modelling distributed communication over n-participant sessions. 

Its key features include non-deterministic failure injection into the runtime of a program, asynchronous communication via bag buffers (allowing for total message reordering), and a generic type system capable of providing guarantees of runtime properties via session types.

Session types <cit.> are behavioural type systems allowing for formal specification of communication protocols—their main benefit being that they provide correctness guarantees on both protocol design and implementation.

Multiparty session types (MPST) <cit.> are a branch of session type theory that aims to support protocols involving any number of participants with interleaving communication.

 builds upon a generalised form of MPST <cit.>, where protocols are defined by a collection of local types—the communication patterns of individual participants' perspectives—which should be exhaustively checked ( via model checking) to determine any properties they observe.

Novelties of  stem from how it embraces the impossibility result of distinguishing between dropped or delayed messages; its language and type system use non-deterministic timeouts to model the assumption of failures.

The type system guarantees that all failure-prone communication is handled by a timeout branch.

In this work, we argue that the previous approach can, in some scenarios, be unnecessarily strict—resulting in needlessly more complex protocols.

Some configurations may wish to leave the handling of failures up to senders, as opposed to recipients; these usually take the form of client-server interactions where servers are designed to remain infinitely available.

 if a request to a web-server were to drop, it is the client's responsibility to re-issue that request.

We present an extension to  that better models infinitely available servers and simplifies failure-handling for client-server interactions.


In the π-calculus <cit.>, a standard construct often used for representing infinite behaviour is that of replication.

A replicated process is one which can be informally described as infinitely available.

Naturally, the use of replicated processes lends itself well to the modelling of client-server interactions.

We demonstrate how the use of replication in  can, not only better model infinitely available servers, but also simplify their protocols by relaxing the requirement of failure-handling branches from every receive to only linear receives.

[Type-level replication]
We evolve the motivating example presented in <cit.>, the ping protocol.

Consider three participants: client ,  server , and result channel .

Communication between  and  is reliable; whereas with  is unreliable.

The session types for a three-attempt ping in ! are:

    [                                                                                                                                                      _                                                                                                                                          = &{ : ,  : };                                                                                                                                                      _ = ø  : &{[                                                             : ø : ,; ø : &{[                     : ø : ,; ø : &{[ : ø : ,;     ø : ]. ]. ].;                                                                                                                                                      _                                                                                                                                              = ! : ø : ]


Client  sends a message with label  to server  (ø  :) and waits for a  response (& :).

If successful, an  message is sent to results role  and the session is terminated for the client ().

Since communication with the server is unreliable, receipt of the  message is not guaranteed, and must be handled by a timeout branch .

The client attempts to reach the server 3 times—if all attempts fail, it sends a  message to .

The result role  waits for either of the reliable responses from , thus no timeout is defined.

Server  is defined as the replicated receive ! : ø :, denoting its constant availability to receive a  request and send a  response.

We highlight the absence of a failure-handling timeout branch in _; the server does not need to change its behaviour if a client request fails.

Furthermore, if the  reply fails, the server remains available to handle any number of retries from the client.

Thus, the use of replication has offloaded the handling of failures entirely onto the client-side, has made the protocol more modular (since the type for  is now agnostic of a client's retry limit), and is simpler  to the original specification in  (a full comparison is made in <ref>).







  §.§.§ Contributions.
 
Concretely, our contributions are as follows:

    
  * ! Language:
    
    We present ! (<ref>), an extension of  that does away with recursion in favour of replication as a better means of modelling client-server interactions.
    
    
    
  * ! Types:
    
    We lift replication to type-level in <ref>.
    
    To the best of our knowledge, this work serves as the first introduction of replication into MPST.
    
    We improve upon the theory of  and show how three type contexts (unrestricted, linear and affine) can be used to type—and simplify—failure-prone communication in client-server interactions.

    
  * ! Meta-Theory:
    
    <Ref> expounds upon the meta-theory of our type system.
    
    We prove subjection reduction and session fidelity, and demonstrate how they can be used for property verification.
    
    ! provides a failure handling guarantee, ensuring all failure-prone communication is handled by a timeout branch—a responsibility which servers offload to clients.


In <ref> we conclude and give an account of related and future work.




  §.§.§ On delegation and language simplification.


This work builds upon a subset of  <cit.> as our language only considers communication over a single session.

Reasons for this are: 

[label=(*)]
    
  * to simplify notation for better readability due to limited space; and
    
  * to remove session fidelity assumptions.


On the latter, generalised MPST theory assumes communication over a single session to prove session fidelity (a.k.a. protocol compliance) <cit.>.

This is to remove deadlocks that can occur due to incorrect interleaving of multiple sessions.

Effectively, the language subset we consider syntactically abides by the assumptions of session fidelity by assuming all communication happens over a single session and by removing delegation.

We foresee no issues with extending ! to multiple sessions, although this will only improve the number of safe protocols that can be expressed and has no effect on verification of other properties.

Lastly, replication in ! is a top-level construct only.

This simplifies our type-system at the cost of sacrificing expressivity of nested replication.

The type system can still express meaningful examples ( load balancers), and we intend to explore hidden and nested replication in future work.



§ BIRD SONGS


We present !, an extension of  that replaces recursion with replicated processes as its preferred means of reasoning about infinite behaviour.

Programs in ! represent distributed networks, consisting of concurrent and parallel processes running on machines connected over some failure-prone medium.

We discuss how networks of various topologies are defined in <ref>.

<Ref> details the syntax and semantics of processes.




 §.§ Topology


Distributed protocols typically consist of a number of participants (or roles) representing physically separated devices, communicating over a failure-prone network.

We model such a setting by associating processes to uniquely identifiable roles, which communicate asynchronously through a bag buffer allowing for total message reordering.

Roles are related through a notion of reliability, modelling physical locations of processes— reliable roles are ones that live on the same physical device and thus are not susceptible to communication errors.

A formal account of networks, buffers and reliability is given below.




  §.§.§ Networks.


A program in ! models some distributed network .

These networks consist of a parallel composition of processes, each representing specific roles in the network.

The formal description of a network is given by <ref>.


    A network  is given by the following grammar:
    
    ::= 𝒫||

    where  is a message buffer; 𝒫 is the process instruction; and  is a role name.


A process 𝒫 consists of a uniquely identifying role name , and process instructions 𝒫.

It is key to note that all processes,  participants, of a network are syntactically defined—thus, ! assumes a finite network size where all participants are statically known.

The  constructor denotes parallel composition of processes within a network, and  is its message buffer.



  §.§.§ Buffers.


! models asynchrony through a bag buffer (semantics discussed in <ref>).

The buffer, <ref>, serves two purposes.

Firstly, it allows for non-blocking (fire and forget) sends by acting as an intermediary where messages wait until recipients are ready to consume them.

Second, and important to distributed communication, is that it models messages in transit over the network and is thus the point-of-failure in our system.



    A message  is defined as ::= ⟨p→q, ⟨ṽ⟩⟩,  a tuple identifying the source and destination of the message (p→q), along with a message label and payload contents (⟨ṽ⟩).
    
    A buffer  is a multiset of messages .
    
    Concatenating a message  with a buffer , written  corresponds to the multiset sum of + {}.





  §.§.§ Reliability.


A network is initialised with a reliability relation  (<ref>),

defining roles which may communicate sans failure.

All communication outwith the reliability relation is considered failure-prone; 
this may be used to simulate physical topologies, or to study a protocol at various degrees of reliability.


    Given a network , and set of roles ρ acting in ,
    the reliability relation  is a subset of (or equal to) {{,} : ,∈ρ  ≠}.
    
    We write :: to denote a network  governed by reliability relation .
    
    We use shorthand :: to denote a fully reliable network, and :: ∅ to denote a fully unreliable network. 
    


[Load Balancer: Network]
    Consider a load balancer network with server s, workers w_1, w_2, and client c.
    
    Assuming server-worker communication to be reliable, the network may be configured as below:
    
    
    s𝒫_𝓈w_1𝒫_𝓌_1w_2𝒫_𝓌_2c𝒫_𝒸 :: {{ s, w_1}, { s, w_2}}






 §.§ Processes



    The syntax for defining process instructions 𝒫 is given by the following grammar:
    
    𝒫   ::= !_i ∈ Ip_i : _i (x̃_̃ĩ)  P_i |𝒫𝒫| P
    
            P       ::= |&_i ∈ Ip_i : _i (x̃_̃ĩ)  P_i [,  P^'] |ø  : ⟨c̃⟩ P
    
            c       ::= x | v
             
            v ::= basic values


    All branching terms assume I ≠∅ and all couples p_i : _i to be pairwise distinct. 
    
    Receiving constructs act as binders on their payloads.
    


A process 𝒫 can either be a replicated server or a linear process.

Replicated receive !_i ∈ Ip_i : _i (x̃_̃ĩ)  P_i denotes a server constantly available to receive any of a set of messages from roles p_i with labels _i.

The received payload is bound to x̃_̃ĩ before pulling out a copy of P_i to run in parallel with the server.

Parallel composition  is a runtime only construct at the process-level.

It is used to denote composition of linear continuations pulled out of a replicated receive.

Linear processes (P, Q, …) consist of:

[label=(*)]
    
  * the empty process ;
    
  * linear receives &_i ∈ Ip_i : _i (x̃_̃ĩ)  P_i [,  P^'], where a role waits for one of a set of messages from some other roles p_i with labels _i, binding the received payload to x̃_̃ĩ before proceeding according to P_i; 
    
  * an optional nondeterministic timeout branch [,  P^'] attached to linear receives to handle possible failure of messages, instructing the process to proceed according to P^'; and
    
  * linear sends ø  : ⟨c̃⟩ P which sends a message towards  with label  and payload c̃ before continuing according to P.


A payload c is either a variable (x,y,…) or some assumed basic value (integers, reals, strings, …).

We omit conditional branching constructs such as if-then-else and case statements as they are routine and orthogonal to our work (we assume them in examples).






    Reduction on networks is parametric on a reliability relation . 
    
    The reduction relation  is inductively defined by the rules listed in <ref>, up-to congruence (<ref>).


Network dynamics (<ref>) are divided into process and failure semantics.

A process sends a message via rule <ref>, which places the message in the network buffer and advances the sending process to its continuation.

Conversely, processes receive messages (rule <ref>) by consuming a message from the buffer, advancing the process to its continuation and substituting bound payloads with the received data.

In a similar manner, servers may consume messages from the buffer using rule <ref>; instead of advancing the process, a copy of its continuation is pulled out and placed in parallel.

This allows servers to concurrently handle and receive client requests.


Message failure is modelled through rule <ref>.

We recall that buffers model messages in transit, thus this rule may—at any time—drop a message from the buffer if it is unreliable.

It is key to note that failure in these semantics is nondeterministic.

A client may consume a message before it is dropped, representing a successful transmission; or the message may be dropped before consumed, representing the failure case.

Reduction of timeout branches is also nondeterministic since it is impossible to distinguish between dropped messages (no magpie) and delayed messages (the magpie that has not yet arrived).

Therefore, rule <ref> can at any time reduce a waiting process to its timeout branch, modelling either the handling of message failure or an incorrect assumption of failure ( message delay).


[Load Balancer: Processes]
    We present the processes of our load balancer. 
    
    An output role o, which is reliable  the client, has been added.
    
    
    s   !c : req(x) {[ →øw_1 : req⟨ x⟩; →øw_2 : req⟨ x⟩ ].  
    w_1   !s : req(d) øc : ans⟨ f(d)⟩
    w_2   !s : req(d) øc : ans⟨ f(d)⟩
    c   øs : req⟨ 42 ⟩&{[ w_1 : ans(y) øo : output⟨ y ⟩; w_2 : ans(y) øo : output⟨ y ⟩; øo : err⟨“Request timed out”⟩ ]. 
    o   &{c : output(out) , c : err(msg) }



[Interactions with Failure: Processes]
    Now we demonstrate interactions unique to our language which result from the use of timeouts as imperfect failure detectors.
    
    Consider the following network snippet _f :: ∅:
    
    
    ø  : ⟨ 42 ⟩ P  &{ : (x)  P^',  P^''}  {“Life is”}


    These processes denote communication between two roles ( and ), where a message labelled  with the string “Life is” has already been sent, and a second message also labelled  is to be sent with payload 42.
    
    There are four possible immediate reduction steps for this network: 
    [label=(*)]
        
  * role  consumes the message in the buffer via <ref> (the intended behaviour);
        
  * role  places message 42 in the buffer via <ref>, this may possibly result in message reordering due to the bag buffer semantics;
        
  * message “Life is” is dropped from the buffer via <ref>, then  may either correctly assume failure through a timeout, or if the sender is quick enough the message 42 could still be received in its place; and 
        
  * role  can incorrectly assume a failure and timeout via <ref> even though message “Life is” is in the buffer.
    
    
    It is not difficult to see how <ref> may lead to errors.
    
    Our types and meta-theory mitigate the occurrence of these possibly unsafe networks by enforcing a safe design of protocols.




§ HARMONISATION


We now present the multiparty, asynchronous, and generalised type system for !.

To the best of our knowledge, this is the first work to introduce replication and parallel composition for local types in MPST.

We show how these constructs lend themselves well to typing distributed client-server interactions.



 §.§ Types


The syntax for ! types are given in <ref>.

Our type system does away with tail-recursive binders (as is standard in MPST), instead opting for a replicated receive type.

The syntax distinguishes between different classes of types.

Namely, we present replicated-, session-, message- and basic-types—each of which are used differently by the type contexts (<ref>).


    The syntax for ! types is given by:
    
    R   ::= !_i ∈ Ip_i : _i (B̃_̃ĩ)  S_i
    S   ::= ø_i ∈ Ip_i : _i (B̃_̃ĩ)  S_i|&_i ∈ Ip_i : _i (B̃_̃ĩ)  S_i  [, S^']|S  S|
    M   ::= (→, (B̃))
    B   ::= Int, Real, String,… (basic types)


    Branching constructs assume I ≠∅ and couples p_i : _i to be pairwise distinct.
    
    Replicated types R assume a pool of labels distinct from their continuations.


A replicated type R defines the protocol of a server.

Type !_i ∈ Ip_i : _i (B̃_̃ĩ)  S_i denotes the receipt of requests labelled _i from p_i carrying payload types B̃_̃ĩ having continuation types S_i.

Replicated types never appear guarded and always have linear continuations.


Session types S describe the protocol of a linear process.

The selection and branching types (ø and &) detail possible sends and receives, indicating direction and content of payloads.

Branching types may optionally include a failure-handling timeout branch S, where S details the protocol to employ upon assuming a failure.

As in processes, types also have a notion of runtime only parallel composition, identifying the protocols of continuations pulled out of a replicated receive.

The  type denotes termination of a party's protocol.


Message types M are used to type messages in a buffer. 

They record the direction of communication, as well as the chosen branching label and types of its payload.

Lastly, B represents a range of assumed basic types.





    Context Γ is unrestricted and maps variables to basic types and roles to replicated types.
    
    Context Δ is linear and maps roles to session types.
    
    Context Θ is affine and holds a multiset of message types M.
    
    Γ ::= ∅| : R, Γ| x : B, ΓΔ ::= ∅| : S, ΔΘ ::= {M_1,…,M_n}


    Updating and splitting operations are defined for Δ by the rules in <ref>.
    
    Context composition Γ, (resp. Δ,) is defined iff (Γ) ∩() = ∅ (resp. (Δ) ∩() = ∅).


<Ref> defines two relations on Δ.

Context addition joins two contexts by performing a union on their contents (in the case  that there are no conflicts in their domains).

If their domains are not unique, then the types are placed in parallel, indicating a role employing multiple active session types (this is explained in more detail after introducing context reduction  <ref>).

Context splitting extracts a piece of a larger context.

Notably, types placed in parallel may be split using this operation; in other cases splitting functions similar to context composition.





    An action α is given by
    
    
    α ::= ||p


    read as (left to right) output, communication, and timeout.
    
    Context transition α is defined by the Labelled Transition System (LTS) in <ref>.
    
    Context reduction ΓΔΘΓ is defined iff ΓΔΘαΓ for some α.
    
    We write ΓΔΘ iff ∃, s.t. ΓΔΘΓ; and ^* for its transitive and reflexive closure.


Context reduction (<ref>) models type-level communication by means of the LTS in <ref>.

Transition <ref> allows a role  with a defined timeout to transition to the timeout continuation by firing a p action.

Transition <ref> is a synchronisation action between a selection type and the type buffer Θ.

Effectively, a role with a send type can transition to its continuation by firing any of the paths indicated in the selection (q_k_k) and adding the message into the buffer context.

On the receiving end, a role with a branch type can consume a message from the type buffer to model a communication action via transition <ref>.

Communication with replicated servers is handled seperately by transition <ref>.

This rule allows a communication action to be fired when a replicated type in Γ can receive a message in the buffer.

This transition has no effect on Γ (since it is an unrestricted context) and instead updates the linear context Δ with the continuation of the replicated receive.

This is why types require runtime parallel composition, and context updating and splitting operations (<ref>), as multiple requests may be made to a replicated receive.




 §.§ Typing Rules


Protocols defined in ! types are used in type judgements (<ref>) to check whether network implementations conform to their specifications.


    Type contexts are used in judgements as ΓΔΘ⊢, inductively defined by the rules in <ref>.
    
    To improve readability, empty type contexts are omitted from rules.



    A context Δ is -typed, by:
    
    end∀ i ∈ 1..n :  _i = (p_1 : S_1·…·p_n : S_n)







Typing rules <ref>, <ref>, <ref> are auxiliary judgements typing linear roles, variables and values.

A role  of type  is typed by a linear context containing exactly a mapping of  to ; 
variables are typed to a basic type if that mapping is held by Γ; and
values are typed to a basic type if they belong to their sets.

The empty process  is typed by <ref> if the linear context is -typed (<ref>),  Δ only contains roles mapped to .


The send process q_kø_k ⟨ c_1,…,c_n ⟩ P is well typed by <ref> if: 
Δ can map  to a selection type containing the path chosen by the process; Γ verifies all payloads with their types indicated in the session type; and the continuation type can check the continuation process.


The receive process &_i ∈ Iq_i : _i (y_i_1,…,y_i_n)  P_i [,  P^'] is well typed by <ref> if:
Δ maps  to a branch with all the same paths contained in I; the payloads and continuation types of every path in the branch can type all process continuations P_i; and if a timeout process P^' is defined, then it must be typed under a timeout branch in the session type.


Replicated receive !_i ∈ Iq_i : _i (y_i_1,…,y_i_n)  P_i is typed using <ref> in a similar manner to <ref>; the type of  instead lives in the unrestricted context.


Network composition is typed by <ref> and <ref>.

The former separates the linear context to be used on processes and the buffer context to be used on the network buffer; the latter splits context domains to type different roles in the network.

Process-level composition is typed via <ref> which utilises the context splitting operation (<ref>) to separate parallel session types.


Network buffers are typed by repeated applications of <ref>, which removes messages from the buffer one at a time if they match a message type in the type buffer.

The empty buffer is typed under <ref>, allowing for possible leftover types in Θ. 

It is key to note that the buffer context is affine, as any message that gets dropped at runtime will result in an unused message type.


[Interactions with Failure: Types]
    Due to the generalised nature of the type system, the type judgement alone is not enough to detect the errors that may occur in _f.
    
    This is because the type-system does not provide syntactic guarantees, but rather should be used in conjunction with exhaustive verification techniques post protocol design (this is standard in generalised MPST <cit.>).
    
    In fact, network _f can be typed under the following contexts:
    
    
    Γ : ø  : (ℕ)  S,  : &{ : (String)  S^',  S^''}Θ(→, (String))


    for some Γ, Θ, S, S^', S^'' assuming that P, P^' and P^'' are well typed using S, S^' and S^'' respectively.
    
    Note that Γ and Θ can be non-empty since the former is unrestricted and the latter is affine. 
    
    In contrast, the linear context must be exactly as stated above.
    
    We now need a way to determine this protocol as unsafe. 




§ SONGS ABOUT SONGS


Unlike most session type theories, generalised MPST do not syntactically guarantee any properties on the processes they type.

Rather, they provide a framework for exhaustively checking runtime properties on the type context, from which process-level properties may be inferred.

This seemingly unconventional approach to session types was discovered to be more expressive than its syntactic counterpart  the amount of well-typed programs it can capture <cit.>.

Furthermore, its generalised nature allows for fine-tuning based on specific requirements of its applications.

Informally, generalisation of the type system works by proving the meta-theory parametric of a safety property;  all theorems proved and presented assume that the type contexts are safe (<ref>).

With this assumption we present our main results in <ref>.




 §.§ Type Safety


The technical definition of safety refers to the minimal requirements on types to guarantee subjection reduction ( <ref>, <ref>). 

But what does safety even mean for a distributed network with message loss, delays and reordering?

It is impossible for our type system to adopt standard notions of safety which may guarantee properties such as no unexpected messages or correct ordering of messages, since the failures experienced at runtime can mitigate such guarantees.

Hence, the minimal guarantee of safety (<ref>) in ! ensures that: 

    
  * timeout branches are always (and only) defined for failure-prone communication between linear processes; and
    
  * if a message eventually reaches its destination, then the expected types of the payload from the recipient should match the data carried on the message.




    _ is a safety property on contexts iff:
    
    flushleft
        -r_1safe-r1
        _(ΓΔ: &_i ∈I q_i : _i (B̃_̃ĩ) S_iβ)   implies   ∀i ∈I : {q_i, } ∈

        -r_2safe-r2
        _(ΓΔ: &_i ∈I q_i : _i (B̃_̃ĩ) S_i, S^'β)   implies   ∃k ∈I : {q_k, } ∉
        
        -csafe-c
        _(ΓΔ: &_i ∈I q_i : _i (B̃_̃ĩ) S_i [, S^']β(q_k →, _k(B̃^̃'̃))) 

 and  k ∈I   implies   |B̃_̃k̃| = |B̃^̃'̃|  and  ∀j ∈1..|B̃_̃k̃| : B_k_j = B^'_j 

        -!csafe-!c
        _(Γ, : !_i ∈I q_i : _i (B̃_̃ĩ) S_iΔβ(q_k →, _k(B̃^̃'̃))) 

 and  k ∈I   implies   |B̃_̃k̃| = |B̃^̃'̃|  and  ∀j ∈1..|B̃_̃k̃| : B_k_j = B^'_j 

        -safe-r
        ∀: _(ΓΔβ)  and  ΓΔβ Γ   implies   _(Γ)
    



Conditions <ref> and <ref> ensure that timeouts are only omitted (resp. defined) when communication is reliable (resp. unreliable).

<ref> and <ref> require payload types to match for any communication; note that no message is ever incorrectly delivered to a linear channel instead of a replicated (and ) because we assume that message labels for replicated receives are not reused in their continuations.

The last condition, <ref>, requires all possible reductions of safe contexts to also be safe.



[Interactions with Failure: Safety]
    The type contexts presented in <ref> do not abide by the conditions of _∅ and thus are not safe.
    
    The types do meet conditions <ref> to <ref>, but fail <ref>.
    
    We observe the following traces of the LTS:

    
        (s)  at (0,0)                        ·;
        (r1) at (3,1.5)  [anchor=west] Γ : ø  : (ℕ)  S,  : S^'Θ;
        (r2) at (3,0)    [anchor=west, text width=7.2cm] Γ ;  : S,  : &{ : (String)  S^',  S^''} ;
Θ(→, (String))(→, (ℕ));
        (r3) at (3,-1.5) [anchor=west] Γ : ø  : (ℕ)  S,  : S^''Θ(→, (String));
        
        [->] (s.east) – (r1.west) node[midway,above,sloped] ;
        [->] (s.east) – (r2.west) node[midway,above,sloped] ;
        [->] (s.east) – (r3.west) node[midway,above,sloped] p;
        
        (x) at (10.5,0) ;
    

    The transition over label  yields contexts in violation of <ref>.
    
    This example highlights the impact of message labels in protocol design, as reusing labels may lead to nondeterministic receipt of messages.
    
    However, this does not mean that messages with the same label can never be reused—it is possible for this nondeterminism to still be safe w.r.t. <ref>. 
    
     consider the types in <ref>, the types reuse labels  and .
    
    This is safe because the protocol has no dependency on receiving messages with the same label in a specific order.


[Load Balancer: Types]
    We type our load balancer using the protocol below in a judgement as s:_s, w_1:_w_1, w_2:_w_2c:_c, o:_o∅⊢∅ where  contains the processes from <ref>.
    
    The protocol observes the safety property  the reliability relation defined in <ref>.

    
    _s   = !c : req(ℕ) ø{[ w_1 : req(ℕ); w_2 : req(ℕ) ].
    _w_1   = !s : req(ℕ) øc : ans() 
    _w_2   = !s : req(ℕ) øc : ans() 
    _c   = øs : req(ℕ) &{[ w_1 : ans() øo : output(); w_2 : ans() øo : output();                øo : err() ].
    _o   = &{c : output() , c : err() }






 §.§ Type Properties


Our main results are presented below (proof details are given in <ref>).

Subject reduction (<ref>) states that any process typed under a safe context remains well-typed and safe after reduction (even in the presence of failures).

From this we obtain <ref>, stating that timeout branches are only omitted from linear receives if communication is reliable; hence certifying that all processes typed by safe contexts guarantee that no linear failure-prone communication goes unhandled.

A key contribution of our work is that this corollary is relaxed to linear processes instead of all processes, since we do not wish for replicated servers to handle dropped client requests.



    If ΓΔΘ⊢ with _(ΓΔΘ) and _^', then ∃, s.t. ΓΔΘ^*Γ and Γ⊢^' with _(Γ). 



    If ΓΔΘ⊢ with _(ΓΔΘ) and _^* &_i ∈ Iq_i : _i (c̃_̃ĩ)  P_i 𝒫^', then ∀ i ∈ I : {, q_i}∈.


Session fidelity (<ref>) states the opposite implication  subjection reduction,  processes typed under a safe context can always match at least one reduction available to the context.


    If ΓΔΘ and ΓΔΘ⊢ with _(ΓΔΘ), then ∃,,^' s.t. ΓΔΘΓ and _^* ^' and Γ⊢^' with _(Γ). 


Using this result we can verify properties other than just safety.

This is the benefit of the generalised approach to MPST, where instead of forcing protocols to abide by specific properties, types can be checked a posteriori to determine any properties they observe.

We demonstrate for deadlock freedom (<ref>).


    A network  is deadlock free, written (), iff ^* ^' implies either 
        
  * ^'≡; or
        
  * ^'≡ _1^'⋯_n^' s.t. ∀ i ∈ 1..n : _i^' = p_i!_j ∈ Jq_j : _j(x̃_̃j̃)  P_j.
    


A deadlock free network is one that only gets stuck when all processes reach , or when the only non- processes left in the network are servers.

(Note, the buffer is allowed to be non-empty because of message delays.)

We define deadlock freedom on types in <ref>, stating that type contexts are deadlock free if they only get stuck when the linear context is -typed.


    Contexts ΓΔΘ are deadlock free, written (ΓΔΘ), iff ΓΔΘ^* Γ implies ().



    If ΓΔΘ⊢ with _(ΓΔΘ), then (ΓΔΘ) implies ().


Lastly, in <ref> we state that deadlock free contexts imply deadlock freedom in the networks they type, a result which follows from <ref>.





  §.§.§ Decidability.


Asynchronous generalised MPST are known to be undecidable in general <cit.>.

This stems from the fact that session types with asynchronous buffers can encode Turing machines <cit.>.

However, we note that this simulation relies on buffers with queue semantics and tail-recursion; whereas our type system uses bag buffers and replication.

Comparing the expressive power of recursion and replication, previous studies show that for π-calculi with communication of free names the two are equally as expressive <cit.>; whereas without communication of free names ( CCS) recursion is strictly more expressive than replication <cit.>.

Thus, we raise the question: “What is the expressive power of asynchronous session types with bag buffers and replication?”, which we aim to answer in future work.


For now, we present a predicate on type contexts which can be used to determine decidable subsets of the type system.

This predicate, which we call trivially terminating (<ref>), is decidable and implies decidability of safety (and subsequently property verification).


    We say ΓΔΘ are trivially terminating, written (ΓΔΘ), iff ∀∈(Γ): Γ() = !_i ∈ Iq_i : _i (B̃_i) S̃_i where ∀ i ∈ I : q_i∉(Γ).



    For any contexts, (ΓΔΘ) is decidable and (ΓΔΘ) implies checking _(ΓΔΘ) is decidable.




§ ENCORE



Modelling of failures and distributed communication is increasingly becoming a more relevant and widely researched topic within the area of programming languages.

We highlight below some key related work, identifying the main differences  !.


Affine session types <cit.> use affine typing to allow sessions to be prematurely cancelled in the event of failure.

They may be used in a similar fashion to try-catch blocks, where a main protocol is followed until a possible failure is met and handled gracefully.

Similar in approach to ! is work by Barwell  <cit.>, where generalised MPST theory is extended to reason about crash-stop failures.

Where ! uses timeouts, the previous uses a “crash” message label which can be fed to a receiving process via some assumed failure detection mechanism.

Viering  <cit.> present an event-driven and distributed MPST theory, where a central robust node is assumed and is capable of restarting crashed processes.

Chen  <cit.> remove the dependency on a reliable node, instead using synchronisation points to handle failures as they are detected.

Adameit  <cit.> consider session types for link failures where default values act as failure-handling mechanism to substitute lost data.

! models lower-level failures than all of these works.

Most of the aforementioned assume some perfect failure-detection mechanism, whereas ! embraces timeouts as a weak failure detector to show that some degree of safety can still be achieved.

Our theory is designed to operate at a lower level of abstraction, thus often providing weaker guarantees ( consider our minimal definition of type safety) in exchange for modeling a wider set of communication failures. 



The adoption of replication in MPST theory is a novel contribution of this paper.

Replication in broader session types research has been utilised on numerous accounts <cit.>,
specifically in work pertaining to Curry-Howard interpretations of linear logic as session types, where the exponential modality from linear logic !A is typically linked to replication from the π-calculus.  

Disregarding our modeling of failure, the largest difference between these works and ours is that we focus on a multiparty setting, whereas these theories are all based on binary communication.

Furthermore, we did not opt to approach our problem from a logic-perspective, as is the main motivation behind this line of research.

Instead, we build upon already-standard generalised MPST theory, adapting it towards our problem domain.

We do note, however, that exploring a logical approach to replication in MPST (and, in turn, to failures in session types) is an interesting direction for future work.

A more related use of replication in types is by Marshall and Orchard <cit.>, where the authors discuss how non-linear types can be used in a controlled fashion to type behaviours such as repeatedly spawning processes.

This resembles the semantics of our type system and dynamic definition of replication in our language, where replicated processes (resp. types) can be reused as necessary to pull out linear copies of their continuations.

The mentioned work focuses on how to control the use of non-linear types and how this can be utilised with session types in a functional programming language.

Our work, on the other hand, uses replication as a means of better modeling client-server interactions and distinguishing between failure-prone communication that should be handled by the recipient or the sender.


On session types for client-server communication, research largely takes the approach of linear-logic correspondences <cit.>.

The topology these works target are of binary sessions between a pool of clients and a single server.

In Qian et al. <cit.> a logic is developed, called  (client-server linear logic), utilising the coexponential modality ¡A.

The subtle difference between this modality and the exponential !A is that the latter represents an unlimited number of a type A, while the former serves type A as many times as required according to client requests, in a sequential yet still unordered manner.

This is very similar to how our type system operates, given that replicated receives only pull out copies of continuations upon communication. 

Multiple requests induce non-determinism into further reductions, in our work this is seen in the extension of parallel types, which in Qian et al. <cit.> is observed through hyper-environments.

The difference in goal between the work of <cit.> (followed up by <cit.>) and ours, is that the mentioned works focus on providing fixed static guarantees on the processes they type (the former work with a focus on deadlock freedom, the latter on weak termination) whilst we take a generalised approach.

Our type system does not force programs to be deadlock-free or terminating, but rather requires a less restrictive safety property and allows verification of deadlock freedom and termination to be done a posteriori—the trade-off being our weaker form of type safety given the failure-prone nature of our setting.



To conclude, we presented !, an extension to  made to use replication (instead of recursion) to express infinite computation—both at the language and type levels.

We did so with the aim of better modelling multiparty client-server interactions, where servers are designed to remain infinitely available.

Specifically, we find type-level replication to be a clean mechanism for offloading the handling of certain failures from the recipient to the sender—a practical procedure for client-server interactions.

We have generalised our theory by proving our meta-theoretic results parametric of the largest safety property, allowing for more specific properties to be instantiated and used to verify runtime behaviours.

As future work, we plan to investigate more specific properties for verification through our general type system.

We aim to explore in detail the decidability of type-level properties and if/how they may be restricted to obtain decidable bounds in cases where they are not.

Lastly, we wish to conduct a foundational study of the use of replication in MPST—we anticipate their use for modelling client-server interactions to have further benefit outwith a failure-prone setting.




  §.§.§ Acknowledgements.

Supported by the UK EPSRC New Investigator Award grant EP/X027309/1 “Uni-pi: safety, adaptability and resilience in distributed ecosystems, by construction”.










splncs04





10em-5em-5em 


§ SIMPLIFICATION VIA REPLICATION


We compare session types for the ping protocol written in  <cit.> with our extension, !.

The example consists of three participants (or roles): the client ,  server , and a result channel .

Client side communication between  and  is reliable, as we assume these are processes on a single machine.

Communication with the server  is unreliable, thus failures must be handled through timeouts.

The client-side session types are defined as _ and _ below.

 
    [                                                                                                                                                      _                                                                                                                                          = &{ : ,  : };                                                                                                                                                      _ = ø  : &{[                                                             : ø : ,; ø : &{[                     : ø : ,; ø : &{[ : ø : ,;     ø : ]. ]. ]. ]


Client  begins by sending a message with label  to server  (ø  :) and then waits for a  response (& :).

If successful, an  message is sent to the results role  and the session is terminated for the client ().

Since communication with the server is unreliable, receipt of the  message is not guaranteed, and thus must be handled by a timeout branch .

The client attempts to reach the server 3 times—if all attempts fail, it sends a  message to .

The result role  waits for either of the reliable responses from , thus no timeout is defined.


Now we consider the server-side protocol. 

One possible definition of the server session type could be _ below (as show in <cit.>).

 
    _ = &{[                                           : ø :; &{[               : ø :; &{[ : ø :;       ]. ]. ].


However, although this is a safe definition, it does not cater for all possible scenarios.

The above definition only allows for up to three failures of the initial , and not the  reply.

If any  reply were to fail, then the result would always be , even though the client may try again.

If we were to also cater for three attempts from the server-side, then the server session type in  could be defined as S_^'.


 
    _^' = &{[ : ø : &{[ : ø : &{[ : ø :;       ].;       &{[ : ø :;       ]. ].;       &{[ : ø : &{[ : ø :;       ].;       &{[ : ø :;       ]. ]. ].


The key difference here is that the server must listen for a  even after its  reply, since  could fail and the client will reattempt the request.

In practice, servers avoid these cumbersome definitions by doing away with a specific retry count.

Retries (and the handling of failures in general), is left up to the client; servers instead opt to listen for requests for as long as they are available.

Hence, no matter the direction in which a message is dropped, servers will always attempt to respond to requests (unlike _).

We demonstrate this approach using replication at type-level in !. 


    _^! = ! : ø :



The replicated receive ! : denotes the server's constant availability to receive a  request.

Upon receiving a message from the client, the  response is issued, but the server remains available to receive further requests.

We highlight the absence of a failure-handling timeout branch in _^!; the server does not need to change its behaviour if a client request fails.

Furthermore, if the  reply fails, the server remains available to handle any number of retries from the client.

Thus, _^! handles all the failures covered by _^' whilst also being agnostic to the client-side implementation ( can handle any number of retries) and reducing complexity of the server-side protocol. 




§ STRUCTURAL CONGRUENCE


The full list of congruence rules used in ! is given in <ref> below.

Note that, different to most standards, no congruence rules are used for replication—extracting processes out of replicated receives is treated as an irreversible action and is handled by reduction (<ref>).


    
    cong-par-sym
        
        _1  _2 ≡_2  _1

    cong-par-ass
        
        (_1  _2)  _3 ≡_1  (_2  _3)

    [if  ∉()]cong-par-id
        
          ≡

    proc-par-sym
        
        𝒫_1 𝒫_2 ≡𝒫_2 𝒫_1

    proc-par-ass
        
        (𝒫_1 𝒫_2) 𝒫_3 ≡𝒫_1 (𝒫_2 𝒫_3)

    proc-par-id
        
        𝒫  ≡𝒫





§ SUBJECT REDUCTION AND SESSION FIDELITY


1[Subject Reduction]
    If ΓΔΘ⊢ with _(ΓΔΘ) and _^', then ∃, s.t. ΓΔΘ^*Γ and Γ⊢^' with _(Γ). 



    The proof is by induction on the derivation of _^'.
    
    For most cases, we infer the shape of relevant types in the contexts by inversion of typing rules and the assumption of ΓΔΘ⊢.
    
    Any message in the network buffer being used for reduction (by sending or receiving) is present in the type buffer—recall the affine nature of type buffers, and the fact that failures only drop network level messages.
    
    Therefore, the contexts can match the network reduction, and we already know that the reduced contexts can type the process continuations from the typing rules.
    
    The last thing to show is that the reduced contexts are also safe, which is obtained via 0 or more applications of <ref>.

    For the case where  reduces via <ref>, the network reduction is typed under the same context as the assumption, because Θ is affine and will allow for an unused message type in the type buffer. 

2[Session Fidelity]
    If ΓΔΘ and ΓΔΘ⊢ with _(ΓΔΘ), then ∃,,^' s.t. ΓΔΘΓ and _^* ^' and Γ⊢^' with _(Γ). 



    The proof begins by induction on the derivation of ΓΔΘ, for which we observe 4 possible cases from <ref>.
    
    Case <ref> is straight forward. From the assumption ΓΔΘ⊢ and rule <ref>, using action p we may infer the shape of  to at least contain process  with a top level linear receive with a defined timeout branch.
    
    Therefore the context action can be matched by the network via an application of <ref>.

    For the sending case, we infer the shape  by inversion of the typing rule <ref>.
    
    From this we obtain a network that can match exactly one of the paths identified in the type-level selection.
    
    Receiving cases are similar to each other.
    
    By  we know that any receive without a timeout is reliable, thus the network is guaranteed to not drop the messages required to match the type-level reduction.
    
    If the receive is unreliable, then the process can always, at the very least, match the timeout action.
    
    The remaining case is an unreliable communication to a replicated receive, as there is no guarantee that the message used for type-level reduction still exists in the network.
    
    In this case, if the message towards the replicated receive has already failed, then by , either the continuation of the replicated receive is -typed; or there is at least one other reduction possible by the contexts which the network can match. 





§ PROPERTY VERIFICATION


To demonstrate how our generalised meta-theory can verify configurable runtime properties, we 
[label=(*)]
    
  * define two sample properties on networks (deadlock freedom and termination); 
    
  * present their equivalent on type contexts; and 
    
  * prove the context property implies the network property.



    
        
  * A network  is deadlock free, written (), iff ^* ^' implies either 
            
  * ^'≡ 0; or
            
  * ^'≡ _1^'⋯_n^' s.t. ∀ i ∈ 1..n : _i^' = p_i!_j ∈ Jq_j : _j(x̃_̃j̃)  P_j.
        
        
        
  * A network  is terminating, written (), iff () and ∃ k finite s.t. ∀ n ≥ k :  = _0 _1 ⋯_n either 
            
  * _n ≡ 0; or
            
  * ^'≡ _1^'⋯_n^' s.t. ∀ i ∈ 1..n : _i^' = p_i!_j ∈ Jq_j : _j(x̃_̃j̃)  P_j.
        
    



Note that our definitions of deadlock freedom and termination (<ref>) differ from standard definitions in the π-calculus.

Specifically, it is typical for a process to only be considered deadlock free if it only stops reducing because of reaching the inactive process.

Our definition, on the other hand, allows for leftover replicated receives.

In the domain of client-server interactions where servers are designed to be infinitely available, a server will never reach .

This is an intended design choice of the calculus, as replicated receives are meant to model servers which do not terminate and may occasionally get stuck waiting in an idle state.

<Ref> reflects this design choice.



    
        
  * Contexts ΓΔΘ are deadlock free, written (ΓΔΘ), iff ΓΔΘ^* Γ implies ().
        
        
  * A context Γ00 is terminating, written (Γ00), iff (Γ00) and ∃ k finite s.t. ∀ n ≥ k : Γ00⋯Γnn implies (n).
    


The type-level equivalents of the process properties are given in <ref> above.

Concretely, a context is considered deadlock free iff it only stops reducing because its linear part is -typed.

A context is terminating iff it is deadlock free and it reaches the state in which it can no longer reduce within a finite number of reduction steps.



    If ΓΔΘ⊢ with _(ΓΔΘ), then ϕ(ΓΔΘ) implies ϕ(), for ϕ∈{, }.



    <Ref> follows directly from <ref>. 
    
    We know that if a context can reduce, then the network can match at least one reduction.
    
    Hence to prove property verification, we infer the shape of a network typed under the definition of ϕ on types, and show that this fits the definition of ϕ described for networks.
    
    We elaborate the case of  below, the other case is similar.

    From (ΓΔΘ) it follows that there are two subcases:
    
        
  * Consider ΓΔΘ can reduce,  ΓΔΘ.
        
        Then from ΓΔΘ⊢ and <ref> we infer that  can reduce, which satisfies () trivially.

        
  * Consider ΓΔΘ cannot reduce,  ΓΔΘ.
        
        Then, from the definition of  we know (Δ). 
        
        If the linear context is -typed then we can infer the shape of the entire network to be at most some composition of replicated receives with the network buffer.
        
        This shape of  fits the definition of  in <ref>, and thus we can conclude ().
    


