Choreographic programming promises a simple approach to concurrent and distributed programming: write the collective communication behaviour of a system of processes as a choreography, and then the programs for these processes are automatically compiled through a provably-correct procedure known as endpoint projection. While this promise prompted substantial research, a theory that can deal with realistic communication failures in a distributed network remains elusive. In this work, we provide the first theory of choreographic programming that addresses realistic communication failures taken from the literature of distributed systems: processes can send or receive fewer messages than they should (send and receive omission), and the network can fail at transporting messages (omission failure). Our theory supports the programming of strategies for failure recovery and is expressive enough to capture diferent communication patterns that usually required ad-hoc choreographic primitives and realistic protocols like two-phase commit.
In the paradigm of choreographic programming [
Key to choreographic programming is the notion of endpoint projection (EPP), a procedure for
compiling choreographies into distributed implementations in terms of appropriate send and receive
actions [
Despite all the recent interest in choreographic programming and neighbouring approaches, like
multiparty session types [
To meet this need, in this work we present a new theory of choreographic programming: Lossy
Choreographies (LC). LC is the first choreographic programming theory that can deal with realistic
communication failures from the literature of distributed systems: processes can send or receive fewer
messages than they should – send and receive omission [
The key technical challenge in developing LC lies in designing its syntax and semantics, because we need to equip programmers with the ability to program recovery strategies for failures. These strategies can be asymmetric, e.g., the sender of a message might use exponential backof while the intended receiver a timeout. This calls for deconstructing the syntax and semantics of the usual choreographic communication primitive to allow for independent implementations and executions of the send and receive sides. However, at the same time, we need to retain the high-level view of choreographies on what communications and computations the programmer wants to take place.
LC ofers a simple solution by introducing a notion of frames to choreographic programming. Specifically, we declare the intent to communicate a message of type T from p to q by writing (, ′)T : p → q,which creates the frames at p and ′ at q. Intuitively, the frame is a promise that p will send a value of type T for this particular communication, and dually ′ is a future where q can try to receive that value. Frames can then be used separately at the two processes in their own strategies for performing their respective obligations (sending or receiving). For example, p could use a procedure with exponential backof and q one with a timeout, written as sendExpBackoff(p; ); recvTimeout(q; ′). Leveraging this design and the high-level view of choreographic programming, LC enables processes to interleave the handling of multiple frames, each with its own recovery strategy. LC is thus expressive enough to capture diferent communication patterns that usually required ad-hoc choreographic primitives like scatter and to model realistic protocols like 2PC. Indeed, we will show that LC can serve as a general model where such primitives can be reconstructed as syntactic sugar.
Structure and contributions We introduce Lossy Choreographies in Section 2 and give some
examples of protocols modelled in this language in Section 3. In Section 4 we equip LC with a type
system and show that well-typed choreographies enjoy progress. In Section 5 we present a language for
local processes and endpoint projection for compiling choreographies to processes. Finally, we compare
our development to related work in Section 6 and conclude in Section 7. In the accompanying technical
report [
The language of Lossy Choreographies (LC) is defined by the following grammar.
::= ; | 0 ::= | ::= | ! | ? | ? ::= | (p, ) #» #» ::= (, ′)T : p → q | p.! | p.? | p. := | if p. then 1 else 2 | ⟨ p ; ⟩ A choreography is a sequence of instructions () ending in 0. Term (, ′)T : p → q declares a communication of a message of type T from p to q, binding the frame names for the sender and ′ for the receiver to the continuation — for simplicity we assume the Barendregt convention replacing bound names as needed. When this declaration is executed, frame names are substituted with pairs – (q, ) – that contain the name of the other process in the communication (q) and a natural number () called frame number that identifies this specific communication from p to q.1 Communications are then implemented with send terms like p.! (read ‘p sends on frame ’) and receive terms like q.′? (read ‘q receives a message on ′ and stores it in ’). These actions may fail, as we will show in our semantics.
Following standard practice from choreographic programming and session types, we syntactically
distinguish when a process sends the result of a local expression () or a statically-defined literal ( ,
also known as selection labels) [
In the local assignment term p. := , p assigns its local variable the value of local computation
. In a conditional if p. then 1 else 2, p evaluates the guard and chooses between the possible
continuations 1 and 2 accordingly. Guards can be of four forms: ! evaluates to true if the last
send attempt for was successful and to false otherwise; ? behaves like ? but for receive attempts;
? behaves like ? but additionally checks that the received values is the label ; and evaluates
#»
according to the semantics of the language of local expressions. Term ⟨ p ; #»⟩ invokes procedure
with arguments #p» and #». Procedures are defined by providing equations as usual in process calculi [
(, ′)T : p → q; p. := 0; sendExpBackoff⟨p; ⟩; q. := ; recvTimeout⟨p; ⟩; 0
LC is expressive enough to capture other strategies as syntactic sugar, including acknowledgements and compensations (custom code triggered in case of failure). Examples are given in Section 3. Semantics We give the semantics for LC in terms of a labelled transition system (LTS). The states of this system are triples of the form ⟨, Σ, ⟩ called configurations comprised by a choreography (a term in LC extended with two runtime terms discussed later), a choreographic store Σ modelling the processes memory, and a communication transit modelling messages in transit over the network.
A choreographic store Σ is a map from process names to their local memory stores ranged over by ,
similarly to several previous theories [
⟨, Σ[p. ↦→ ], ⟩ Σ(p.fc.q) = Σ′ = Σ[p.fc.q ↦→ + 1][p.fb.q. ↦→ ⊥ CFrame ] ⟨p.(q, )T; , Σ, ⟩− →− ⟨p.(q, )T; q.(p, ′)T; , Σ, ⟩→− ⟨[(q, )/], Σ′, ⟩
⟨(, ′)T : p → q; , Σ, ⟩→− ⟨′, Σ′, ⟩
Σ(p) ⊢ ↓ ⟨p.(q, )!; , Σ, →−−− ⟩−− −
⟨, Σ[p.fb.q. ↦→ ✓], ⊎ (p, q, , )⟩ #» #» ⟨⟨ p ; ⟩; ′, Σ, ⟩→−− #»
#» #» ⟨if p. then 1 else 2; , Σ, ⟩− →−− ⟨if p. then 1 else 2; , Σ, →−⟩−− − Σ(p) ⊢ ↓ true Σ(p) ⊢ ↓ false ( p ; ): ∈
r ∈ p #»
#» #» #» #» r ∈ q #» #» q ∖ r ̸= ∅ #» ⟨1 # , Σ, ⟩ #» ⟨2 # , Σ, ⟩ #» #»
#» #» #» #»
CThen CElse
CEnter ⟨ p ∖ r : [ p ; ].′; [ p / q ][ / ] # ′, Σ, ⟩
CSend CRecv
CCall ⟨p.(q, )!; , Σ, →−−− ⟩−− −
⟨, Σ, ⟩ ⟨p.(q, )?; , Σ, →−−− ⟩−− − Σ(p) ⊢ ↓ ⟨, Σ, ⊎ (p, q, , )→⟩− ⟨, Σ[q.fb.p. ↦→ ], ⟩ ⟨, Σ, ⊎ (p, q, , )→⟩− ⟨, Σ, ⟩ ⟨1, Σ, ⟩→− ⟨1′, Σ′, ′⟩
⟨2, Σ, ⟩→− ⟨2′, Σ′, ′⟩ p ∈/ pn( )
CDelayC CFinish ⟨, Σ, ⟩→− ⟨′, Σ′, ′⟩
pn() ∩ pn( ) = ∅ CDelayI ⟨; , Σ, ⟩→− ⟨; ′, Σ′, ′⟩ ⟨if p. then 1 else 2; , Σ, ⟩→− ⟨if p. then 1′ else 2′; , Σ′, ′⟩ ⟨ q :[ p ; ].′; , Σ, ⟩→−−
⟨ q ∖ r : [ p ; ].′; , Σ, ⟩ counters locally, i.e., without synchronising with the other party; (3) frames are assigned the value held by the corresponding counter when they are created. Our semantics ensures that frame counters remain consistent through the execution of a choreography and so it sufices to agree on an initial value — we formalise this property after we present the semantics (Definition 1).
The network and the messages transiting on it are modelled by a communication transit : a multiset of messages that have been successfully handed over to the network from the sender, but have not been delivered to the receiver. Each message has the form (p, q, , ) where p is the sender, q is the receiver, is the frame number, and is the payload. may contain messages with the same sender, receiver, and frame number but diferent payloads e.g., when a sender makes multiple attempts updating a timestamp or counter in the payload each time and these are still in transit. The defining as a multiset, we model a network without any ordering guarantee.
#»
The transition relation of the LTS is giv#»en by the SOS specification in Figure 1 and it is p#»arameterised on a set of procedure definitions ( p ; ): where is the procedure name, p and are its formal parameters for process and frame names, the choreography (free from runtime terms) is its body. #»
In the remainder, we write pn() and and pn( ) for the set of process names that appear in the choreography and the label , respectively.
Rule CAssign models local assignments and is standard: the update notation Σ[p. ↦→ ] denotes a
choreographic store such that (Σ[p. ↦→ ])(p.) = and behaves like Σ otherwise [
Rules CCom and CFrame model the creation of a pair of frames for a communication from p to q without relying on any rendezvous mechanism. Instead, these rules rely on the runtime term p.(q, )T to represent the creation of a frame to/from q at p: in rule CFrame, p.(q, )T is consumed, the frame is assigned a number , its state is initialised to ⊥, and the frame counter for q is incremented; and in rule CCom, the semantics of (, ′)T : p → q is essentially defined as that of p.(q, )T; q.(p, ′)T. The order of the runtime terms in the premise of rule CCom is immaterial since the semantics allows these to be executed in any order via rule CDelayI (explained below).
Rules CSend and CSendFail capture the possible executions of a send attempt for a frame (q, ) at p. The first, Rule CSend models a successful send: a payload is computed and the message (p, q, , ) is successfully handed of to the communication transit ( ). It also updates the frame state at the sender accordingly. Rule CSendFail, instead, models a send omission failure: the send action is consumed but it omits (fails at) adding the message to . In both cases, no information about the attempt is propagated to the receiver: our semantics is asynchronous and the only way to exchange information across processes is through fallible communication actions and a lossy . Note that rule CSend does not check the state of the frame and that the new one is added to with a multiset union (⊎), to reflect the real-world situation that a sender may perform multiple send actions resulting in the transmission of multiple messages (regardless of diferences for the payload ) for the same frame.
Once a message is in transit, there are two possibilities: It can either be successfully delivered to the receiver, which causes a corresponding update to its frame state (rule CDel), or it can incur an omission failure and be lost (rule CLoss). The sender has no knowledge of what happens.
Rules CRecv and CRecvFail model a receive attempt. The attempt can be successful (CRecv) only if the receiver’s state for the desired frame contains a value (previously put there by rule CDel). Otherwise, if no message for that frame has reached the receiver yet, the receive attempt fails (rule CRecvFail).
Rules CThen and CElse model conditionals. The evaluation of guards on frames is as follows: Σ(p.fb.q.) = ✓ Σ(p) ⊢ (q, )? ↓ true Σ(p.fb.q.) ̸= ✓ Σ(p) ⊢ (q, )? ↓ false
Σ(p.fb.q.) = ✓ Σ(p) ⊢ (q, )! ↓ true
Σ(p.fb.q.) ̸= ✓ Σ(p) ⊢ (q, )! ↓ false
Σ(p.fb.q.) = ✓ Σ(p) ⊢ (q, )? ↓ true
Σ(p.fb.q.) ̸= ✓
Σ(p) ⊢ (q, )? ↓ false
We use a meta-operator for sequential composition of choreographies ‘#’ [
Remaining rules are standard for the theory of choreographic languages [
With the language fully defined, we formalise the property that frame states, counters, and runtime terms are consistent across a choreography and store.
Definition 1. Σ is consistent with if, for any two p and q in : (1) Σ(p.fb.q.) is defined for any < Σ(p.fc.q); and (2) |qp()| = max(0, Σ(p.fc.q) − Σ(q.fc.p)) where the (partial) function qp computes the set of frame names to q that p has yet to initialise as follows.
qp(0) ≜ ∅
qp(; ) ≜ qp() ∪ qp() where pq() ∩ qp() = ∅ qp(p.(q, )T) ≜ {}
qp(if p. then 1 else 2) ≜ qp(1) where pq(1) = qp(2) qp() = ∅ for ∈/ {p.(q, )T, if p. then 1 else 2} Σ′ = Σ[p.fb.q.1 ↦→ ✓] Σ(p.fb.q.1) = Σ(p.fb.q.1) = ⊥
(a)
CRecv CDel ⟩ ⟨ (c) CSend ⟨ ⟨ (b) (h) CDel
q.(p, 1)?; 0, ⟩ Σ[p.fb.q.1 ↦→ ✓], {(p, q, 1, 3)}
0, Σ[p.fb.q.1 ↦→ ✓], {(p, q, 1, 3)}
⟩ CRecvFail
q.(p, 1)?; 0, ⟩ Σ′[q.fb.p.1 ↦→ 3],
∅ CLoss (i) CLoss ⟨ q.(p, 1)?; 0,⟩ (j) Σ′, ∅ ⟨ 0, ⟩ Σ′, ∅
Note that the function qp is partial and rejects choreographies that misuse runtime terms for frame creation e.g., the condition on the case ; excludes repetitions of runtime terms for the same .
Proposition 1. If ⟨, Σ, →⟩− ⟨′, Σ′, ′⟩ and Σ is consistent with , then Σ′ is consistent with ′.
We illustrate the realism of our model wrt communication failures with a simple end-to-end communication. Consider the choreography p.(q, 1)!3; q.(p, 1)?; 0 where p attempts to communicate the number 3 to q; the LTS in Figure 2 captures all the possible executions for this program. For convenience of exposition, we assign a letter to each state. Also, we do not show transition labels but rather the name of the rule applied to derive the transition – the transition from (a) to (e) is the only one that also requires rule CDelayI.
Every run of the program begins in state (a) and eventually terminates reaching 0. We describe the diferent situations at the ends of the possible executions.
(d) This is the final state of the only successful execution: the value 3 is marked as delivered and no transition from (a) to (d) uses any of the rules that model send, receive, and omission failures. (g) This state is reached if we have both a send and a receive omissions. In the path via (f), a send omission stops the receive from ever succeeding. In the path via (e), we have a receive omission because the receive is attempted before the send action had a chance to put the message in the network. The latter case exemplifies how our semantics captures timeouts at the receiver. In fact, (e) may transition to (h) failing because of timing, as this is before the successful transit. (j) This state is reached because of an omission failure. In the path via (i), the omission failure causes the receive to fail. In the path via (e), the receive fails regardless of the omission because of timing. (k) This state is reached if the send succeeds but the receive fails because of timing issues: in the path through (e), the receive is executed before the send; in the path through (b), the receive is executed before the network could carry the message to the receiver.
Assume a setting with omission failure (rule CLoss). In this setting, the definition of p. →T q. presented in Example 1 risks ending up in a state where the sender believes it has completed a communication but the receiver has timed out due to the message being lost by the network. This is a common problem in practice, which is addressed by switching to “best-efort” strategies where delivery is possible (to varying degrees) but not certain.
The procedure below implements a simple communication protocol with capped retries and acknowledgements to the sender. In this, the strategy use by comACK, can be regarded as a simplification of that of TCP; four-phase handshakes or other protocols are implementable in LC as well. 1 comACK,(s, r): 2 (, ′)T : s → r; //Create new frame for this communication 3 (′, )Unit : r → s; //Create new frame for the acknowledgement 4 sendExpBackoff(s; ); //Send 5 recvTimeout(r; ′); //Receive 6 sendExpBackoff(r; ′
); //Send acknowledgement 7 sendUntilACK,(s; , ); //Call send procedure 8 sendUntilACK,(s; , ): 9 recvTimeout(s; ); //Try receiving acknowledgement 10 if s.( > 0) ∧ ¬s.? then //Check number of attempts and received acknowledgement 11 s. := − 1; //Update send attempt number 12 sendExpBackoff(s; ); //Make another attempt at sending 13 sendUntilACK,(s; , ); //Repeat 14 else 0 //When acknowledgement has been received or we run out of attempts, end.
Compensations With comACK, we can also use LC to develop a new variant of choreographies
that does not assume reliable transmission, i.e., when we are in a setting with omission failures. In
this setting, a common pattern to deal with failures of best-efort communications are compensations.
Fault compensations can be defined in LC (for both settings with and without omission failures) using
conditionals, comACK, (or variations thereof), and some syntax sugar to improve readability. An
expression s. ⇒ r.{s}{r} is a communication as in comACK,(s, r) where choreographies s
and r are executed as compensations for faults detected by the sender s (no ack) or the receiver r,
respectively. An example of communications with fault compensations is the communication construct
defined in [
1 sendAll,(s; 1, . . . , ):
2 s.!; //Send to the last frame in the list
3 if s.! then //Check if send was successful
4 sendAll− 1,(s; 1, . . . , − 1) //Send to the remaining frames
5 else sendAll,(s; 2, . . . , , 1) //Otherwise, try this frame again later
1 sendAny,(s; 1, . . . , ):
2 s.1!; //Send to the first frame in the list
3 if ¬s.1! then //Check if send was unsuccessful
4 sendAny,(s; 2, . . . , , 1) //Retry cycling through the frames
5 else 0 //End function if the send succeeded
We omit the dual procedures for receiving all or some frames, which are similarly defined. Combining
these it is possible to implement scatter/gather communication primitives from [
Two-phase commit LC can be used to implement common protocols for dealing with failures. The
two-phase commit protocol [
Note that sendAllUntilAck is a combination of sendAll and sendUntilAck without the check on the number of send attempts; we omitted this for brevity but it could easily be reintroduced if one is concerned about c being blocked by a lost acknowledgement.
LC programs can get stuck if procedures are called on wrong arguments, communication actions are performed against the wrong frames or processes, and guards of conditionals are not of the expected type. We introduce a type system for LC that rejects this kind of programs and ensures progress.
Type judgements are of the form Γ ⊢ where Γ is an environment for tracking the types of choreographic procedures, frames and the local memory.
#» # » Γ := ⟨ p ; : T⟩ | p. : | p. : T := !T | ?T Γ, p. : !T, q.′ : ?T ⊢ TCom Γ ⊢ (, ′)T : p → q; Γ(p.) ∈ {!T, ?T} Γ ⊢ Γ ⊢ p.(q, )T;
TFrame Γ(p.) = !T Γ(p) ⊢ : T Γ ⊢
TSend Γ(p.) = ?T
Γ(p.) = T Γ ⊢ TRecv Γ ⊢ p.!; Γ ⊢ p.?;
The frame types !T and ?T denote a frame that sends a payload of type T and one that receives a payload of type T. We write Γ(p.) and Γ(p.) for the type of frame p. and of variable p., and Γ(p) for the environment local to p. Just like we assumed a user-defined local language, we do the same for guards about frame status (!, ?, ?) as one would expect (see [21, §4] for details). the local type system, which we assume has local judgements Γ(p) ⊢ : T extended to account for
For the most part, these rules are fairly intuitive. We report a selection of illustrative derivation rules of the type system in Figure 3, the full system is available in the report [21, §4]. Rule TCom adds both ends of the frame to the environment with the expected send and receive types and rule TFrame checks that the runtime term for frame creation refers to a frame in the environment.2 Rules TSend and TRecv check that the type of the frame matches the type of the payload and the variable it gets stored on. Definition 2.
We say that a configuration
⟨, Σ, ⟩ is well-typed if there is a type environment Γ(q.(p, )) = ?T, and ⊢ : T for any (p, q, , ) ∈ ; (4) Σ is consistent with . Γ such that (1) Γ ⊢ ; (2) Γ ⊢ Σ(p.) : Γ(p.) for any variable p. ∈ Σ; (3) Γ(p.(q, )) = !T,
Our type system enjoys typability preservation: if a configuration is well-typed then so is any configuration that can be reached from it.
Proposition 2 (Typability Preservation). Given a well-typed configuration ⟨, Σ, ⟩ and set of procedure definitions , if ⟨, Σ, →⟩− ⟨′, Σ′, ′⟩, then ⟨′, Σ′, ′⟩ is also well-typed.
Well-typed configurations enjoy progress: they either do an action or their choreography is 0. Theorem 1 (Progress). Given a well-typed ⟨, Σ, ⟩ and , = 0 or ⟨, Σ, →⟩− ⟨′, Σ′, ′⟩.
We present an EndPoint Projection (EPP) procedure that compiles a choreography to a concurrent implementation in terms of a process calculus, which assumes the same failure model as in LC.
The target process language, Lossy Processes, is based on Recursive Processes –
the textbook target for choreography projection [
The next grammar allows for writing process programs, or behaviours ().
::= ; | 0 ::= | ::= | ::= | (p, ) ::= (p, ) | ! | ? | := | if then 1 else 2 | &{1 : }∈ | ⟨ p ; ⟩ #» #» 2For conciseness, neither rule check for misuses of runtime terms like p.(q, )T; p.(q, )T or (, ′)T : p → q; p.(q, )T as these are already excluded by Definition 1; these checks amount to adding the premises ∈/ qp() and ′ ∈/ pq(). ⟨p[(q, )?; ], Σ, →−−− ⟩−− −
⟨, Σ, ⟩→− ℬ ⟨ ′, Σ′, ′⟩ ⟨ | , Σ, ⟩→− ℬ ⟨ ′ | , Σ′, ′⟩
Term (p, ) represent the creation of a new frame. Terms ! and ? express send and receive actions for . Term &{1 : }∈ describes a branching based on a label communicated for , if any label has been successfully received then, the process proceeds with the corresponding behaviour otherwise it proceeds with the one labelled with default which is reserved for this purpose and cannot be sent. has been successfully completed. Remaining terms are standard.
If = ∅, then the term is simply discarded. Guard states that the last communication action for frame
Borrowing notation from [
The semantics of networks is given as an LTS. States are configurations ⟨, Σ, ⟩ where is a network and Σ and are as in the LTS of LC. The transition relation uses the same labels of LC and is which we discuss below—the remaining ones are standard and can be found in [21, §5]. parameterised in a set ℬ of procedure definitions. We report a selection of the core rules in Figure 4
Rule PFrame models the creation at p of a new frame for q using the value of the corresponding counter. Rule PSend models the sending of a message to frame (q, ), marking the frame as sent and rule PSendFail models the case where the send fails. Dually, rules PRecv and PRecvFail model the successful reception of a message from frame (q, ), marking the frame as received and storing in the received value , and the case where the receive fails, respectively. Rules NLoss and NDel model the loss and delivery of messages by the network like rules CLoss and CDel.
Given a choreography , the projected behaviour of process p in is defined
as JKp where J− Kp is the partial function defined by structural recursion in Figure 5. Each case in the
definition follows the intuition of writing, for each choreographic term, the local actions performed
by the given process. For instance, p.! is skipped during the projection of any process but p, for
which the send action ! is produced. Cases for receiving, procedure calls, and frame creation are
similar. The projection of frame declaration expands it to two frame creation runtime terms similarly
to its semantics, ensuring that as long as the starting configuration is consistent, the frame counters
will remain synchronised for the entire execution. The case for conditionals combines the normal
conditionals and branching over labels selection but otherwise follows the standard approach (see
e.g., [
JKr {︃(q, ); JKr if r = p
else Jp. := ; Kr ≜
JKr {︃ := ; JKr if r = p
#» #»
J⟨ p ; ⟩; Kr ≜ else
JKr J #q»:[ p ; ].′; Kr ≜ #» #»
#» #» #» #» {︃( p ∖ r; ); J′Kr if r ∈ q and r = p []
else s if p. then 1 { else 2; r ≜ ⎪ ⎪ ⎩(J1Kr ⊔ J2Kr); JKr ⎪⎨(if then J1Kr else J2Kr); JKr ⎪(if then J1Kr else J2Kr); JKr ⎪ ⎧(&{ : J1Kr , default : J2Kr}); JKr if p. = r.? ⎪ if p. = r. if p. = r.! or p. = r.? else Jp.!; Kr ≜ Jp.?; Kr ≜
JKr
J Kr
JKr {︃!; JKr if r = p {︃?; JKr if r = p else else else
J0Kr ≜ 0 #» #» #» {︃( p ∖ r; ); JKr if r = p [] labels are also included. One proceeds homomorphically (e.g., !; ⊔ !; ′ is !; ( ⊔ ′)) on all terms but branches which are handled defining the merge of &{ : }∈ ; and &{ : ′ }∈ ; ′ as &{ℎ : ℎ′′}ℎ∈ ; ( ⊔ ′) where {ℎ : ℎ′′}ℎ∈ is the union of { : }∈∖ , { : ′ }∈∖ , and { : ⊔ ′}∈∩ . A choreography is projected to JK ≜ p. JKp and procedure definitions as: JK ≜ ⋃︀
#» (p1,...pn; )=∈ ⃒ }︁ {︁(p1, . . . , p− 1, p+1, . . . pn; )JKp ⃒⃒ 1 ≤ ≤ .
#» Observe that since a procedure may be called multiple times on any combination of its arguments it is necessary to project the behaviour of each possible process parameter p as the procedure .
There is an operational correspondence between choreographies and their projections, which we
can be formulated in the standard way up to the ‘branching’ relation ⊒ (the natural order induced by
merging i.e., 1 ⊒ 2 if 1 ⊔ 3 = 2 for some 3 [
• If ⟨, Σ, →⟩− ⟨′, Σ′, ′⟩ then J, Σ, →K−
J K such that J′K ⊒ .
• If ⟨JK , Σ, →⟩− JK ⟨, Σ′, ′⟩, then ⟨, Σ, →⟩− ⟨′, Σ′, ′⟩ such that J′K ⊒ .
The work nearest to ours is [
Another extension of MPST focuses on process failures (instead of communication failures) [
In [
A diferent approach to MPST with failures is seen in [
In [
Some work on choreographies include choice operators that behave nondeterministically, e.g., + ′,
read ‘run either or ′’ [
Our approach of recovering high-level choreographic constructs by wrapping lower-level
communication actions (as in Example 1) follows the practice established by Choral, the most expressive
implementation of choreographic programming to date [
Recent work explored how choreographic programming can be ofered as embedded domain-specific
languages in, for example, Haskell and Rust [
Our new primitive for communication declaration is reminiscent of the ‘cut’ operator found in
sessiontyped process calculi for connecting two endpoints of a channel [
Choreographic programming has seen significant advancements over the past decade, but always under
the strong assumption of reliable communication [
Our work covers all failure modes with honest participants. A natural next step is therefore to investigate Byzantine failures modes where participants may act maliciously. Exploring this direction would touch on a realm where possible guarantees are more limited. Therefore, it would be interesting and challenging to understand how close choreographic programming can be brought to the theoretical limit. Another interesting direction is to explore a quantitative semantics of Lossy Choreographies. For instance, in a probabilistic settings, failures are characterised by probability distributions. This would enable reasoning about aspects such as quality of service, throughput, probability of critical failure, etc.
Partially supported by Villum Fonden (grant no. 29518), and by the Ministry of Education and Research Centres of Excellence grant TK213 Estonian Centre of Excellence in Artificial Intelligence (EXAI). Cofunded by the European Union (ERC, CHORDS, 101124225). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
04131. doi:10.48550/ARXIV.2401.04131. arXiv:2401.04131.