Reo is a channel-based exogenous coordination language.
Reo is a channel-based exogenous coordination language in which complex coordinators, called connectors, are compositionally built out of simpler ones. Each connector in Reo imposes a specific coordination pattern on the entities (e.g., components) that connect to it. Thus, connectors essentially model the protocol or ‘glue code’ between components. The emphasis in Reo is on connectors and their composition only, not on the entities that connect to, communicate, and cooperate through these connectors.
Ideally, a complex system is a coordination of modular components. In such a system, components are not modified to match their particular environments: they only perform their dedicated functionality, facilitating their reuse.
Traditional software design tends to violate this principle in multiple ways. To illustrate, consider the pseudocode below, which represents a typical software design pattern. Assume that the send
and receive
operations are synchronous.
process P {
x <- doWork()
await signal
send x to Q
send signal to R
repeat
}
process Q {
y <- receive datum
doStuff(y)
repeat
}
process R {
x <- doThings()
send x to Q
send signal to P
await signal
repeat
}
The following set of observations applies to this example:
P
and R
explicitly target consumer
process Q
. If the data they produce is required by some other process, their definitions would have to be modified. Process Q
, by contrast, is properly modular: it requires an input to its doStuff()
operation, but otherwise makes no assumptions about its environment.What is the interaction between these processes? If we perform a careful analysis of each process, we will find that it is something along the following lines: process Q
alternatingly receives data from P
and R
, and the first datum it receives will be from P
.
In this case, the analysis was quite easy. But now imagine a scenario with:
It will no longer be so easy to determine, verify or reuse the protocol.
These three issues can be addressed as follows. First, we limit the admissible I/O operations for each component C
to putting and getting data from ports that now reside at the boundary of C
. In this case, we assume the existence of ports pOut
, qIn
and rOut
that reside at the boundaries of P
, Q
and R
, respectively:
process P {
x <- doWork()
put(x, pOut)
repeat
}
process Q {
y <- get(qIn)
doStuff(y)
repeat
}
process R {
x <- doThings()
put(x, rOut)
repeat
}
The assumptions about the environments are eliminated. But now these components do not interact! Ironically, this is a desirable outcome, because these totally agnostic components can now participate in any interaction pattern. In order to specify interaction patterns, we require a language to explicitly coordinate the alternating behaviour of these components. If modularity is to be preserved, this coordination must be performed from the outside, or exogenously.
Reo is such an exogenous coordination language. It has both a visual and a textual syntax. The visually defined Reo connector below is one way of specifying the desired protocol, in which P
is the top writer, R
is the bottom writer, and Q
is the reader:
We will consider the details of the Reo language later. For now, we trust that it is sufficiently convincing that the connector imposes the desired behaviour on the protocol-agnostic components.
Our solution demonstrates another important advantage of our approach: the protocol itself has become a distinguished software artefact. This fact facilitates both the reuse and verification of protocols. Vereofy is one particular example of how Reo has been leveraged for verification purposes.
Finally, we must address one important question. We have moved our protocol specification to a higher level of abstraction. How can one get back to executable code? The Reo design philosophy dictates that this gap between specification and implementation should – as much as possible – be closed by automated procedures. Much of our work revolves around this philosophy. We have, for instance, developed an extensible compiler that can already generate code for the Java programming language, the Promela modelling language, and more. Preliminary results, moreover, show that such generated code need not be slower than their hand-crafted counterparts, even if concurrency is involved [1,2]. While this may sound surprising, an analogy can be made between the performances of hand-crafted assembly code versus the output of today’s compilers for high-level programming languages. For non-trivial applications, a modern compiler’s output is bound to be more performant (and more likely to be correct) than the hand-crafted code. The crucial insight is that high-level specifications provide a sophisticated compiler more room for optimization.
We now give a more detailed (but non-technical) explanation of the Reo language. For a more formal account, see, for instance, [1].
A Reo application consists of a set of user-defined channels. Each channel has its own well-defined behaviour, representing a particular type of point-to-point communication. The ends of these channels can be joined to form nodes, resulting in a complex connector. The behaviour of such a connector is derived completely from the behaviour of its channels and the Reo-defined behaviour of nodes.
In this section, we first look at a set of channels that are usually considered in the context of Reo. Then, we explain the basic semantics of Reo nodes. Finally, we look at some examples of complex connectors that illustrate how Reo can be used to capture interesting protocols.
All animations in this section are derived from José Proença and David de Oliveira Costa’s Flash animations, which can be found here. Aside from being intuitively understandable, the colours used in the animations also have a precise meaning, as explained in the so-called colouring semantics for Reo [3].
A channel has two ends. An end is either a source end, which accepts data into the channel, or a sink end, which dispenses data from the channel. Each channel has a type, which is completely user-defined. The type fixes the channel ends, and imposes a particular constraint on the data flow through the channel.
In this section we consider a number of ‘standard’ channels, i.e., channels which are typically considered in the context of Reo.
A synchronous channel (or sync channel) has a source end and a sink end. It accepts a datum into its source end if and only if it can dispense it from its sink end. Thus, if a writer wishes to put
a datum at its source end, it is blocked until a reader gets
the datum from its sink end:
Similarly, a reader that wishes to get
a datum from the sink end is blocked until a writer puts
a datum at its source end:
If the reader and writer appear simultaneously, finally, neither is blocked:
A lossy synchronous channel (or lossy sync channel) is essentially a synchronous channel that always accepts data into its source end. If it cannot dispense the datum out of its sink end, the datum is lost. This is shown in the animation below, in which the writer appears before the reader:
In the other cases, the lossy synchronous channel behaves just like the synchronous channel.
The two channels we have considered so far do not have any buffering capabilities. The empty FIFO1 channel (also called the empty one slot buffer), by contrast, can store a single datum. Thus, when the writer appears before the reader, the datum is stored inside the buffer, which can then later be retrieved by the reader:
What should happen when the writer and reader appear at the same time? The default definition of the empty FIFO1 channel is asynchronous in that the datum is first accepted into the channel, and then dispensed:
An alternative synchronous definition is also possible, where the source and sink end become active in the same instance of time. In this case, the channel would then behave just like a synchronous channel.
A FIFO1 channel that is full is called a full FIFO1 channel. In some protocols it makes sense to initialize a FIFO1 channel to a full state, as we will see when we consider some complex connectors.
When the FIFO1 channel is full, any writer acting at the source end blocks until the datum has been dispensed:
The filter channel filters data that is put at its source end. If the datum does not pass the filter, it is lost immediately, even if no get
is pending on its sink end:
In all other cases, the filter behaves like a synchronous channel. For instance, a put
of a datum that passes the filter exhibits blocking behaviour:
The synchronous drain (or syncdrain) has two source ends. A put
at either end blocks until a put
is performed on the other end. Then, both data are lost in the channel:
If both put
requests are made simultaneously, then both data are lost simultaneously:
The asynchronous drain (or asyncdrain) is the asynchronous counterpart of the synchronous drain. A put
at either end succeeds immediately, and the datum is lost in the channel:
When two put
requests are performed simultaneously, then one put
is non-deterministically selected to succeed first (in this case, the left one):
The synchronous spout (or syncspout) is the dual of the synchronous drain. It has two sink ends. A get
at either end blocks until a get
is performed on the other end. Then, both sink ends dispense arbitrary data:
If both get
requests are performed simultaneously, then both ends dispense data simultaneously:
The asynchronous spout (or asyncspout) is the asynchronous counterpart of the synchronous spout. A get
performed at either sink end succeeds immediately, causing the end to dispense an arbitrary datum:
When two get
requests are performed simultaneously, then one get
is non-deterministically selected to succeed first (in the case, the left one):
Channel ends can be joined to construct complex connectors. The point at which channel ends are logically joined is called a node. We may distinguish between three types of nodes: a node at which only source ends are joined (a source node), a node at which only sink ends are joined (a sink node), and a node at which both source ends and sink ends are joined (a mixed node). Each type of node imposes a specific kind of behaviour on its coincident channels.
A source node acts like a replicator. Any datum that is put
at a source node is replicated through all of its coincident channels if and only if all of the channels can accept the datum.
A sink node acts like a merger. A get
that is performed at a sink node receives a datum from one of its offering coincident channels. If multiple channels can offer data, one channel is selected non-deterministically.
A mixed node acts like a pumping station, combining the behaviour of the merger for all sink ends with the replicator for all source ends.
For illustration purposes, we now consider a number of complex connectors that define useful protocols.
In the write-cue regulator below, a datum is sent from port A
to port B
only if an independent put
is performed at port R
. Thus, a process that connects to port R
acts as a regulator of the communication between the writer and the reader connecting to ports A
and B
, respectively.
The barrier below forces two writer-reader pairs to synchronize.
The barrier can be easily generalized to any number of writer-reader pairs by simply repeating the pattern downwards.
The alternator has two input ports A
and B
, and one output port C
. Port C
receives data from A
and B
in an alternating pattern (ABABAB...
), starting with the datum initially put
at port A
.
The exclusive router below ensures that a datum put
at port A
can be taken from either B
or C
, but not both. If get
requests are pending on both B
and C
, then the get
that succeeds is non-deterministically determined. In the animation below, it is port B
that is non-deterministically selected to go first.
The sequencer below moves a black token around, which can be alternatingly received through ports A
, B
and C
. Thus, the connector can be used to sequence processes that connect to these ports.
The inhibitor connector allows data to synchronously flow from port A
to port C
. When a datum is put at the inhibitor port I
, such data flow is no longer possible.
The or-selector has two input ports A
and B
, and one output port C
. Once a datum flows from port A
to C
, port B
will forever be inhibited. Similarly, if a datum flows from port B
to port C
, port A
will forever be inhibited.
This connector illustrates how compositionality can be scaled arbitrarily by treating complex connectors as black boxes.