Much research has studied foundations for correct and reliable communication-centric systems. A salient approach to correctness uses session types to enforce structured communications; a recent approach to reliability uses reversible actions as a way of reacting to unanticipated events or failures. This note describes recent work that develops a simple observation: the machinery required to define monitored semantics can also support reversible protocols. We illustrate a process framework of session communication in which monitors support reversibility. A key novelty in our approach are session types with present and past, which allow us to streamline the semantics of reversible actions.
The purpose of this short paper is to motivate and describe our ongoing work in
reversible models of structured communications [
Models of reversible computation and structured communications have
received much attention (cf. [
The key observation that underlies our work is that the design of casually consistent operational semantics for concurrent processes can take advantage of the structured protocols that typically govern their behavior. As session types abstract sequences of communication actions (protocols), they appear as a natural choice for recording the forward and backward actions of interacting processes.
In recent work, we have started to formalize the integration of reversibility
and session-based concurrency [
Our proposal builds upon the approach of models of concurrency such as the πcalculus. As such, main ingredients in our approach are configurations, processes, and (protocol) types, whose syntax is given in Figure 1. We assume a language of the expressions e, e0, . . . that includes basic values, variables, and functions on them. The syntax of configurations includes the empty configuration 0, name restriction νn.M , parallel composition M k N , but also running processes and monitors: – eAndrupnoni nintsg porcocucersrsingPi n· σP·. ueTesheisluoncaivlosctaolrlye iσdeinstiafieldistbyofs,ptahiersliostf otfhesesfosiromn e {x, ve} (i.e., a set of mappings from variables to values); the list u collects the subjects of actions already performed by P . e – Given a session name s, a monitor sbH · eec contains a protocol (session) type H that describes the structured behavior associated to s (see below) and a list e containing all the expressions (including variables) used by the process.
e Intuitively, the list u in the running process and the list e in the monitor will be e e used to record previously performed actions and reconstruct the process structure accordingly.
The design of the operational semantics for our model is inspired by the
approach of [
M, N ::= (processes) (actions) 0 |
P · σ · ue es | sbH · eec | νn.M | M k N P, Q ::=
u(x : S).P | uhx : Si.P | khei.P | k(x).P | νa.P | 0 α, β ::= !U | ?U (protocol types)
S, T ::= end | α.S (history types)
H, K ::=
^ S | S ^ | α1. · · · .αn. ^ S in keeping, rather than consuming, these monitor types. For this to work, we need to distinguish the part of the protocol that has been already executed (its past), from the protocol that still needs to execute (its present). We thus introduce session types with present and past (H in the syntax): the type α1. · · · .αn. ^ S says that actions α1, · · · , αn are past protocol actions, whereas actions in protocol S are yet to be executed. That is, the cursor ^ in history types helps us to distinguish the past from the present. Each action αi corresponds to the input or output of a value; we use U to range over the types of these values (e.g., int, str, etc.).
We illustrate our approach by means of a simple business protocol example [
Sa : ?str.!int.?str.?int.!cal.end Ta : !str.?int.!str.!int.?cal.end Sb : ?int.!int.end Tb : !int.?int.end Above, Sa describes the interaction between Buyer and Seller from Seller’s perspective; type Ta is its dual and describes the protocol from Buyer’s perspective. In session types, duality is essential to (statically) ensure action compatibility between partners (and therefore, to guarantee absence of communication errors). Types Tb and Sb describe the interaction between Buyer and Friend, from each perspective.
Having defined the interaction protocols using types, we proceed to examine some possible process implementations for Buyer, Seller, and Friend. The behavior of Buyer may be specified by the following process:
The implementation for Buyer involves the creation of two interleaved sessions: the first one is established with the prefix ahz : Tai, which explicitly mentions the session protocol to be executed with the implementation of Seller; the second session is established with the implementation of Friend through the prefix bhw : Tbi. Process implementations for Seller and Friend can be specified by the following processes: S e l l e r , a(z : Sa).z(title).zhquote(title)i.z(addr).z(paymnt).zhdate(addr)i.0
Note that functions loan(), quote() and date() are used to calculate the amount of money to be borrowed, the book price and the delivery date, respectively. The overall system specification is then given by the parallel composition of configurations containing the three processes (in what follows, denotes the empty list):
S y s t e m ,
B u y e r · · k S e l l e r · · k F r i e n d · · In the following, we will indicate with B u y e ri (resp. S e l l e ri and F r i e n di) the process B u y e r after performing its i-th action. We will do the same with types.
The operational semantics that we have defined in [
B u y e r1 · {z, s} · a s k sb ^ Ta · zc k S e l l e r1 · {z, s} · a s k sb ^ Sa · zc k F r i e n d · · (1) As we can see, once a session is established two monitors are created, one per endpoint; their task is to discipline the behavior of the process holding the endpoint. For example, the behavior of Buyer in session s has to obey type Sa. Buyer then sends (according to Sa) to Seller the request for the book, and the entire system evolves as:
B u y e r2 · ({z, s}) · a, z s k sb!str ^ Ta1 · z, “dune”c k
S e l l e r2 · ({z, s}, {title, “dune”}) · a, z s k sb?str ^ Sa1 · z, titlec k F r i e n d · · We can easily check that the configurations in (3) and (1) are equivalent. From M in (2) the interaction between Buyer and Seller goes on, and the system arrives to a point in which Buyer establishes a new session with Friend: M ∗(νs, s, r, r).
B u y e r4 · ({z, s}, {w, r}) · ue1, b s,r k rb ^ Tb · bc k sbTa0 ^ Ta3 · z, “dune”, prc, wc k
S e l l e r3 · ({z, s}, {title, “dune”}) · a, z, z s k sbSa0 ^ Sa3 · z, title, quote(title)c k
F r i e n d1 · {w, r} · b r k rb ^ Sb · wc As effect of the communication, both types register the action and move forward. Another effect is that the information needed to restore back the consumed prefixes is stored into the running configurations and the related monitors. Communication in (2) can be reverted by moving backward the monitor types, by restoring the prefixes and deleting the read value from the receiver store, that is: M
zh“dune”i.B u y e r2 · ({z, s} · a s k sb ^ !str.Ta1 · zc k z(title).S e l l e r2 · {z, s} · a s k sb ^ ?str.Sa1 · zc k F r i e n d · · As (4) shows, the running process for Buyer is present in two sessions: one with Seller and another one with Friend, and has two associated monitors, identified by endpoints s, r. The list of subjects stored into the running process allows us to reverse communications (possibly in different sessions) and session establishments in the order in which they were performed, thus respecting causality of actions. In this way, Buyer cannot undo a communication with Seller while the session with Friend is still established. 3
We have described recent work on the integration of reversible semantics and
session-based concurrency [