An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems

Abstract

This paper presents a model of session-based concurrency with mechanisms for runtime adaptation. Thus, our model allows to specify communication-centric systems whose session behavior can be dynamically updated at runtime. We propose an event-based approach: adaptation requests, issued by the system itself or by its environment, are assimilated to events which may trigger runtime adaptation routines. Based on type-directed checks, these routines naturally enable the reconfiguration of processes with active sessions. We develop a type system that ensures communication safety and consistency properties: while the former guarantees absence of runtime communication errors, the latter ensures that update actions do not disrupt already established sessions.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Context. Modern software systems are built as assemblies of heterogeneous artifacts which must interact following predefined protocols. Correctness in these communication-centric systems largely depends on ensuring that dialogues are consistent. Session-based concurrency is a type-based approach to ensure conformance of dialogues to prescribed protocols: dialogues are organized into units called sessions; interaction patterns are abstracted as session types [9], against which specifications may be checked.

As communication-centric systems operate on open infrastructures, runtime adaptation appears as a crucial feature to ensure continued system operation. Here we understand runtime adaptation as the dynamic modification of (the behavior of) the system in response to an exceptional event, such as, e.g., a varying requirement or a local failure. These events are not necessarily catastrophic but are hard to predict. As such, protocol conformance and dynamic reconfiguration are intertwined concerns: although the specification of runtime adaptation is not strictly tied to that of structured protocols, steps of dynamic reconfiguration have a direct influence in a system’s interactive behavior.

We are interested in integrating forms of runtime adaptation into models of session-based concurrency. As a first answer to this challenge, in previous work [8] we extended a typed process framework for binary sessions with basic constructs from the model of adaptable processes [2]. In this work, with the aim of extending the applicability and expressiveness of the approach in [8], we propose adaptation mechanisms which depend on the state of the session protocols active in a given location. As a distinctive feature, we advocate an event-based approach: by combining constructs for dynamic type inspection and non-blocking event detection (as put forward by Kouzapas et al. [11, 13]), adaptation requests, both internal or external to the location, can be naturally assimilated to events.

A Motivating Example. Here we consider a standard syntax for binary session types [9]:

$$ \begin{aligned} \begin{array}{rll} \alpha , \beta :\,\!:= &{} ?(T).\beta &{}\,\, \text {input a value of type} { T}, \text {continue as}~\beta \\ \ \mid \ &{} !(T).\beta &{}\,\, \text {output a value of type} { T}, \text {continue as}~\beta \\ \ \mid \ &{} \& \{n_1{:}\alpha _1 \dots n_m{:}\alpha _m \} \qquad &{}\,\, \text {branching (external choice)} \\ \ \mid \ &{} \oplus \{n_1{:}\alpha _1 \dots n_m{:}\alpha _m \} &{}\,\, \text {selection (internal choice)} \\ \ \mid \ &{} \varepsilon ~~ \ \mid \ ~~ \mu t.\alpha \ \mid \ t &{}\,\, \text {terminated and recursive session} \end{array} \end{aligned}$$

where T stands for both basic types (e.g., booleans, integers) and session types $\alpha$. Also, $n_1, \ldots , n_m$ denote labels. To illustrate session types, consider a buyer $\mathtt {B}$ and a seller $\mathtt {S}$ which interact as follows. First, $\mathtt {B}$ sends to $\mathtt {S}$ the name of an item and $\mathtt {S}$ replies back with its price. Then, depending on the amount, $\mathtt {B}$ either adds the item to its shopping cart or closes the transaction. In the latter case the protocol ends. In the former case $\mathtt {B}$ must further choose a paying method. From $\mathtt {B}$’s perspective, this protocol may be described by the session type $\alpha = \,\,!\mathsf {item}.\,?\mathsf {amnt}.\,\alpha _{\mathtt {pay}}$, where $\mathsf {item}$ and $\mathsf {amnt}$ are base types and

$$\begin{aligned} \alpha _{\mathtt {pay}} \,=\,\oplus \{\mathtt {addItem}:\, \oplus \{\mathtt {ccard}:\, \alpha _\mathtt {cc} \,,\, \mathtt {payp}:\, \alpha _\mathtt {pp}\}\,,\,\mathtt {cancel}:\,\varepsilon \}. \end{aligned}$$

Thus, session type $\alpha$ says that protocol $\alpha _{\mathtt {pay}}$ may only be enabled after sending a value of type $\mathsf {item}$ and receiving a value of type $\mathsf {amnt}$. Also, $\mathtt {addItem}$, $\mathtt {ccard}$, $\mathtt {cc}$, and $\mathtt {payp}$ denote labels in the internal choice. Types $\alpha _\mathtt {cc}$ and $\alpha _\mathtt {pp}$ denote the behavior of each payment method. Following the protocol abstracted by $\alpha$, code for $\mathtt {B}$ may be specified as a $\pi$-calculus process. Processes P and R below give two specifications for $\mathtt {B}$:

Thus, although both P and R implement $\alpha$, their behavior is rather different, for they purchase different items using different payment methods (which are abstracted by processes $P^{\mathsf {c}}$ and $R^{\mathsf {p}}$). Let us now analyze the situation for the seller $\mathtt {S}$. To ensure protocol compatibility and absence of communication errors, the session type for $\mathtt {S}$, denoted $\beta$, should be dual to $\alpha$. This is written $\alpha \,\bot _{\mathtt {C}}\,\beta$. Intuitively, duality decrees that every action from $\mathtt {B}$ must be matched by a complementary action from $\mathtt {S}$, e.g., every output of a string in $\alpha$ is matched by an input of a string in $\beta$. In our example, we let $\beta = \,\,?\mathsf {item}.\,!\mathsf {amnt}.\,\beta _{\mathtt {pay}}$, where $\beta _{\mathtt {pay}}$ and a process implementation for $\mathtt {S}$ are as follows:

where price stands for an auxiliary function. Also, $\beta _{\mathtt {cc}}$ and $\beta _{\mathtt {pp}}$ are the duals of $\alpha _{\mathtt {cc}}$ and $\alpha _{\mathtt {pp}}$; they are realized by processes $Q_y^{\mathsf {c}}$ and $Q_y^{\mathsf {p}}$. The interaction of P and Q is defined using session initialization constructs: process $\overline{u}(x{:}\alpha ).P$ denotes the request of a session of type $\alpha$; dually, $u(x{:}\alpha ).P$ denotes the acceptance of a session of type $\alpha$. In both cases, u denotes a (shared) name used for synchronization. In our example, we may have

Thus, upon synchronization on u, a new session $\kappa$ is established. Intuitively, in process $S'$ session $\kappa$ is “split” into two session channels (or endpoints) $\kappa ^+$ and $\kappa ^-$: we write + and − to denote their opposing polarities, which make their complementarity manifest. The use of restriction $(\nu \kappa )$ covers both channels, thus ensuring an interference-free medium for executing the session protocols described by $\alpha$ and $\beta$.

In this work, we are interested in ways of expressing and reasoning about the dynamic modification of session-typed processes such as P and Q above. Such modifications may be desirable to react to exceptional runtime conditions (say, an error) or to implement new requirements. For instance, the type below defines a new payment method for $\mathtt {S}$:

$$ \begin{aligned} \beta _{\mathtt {gift}} \,=\, \& \{\mathtt {addItem}:\, \& \{\mathtt {giftc}:\, \beta _\mathtt {gc} \,,\, \mathtt {ccard}:\, \beta _\mathtt {cc} \,,\, \mathtt {payp}:\, \beta _\mathtt {pp}\}\,,\,\mathtt {cancel}:\,\varepsilon \} \end{aligned}$$

Intuitively, $\beta _{\mathtt {gift}}$ extends $\beta _{\mathtt {pay}}$ with a new alternative on label $\mathtt {giftc}$. As such, it is safe to use a process implementing $\beta _{\mathtt {gift}}$ wherever a process implementing $\beta _{\mathtt {pay}}$ is required. The safe substitution principle that connects $\beta _{\mathtt {gift}}$ and $\beta _{\mathtt {pay}}$ is formalized by a subtyping relation on session types [7], denoted $\le _{\mathtt {C}}$. In our example, we have $\beta _{\mathtt {pay}} \le _{\mathtt {C}} \beta _{\mathtt {gift}}$.

In previous work [8] we studied how to update processes when sessions have not yet been established; this suffices to analyze runtime adaptation for processes such as Sys above. In this paper, we go further and address the runtime adaptation of processes such as $S'$ above, which contain already established session protocols. As we would like to guarantee that adaptation preserves overall system correctness, a key challenge is ensuring that adaptation does not jeopardize such protocols. Continuing our example, let $S''$ be the process resulting from $S'$ above, after the first step stipulated by $\alpha$ and $\beta$ (i.e., an exchange of a value of type $\mathsf {item}$). Intuitively, at that point, the buyer part of $S'$ will have session type $?\mathsf {amnt}.\,\alpha _{\mathtt {pay}}$, whereas the seller part of $S'$ will have session type $!\mathsf {amnt}.\,\beta _{\mathtt {pay}}$. Suppose we wish to modify at runtime the part of $S''$ realizing the buyer behavior. To preserve protocol correctness, a candidate new implementation must conform, up to $\le _{\mathtt {C}}$, to the type $?\mathsf {amnt}.\,\alpha _{\mathtt {pay}}$; a process realizing any other type will fail to safely interact with the part of $S''$ implementing the seller. In [8] we defined the notion of consistency to formalize the correspondence between declared session protocols and the processes installed by steps of runtime adaptation. As we will see, consistency is still appropriate for reasoning about runtime adaptation of processes with active sessions.

Our Approach. Having motivated the context of our contributions, we move on to describe some technical details. We rely on a process language which extends session $\pi$-calculi with locations, located processes, and update processes [2]. We use locations as explicit delimiters for process behavior: these are transparent, possibly nested computation sites. Given a location ${\mathrm {loc}}$ and a process P, the located process ${\mathrm {loc}}[P]$ denotes the fact that P resides in ${\mathrm {loc}}$ (or, alternatively, that P has scope ${\mathrm {loc}}$). This way, e.g., process

$$\begin{aligned} W = {\mathrm {sys}}\big [\,{\mathrm {buyer}}\big [ \overline{u}(x{:}\alpha ).P\big ] \mathord {\;\varvec{|}\;}{\mathrm {seller}}\big [ u(y{:}\beta ).Q\big ] \,\big ] \end{aligned}$$

represents an explicitly distributed variant of Sys above: the partners now reside in locations ${\mathrm {buyer}}$ and ${\mathrm {seller}}$; location ${\mathrm {sys}}$ encloses the whole system. An update process, denoted ${\mathrm {loc}}\{U\}$, intuitively says that the behavior currently enclosed by ${\mathrm {loc}}$ should be replaced according to the adaptation routine U. Since a location may enclose one or more session channels, update processes allow for flexible specifications of adaptation routines. This way, e.g., one may specify an update on ${\mathrm {buyer}}$ that does not involve ${\mathrm {seller}}$ (and vice versa); also, a system-level adaptation could be defined by adding a process ${\mathrm {sys}}\{U_s\}$ in parallel to W, given an $U_s$ that accounts for both buyer and seller behaviors.

The integration of runtime adaptation into sessions is delicate, and involves defining not only what should be the state of the system after adaptation but also when an adaptation step should be triggered. To rule out careless adaptation steps which jeopardize established protocols, communication and adaptation actions should be harmonized. As hinted at above, in previous work [8] we proposed admitting adaptation actions only when locations do not enclose running sessions. This is a simple solution that privileges communication over adaptation, in the sense that adaptation is enabled only when sessions are not yet active. Still, in realistic applications it may be desirable to give communication and adaptation a similar status. To this end, in this paper we admit the adaptation of locations with running sessions. We propose update processes ${\mathrm {loc}}\{U\}$ in which U is able to dynamically check the current state of the session protocols running in ${\mathrm {loc}}$. In their simplest form, our update processes concern only one session channel and are of the shape

$$\begin{aligned} {{\mathrm {loc}}\big \{\mathsf {case}\,{x}\,\mathsf {of}\,\{({x_{}^{}{:}\beta _{}^{i}}):U_i\}_{i \in I}\big \}} \end{aligned}$$

where I is a finite index set, x denotes a channel variable, each $\beta ^i$ and $U_i$ denotes a session type and an alternative (process) $U_i$, respectively. (We assume x occurs free in $U_i$.) The informal semantics for this construct is better understood by considering its interaction with a located process ${\mathrm {loc}}\big [ Q\big ]$ in which Q implements a session of type $\alpha$ along channel $\kappa ^p$. The two processes may interact as follows. If there is a $j \in I$ such that types $\alpha$ and $\beta ^j$ “match” (up to $\le _{\mathtt {C}}$), then there is a reduction to process . Otherwise, if no $\beta ^j$ validates a match, then there is a reduction to process ${\mathrm {loc}}\big [ Q\big ]$, keeping the behavior of ${\mathrm {loc}}$ unchanged and consuming the update.

In general, update processes may define adaptation for locations enclosing more than one session channel. In the distributed buyer-seller example, the process below defines a runtime update which depends on the current state of the two channels at location ${\mathrm {sys}}$:

$$\begin{aligned} U_{xy} = {{\mathrm {sys}}\,\Bigg \{ \mathsf {case\,}x,y\, \mathsf {of} {\left\{ \begin{aligned} (x{:}\alpha \,;\, y{:}\beta )&: {\mathrm {buyer}}[R] \mathord {\;\varvec{|}\;}{\mathrm {seller}}[Q] \\ (x{:}\alpha ^{}_{\mathtt {pay}} \,;\, y{:}\beta ^{}_{\mathtt {pay}})&: {\mathrm {buyer}}[ P^*] \mathord {\;\varvec{|}\;}{\mathrm {seller}}[ Q^*] \end{aligned}\right\} } \Bigg \}} \end{aligned}$$

(1)

$U_{xy}$ defines two possibilities for runtime adaptation. If the protocol has just been established (i.e., current types are $\alpha$ and $\beta$) then only the buyer is updated—its new behavior will be given by R above. If both item and price information have been already exchanged then implementations $P^*$ and $Q^*$, compliant with types $\alpha _{\mathtt {pay}}$ and $\beta _{\mathtt {pay}}$, are installed.

Update processes rely on the protocol state at a given location to assess the suitability of adaptation routines. Our semantics for update relies on (a) monitors which store the current type for each running session; and (b) a type-directed test on the monitors enclosed in a given location. This test generalizes the $\mathtt {typecase}$ construct in [11].

While expressive, our typeful update processes by themselves do not specify when adaptation should be available. Even though update processes could be embedded within session communication prefixes (thus creating causal dependencies between communication and adaptation), such a specification style would only allow to handle exceptional conditions which can be fully characterized in advance. Other kinds of exceptional conditions, in particular contextual and/or unsolicited runtime conditions, are much harder to express by interleaving update processes within structured protocols.

To offer a uniform solution to this issue, we propose a event-based approach to trigger updates. We endow each location with a queue of adaptation requests; such requests may be internal or external to the location. In our example, an external request could be, e.g., a warning message from the buyer’s bank indicating that an exchange with the bank is required before committing to the purchase with the seller.

Location queues are independent from session behavior. Their identity is visible to processes; they are intended as interfaces with other processes and the environment. To issue an adaptation request r for location ${\mathrm {loc}}$, our process syntax includes adaptation signals, written ${\overline{{\mathrm {loc}}}}( r )$. Similar to ordinary communication prefixes, these signals are orthogonal to sessions. Then, we may detect the presence of request r in the queue of ${\mathrm {loc}}$ using the arrival predicate $\mathsf {arrive}({\mathrm {loc}}, r)$ [11]. As an example, let $\mathtt {upd}_E$ denote an external adaptation request. To continuously check if an external request has been queued for ${\mathrm {sys}}$, the process below combines process $U_{xy}$ in (1) with arrival predicates, conditionals, and recursion:

$$\begin{aligned} U^*_{xy} = \mu \mathcal {X}.\mathsf {if}~ \mathsf {arrive}({\mathrm {sys}}, \mathtt {upd}_E) ~\mathsf {then}~ U_{xy} ~\mathsf { else }~\mathcal {X} \end{aligned}$$

(2)

We couple our process model for session-based concurrency and runtime adaptation with a type system that ensures the following key properties:

• Safety: well-typed programs do not exhibit communication errors (e.g., mismatched messages).

• Consistency: well-typed programs do not allow adaptation actions that disrupt already established sessions.

Safety is the typical guarantee expected from any session type discipline, here considered in a richer setting that combines session communication with runtime adaptation. In contrast, consistency is a guarantee unique to our setting: it connects the behavior of the adaptation mechanisms with the preservation of prescribed typed interfaces. We show that well-typed programs are safe and consistent (Theorem 3.6): this ensures that specified session protocols are respected, while forbidding incautious adaptation steps that could accidentally remove or disrupt the session behavior of interacting partners.

Organization. The rest of the paper is organized as follows. Next we present our event-based process model of session communication with typeful constructs for runtime adaptation (Sect. 2). Then, we present our session type system, which ensures safety and consistency for processes with adaptation mechanisms (Sect. 3). In Sect. 4 we discuss a process model of communication and adaptation with explicit compartments; it distills the main features of the model in Sect. 2. At the end, we discuss related works and draw some concluding remarks (Sect. 5). The appendix gives full sets of reduction and typing rules. Additional technical details and omitted definitions can be found in an online technical report [5].

2 The Process Model: Syntax and Semantics

Syntax. We rely on base sets for names, ranged over by $u, a, b \ldots$; (session) channels, ranged over by $k, \kappa ^p, \ldots$, with polarity $p \in \{+,-\}$; labels, ranged over by $n, n', \ldots$; and variables, ranged over by $x, y, \ldots$. Values, ranged over $v, v', \ldots$, may include booleans (written $\mathtt {false}$ and $\mathtt {true}$), integers, names, and channels. We use r to range over adaptation messages: two instances are $\mathtt {upd}_I$ and $\mathtt {upd}_E$, for internal and external requests. We use $\,\widetilde{\cdot }\,$ to denote finite sequences. Thus, e.g., $\widetilde{x}$ is a sequence of variables $x_1, \ldots , x_n$. We use $\epsilon$ to denote the empty sequence.

Table 1 reports the syntax of expressions and processes. Processes include usual constructs for input, output, and labeled choice. Common forms of recursion, parallel composition, conditionals, and restriction are also included. As illustrated in Sect. 1, constructs for session establishment are annotated with a session type $\alpha$, which is useful in derived static analyses. A prefix for closing a session, inherited from [8], is convenient to structure specifications. Variable x is bound in processes $\overline{u}(x{:}\alpha ).P$, $u(x{:}\alpha ).P$, and $k(x).P$. Binding for name and channel restriction is as usual. Also, recursion variable $\mathcal {X}$ is bound in process $\mu \mathcal {X}.P$. Given a process P, its sets of free/bound channels, names, variables, and recursion variables—noted $\mathsf {fc}(P)$, $\mathsf {fn}(P)$, $\mathsf {fv}(P)$, $\mathsf {fpv}(P)$, $\mathsf {bc}(P)$, $\mathsf {bn}(P)$, $\mathsf {bv}(P)$, and $\mathsf {bpv}(P)$, respectively—are as expected. We always rely on usual notions of $\alpha$-conversion and (capture-avoiding) substitution, denoted (for channels) and (for processes). We write to stand for an n-ary simultaneous substitution. Processes without free variables or free channels are called programs.

Table 1. Process syntax. Above, annotation $\alpha$ denotes a session type.

Up to here, the language is a synchronous $\pi$-calculus with sessions. Building upon locations ${\mathrm {loc}}, {\mathrm {l_1}}, {\mathrm {l_2}}, \ldots$, constructs for adaptationare: located processes, denoted ${\mathrm {loc}}[P]$; update processes, denoted ${\mathrm {loc}}\big \{\mathsf {case}\,x_1, \ldots , x_m\,\mathsf {of}\,\{({x_{1}^{}{:}\beta _{1}^{i}; \cdots ;x_{m}^{}{:}\beta _{m}^{i}}):Q_i\}_{i \in I}\big \}$; (session) monitors, denoted $\kappa ^p\lfloor \alpha \rfloor$; location queues, denoted ${\mathrm {loc}}\lfloor \widetilde{r}\rfloor$; and adaptation signals, denoted ${\overline{{\mathrm {loc}}}}( r )$. Moreover, expressions include the arrival predicate $\mathsf {arrive}({\mathrm {loc}}, r)$.

We now comment on these elements. Located processes and update processes have been motivated in Sect. 1. Here we just remark that update processes are assumed to refer to at least one variable $x_i$ and to offer at least one alternative $Q_i$. Also, variables $x_1, \ldots , x_m$ are bound in ${\mathrm {loc}}\big \{\mathsf {case}\,x_1, \ldots , x_m\,\mathsf {of}\,\{({x_{1}^{}{:}\beta _{1}^{i}; \cdots ;x_{m}^{}{:}\beta _{m}^{i}}):Q_i\}_{i \in I}\big \}$; this process is often abbreviated as ${\mathrm {loc}}\big \{\mathsf {case}\,\widetilde{x}\,\mathsf {of}\,\{({x_{1}^{}{:}\beta _{1}^{i}; \cdots ;x_{m}^{}{:}\beta _{m}^{i}}):Q_i\}_{i \in I}\big \}$. Update processes generalize the $\mathtt {typecase}$ introduced in [11], which defines a case-like choice based on a single channel; in contrast, to specify adaptation for locations with multiple open sessions, our update processes define type-directed checks over one or more channels.

Update processes go hand-in-hand with monitors, runtime entities which keep the current protocol state at a given channel. We write $\kappa ^p\lfloor \alpha \rfloor$ to denote the monitor which stores the protocol state $\alpha$ for channel $\kappa ^p$. In [11], a similar construct is used to store in-transit messages in asynchronous communication. For simplicity, here we consider synchronous communication; monitors store only the current protocol state. This choice is aligned with our goal of identifying the core elements from the eventful session framework that are central in defining runtime adaptation (cf. Remark 3.7).

Location queues, not present in [11], handle adaptation requests, modeled as a possibly empty sequence of messages $\widetilde{r}$. Location queues enable us to give a unified treatment to adaptation requests, internal and external. Given ${\mathrm {loc}}\lfloor \widetilde{r}\rfloor$, it is worth observing that messages $\widetilde{r}$ are not related to communication as abstracted by session types. This represents the fact that we handle adaptation requests and structured session exchanges as orthogonal issues. An adaptation signal ${\overline{{\mathrm {loc}}}}( r )$ enqueues request r into the location queue of ${\mathrm {loc}}$. To this end, as detailed below, the operational semantics defines synchronizations between adaptation signals and location queues. To connect runtime adaptation and communication, our language allows the coupling of update processes with the arrival predicate on locations, denoted $\mathsf {arrive}({\mathrm {loc}}, r)$. Inspired by the $\mathtt {arrive}$ predicate in [11], this predicate detects if a message r has been placed in the queue of ${\mathrm {loc}}$.

Our language embodies several concerns related to runtime adaptation: using adaptation signals and location queues we may formally express how an adaptation request is issued; arrival predicates enable us to specify when adaptation will be handled; using update processes and monitors we may specify what is the goal of an adaptation event.

Table 2. Reduction semantics: selected rules. Both $\alpha$ and $\beta$ denote session types.

Semantics. The semantics of our language is given by a reduction semantics, the smallest relation generated by the rules in Table 5 (Appendix A). We write $P \longrightarrow P'$ for the reduction from P to $P'$. Reduction relies on a standard notion of structural congruence, denoted $\equiv$ (see [8, Def. 1]). It also relies on evaluation and location contexts:

$$\begin{aligned} \mathsf {E} :\,\!:= - \ \mid \ {\overline{k}}( \mathsf {-} ).P \ \mid \ \mathsf {if}~ \mathsf {-} ~\mathsf {then}~ P ~\mathsf { else }~Q \qquad \quad C,D :\,\!:= - \ \mid \ {\mathrm {loc}}[C \mathord {\;\varvec{|}\;}P] \end{aligned}$$

Given $C\big \{\!\!-\!\!\big \}$ (resp. $\mathsf {E}[-]$), we write $C\big \{P\big \}$ (resp. $\mathsf {E}[e]$) to denote the process (resp. expression) obtained by filling in occurrences of hole − in C with P (resp. in $\mathsf {E}$ with e).

Table 2 gives a selection of reduction rules; we comment on these rules below. The first four rules formalize session behavior within hierarchies of nested locations. Using duality for session types, denoted $\,\bot _{\mathtt {C}}\,$ (see [7] and Sect. 3), in rule $\langle {\textsc {r:Open}}\rangle$ the synchronization on a name u leads to establish a session on fresh channels $\kappa ^p$ and $\kappa ^{\overline{p}}$; also, two monitors with the declared session types are created. Duality for polarities p is as expected: $\overline{+} = -$ and $\overline{-} = +$. Monitors are local by construction: they are created in the same contexts in which the session is established. Rule $\langle {\textsc {r:Com}}\rangle$ represents communication of a value: we require both complementary prefixes and that the monitors support input and output actions. After reduction, prefixes in processes and monitors are consumed. Similarly, rule $\langle {\textsc {r:Sel}}\rangle$ for labeled choice is standard, augmented with monitors. Rule $\langle {\textsc {r:Clo}}\rangle$ formalizes session termination, discarding involved monitors. The monitors in these three rules allow us to track the evolution of active session protocols.

The remaining rules in Table 2 define our event-based approach to runtime adaptation. Rule $\langle {\textsc {r:UReq}}\rangle$ treats the issue of an adaptation request r as a synchronization between a location queue and an adaptation signal. The queue and the signal may be in different contexts; this enables “remote” requests. Rules $\langle {\textsc {r:Arr1}}\rangle$ and $\langle {\textsc {r:Arr2}}\rangle$ resolve arrival predicates by querying the (possibly remote) queue $\widetilde{r}$. Rule $\langle {\textsc {r:Upd}}\rangle$ defines the typeful update of the current protocol state at ${\mathrm {loc}}$, which is given by an indexed set of open sessions with their associated monitors. The rule attempts to match such protocol state with the first suitable option offered by an update process for ${\mathrm {loc}}$. If there is no matching alternative the current protocol state at ${\mathrm {loc}}$ is kept unchanged. By an abuse of notation, we write $P_1 \in P$ to indicate that $P_1$ occurs in P, i.e., if $P = C[P_1]$ for some C. Formally, given an index set I over the update process, suitability with respect to the behavior at ${\mathrm {loc}}$ is defined by predicate $\mathsf {match}_I$ in Definition 2.1 below. Using subtyping $\le _{\mathtt {C}}$ (see [7] and Sect. 3), the predicate holds for an $l \in I$ which defines a new protocol state.

In addition to the rules in Table 2, our semantics includes standard and/or self-explanatory treatments for reduction under evaluation contexts, parallel composition, located context, and restriction. Also, it accounts for applications of structural congruence, recursion and conditionals. The full set of rules is in Table 5 (Appendix A).

Definition 2.1

(Matching). Given an index set I, session types $\alpha _1, \ldots , \alpha _m$, an indexed sequence of session types $\{\beta _1^i, \ldots , \beta _m^i\}_{i \in I}$, and an $l \in I$, we write

$$\begin{aligned} \mathsf {match}_I(l,\, \{\alpha _1, \ldots , \alpha _m\} ,\, \{\beta _1^i, \ldots , \beta _m^i\}_{i \in I}) \end{aligned}$$

if and only if $\forall n < l.(\exists j \in [1..m].~\beta ^{n}_j \not \le _{\mathtt {C}} \alpha _j) \wedge (\bigwedge _{h \in [1..m]} \beta ^{l}_h \le _{\mathtt {C}} \alpha _h)$.

Example 2.2

Recall process W given in the Introduction. According to our semantics:

Suppose that following an external request the seller must offer a new payment method. (a gift card). Precisely, we would like $\mathtt {S}$ to act according to the type $\beta _{\mathtt {gift}}$ given in Sect. 1. Let $\alpha _{\mathtt {gift}}$ be the dual of $\beta _{\mathtt {gift}}$. We then may define the following update process $R^1_{xy}$:

$$\begin{aligned} {{\mathrm {sys}}\big \{\mathsf {case}\,{x,y}\,\mathsf {of}\,\{(x{:}\alpha ^{}_{\mathtt {pay}} \,;\, y{:}\beta ^{}_{\mathtt {pay}}):{\mathrm {buyer}}\big [ P' \mathord {\;\varvec{|}\;}x\lfloor \alpha _{\mathtt {gift}}\rfloor \big ] \mathord {\;\varvec{|}\;}{\mathrm {seller}}\big [Q'' \mathord {\;\varvec{|}\;}y\lfloor \beta _{\mathtt {gift}}\rfloor \big ] \}_{}\big \}} \end{aligned}$$

Thus, $R^1_{xy}$ keeps the expected implementation for the buyer ($P'$), but updates its associated monitor. For the seller, both the implementation and monitor are updated; above, $Q''$ stands for a process offering the three payment methods. We may then specify the whole system as: $W \mathord {\;\varvec{|}\;}\mu \mathcal {X}.\mathsf {if}~ \mathsf {arrive}({\mathrm {sys}}, \mathtt {upd}_E) ~\mathsf {then}~ R^1_{xy} ~\mathsf { else }~\mathcal {X}$. The type system introduced next ensures, among other things, that updates such as $R^1_{xy}$ consider both a process and its associated monitors, ruling out the possibility of discarding the monitors that enable reduction.

3 Session Types for Eventful Runtime Adaptation

This section introduces a session type system for the process language of Sect. 2. Our main result (Theorem 3.6) is that well-typed programs enjoy both safety (absence of runtime communication errors) and consistency properties (update actions do not disrupt established sessions). Our development follows the lines of the typed framework in [8].

The syntax of session types (ranged over by $\alpha , \beta , \ldots$) has been already presented in the Introduction. We consider basic types (ranged over by $\tau , \sigma , \ldots$) and write $T, S, \ldots$ to range over $\tau , \alpha$. Therefore, although our process language copes with runtime adaptation, our type syntax is standard and retains the intuitive meaning of session types [9], which we now briefly recall. Type $?({\tau }).\alpha$ (resp. $?(\beta ).\alpha$) abstracts the behavior of a channel which receives a value of type $\tau$ (resp. a channel of type $\beta$) and then continues as $\alpha$. Dually, type $!({\tau }).\alpha$ (resp. $!(\beta ).\alpha$) represents the behavior of a channel which sends a value of type $\tau$ and then continues as $\alpha$. Type $\,\! \& \{n_1:\alpha _1 \dots n_m:\alpha _m \}$ describes a branching behavior: it offers m behaviors, and if the j-th alternative is selected then it behaves as described by type $\alpha _j$ ($1 \le j \le m$). In turn, type $\oplus \{n_1:\alpha _1 \dots n_m:\alpha _m \}$ describes the behavior of a channel which may select a single behavior among $\alpha _1, \ldots , \alpha _m$ and then continues as $\alpha _j$. We use $\varepsilon$ to type a channel with no communication behavior. Type $\mu t.\alpha$ describes recursive behavior; as usual, we consider recursive types under equi-recursive and contractive assumptions.

Along the paper we have informally appealed to duality and subtyping over session types (denoted $\,\bot _{\mathtt {C}}$ and $\le _{\mathtt {C}}$, resp.). For the sake of space, we omit their full definitions; we just remark that since our session type structure is standard, we may rely on the (coinductive) definitions given by Gay and Hole [7], which are standard and well-understood.

Our typing judgments generalize usual notions with an interface $\mathcal {I}$. Based on the syntactic occurrences of session establishment prefixes $\overline{a}(x{:}\alpha )$, and $a(x{:}\alpha )$, the interface of a process describes the services appearing in it. We annotate services with a qualification $\mathsf {q}$, which may be ‘$\mathsf {lin}$’ (linear) or ‘$\mathsf {un}$’ (unrestricted). Thus, the interface of a process gives an “upper bound” on the services that it may execute. The typing system uses interfaces to control the behavior contained by locations after an update. We have:

Definition 3.1

(Interfaces). We define an interface as the multiset whose underlying set of elements is $\mathrm {I} = \{ \mathsf {q}\,u{:}\alpha ~|~ \mathsf {q}\in \{\mathsf {lin}, \mathsf {un}\}\}$ (i.e., a set of assignments from names to qualified session types). We use $\mathcal {I}, \mathcal {I}', \ldots$ to range over interfaces. We write $dom(\mathcal {I})$ to denote the set $\{u \mid u:\alpha _\mathsf {q}\in \mathcal {I}\}$ and $\#_\mathcal {I}(a) = h$ to mean that a occurs h times in $\mathcal {I}$.

The union of two interfaces is essentially the union of their underlying multisets. We sometimes write $\mathcal {I}\uplus a:\alpha _\mathsf {lin}$ and $\mathcal {I}\uplus a:\alpha _\mathsf {un}$ to stand for $\mathcal {I}\uplus \{\mathsf {lin}\,a{:}\alpha \}$ and $\mathcal {I}\uplus \{\mathsf {un}\,a{:}\alpha \}$, respectively. Moreover, we write $\mathcal {I}_\mathsf {lin}$ (resp. $\mathcal {I}_\mathsf {un}$) to denote the subset of $\mathcal {I}$ involving only assignments qualified with $\mathsf {lin}$ (resp. $\mathsf {un}$). We now define an ordering relation over interfaces, relying on subtyping:

Definition 3.2

(Interface Ordering). Given interfaces $\mathcal {I}$ and $\mathcal {I}'$, we write $\mathcal {I}\sqsubseteq \mathcal {I}'$ iff

• 1. $\forall (\mathsf {lin}\,a{:}\alpha )$ such that $\#_{\mathcal {I}_\mathsf {lin}}(\mathsf {lin}\,a{:}\alpha ) = h$ with $h > 0$, then one of the following holds:

  • (a) there exist h distinct elements $(\mathsf {lin}\,a{:}\beta _i) \in \mathcal {I}'_\mathsf {lin}$ such that $\alpha \le _{\mathtt {C}} \beta _i$ for $i \in [1..h]$;

  • (b) there exists $(\mathsf {un}\,a{:}\beta ) \in \mathcal {I}'_\mathsf {un}$ such that $\alpha \le _{\mathtt {C}} \beta$.

• 2. $\forall (\mathsf {un}\,a{:}\alpha ) \in \mathcal {I}_\mathsf {un}$ then $(\mathsf {un}\, a{:}\beta ) \in \mathcal {I}'_\mathsf {un}$ and $\alpha \le _{\mathtt {C}} \beta$, for some $\beta$.

Table 3. Well-typed processes: selected rules.

We now define our typing environments. We write $\mathsf {q}$ to range over qualifiers $\mathsf {lin}$ and $\mathsf {un}$.

$$\begin{aligned} \begin{array}{lclr} \varDelta &{} :\,\!:= &{} \emptyset \ \mid \ \varDelta , k:\alpha \ \mid \ \varDelta , k:\lfloor \alpha \rfloor &{} \text {typing with active sessions} \\ \varGamma &{}:\,\!:= &{} \emptyset \ \mid \ \varGamma , e:\tau \ \mid \ \varGamma , u:\langle \alpha _\mathsf {q}, \beta _\mathsf {q}\rangle \quad &{} \text {first-order environment (with }\alpha _\mathsf {q}\,\bot _{\mathtt {C}}\,\beta _\mathsf {q}\text {)} \\ \varTheta &{}:\,\!:= &{} \emptyset \ \mid \ \varTheta ,\mathcal {X}:\varDelta ;\mathcal {I} \ \mid \ \varTheta ,{\mathrm {loc}}:\mathcal {I}\quad &{} \text {higher-order environment} \end{array} \end{aligned}$$

We consider typings $\varDelta$ and environments $\varGamma$ and $\varTheta$. Typing $\varDelta$ collects assignments from channels to session types; it describes currently active sessions. In our system, $\varDelta$ also includes bracketed assignments, denoted $\kappa ^p:\lfloor \alpha \rfloor$, which represent the type for monitors. Subtyping extends to these assignments ($\lfloor \alpha \rfloor \le _{\mathtt {C}} \lfloor \beta \rfloor$ if $\alpha \le _{\mathtt {C}} \beta$) and thus to typings. We write $dom(\varDelta )$ to denote the set $\{ k^p \mid k^p:\alpha \in \varDelta \vee k^p:\lfloor \alpha \rfloor \in \varDelta \}$. We write $\varDelta , k:\alpha$ where $k \not \in dom(\varDelta )$. Furthermore, we write $\varDelta , k:\langle \!\langle \alpha \rangle \!\rangle$ to abbreviate $\varDelta , k:\alpha , k:\lfloor \alpha \rfloor$. That is, $k:\langle \!\langle \alpha \rangle \!\rangle$ describes both a session and its associated monitor.

$\varGamma$ is a first-order environment which maps expressions to basic types and names to pairs of qualified session types. As motivated earlier, a session type is qualified with ‘$\mathsf {un}$’ if it is associated to a unrestricted/persistent service; otherwise, it is qualified with ‘$\mathsf {lin}$’. The higher-order environment $\varTheta$ collects assignments of typings to process variables and interfaces to locations. While the former concerns recursive processes, the latter concerns located processes. As we explain next, by relying on the combination of these two pieces of information the type system ensures that runtime adaptation actions preserve the behavioral interfaces of a process. We write $vdom(\varTheta )= \{ \mathsf {X} \mid \mathsf {X}:\mathcal {I}\in \varTheta \}$ to denote the variables in the domain of $\varTheta$. Given these environments, a type judgment is of form

$$\begin{aligned} \varGamma \,;\, \varTheta \vdash P\triangleright \varDelta ;\mathcal {I} \end{aligned}$$

meaning that, under environments $\varGamma$ and $\varTheta$, process P has active sessions declared in $\varDelta$ and interface $\mathcal {I}$. Selected typing rules are shown in Table 3; remaining rules can be found in Table 6 (Appendix B). Below we comment on some of the rules in Table 3: the rest are standard and/or self explanatory. Rule $\langle {\textsc {t:Adapt}}\rangle$ types update processes. Notice that the typing rule ensures that each process $Q_i$ has exactly the same active sessions that those declared in the respective case. Also, we require that alternatives contain both processes and monitors. With $\mathcal {I}_j \sqsubseteq \mathcal {I}$ we guarantee that the process behavior does not “exceed” the expected behavior within the location. Rule $\langle {\textsc {t:sub}}\rangle$ takes care of subtyping both for typings $\varDelta$ and interfaces. Rule $\langle {\textsc {t:CRes}}\rangle$ types channel restriction that ensures typing duality among partners of a session and their respective queues. Typing of queues is given by rule $\langle {\textsc {t:Que}}\rangle$ that simply assigns type $k:\lfloor \alpha \rfloor$ to queue $k\lfloor \alpha \rfloor$. Finally, rule $\langle {\textsc {t:NRes}}\rangle$ types hiding of service names, by simply removing their declarations from the interface $\mathcal {I}$ of the process. In the rule, $\mathcal {I}_u$ contains only declarations for u, i.e., $\forall v\ne u, v\notin \mathrm {dom}(\mathcal {I}_u)$.

Our type system enjoys the standard subject reduction property. We rely on balanced typings: $\varDelta$ is balanced iff for all $\kappa ^p:\alpha \in \varDelta$ (resp. $\kappa ^p:\lfloor \alpha \rfloor \in \varDelta$) then also $\kappa ^{\overline{p}}: \beta \in \varDelta$ (resp. $\kappa ^{\overline{p}}: \lfloor \beta \rfloor \in \varDelta$), with $\alpha \,\bot _{\mathtt {C}}\,\beta$. The proof proceeds by induction on the last rule applied in the reduction; it adapts the one given in [8].

Theorem 3.3

(Subject Reduction). If $\varGamma \,;\, \varTheta \vdash P\triangleright \varDelta ;\mathcal {I}$ with $\varDelta$ balanced and $P \longrightarrow Q$ then $\varGamma \,;\, \varTheta \vdash Q\triangleright \varDelta ';\mathcal {I}'$, for some $\mathcal {I}'$ and balanced $\varDelta '$.

We now define and state safety and consistency properties. While safety guarantees adherence to prescribed session types and absence of runtime errors, consistency ensures that sessions are not jeopardized by careless runtime adaptation actions. Defining both properties requires the following notions of $\kappa$ -processes, $\kappa$ -redexes, and error process.

Definition 3.4

( $\kappa$ -processes, $\kappa$ -redexes, Errors). A process P is a $\kappa$ -process if it is a prefixed process with subject $\kappa ^p$, i.e., P is one of the following:

$$\begin{aligned} \kappa ^{\,p}(x).P' \qquad {\overline{\kappa }^{\,p}}( v ).P' \qquad \mathsf {close}\,(\kappa ^{\,p}).P' \qquad \kappa ^{\,p}\triangleright \{n_i{:}P_i\}_{i \in I} \qquad \kappa ^{\,p}\triangleleft n.P' \end{aligned}$$

Process P is a $\kappa$ -redex if it contains the composition of exactly two $\kappa$-processes with opposing polarities. P is an error if $P \equiv (\nu \widetilde{\kappa })(Q \mathord {\;\varvec{|}\;}R)$ where, for some $\kappa$, Q contains either exactly two $\kappa$-processes that do not form a $\kappa$-redex or three or more $\kappa$-processes.

Informally, a process P is called consistent if whenever it has a $\kappa$-redex then update actions do not destroy such a redex. Below, we formalize this intuition. Let us write $P \longrightarrow _{\text {upd}} P'$ for any reduction inferred using rule $\langle {\textsc {r:Upd}}\rangle$. We then define:

Definition 3.5

(Safety, Consistency). Let P be a process. We say P is safe if it never reduces into an error. We say P is update-consistent if and only if, for all $P'$ and $\kappa$ such that $P \longrightarrow ^{*} P'$ and $P'$ contains a $\kappa$-redex, if $P' \longrightarrow _{\text {upd}} P''$ then $P''$ contains a $\kappa$-redex.

We now state our main result; it follows as a consequence of Theorem 3.3.

Theorem 3.6

(Typing Ensures Safety and Consistency). If $\varGamma \,;\, \varTheta \vdash P\triangleright \varDelta ;\mathcal {I}$ with $\varDelta$ balanced then program P is update consistent and safe.

Remark 3.7

(Asynchronous Communication). We have focused on synchronous communication: this allows us to give a compact semantics, relying on a standard type structure. To account for asynchrony, we would require a runtime syntax for programs with queues for in-transit messages (values, sessions, labels). The type system must be extended to accommodate these new runtime processes. In our case, an extension with asynchrony would rely on the machinery defined in [11].

4 Discussion: A Compartmentalized Model of Communication and Adaptation

Given that the process model in Sect. 2 enables the interplay of communication and adaptation, how can we organize specifications to reflect a desirable separation of concerns? In ongoing work, with the aim of specifying systems at a high-level of abstraction, we have developed a model which defines compartments to isolate communication behavior and adaptation routines. Here we briefly describe this model, which is given in Table 4.

In a nutshell, programs of Sect. 2 are now organized into systems. A system G is the composition of a set of applications $A_1, \ldots , A_n$ each comprising three elements: a behavior R, a state $\mathsf {S}$, and a manager $\mathcal {M}$. As a simple example of a system, we may consider the operating system of a smartphone, which is meant to manage a number of applications that may interact among them. Applications in our model can communicate between each other or exhibit intra-application communication. The behavior R is specified as a process; we distinguish between located processes representing service definitions from located processes which make use of such definitions. A reduction semantics (omitted) ensures that locations enclosing service definitions do not contain open (active) sessions. This may be convenient for defining adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. The state $\mathsf {S}$ collects session monitors and location queues and it is kept separate from R. As a simple example, the buyer-seller scenario given in Sect. 1 can be casted in our model as

$$\begin{aligned} \mathsf {byr}\big \langle {\mathrm {buyer}}\big [\, \overline{u@\mathsf {slr}}(x:\alpha ).P\big ] \,;\, \mathsf {S_b}\,;\, \mathcal {M}_b\big \rangle \parallel \mathsf {slr}\big \langle {\mathrm {seller}}\big [ \!*u(y{:}\beta ).Q\big ] \,;\, \mathsf {S_s}\,;\, \mathcal {M}_s\big \rangle \end{aligned}$$

That is, buyer and seller are implemented as separate applications, named $\mathsf {byr}$ and $\mathsf {slr}$, respectively. Above, we have $\mathsf {S_b} = {\mathrm {buyer}}\lfloor \epsilon \rfloor$ and $\mathsf {S_s} = {\mathrm {seller}}\lfloor \epsilon \rfloor$.

While the manager $\mathcal {M}$ implements adaptation at the application (local) level, a handler $\mathcal {H}$ defines adaptation at the system (global) level. As we wish to describe communication behavior separately from adaptation routines, update processes are confined to handlers and managers. A manager is meant to react upon the arrival of an internal adaptation message $\mathtt {upd}_I$. As in Sect. 2, managers may act upon the issue of an internal update request $\mathtt {upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt {upd}_E$ and $\mathtt {upg}$, respectively). A handler may either $\mathtt {upd}$ate or $\mathtt {upg}$rade the behavior at some location ${\mathrm {loc}}$ within application a; this is written ${\mathrm {loc}}@a$. Upgrades are denoted ${\mathrm {l}}_1\big \{\!\!\big \{P\big \}\!\!\big \}$; they are a particular form of update intended for service definitions only. In Table 4 we write $*\mathsf {if}~ e ~\mathsf {then}~ P$ and $*u(x{:}\alpha ).P$ as shorthands for persistent conditionals and services, respectively.

Table 4. A compartmentalized model of communicating systems: syntax.

Our compartmentalized model induces specifications in which communication, runtime adaptation, and state (as in, e.g., asynchronous communication) are jointly expressed, while keeping a desirable separation of concerns. Notice that the differences between “plain” processes (as given in Sect. 2) and systems (as defined in Table 4) are mostly conceptual, rather than technical. In fact, the higher level of abstraction that is enforced by our model does not result in additional technicalities. We conjecture that a reduction-preserving translation of application-based specifications into processes does not exist—a main difficulty being, unsurprisingly, properly representing the separation between behavior and state. This difference in terms of expressiveness does not appear to affect the type system. In future work we plan to extend the typing discipline in Sect. 3 (and its associated safety and consistency guarantees) to systems.

5 Related Work and Concluding Remarks

Related Work. The combination of static typing and type-directed tests for dynamic reconfiguration is not new. For instance, Seco and Caires [14] study this combination for a calculus for object-oriented component programming. To the best of our knowledge, ours is the first work to develop this combination for a session process language. As already discussed, we build upon constructs proposed in [10–13]. The earliest works on eventful sessions, covering theory and implementation issues, are [10, 12]. Kouzapas’s PhD thesis [11] provides a unified presentation of the eventful framework, with case studies including event selectors (a building block in event-driven systems) and transformations between multithreaded and event-driven programs. At the level of types, the work in [11] introduces session set types to support the $\mathtt {typecase}$ construct. We use dynamic session type inspection only for runtime adaptation; in [11] $\mathtt {typecase}$ is part of the process syntax. This choice enables us to retain a standard session type syntax. Runtime adaptation of session typed processes—the main contribution of this paper—seems to be an application of eventful session types not previously identified.

Previous works on runtime adaptation for session types (binary and multiparty) include [1, 3, 8]. We have already commented on how our current approach enhances that in our previous work [8]. Both [1] and [3] study adaptation for multiparty communications, which already sets a substantial difference with respect to our work. In [3], a set of monitors which govern the behavior of participants are derived from a global specification. Self-adaptation for monitored processes is triggered by an external adaptation function, which is often left unspecified. As in our work, the operational semantics for adaptation in [3] uses (local) types and monitors; key differences include the use of type-directed checks for selecting adaptation routines that preserve consistency, and the use of events and queues to handle adaptation requests. The work [1] studies dynamic update for message passing programs; a form of consistency for updates over threads is ensured using multiparty session types, following an asynchronous communication discipline.

Concluding Remarks. Building upon [11], we have introduced an eventful approach to runtime adaptation of session typed processes. We identified the strictly necessary eventful process constructs that enhance and refine known mechanisms for runtime adaptation. Adaptation requests, both internal and external, are handled via event detectors and queues associated to locations. Our approach enables us to specify rich forms of updates on locations with running sessions; this represents a concrete improvement with respect to previous works [8]. We notice that expressing both internal and external exceptional events is useful in practice; for instance, both kinds of events coexist in BPMN 2.0 (see, e.g., [6, Chap. 4]). To rule out update steps that jeopardize running session protocols, we also introduced a type system that ensures communication safety and update consistency for session programs. We have also outlined a high-level model of structured interaction which organizes communication and adaptation components into a sensible structure.

Adaptation in our framework is “monotonic” or “incremental” in that changes always preserve/extend active session protocols, exploiting subtyping for enhanced flexibility. Interestingly, our framework can be modified so that arbitrary protocols are installed as a result of an update. One needs to ensure that the endpoints of a session are present in the same location: arbitrary updates are safe as long as both endpoints are simultaneously updated with dual protocols. To relax our framework in this way, we would need to modify definitions for session matching (Definition 2.1) and interface ordering (Definition 3.2).

In future work, we plan to further validate the constructs in our framework by revisiting the model of supervision trees (a mechanism for fault-tolerance in Erlang) that we gave in [4]. Other interesting topics for further development include accounting for asynchronous communication (cf. Remark 3.7) and extending our event-based approach to choreographic protocols; the framework in [3] may provide a good starting point.

Appendices

A Reduction Semantics: Full Set of Rules

Table 5 gives the full set of reduction semantics rules.

Table 5. Reduction semantics: Full set of rules. Above, $\alpha$ and $\beta$ denote session types.

B Type System: Additional Typing Rules

Table 6 gives additional typing rules for the system in Sect. 3.

Table 6. Additional typing rules.