Many distributed software systems are communication-centric: they are composed of heterogeneous software artifacts that interact following precise communication structures (protocols). One much-studied approach to system analysis equips process calculi with behavioral types (such as session types) so to abstract protocols and verify interacting programs. Unfortunately, existing behaviorally typed frameworks do not adequately support reactive behavior, an increasingly relevant feature in protocols. To address this shortcoming, We have been exploring how the synchronous programming paradigm can uniformly support the formal analysis of reactive, communication-centric programs. In this short communication, we motivate our approach and report on ongoing developments.
In this short note, we describe our ongoing work on a reactive programming model
for communication-centric software systems. While most previous work relies on
models based on the π-calculus [
In communication-centric software systems, collections of heterogeneous
software artifacts usually follow well-defined communication structures, or protocols.
Ensuring that programs conform to these protocols is key to certify system
correctness. One much-studied approach to the analysis of communicating programs
uses behavioral types [
Reliable Large-Scale Software Systems) and CNRS PICS project 07313 (SuCCeSS).
Copyright c by the paper’s authors. Copying permitted for private and academic
purposes.
types [
One shortcoming of existing implementations is that they are based on
overly rigid programming models. In particular, current practical support for
communication-centric software systems does not explicitly consider reactive
behavior in communicating programs. This is a crucial feature, especially as
autonomous agents can now engage into protocols in our behalf (e.g., financial
transactions). In fact, reactive behavior is central in realistic implementations
of protocols with, e.g., exception handling, dynamic reconfiguration, and time.
While these features can be represented in languages based on the π-calculus
(cf. e.g., [
To our knowledge, the amalgamation of reactive behavior into models of
structured communications has been little explored by previous works (see, e.g., [
Session types offer a type-based methodology to the validation of communicating
programs [
Receive a value of type T , continue as type/protocol S External choice among labeled types/protocols Ti (branching) Internal choice of a labeled type/protocol Tj , with j ∈ I (selection) Recursive protocol/type (with type variable X)
Terminated protocol In session-based concurrency, the notion of duality is key to ensure communication safety. Intuitively, duality relates session types with opposite behaviors: e.g., the dual of input is output, and vice versa; branching is the dual of selection, and vice versa.
We illustrate session types using a traditional example in the literature: the Buyer-Seller-Shipper protocol, which can be informally described as follows:
2. Seller replies back asking for Buyer’s unique address. 3. Buyer sends his address to Seller, confirming the order. 4. Seller forwards Buyer’s address to Shipper. 5. Shipper sends to Buyer the estimated delivery time. 6. Buyer confirms to Shipper his availability for receiving the item. We may formalize this protocol using the following session types: BuySell = !item.?confirmation.!address.end SellShip = !address.end
ShipBuy = !ETA.&{yes :!ok.end, no :!bye.end} where item, confirmation, address, and ETA denote basic types. Type BuySell describes interactions between Buyer and Seller from Buyer’s perspective. Similarly, SellShip describes an interaction from Seller’s perspective, and ShipBuy takes the standpoint of Shipper in communications. Complementary types can be obtained using duality. These three sessions take place in order, as in the informal description above. 3
The protocol presented before is well-suited for deployment using traditional technologies (e.g., web services). However, it does not consider the possibility of changes at runtime due to unexpected circumstances or external events. Moreover, the protocol is not suited to emerging scenarios in which protocol partners are deployed in, e.g., mobile devices with limited computational power and availability. For instance, it is easy to imagine Shipper being implemented by a drone with communication capabilities.
To address these shortcomings of protocol descriptions in session-based concurrency, we propose to use reactive behavior, as present in synchronous reactive programming. In this context, we can envision a reactive variant of the BuyerSeller-Shipper protocol, in which Shipper is a drone, and Buyer communicates from a mobile phone. In this variant of the protocol, the first six steps are as before; after Steps 1–6, an event from Buyer to Seller triggers the following protocol:
R2. Seller replies back confirming the modified order.
R3. Seller forwards the modified order to Shipper.
R4. Shipper replies back in one of the following ways: a) Shipper returns back to the store, picks up the new item, and confirms to Buyer the previously given estimated delivery time, or b) Shipper continues with the original order, and informs Buyer that the second item will be delivered separately.
That is, in the reactive Buyer-Seller-Shipper protocol some of the exchanges are “standard” or “default” (cf. Steps 1-6); there are also other exchanges that are executed as a reaction to some event or external circumstance (cf. Steps R1-R4). In the latter steps, the external event concerns the request by Buyer of modifying his order; other conceivable conditions include, e.g., drone malfunctioning and wrong/delayed package deliveries. These extra exchanges also constitute structured protocols, amenable to specification and validation using sessions; however, their occurrence can be very hard to predict.
Synchronous Reactive Programming and ReactiveML. Synchronous Reactive
Programming (SRP) is an event-based model of computation, optimized for
programming reactive systems [
ReactiveML is an SRP-based extension to the OCaml programming
language [
In ReactiveML, synchronization is based on signals: events that occur in one logical instant. Signals can trigger reactions in processes, to be executed instantaneously or in the next time unit. Signals can carry values and can be emitted from different processes in the same logical instant. There are three basic ReactiveML constructs: emit s v emits signal s with value v. await one s <e> in P awaits a value along signal s that is patternmatched to expression <e>. Process P is executed in the next instant. signal s in P declares signal s and bounds it to continuation
P.
Our Current Work: Structured Communications in SRP. Models of
communicationcentric systems (such as session types) usually rely on directed exchanges along
named channels. However, in SRP there is no native notion of channels: as we
have seen, signals are the main synchronization unit in ReactiveML. To deal with
this discrepancy, a key idea in our work is “simulating” channels using signals.
To this end, and since we would like to represent protocols respecting linearity,
we follow the representation of session channels in [
We describe our ReactiveML implementation for Seller in the reactive BuyerSeller-Shipper protocol. Recall that Seller is involved in two sessions: he first communicates with Client, then interactions with Shipper occur. In the code below we assume that all sessions have been already initiated; these are noted cb for Buyer and cs for Seller. let process seller conf = await one cb (item,y) in signal c1 in emit y (conf,c1);pause; await one c1 (addr,u) in signal c2 in emit cs (addr,c2);pause The code declares seller as a process in ReactiveML (a non-instantaneous function); we describe its body. The first line awaits a signal cb, which carries a pair of elements: a value and a reference to the signal where further interactions will occur (i.e., y). Then, a signal c1, where the next interaction will occur, is declared. Subsequently, a pair (containing a message conf and a reference to signal c1) is emitted over signal y; no further actions are taken in this time unit. Once the message is received by Buyer, seller awaits Buyer’s address. At this point, the first session has finished and communication with Shipper begins. In the last line, Buyer’s address is sent to Shipper.
Notice that once seller is finished, so is any communication from Seller. But in the reactive protocol, Seller must await possible further actions from either Buyer or Shipper. To implement this key feature, we extend the previous code with the following line of code: await one g (v,e) in P. This new line puts seller to “sleep" until an event/signal g from either Buyer or Seller triggers a new reaction P from it. Note that this signal for interrupts or events should be known to every party in the communication. The idea is then that the continuation process P should decide which course of action to take depending on the value carried by g. In our reactive protocol, process P could implement Steps R1-R4, following the implementation scheme of seller. 4
We have described our ongoing implementation of essential features of
sessionbased concurrency in ReactiveML, a reactive functional programming language.
Our implementation uses ReactiveML processes to handle usual session protocols
(send, receive, select, and branch constructs). We believe that our approach is
already on a par with other session implementations (such as [