About

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.

• Why Reo?
• Reo: the language
  • Channels
  • Nodes
  • Examples of complex connectors

Why Reo?

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:

1. ‘Producer’ processes 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.

2. 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:

   • More process definitions.
   • The process definitions are more complicated, with nested loops containing if-statements whose complex conditions determine whether communication primitives execute, and where the conditions depend on the values of parameters, input variables or earlier communication. Such deep entanglement makes it more difficult to distinguish between what we may call a process’s ‘computation code’ and a process’s ‘communication code’.
   • The process definitions are written in different languages.
   • The process definitions are contained in different files, and may even be located on different systems.

   It will no longer be so easy to determine, verify or reuse the protocol.

3. The processes explicitly communicate through message passing. Is this essential to the protocol? Quite likely, it is not: if the processes are on the same system, it may be better to communicate through shared memory. Thus, the specification of a message passing protocol betrays an another assumption about the environment in which the processes are embedded.

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.

Reo: the language

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].

Channels

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.

Synchronous channel

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:

Lossy synchronous channel

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.

Empty FIFO1 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.

Full FIFO1 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:

Filter channel

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:

Synchronous drain

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:

Asynchronous drain

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):

Synchronous spout

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:

Asynchronous spout

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):

Nodes

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.

Source node: replicator

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.

Sink node: merger

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.

Mixed node: pumping station

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.

Examples of complex connectors

For illustration purposes, we now consider a number of complex connectors that define useful protocols.

Write-cue regulator

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.

Barrier

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.

Alternator

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.

Exclusive router

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.

Sequencer

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.

Inhibitor

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.

Or-selector

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.

References

1. Farhad Arbab. 2016. Proper Protocol. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, 65–87. doi:10.1007/978-3-319-30734-3_7
   
   
2. Sung-Shik Theodorus Quirinus Jongmans. 2016. Automata-theoretic protocol programming (PhD thesis). Centrum Wiskunde & Informatica (CWI), Faculty of Science, Leiden University. hdl:1887/38223
   
   
3. Dave Clarke, David Costa, and Farhad Arbab. 2006. Connector Colouring I: Synchronisation and Context Dependency. In Proceedings of FOCLASA 2005, Carlos Canal and Mirko Viroli (eds.). Elsevier, 101–119. doi:10.1016/j.entcs.2005.12.035