# ARx: Reactive Programming for Synchronous Connectors

José Proença, Guillermina Cledou

► To cite this version:

José Proença, Guillermina Cledou. ARx: Reactive Programming for Synchronous Connectors. 22th International Conference on Coordination Languages and Models (COORDINATION), Jun 2020, Valletta, Malta. pp.39-56, 10.1007/978-3-030-50029-0_3 . hal-03274003

HAL Id: hal-03274003

https://inria.hal.science/hal-03274003

Submitted on 29 Jun 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# ARx: Reactive Programming for Synchronous Connectors

José Proença<fnref n="1" /> and Guillermina Cledou<fnref n="2" />

**Abstract.** Reactive programming (RP) languages and Synchronous Coordination (SC) languages share the goal of orchestrating the execution of computational tasks, by imposing dependencies on their execution order and controlling how they share data. RP is often implemented as libraries for existing programming languages, lifting operations over values to operations over streams of values, and providing efficient solutions to manage how updates to such streams trigger reactions, i.e., the execution of dependent tasks. SC is often implemented as a standalone formalism to specify existing component-based architectures, used to analyse, verify, transform, or generate code. These two approaches target different audiences, and it is non-trivial to combine the programming style of RP with the expressive power of synchronous languages.

This paper proposes a lightweight programming language to describe component-based Architectures for Reactive systems, dubbed ARx, which blends concepts from RP and SC, mainly inspired to the Reo coordination language and its composition operation, and with tailored constructs for reactive programs such as the ones found in ReScala. ARx is enriched with a type system and with algebraic data types, and has a reactive semantics inspired in RP. We provide typical examples from both the RP and SC literature, illustrate how these can be captured by the proposed language, and describe a web-based prototype tool to edit, parse, and type check programs, and to animate their semantics.

## 1 Introduction

This paper combines ideas from reactive programming languages and from synchronous coordination languages into a new reactive language that both enriches the expressiveness of typical reactive programs and facilitates the usage of typical synchronous coordination languages.

**Reactive programming languages**, such as Yampa [14], ReScala [11], and Angular<fnref n="3" />, address how to lift traditional functions from concrete data values to streams of values. These face challenges such as triggering reactions when these streams are updated, while avoiding glitches in a concurrent setting (temporarily

<footnote n="1">¹ CISTER, ISEP, Portugal</footnote>

<footnote n="2">² HASLab/INESC TEC, Universidade do Minho, Portugal
pro@isep.ipp.pt, mgc@inesctec.pt</footnote>

<footnote n="3">³ https://angular.io/</footnote>
inconsistent results), distinguishing between continuous streams (always available) and discrete streams (publishing values at specific points in time), and avoiding the callback hell [15] resulting from abusing the observable patterns that mask interactions that are not explicit in the software architecture.

**Synchronous coordination languages**, such as Reo [2], Signal Flow Graphs [7], or Linda [9], address how to impose constraints over the interactions between software objects or components, restricting the order in which the interactions can occur, and where data should flow to. These face challenges such as how to balance the expressivity of the language—capturing, e.g., real-time [16], data predicates [18], and probabilities [3]—with the development of tools to implement, simulate, or verify these programs.

Both programs in Reactive Programming (RP) and Synchronous Coordination (SC) provide an architecture to reason about streams: how to receive incoming streams and produce new outgoing ones. They provide mechanisms to: (1) calculate values from continuous or discrete data streams, and (2) constrain the scheduling of parallel tasks. RP is typically more pragmatic, focused on extending existing languages with constructs that manage operations over streams, while making the programmer less aware of the stream concept. SC is typically more fundamental, focused on providing a declarative software layer that does not address data computation, but describes instead constraints over interactions that can be formally analysed and used to generate code.

This paper provides a blend of both worlds, by proposing a language—ARx— with a syntactic structure based on *reactive programs*, and with a semantics that captures the synchronisation aspects of *synchronous coordination programs*. This paper starts by providing a better context overview of reactive and synchronous programs (Section 2). It then introduces the toolset supporting ARx in Section 3, available both to use as a web-service<fnref n="4" /> or to download and run locally. The rest of the paper formalises the ARx language, without providing correctness results and focusing on the tools. It presents the core features of ARx in Section 4, introducing an intermediate language to give semantics to ARx of so-called stream-builders and providing a compositional encoding of ARx into stream-builders. Two extensions to ARx are then presented. The first consists of algebraic data types, in Section 5, making the data values more concrete. The second, in Section 6, enriches the syntax of ARx and of stream-builders, and introduces new rules to the operational semantics, to support the notion of reactivity.

## 2 Overview over reactive and synchronous programs

This section selects a few representative examples of reactive programs and of synchronous coordinators. It uses a graphical notation to describe these programs, partially borrowed from Drechsler et al. [11], and explains the core challenges addressed by both approaches.

<footnote n="4">⁴ http://arcatools.org/#arx</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 1: Example of typical Reactive Programs.</figcaption></figure>

**Reactive programs** Figure 1 includes 3 examples of reactive programs:

(top-left) A simple arithmetic computation, used by Bainomugisha et al. [5], with the program `c = a × b; d = a + c` using reactive variables.

(right) A controller of a fan switch for embedded systems, used by Sakurai et al. [19], with the program `di = 0.81 × tmp + 0.01 × hmd × (0.99 × tmp - 14.3) + 46.3; fan = di >= th; th = 75 + if fan@last then -0.5 else 0.5`.

(bottom-left) A GUI manager that selects which information to display, either from the continuous stream of mouse coordinates, or from the continuous stream of current time, with the program `disp = if sel then mouse else time`.

Consider the arithmetic computation example. It has 4 (reactive) variables, *a*, *b*, *c*, *d*, and the sources (depicted as triangles) may fire a new value. Firing a new value triggers computations connected by arrows; e.g., if *b* fires 5, the `×` operation will try to recompute a new product, and will update *c*, which in turn will fire its new value. So-called *glitches* can occur, for example, if *a* fires a value, and `+` is calculated with the old value of *c* (before `×` updates its value). Different techniques exist to avoid glitches, by either enforcing a scheduling of the tasks, or, in a distributed setting, by including extra information on the messages used to detect missing dependencies. Languages that support reactive programming often include operations to fire a variable (e.g., `a.set("abc")` in `ReScala`), to react to a variable update (e.g., `d observe(println)` in `ReScala`), to ask for a value to be updated and read (e.g., `d.now` in `ReScala`), and to read or update a value without triggering computations. Hence the effort is in managing the execution of a set of tasks, while buffering intermediate results, and propagate updates triggered by new data.

Consider now the fan controller. It includes a loop with dashed arrows, capturing the variable `fan@last`, i.e., the previous value of `fan`. This is a solution to handle loops, which are either forbidden or troublesome in RP. Consequently, the system must know the initial value of `fan` using a dedicated annotation.

Finally, consider the GUI example. This includes dashed triangles, which denote continuous streams of data (often refer to as *behaviour* in functional RP, as opposed to *signal*). This means that updates to the mouse coordinates or to the time passing do not trigger a computation. Here `sel` can fire a boolean
<figure><img src="image_3.png" /><figcaption>Figure 2: Example of typical Synchronous Coordinators: variations of an alternator.</figcaption></figure>

that will trigger data to flow from either *mouse* or *time* to *disp*. Furthermore, the computation may not depend on all of its inputs, as opposed to the other operations seen so far. Hence, the composing operation depends, at each phase, on either *mouse* or *time*, and not on both.

**Synchronous coordinators** Synchronous coordinators provide a finer control over the scheduling restrictions of each of the stream updates, as illustrated in the two examples of Figure 2. These represent different coordinators that have two inputs, *a* and *b*, and alternate their values to an output stream *o*. In RP a similar behaviour could be captured by "o = if(*aLast*) then *b* else *a*; *aLast* = not(*aLast@last*)". Using a synchronous coordinator, one can exploit synchrony and better control the communication protocol.

The coordinators of Figure 2 use the blocks `fifo`, `barrier`, and `altBarrier`, and may connect streams directly. Unlike RP, these connections are *synchronous*, meaning that all streams involved in an operation must occur atomically. E.g., each stream can fire a single message only if the connected block or stream is ready to fire, which in turn can only happen if all their outputs are ready to fire. In the left coordinator, the top *a* can output a message only if it can send it to both *o* and the `barrier`. This `barrier` blocks *a* or *b* unless both *a* and *b* can fire atomically. The `PIO` can buffer at most one value, blocking incoming messages when full. The left coordinator receives each data message from both *a* and *b*, sending the message from *a* to *c* atomically and buffering the value from *b*; later the buffered message is sent to *c*, and only then streams *a* and *b* can fire again. The right coordinator uses a `altBarrier` that alternates between blocking *a* and blocking *b*, and it buffers the value temporarily to avoid *o* from having to synchronise with *a* or *b*.

**Remarks** In SC data streams can fire only once, and do not store this value unless it is explicit in the coordinator. In RP, when a stream fires a value, this value is stored for later reuse – either by the sender or by the computing tasks, depending on the implementation engine. Also, the notion of synchronisation, describing sets of operations that occur atomically, is not common in RP, since RP targets efficient implementations of tasks that run independently.

The term *reactive* has also been applied in the context of *reactive systems* and *functional reactive systems*. The former addresses systems that react to incoming stimuli and are responsive, resilient, elastic and message driven, described
<figure><img src="image_4.png" /><figcaption>Figure 3: Screenshot of the widgets in the online tool for ARx programs.</figcaption></figure>

in the *Reactive Manifesto* [1]. The latter is a specific take on reactive programming based on functions over streams that distinguish (continuous) behaviour from (discrete) events [12]. Early work on synchronous languages for (real-time) reactive systems has been focused on safety-critical reactive control system, and includes synchronous programming and (synchronous) dataflow programming [5]. Similarly to synchronous coordination, synchronous languages such as Esperel [6] and StateCharts [13], assume that reactions are atomic and take no time, simplifying programs and allowing their representation as finite state machines which can be later translated into sequential programs.

## 3 ARx toolset

We implemented an open-source web-based prototype tool to edit, parse, and type check ARx programs, and to animate their semantics.<fnref n="5" /> These tools are developed in Scala, which is compiled to JavaScript using ScalaJS.<fnref n="6" /> This section starts by giving a quick overview on how to use the tools, using as running example a version of the GUI manager from Figure 1 in ARx. The toolset includes

<footnote n="5">5 http://arcatools.org/#arx</footnote>

<footnote n="6">6 https://www.scala-js.org</footnote>
several widgets, depicted in Figure 3: ① the editor to specify the program, ② the
architectural view of the program, ③ the type and semantic analysis of the
program, ④ a finite automaton capturing the reactive semantics of the program,
and ⑤ a set of predefined examples.

Most of the syntax in ① is introduced in Section 4. Variables, such as `mouse` and `time`, denote streams of data; line breaks are ignored; and the statements `"display←mouse display←time"` mean that the stream `display` merges the data from `mouse` and `display`. Extensions to the core syntax include (1) algebraic data types (Section 5), deconstructed with `match` (line 5), and (2) a reactive variable introduced by the arrow `↔` in line 4 (Section 6).

The semantics of an ARx program is given by a guarded command lan-
guage, which we call stream builders (Section 4.2), following the ideas from
Dokter and Arbab's stream constraints [10]. An instance of this intermediate
language is illustrated in ③, and includes not only stream variables from ARx,
but also memory variables (e.g., `m0`). Guarded commands include the guards (1)
`getmouse)` to denote a destructive read from the `mouse` stream, (2) `isFalse(m0)`
as a predicate introduced in our first extension, and `ask(m0)` is a non-destructive
read introduced in our second extension.

Stream builders have an operational semantics: they evolve by consuming
input streams and memory variables, and by writing to output streams. Fur-
thermore, the reactive extension in Section 6 adds an extra step to signal the
interest in writing-to or reading-from a stream. This reactive semantics is an-
imated in an automata view, depicted in ④. Note that this automata grows
quickly, but it is usually unnecessary, as the stream builders act as a compact
and symbolic representation of the automata.

# 4 Core ARx

## 4.1 ARx: Syntax

A program is a statement, according to the syntax in Figure 4. Expressions are either *terms t*, or names of so-called *stream builders bn* parameterised by a sequence of variables $\bar{x}$. In turn, terms can be *stream variables x*, *data values d*, or *function names* parameterised by variables $\bar{x}$.

So far we leave open the notions of *stream builders* and *functions*. Stream
builders will be introduced in Section 4.2, and will give semantics to ARx pro-
grams. Functions are assumed to be deterministic and total with an interpreta-
tion $\mathcal{I}$ that maps closed terms to values; in Section 5 we will restrict to construc-
tors of user-defined algebraic data types, as in our prototype implementation.

Regarding the remaining constructions, a *statement* is either an assignment *a*, a stream expression *e*, a builder definition *d*, or a parallel composition of statements *s s*. An *assignment* assigns a stream expression *e* to a non-empty sequence of stream variables $\bar{x}$. A builder definition **def** introduces a name *bn* associated to a new stream builder of a given block of statements *s*.
<table><caption>Figure 4: ARx' basic syntax, where *bn* ranges over names of stream builders, *fn* ranges over names of functions, and *x* over stream variables.</caption><tr><td>Statement</td><td>s ::= a | e | d | s s</td><td>Stream Expression</td><td>e ::= t | bn(x̄)</td></tr><tr><td>Assignment</td><td>a ::= x̄ ← e</td><td>Term</td><td>t ::= x | d | fn(x̄)</td></tr><tr><td></td><td></td><td>Builder Definition</td><td>d ::= def bn(x̄) = {s}</td></tr></table>

**Examples** The examples below assume the existence of stream builders `fifo` and `barrier`,<fnref n="7" /> and the function `ifThenElse` with some interpretation. Consider the `alternator` definition, capturing the program from the left of Figure 2. This has two input streams as parameters: `a` and `b`, which must fire together because of the `barrier`. Their values are redirected to `c`: the one from `a` flows atomically, and the one from `b` is buffered until a follow-up step. The stream `c` is the only output of the definition block.

```python
def alternator(a,b) = {
    barrier(a,b) c ← a
    c ← fifo(b) c
}
def gui sel mouse time = {
    display ←
    ifThenElse sel mouse time
}
```

Stream builders are typed, indicating the data types that populate the each input and output stream. Our implementation uses a type-inference engine that unifies matching streams and uses type variables. In our example from Figure 3, the inferred type of the `gui` builder is `Bool × p × p → p`, meaning that its first argument has type `Bool`, and all other ports must have the same type `p`. The type system also imposes all input stream variables inside `def` clauses to be parameters. We leave the type rules out of the scope of this paper, which focuses on the tools and on the semantics of ARx.

## 4.2 Stream builders: Syntax

Programs in ARx express functions from streams to streams, and describe the (non-strict) order between consuming and producing values. ARx's semantics is given by stream builders, defined below, which are closely inspired on Dokter and Arbab's stream constraints [10].

**Definition 1 (Stream builder).** A stream builder `sb` follows the grammar:

```
sb ::= \overline{upd} ∧ [\overline{gc}]              (stream builder)
gc ::= \overline{guard} → \overline{upd}            (guarded command)
guard ::= get(v) | und(v) | t                          (guard)
upd ::= v := t                                     (update)
```

where *v* is a variable name, *t* is a term, and *x̄* is a sequence of elements from *x*.

<footnote n="7">⁷ *barrier* is known as *drain* in our tools.</footnote>
Each variable $v$ can represent an *input stream* or an *output stream* (or both), as in ARx, or *internal memory*. Terms $t$ are the same as in ARx, but with variables also over the internal memory, and we write $fv(t)$ to denote the set variables in $t$. Let $s$ be a variable pointing to a stream and $m$ a memory variable. Intuitively, a guard $get(s)$ means that the head of $s$, denoted by $s(0)$, is ready to be read; a guard $get(m)$ means that the memory variable $m$ is defined; and a guard $und(x)$ means that $x$ has no value yet or is undefined.

A stream builder consists of an initial update that initialises memory variables and a set of guarded commands of the form $g \to u$ that specify a set of non-deterministic rules, such that the update $u$ can be executed whenever guard $g$ holds. When *executing* an update from a guarded command with a guard that succeeds, each $s := t$ sets $s(0)$ to the value obtained from $t$, each $m := t$ sets $m$ to be the value from $t$; every stream $s$ with $get(s)$ in the guard is updated to $s'$ (the head of $s$ is consumed), and every memory $m$ with $get(m)$ in the guard—and not set in the update—becomes undefined. As a side-remark, these constructions *get*, *und*, and $v := t$ are analogue to the operations *get*, *nask*, and *tell*, respectively, over shared tuple-spaces in Linda-like languages, well studied in the literature in that context [8].

We further restrict which streams can be used in updates and guards based on whether they are input streams $I$—that can be read—or output streams $O$—that can be built. This is formalised by the notion of well-definedness below. Intuitively, in addition to the previous restrictions, the initial updates can be only over memory variables and use terms with no variables, i.e., memory variables can only be initialized with data values rather than streams; and for every guarded command, undefined variables cannot be “gotten”, both guards and terms in updates can only use defined memory and input stream variables, and assignments in guarded commands cannot have cycles (which can occur since input and output stream variables may intersect). We use the following notation: given a stream builder $sb$, we write $sb.I$, $sb.O$, and $sb.M$ to denote its input streams, output streams, and memory variables; and we write $get(v̄)$ (and analogously for $und$) to denote a set of occurrences of $get(v)$, for every $v \in \bar{v}$.

**Definition 2 (Well-defined stream builder).** Let $sb$ be the stream builder:

$$ \overline{v_{init}} := t_{init} \land [get(\overline{v_{get}}), und(\overline{v_{und}}), t_{guard} \to \overline{v_{out}} := t_{out}, \dots]. $$

We say $sb$ is well-defined if $\overline{v_{init}} \subseteq sb.M$ and $fv(t_{init}) = \emptyset$, and if for every guarded command, the following conditions are met:

$$ \begin{array}{lclcl} \overline{v_{get}} \cap \overline{v_{und}} = \emptyset & \quad & \overline{v_{get}} \cup \overline{v_{und}} \subseteq sb.I \cup sb.M & \quad & \overline{v_{out}} \subseteq sb.O \cup sb.M \\ fv(t_{guard}) \subseteq \overline{v_{get}} & \quad & fv(t_{out}) \times \overline{v_{out}} \text{ is acyclic} & \quad & fv(t_{out}) \subseteq \overline{v_{get}} \end{array} $$

**Examples** We omit the initial updates of a stream builder when empty, and write `builder(v₁, v₂, ...)` = `upd \ gc` in the examples below to define a stream builder `builder` as `upd \ gc` over variables `{v₁, v₂, ...}`, using the convention that $i$
denotes an input stream, o denotes an output stream, and m denotes a memory.

$$
\begin{align*}
\mathit{sb}_{\mathit{add}} \langle i_1, i_2, o \rangle &= [\mathit{get}(i_1), \mathit{get}(i_2) \to o := i_1 + i_2] \\
\mathit{sb}_{\mathit{xor}} \langle i, o_1, o_2 \rangle &= [\mathit{get}(i) \to o_1 := \mathit{in} , \ \mathit{get}(i) \to o_2 := \mathit{in}] \\
\mathit{sb}_{\mathit{fifo}} \langle i, o, m \rangle &= [\mathit{get}(i), \mathit{und}(m) \to m := i , \ \mathit{get}(m) \to o := m] \\
\mathit{sb}_{\mathit{fifoFull42}} \langle i, o, m \rangle &= m := 42 \land \mathit{sb}_{\mathit{fifo}} \langle i, o, m \rangle \\
\mathit{sb}_{\mathit{barrier}} \langle i_1, i_2 \rangle &= [\mathit{get}(i_1), \mathit{get}(i_2) \to \emptyset] \\
\mathit{sb}_{\mathit{alternator}} \langle i_1, i_2, o, m \rangle &= \left[ \begin{array}{@{}l@{}}
    \mathit{get}(i_1), \mathit{get}(i_2), \mathit{und}(m) \to o := i_1, m := i_2 \\
    \mathit{get}(m) \to o := m
  \end{array} \right]
\end{align*}
$$

Informally, the `sb_add` stream builder receives values from two streams and outputs their sum. At each round, it atomically collects a value from each input stream and produces a new output value. In `sb_xor` there are two non-deterministic options at each round: to send data to one output stream or to a second output stream. In `sb_fifo` the two options are disjoint: if `m` is undefined only the left rule can be triggered, and if `m` is defined only the right rule can be triggered, effectively buffering a value when `m` is undefined, and sending `m` when `m` is defined (becoming undefined again). The formal behaviour is described below. Later in the paper, we will present a composition operator for stream builders, allowing `sb_alternator` to be built out of simpler builders.

4.3 Stream builders: operational semantics

Consider a stream builder `sb = init ∧ gc` with an interpretation $\mathcal{I}$ of closed terms as data values. The semantics of `sb` is given by a rewriting rule over the state of a stream builder. This state consists of a map $\sigma_m$ that assigns memory variables to their data values, and is initially set to $\langle init \rangle$. We use the following notation: $t[\sigma]$ captures the substitution on $t$ of $\sigma$, $\text{dom}(\sigma)$ is the domain of $\sigma$, $\sigma - X$ is the map $\sigma$ excluding the keys in $X$, $\sigma_1 \cup \sigma_2$ is the map $\sigma_1$ extended with $\sigma_2$, updating existing entries, and `gets(g)` returns the variables within `get` constructs in the guard `g`. We use $\sigma_i$ and $\sigma_o$ to represent the current mapping from (the first element of) input and output stream variables to data values, respectively.

**Definition 3 (Guard satisfaction).** Given a guard *g* and the current state of a system, given by $\sigma_m$ and $\sigma_i$, the satisfaction of *g*, denoted $\sigma_m, \sigma_i \models g$, is defined as follows.

$$
\begin{align*}
\sigma_m, \sigma_i \models \mathit{get}(\bar{v}) \quad &\text{if } \bar{v} \subseteq \mathit{dom}(\sigma_m) \cup \mathit{dom}(\sigma_i) & \quad \sigma_m, \sigma_i \models t \quad &\text{if } \mathcal{I}(t[\sigma_m][\sigma_i]) = \text{true} \\
\sigma_m, \sigma_i \models \mathit{und}(\bar{v}) \quad &\text{if } \bar{v} \cap \sigma_m = \emptyset & \quad \sigma_m, \sigma_i \models \bar{g} \quad &\text{if } \forall g_i \in \bar{g} \cdot \sigma_m, \sigma_i \models g_i
\end{align*}
$$

**Definition 4 (Operational semantics).** The semantics of a stream builder
`sb = init ∧ gc` is given by the rule below, with an initial configuration $\langle init \rangle$.

$$
\frac{
  \begin{array}{l}
    (g \to u) \in \bar{gc} \\
    \sigma_m, \sigma_i \models g
  \end{array}
}{
  \begin{array}{l}
    \sigma_o = \{ v \mapsto d \mid (v := t) \in u, v \in \mathit{sb.O}, d = \mathcal{I}(t[\sigma_m][\sigma_i]) \} \\
    \sigma'_m = \{ v \mapsto d \mid (v := t) \in u, v \in \mathit{sb.M}, d = \mathcal{I}(t[\sigma_m][\sigma_i]) \}
  \end{array}
}
\frac{
  \langle \sigma_m \rangle \xrightarrow{\sigma_i, \sigma_o} \langle (\sigma_m - \mathit{gets}(g)) \rangle \cup \sigma'_m
}{
  \langle \sigma_m \rangle
}
$$
Intuitively, $\langle\sigma\rangle \xrightarrow{\sigma_i, \sigma_o} \langle\sigma'\rangle$ means that, for every variable $i$ and data value $d$ such that $\sigma(i) = d$, the state evolves by reading the value $d$ from the head of the stream $i$, and by adding a value to each stream $o \in \text{dom}(\sigma_o)$, given by $\sigma_o(o)$. The internal state is captured by $\sigma_m$ that stores values of memory variables in $sb.M$, which is updated based on $\sigma_i$. Furthermore, the system can only evolve by executing an active guarded command. Intuitively, a guarded command is active if the current state of memory ($\sigma_m$) and input stream ($\sigma_i$) variables satisfy the guard $g$, such that: each term guard has an interpretation that evaluates to true; all required input stream variables coincide with the set of defined input stream variables; all required memory variables are contained in the defined memory variables; and all required undefined memory variables are indeed undefined. For example, the following are valid runs of the stream builders of Section 4.2.

$$sb_{\text{alternator}} : \langle\emptyset\rangle \xrightarrow{\{in_1\mapsto 5, in_2\mapsto 8\}, \{out_1\mapsto 5\}} \langle m \mapsto 8\rangle \xrightarrow{\emptyset, \{out\mapsto 8\}} \langle\emptyset\rangle$$

$$sb_{\text{add}} : \langle\emptyset\rangle \xrightarrow{\{in_1\mapsto 3, in_2\mapsto 2\}, \{out\mapsto 3+2\}} \langle\emptyset\rangle \xrightarrow{\{in_1\mapsto 2, in_2\mapsto 7\}, \{out\mapsto 2+7\}} \langle\emptyset\rangle$$

## 4.4 Composing Stream Builders

The composition of two stream builders yields a new stream builder that merges their initial update and their guarded commands, under some restrictions. I.e., the memory variables must be disjoint, some guarded commands can be included, and some pairs of guarded commands from each stream builder can be combined. This is formalised below in Definitions 5 and 6 after introducing some preliminary concepts. In the following we use the following auxiliary functions: $out(gc)$ returns the output streams assigned in the RHS of $gc$, $in(gc)$ returns the input streams inside get statements of $gc$, and vars($gc$) returns $out(gc) \cup in(gc)$.

The composition of stream builders follows the same principles as the composition of, e.g., constraint automata (CA) [4]. But unlike CA and most Reo semantics, it supports explicit many-to-many composition. I.e., a builder with an input stream $i$ can be composed with another builder with the same input stream $i$, preventing individual guarded commands from each builder to use $i$ without involving the other stream builder. Similarly, a builder with an output stream $o$ can be combined with another one with the same output stream $o$, although only one builder can write to $o$ at a time. A builder with an input stream $x$ can be composed with another with an output stream with the same name $x$, making $x$ both an input and an output in further compositions. The composition rules were carefully designed to keep the composition commutative and associative, which we do not prove in this paper.

We introducing the following auxiliary predicates used in the composition, using $gc_i$ to range over guarded commands and $I_1$ to range over stream variables
(meant to be from the same stream builder as $gc_1$).

$$ \mathit{matchedOuts}(I_1, gc_1, gc_2) \equiv I_1 \cap \mathit{out}(gc_2) \subseteq \mathit{in}(gc_1) $$

$$ \mathit{matchedIns}(I_1, gc_1, gc_2) \equiv I_1 \cap \mathit{in}(gc_2) \subseteq \mathit{vars}(gc_1) $$

$$ \mathit{exclusiveOut}(gc_1, gc_2) \equiv \mathit{out}(gc_1) \cap \mathit{out}(gc_2) = \emptyset $$

$$ \mathit{noSync}(I_1, gc_2) \equiv I_1 \cap \mathit{vars}(gc_2) = \emptyset $$

The predicate `matchedOuts(I₁, gc₁, gc₂)` means that any input stream in `I₁` that is an output of `gc₂` must be read by `gc₁`, i.e., must be an input stream used by `gc₁`. Its dual `matchedIns(I₁, gc₁, gc₂)` is not symmetric: it means that any input stream in `I₁` that is an input `gc₂` must either be written-to or read-by `gc₁`. This reflects the fact that input streams replicate data, and that input streams may also be output streams that could be used to synchronise. The predicate `exclusiveOut gc₁, gc₂`) states that `gc₁` and `gc₂` do not share output streams, reflecting the fact that only one rule can write to a stream at a time. The last predicate `noSync(I₁, gc₂)` states that `gc₂` will not affect any of the input streams in `I₁`. Intuitively this means that `gc₂` may read-from or write-to streams from another builder `sb₁` if they can also be written by `sb₁`, but not if they are read by `sb₁`.

The composition of guarded commands and of stream builders is defined below, based on these predicates.

**Definition 5 (Composition of guarded commands (gc₁ ⋉ gc₂)).** For $i \in \{1, 2\}$, let $gc_i = \mathit{get}(\overline{v_{gi}})$, $\mathit{und}(\overline{v_{ui}})$, $t_{gi} \to v_{oi} := t_{oi}$ be two guarded commands. Their composition yields $gc_1 ⋉ gc_2$ defined below.

$$ \mathit{get}((\overline{v_{g1}} \cup \overline{v_{g2}}) - (\overline{v_{o1}} \cup \overline{v_{o2}})), \mathit{und}(\overline{v_{u1}} \cup \overline{v_{u2}}), \overline{t_{g1}} \cup \overline{t_{g2}} \to \overline{v_{o1}} := \overline{t_{o1}} \cup \overline{v_{o2}} := \overline{t_{o2}} $$

**Definition 6 (Composition of stream builders (sb₁ ⋉ sb₂)).** For $i \in \{1, 2\}$, let $sb_i = \mathit{init}_i \wedge [\overline{gc}_i]$ be two stream builders. Their composition yields $sb = sb_1 \bowtie sb_2 = (\mathit{init}_1 \cup \mathit{init}_2) \wedge [gcs]$, where $sb.O = sb_1.O \cup sb_2.O$, $sb.I = sb_1.I \cup sb_2.I$, $sb.M = sb_1.M \cup sb_2.M$, and $gcs$ is given by the smallest set of guarded commands that obeys the rules below, which are not exclusive.

$$ \begin{array}{l@{\qquad}l} \text{(Com1)} & \begin{array}{@{}l@{}} gc \in \overline{gc_1} \\ \frac{\mathit{noSync}(sb_2.I, gc)}{gc} \end{array} \\ \text{(Com2)} & \begin{array}{@{}l@{}} gc \in \overline{gc_2} \\ \frac{\mathit{noSync}(sb_1.I, gc)}{gc} \end{array} \\ \text{(Com3)} & \begin{array}{@{}l@{}} \forall i, j \in \{1, 2\}, i \neq j: \quad gc_i \in \overline{gc_i} \\ \mathit{matchedOuts}(sb_i.I, gc_i, gc_j) \\ \mathit{matchedIns}(sb_i.I, gc_i, gc_j) \\ \mathit{exclusiveOut}(gc_i, gc_j) \end{array} \end{array} $$

Intuitively, any guarded command can go alone, unless it must synchronise on shared streams. Any two guarded commands can go together if their synchronization is well-defined and do not perform behaviour that must be an exclusive choice. Observe that the composition of two well-defined stream builders
$$
\begin{align*}
\llbracket bn(\bar{x}) \rrbracket_{\Gamma} &= (sb[\bar{x}/\bar{x}_I, \bar{y}/\bar{x}_O, \bar{z}/\text{rest}], \bar{y}) &
\left\{
\begin{array}{l}
\Gamma(bn) = (sb, \bar{x}_I, \bar{x}_O) \\
\text{rest} = \text{fv}(sb) - \bar{x}_I - \bar{x}_O \\
\text{for some fresh } \bar{y}, \bar{z}
\end{array}
\right. \\
\llbracket t \rrbracket_{\Gamma} &= (\overline{\text{get}(fv(t))} \to o := t], o) &
\left\{
\begin{array}{l}
\text{for some fresh } o \\
I = \text{fv}(t), O = \{o\}, M = \emptyset
\end{array}
\right. \\
\llbracket x \rrbracket_{\Gamma} &= ([\text{get}(x) \to o := x], o) &
\left\{
\begin{array}{l}
\text{for some fresh } o \\
I = \{x\}, O = \{o\}, M = \emptyset
\end{array}
\right. \\
\llbracket \bar{x} \leftarrow e \rrbracket_{\Gamma} &= (sb[\bar{x}/\bar{x}_O], \emptyset) &
\left\{
\begin{array}{l}
\llbracket e \rrbracket_{\Gamma} = (sb, \bar{x}_O)
\end{array}
\right. \\
\llbracket s_1, s_2 \rrbracket_{\Gamma} &= (sb_1 \bowtie sb_2, \bar{x}_O \cdot \bar{y}_O) &
\left\{
\begin{array}{l}
\llbracket s_1 \rrbracket_{\Gamma} = (sb_1, \bar{x}_O) \\
\llbracket s_2 \rrbracket_{\Gamma} = (sb_2, \bar{y}_O)
\end{array}
\right. \\
\llbracket \mathbf{def} \ bn(\bar{x}) = \{s_1\} \rrbracket_{\Gamma} &= \llbracket s_2 \rrbracket_{\Gamma[bn \to (sb, \bar{x}, \bar{x}_O)]} &
\left\{
\begin{array}{l}
\llbracket s_1 \rrbracket_{\Gamma} = (sb, \bar{x}_O)
\end{array}
\right.
\end{align*}
$$

<caption>Figure 5: Semantics: encoding of statements of ARx as a stream builder.</caption>

(c.f. Definition 2) may not produce a well-defined stream builder (e.g. cyclic assignments), in which case we say that the stream builders are incompatible and cannot be composed.

**Example** The sequential composition of two `fifo` builders is presented below, annotated with the rule name that produced it. The `get(b)` guard was dropped during composition (Definition 5), but included here to help understanding. The last two guarded commands, in `gray`, denote scenarios where the middle stream `b` remains open for synchronization. These are needed to make the composition operator associative, but can be discarded when hiding the internal streams like `b`. This is not explained here, but is implemented in our prototype tool. Following a similar reasoning, the stream builder `sb_alternator` can be produced by composing the stream builders `sbatuier` `a,b`, `sbfio` `b,c,m`, and `sbsync` `a,c`, which has no internal streams.

$$
\begin{align*}
& sb_{fifo}(a, b, m_1) \bowtie sb_{fifo}(b, c, m_2) = \\
& \quad \left[
  \begin{array}{@{}l@{\quad}l@{\quad}l@{}}
    \text{get}(a), \text{und}(m_1) & \rightarrow & m_1 := a & \text{(Com1)} \\
    \text{get}(b), \text{get}(m_1), \text{und}(m_2) & \rightarrow & b := m_1, m_2 := b & \text{(Com3)} \\
    \text{get}(a), \text{und}(m_1), \text{get}(m_2) & \rightarrow & m_1 := a, c := m_2 & \text{(Com3)} \\
    \text{get}(m_2) & \rightarrow & c := m_2 & \text{(Com2)} \\
    \text{get}(a), \text{und}(m_1), \text{get}(b), \text{und}(m_2) & \rightarrow & m_1 := a, m_2 := b & \text{(Com3)} \\
    \text{get}(b), \text{und}(m_2) & \rightarrow & m_2 := b & \text{(Com2)}
  \end{array}
\right]
\end{align*}
$$

## 4.5 ARx's Semantics: Encoding into Stream Builders

A statement in ARx can be encoded as a single stream builder under a context $\Gamma$ of existing stream builders. More precisely, $\Gamma$ maps names of stream builders `bn` to triples $(sb, \bar{x}_I, \bar{x}_O)$ of a stream builder `sb`, a sequence of variables for input
streams $\overline{x_I}$ of $sb$, and a sequence of variables for output streams $\overline{x_O}$. Given a statement $s$ and a context $\Gamma$, we define the encoding of $s$ as $\llbracket s \rrbracket_\Gamma$, defined in Figure 5. Evaluating $\llbracket s \rrbracket_\Gamma$ results in a pair $(sb, \overline{x_O})$ containing the encoded stream buffer and a sequence of variables. This sequence captures the output stream variables of $sb$. In the encoding definition we write $[x/y]$ to mean that $y$ substitutes $x$. Our implementation further applies a simplification of guarded commands in the **def** clause, by hiding output streams not in $\overline{x_O}$ and guarded commands that consume streams that are both input and output; but we do omit this process in this paper.

The composition exemplified in Section 4.4, regarding the alternator, is used when calculating the encoding of “**barrier(a,b)** c←**fifo(b)** c←**a**” below, where $\Gamma = \{ \mathbf{fifo} \mapsto (sb_{\mathbf{fifo}}\langle i, o \rangle, i, o), \mathbf{barrier} \mapsto (sb_{\mathbf{barrier}}\langle i_1, i_2 \rangle, i_1 \cdot i_2, \emptyset) \}$.

$$ \llbracket \mathbf{barrier}(a,b) \rrbracket_\Gamma = ([\mathbf{get}(a), \mathbf{get}(b) \to \emptyset], \emptyset) \quad (sb_1) $$

$$ \llbracket \mathbf{fifo}(b) \rrbracket_\Gamma = ([\mathbf{get}(b), \mathbf{und}(y_1) \to y_1 := b, \mathbf{get}(y_1) \to y_2 := y_1], y_2) $$

$$ \llbracket c \leftarrow \mathbf{fifo}(b) \rrbracket_\Gamma = ([\mathbf{get}(b), \mathbf{und}(y_1) \to y_1 := b, \mathbf{get}(y_1) \to c := y_1], \emptyset) \quad (sb_2) $$

$$ \llbracket c \leftarrow a \rrbracket_\Gamma = ([\mathbf{get}(a) \to c := a], c) \quad (sb_3) $$

$$ \left[ \begin{array}{c} \mathbf{barrier}(a,b) \\ c \leftarrow \mathbf{fifo}(b) \\ c \leftarrow a \end{array} \right]_\Gamma = (sb_1 \bowtie sb_2 \bowtie sb_3, \emptyset) = (sb_{\mathbf{alternator}}\langle a, b, c, y_1 \rangle, \emptyset) $$

# 5 Extension I: Algebraic Data Types

This section extends our language of stream builders with constructs for algebraic data types, allowing types to influence the semantics. The grammar, presented in Figure 6, extends the grammar from Figure 4 with declarations of Algebraic Data Types (ADTs), **build** and **match** primitive stream builders, and type annotations for builder definitions. For simplicity, we use the following notation: we omit $\overline{X}$, $\langle \overline{X} \rangle$, and $(\overline{X})$ when $\overline{X}$ is empty; we write **build**, **match**, and $bn(x)$ instead of **build**($\alpha$), **match**($\alpha$), and $bn(x : \alpha)$, respectively, when $\alpha$ is a type variable not used anywhere else; and we omit the output type $\overline{T}$ in builder definitions to denote a sequence of fresh type variables, whose dimension is determined during type-checking (when unifying types).

$$ \begin{array}{l@{\quad}l@{\quad}l} \text{Program} & P ::= \overline{D} s & \text{New Data Type} & D ::= \mathbf{data} \ D\langle \bar{\alpha} \rangle = Q(\overline{T}) \mid Q(\overline{T}) \\ \text{Data Type} & T ::= \alpha \mid D\langle \overline{T} \rangle & \text{Stream Expression} & e ::= \dots \mid \mathbf{build}\langle T \rangle(\bar{x}) \mid \mathbf{match}\langle T \rangle(\bar{x}) \\ \text{Data Term} & t ::= Q(\bar{x}) & \text{Builder Definition} & d ::= \mathbf{def} \ bn(\bar{x} : \overline{T}) : \overline{T} = \{s\} \end{array} $$

<caption>Figure 6: Syntax: extending the syntax from Figure 4 with ADTs, where $\alpha$ ranges over type variables, $D$ over type names, and $Q$ over data constructors.</caption>
A program starts by a list of definitions of algebraic data types, such as the ones below, which we will assume to be included in the header of all programs.

$$
\begin{align*}
\mathbf{data} \ Unit &= U & \mathbf{data} \ Nat &= \text{Zero} \mid \text{Succ}(\text{Nat}) \\
\mathbf{data} \ Bool &= \text{True} \mid \text{False} & \mathbf{data} \ List\langle\alpha\rangle &= \text{Nil} \mid \text{Cons}(\alpha, \text{List}\langle\alpha\rangle)
\end{align*}
$$

These ADTs are interpreted as the smallest fix-point of the underlying func-
tor, i.e., they describe finite terms using the constructors for data types. All
constructors *Q* must have at least one argument, but we write *Q* without argu-
ments to denote either *Q*(Unit) or *Q*(U). Each definition of an ADT **data** *D*⟨*T*⟩ =
*Q*₁(*g*) | ... | *Q*ₙ(*g*), e.g., **data** *List*⟨*α*⟩ = *Nil* | *Cons*(*α*, *List*⟨*α*⟩), introduces:

- Term constructors $Q_i$ to build new terms, e.g. `Nil` and `Cons(True, Nil)`;

- Term inspectors `isQ_i(x)` that check if `x` was built with `Q_i`, e.g. `isNil` and `isCons`
return `True` only if their argument has shape `Nil` or `Cons`, respectively;

- Term projections `getQ_i,j` that given a term built with `Q_i` return the `j`-th argument, e.g. `getCons₂(Cons(True, Cons(False, Nil))) = Cons(False, Nil)`;

Given these new constructs the new semantic encodings is presented in Figure 7.

$$
\llbracket \mathbf{match} \langle D \langle \bar{T} \rangle \rangle \rrbracket =
\left(
  \begin{array}{@{}l@{}}
    \left[
      \begin{array}{@{}l@{}}
        \mathbf{get}(in), isQ_1(in) \rightarrow out_{1,1} := getQ_{1,1}(in), \dots, out_{1,k_1} := getQ_{1,k_1}(in) \\
        \dots \\
        \mathbf{get}(in), isQ_n(in) \rightarrow out_{n,1} := getQ_{n,1}(in), \dots, out_{n,k_n} := getQ_{n,k_n}(in)
      \end{array}
    \right] \\
    out_{1,1} \cdots out_{1,k_1} \cdots out_{n,1} \cdots out_{n,k_n}
  \end{array}
\right)
$$

$$
\llbracket \mathbf{build} \langle D \langle \bar{T} \rangle \rangle \rrbracket = \left( \left[ \begin{array}{@{}l@{}} \mathbf{get}(in_{1,1}), \dots, \mathbf{get}(in_{1,k_1}) \rightarrow out := Q_1(in_{1,1}, \dots, in_{1,k_1}) \\ \dots \\ \mathbf{get}(in_{n,1}), \dots, \mathbf{get}(in_{n,k_n}) \rightarrow out := Q_n(in_{n,1}, \dots, in_{n,k_n}) \end{array} \right] , out \right)
$$

Figure 7: Semantics of match and build, considering that *D* is defined as
**data** *D*⟨*T*⟩ = *Q*₁(*g*₁, ..., *g*₁,*) | ... | *Q*ₙ(*g*ₙ, ..., *g*ₙ,*)

For example, [[**match**⟨**List**⟨**α**⟩⟩]] yields the builder below, and [[**match**⟨**α**⟩]] is un-defined unless the type-inference can instantiate **α** with a concrete ADT.

$$
\left[
  \begin{array}{l@{\quad}l}
    \mathit{get}(in), & \mathit{isNil}(in) \rightarrow \mathit{out}_{1,1} := \mathit{getNil}_1(in); \\
    \mathit{get}(in), & \mathit{isCons}(in) \rightarrow \mathit{out}_{2,1} := \mathit{getCons}_1(in), \mathit{out}_{2,2} := \mathit{getCons}_2(in)
  \end{array}
\right]
$$

6 Extension II: Reactive Semantics

In reactive languages, produced data is typically kept in memory, possibly trig-
gering consumers when it is initially produced. In this section we provide a finer
control about who can trigger the computation, and a notion of memory that is
read without being consumed. This will allow us to have memory variables that
trigger computations, and others that do not.
In the semantics of stream builders we add a notion of *active* variables, whereas a guarded command can only be selected if one of its variables is active, and adapt the operational semantics accordingly. We also introduce a new element to the guards: ask(v), that represents a non-destructive read.

**Syntax: asking for data** The extension for our language updates the grammar for assignments:

$$ \text{Assignment} \qquad a ::= \bar{x} \leftarrow e \mid \bar{x} \leftrightarrow e $$

whose squiggly arrow is interpreted as a creation of a reactive variable: the values from e are buffered before being used by $\bar{x}$, and this values can be read (non-destructively) when needed using the new guard ask. This is formalised below.

$$ [[\bar{x} \leftrightarrow e]]_\Gamma = [[(\bar{y} \leftarrow e) (\bar{x} \leftrightarrow \bar{y})]]_\Gamma \quad \text{for some fresh } \bar{y} $$

$$ [[x \leftrightarrow y]]_\Gamma = ([\text{ask}(m) \to x := m, \text{get}(y) \to m := y], \emptyset) $$

Observe that "$\text{get}(m) \to x := m, m := m$" is very similar to "$\text{ask}(m) \to x := m$". The former consumes the variable *m* and defines it with its old value, and the latter reads *m* without consuming it. This subtle difference has an impact in our updated semantics, defined below, by marking assigned variables as "active". In the first case *m* becomes active, allowing guarded commands that use *m* to be fired in a follow up step. In the second case *m* will become inactive, and guarded commands using *m* with no other active variables will not be allowed to fire.

**Semantics: active/passive variables** The reactive semantics for a stream builder $sb = \text{init} \wedge \bar{gc}$ is given by the rules below. The state is extended with two sets of so-called *active* input and output variables, with initial state $\langle \text{init}, \emptyset, \emptyset \rangle$. A system can evolve in two ways: (1) by evolving the program as before, consuming and producing data over variables, or (2) by an update to the context that becomes ready to write to (push) or read from (pull) a stream. Below we write "$\text{out}(u)$" to return the assigned variables in *u* (c.f. Section 4.4), "$\text{in}(g)$" to return the variables of *g* within get and ask constructs, and $\langle \sigma \rangle \xrightarrow{x} g, u \langle \sigma' \rangle$ to denote the step from state $\sigma$ to $\sigma'$ by *x* when selecting the guarded command $g \to u$.

$$ \begin{array}{l@{\qquad}l} (g \to u) \in \bar{gc} & \langle \sigma_m \rangle \underset{\sigma_i, \sigma_o}{\stackrel{\sigma_i, \sigma_o}{\rightleftharpoons}} g, u \quad \langle \sigma'_m \rangle \\ (\text{in}(g) \cap A_i \neq \emptyset) \lor (\text{out}(u) \cap A_o \neq \emptyset) & \langle \sigma_m \rangle \to \langle \sigma'_m \rangle \quad x \in sb.I \\ A'_i = (A_i - \text{in}(g)) \cup (\text{out}(u) \cap sb.M) & \langle \sigma_m, A_i, A_o \rangle \xrightarrow{\text{push}(x)} \langle \sigma'_m, A_i \cup \{x\}, A_o \rangle \\ A'_o = A_o - \text{out}(u) & \langle \sigma_m \rangle \to \langle \sigma'_m \rangle \quad x \in sb.O \\ \langle \sigma_m, A_i, A_o \rangle \underset{\sigma_i, \sigma_o}{\stackrel{\sigma_i, \sigma_o}{\rightleftharpoons}} \langle \sigma'_m, A'_i, A'_o \rangle & \langle \sigma_m, A_i, A_o \rangle \xrightarrow{\text{pull}(x)} \langle \sigma'_m, A_i, A_o \cup \{x\} \rangle \end{array} $$

The previous semantic rules must be accommodated to take the ask constructor into account. This is done by redefining the *guard satisfaction* definition in Section 4.3 to incorporate a new rule, presented below, and *vars* in Section 4.4 to include also the ask variables.

$$ \sigma_m, \sigma_i \models \text{ask}(\bar{v}) \qquad \bar{v} \subseteq \text{dom}(\sigma_m) $$
**Example: ADT and reactivity** We illustrate the encoding and semantics of reactive stream builders using the GUI manager example (Figure 1 and Figure 3). The equality below depicts the adapted system following the ARx syntax (left) and its semantics (right).

$$ \left[ \begin{array}{l} \text{last} \rightsquigarrow \text{sel} \\ t, f \leftarrow \text{match}(\text{last}) \\ \text{barrier}(t, \text{mouse}) \\ \text{barrier}(f, \text{time}) \\ \text{display} \leftarrow \text{mouse} \\ \text{display} \leftarrow \text{time} \\ \text{display} \end{array} \right] = \left[ \begin{array}{ll} \text{get}(\text{sel}) & \rightarrow m := \text{sel} \\ \text{get}(\text{mouse}), & \text{last} := m, \\ \text{get}(\text{last}), \text{get}(t), & \rightarrow t := \text{getTrue}_1(\text{last}), \\ \text{ask}(m), \text{isTrue}(m) & \text{display} := \text{mouse} \\ \text{get}(\text{time}), & \text{last} := m, \\ \text{get}(\text{last}), \text{get}(f), & \rightarrow f := \text{getFalse}_1(\text{last}), \\ \text{ask}(m), \text{isFalse}(m) & \text{display} := \text{time} \end{array} \right] $$

This encoding also returns the sequence of output streams, which in this case is `display`. The stream builder is further simplified by our toolset by removing intermediate stream variables `last`, `t`, and `f` from the updates, as depicted in the screenshot of Figure 3-③.

The following transitions are valid runs of this program.

$$ \begin{array}{lclcl} \langle \emptyset, \emptyset, \emptyset \rangle & \rightarrow & \text{pull}(\text{display}) & \rightarrow & \langle \emptyset, \emptyset, \{\text{display}\} \rangle \\ & \rightarrow & \text{push}(\text{sel}) & \rightarrow & \langle \emptyset, \{\text{sel}\}, \{\text{display}\} \rangle \\ & \rightarrow & \text{sel} \rightarrow \text{True} & \rightarrow & \langle \{m \mapsto \text{True}\}, \{m\}, \{\text{display}\} \rangle \\ & \rightarrow & \text{mouse} \rightarrow (2,3); \text{display} \rightarrow (2,3) & \rightarrow & \langle \{m \mapsto \text{True}\}, \emptyset, \emptyset \rangle \\ & \rightarrow & \text{pull}(\text{display}) & \rightarrow & \langle \{m \mapsto \text{True}\}, \emptyset, \{\text{display}\} \rangle \\ & \rightarrow & \text{mouse} \rightarrow (5,8); \text{display} \rightarrow (5,8) & \rightarrow & \langle \{m \mapsto \text{True}\}, \emptyset, \emptyset \rangle \end{array} $$

# 7 Conclusions

We proposed ARx, a lightweight programming language to specify component-based architecture for reactive systems, blending principles from reactive programming and synchronous coordination languages. ARx supports algebraic data types and is equipped with a type checking engine (not introduced here) to check if streams are well-composed based on the data being streamed.

Programs are encoded into stream builders, which provide a formal and compositional semantics to build programs out of simpler ones. A stream builder specifies the initial state of a program and a set of guarded commands which describe the steps (commands) that the program can perform provided some conditions (guards)—over the internal state and the inputs received from the environment—are satisfied.

We built an online tool to specify, type check, and analyse the semantics of ARx programs, and visualize both the architectural view of the program and its operational reactive semantics.
Future work plans include the *verification* of properties, the addition of new *semantic extensions*, and the development of *code generators*. These properties could be specified using hierarchical dynamic logic and verified with model checkers such as mCRL2, following [17], or could address the possibility of infinite loops caused by priorities of push and pulls from the environment. The semantic extensions could target, e.g., notions of variability, probability, time, and quality of service.

**Acknowledgments** This work was partially supported by National Funds through FCT/MCTES (Portuguese Foundation for Science and Technology), within the CIS-TER Research Unit (UIDB/04234/2020); by the Norte Portugal Regional Operational Programme (NORTE 2020) under the Portugal 2020 Partnership Agreement, through the European Regional Development Fund (ERDF) and also by national funds through the FCT, within project NORTE-01-0145-FEDER-028550 (REASSURE); and by the Operational Competitiveness Programme and Internationalization (COMPETE 2020) under the PT2020 Partnership Agreement, through the European Regional Development Fund (ERDF), and by national funds through the FCT, within projects POCI-01-0145-FEDER-029946 (DaVinci) and POCI-01-0145-FEDER-029119 (PReFECT).

## References

1. The reactive manifesto v2.0. https://www.reactivemanifesto.org, 2014.

2. Farhad Arbab. Reo: a channel-based coordination model for component composition. *Mathematical Structures in Computer Science*, 14(3):329–366, 2004.

3. Christel Baier. Probabilistic models for Reo connector circuits. *Journal of Universal Computer Science*, 11(10):1718–1748, 2005.

4. Christel Baier, Marjan Sirjani, Farhad Arbab, and Jan J. M. M. Rutten. Modeling component connectors in Reo by constraint automata. *Science of Computer Programming*, 61(2):75–113, 2006.

5. Engineer Bainomugisha, Andoni Lombide Carreton, Tom Van Cutsem, Stijn Mostinckx, and Wolfgang De Meuter. A survey on reactive programming. *ACM Comput. Surv.*, 45(4):52:1–52:34, 2013.

6. Gérard Berry. The foundations of Esterel. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, *Proof, Language, and Interaction*, pages 425–454. The MIT Press, 2000.

7. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In *Proceedings of the 42nd Annual Symposium on Principles of Programming Languages*, POPL ’15, pages 515–526, New York, NY, USA, 2015. ACM.

8. Antonio Brogi and Jean-Marie Jacquet. On the expressiveness of coordination via shared dataspaces. *Sci. Comput. Program.*, 46(1-2):71–98, 2003.

9. Régis Cridlig and Eric Goubault. Semantics and analysis of linda-based languages. In Patrick Cousot, Moreno Falaschi, Gilberto Filé, and Antoine Rauzy, editors, *WSA*, volume 724 of *Lecture Notes in Computer Science*, pages 72–86. Springer, 1993.

10. Kasper Dokter and Farhad Arbab. Rule-based form for stream constraints. In Giovanna Di Marzo Serugendo and Michele Loreti, editors, *Coordination Models and Languages*, pages 142–161, Cham, 2018. Springer International Publishing.
11. Joscha Drechsler, Guido Salvaneschi, Ragnar Mogk, and Mira Mezini. Distributed REScala: an update algorithm for distributed reactive programming. In *Andrew P. Black and Todd D. Millstein, editors, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014*, pages 361–376. ACM, 2014.

12. Conal Elliott and Paul Hudak. Functional reactive animation. In *International Conference on Functional Programming*, 1997.

13. David Harel. Statecharts: A visual formalism for complex systems. *Science of Computer Programming*, 8(3):231–274, June 1987.

14. Paul Hudak, Antony Courtney, Henrik Nilsson, and John Peterson. *Arrows, Robots, and Functional Reactive Programming*, pages 159–187. Springer Berlin Heidelberg, Berlin, Heidelberg, 2003.

15. Ingo Maier, Tiark Rompf, and Martin Odersky. Deprecating the observer pattern. page 18, 2010.

16. Sun Meng and Farhad Arbab. On resource-sensitive timed component connectors. In *FMOODS*, pages 301–316, 2007.

17. José Proença and Alexandre Madeira. Taming hierarchical connectors. In *Fundamentals of Software Engineering - 8th International Conference, FSEN 2019, Tehran, Iran, 2019*, Lecture Notes in Computer Science (to appear), 2019.

18. José Proença and Dave Clarke. Interactive interaction constraints. In Rocco De Nicola and Christine Julien, editors, *COORDINATION*, volume 7890 of *Lecture Notes in Computer Science*, pages 211–225. Springer, 2013.

19. Yoshitaka Sakurai and Takuo Watanabe. Towards a statically scheduled parallel execution of an FRP language for embedded systems. In *Proceedings of the 6th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems, REBLS 2019*, pages 11–20, New York, NY, USA, 2019. Association for Computing Machinery.