Kasper Dokter

Farhad Arbab

Rule-Based Form for Stream Constraints

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Over a decade ago, Baier et al. introduced constraint automata for the specification of interaction protocols [START_REF] Baier | Modeling component connectors in reo by constraint automata[END_REF]. Constraint automata feature a powerful composition operator that preserves synchrony: composite constructions not only yield intuitively meaningful asynchronous protocols but also synchronous protocols. Constraint automata have been used as basis for tools, like compilers and model checkers. Jongmans developed Lykos: a compiler that translates constraint automata into reasonably efficient executable Java code [START_REF] Jongmans | Automata-theoretic protocol programming[END_REF]. Baier, Blechmann, Klein, and Klüppelholz developed Vereofy, a model checker for constraint automata [START_REF] Baier | A uniform framework for modeling and verifying components and connectors[END_REF][START_REF] Klüppelholz | Verification of Branching-Time and Alternating-Time Properties for Exogenous Coordination Models[END_REF]. Unfortunately, like every automaton model, composition of constraint automata suffers from state space and transition space explosions. These explosions limit the scalability of the tools based on constraint automata.

To improve scalability, Clarke et al. developed a compiler that translates a constraint automaton to a first-order formula [START_REF] Clarke | Channel-based coordination via constraint satisfaction[END_REF]. The transitions of the constraint automaton correspond to the solutions of this formula. At run time, a generic constraint solver finds these solutions and simulates the automaton. Since composition and abstraction for constraint automata respectively correspond to conjunction and existential quantification, the first-order specification does not suffer from state space or transition space explosion. However, the approach proposed by Clarke et al. only delays the complexity until run time: calling a generic constraint solver at run time imposes a significant overhead.

Jongmans realized that the overhead of this constraint solver is not always necessary. He developed a commandification algorithm that accepts constraints without disjunctions (i.e., conjunctions of literals) and translates them into a small imperative program [START_REF] Jongmans | Prdk: Protocol programming with automata[END_REF]. The resulting program is a light-weight, tailormade constraint solver with minimal run time overhead. Since commandification accepts only constraints without disjunction, Jongmans applied this technique to data constraints on individual transitions in a constraint automaton. Relying on constraint automata, his approach still suffers from scalability issues [START_REF] Jongmans | Constraint automata with memory cells and their composition[END_REF].

We aim to prevent state space and transition space explosions by combining the ideas of Clarke et al. and Jongmans. To this end, we present the language of stream constraints: a generalization of constraint automata based on temporal logic. A stream constraint is an expression that relates streams of observed data at different locations (Section 2). We identify a subclass of stream constraints, called regular (stream) constraints, which is closed under composition and abstraction (Section 3). Regular constraints can be viewed as a constraint automata, and conjunction of reflexive regular constraints is similar to composition of constraint automata (Section 4).

A straightforward application of the commandification algorithm of Jongmans to regular stream constraints entails transforming a stream constraint into disjunctive normal form and applying the algorithm to each clause separately. However, the number of clauses in the disjunctive normal form may grow exponentially in the size of the composition. To prevent such exponential blowups of the size of the formula, we recognize and exploit symmetries in the disjunctive normal form. Each clause in the disjunctive normal form can be constructed from a set of basic stream constraints, which we call rules. This idea allows us to represent a single large constraint as certain combination of a set of smaller constraints, called the rule-based form (Section 5). We express the composition of stream constraints in terms of the rule-based normal form (Section 6), and show that, for simple sets of rules, the number of rules to describe the composition is only linear in the size of the composition (Section 7). The class of stream constraints defined by a simple set of rules contains constraints for which the size of the disjunctive normal form explodes, which shows that our approach improves upon existing approaches by Clarke et al. and Jongmans. We express abstraction on stream constraints in terms of the rule-based normal form and provide a sufficient condition under which the number of rules remains constant (Section 8). Finally, we conclude and point out future work (Section 10).

Related work

Representation of stream constraints in rule-based form is part of a larger line of research on symbolic approaches, such a symbolic model checking [START_REF] Burch | Symbolic model checking: 10ˆ20 states and beyond[END_REF][START_REF] Baier | Symbolic model checking for probabilistic processes[END_REF][START_REF] Kwiatkowska | Symbolic model checking for probabilistic timed automata[END_REF] and symbolic execution [START_REF] Clavel | All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic[END_REF]. These approaches not only use logic (cf., SAT solving techniques [START_REF] Kemper | Sat-based verification for timed component connectors[END_REF][START_REF] Ehlers | Minimising deterministic büchi automata precisely using SAT solving[END_REF] for verification), but also other implicit representations, like binary decision diagrams [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF] and Petri nets [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF]. Petri nets offer a small representation of protocols with an exponentially large state space. While our focus is more on compilation, Petri nets have been studied in the context of verification. As inspiration for future work, it is interesting to study the similarities between Petri nets and stream constraints.

Since regular stream constraints correspond to constraint automata, we can view regular stream constrains as a restricted temporal logic for which distributed synthesis is easy. In general, distributed (finite state) synthesis of protocols is undecidable [START_REF] Pnueli | On the synthesis of a reactive module[END_REF][START_REF] Pnueli | Distributed reactive systems are hard to synthesize[END_REF]. Pushing the boundary from regular to a larger class of stream constraints can be useful for more effective synthesis methods.

Syntax and semantics

The semantics of constraint automata is defined as a relation over timed data streams [START_REF] Arbab | A coinductive calculus of component connectors[END_REF], which are pairs, each consisting of a non-decreasing stream of time stamps and a stream of observed (exchanged) data items. The primary significance of time streams is the proper alignment of their respective data streams, by allowing "temporal gaps" during which no data is observed. For convenience, we drop the time stream and model protocols as relations over streams of data, augmented by a special symbol that designates "no-data" item.

We first define the abstract behavior of a protocol C. Fix an infinite set X of variables, and fix a non-empty set of user-data Data ⊇ {0} that contains a datum 0. Consider the data domain D = Data ∪ { * } of data stream items, where we use the "no-data" symbol * ∈ D \ Data to denote the absence of data. We model the a single execution of protocol C as a function

θ : X -→ D N (1)
that maps every variable x ∈ X to a function θ(x) : N -→ D that represents a stream of data at location x. We call θ a data stream tuple (over X and D). For all n ∈ N and all x ∈ X, the value θ(x)(n) ∈ D is the data that we observe at location x and time step n. If θ(x)(n) = * , we say that no data is observed at x in step n (i.e., we may view θ as a partial map N × X Data). The behavior of protocol C consists of the set

L(C) ⊆ (D N ) X (2)
of all possible executions of C, called the accepted language of C. We can think of accepted language L(C) as a relation over data streams. In this paper, we study protocols that are defined as a stream constraint:

Definition 1 (Stream constraints). A stream constraint φ is an expression generated by the following grammar

φ ::= ⊥ | t 0 . = t 1 | φ 0 ∧ φ 1 | ¬φ | ∃xφ | φ t ::= x | d | t
where x ∈ X is a variable, d ∈ D is a datum, and t is a stream term.

We use the following standard syntactic sugar: = ¬⊥,

φ 0 ∨ φ 1 = ¬(¬φ 0 ∧ ¬φ 1 ), ♦φ = ¬ ¬φ, ¬(t 1 . = t 2 ) = (t 1 . = t 2 ), (t 1 . = t 2 ∧ • • • ∧ t n-1 . = t n ) = (t 1 . = • • • . = t n ), t (0) = t, and t (k+1) = (t (k)
) , for all k ≥ 0. Following Rutten [START_REF] Rutten | Elements of stream calculus (an extensive exercise in coinduction)[END_REF], we call t (k) , k ≥ 0, the k-th derivative of term t.

We interpret a stream constraint as a constraint over streams of data in D N . For a datum d ∈ D, d is the constant stream defined as d(n) = d, for all n ∈ N. The operator (-) , called stream derivative, drops the head of the stream and is defined as σ (n) = σ(n + 1), for all n ∈ N and σ ∈ D N . Streams can be related by . = that expresses equality of their heads: x . = y iff x(0) = y(0), for all

x, y ∈ D N . The modal operator allows us to express that a stream constraint holds after applying any number of derivatives to all variables. For example, (x . = y) iff x (k) (0) = y (k) (0), for all k ∈ N and x, y ∈ D N . Stream constraints can be composed via conjunction ∧, or negated via negation ¬. Streams can be hidden via existential quantification ∃.

Each stream term t evaluates to a data stream in D N . Let θ : X -→ D N be a data stream tuple. We extend the domain of θ from the set of variables X to the set of terms T ⊇ X as follows: we define θ : T -→ D N via θ(d) = d and θ(t ) = θ(t) , for all d ∈ D and terms t ∈ T .

Next, we interpret a stream constraint φ as a relation over streams.

Definition 2 (Semantics). The language L(φ) ⊆ (D N ) X of a stream constraint φ over variables X and data domain D is defined as

1. L(⊥) = ∅; 2. L(t 0 . = t 1 ) = {θ : X -→ D N | θ(t 0 )(0) = θ(t 1 )(0)}; 3. L(φ 0 ∧ φ 1 ) = L(φ 0 ) ∩ L(φ 1 ); 4. L(¬φ) = (D N ) X \ L(φ); 5. L(∃xφ) = {θ : X -→ D N | θ[x → σ] ∈ L(φ), for some σ ∈ D N }; 6. L( φ) = {θ : X -→ D N | θ (k) ∈ L(φ), for all k ≥ 0}, where θ[x → σ] : X -→ D N is defined as θ[x → σ](x) = σ and θ[x → σ](y) = θ(y), for all y ∈ X \ {x}; and θ (k) : X -→ D N is defined as θ (k) (x) = θ(x (k) ), for all x ∈ X.
Let φ and ψ be two stream constraints and θ : X -→ D N a data stream tuple. We say that θ satisfies φ (and write θ |= φ), whenever θ ∈ L(φ). We say that φ implies ψ (and write φ |= ψ), whenever L(φ) ⊆ L(ψ). We call φ and ψ equivalent (and write φ ≡ ψ), whenever L(φ) = L(ψ). Conjunction ∧ and existential quantification ∃ provide natural operators for composition and abstraction for stream constraints. For example, the composition sync(a, b) ∧ sync(b, c) synchronizes ports a, b, and c. Hiding port b yields ∃b(sync(a, b) ∧ sync(b, c)), which is equivalent to sync(a, c).

Example 2. Recall that x (k) , for k ≥ 0, is the k-th derivative of x. We can express that a stream x is periodic via the stream constraint (x (k) .

= x), for some k ≥ 1. For k = 1, stream x is constant, like 0 and * .

Example 3. The stream constraint fifo(a, b, m) defined as m . = * ∧ ((a . = m . = 0 ∧ b . = m . = * ) ∨ (a . = m . = * ∧ b . = m . = 0) ∨ (a . = b . = * ∧ m . = m
)) models a 1-place buffer with input location a, output location b, and memory location m that can be full (m . = 0) or empty (m . = * ).

Example 4. Recall that * models absence of data. Stream constraint ♦(a . = * ) expresses that always eventually we observe some datum at a. A constraint of such form can be used to define fairness.

Regular constraints

We identify a subclass of stream constraints that naturally correspond to constraint automata. We first introduce some notation.

To denote that a string s occurs as a substring in a stream constraint φ or a stream term t, we write s ∈ φ or s ∈ t, respectively.

Every stream constraint φ admits a set free(φ) ⊆ X of free variables, defined inductively via free(⊥) = ∅, free(t 0 . = t 1 ) = {x ∈ X | x ∈ t 0 or x ∈ t 1 }, free(φ 0 ∧ φ 1 ) = free(φ 0 ) ∪ free(φ 1 ), free(¬φ) = free( φ) = free(φ), and free(∃xφ) = free(φ) \ {x}.

For every variable x ∈ X, we define the degree of x in φ as

deg x (φ) = max({-1} ∪ {k ≥ 0 | x (k) ∈ φ}),
and the degree of φ as deg(φ) = max x∈X deg x (φ). Note that for x / ∈ φ we have deg x (φ) = -1. For k ≥ 0, we write free k (φ) = {x ∈ free(φ) | deg x (φ) = k} for the set of all free variables of φ of degree k.

We call a variable x of degree zero in φ a port variable and write P (φ) = free 0 (φ) for the set of port variables of φ. We call a variable x of degree one or higher in φ a memory variable and write M (φ) = k≥1 free k (φ) for the set of memory variables of φ.

Definition 3 (Regular). A stream constraint φ is regular if and only if

φ = ψ 0 ∧ ψ, such that / ∈ ψ 0 ∧ ψ and deg x (ψ 0 ) < deg x (ψ) ≤ 1, for all x ∈ X.
For a regular stream constraint φ = ψ 0 ∧ ψ, we refer to ψ 0 as the initial condition of φ and we refer to ψ as the invariant of φ. Stream constraints sync(a, b) and fifo(a, b, m) in Examples 1 and 3 are regular stream constraints.

A regular stream constraint φ has an operational interpretation in terms of a labeled transition system φ . States of the transition system consist of maps q : M (φ) -→ D that assign data to memory locations, and its labels consist of maps α : P (φ) -→ D that assign data to ports. We write Q(φ) for the set of states of φ and A(φ) for the set of labels of φ. Definition 4 (Operational semantics). The operational semantics φ of a regular stream constraint φ = ψ 0 ∧ ψ consists of a labeled transition system

(Q(φ), A(φ), →, Q 0 ), with set of states Q(φ), set of labels A(φ), set of transitions → = {(q φ (θ), q φ (θ ), α φ (θ)) | θ ∈ L(ψ)}, and set of initial states Q 0 = {q φ (θ) | θ ∈ L(ψ 0 ∧ ψ)}, where 1. q φ (θ) : M (φ) -→ D is defined as q φ (θ)(x) = θ(x)(0), for x ∈ M (φ); and 2. α φ (θ) : P (φ) -→ D is defined as α φ (θ)(x) = θ(x)(0), for x ∈ P (φ).
and θ is defined as θ (x)(n) = θ(x)(n + 1), for all x ∈ X and n ∈ N.

Example 5. Consider the regular stream constraint fifo(a, b, m) from Example 3. Note that in this example, the set of ports equals free 0 (fifo) = {a, b} and the set of memory locations equals free 1 (fifo) = {m}. The semantics of fifo(a, b, m) over the trivial data domain D = {0, * } consists of 4 transitions:

[a → 0, b → * ] [a → * , b → 0] [a → * , b → * ] [a → * , b → * ]

([m

→ * ], [m → 0], [a → 0, b → * ]); 2. ([m → 0], [m → * ], [a → * , b → 0]); and 3. ([m → d], [m → d], [a → * , b → * ]), for every d ∈ { * , 0}.
Figure 1 shows the semantics of fifo over the trivial data domain.

Equivalent stream constraints do not necessarily have the same operational semantics. We are, therefore, interested in operational equivalence of constraints: Definition 5 (Operational equivalence). Stream constraints φ and ψ are operationally equivalent (φ ψ) iff φ ≡ ψ and free k (φ) = free k (ψ), for k ≥ 0. Example 6. Let φ be a stream constraint, let t be a term and let x / ∈ t be a variable that does not occur in t. Then, we have ∃x(x

. = t ∧ φ) ≡ φ[t/x],
where φ[t/x] is obtained from φ by substituting t for every free occurrence of x. Observe that ∃x(x . = t ∧ φ) and φ[t/x] may admit different sets of free variables: if φ is just and t is a variable y, the equivalence amounts to ∃x(x . = y) ≡ . To ensure that the free variables coincide, we can add the equality t . = t and obtain the operational equivalence ∃x(x

. = t ∧ φ) φ[t/x] ∧ t . = t.
Operational equivalence of stream constraints φ and ψ implies that their operational semantics are identical, i.e., φ = ψ . It is possible to introduce weaker equivalences by, for example, demanding that φ and ψ are only weakly bisimilar. Such weaker equivalence offer more room for simplification of stream constraints than operational equivalence does. As our work does not need this generality, we leave the study of such weaker equivalences as future work.

The most important operations on stream constraints are composition (∧) and hiding (∃). The following result shows that regular stream constraints are closed under conjunction and existential quantification of degree zero variables.

Theorem 1. For all stream constraints φ and ψ and variables x, we have

1. φ ∧ ψ ≡ (φ ∧ ψ); and 2. ∃x φ ≡ ∃xφ, whenever deg x (φ) ≤ 0 and / ∈ φ. Proof. For assertion 1, L( φ ∧ ψ) = {θ ∈ (D N ) X | ∀k ≥ 0 : θ (k) |= φ ∧ ψ} = L( (φ ∧ ψ)) shows that φ ∧ ψ ≡ (φ ∧ ψ).
For assertion 2, suppose that deg x (φ) ≤ 0 and / ∈ φ. We show that θ ∈ L( ∃xφ) if and only if θ ∈ L(∃x φ), for all θ ∈ (D N ) X . By Definition 2, this equivalence can be written as

θ (k) [x → µ k ] |= φ ⇔ (θ[x → σ]) (k) |= φ, (3)
for all k ≥ 0, σ ∈ D N , and

µ k ∈ D N such that µ k (0) = σ (k) (0).
To prove Equation (3), we proceed by induction on the length of φ: Case 1 (φ := ⊥): Since L(⊥) = ∅, Equation (3) holds trivially.

Case 2 (φ := t 0 . = t 1 ): Observe that, since deg x (φ) ≤ 0, for all terms t, we have x ∈ t iff t = x. We conclude Equation (3) from µ k (0) = σ (k) (0) and

θ (k) [x → µ k ](t)(0) = µ k (0) if t = x θ (k) (t)(0) if t = x = (θ[x → σ]) (k) (t)(0).
= x. Then, θ (k) [x → µ k ] |= φ is equivalent to (θ[y → τ ]) (k) [x → µ k ] |= ψ, for some τ ∈ D N . Applying the induction hypothesis for θ equal to θ[y → τ ], we conclude that θ (k) [x → µ k ] |= φ is equivalent to (θ[y → τ ][x → σ]) (k) |= ψ, for some τ ∈ D N . Since y = x, we conclude that Equation (3) holds.
We conclude that the claim holds for all φ with deg x (φ) ≤ 0 and / ∈ φ.

Reflexive constraints

Conjunction of stream constraints is a simple syntactic composition operator with clear semantics: a data stream tuple θ satisfies a conjunction φ 0 ∧ φ 1 if and only if θ satisfies both φ 0 and φ 1 . In view of the semantics of regular stream constraints in Definition 2, it is less obvious how φ 0 ∧ φ 1 relates to φ 0 and φ 1 . The following result characterizes their relation when no memory is shared.

Theorem 2. Let φ 0 and φ 1 be regular stream constraints such that free(φ 0 ) ∩ free(φ 1 ) ⊆ P (φ 0 ∧ φ 1 ), and let

(q i , q i , α i ) ∈ Q(φ i ) 2 × A(φ i ), for i ∈ {0, 1}.
The following are equivalent:

1. q 0 α0 -→ q 0 in φ 0 , q 1 α1 -→ q 1 in φ 1 , and α 0 | P (φ1) = α 1 | P (φ0) ; 2. q 0 ∪ q 1 α0∪α1 ----→ q 0 ∪ q 1 in φ 0 ∧ φ 1 ,
where | is restriction of maps, and ∪ is union of maps.

Proof.

Write φ i = ψ i0 ∧ ψ i , with / ∈ ψ i0 ∧ ψ i and deg x (ψ i0 ) < deg x (ψ i ) ≤ 1, for all x ∈ X. Then, free k (φ i ) = free k (ψ i ), for all i, k ∈ {0, 1}.
Suppose that assertion 1 holds. By Definition 2, we find, for all i ∈ {0, 1}, some θ i ∈ L(ψ i ) such that q i = q φi (θ i ), q i = q φi (θ i ), and α i = α φi (θ i ). Define θ : X -→ D N by θ(x) = θ i (x), if x ∈ free(φ i ), and θ(x) = * , otherwise. Since free(φ 0 ) ∩ free(φ 1 ) ⊆ P (φ 0 ∧ φ 1 ) and α 0 | P (φ1) = α 1 | P (φ0) , we have that θ 0 (x) = θ 1 (x), for all x ∈ free(φ 0 ) ∩ free(φ 1 ). Hence, θ is well-defined. By construction, θ |= ψ 0 and θ |= ψ 1 . By Definition 2, we have θ |= ψ 0 ∧ψ 1 . By Theorem 1, we have φ 0 ∧ φ 1 = ψ 00 ∧ ψ 10 ∧ (ψ 0 ∧ ψ 1 ). Since q 0 ∪ q 1 = q φ0∧φ1 (θ), q 0 ∪ q 1 = q φ0∧φ1 (θ ), and α 0 ∪ α 1 = α φ0∧φ1 (θ), we conclude assertion 2.

Suppose that assertion 2 holds. We find some θ ∈ L(ψ 0 ∧ ψ 1 ), such that q 0 ∪ q 1 = q θ , q 0 ∪ q 1 = q θ , and α 0 ∪ α 1 = α θ . Then, we conclude assertion 1, for q i = q φi (θ), q i = q φi (θ ), and α i = α φi (θ).

Stream constraints φ 0 and φ 1 without shared variables (free(φ 0 ) ∩ free(φ 1 ) = ∅) seem completely independent. However, Theorem 2 shows that their composition φ 0 ∧ φ 1 admits a transition only if φ 0 and φ 1 admit respective local transitions (q 0 , q 0 , α 0 ) and (q 1 , q 1 , α 1 ), such that α 0 | P (φ1) = α 1 | P (φ0) . Since φ 0 and φ 1 do not share variables, the latter condition on α 0 and α 1 is trivially satisfied. Still, for one protocol φ i , with i ∈ {0, 1}, to make progress in the composition φ 0 ∧ φ 1 , constraint φ 1-i must admit an idling transition.

To allow such independent progress, we assume that φ 1-i admits an idling transition (q, q, τ ), where τ is the silent label over P (φ 1-i ). The silent label over a set of ports P ⊆ X is the map τ : P -→ D that maps x ∈ P to * ∈ D. If such idling transitions are available in every state of φ 1 , we say that φ 1 is reflexive:

Definition 6 (Reflexive). A stream constraint φ is reflexive if and only if q τ -→ q in φ , for all q ∈ Q(φ).
For regular constraints, we can define reflexiveness also syntactically, for which we need some notation. For a variable x ∈ X and an integer k ∈ N ∪ {-1}, we define the predicate x † k (pronounced: "x is blocked at step k") as follows:

x † k := (x (k) .

= x (k-1) ), with x (k) . = * , for all k < 0.

Predicate x † -1 ≡ is trivially true. Predicate x † 0 ≡ (x . = * ) means that we observe no data flow at port x. Predicate x † 1 ≡ (x . = x) means that the data in memory variable x remains the same.

We now provide a syntactic equivalent of Definition 6 for regular constraints.

Lemma 1. A regular stream constraint φ = ψ 0 ∧ ψ is reflexive if and only if

x∈X x † d(x) |= ψ, where d(x) = deg x (φ)
, for all x ∈ X. Proof. Since d(x) = -1, for all but finitely many x ∈ X, the stream constraint x∈X x † d(x) is well-defined. By definition, x∈X x † d(x) |= ψ if and only if, for all q ∈ Q(φ), there exists some θ ∈ L(ψ), such that q θ = q θ = q and α θ = τ .

Example 7. The stream constraint sync(a, b) := (a . = b) from Example 1 is reflexive, because x∈X x † d(x) = a . = * ∧ b . = * implies a . = b. The stream constraint fifo from Example 3 is reflexive, because x∈X x † d(x) = a . = * ∧ b . = * ∧ m . = m is one of the clauses of fifo.
Theorem 2 suggests a composition operator × on labeled transition systems, satisfying φ 0 × φ 1 = φ 0 ∧φ 1 . For reflexive constraints φ 0 and φ 1 , composition × simulates composition of constraint automata [START_REF] Baier | Modeling component connectors in reo by constraint automata[END_REF]. Constraint automata also feature a hiding operator that naturally corresponds to existential quantification ∃ for stream constraints. We leave a full formal comparison between stream constraints and constraint automata as future work.

Rule-based form

The commandification algorithm developed by Jongmans accepts only conjunctions of literals [START_REF] Jongmans | Prdk: Protocol programming with automata[END_REF]. To apply commandification to the invariant ψ of an arbitrary regular stream constraint ψ 0 ∧ ψ, we can first transform ψ into disjunctive normal form (DNF). However, the number of clauses in the disjunctive normal form may be exponential in the length of the constraint. In this section, we introduce an alternative to the disjunctive normal form that prevents such exponential blow up, for a strictly larger class of stream constraints. Our main observation is that the clauses of the disjunctive normal form may contain many symmetries, in the sense that we may generate all clauses from a set of stream constraints R, called a set of rules. A rule is a stream constraint ρ, such that deg(ρ) ≤ 1 and / ∈ ρ.

Definition 7 (Rule-based form). A reflexive stream constraint φ is in rulebased form iff φ equals

rbf(R) = x∈free(R) x † d(x) ∨ ρ∈R:x∈free(ρ) ρ (4)
with R a finite set of rules, free(R) = ρ∈R free(ρ), and

d(x) = max ρ∈R deg x (ρ). A stream constraint φ is defined by R iff φ rbf(R).
We apply the rule-based form to the invariant of regular constraints, via ψ 0 ∧ rbf(R), for some degree zero stream constraint ψ 0 and set of rules R. Intuitively, R remains smaller than the DNF of rbf(R) under composition. = x, we assume without loss of generality that free(ρ i ) = free(φ), for all 2

≤ i ≤ n. For R = {ρ i | 2 ≤ i ≤ n}, it follows from rbf(R) ≡ x∈free(R)   x † d(x) ∨ ρ∈R ρ   ≡   x∈free(φ) x † d(x)   ∨ ρ∈R ρ ≡ φ (5)
that φ is defined by the set R.

Definition 7 presents the rule-based form as a conjunctive normal form. The following result computes the disjunctive normal form of rbf(R).

Lemma 2. For every set of rules R, we have

rbf(R) dnf(R) := T ⊆R ρ∈T ρ ∧ x∈free(R)\free(T )
x † d(x) .

Proof. Let x ∈ X be arbitrary. By construction, we have deg

x (dnf(R)) ≤ max ρ∈R deg x (ρ). Since d(x) = max ρ∈R deg x (ρ), the clause for T = ∅ shows that deg x (dnf(R)) ≥ d(x). By Lemma 4, deg x (rbf(R)) = deg x (dnf(R)), for all x ∈ X. Hence, free k (rbf(R)) = free k (dnf(R)), for all k ≥ 0.
Next, we show that rbf(R) |= dnf(R). Let θ ∈ L(rbf(R)). We find, for every x ∈ free(R), some rule ρ x ∈ R, such that θ |= ρ and x ∈ free(ρ). Now, define T θ := {ρ x | x ∈ free(R) and θ / ∈ L(x † d(x) )}. By construction, θ |= ρ x , for every ρ x ∈ T θ . If x ∈ free(R) and θ / ∈ L(x † d(x) ), then ρ x ∈ T θ and x ∈ free(ρ x ) ⊆ free(T θ ). By contraposition, we conclude that θ |= x † d(x) , for all x ∈ free(R) \ free(T θ ). Hence, θ |= dnf(R), and L(rbf(R)) ⊆ L(dnf(R)).

Finally, we show that dnf(R) |= rbf(R). Let θ ∈ L(dnf(R)). By definition of dnf(R), we find some T ⊆ R with θ |= ρ, for all ρ ∈ T , and θ |= x † d(x) , for all x ∈ free(R) \ free(T ). Suppose that x ∈ free(R) and θ |= x † d(x) . Since θ |= x † d(x) , for all x ∈ free(R) \ free(T ), we find by contraposition that x ∈ free(T ). Hence, we find some ψ ∈ T with x ∈ free(ψ). Since θ |= ρ, for all ρ ∈ T , we find that θ |= ψ. Hence, θ |= rbf(R) and we conclude that rbf(R) dnf(R).

Composition

We express conjunction of stream constraints in terms of their defining sets of rules. That is, for two sets of rules R 0 and R 1 , we define the composition R 0 ∧R 1 of R 0 and R 1 , such that rbf(R 0 ∧ R 1 ) rbf(R 0 ) ∧ rbf(R 1 ). If R 0 and R 1 do not share any variable (i.e., free(R 0 ) ∩ free(R 1 ) = ∅), composition R 0 ∧ R 1 is given by the union R 0 ∪ R 1 . In this section, we define the composition R 0 ∧ R 1 of R 0 and R 1 for free(R 0 ) ∩ free(R 1 ) = ∅.

In view of Example 11, consider the normal form dnf(R 0 ∧R 1 ). Since dnf(R 0 ∧ R 1 ) equals dnf(R 0 ) ∧ dnf(R 1 ), it suffices to characterize the set of clauses of dnf(R 0 ) ∧ dnf(R 1 ). Every such clause is a conjunction of a clause in dnf(R 0 ) and a clause in dnf(R 1 ). Lemma 2 shows that the clauses of dnf(R i ) correspond to subsets T i of R i , for all i ∈ {0, 1}. Not every pair of subsets T 0 ⊆ R 0 and T 1 ⊆ R 1 yields a clause of dnf(R 0 ) ∧ dnf(R 1 ), but only if S = T 0 ∪ T 1 is synchronous: Definition 8 (Synchronous). A synchronous set over sets of rules R 0 and R 1 is a subset S ⊆ R 0 ∪ R 1 , with free(S) ∩ free(R i ) ⊆ free(S ∩ R i ), for all i ∈ {0, 1}.

Example 12. For any integer

i ≥ 1, let ϕ i := a i . = m i . = 0 ∧ m i . = * and ψ i := m i . = * ∧a i+1 . = m i .
= 0 be the two rules that define fifo(a i , a i+1 , m i ), from Example 10. The synchronous sets consist of exactly those sets S ⊆ {ϕ 1 , ψ 1 } ∪ {ϕ 2 , ψ 2 } that satisfy ψ 1 ∈ S iff ϕ 2 ∈ S. That is, the synchronous sets are given by ∅, {ϕ

1 }, {ψ 2 }, {ψ 1 , ϕ 2 }, {ϕ 1 , ψ 1 , ϕ 2 }, {ψ 1 , ϕ 2 , ψ 2 }, {ϕ 1 , ψ 1 , ϕ 2 , ψ 2 }.
Next, we recognize symmetries in the collection of synchronous sets. We can construct every synchronous set as a union of irreducible synchronous subsets:

Definition 9 (Irreducibility). A non-empty synchronous set ∅ = S ⊆ R 0 ∪R 1 is irreducible if and only if S = S 0 ∪ S 1 implies S = S 0 or S = S 1 , for all synchronous subsets S 0 , S 1 ⊆ R 0 ∪ R 1 .
Example 13. Let R 0 and R 1 be sets of rules, and let ρ ∈ R 0 be a rule, such that free(ρ) ∩ free(R 1 ) = ∅. We show that {ρ} is irreducible synchronous. Since free({ρ}) ∩ free(R 0 ) = free(ρ) = free({ρ} ∩ R 0 ) and free({ρ}) ∩ free(R 1 ) = ∅ ⊆ free({ρ} ∩ R 1 ), we conclude that {ρ} is synchronous. Suppose {ρ} = S 0 ∪ S 1 . Then, ρ ∈ S i , for some i ∈ {0, 1}. Hence, {ρ} ⊆ S i ⊆ {ρ}, which shows that S i = {ρ}. We conclude that {ρ} is irreducible synchronous in R 0 ∪ R 1 .

Example 14. Consider ϕ i and ψ i , for i ∈ {1, 2}, from Example 12. The irreducible synchronous sets of {ϕ 1 , ψ 1 }∪{ϕ 2 , ψ 2 } are {ϕ 1 }, {ψ 2 }, and {ψ 1 , ϕ 2 }.

Definition 10 (Composition). The composition of sets of rules

R 0 and R 1 is R 0 ∧ R 1 := { ρ∈S ρ | S ⊆ R 0 ∪ R 1 irreducible synchronous}. Example 15. Let R 0 and R 1 be sets of rules, with free(R 0 ) ∩ free(R 1 ) = ∅. By Example 13, we find that {ρ} ⊆ R 0 ∪ R 1 , for all ρ ∈ R 0 ∪ R 1 , is irreducible syn- chronous. Hence, every synchronous set S ⊆ R 0 ∪ R 1 , with |S| ≥ 2, is reducible. Therefore, S ⊆ R 0 ∪ R 1 is irreducible synchronous if and only if S = {ρ}, for some ρ ∈ R 0 ∪ R 1 . We conclude that R 0 ∧ R 1 = R 0 ∪ R 1 .
Consequently, ∅ is a (unique) identity element with respect to composition ∧ of sets of rules.

To show that the composition of sets of rules coincides with conjunction of stream constraints, we need the following result that shows that every non-empty synchronous set can be covered by irreducible synchronous sets. Lemma 3. Let R 0 and R 1 be sets of rules, and let S ⊆ R 0 ∪ R 1 be a non-empty synchronous set. Then, S = n i=1 S i , where

S i ⊆ R 0 ∪ R 1 , for 1 ≤ i ≤ n, is irreducible synchronous.
Proof. We prove the lemma by induction on the size |S| of S. For the base case, suppose that |S| = 1. We show that S is irreducible synchronous, which provides a trivial covering. Suppose that S = S 0 ∪ S 1 , for some synchronous sets S 0 , S 1 ⊆ R 0 ∪R 1 . Since, |S| = 1, we have S ⊆ S i ⊆ S, for some i ∈ {0, 1}. Hence, S = S i , and S is irreducible. We conclude that the lemma holds, for |S| = 1.

For the induction step, suppose that |S| = k > 1, and suppose that the lemma holds, for |S| < k. If S is irreducible, we find a trivial covering of S. If S is reducible, we find S = S 0 ∪ S 1 , where

S 0 = S = S 1 are synchronous sets in R 0 ∪ R 1 . Since |S i | < |S|, for i ∈ {0,
Theorem 3. rbf(R 0 ∧ R 1 ) rbf(R 0 ) ∧ rbf(R 1 )
, for all sets of rules R 0 and R 1 .

Proof. By Lemma 4 and Definition 10, deg

x (rbf(R 0 ∧ R 1 )) = deg x (rbf(R 0 ) ∧ rbf(R 1 )), for all x ∈ X. Hence, free k (rbf(R 0 ∧ R 1 )) = free k (rbf(R 0 ) ∧ rbf(R 1 )), for all k ≥ 0. Next, we show rbf(R 0 ) ∧ rbf(R 1 )) |= rbf(R 0 ∧ R 1 ). Let θ ∈ L(rbf(R 0 ) ∧ rbf(R 1 )
). By Definition 7, we must show that for every x ∈ free(R 0 ∧ R 1 ) there exists some

ρ x ∈ R 0 ∧ R 1 such that x ∈ free(ρ x ) and either θ |= x † d(x) or θ |= ρ x . Hence, suppose that θ / ∈ L(x † d(x)
), for some variable x ∈ free(R 0 ∧ R 1 ). Since free(R 0 ∧ R 1 ) = free(R 0 ) ∪ free(R 1 ) and θ |= free(R 0 ) ∧ free(R 1 ), we find from Definition 7 some ψ ∈ R 0 ∪ R 1 , with θ |= ψ and x ∈ free(ψ). We now show that there exists an irreducible synchronous set S ⊆ R 0 ∪ R 1 , such that, for ρ x := ρ∈S ρ, we have θ |= ρ x and x ∈ free(ρ x ). By repeated application of Definition 8, we construct a finite sequence

{ψ} = S 0 • • • S n , such that S n ⊆ R 0 ∪R 1 is synchronous, and θ |= ρ∈Sn ρ. Suppose S k ⊆ R 0 ∪R 1 , for k ≥ 1,
is not synchronous. By Definition 8, there exists some i ∈ {0, 1} and a variable x ∈ free(S k ) ∩ free(R i ), such that x / ∈ free(S k ∩ R i ). Since x ∈ free(R i ), we have

R x i := {ρ ∈ R i | x ∈ free(ρ)} = ∅. Since θ |= rbf(R i ), there exists some ψ k ∈ R x i such that θ |= ψ k . Now define S k+1 := S k ∪{ψ k }. Since x /
∈ free(S k ∩R i ) and x ∈ free(S k+1 ∩ R i ), we have a strict inclusion S k S k+1 . Due to these strict inclusions, we have, for k

≥ |R 0 ∪ R 1 |, that S k = R 0 ∪ R 1 , which is trivially synchronous in R 0 ∪ R 1 .
Therefore, our sequence S 0 • • • of inclusions terminates, from which we conclude the existence of S n . By Lemma 3, we find some irreducible synchronous set S ⊆ S n , such that ψ ∈ S. We conclude that ρ x := ρ∈S ρ ∈ R 0 ∧R 1 satisfies θ |= ρ x and x ∈ free(ψ) ⊆ free(S) = free(ρ x ). By Definition 7, we have θ |= rbf(R 0 ∧ R 1 ), and rbf(R

0 ) ∧ rbf(R 1 ) |= rbf(R 0 ∧ R 1 ). Finally, we prove that rbf(R 0 ∧ R 1 ) |= rbf(R 0 ) ∧ rbf(R 1 ). Let θ ∈ L(rbf(R 0 ∧ R 1 )
). We show that θ |= rbf(R i ), for all i ∈ {0, 1}. By Definition 7, we must show that for every i ∈ {0, 1} and every x ∈ free(R i ) there exists some ρ ∈ R i such that x ∈ free(ρ) and either θ |= x † d(x) or θ |= ρ. Hence, let i ∈ {0, 1} and x ∈ free(R i ) be arbitrary, and suppose that θ / ∈ L(x † d(x) ). Since free(R i ) ⊆ free(R 0 ∧ R 1 ), it follows from our assumption θ |= rbf(R 0 ∧ R 1 ) that θ |= ρ∈S ρ, for some irreducible synchronous set S ⊆ R 0 ∪R 1 satisfying x ∈ free(S). Since S ⊆ R 0 ∪R 1 synchronous, we find that x ∈ free(S) ∩ free(R i ) = free(S ∩ R i ). Hence, we find some ρ ∈ S ∩ R i , such that θ |= ρ and x ∈ free(ρ). By Definition 7, we conclude that θ |= rbf(R i ), for all i ∈ {0, 1}. Therefore, rbf(R Example 16. Let ϕ i and ψ i , for i ≥ 1, be the rules from Example 12. By Example 14, the composition fifo 2 := 2 i=1 fifo(a i , a i+1 , m i ) is defined by the set of rules {ϕ 1 , ψ 1 ∧ ϕ 2 , ψ 2 }. 1 To compute a set of rules that defines the composition, it is not efficient to enumerate all (exponentially many) synchronous subsets of R 0 ∪ R 1 and remove all reducible sets. Our tools use an algorithm based on hypergraph transformations to compute the irreducible synchronous sets. The details of this algorithm fall outside the scope of this paper. Figure 2 shows a graphical representation of composition fifo 2 , using hypergraphs. These hypergraphs consist of sets of hyperedges (x, F ), where x is a variable and F is a set of rules. Each hyperedge (x, F ) in a hypergraph corresponds to a disjunction x † d(x) ∨ ρ∈F ρ of the rule-based form in Definition 7.

0 ∧ R 1 ) rbf(R 0 ) ∧ rbf(R 1 ). ϕ 1 ψ 1 ϕ 2 ψ 2 a 1 m 1 a 2 m 2 a 3 (a) 2 i=1 rbf({ϕi, ψi}) ϕ 1 ψ 1 ∧ ϕ 2 ψ 2 a 1 m 1 a 2 m 2 a 3 (b) rbf( 2 i=1 {ϕi, ψi})

Complexity

In the worst case, composition R 0 ∧ R 1 of arbitrary sets of rules R 0 and R 1 may consists of |R 0 | × |R 1 | rules. However, if R 0 and R 1 are simple, the size of the composition is bounded by Lemma 5. Let R 0 and R 1 be sets of rules, such that free(R 0 ) ∩ free(R 1 ) ⊆ P (rbf(R 0 ∪ R 1 )), and let S ⊆ R 0 ∪ R 1 be synchronous. Let G S be a graph with vertices S and edges E S = {(ρ, ρ ) ∈ S 2 | free(ρ)∩free(ρ )∩P (rbf(R 0 ∪R 1 )) = ∅}.

|R 0 | + |R 1 |. Definition 11 (Simple). A set R of rules is simple if and only if free(ρ) ∩ free(ρ ) ∩ P (rbf(R)) = ∅ implies ρ = ρ , for every ρ, ρ ∈ R.
If S irreducible, then G S is connected.

Proof. Suppose that G S is disconnected. We find ∅ = S 0 , S 1 ⊆ S, with S 0 ∪ S 1 = S, S 0 ∩ S 1 = ∅ and free(S 0 ) ∩ free(S 1 ) ∩ P (rbf(R 0 ∪ R 1 )) = ∅. We show that S 0 and S 1 are synchronous. Let i, j ∈ {0, 1} and x ∈ free(S i ) ∩ free(R j ). We distinguish two cases: Case 1 (x ∈ free(R 1-j )): Then, x ∈ free(R 0 ) ∩ free(R 1 ) ⊆ P (rbf(R 0 ∪ R 1 )). Since free(S 0 )∩free(S 1 )∩P (rbf(R 0 ∪R 1 )) = ∅, we have x / ∈ free(S 1-i ). Since S is synchronous, we have x ∈ free(S i ) ∩ free(R j ) ⊆ free(S) ∩ free(R j ) ⊆ free(S ∩ R j ). Hence, we find some ρ ∈ S ∩ R j , with x ∈ free(ρ). Since x / ∈ free(S 1-i ), we conclude that ρ ∈ S i ∩ R j . Thus, x ∈ free(S i ∩ R j ), if x ∈ free(R 1-j ).

Case 2 (x / ∈ free(R 1-j )): Since x ∈ free(S i ), we find some ρ ∈ S i , with x ∈ free(ρ). Since x / ∈ free(R 1-j ), we conclude that ρ ∈ R j . Hence, x ∈ free(ρ) ⊆ free(S i ∩ R j ), if x / ∈ free(R 1-j ). We conclude in both cases that x ∈ free(ρ) ⊆ free(S i ∩ R j ). Hence, free(S i ) ∩ free(R j ) ⊆ free(S i ∩ R j ), for all i, j ∈ {0, 1}, and we conclude that S 0 and S 1 are synchronous. Since S 0 = S = S 1 , we conclude that S is reducible. By contraposition, we conclude that G S is connected, whenever S is irreducible. Lemma 6. Let R 0 and R 1 be simple sets of rules, with free(R 0 ) ∩ free(R 1 ) ⊆ P (rbf(R 0 ∪R 1 )), and let S 0 , S 1 ⊆ R 0 ∪R 1 be irreducible synchronous. If S 0 ∩S 1 = ∅, then S 0 = S 1 .

Proof. Suppose that S 0 ∩ S 1 = ∅. Then, there exists some ρ 0 ∈ S 0 ∩ S 1 . We show that S i ⊆ S 1-i , for all i ∈ {0, 1}. Let i ∈ {0, 1}, and ρ ∈ S i . By Lemma 5, we find an undirected path in G Si from ρ 0 to ρ. That is, we find a sequence ρ 0 ρ 1 • • • ρ n ∈ S * , such that ρ n = ρ and (ρ i , ρ i+1 ) ∈ E Si , for all 0 ≤ i < n. We show by induction on n ≥ 0, that ρ n ∈ S 1-i . For the base case (n = 0), observe that ρ n = ρ 0 ∈ S 0 ∩ S 1 ⊆ S 1-i . For the induction step, suppose that ρ n ∈ S 1-i . By construction of G Si , we find that free(ρ n )∩free(ρ n+1 )∩P 01 = ∅, where P 01 = P (rbf(R 0 ∪ R 1 )). Let j ∈ {0, 1}, such that ρ n+1 ∈ R j . Since ρ n ∈ S 1-i and S 1-i is synchronous, we have ∅ = free(S 1-i ) ∩ free(R j ) ∩ P 01 = free(S 1-i ∩ R j ) ∩ P 01 . We find some ρ ∈ S 1-j ∩ R j , with free(ρ n+1 ) ∩ free(ρ ) ∩ P 01 = ∅. Since R j is simple, we have ρ n+1 = ρ ∈ S 1-i , which concludes the proof by induction. It follows from ρ n ∈ S 1-i that S i ⊆ S 1-i , for all i ∈ {0, 1}, that is, S 0 = S 1 .

As seen in Lemma 2, the number of clauses in the disjunctive normal form dnf(R 0 ∧ R 1 ) can be exponential in the number of rules |R 0 ∧ R 1 | of the composition of R 0 and R 1 . However, the following (main) theorem shows the number of rules required to define i φ i is only linear in k.

(R 0 ) ∩ free(R 1 ) ⊆ P (rbf(R 0 ∪ R 1 )), then R 0 ∧ R 1 is simple and |R 0 ∧ R 1 | ≤ |R 0 | + |R 1 |.
Proof. From Lemmas 3 and 6, we find that the irreducible synchronous subsets partition R 0 ∪ R 1 . We conclude that |R 0 ∧ R 1 | ≤ |R 0 | + |R 1 |. We now show that R 0 ∧ R 1 is simple. Let ρ 0 and ρ 1 be rules in R 0 ∧ R 1 , with free(ρ 0 ) ∩ free(ρ 1 ) ∩ P 01 = ∅, where P 01 = P (rbf(R 0 ∪ R 1 )). By Definition 10, we find, for all i ∈ {0, 1}, an irreducible synchronous set S i , such that ρ i = ψ∈Si ψ. Since free(ρ 0 )∩free(ρ 1 )∩P 01 = ∅ and free(ρ i ) = free(S i ), for all i ∈ {0, 1}, we find some x ∈ free(S 0 )∩free(S 1 )∩P 01 . Suppose that x ∈ free(R j ), for some j ∈ {0, 1}. Since S 0 and S 1 are synchronous sets, we have x ∈ free(S i ) ∩ free(R j ) ⊆ free(S i ∩ R j ), for all i ∈ {0, 1}. We find, for all i ∈ {0, 1}, some ψ i ∈ S i ∩ R j , such that x ∈ free(ψ i ). Hence, free(ψ 0 ) ∩ free(ψ 1 ) ∩ P 01 = ∅, and since R j is simple, we conclude that ψ 0 = ψ 1 . Therefore, S 0 ∩S 1 = ∅, and Lemma 6 shows that S 0 = S 1 and ρ 0 = ρ 1 . We conclude that R 0 ∧ R 1 is simple.

The number of clauses in the disjunctive normal form of direct compositions of k fifo constraints grows exponentially in k. This typical pattern of a sequence of queues manifests itself in many other constructions, which causes serious scalability problems (cf., the benchmarks for 'Alternator k ' in [START_REF] Jongmans | Constraint automata with memory cells and their composition[END_REF]Section 7.2]). However, Theorem 4 shows that rule-based composition of k fifo constraints does not suffer from scalability issues: by Example 17, the fifo constraint can be defined by a simple set of rules. The result in Theorem 4, therefore, promises (exponential) improvement over the classical constraint automaton representation.

Unfortunately, it seems impossible to define any arbitrary stream constraint by a simple set of rules. Therefore, the rule-based form may still blow up for certain stream constraints. It seems, however, possible to recognize even more symmetries (cf., the queue-optimization in [START_REF] Jongmans | Automata-based optimization of interaction protocols for scalable multicore platforms[END_REF]) to avoid explosion and obtain comparable compilation and execution performance for these stream constraints.

Abstraction

We now study how existential quantification of stream constraints operates on its defining set of rules.

Definition 12 (Abstraction). Hiding a variable x in a set of rules R yields ∃xR := {∃xρ | ρ ∈ R}.

Unfortunately, ∃xR does not always define ∃xφ, for a stream constraint φ defined by a set of rules R. The following result shows that ∃xR defines ∃xφ if and only if rbf(∃xR) |= ∃x rbf(R). In this case, we call variable x hidable in R.

It is non-trivial to find a defining set of rules for ∃xφ, if x is not hidable in R, and we leave this as future work.

Theorem 5. Let R be a set of rules, and let x ∈ X be a variable. Then, ∃x rbf(R) rbf(∃xR) if and only if rbf(∃xR) |= ∃x rbf(R).

Proof. Trivially, ∃x rbf(R) rbf(∃xR) implies rbf(∃xR) |= ∃x rbf(R). Conversely, suppose that rbf(∃xR) |= ∃x rbf(R). From Lemma 2, it follows that ∃x rbf(R) ≡ ∃x dnf(R). Since existential quantification distributes over disjunction and ∃xφ ∧ ψ |= ∃xφ ∧ ∃xψ, for all stream constraints φ and ψ, we find

∃x dnf(R) |= S⊆R ρ∈S ∃xρ ∧ x =y∈free(R)\free(S) y † d(y) ≡ dnf(∃xR).
By Lemma 2, we have ∃x rbf(R) |= rbf(∃xR), and by assumption ∃x rbf(R) ≡ rbf(∃xR). Using Lemma 4, we have deg y (∃x rbf(R)) = max ρ∈R deg y (∃xρ) = deg y (rbf(∃xR)), for every variable y. We conclude ∃x rbf(R) rbf(∃xR).

Example 18. Suppose Data = {0, 1}, which means that the data domain equals D = {0, 1, * }. Let 1 be the constant stream defined as 1(n) = 1, for all n ∈ N. For i ∈ {0, 1}, consider the set of rules

R i = {x = x, x = y i = i}. Observe that {x = x, x = y i = i} ⊆ R 0 ∪ R 1 is synchronous, for all i ∈ {0, 1}. Hence, x = y i = i ∈ R 0 ∧ R 1 , for all i ∈ {0, 1}. However, for θ = [y 0 → 0, y 1 → 1], we have θ |= i∈{0,1} ∃x(x = y i = i), while ∃x i∈{0,1} x = y i = i ≡ ⊥. Thus, variable x is not hidable from R 0 ∧ R 1 .

Application

In on-going work, we applied the rule-based form to compile protocols (in the form of Reo connectors) into executable code. Reo is an exogenous coordination language that models protocols as graph-like structures [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Arbab | Puff, the magic protocol[END_REF]. We recently developed a textual version of Reo, which we use to design non-trivial protocols [START_REF] Dokter | Treo: Textual syntax of reo connectors[END_REF]. An example of such non-trivial protocol is the Alternator k , where k ≥ 2 is an integer. Figure 3(a) shows a graphical representation of the Alternator k protocol.

Intuitively, the behavior of the alternator protocol is as follows: The nodes P 1 , . . . , P k accept data from the environment. Node C offer data to the environment. All other nodes are internal and do not interact with the environment. In the first step of the protocol, the Alternator k waits until the environment is ready to offer data at all nodes P 1 , . . . , P k and is ready to accept data from node C. Only then, the Alternator k transfers the data from P k to C via a synchronous channel, and puts the data from P i in the i-th fifo channel, for all i < k. The behavior of a synchronous channel is defined by the sync stream constraint in Example 1. Each fifo channel has buffer capacity of one, and its behavior is defined by the fifo stream constraint from Example 3. In subsequent steps, the environment can one-by-one retrieve the data from the fifo channel buffers, until they are all empty. Then, the protocol cycles back to its initial configuration, and repeats its behavior. For more details on the Reo language and its semantics, we refer to [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Arbab | Puff, the magic protocol[END_REF].

As mentioned in the introduction, Jongmans developed a compiler based on constraint automata [START_REF] Jongmans | Constraint automata with memory cells and their composition[END_REF]. The otherwise stimulating benchmarks presented in [START_REF] Jongmans | Constraint automata with memory cells and their composition[END_REF] show that Jongmans' compiler still suffers from state-space explosion. Every fifo channel in the Alternator k , except the first, either accepts data from the environment or accepts data from the previous fifo channel. This choice is made by the internal node at the input of each fifo channel. Unfortunately, the behavior of such nodes is not defined in terms of a simple set of rules. Consequently, we cannot readily apply Theorem 4 to conclude that the number of rules depends only linearly on k. However, it turns out that Alternator k can be defined using only k rules: one rule for filling the buffers of all fifo channels, plus k -1 rules, one for taking data out of the buffer of each of the k -1 fifo channels. This observation explains why our compiler drastically improves upon Jongmans' compiler.

Conclusion

We introduce (regular) stream constraints as an alternative to constraint automata that does not suffer from state space explosions. We define the rule-based form for stream constraints, and we express composition and abstraction of constraints in terms of their rule-based forms. For simple sets of rules, composition of rule-based forms does not suffer from 'transition space explosions' either.

We have experimented with a new compiler for protocols using our rule-based form, which avoids the scalability problems of state-and transition-space explosions of previous automata-based tools. Our approach still leaves the possibility for transition space explosion for non-simple sets of rules. In the future, we intend to study symmetries in stream constraints that are not defined by simple sets of rules. The queue-optimization of Jongmans serves as a good source of inspiration for exploiting symmetries [START_REF] Jongmans | Automata-based optimization of interaction protocols for scalable multicore platforms[END_REF].

The results in this paper are purely theoretical. In on-going work, we show practical implications of our results by developing a compiler based on stream constraints. Such a compiler requires an extension to the current theory on stream constraints: we did not compute the abstraction ∃xR on sets of rules R wherein variable x is not hidable. Example 11 indicates the existence of situations where we can compute ∃xR even if x is not hidable, a topic which we leave as future work.

Example 1 .

 1 One of the simplest stream constraints is sync(a, b), which is defined as (a . = b). Constraint sync(a, b) encodes that the data streams at a and b are equal: θ(a)(k) = θ(b)(k), for all k ∈ N and all θ ∈ (D N ) X . Therefore, sync(a, b) synchronizes the data flow observed at ports a and b.

Fig. 1 .

 1 Fig. 1. Semantics of fifo(a, b, m) over the trivial data domain {0, * }.

Case 3

 3 (φ := ψ 0 ∧ ψ 1 ): By the induction hypothesis, Equation (3) holds for ψ 0 and ψ 1 . By conjunction of Equation (3), we conclude Equation (3) for φ. Case 4 (φ := ¬ψ): By the induction hypothesis, Equation (3) holds for ψ. By contraposition of Equation (3), we conclude Equation (3) for φ. Case 5 (φ := ∃yψ): If y = x, then x / ∈ free(φ) and both sides in Equation (3) are equivalent to θ (k) |= φ. Hence, Equation (3) holds for y = x. Suppose y

Example 8 .Example 9 .Example 10 .Example 11 .

 891011 ψ rbf({ψ}), for all reflexive stream constraints ψ, with deg(ψ) ≤ 1 and / ∈ ψ. Hence, Example 7 shows sync(a, b) = (a . The stream constraint lossy(a, b) := rbf({a . = a, a . = b}) is equivalent to (b . = * ∨ a . = b). Note that rbf({ , a . = b}) rbf({a . = b}) sync(a, b). Hence, rules a . = a and are very different. The set of rules that define a stream constraint is not unique. Consider the stream constraint fifo from Example 3. On the one hand, we have fifo(a, b, m) m . = * ∧ rbf({ϕ, ψ}), where ϕ a . = m . = 0 ∧ m . = * models the action that puts data in the buffer and ψ m . = * ∧b . = m . = 0 models the action that takes data out of the buffer. On the other hand, we have fifo(a, b, m) m . = * ∧ rbf({a . Rule-based forms are an alternative to disjunctive normal forms. Consider the reflexive constraint φ := n i=1 ρ i in DNF for which the first conjunctive clause ρ 1 is equivalent to x∈free(φ) x † d(x) , with d(x) = deg x (φ). By adding equalities of the form x .

  1}, we find by the hypothesis that S i = ni j=1 S ij . Hence, S = S 0 ∪ S 1 = 1 i=0 ni j=1 S ij . We conclude that the lemma holds, for |S| = k. By induction on |S|, we conclude the lemma. Lemma 4. deg x (rbf(R)) = max ρ∈R deg x (ρ), for all sets of rules R and x ∈ X. Proof. For any set of rules R and y ∈ X, we have deg y (rbf(R)) = max x∈free(R) max(deg y (x † d(x) ), max ρ∈R:x∈free(ρ) deg y (ρ)). Note that deg y (x † d(x) ) = d(y), if y = x, and deg y (x † d(x) ) = -1, otherwise. Since d(y) = max ρ∈R deg y (ρ), we have deg y (rbf(R)) = max ρ∈R deg y (ρ).

Fig. 2 .

 2 Fig. 2. Hypergraph representations of 2 i=1 fifo(ai, ai+1, mi).

Example 17 .

 17 By Example 10, the invariant of fifo(a, b, m) is defined by R := {a . The set R is simple, while R is not.

Theorem 4 .

 4 If R 0 and R 1 are simple sets of rules, and free

Figure 3 (Fig. 3 .

 33 Fig. 3. Graphical representation (a) of the Alternator k protocol in [17], for 2 ≤ k ≤ 500, and its compilation time (b). The dotted red line is produced by the Jongmans' compiler (and corresponds to [17, Fig 11(a)]), and the solid blue line is our compiler.

The rules for the composition of two fifo stream constraints has striking similarities with synchronous region decomposition developed by Proença et al.[START_REF] Proença | Dreams: a framework for distributed synchronous coordination[END_REF]. Indeed, ϕ1, ψ1 ∧ ϕ2, and ψ2 correspond to the synchronous regions in the composition of two buffers. Therefore, rule-based composition generalizes synchronous region decomposition that has been used as a basis for generation of parallel code[START_REF] Jongmans | Centralized coordination vs. partially-distributed coordination with reo and constraint automata[END_REF].

Dokter & Arbab

Acknowledgements The authors thank Benjamin Lion for his help in developing a rule-based compiler and for generating Figure 3(b).


Kiko Fernandez-Reyes

Dave Clarke

Elias Castegren

Huu-Phuc Vo

Forward to a Promising Future

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.

Introduction

Futures extend the actor programming model to express call-return synchronisation of message sends [START_REF] De Boer | A survey of active object languages[END_REF]. Each actor is single-threaded, but different actors execute concurrently. Communication between actors happens via asynchronous method calls (messages), which immediately return a future; futures are placeholders for the eventual result of these asynchronous method calls. An actor processes one message at a time and each message has associated a future that will be fulfilled with the returned value of the method. Futures are first-class values, and operations on them may be blocking, such as getting the result out of the future (get), or asynchronous, such as attaching a callback to a future. This last operation, known as future chaining (f x e), attaches a closure λx.e to the future f and immediately returns a new future that will contain the result of applying the closure to the value eventually stored in future f . Consider the following code (in the actor-based language Encore [START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF]) that implements the broker delegation pattern: the developer's intention is to connect clients (the callers of the Broker actor) to a pool of actors that will actually process a job (lines 6-7): The problem with this code is that the connection to the Broker cannot be completed immediately without blocking the Broker's thread of execution: returning the result of the worker running the computation requires that the Broker blocks until the future is fulfilled (line 8). This implementation makes the Broker the bottleneck of the application.

One obvious way to avoid this bottleneck is by returning the future, instead of blocking on it, as in the following code: This solution removes the blocking from Broker, but returns a future, which results in the client receiving a future containing a future Fut (Fut int), cluttering client code and making the typing more complex. Another way to avoid the bottleneck is to not block but yield the current thread until the future is fulfilled. This can be done using the await command [START_REF] Broch Johnsen | ABS: A core language for abstract behavioral specification[END_REF][START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF], which frees up the Broker to do other work: This solution frees up the Broker, but can result in a lot of memory being consumed to hold the waiting instances of calls Broker.run().

Another alternative is to use promises [START_REF] Liskov | Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems[END_REF]. A promise can be passed around and fulfilled explicitly at the point where the corresponding result is known. Passing a promise around is akin to passing the responsibility to provide a particular result, thereby fulfilling the promise. Promises are problematic because they diverge from the commonplace call-return control flow, there is no explicit requirement to actually fulfil a promise, and care is required to avoid fulfilling multiple times. This latter issue, fulfilling a promise multiple times, can be solved by a substructural type system, which guarantees a single writer to the promise [START_REF] Ábrahám | Behavioral interface description of an object-oriented language with futures and promises[END_REF][START_REF] Niehren | A concurrent lambda calculus with futures[END_REF]. Substructural type systems are more complex and not mainstream, which rules out adoption in languages such as Java and C#. Our solution relies on futures and is suitable for mainstream languages.

The main difference between promises and futures are that developers explictly create and fulfil promises, whereas futures are implictly created and fulfilled. Promises are thus more flexible at the expense of any fulfilment guarantees.

This paper explores a construct called forward that retains the guarantees of using futures, while allowing some degree of delegation of responsibility to fulfil a future, as in promises. This construct was first proposed a while ago [START_REF] Clarke | Concurrent objects à la carte[END_REF], but only recently has been implemented in the language Encore [START_REF] Brandauer | Parallel objects for multicores: A glimpse at the parallel language Encore[END_REF].

With forward, the run of Broker method now becomes: Forward delegates the fulfilment of the future that run will put its result in, to the call worker!start(job). Using forward frees up the Broker object, as run completes immediately, though the future is fulfilled only when worker!start(job) produces a result. The paper makes the following contributions:

a formalisation and soundness proof of the forward construct in a concise, high-level language (Section 2); a formalisation of a low-level, promise-based language (Section 3), a translation from the high-level language to the low-level language, a proof of program equivalence, between the high-level language and its translation to the low-level language (Section 4); and microbenchmarks that compare the get-and-return and await-and-get pattern versus the forward construct (Section 5).

This section presents a core calculus that includes tasks, futures and operations on them, and forward. The calculus consists of two levels: expressions and configurations. Expressions correspond to programs and what tasks evaluate. Configurations capture the run-time configuration; they are collections of tasks (running expressions), futures, and chains. This calculus is much more concise than the previous formalisation of forward [START_REF] Clarke | Concurrent objects à la carte[END_REF].

The syntax of the core calculus is as follows: Expressions include values (v ), function application (e e), spawning asynchronous computations (async e), future chaining (e x e ), which attaches λx.e onto a future to run as soon as the future produced by e is fulfilled, if-then-else expressions, forward, and get, which extracts the value from a future. Values are constants (c), futures (f ), variables (x ) and lambda abstractions (λx.e). The calculus has neither actors nor message sends/method calls. For our purposes, tasks play the role of actors and spawning asynchronous computations is analogous to message sends. Configurations, config , give a partial view on the system and are (non-empty) multisets of tasks, futures and chains. They have the following syntax:

config ::= (fut f ) | (fut f v) | (task f e) | (chain f f e) | config config
Future configurations are (fut f ) and (fut f v), representing an unfulfilled future f and a fulfilled future f with value v. Configuration (task f e) is a task running expression e that will write the result of e in future f. 4 Configuration (chain f g e) denotes a computation that waits until future g is fulfilled, applies expression e to the value stored in g in a new task whose result will be stored in future f . The initial configuration for program e is (task f e) (fut f ), where the result of e will be written into future f at the end result of the program's execution.

Operational Semantics

The operational semantics use a small-step semantics with reduction-based, contextual rules for evaluation within tasks. Evaluation contexts E contains a hole • that denotes where the next reduction step happens [START_REF] Wright | A syntactic approach to type soundness[END_REF]:

E ::= • | E e | v E | E x e | forward E | get E | if E then e else e (Red-If-True) (task f E[if true then e else e ]) -→ (task f E[e]) (Red-β) (task f E[λx.e v]) -→ (task f E[e[v/x]]) (Red-If-False) (task f E[if false then e else e ]) -→ (task f E[e ]) (Red-Fwd-Fut) (task f E[forward h]) -→ (chain f h λx.x) (Red-Chain-Run) (chaing f e) (fut f v) -→ (task g (e v)) (fut f v) (Red-Get) (task f E[get h]) (fut h v) -→ (task f E[v]) (fut h v) (Red-Fut-Fulfil) (task f v) (fut f ) -→ (fut f v) (Red-Async) fresh f (task g E[async e]) -→ (fut f ) (task f e) (task g E[f ]) (Red-Chain-Create) fresh g (task f E[h x e]) -→ (fut g ) (chaing h λx.e) (task f E[g])
Fig. 1: Reduction Rules. f, g, h range over futures. The evaluation rules are given in Fig. 1. The evaluation of if-then-else expressions and functions applications proceed in the standard fashion (Red-If-True, Red-If-False, and Red-β). The async construct spawns a new task to execute the given expression, and creates a new future to store its result (Red-Async). When the spawned task finishes its execution, it places the value in the designated future (Red-Fut-Fulfil). To obtain the contents of a future, the blocking construct get stops the execution of the task until the future is fulfilled (Red-Get). Chaining an expression on a future results immediately in a new future that will eventually contain the result of evaluating the expression, and a chain configuration storing the expression is connected with the original future (Red-Chain-Create). When the future is fulfilled, any chain configurations become task configurations and start evaluating the stored expression on the value stored in the future (Red-Chain-Run). Forward applies to a future where the result of the future computation will be the result of the current computation, stored in the future associated with the current task. Forwarding to future h throws away the remainder of the body of the current task and chains the identity function on the future, the effect of which is to copy the eventual result stored in h into the current future (Red-Fwd-Fut).

config → config config config → config config config ≡ config config → config config ≡ config config → config
The configuration evaluation rules (Fig. 2) describe how configurations make progress, which is either by some subconfiguration making progress, or by rewriting a configuration to one that will make progress using the equations of multisets.

Example and Optimisations

The following example illustrates some aspects of the calculus.

(task f E[async (forward h)]) (fut h 42) Red-Async -------→ (task f E[g]) (fut h 42) (fut g ) (task g forward h) Red-Fwd-Fut --------→ (task f E[g]) (fut h 42) (fut g ) (chain g h λx.x) Red-Chain-Run ----------→ (task f E[g]) (fut h 42) (fut g ) (task g (λx.x) 42) Red-β ----→ (task f E[g]) (fut h 42) (fut g ) (task g 42) Red-Fut-Fulfil ----------→ (task f E[g]) (fut h 42) (fut g 42)
Firstly, a new task is spawned with the use of async. This task forwards the responsibility to fulfil its future to (the task fulfilling) future h, i.e. future g gets fulfilled with the value contained in future h.

Two special cases of forward can be given more direct reduction sequences, which correspond to optimisations performed in the Encore compiler. The first case corresponds to forwarding directly to another method call, which is the primary use case for forward, namely, forwarding to another method forward(e!m()). The optimised reduction rule is

(task f E[forward (async e)]) → (task f e)
For comparison, the standard reduction sequence5 is

(task f E[forward (async e)]) → (task f E[forward g]) (task g e) (fut g ) → (chain f g λx.x) (task g e) (fut g ) → * (chain f g λx.x) (task g v) (fut g ) → (chain f g λx.x) (fut g v) → (task f (λx.x) v) (fut g v) → (task f v) (fut g v)
This can be seen as equivalent to the reduction sequence

(task f E[forward (async e)]) → (task f e) → * (task f v)
because the future g will no longer be accessible.

Similarly, forwarding a future chain can be reduced directly to a chain configuration:

(

task f E[forward (h x e)]) → (chain f h λx.e)
In both cases, forward can be seen as making a call-with-current-future.

Fig. 3: Typing Rules

Static Semantics

The type system has basic types, K, and future types:

τ ::= K | Fut τ
The typing rules (Fig. 3) define the judgement Γ ρ e : τ , which states that in the typing environment Γ , which gives the types of futures and free variables, expression e has type τ , where ρ is the expected task type, the result type of the task in which the expression appears. ρ ranges over both types τ and symbol • which is not a type. • is used to prevent the use of forward in contexts where the expected task type is not clear, specifically within closures, as a closure can be passed between tasks and run in a context different from their defining contexts. The types of constants are assumed to be provided (Rule T-Constant). Variables and futures types are defined in the typing environment (Rules T-Variable and T-Future). Function application and abstraction have the standard typing rules (Rules T-Application and T-Abstraction), except that within the body of a closure the expected task type is not known. When async is applied to an expression e, a new task is created and the expected task type changes to the type of the expression. The result type of the async call is a future type of the expression's type (Rule T-Async). Chaining is essentially mapping for the Fut type constructor, and rule T-Chain reflects this fact. In addition, because chaining ultimately creates a new task to run the expression, the expected task type ρ changes to the return type of the expression. Getting the value from a future of some type results in a value of that type (Rule T-Get). Forwarding requires the argument to forward to be a future of the same type as the expected task type (Rule T-Forward). As forward does not return locally, the result type is arbitrary.

Well-formed configurations, Γ config ok, are typed against environment, Γ , that gives the types of futures (Fig. 4). The type rules depend on the following definitions. writers( ) = ∅ Rules Fut and F-Fut define well-formed future configurations. Rules Task and Chain define well-formed task and future chaining configurations and set the expected task types. Rule Config defines how to build larger configurations from smaller ones. Each future may be defined at most once and there is at most one writer to each future.

(Fut) f ∈ dom(Γ ) Γ (fut f ) ok (F-Fut) f : Fut τ ∈ Γ Γ • v : τ Γ (fut f v) ok (Task) f : Fut τ ∈ Γ Γ τ e : τ Γ (task f e) ok (Chain) f : Fut τ ∈ Γ g : Fut τ ∈ Γ Γ τ e : τ → τ Γ (chain f g e) ok (Config) Γ config 1 ok Γ config 2 ok defs(config 1 ) ∩ defs(config 2 ) = ∅ writers(config 1 ) ∩ writers(config 2 ) = ∅ Γ config 1 config 2 ok

defs((fut

f )) = defs((fut f v)) = {f } defs((config 1 config 2 )) = defs(config 1 ) ∪ defs(config 2 ) defs( ) = ∅
The rules for well-formed configurations apply to partial configurations. Complete configurations can be typed by adding extra conditions to ensure that all futures in Γ have a future configuration, there is a one-to-one correspondence between tasks/chains and unfulfilled futures, and dependencies between tasks are acyclic. These definitions have been omitted and are similar to those found in our earlier work [START_REF] Fernandez-Reyes | ParT: An asynchronous parallel abstraction for speculative pipeline computations[END_REF].

Formal Properties

The proof of soundness of the type system follows standard techniques [START_REF] Wright | A syntactic approach to type soundness[END_REF]. The proof of progress requires that there is no deadlock, which follows as there is no cyclic dependency between tasks [START_REF] Fernandez-Reyes | ParT: An asynchronous parallel abstraction for speculative pipeline computations[END_REF].

Lemma 1 (Type preservation). If Γ config ok and config → config , then there exists a Γ such that Γ ⊃ Γ and Γ config ok

Proof. By induction on the derivation of config → config .

Definition 3 (Terminal Configuration).

A complete configuration config is terminal iff every element of the configuration has the shape: (fut f v).

Lemma 2 (Progress). For a complete configuration config , if Γ config ok, then config is a terminal configuration or there exists a config such that config → config .

Proof. By induction on a derivation of config → config , relying on the invariance of the acyclicity of task dependencies.

A Promising Implementation Calculus

The implementation of forward in the Encore programming language is via compilation into C, linking with Pony's actor-based run-time [START_REF] Clebsch | Fully concurrent garbage collection of actors on many-core machines[END_REF]. At this level, Encore's futures are treated like promises in that they are passed around to the place where the result of a method call is known in order to be fulfilled. To model this implementation approach, we introduce a low-level target calculus based on tasks and promises. This section presents the formalised target calculus, and the next section presents the compilation strategy from the source to the target language.

The syntax of the target language is as follows: Expressions consist of values, function application (e e), sequential composition of expressions (e; e), the spawning and stopping of tasks (Task(e, e) and stop), the creation, fulfilment, reading, and chaining of promises (Prom, fulfil(e, e), get e, and Chain(e, e, e)) and the standard if-then-else expression. Values are constants, futures, variables, abstractions and unit (). The main differences with the source language are that tasks have to be explicitly stopped, which captures non-local exit, and promises must be explicitly created and fulfilled.

Operational Semantics

The semantics of the target calculus is analogous to the source calculus. The evaluation contexts are:

E ::= • | E e | v E
(prm f v) (task E[fulfil(f, v )]) -→ ERROR (RI-If-False) (task E[if false then e else e ]) -→ (task E[e ]) (RI-Promise) freshf (task E[Prom]) -→ (prm f ) (task E[f ]) (RI-Statement) (task E[v; e]) -→ (task E[e]) (RI-Chain) (task E[Chain(f, g, (λx.e))]) -→ (chain g e[f /x]) (task E[f ]) (RI-β) (task E[(λx.e) v]) -→ (task E[e[v/x]]) (RI-Fulfil) (prm f ) (task E[fulfil(f, v)]) -→ (prm f v) (task E[()]) (RI-Stop) (task E[stop]) -→ (RI-Task) (task E[Task(f, (λx.e))]) -→ (task E[f ]) (task e[f /x]) (RI-Config-Chain) (chain g e) (prm g v) -→ (task (e v)) (prm g v) (RI-Get) (task E[get h]) (prm h v) -→ (task E[v]) (prm h v)
Fig. 5: Target reduction rules Configurations are multisets of promises, tasks, and chains:

config ::= | (prm f ) | (prm f v) | (task e) | (chain f e) | config config
The empty configuration is represented by , an unfulfilled promise is written as (prm f ) and a fulfilled promise holding value v is written as (prm f v).

Tasks and chains work in the same way as in the source language, except that they work now on promises (Fig. 5). Promises are handled much more explicitly than futures are, and need to be passed around like regular values. The creation of a task needs a promise and a function to run; the spawned task runs the function, has access to the passed promise and leaves the promise reference in the spawning task (RI-Task). Stopping a task just finishes the task (RI-Stop). The construct Prom creates an empty promise (RI-Promise). Fulfilling a promise results in the value being stored if the promise was empty (RI-Fulfil), or an error otherwise (RI-Error). Promises are chained in a similar fashion to futures: the construct Chain(f, g, e) immediately passes the promise f to expression ethe intention being that f will hold the eventual result; the chain then waits on promise g, and passes the value it receives into expression (e f ) (RI-Chain and RI-Config-Chain). The target language borrows the configuration evaluation rules from the source language (Fig. 2).

Example For illustration purposes we translate the example from the high-level language, (fut f ) (task f E[forward (async e)]) shown in Section 2, and show the reduction steps of the low-level language:

-→ (prm f ) (prm g ) (task E[f ; stop]) (chain g (λx.fulfil(f, x); stop)) (task fulfil(g, e); stop) -→ (prm f ) (prm g ) (task E[stop]) (chain g (λx.fulfil(f, x); stop)) (task fulfil(g, e); stop) -→ (prm f ) (prm g ) (chain g (λx.fulfil(f, x); stop)) (task fulfil(g, e); stop) -→ * (prm f ) (prm g ) (chain g (λx.fulfil(f, x); stop)) (task fulfil(g, v); stop) -→ (prm f ) (prm g v) (chain g (λx.fulfil(f, x); stop)) (task (); stop) -→ (prm f ) (prm g v) (chain g (λx.fulfil(f, x); stop)) (task stop) -→ (prm f ) (prm g v) (chain g (λx.fulfil(f, x); stop)) -→ (prm f ) (prm g v) (task (λx.fulfil(f, x); stop) v) -→ (prm f ) (prm g v) (task fulfil(f, v); stop) -→ (prm f v) (prm g v) (task (); stop) -→ (prm f v) (prm g v) (task stop) -→ (prm f v) (prm g v)
We show how the compilation strategy proceeds in Section 4.

Static Semantics

The type system has basic types, K, and promise types defined below:

τ ::= K | Prom τ
The type rules define the judgment Γ e : τ which states that, in the environment Γ , which records the types of promises and free variables, expression e has type τ . The rules for constants, promises, and variables, if-then-else, abstraction and function application are analogous to the source calculus, except no expected task type is recorded. The unit value has type unit (TI-Unit); the stop expression finishes a task and has any type (TI-Stop). The creation of a promise has type Prom τ (TI-Promise-New); the fulfilment of a promise fulfil(e, e ) has type unit and requires the first parameter to be a promise and the second to be an expression that matches the type of the promise (TI-Fulfil). To spawn a task (Task(e, e)), the first argument of the task must be a promise and the second a function that takes a promise having the same type as the first argument (TI-Task); promises can be chained on with functions that run if the promise is fulfilled: Chain(e, e , e ) has type Prom τ and e and e are promises and e is an abstraction that takes arguments of the first and second promise types. Both task and chain constructors return the promise that is passed to them, for convenience in the compilation scheme.

Soundness of the type system is proven using standard techniques.

(TI-Constant) c is a constant of type τ Γ c : τ Γ config 1 ok Γ config 2 ok Γ config 1 config 2 ok
Fig. 6: Typing rules for expressions and configurations in the target language 4 Compilation: From Futures and Forward to Promises

This section presents the compilation function from the source to the target language and outlines a proof that it preserves semantics. The compilation strategy is defined inductively (Fig. 7); the compilation of expressions, denoted C e destiny , takes an expression e and a meta-variable destiny which holds the promise that the current task should fulfil, and produces an expression in the target language. Futures are translated to promises, and most other expressions are translated homomorphically. The constructs where something interesting happens are async, forward and future chaining; these constructs adopt a common pattern implemented using a two parameter lambda abstraction: the first parameter, variable destiny , is the promise to be fulfilled and the second parameter is the value that fulfils the promise. The best illustration of how forward behaves differently from a regular asynchronous call is the difference in the rules

T (fut f v) = (prm f C v f ) T config config = T config T config T (chain f g e) = (chain g (λx.fulfil(f, C e f x); stop))
where x is fresh for async e and the optimised rule for forward (async e). The translation of async e creates a new promise to store e's result value, whereas the translation of forward(async e) reuses the promise from the context, namely the one passed in via the destiny variable. The compilation of configurations, denoted T config , translates configurations from the source language to the target language. For example, the compilation of the source configuration (fut f ) (task f forward (async e)) compiles into:

T (task f e) = (task (fulfil(f, C e f ); stop)) C τ Type translation C ok = ok C K = K C Fut τ = Prom C τ C τ → τ = C τ → C τ T Γ f : τ Environment Translation T Γ ρ config = C Γ T config C ∅ = C Γ, f : Fut τ = C Γ , C f : Fut τ C x : τ = x : C τ C Γ, x : τ = C Γ , C x : τ C f : Fut τ = f : C Fut τ
T (fut f ) (task f forward (async e)) = T (fut f ) T (task f forward (async e)) = (prm f ) (task fulfil(f, C forward (async e) f ))
The optimised compilation of C forward (async e) f is:

(prm f ) (task E[Task(f, (λd .fulfil(d , C e d ); stop)); stop])
For comparison, the base compilation gives: Types and typing rules are compiled inductively (Fig. 7). The following lemmas guarantee that the compilation strategy does not produce broken target code and state the correctness of the translation.

Correctness

The correctness of the translation is proven in a number of steps.

The first step involves converting the reduction rules to a labelled transition system where communication via futures is made explicit. This involves splitting several rules involving multiple primitive configurations on the left-hand side to involve single configurations, and labelling the values going into and out of futures. For example, (task f v) (fut f ) → (fut f v) is replaced by the two rules:

(task f v) f ↓v --→ (fut f ) f ↓v --→ (fut f v)
The other rules introduced are:

(fut f v) f ↑v --→ (fut f v) (task f E[get h]) h↑v --→ (task f E[v]) (chain g f e) f ↑v --→ (task g e[v/x])
Label f ↓ v captures a value being written to a future, and label f ↑ v captures a value being read from a future, both from the future's perspective. Labels f ↓ v and f ↑ v are the duals from the perspective of the remainder of the configuration. The remainder of the rules are labelled with τ to indicate that no observable behaviour occurs. The same pattern is applied to the target language.

It is important to note that the values in the labels of the source language are the compiled values, while the values in the labels of the target language remain the same. 6 This is needed so that labelled values such as lambda abstraction match during the bisimulation game.

The composition rules are adapted to propagate or match labels in the standard way. For instance, the rule for matching labels in parallel configurations is:

config l -→ config config l -→ config config config τ -→ config config
The following theorems capture correctness of the translation.

Theorem 1. If Γ config ok, then C Γ T config ok.
Theorem 2. If Γ config ok, then config ∼ T config .

The first theorem states that translating well-typed configurations results in well-typed configurations. The second theorem states that any well-typed configuration in the source language is bisimilar to its translation. The precise notion of bisimilarity used is bisimilarity up-to expansion [START_REF] Pous | Enhancements of the bisimulation proof method[END_REF]. This notion of bisimilarity compresses the administrative, unobservable transitions introduced by the translation.

The proof involves taking each derivation rule in the adapted semantics for the source calculus (described above) and showing that each source configuration is bisimilar to its translation. This is straightforward for the base cases, because tasks are deterministic in both source and target languages, and at most two unobservable transitions are introduced by the translation. To handle the parallel composition of configurations, bisimulation is shown to be compositional, meaning that if config ∼ T config and config ∼ T config , then config config ∼ T config config ; now by definition T config config = T config T config , hence config config ∼ T config T config .

Experiments

We benchmarked the implementation of forward by comparing it against the blocking pattern get-and-return and an implementation that uses the awaitand-get (both described in Section 1). The micro-benchmark used is a variant of the broker pattern with 4 workers, compiled with aggresive optimisations (-O3). We report the average time (wall clock) and memory consumption of 5 runs of this micro-benchmark under different workloads (Fig. 8). The processing of each message sent involves complex nested loops with quadratic complexity (in the Workload value) written in such a way to avoid the compiler optimising them away -the higher the workload, the higher the probability that the Broker actor blocks or awaits in the non-forward implementations. The performance results (Fig. 8) show that the forward version is always faster than the get-and-return and await-and-get version. In the first case, this is expected as blocking prevents the Broker actor from processing messages, while the forward version does not block. In the second case, we also expected the forward version to be faster than the await-and-get: this is due to the overhead of the context switching operation performed on each await statement.

The forward version consumes the least amount of memory, while the awaitand-get version consumes the most (Fig. 8). This is expected: forward creates one fewer future per message sent than the other two versions; the await-and-get version has around 5 times more overhead than the forward implementation, as it needs to save the context (stack) whenever a future cannot immediately be fulfilled.

Threats to validity The experiments use a microbenchmark, which provides useful information but is not as comprehensive as a case study would be.

Related work

Baker discovered futures in 1977 [START_REF] Henry | The incremental garbage collection of processes[END_REF]; later Liskov introduced promises to Argus [START_REF] Liskov | Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems[END_REF]. Around the same time, Halstead introduced implicit futures in Multilisp [START_REF] Halstead | Multilisp: A language for concurrent symbolic computation[END_REF]. Implicit futures do not appear as a first-class construct in the programming language at either the term or type level, as they do in our work.

The forward construct was introduced in earlier work [START_REF] Clarke | Concurrent objects à la carte[END_REF], in the formalisation of an extension to the active object-based language Creol [START_REF] Broch Johnsen | Creol: A type-safe objectoriented model for distributed concurrent systems[END_REF]. The main differences with our work are: our core calculus is much smaller, based on tasks rather than active objects; our calculus includes closures, which complicate the type system, and future chaining; we defined a compilation strategy for forward, and benchmark its implementation.

Caromel et al. [START_REF] Caromel | Asynchronous sequential processes[END_REF] formalise an active object language that transparently handles futures, prove determinism of the language using concepts similar to weak bisimulation, and provide an implementation [START_REF] Caromel | ProActive: an integrated platform for programming and running applications on grids and P2P systems[END_REF]. In contrast, our work uses a task-based formalism built on top of the lambda calculus and uses fu-tures explictly. It is not clear whether forward can be used in conjunction with transparent futures.

Proving semantics preservation of whole programs is not a new idea [START_REF] Leroy | A formally verified compiler back-end[END_REF][START_REF] Leroy | Formal certification of a compiler back-end or: programming a compiler with a proof assistant[END_REF][START_REF] Lochbihler | Verifying a compiler for Java threads[END_REF][START_REF] Chlipala | A certified type-preserving compiler from lambda calculus to assembly language[END_REF][START_REF] Wand | Compiler correctness for parallel languages[END_REF][START_REF] Liu | Confluence of processes and systems of objects[END_REF]. We highlight the work from Lochbihler, who added a new phase to the verified, machine-checked Jinja compiler [START_REF] Klein | A machine-checked model for a Java-like language, virtual machine, and compiler[END_REF] that proves that the translation from multi-threaded Java programs to Java bytecode is semantics preserving, using a delay bisimulation. In contrast, our work uses an on-paper proof using weak bisimilarity up-to expansion, proving that the compilation strategy preserves the semantics of the high-level language.

Ábrahám et al [START_REF] Ábrahám | Behavioral interface description of an object-oriented language with futures and promises[END_REF] present an extension of the Creol language with promises. The type system uses linear types to track the use of the write capability (fulfilment) of promises to ensure that they are fulfilled precisely once. In contrast to the present work, their type system is significantly more complex, and no forward operation is present. Curiously, Encore supports linear types, though lacks promises and hence does not use linear types to keep promises under control.

Niehren et al [START_REF] Niehren | A concurrent lambda calculus with futures[END_REF] present a lambda calculus extended with futures (which are really promises). Their calculus explores the expressiveness of programming with promises, by using them to express channels, semaphores, and ports. They also present a linear type system that ensures that promises are assigned only once.

Conclusion

One key difference between futures, futures with forward and promises is that the responsibility to fulfil a future cannot be delegated. The forward construct allows such delegation, although only of the implicit future receiving the result of some method call, while promises allow arbitrary delegation of responsibility. This paper presented a formal calculus capturing the forward construct, which retains the static fulfilment guarantees of futures. A translation of the source calculus into a target calculus based on promises was provided and proven to be semantics preserving. This translation models how forward is implemented in the Encore compiler. Microbenchmarks demonstrated that forward improves performance in terms of speed and memory overhead compared to two alternative implementations in the Encore language.

1

  def run(job: Job): Fut[int] 2 val worker = this.workers[++this.current % workers.size()] 3 return worker!start(job) 4 end

3

 3

1

  def run(job: Job): int 2 val worker = this.workers[++this.current % workers.size()] 3 val future = worker!start(job) 4 await(future) 5 return get(future) 6 end

e

  ::= v | e e | async e | e x e | if e then e else e | forward e | get e v ::= c | f | x | λx.e

Fig. 2 :

 2 Fig. 2: Configuration evaluation rules. Equivalence ≡ (omitted) captures the fact that configurations are a multiset of basic configurations.

Fig. 4 :

 4 Fig. 4: Configuration typing

Definition 2 .

 2 The function writers(config ) extracts the set of writers to futures in configuration config. writers((chain f g e)) = writers((task f e)) = {f } writers(config 1 config 2 ) = writers(config 1 ) ∪ writers(config 2 )

e

  ::= v | e e | Task(e, e) | stop | e; e | Prom | fulfil(e, e) | get e | Chain(e, e, e) | if e then e else e v ::= c | f | x | λx.e | ()

  | E; e | get E | fulfil(E, e) | fulfil(v, E) | Task(E, e) | Chain(e, E, e) | Chain(E, v, e) | Chain(v, v, E) | if E then e else e (RI-If-True) (task E[if true then e else e ]) -→ (task E[e]) (RI-ERROR)

(

  prm f ) (task E[Chain(f, Task(Prom, (λd .fulfil(d , e); stop)), λd .λx.fulfil(d , x); stop); stop]) -→ (prm f ) (prm g ) (task E[Chain(f, Task(g, (λd .fulfil(d , e); stop)), λd .λx.fulfil(d , x); stop); stop]) -→ (prm f ) (prm g ) (task E[Chain(f, g, λd .λx.fulfil(d , x); stop); stop]) (task fulfil(g, e); stop)

C

  e destiny Compilation Strategy C f destiny = f C x destiny = x C c destiny = c C λx.e destiny = λx.C e destiny C e1 e2 destiny = C e1 destiny C e2 destiny C get e destiny = get C e destiny C async e destiny = Task(Prom, (λdestiny .fulfil(destiny , C e destiny ); stop)) C forward e destiny = Chain(destiny, C e destiny, λdestiny .λx.fulfil(destiny , x); stop); stop C e x e destiny = Chain(Prom, C e destiny, (λdestiny .λx.fulfil(destiny , C e destiny ); stop)) C e destiny Optimised Compilation Strategy C forward(async(e)) destiny = Task(destiny, (λdestiny .fulfil(destiny , C e destiny ); stop)); stop C forward (e x e ) destiny = Chain(destiny, C e destiny, λdestiny .λx.fulfil(destiny , C e destiny ); stop); stop T config Configuration Compilation Strategy T (fut f ) = (prm f ) T (task f e) = (task fulfil(f, C e f ); stop)

Fig. 7 :

 7 Fig. 7: Compilation strategy of terms, configurations, types and typing rules

(

  prm f ) (task E[Chain(f, Task(Prom, (λd .fulfil(d , C e d ); stop)), λd .λx.fulfil(d , x); stop); stop])

Fig. 8 :

 8 Fig. 8: Elapsed time (left) and memory consumed (right) by the Broker microbenchmark (the lower the better).

The essential difference between get and await is that get blocks an actor, whereas await blocks only the current method invocation and frees up the actor.

A reviewer suggested that (fut f ), (fut f v), and (task f e) could be combined into a single configuration component. We have considered this conflation in the past. While it would reduce the complexity of the calculus, it would also make compilation into the target calculus and the proofs of correctness more complex.

→ * is the reflexive, transitive closure of the reduction relation →.(T-Constant) c is a constant of type τ Γ ρ c : τ (T-Future) f : Fut τ ∈ Γ Γ ρ f : Fut τ (T-Variable) x : τ ∈ Γ Γ ρ x : τ (T-Abstraction) Γ, x : τ • e : τ Γ ρ λx.e : τ → τ (T-Application) Γ ρ e 1 : τ → τ Γ ρ e 2 : τ Γ ρ e 1e 2 : τ (T-If-Then-Else) Γ ρ e : bool Γ ρ e : τ Γ ρ e : τ Γ ρ if e then e else e : τ (T-Get) Γ ρ e : Fut τ Γ ρ get e : τ (T-Async) Γ τ e : τ Γ ρ async e : Fut τ (T-Chain) Γ ρ e : Fut τ Γ, x : τ τ e : τ Γ ρ e x e : Fut τ (T-Forward) Γ ρ e : Fut ρ ρ = • Γ ρ forward e : τ

(TI-Promise) f : Prom τ ∈ Γ Γ f : Prom τ (TI-Variable) x : τ ∈ Γ Γ x : τ (TI-Unit) Γ () : unit (TI-Stop) Γ stop : τ (TI-Promise-New) Γ Prom : Prom τ (TI-If) Γ e : bool Γ e : τ Γ e : τ Γ if e then e else e : τ (TI-Statement) Γ e 1 : τ Γ e 2 : τ Γ e 1 ; e 2 : τ (TI-Abstraction) Γ, x : τ e : τ Γ λx.e : τ → τ (TI-App) Γ e : τ → τ Γ e : τ Γ e e : τ (TI-Fulfil) Γ e : Prom τ Γ e : τ Γ fulfil(e, e ) : unit (TI-Task) Γ e : Prom τ Γ e : Prom τ → τ Γ Task(e, e ) : Prom τ (TI-Get) Γ e : Prom τ Γ get e : τ (TI-Chain) Γ e : Prom τ Γ e : Prom τ Γ e : Prom τ → τ → τ Γ Chain(e, e , e ) : Prom τ (Prom)f ∈ dom(Γ ) Γ (prm f ) ok (F-Prom) f : Prom τ ∈ Γ Γ (prm f v) ok (Chain-Target) Γ f : Prom τ Γ e : τ → τ Γ (chain f e) ok(Task-Target) Γ e : τ Γ (task e) ok (Config-Target)

The underlying research was funded by the Swedish VR project: SCADA.

//github.com/parapluu/encore