# Partial Connector Colouring

Dave Clarke, José Proença

► To cite this version:

Dave Clarke, José Proença. Partial Connector Colouring. 14th International Conference on Co-ordination Models and Languages (COORDINATION), Jun 2012, Stockholm, Sweden. pp.59-73, 10.1007/978-3-642-30829-1_5 . hal-01529589

HAL Id: hal-01529589

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

Submitted on 31 May 2017

**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
Partial Connector Colouring*

Dave Clarke and José Proença

IBBT-DistriNet, Department of Computer Science,
K.U.Leuven, Belgium

`{firstname.lastname}@cs.kuleuven.be`

**Abstract.** Connector colouring provided an intuitive semantics of Reo connectors which lead to effective implementation techniques, first based on computing colouring tables directly, and later on encodings of colouring into constraints. One weakness of the framework is that it operates globally, giving a colouring to all primitives of the connector in lock-step, including those not involved in the interaction. This global approach limits both scalability and the available concurrency. This paper addresses these problems by introducing partiality into the connector colouring model. Partial colourings allow parts of a connector to operate independently and in isolation, increasing scalability and concurrency.

# 1 Introduction

Reo [1] is a visual language for coordinating components and web services using
connectors composed from a small, but open, collection of primitives. A lot of
research has gone into semantic models for Reo, with the following (incomplete)
goals: to facilitate reasoning about Reo connectors; to provide context-dependent
behaviour; and to enable efficient implementations. Connector colouring [8] pro-
vided a great leap forward on these three fronts. Firstly, it is an intensional
semantic model that also gives a visual representation of what's going on in-
side a connector. Secondly, connector colouring offered the first context depen-
dent semantics for Reo. Thirdly, the semantics were simple enough to enable a
straightforward implementation of Reo [4]. Further improvements in implemen-
tation efficiency were obtained by encoding connector colouring as constraints
and using SAT and constraint satisfaction techniques [9].

The problem with the resulting implementation approach, and indeed with
connector colouring as a semantic model, is that it gives only a *global* descrip-
tion of the behaviour of a connector, with *all* primitives participating *lock-step*
to determine what to do next. In the constraints encoding, the constraints of
all primitives are conjoined together to compute the next step. This has three
negative consequences: the amount of available concurrency is reduced; imple-
mentations are inherently unscalable; and the behavioural possibilities offered by
connectors are actually reduced—some desirable behaviour becomes impossible.

* This research is partly funded by the EU project FP7-231620 HATS: Highly Adapt-
able and Trustworthy Software using Formal Models (http://www.hats-project.eu)
and KULeuven BOF Project STRT1/09/031: DesignerTypeLab.
This paper proposes a solution to this problem which overcomes these negative consequences, simply by considering certain partial connector colourings as valid. Rather than giving behaviour to the entire connector, a partial colouring can give behaviour to a part of a connector in a coherent fashion. This enables the local colouring of multiple parts of a connector concurrently and independently. The details of partial connector colouring are worked out for existing colouring schemes and new encodings as constraints are presented. We describe how existing constraint satisfaction engines can be used to implement partial colouring, and provide some benchmarks.

The paper is organised as follows. Section 2 gives a review of Reo and the connector colouring model. Section 3 details the problem being addressed. Section 4 describes one solution, namely, partial connector colouring. Section 5 reviews and adapts the constraint-based encoding of connector colouring. Section 6 discusses the implementation of our approach and gives some benchmarks. Section 7 discusses related work and Section 8 concludes.

# 2 Background: Reo and Connector Colouring

## 2.1 Reo Coordination Model

Reo [1] is a coordination model, wherein coordinating *connectors* are constructed by composing more primitive connectors. Reo's primitives, such as channels, offer a variety of behavioural policies regarding synchronisation, buffering, and lossiness. Being able to compose connectors out of smaller primitives is one of the strengths of Reo. It allows, for example, multi-party synchronisation to be expressed simply by plugging simple channels together. In addition, Reo's graphical notation helps bring intuition about the behaviour of a connector.

Communication with a primitive occurs through its ports, called *ends*: primitives consume data through their *source ends*, and produce data through their *sink ends*. (Source and sink ends correspond to the notions of source and sink in directed graphs.) Connectors are formed by plugging the ends of primitives together, without loss of generality, in a 1:1 fashion, connecting a sink end to a source end, to form *nodes*. Data flows through a connector from primitive to primitive through nodes, subject to the constraint that nodes cannot buffer data—the two ends in a node are synchronised. The behaviour of each primitive depends upon its current state and the semantics of a connector can be described *per-state* in a series of *rounds*. *Data flow* on a primitive's end occurs when a single datum is passed through that end. Within any round data flow may occur on some number of ends. This is equated with the notion of *synchrony*. Components attach to the boundary of a connector.

Some Reo primitives are:

**Replicator** ($\begin{array}{c} a \to b \\ c \end{array}$) replicates data synchronously from *a* to *b* and *c*.
**Merger** ( $\begin{array}{c} a \\ b \end{array} \mathbf{\rightarrow} c$ ) copies data synchronously either from *a* to *c* or *b* to *c*, but not from both.

**Priority merger** ( $\begin{array}{c} a \\ b \end{array} \mathbf{\rightarrow} c$ ) behaves like a merger, but prefers to select data from *a* over *b*, if both alternatives are possible. The ! marks the higher priority input.

**LossySync** ( $a \rightarrow b$ ) has two possible behaviours. Data can either flow synchronously from *a* to *b*, when possible, or can flow on *a* but not on *b*. The LossySync is context-dependent, in that it prefers to allow data to flow from *a* to *b* rather than lose it.

**Sync** ( $a \mathbf{\rightarrow} b$ ) passes data synchronously from *a* to *b*

**SyncDrain** ( $a \mathbf{\leftarrow} b$ ) synchronises ends *a* and *b*, consuming the data.

**AsyncDrain** ( $a \mathbf{\rightarrowleft} b$ ) consumes data either from *a* or from *b*, but not from both.

**FIFO<sub>1</sub>** ( $a \mathbf{\leftarrowbox{b}}$ ) is a stateful channel representing a buffer of size 1. When the buffer is empty it can receive data on *a*, but not output data on *b*. It then changes state and becomes full. A full FIFO<sub>1</sub> with data *d*, denoted $ (a \mathbf{\leftarrowleft d} \rightarrow b) $ , can output *d* through *b*, but cannot receive data on *a*. It then changes state and becomes empty again.

**Exclusive Router** ($\box{X}$) denotes an exclusive router, which has one input and multiple outputs. The input data is synchronously sent to exactly one output.

Doing nothing—no data flow—is always one of the behavioural possibilities.

In diagrams of connectors, nodes will be denoted ($\bullet$). In general, these can also have multiple source and sink ends, to denote generalised mergers and replicators, but these can be encoded in terms of binary mergers and replicators.

*Example 1.* The synchronous merge connector, presented in Fig. 1, is a common workflow pattern [18]. The connector controls the execution of two components A and B such that either A executes, or B executes, or both execute. The connector then synchronises on the completion of whichever of A and/or B ran.

## 2.2 Connector colouring: an overview

The connector colouring (CC) semantics for Reo [8] is based on colouring the ends of a connector using 2 colours to represent the presence or absence of data flow. A more refined version using 3 colours enabled context-dependent semantics. In each state, each primitive has a set of possible *colourings* that determine its synchronisation constraints. Each colouring is a mapping from the ends of a primitive to a colour, and the set of the colourings of a connector is called its *colouring table*. These tables are composed by considering each entry in one table with every entry in the other and joining compatible ones. Compatibility
<figure><img src="image_2.png" /><figcaption>Fig. 1. Synchronous merge connector.</figcaption></figure>

Primitives and their colouring tables

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

Connector and its colouring table

<figure><img src="image_4.png" /><figcaption>Fig. 2. Connector colouring. The dotted lines indicate compatible colourings.</figcaption></figure>

between colourings is determined by ensuring that they match where two ends
are joined to form a node. Fig. 2 illustrates the idea.

**2-Colouring** The 2-colouring scheme consists of colours `->`, which denotes the presence of data flow, and `---->`, which denotes its absence. For orientation, the `•` indicates the end. When plugging together colouring tables to compute the behaviour of connectors, both colours match only with themselves. That is, `--->` and `---.--` are the only valid combinations.

**3-Colouring** The 3-colouring scheme is used to express context-dependent behaviour. A primitive depends on its context if its behaviour changes non-monotonically with increases in possibilities of data flowing on its ends [8, 6]. That is, by adding more possibilities of data flow, the primitive actually rules out already valid behaviour possibilities. One colour (`->`) marks ends in the connector where data flows, and two colours mark the absence of data flow (`<->` and `->->`). The arrow indicates the *reason for no flow*, which can be either because no data is being written or because connector or component is not ready to receive the data. The arrow flows from the cause. `<->` denotes that the reason for no-flow originates from the context, and we say that the end *requires a reason* for no flow. Dually, `->>` indicates that the reason for no-flow originates from the primitive and we say that the end *gives a reason* for no-flow. Two 3-colours
<figure><img src="image_5.png" /><figcaption>Fig. 3. Evolution of example connector.</figcaption></figure>

following colouring table, whose domain is the union of the domains of $T_1$ and $T_2$, $T_1 \odot T_2 = \{c_1 \cup c_2 | c_1 \in T_1, c_2 \in T_2, c_1 \frown c_2\}$.

2-colouring is given by colouring scheme where Colour = {⊤, —, —•}, where binary relation ⌜ is '='. 3-colouring is given by Colour = {⊤, -▷•, -◁•} and ⌜ = {⟨⊤, —⟩, ⟨-▷•, -▷•⟩, ⟨-▷•, -◁•⟩, ⟨-▷•, -▷•⟩}.

The second colouring from Fig. 2, namely $a \dashv \Leftrightarrow b$, is formalised as colouring $\{a^\downarrow \mapsto \Leftrightarrow, b^\uparrow \mapsto -\Delta•\}$. It models the scenario where end $a$ has data flow and end $b$ has no data flow but requires a reason for its absence.

A stateful connector with ends $X$ and states $Q$ can be modelled using automata with transition structure $\Delta \subseteq Q \times (X \to Colour) \times Q$, such that state changes occur only when flow occurs at some end.

# 3 Problem Statement

The problem with connector colouring semantics (and their encoding into constraints) is that it takes a global view of the connector, that is, all primitives of the connector are considered at every round. This has two negative consequences.
Firstly, it eliminates the opportunity to exploit the concurrent, potentially asynchronous, evolution of distinct parts of a connector. Secondly, it means that implementations based on connector colouring will not be scalable.

Consider the connector in the top left-hand corner of Fig. 3. This consists of a $FIFO_1$ connected to priority merger. On the boundary are three components: Both $A$ and $B$ are attempting to write a single message, while $C$ is able to accept as many messages as possible. The different boxes in the figure correspond to different states of this connector. The transitions between these states are labelled with a 3-colouring if one exists, and a 2-colouring if not. (Valid 3-colourings can be converted to valid 2-colourings by forgetting the direction-of-reason arrows.)

Ideally, all transitions except the dotted one should be permitted—the dotted transition violates the preference of the priority merger. However, 2-colouring allows all transitions, which is too lax. On the other end of the spectrum, the only reachable transitions permitted by 3-colouring are those indicated with a thick line. 3-colouring rules out the dotted transition, but it also rules out other possibilities. Consider, for example, the transitions from the start state. These correspond to allowing writers $A$ and $B$ to succeed independently or together. But 3-colouring allows only both succeeding together. The other two behaviours are reasonable, as there is no channel synchronising actions $A$ and $B$.

# 4 Partial Connector Colouring

The problems described in the previous section are solved by partial connector colouring. The idea is simple: only part of the connector is coloured to determine the behaviour. The part that is not coloured plays no role in the computation. The challenge is determining which partial colourings are sensible; this comes down determining where the boundary of the coloured part can be drawn and what that boundary may look like.

Partial connector colouring is based on partial colouring schemes, which are triples $(Colour, \frown, valid)$, where $Colour$ is a set of colours, $\frown \subseteq (Colour + 1) \times (Colour + 1)$ is a symmetric matching relation such that $\perp \frown \perp$, and $valid: Colour \to 2$ is a predicate that states which colours can appear on the boundary of the coloured part, defined as $valid(x)$ if and only if $x \frown \perp$.

**Definition 2 (Partial Connector Colouring).** Given a partial colouring scheme $(Colour, \frown, valid)$, a partial colouring $c: X \to Colour$ for $X \subseteq \mathcal{X}^\perp$ is a partial function from ends to colours. The remainder of the definition (partial colouring tables and table composition) follows Definition 1, with partial colourings instead of total colourings.

A light gray colour will be used to denotes places where no colouring is computed—that is where the colouring table is undefined. Valid partial colourings satisfy two well-formedness conditions on the internal ends and boundary ends.

**Definition 3 (Valid Partial Colouring).** A partial colouring $c: X \to Colour$ for connector $P$, where $X = \text{ends}(P)$, is valid iff for all $x \in \text{internal}(P)$, $c(x^\uparrow) \frown c(x^\downarrow)$ and $valid(x^\circ)$ holds for all $x^\circ \in \text{boundary}(P)$.
Partial 2-colouring is defined as $Colour = \{ \text{---}, \text{---}\}$ and $\frown = \{ \langle \text{---}, \text{---} \rangle, \langle \text{---}, \text{---} \rangle, \langle \text{---}, \perp \rangle, \langle \perp, \text{---} \rangle, \langle \perp, \perp \rangle \}$. Only valid($\text{---}$) holds. A valid partial 2-colouring is one where no data flows at the boundaries. Partial 3-colouring is defined as $Colour = \{ \text{---}, \text{\textcolor{red}{-} \text{---}}, \text{---} \}$ and $\frown = \{ \langle \text{---}, \text{---} \rangle, \langle \text{---}, \text{\textcolor{red}{-} \text{---}}, \text{\textcolor{red}{-} \text{---}} \rangle, \langle \text{\textcolor{red}{-} \text{---}}, \text{---} \rangle, \langle \text{\textcolor{red}{-} \text{---}}, \text{\textcolor{red}{-} \text{---}} \rangle \langle \text{\textcolor{red}{-} \text{---}}, \perp \rangle, \langle \perp, \text{\textcolor{red}{-} \text{---}} \rangle, \langle \perp, \perp \rangle \}$. Only valid($\text{\textcolor{red}{-} \text{---}}$) holds. A valid partial 3-colouring is one where all boundary ends give a reason for no flow.

Partial 2- and 3-colouring schemes are well-behaved with respect to composition; the composition of two valid colourings produces a valid colouring. A partial *n*-colouring scheme can be seen as an (*n* + 1)-colouring scheme, but the way it is used is different, as the aim is to avoid computing the (*n* + 1)th colour.

The level of granularity expressed thus far is that of whole primitives, but we can go finer. For some primitives, the behaviour of some ends is independent of their other ends. This means that different parts of the primitive can be coloured (or not coloured) independently. This kind of behaviour is called *split colouring*.

We illustrate split colourings using the FIFO₁ buffer. Consider the partial colouring of the FIFO₁ buffer is its empty state in Fig. 4(a). It is the case that both ends of this primitive are independent (in the empty state), so the colour tables could be presented as in Fig. 4(b), where the FIFO₁ is actually treated as two separate primitives. Based on this, the effective colouring table for the FIFO₁ buffer is the one in Fig. 4(c).

The remainder of the figure revisits our example connector. Fig. 4(d) shows an attempt to find a colouring without split colourings for one of the transitions leaving the initial state, but this colouring is not valid due to the node marked x. This corresponds to a writer blocking for no reason. With split colourings, the colouring in Fig. 4(e) can instead be used. This colouring does not even look at the writer; it is not blocked, just not involved in the computation.

Two conditions govern the validity of a split colouring. The first is that when we split the colouring table for the connector and then rejoin it, as in Fig. 4(a-c), no additional data flow behaviour is introduced. The second condition deals with stateful primitives. As each split colouring is derived from some partial colouring, which itself may cause a change in the state, consistency demands that no no-flow colouring can result in a state change and that any combination of split

<figure><img src="image_6.png" /><figcaption>**Fig. 4.** Splitting the colouring table of an empty FIFO₁ buffer (a-c). Candidate connector without split colourings (d) and with them (e)</figcaption></figure>
<figure><img src="image_7.png" /><figcaption>**Fig. 5.** Splitting the automaton of a FIFO₁. The automata for the parts of the split FIFO₁ have an *out-of-phase* synchronisation step to keep the same view on the state.</figcaption></figure>

colourings do not result in different state changes—there is at most one state change among the split colourings. Formal conditions capturing the correctness criteria have been explored in Proença's thesis [16].

When only one part causes a change of state, the two parts need to synchronise to ensure that both have the same view on the state. We illustrate with an example. Fig. 5(a) gives an automaton for a FIFO₁, where transitions are labelled with the split colourings that cause the respective transitions—each transition has multiple colourings. When the primitive is split it results in the two automata shown in Fig. 5(b-c), one for each end of the FIFO₁. Now, if a data flow transition is taken in the first automaton in state *e*, the second automaton is not aware of the state change, as it has no behaviour to change the state. In order for them to get into the same state, an *out-of-phase* synchronisation step is made between the two ends of the split primitive.

Fig. 6 presents what partial 3-colouring will allow. Split colouring of the FIFO₁ primitive is required for the transitions marked **1** and **2**. Not only does partial 3-colouring with split colouring allows all desirable behaviours, but it also reduces the computation required to achieve these, thereby increasing scalability. It allows *mosaic evolution*, whereby different parts of the connector can evolve at different rates, increasing concurrency. Partial and split colourings thus offer more potential concurrency, as the ends can be computed independently, better scalability, as the size of the connector being considered can be smaller, and more behavioural possibilities.

# 5 Constraint-based Encoding

In previous work we showed how to encode connector colouring as constraints [9]. The constraints encode three aspects of behaviour: *synchronisation constraints* (SC) describe the presence or absence of data flow at each end—that is, whether or not those ends synchronise; *data flow constraints* (DFC) describe the data
<figure><img src="image_8.png" /><figcaption>Fig. 6. Evolution of example connector with partial colouring.</figcaption></figure>

flow at the ends that synchronise (which connector colouring does not capture); and *context constraints* (CC) describe the direction of the reasons for no-flow. For encoding 2-colouring, context constraints can be dropped. State and state transitions can also be encoded, but we omit them here for brevity.

Constraints are defined over (1) propositional synchronisation variables $\mathcal{X}$, (2) data flow variables $\hat{\mathcal{X}} = \{\hat{x} | x \in \mathcal{X}\}$ ranging over $\mathcal{Data}_{\perp} \cong \mathcal{Data} \cup \{\text{NO-FLOW}\}$, where $\mathcal{Data}$ be the domain of data and where $\text{NO-FLOW} \notin \mathcal{Data}$ represents ‘no data flow’, and (3) propositional context variables $\mathcal{X}^{\perp}$. The encoding of colourings into constraints is given in the following table:

<table><thead><tr><th>Colouring</th><th>Constraint</th><th>Colouring</th><th>Constraint</th></tr></thead><tbody><tr><td>$x^{\perp} \mapsto \text{---}$</td><td>$x$</td><td>$x^{\perp} \mapsto \text{---}$</td><td>$x$</td></tr><tr><td>$x^{\perp} \mapsto \text{-\Delta-\bullet}$</td><td>$\neg x \wedge x^{\perp}$</td><td>$x^{\perp} \mapsto \text{-\Delta-\bullet}$</td><td>$\neg x \wedge x^{\perp}$</td></tr><tr><td>$x^{\perp} \mapsto \text{-\Delta-\bullet}$</td><td>$\neg x \wedge \neg x^{\perp}$</td><td>$x^{\perp} \mapsto \text{-\Delta-\bullet}$</td><td>$\neg x \wedge \neg x^{\perp}$</td></tr></tbody></table>

Constraints are expressed as quantifier-free, first-order logical formulas. Table 2 presents the semantics of some commonly used primitives. A *solution* to a formula $\psi$ is an assignment of variables, defined in the usual manner [9].
<table><caption>**Table 2.** Channel Encodings. SC=synchronisation constraints. DC=data flow constraints. CC=context constraints.</caption><thead><tr><th>Channel</th><th>Representation</th><th>SC</th><th>DFC</th><th>CC</th></tr></thead><tbody><tr><td>Sync</td><td>a &rarr; b</td><td>a &harr; b</td><td>hat = b&#770;</td><td>a &or; not a &darr; &or; not b &uarr;</td></tr><tr><td>LossySync</td><td>a &harr; b</td><td>b &harr; a</td><td>b &rarr; (hat = b&#770;)</td><td>not a &rarr; (not b &and; not a &darr; &and; b &uarr;) &and; not b &rarr; ((a &and; not b &uarr;) &or; not a)</td></tr><tr><td>Priority Merger</td><td>a &rarr; b &harr; c</td><td>(c &harr; (a &or; b)) &and; not (a &and; b)</td><td>a &rarr; (c&#770; = hat) &and; b &rarr; (c&#770; = b&#770;)</td><td>(c &and; not a) &rarr; not a &darr; &and; (c &and; not b) &rarr; b &darr; &and; not c &rarr; ((not a &darr; &and; not b &darr;) &or; not c &uarr;)</td></tr><tr><td>Replicator</td><td>a &harr; b &harr; c</td><td>(a &harr; b) &and; (a &harr; c)</td><td>hat = hat &and; c&#770; = hat</td><td>a &or; not a &darr; &or; not b &uarr; &or; not c &uarr;</td></tr><tr><td>FIFO1 (empty)</td><td>a &harr; b</td><td>not b</td><td>&top;</td><td>(not a &rarr; not a &darr;) &and; b &uarr;</td></tr><tr><td>FIFO1 (full)</td><td>a &harr; d &harr; b</td><td>not a</td><td>b &rarr; (hat = d)</td><td>a &darr; (not b &rarr; not b &uarr;)</td></tr></tbody></table>

The following axiom captures the relationship between the different kinds of variables, and it is applicable to all ends in a connector:

$$ (\neg x \leftrightarrow \hat{x} = \text{NO-FLOW}) \wedge (\neg x \to x^{\uparrow} \lor x^{\downarrow}) \qquad \text{(flow axiom)} $$

The first clause captures that **NO-FLOW** is used as the value of a data flow variable when no flow occurs, which is the same as when the corresponding synchronisation variable is $\perp$. The constraint $x^{\uparrow} \lor x^{\downarrow}$ is interpreted as saying that the reason for no data flow either comes from the sink end, from the source end, or from both ends. The second clause is dropped when using 2-colouring. Let $\text{Flow}(X)$ denote the conjunction $\bigwedge_{x \in X} (\neg x \leftrightarrow \hat{x} = \text{NO-FLOW}) \wedge (\neg x \to x^{\uparrow} \lor x^{\downarrow})$.

The constraints for an entire connector are obtained by taking the conjunction of the constraints of the primitives making up the connector and adding in the flow axiom for the ends present. For example, the connector in Fig. 2 is encoded in constraints as follows:

$$ \begin{align*} \Psi_{SC} &= b \to a \wedge \neg c & \Psi_{DFC} &= b \to (\hat{a} = \hat{b}) \wedge \top \\ \Psi_{CC} &= \neg a \to (\neg b \wedge \neg a^{\downarrow} \wedge b^{\uparrow}) \wedge \neg b \to ((a \wedge \neg b^{\uparrow}) \vee \neg a) \wedge (\neg b \to \neg b^{\downarrow}) \wedge c^{\uparrow} \\ \Psi &= \Psi_{SC} \wedge \Psi_{DFC} \wedge \Psi_{CC} \wedge \text{Flow}(\{a, b, c\}). \end{align*} $$

## 5.1 Partial 2- and 3-Constraints

Now we can modify the constraints generated to handle partial colouring. The first difference is that the constraints will be applied not to all primitives, but to a subset of the primitives—split primitives treated as separate primitives. First, let $\text{constraints}_p$ denote the constraints for connector $p$, and define $\text{constraints}_P = \bigwedge_{p \in P} \text{constraints}_p$. Two kinds of additional are constraints generated. The first ensures that the solution to the constraints corresponds to a
valid partial colouring by constraining the boundary:

$$ \bigwedge_{x^\circ \in \text{boundary}(P)} \neg x \wedge x^\circ \qquad (\text{boundary}) $$

The 2-colouring variant is obtained by dropping the ‘$\wedge x^\circ$’ part. It is straightforward to show that the collection of constraints faithfully encodes partial 2/3-colouring. An additional kind of constraint is added to check whether there is any flow within a connector, as ultimately we are only interested in partial colourings where something happens:

$$ \bigvee_{x \in \text{internal}(P)} x \qquad (\text{internal-flow}) $$

# 6 Implementation and Benchmarks

Partial connector colouring is implemented using constraint satisfaction in a fashion similar to our constraint-based implementation of Reo [9]. The previous implementation collected all the constraints for a connector and solved them. The resulting solution described the behaviour in the connector.

To exploit partiality, a different approach is required. This involves trying to solve the constraints for a part of the total connector; if no solution is found, a larger part is tried. More specifically, each thread operating on a connector performs the following steps. The thread is initially given a number of primitives, which it is said to own. It collects the constraints for those primitives, including the boundary and internal flow constraints, and solves the resulting constraint satisfaction problem. A solution corresponds to flow within that part of the connector, so the thread ensures that the corresponding data is moved to where it belongs and the states of stateful primitives change. If, however, there is no solution, then the part of the connector the thread is operating on is expanded and the algorithm repeats. When two threads attempt to own the same part of the connector, one claims both parts of the connector and the other thread is returned to the thread pool to be reassigned work.

Due to the nature of this approach, we cannot expect that it will always be better—implementations will need to be tuned to specific connectors. Nevertheless, a number of preliminary benchmarks do show that partial connector colouring can produce a faster implementation. The benchmarks consist of two parametric connectors, depicted in Fig. 7. These connector each have a part that can be repeated a given number of times. We ran four versions of our implementation on these connectors on a 8-core 2.4 GHz Intel Xeon desktop with 16 GB RAM running Ubuntu Linux. As a baseline, the first version implemented the original connector colouring model. The other versions implement partial connector colouring, using one, two and four threads. These results show that partial colouring can lead to a faster, more concurrent, and scalable implementation.

There are however a number of dimensions where heuristics can be applied to improve the performance of the implementation, such as choosing the number of threads, choosing where they start computing, and choosing how the set of primitives considered grows. These will be investigated in future work.
<figure><img src="image_9.png" /><figcaption>**Fig. 7.** Benchmarks: Multiple Merger (a) demonstrates that partial connector colouring offers an order of magnitude improvement for one thread, though multiple threads create too much contention. Pairwise Asynchronous (b) demonstrates significant advantages of partial colouring, which scales well as more threads (cores) are added.</figcaption></figure>

# 7 Related work

Many semantic models exist for Reo. Clarke et al. [6] outline the difference between various models. Only connector colouring [8], Reo automata [6], intentional automata [10], and the tile model [3] capture context dependent behaviour. Connector colouring was the first to do so, and the others refine it in one way or another. The models are all distinct—and the relationship between them has not been investigated—but for our purposes, we do not consider automata-based models as these do not lead to scalable implementations. The constraint-based encoding of Reo [9] offers orders of magnitude improvement in performance and scalability of Reo implementations.

Wegner describes coordination as constrained interaction [19] and Montanari and Rossi express coordination as a constraint satisfaction problem [15]. They describe how to solve synchronisation problems using constraint solving techniques, but they do not encode context dependency or identify the benefits of partiality. Lazovik et al. [13] utilise constraints to provide a choreography framework for web services. The choreography, the business processes, and the requests are modelled as a set of constraints. Their setting, however, cannot express the same kinds of coordination patterns as Reo. The analogy between Reo
and constraint satisfaction has already been made [2], and indeed Klüppelholz and Baier encode the constraint automata model for Reo in terms of binary decision diagrams in order to model check Reo connectors [12]. Constraint automata are represented by binary decision diagrams, encoded as propositional formulæ. Their encoding is similar to ours, though they use exclusively boolean variables, whilst our constraint encoding is phrased in terms of a richer data domain.

Minsky and Ungureanu introduce the Law-Governed Interaction (LGI) mechanism [14], implemented by the Moses toolkit, where in laws are constraints specified in a Prolog-like language, enforced on regulated events of the agents, such as sending or receiving messages. This mechanism targets distributed coordination of heterogenous agents using a policy that enforces extensible laws. However, laws are local, in the sense that can only refer to the agent being regulated. While this allows LGI to achieve good performance, it limits expressiveness.

Bruni et al.'s stateless algebra of connectors [7] and Sobociński's [17] stateful extension resemble the core of Reo, though they lack context dependency and data. The semantics is similar to 2-colouring in this limited setting. Bliduze and Sifakis [5] present a semantics for their BIP coordination model in terms of boolean propositions. Although similar, BIP is not as expressive as Reo as it lacks the ability to filter data passing through connectors. Jongmans et al. [11] present an encoding of 3-colouring in terms of 2-colouring that resembles our encoding into propositional constraints. Their approach adds fictitious nodes into the Reo level, whereas ours is completely under the surface.

## 8 Conclusion

This paper presented partial connector colouring which improves on the existing connector colouring semantics for Reo and their subsequent encoding as constraints in three respects. Firstly, the semantics enable a more scalable implementation by avoiding the lock-step evaluation of an entire connector. Secondly, the amount of concurrency is increased by enabling different parts of a connector to evolve independently at different rates. Finally, partial 3-colouring retains the context dependent behaviour of 3-colouring but regains some of the behavioural possibilities lost due to the lock-step computation. Benchmarks have also been presented to confirm the possible performance improvements.

An interesting direction for future work is a more in depth empirical exploration of the heuristics alluded to in Section 6.

## References

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

2. F. Arbab. Composition of interacting computations. In D. Goldin, S. Smolka, and P. Wegner, editors, *Interactive Computation: The New Paradigm*, pages 277–321, Secaucus, NJ, USA, 2006. Springer-Verlag New York, Inc.
3. F. Arbab, R. Bruni, D. Clarke, I. Lanese, and U. Montanari. Tiles for Reo. In *Proceedings of Recent Trends in Algebraic Development Techniques (WADT)*, volume 5486 of LNCS, pages 37–55, Berlin, Heidelberg, 2008. Springer.

4. F. Arbab, C. Koehler, Z. Maraikar, Y. Moon, and J. Proença. Modeling, testing and executing Reo connectors with the Eclipse Coordination Tools. In *International Workshop on Formal Aspects of Component Software (FACS)*, Malaga, 2008. Electronic Notes in Theoretical Computer Science (ENTCS).

5. S. Bliudze and J. Sifakis. Synthesizing glue operators from glue constraints for the construction of component-based systems. In *Software Composition*, volume 6708 of Lecture Notes in Computer Science, pages 51–67, 2011.

6. M. M. Bonsangue, D. Clarke, and A. Silva. Automata for context-dependent connectors. volume 5521 of LNCS, pages 184–203, 2009.

7. R. Bruni, I. Lanese, and U. Montanari. A basic algebra of stateless connectors. *Theor. Comput. Sci.*, 366(1-2):98–120, 2006.

8. D. Clarke, D. Costa, and F. Arbab. Connector colouring I: Synchronisation and context dependency. *Science of Computer Programming*, 66(3):205–225, May 2007.

9. D. Clarke, J. Proença, A. Lazovik, and F. Arbab. Channel-based coordination via constraint satisfaction. *Sci. Comput. Program.*, 76(8):681–710, 2011.

10. D. Costa. *Formal Models for Component Connectors*. PhD thesis, Vrij Universiteit Amsterdam, 2010.

11. S-S. T. Q. Jongmans, C. Krause, and F. Arbab. Encoding context-sensitivity in reo into non-context-sensitive semantic models. In *Coordination Models and Languages*, volume 6721 of LNCS, pages 31–48, 2011.

12. S. Klüppelholz and C. Baier. Symbolic model checking for channel-based component connectors. *ENTCS*, 175(2):19–37, 2007.

13. A. Lazovik, M. Aiello, and R. Gennari. Choreographies: Using constraints to satisfy service requests. In *Proc. of the Advanced International Conference on Telecommunications and International Conference on Internet and Web Applications and Services*, page 150, Washington, DC, USA, 2006. IEEE Computer Society.

14. N. H. Minsky and V. Ungureanu. Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems. *ACM Transactions on Software Engineering and Methodology*, 9(3):273–305, 2000.

15. U. Montanari and F. Rossi. Modeling process coordination via tiles, graphs, and constraints. In *3rd Biennial World Conference on Integrated Design and Process Technology*, volume 4, pages 1–8, 1998.

16. J. Proença. *Synchronous coordination of distributed components*. PhD thesis, LIACS, Leiden University, May 2011.

17. P. Sobociński. Representations of Petri net interactions. In *Concurrency Theory (CONCUR '10)*, number 6269 in LNCS, pages 554–568. Springer, 2010.

18. W. M. P. van der Aalst, A. H. M. ter Hofstede, B. Kiepuszewski, and A. P. Barros. Workflow patterns. *Distributed and Parallel Databases*, 14(1):5–51, 2003.

19. P. Wegner. Coordination as constrained interaction (extended abstract). In *Coordination Languages and Models*, volume 1061 of LNCS, pages 28–33, 1996.