Sung-Shik T Q Jongmans
email: [jongmans@cwi.nl

Farhad Arbab
email: farhad]@cwi.nl

Take Command of Your Constraints!

Keywords: {x1, x2} , dx 2 ≈ dx 1 {x1, } , d y ≈ dx 1 {, x2} , dx 2 ≈ dy {x1, x2, x3} , dx {A, } , d

Constraint automata (CA) are a coordination model based on finite automata on infinite words. Although originally introduced for compositional modeling of coordinators, an interesting new application of CA is actually implementing coordinators (i.e., compiling CA to executable code). Such an approach guarantees correctness-by-construction and can even yield code that outperforms hand-crafted code. The extent to which these two potential advantages arise depends on the smartness of CA-compilers and the existence of proofs of their correctness. We present and prove the correctness of a critical optimization for CAcompilers: a sound and complete translation from declarative constraints in transition labels to imperative commands in a sequential language. This optimization avoids expensive calls to a constraint solver at runtime, otherwise performed each time a transition fires, and thereby significantly improves the performance of generated coordination code.

Introduction

Context. A promising application domain for coordination languages is programming protocols among threads in multicore applications. One reason for this is a classical software engineering advantage: coordination languages typically provide high-level constructs and abstractions that more easily compose into correct-with respect to programmers' intentions-protocol specifications than do conventional lower-level synchronization mechanisms (e.g., locks or semaphores). However, not only do coordination languages simplify programming protocols, but their high-level constructs and abstractions also leave more room for compilers to perform optimizations that conventional language compilers cannot apply. Eventually, sufficiently smart compilers for coordination languages should be capable of generating code (e.g., in Java or in C) that can compete with carefully hand-crafted code. Preliminary evidence for feasibility of this goal appears elsewhere [START_REF] Jongmans | Automata-based Optimization of Interaction Protocols for Scalable Multicore Platforms[END_REF][START_REF] Jongmans | Reo: A Dataflow Inspired Language for Multicore[END_REF]. A crucial step toward adoption of coordination languages for multicore programming, then, is the development of such compilers.

To study the performance advantages of using coordination languages for multicore programming, in ongoing work, we are developing compilation technology for constraint automata (ca) [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]. Constraint automata are a general coordination model based on finite automata on infinite words. Every ca models the behavior of a single coordinator; a product operator on ca models the synchronous composition of such coordinators (useful to construct complex coordinators out of simpler ones). Structurally, a ca consists of a finite set of states,

λ1 λ2 λ3 λ4 λ1 : dm ≈ d B ∧ d C1 ≈ d B ∧ d C2 ≈ d B ∧ Mandarin(d C1 ) ∧ d D1 ≈ d C1 ∧ Spanish(d C2 ) ∧ d D2 ≈ d C2 λ2 : dm ≈ d B ∧ d C1 ≈ d B ∧ d C2 ≈ d B ∧ Mandarin(d C1 ) ∧ d D1 ≈ d C1 ∧ ¬Spanish(d C2 ) λ3 : dm ≈ d B ∧ d C1 ≈ d B ∧ d C2 ≈ d B ∧ ¬Mandarin(d C1 ) ∧ Spanish(d C2 ) ∧ d D2 ≈ d C2 λ4 : dm ≈ d B ∧ d C1 ≈ d B ∧ d C2 ≈ d B ∧ ¬Mandarin(d C1 ) ∧ ¬Spanish(d C2 )
Example Languages2

(b) Concrete/instantiated composites a finite set of transitions, a set of directed ports, and a set of local memory cells. Ports represent the boundary/interface between a coordinator and its coordinated agents (e.g., computation threads). Such agents can perform blocking i/o-operations on ports: a coordinator's input ports admit put operations, while its output ports admit get operations. Memory cells represent internal buffers in which a coordinator can temporarily store data items. Different from classical automata, transition labels of ca consist of two elements: a set of ports, called a synchronization constraint, and a logical formula over ports and memory cells, called a data constraint. A synchronization constraint specifies which ports need an i/o-operation for its transition to fire (i.e., those ports synchronize in that transition and their pending i/o-operations complete), while a data constraint specifies which particular data items those i/o-operations may involve. Figure 1 already shows some examples; details follow shortly. Essentially, a ca constrains when i/o-operations may complete on which ports. As such, ca quite literally materialize Wegner's definition of coordination as "constrained interaction" [START_REF] Wegner | Coordination as Constrained Interaction (Extended Abstract)[END_REF]. Given a library of "small" ca, each of which models a primitive coordinator with its own local behavior, programmers can compositionally construct "big" ca, each of which models a composite coordinator with arbitrarily complex global behavior, fully tailored to the needs of these programmers and their programs. Our current ca-compilers can subsequently generate Java/C code. Afterward, these compilers either automatically blend their generated code into programs' computation code or provide programmers the opportunity to do this manually. At run-time, the code generated for a big ca (i.e., a composite co- ordinator) executes a state machine that simulates that ca, repeatedly firing transitions as computation threads perform i/o-operations. Straightforward as this may seem, one needs to overcome a number of serious issues before this approach can yield practically useful code. Most significantly, these issues include exponential explosion of the number of states or transitions of ca, and oversequentialization or overparallelization of generated code. We have already reported our work on these issues along with promising results elsewhere [START_REF] Jongmans | Global Consensus through Local Synchronization[END_REF][START_REF] Jongmans | Toward Sequentializing Overparallelized Protocol Code[END_REF][START_REF] Jongmans | Automata-based Optimization of Interaction Protocols for Scalable Multicore Platforms[END_REF][START_REF] Jongmans | Partially-Distributed Coordination with Reo[END_REF]. Instead of programming with ca directly, one can adopt a more programmerfriendly syntax for which ca serve as semantics. In our work, for instance, we adopted the syntax of Reo [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Arbab | Puff, The Magic Protocol[END_REF], a graphical calculus of channels. Figure 2 already shows some examples; details follow shortly. (Other ca syntaxes beside Reo exist though [START_REF] Arbab | Towards Using Reo for Compliance-Aware Business Process Modeling[END_REF][START_REF] Changizi | A Unified Toolset for Business Process Model Formalization[END_REF][START_REF] Meng | Synthesis of Reo circuits from scenario-based interaction specifications[END_REF][START_REF] Bliudze | Causal semantics for the algebra of connectors[END_REF], which may be at least as programmer-friendly.) Problem. To fire a transition at run-time, code generated for a ca must evaluate the data constraint of that transition: it must ensure that the data involved in blocking i/o-operations pending on the transition's ports satisfy that constraint.

A straightforward evaluation of data constraints requires expensive calls to a constraint solver. Such calls cause high run-time overhead. In particular, because transitions fire sequentially, avoiding constraint solving to reduce this sequential bottleneck is crucial in getting good performance for the whole program.

Contribution & organization. In this paper, we introduce a technique for statically translating a data constraint, off-line at compile-time, into a data command : an imperative implementation (in a sequential language with assignment and guarded failure) of a data constraint that avoids expensive calls to a constraint solver at run-time. As with our previous optimization techniques [START_REF] Jongmans | Global Consensus through Local Synchronization[END_REF][START_REF] Jongmans | Automata-based Optimization of Interaction Protocols for Scalable Multicore Platforms[END_REF][START_REF] Jongmans | Partially-Distributed Coordination with Reo[END_REF], we prove that the translation in this paper is sound and complete. Such correctness proofs are important, because they ensure that our compilation approach guarantees correctness-by-construction (e.g., model-checking results obtained for pre-optimized ca also hold for their generated, optimized implementations). We also give preliminary performance results to show our optimization's potential.

In Section 2, we discuss data constraints and ca. In Sections 3 and 4, we discuss our translation algorithm. In Section 5, we give preliminary performance results. Section 6 concludes this paper. Some relatively lengthy formal definitions and detailed proofs of Theorems 1 and 2 appear in a technical report [START_REF] Jongmans | Take Command of Your Constraints![END_REF].

2 Preliminaries: Data Constraints, Constraint Automata Data constraints. Let D denote the finite set of all data items, typically ranged over by d. Let nil / ∈ D denote a special object for the empty data item. Let P denote the finite set of all places where data items can reside, typically ranged over by x or y; every place models either a port or a memory cells. We model atomic coordination steps-the letters in the alphabet of ca-with elements from the partial function space Distr = P D ∪ {nil}, called distributions, typically ranged over by δ. Informally, a distribution δ associates every place x involved in the step modeled by δ with the data item δ(x) observable in x.

Let

F = {D k → D | k > 0} and R = {℘(D k ) | k > 0}
denote the sets of all data functions and data relations of finite arity. Let Data, Fun, and Rel denote the sets of all data item symbols, data function symbols and data relation symbols, typically ranged over by d, f , and R. Let arity : Fun∪Rel → N + denote a function that associates every data function/relation symbol with its positive arity. Let I : Data ∪ Fun ∪ Rel → D ∪ F ∪ R denote a bijection that associates every data item/function/relation symbol with its interpretation. A data term is a word t generated by the following grammar:

t ::= d x | nil | d | f (t 1 , . . . , t k ) if arity(f ) = k
Let Term denote the set of all data terms. Let eval : Distr × Term → D ∪ {nil} denote a function that evaluates every data term t to a data item eval δ (t) under distribution δ. For instance, eval δ (d x ) = δ(x)-if δ is defined for x-and eval δ (d) = I(d). If a data term t contains nil or d x for some x / ∈ Dom(δ), we have eval δ (t) = nil. This ensures that eval is a total function, even though the deltas in Distr are partial functions. See also [START_REF] Jongmans | Take Command of Your Constraints![END_REF]Definition 7]. We call a term of the form d x a free variable. Intuitively, d x represents the data item residing in place x. Let Free : Term → ℘(Term) denote a function that maps every data term t to its set of free variables.

A data constraint is a word φ generated by the following grammar:

a ::= ⊥ | | t ≈ t | t ≈ nil | R(t 1 , . . . , t k ) if arity(R) = k φ ::= a | ¬φ | φ ∨ φ | φ ∧ φ
Let DC denote the set of all data constraints. We often call t 1 ≈ t 2 atoms equalities. We define the semantics of data constraints over distributions. Let |= dc ⊆ Distr × DC denote the satisfaction relation on data constraints. Its definition is standard for ⊥ (contradiction), (tautology), ¬ (negation), ∨ (disjunction), and ∧ (conjunction). For other atoms, we have the following:

δ |= dc t 1 ≈ t 2 iff eval δ (t 1 ) = eval δ (t 2 ) = nil δ |= dc t ≈ nil iff eval δ (t) = nil (i.e., notation for δ |= dc t ≈ t) δ |= dc R(t 1 , . . . , t k ) iff I(R)(eval δ (t 1 ) , . . . , eval δ (t k ))
In the second rule, if a t i evaluates to nil, the right-hand side is undefined-hence false-because the domain of data relation I(R) excludes nil. If δ |= dc φ, we call δ a solution for φ. Let • : DC → ℘(Distr) denote a function that associates every data constraint φ with its meaning φ = {δ | δ |= dc φ}. We write φ ⇒ φ iff φ ⊆ φ . We also extend function Free from data terms to data constraints.

Constraint automata. A constraint automaton (ca) is a tuple (Q , X , Y , -→ , ı) with Q a set of states, X ⊆ P a set of ports, Y ⊆ P a set of memory cells, -→ ⊆ Q × (℘(X ) × DC) × Q a transition
relation labeled with pairs (X , φ), and ı ∈ Q an initial state. For every label (X , φ), no ports outside X may occur in φ. Set X consists of three disjoint subsets of input ports X in , internal ports X int , and output ports X out . We call a ca for which X int = ∅ a primitive; otherwise, we call it a composite.

Although generally important, we skip the definition of the product operator on ca, because it does not matter in this paper. Every ca accepts infinite sequences of distributions [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]: (Q , X , Y , -→ , ı) accepts δ 0 δ 1 • • • if an infinite sequence of states q 0 q 1 • • • exists such that q 0 = ı and for all i ≥ 0, a transition (q i , (X , φ) , q i+1 ) exists such that Dom(δ i ) = X and δ i |= dc φ.

Without loss of generality, we assume that all data constraints occur in disjunctive normal form. Moreover, because replacing a transition (q , (X , φ 1 ∨φ 2 ) , q ) with two transitions (q , (X , φ 1 ) , q ) and (q , (X , φ 2 ) , q ) preserves behavioral congruence on ca [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF], without loss of generality, we assume that the data constraint in every label is a conjunction of literals, typically ranged over by .

Figure 1a shows example primitives; Figure 2a shows their Reo syntax. Sync models a synchronous channel from an input x 1 to an output x 2 . Fifo models an asynchronous channel with a 1-capacity buffer y from x 1 to x 2 . Repl models a coordinator that, in each of its atomic coordination steps, replicates the data item on x 1 to both x 2 and x 3 . BinOp models a coordinator that, in each of its atomic coordination steps, applies operation f to the data items on x 1 and x 2 and passes the result to x 3 . Filter models a lossy synchronous channel from x 1 to x 2 ; data items pass this channel only if they satisfy predicate R.

Figure 1b shows example composites; Figure 2b shows their Reo syntax. Example-our running example in this paper-consists of instantiated primitives BinOp add (A, B; ; C), Repl(C; ; D, E), and Filter Odd (D; ; F), where add and Odd have the obvious interpretation. In each of its atomic coordination steps, if the sum of the data items (supposedly integers) on its inputs A and B is odd, Example passes this sum to its outputs E and F. Otherwise, if the sum is even, Example passes this value only to E. Figure 2b shows that Example constitutes Fibonacci. Fibonacci coordinates two consumers by generating the Fibonacci sequence. Whenever Fibonacci generates an even number, it passes that number to only one consumer; whenever it generates an odd number, it passes that number to both consumers. Finally, Languages2 consists of instantiated primitives Fifo[m](A; ; B), Repl(B; ; C1, C2), Filter Mandarin (C1; ; D1), and Filter English (C2; ; D2). Languages2 coordinates a producer and two consumers. If the producer puts a Mandarin (resp. English) data item on input A, Languages2 asynchronously passes this data item only to the consumer on output D1 (resp. D2). Languages2 easily generalizes to Languagesi, for i different languages; we do so in Section 5.

From Data Constraints to Data Commands

At run-time, compiler-generated code executes in one or more ca-threads, each of which runs a state machine that simulates a ca. (We addressed the challenge of deciding the number of ca-threads elsewhere [START_REF] Jongmans | Global Consensus through Local Synchronization[END_REF][START_REF] Jongmans | Toward Sequentializing Overparallelized Protocol Code[END_REF][START_REF] Jongmans | Partially-Distributed Coordination with Reo[END_REF].) The context of a ca-thread is the collection of put/get operations on implementations of its input/output ports, performed by computation threads. Every time the context of a ca-thread changes, that ca-thread examines whether this change enables a transition in its current state q: for each transition (q , (X , φ) , q ), it checks whether every port x ∈ X has a pending i/o-operation and if so, whether the data items involved in the pending put operations and the current content of memory cells can constitute a solution for φ. For the latter, the ca-thread calls a constraint solver, which searches for a distribution δ such that δ |= dc φ and δ init ⊆ δ, where:

δ init = {x → d | the put pending on input port x involves data item d} ∪ {y → d | memory cell y contains data item d} (1)
Constraint solving over a finite discrete domain (e.g., D) is np-complete [START_REF] Russell | Artificial Intelligence. 2nd edn[END_REF]. Despite carefully and cleverly optimized backtracking searches, using generalpurpose constraint solving techniques for solving a data constraint φ inflicts not only overhead proportional to φ's size but also a constant overhead for preparing, making, and processing the result of the call itself. Although we generally cannot escape using conventional constraint solving techniques, a practically relevant class of data constraints exists for which we can: the data constraints of many ca in practice are in fact declarative specifications of sequences of imperative instructions (including those in Figure 1). In this section, we therefore develop a technique for statically translating such a data constraint φ, off-line at compile-time, into a data command : a little imperative program that computes a distribution δ such that δ |= dc φ and δ init ⊆ δ, without conventional constraint solving hassle. Essentially, we formalize and automate what a programmer would do if he/she were to write an imperative implementation of a declarative specification expressed as a data constraint. By the end of Section 4, we make the class of data constraints supported by our translation precise.

Data Commands

A data command is a word P generated by the following grammar:

P ::= skip | x := t | if φ -> P fi | P ; P
(We often write "value of x" instead of "the data item assigned to x".)

We adopt the following operational semantics of Apt et al. [START_REF] Apt | Verification of Sequential and Concurrent Programs[END_REF]. True to the idea that data commands compute solutions for data constraints, the state that a data command executes in is either a function from places to data items-a distribution!-or the distinguished symbol fail, which represents abnormal termination. A configuration is a pair of a data command and a state to execute that data command in. Let ε denote the empty data command, and equate ε ; P with P . Let δ[x := eval δ (t)] denote an update of δ as usual. The following rules define the transition relation on configurations, denoted by =⇒.

(skip , δ) =⇒ (ε , δ) (x := t , δ) =⇒ (ε , δ[x := eval δ (t)]) δ |= dc φ (if φ -> P fi , δ) =⇒ (P , δ) δ |= dc φ (if φ -> P fi , δ) =⇒ (ε , fail)
(P , δ) =⇒ (P , δ ) (P ; P , δ) =⇒ (P ; P , δ ) Note that if φ -> P fi commands are failure statements rather than conditional statements: if the current state violates the guard φ, execution abnormally terminates. The partial correctness semantics, which ignores abnormal termination, of a data command P in a state δ is the set of final states M(P , {δ}) = {δ | (P , δ) =⇒ * (ε , δ )}; its total correctness semantics is the set consisting of fail or its final states M tot (P , {δ}) = {fail | (P , {δ}) =⇒ * (ε , fail)} ∪ M(P , {δ}).

Shortly, to prove the correctness of our translation from data constraints to data commands, we use Hoare logic [START_REF] Hoare | An Axiomatic Basis for Computer Programming[END_REF], where triples {φ} P {φ } play a central role. In such triples, φ characterizes the set of input states, P denotes the data command to execute in those states, and φ characterizes the set of output states. A triple {φ} P {φ } holds in the sense of partial (resp. total) correctness, if M(P , φ ) ⊆ φ (resp. M tot (P , φ ) ⊆ φ ). To prove properties of data commands, we use the following sound proof systems for partial (resp. total) correctness, represented by (resp. tot ) and adopted from Apt et al. [START_REF] Apt | Verification of Sequential and Concurrent Programs[END_REF]. The first four rules apply not only to but also to tot . We use to prove the soundness of our upcoming translation; we use tot to prove its completeness.

Precedence

Recall the following typical data constraint over ports A, B, C, D, and E, where A and B are inputs, from Example in Figure 1b (its lower transition):

φ = d C ≈ add(d A , d B ) ∧ d D ≈ d C ∧ d E ≈ d C ∧ ¬Odd(d D ) (2)
To translate data constraints to data commands, the idea is to enforce equalities, many of which occur in practice, with assignments and to check all remaining literals with failure statements. In the case of φ, for instance, we first assign the data items involved in their pending put operations to A and B, whose symbols are denoted by I -1 (δ init (A)) and I -1 (δ init (B)), with δ init as defined in (1), page 6. Next, we assign the evaluation of add(d A , d B ) to C. The order in which we subsequently assign the value of C to D and E does not matter. After the assignment to D, we check ¬Odd(d D ) with a failure statement. The following data command corresponds to one possible order of the last three steps.

P = A := I -1 (δ init (A)) ; B := I -1 (δ init (B)) ; C := add(d A , d B ) ; D := d C ; if ¬Odd(d D ) -> skip fi ; E := d C
If execution of P in an empty initial state successfully terminates, the resulting final state δ should satisfy φ (soundness). Moreover, if a δ exists such that δ |= dc φ and δ init ⊆ δ , execution of P should successfully terminate (completeness). Soundness and completeness crucially depend on the order in which assignments and failure statements occur in P . For instance, changing the order of D := d C and if ¬Odd(d D ) -> skip fi yields a data command whose execution always fails (because D does not have a value yet on evaluating the guard of the failure statement). Such a data command is trivially sound but incomplete. Another complication is that not every equality can become an assignment. In a first class of cases, no operand matches d x . An example is add(d A , d B ) ≈ mult(d A , d B ): this equality should become a failure statement, because neither of its two operands can be assigned to the other. In a second class of cases, multiple equality literals have an operand that matches d

x . An example is C ≈ add(d A , d B ) ∧ C ≈ mult(d A , d B )
: only one of these equalities should become an assignment, while the other should become a failure statement, to avoid conflicting assignments to C.

To deal with these complications, we define a precedence relation on literals that formalizes their dependencies. Recall that the data constraint in every transition label (X , φ) is a conjunction of literals. Let L φ denote the set of literals in φ, and let X in ⊆ X denote the set of input places (i.e., input ports and memory cells) involved in the transition. From L φ and X in , we construct a set of literals L to account for (i) symmetry of ≈ and (ii) the initial values of input places.

L = L φ ∪ {t 2 ≈ t 1 | t 1 ≈ t 2 ∈ L φ } ∪ {d x ≈ I -1 (δ init (x)) | x ∈ X in } (3)
Obviously, δ |= dc L implies δ |= dc φ for all δ (i.e., extending L φ to L is sound). Now, let ≺ L denote the precedence relation on L defined by the following rules: Informally, d x ≈ t ≺ L means that assignment x := t must precede (i.e., depends on x). Note also that the first rule deals with the first class of equalities-that-cannot-become-assignments; shortly, we comment on the second class.

d x ≈ t , ∈ L and d x ∈ Free( ) d x ≈ t ≺ L 1 ≺ L 2 ≺ L 3 and 2 / ∈ { 1 , 3 } 1 ≺ L 3 (4) d A ≈ I -1 (δinit(A)) d B ≈ I -1 (δinit(B)) d C ≈ add(d A , d B ) d D ≈ d C d E ≈ d C ¬Odd(d D ) d C ≈ d D d C ≈ d E
For the sake of argument-generally, this is not the case-suppose that ≺ L is a strict partial order on L. In that case, we can linearize ≺ L to a total order < on L (i.e., embedding ≺ L into < such that ≺ L ⊆ <) with a topological sort on the digraph (L , ≺ L ) [START_REF] Kahn | Topological Sorting in Large Networks[END_REF][START_REF] Knuth | Fundamental Algorithms[END_REF]. Intuitively, such a linearization gives us an order in which we can translate literals in L to data commands in a sound and complete way. In Section 3.3, we give an algorithm for doing so and indeed prove its correctness. Problematically, however, ≺ L is generally not a strict partial order on L: it is generally neither asymmetric nor irreflexive (i.e., graph-theoretically, it contains cycles). For instance, Figure 3 shows a fragment of the digraph (L , ≺ L ) for φ in (2), page 8, which contains cycles. For now, we defer this issue to Section 4, because it forms a concern orthogonal to our translation algorithm and its correctness. Until then, we simply assume the existence of a procedure for extracting a strict partial order from ≺ L , represented by bold arcs in Figure 3.

Henceforth, we assume that every d xi ≈ t i literal precedes all differently shaped literals in a linearization of ≺ L . Although this assumption is conceptually unnecessary, it simplifies some of our notation and proofs. Formally, we can enforce it by adding a third rule to the definition of ≺ L :

d x ≈ t , ∈ L and = d x ≈ t for all x , t d x ≈ t ≺ L (5)
Proposition 1. The rule in (5) introduces no cycles.

(A proof appears in the technical report [START_REF] Jongmans | Take Command of Your Constraints![END_REF].)

Algorithm

We start by stating the precondition of our translation algorithm. Suppose that L as defined in (3), page 8, contains n d x ≈ t literals and m differently shaped literals. Let ≺ L denote a strict partial order on L such that for every d x ≈ t ∈ L and for every d y ∈ Free(t), a d y ≈ t literal precedes d x ≈ t according to ≺ L .

Then, let

1 < • • • < n < n+1 < • • • < n+m denote a linearization of ≺ L , where i = d xi ≈ t i for all 1 ≤ i ≤ n.
The three rules of ≺ L in Section 3.2 induce precedence relations for which all previous conditions hold, except that ≺ L does not necessarily denote a strict partial order; we address this issue in the next section. The previous conditions aside, we also assume {d x1 , . . . , 10].

d xn } = { Free( i ) | 1 ≤ i ≤ n + m}.
P ← skip i ← 1 while i ≤ n do if dx i ∈ {dx j | 1 ≤ j < i} then P ← P ; if dx i ≈ ti -> skip fi else P ← P ; xi := ti i ← i + 1 while i ≤ n + m do P ← P ; if i -> skip fi i ← i + 1
Fig. 4: Algorithm to translate data constraints to data commands Figure 4 shows our algorithm. It first loops over the first n (according to <) d x ≈ t literals. If an assignment for x already exists in data command P , the algorithm translates d x ≈ t to a failure statement; if not, it translates d x ≈ t to an assignment. This approach resolves issues with the second class of equalities-that-cannot-become-assignments. After the first loop, the algorithm uses a second loop to translate the remaining m differently shaped literals to failure statements. The algorithm runs in time linear in n + m, and it clearly terminates.

The desired postcondition of the algorithm consists of its soundness and completeness. We define soundness as { } P { 1 ∧ • • • ∧ n+m }: after running the algorithm, execution of data command P yields a state that satisfies all literals in L on successful termination. We define completeness as δ |= dc 1 ∧ • • •∧ n+m implies tot { } P { } for all δ : after running the algorithm, if a distribution δ exists that satisfies all literals in L, data command P successfully terminated. Although soundness subsequently guarantees that the final state δ satisfies all literals in L, generally, δ = δ . We use a different proof system for soundness (partial correctness, ) than for completeness (total correctness, tot ).

Theorem 1 ([14, Theorem 3]). The algorithm is sound and complete.

(A proof appears in the technical report [START_REF] Jongmans | Take Command of Your Constraints![END_REF].)

Handling Cycles

Our algorithm assumes that a precedence relation ≺ L as defined in Section 3.2 is a strict partial order. However, this is generally not the case. In this section, we describe a procedure for extracting a strict partial order from ≺ L without losing essential dependencies. We start by adding a distinguished symbol to the domain of ≺ L , and we extend the definition of ≺ L with the following rules:

d A ≈ I -1 (δinit(A)) d B ≈ I -1 (δinit(B)) d C ≈ add(d A , d B ) d D ≈ d C d E ≈ d C ¬Odd(d D ) d C ≈ d D d C ≈ d E
∈ L and Free( ) = ∅ ≺ L d x ≈ t ∈ L and Free(t) = ∅ ≺ L d x ≈ t (6)
These rules state that literals without free variables (e.g., d x ≈ I -1 (δ init (x))) do not depend on other literals. Now, ≺ L is a strict partial order if the digraph (L ∪ { } , ≺ L ) is a -arborescence: a digraph consisting of n-1 arcs such that each of its n vertices is reachable from [START_REF] Korte | Combinatorial Optimization: Theory and Algorithms[END_REF]. Equivalently, in a -arborescence, has no incoming arcs, every other vertex has exactly one incoming arc, and the arcs form no cycles [START_REF] Korte | Combinatorial Optimization: Theory and Algorithms[END_REF]. The first formulation is perhaps most intuitive here: every path from to some literal represents an order in which our algorithm should translate the literals on that path to ensure the correctness of the translation of . The second formulation simplifies observing that arborescences correspond to strict partial orders (by their cycle-freeness).

A naive approach to extract a strict partial order from ≺ L is to compute a -arborescence of the digraph (L ∪ { } , ≺ L ). Unfortunately, however, this approach generally fails for d x ≈ t literals where t has more than one free variable. For instance, by definition, every arborescence of the digraph in Figure 3 has only one incoming arc for d C ≈ add(d A , d B ), even though assignments to both A and B must precede an assignment to C. Because these dependencies exist as two separate arcs, no arborescence of a digraph can capture them. To solve this, we should somehow represent the dependencies of d C ≈ add(d A , d B ) with a single incoming arc. We can do so by allowing arcs to have multiple tails (i.e., one for every free variable). In that case, we can replace the two separate incoming arcs of d C ≈ add(d A , d B ) with a single two-tailed incoming arc as in Figure 5. The two tails make explicit that to evaluate an add-term, we need values for both its arguments: multiple tails represent a conjunction of dependencies of a literal.

By replacing single-tail-single-head arcs with multiple-tails-single-head arcs, we effectively transform the digraphs considered so far into b-graphs, a special kind of hypergraph with only b-arcs (i.e., backward hyperarcs, i.e., hyperarcs with exactly one head) [START_REF] Gallo | Directed hypergraphs and applications[END_REF]. Deriving a b-graph over literals from a precedence relation as defined in Section 3.2 is generally impossible though: their richer structure makes b-graphs more expressive-they give more information-than digraphs. In contrast, one can easily transform a b-graph to a precedence relation by splitting b-arcs into single-tailed arcs in the obvious way. Deriving precedence relations from more expressive b-graphs is therefore a correct way of obtaining strict partial orders that satisfy the precondition of our algorithm. Doing so just eliminates information that this algorithm does not care about anyway.

Thus, we propose the following. Instead of formalizing dependencies among literals in a set L ∪ { } directly as a precedence relation, we first formalize those dependencies as a b-graph. If the resulting b-graph is a -arborescence, we can directly extract a precedence relation ≺ L . Otherwise, we compute a -arborescence of the resulting b-graph and extract a precedence relation ≺ L afterward. Either way, because ≺ L is extracted from a -arborescence, it is a strict partial order whose linearization satisfies the precondition of our algorithm.

Let L denote a set of b-arcs on L ∪ { } defined by the following rules, plus the straightforward b-arcs adaptation of the rules in [START_REF] Jongmans | Toward Sequentializing Overparallelized Protocol Code[END_REF], page 11:

∈ L and Free( ) = {d x1 , . . . , d x k } and d x1 ≈ t 1 , . . . , d x k ≈ t k ∈ L {d x1 ≈ t 1 , . . . , d x k ≈ t k } L d x ≈ t ∈ L and Free(t) = {d x1 , . . . , d x k } and d x1 ≈ t 1 , . . . , d x k ≈ t k ∈ L {d x1 ≈ t 1 , . . . , d x k ≈ t k } L d x ≈ t (7)
The first rule generalizes the first rule in (4), page 8, by joining sets of dependencies of a literal in a single b-arc. The second rule states that d x ≈ t literals do not necessarily depend on d x (as implied by the first rule) but only on the free variables in t: intuitively, a value for x can be derived from values of the free variables in t (cf. assignments). Note that literals can have multiple incoming b-arcs. Such multiple incoming b-arcs represent a disjunction of conjunctions of dependencies. Importantly, as long as all dependencies represented by one incoming b-arc are satisfied, the other incoming b-arcs do not matter. An arborescence, which contains one incoming b-arc for every literal, therefore preserves enough dependencies. Shortly, Theorem 2 makes this more precise. Figure 5 In total, thus, we generated twenty coordinators in Java. We ran each of those implementations ten times on a quadcore machine at 2.4 ghz (no Hyper-Threading; no Turbo Boost) and averaged our measurements. In every run, we warmed up the Jvm for thirty seconds before starting to measure the number of coordination steps that an implementation could finish in the subsequent four minutes. Figure 6 shows our results. The command-based implementations outperform their constraint-based versions in all cases. The Languagei coordinators furthermore show that the speed-up achieved by their command-based implementations increases as i increases. This may suggest that our optimization becomes relatively more effective as the size/complexity of a coordinator increases, as also witnessed by Fibonacci. Figure 6 shows first evidence for the effectiveness of our translation in practice, although further study is necessary.

Discussion

In constraint programming, it is well-known that "if domain specific methods are available they should be applied instead [sic] of the general methods" [24, page 2]. The work presented in this paper takes this guideline to an extreme: essentially, every data command generated for a data constraint φ by our translation algorithm is a little constraint solver capable of solving only φ, with good performance. This good performance comes from the fact that the order of performing assignments and failure statements has already been determined at compile-time.

Moreover, this precomputed order guarantees that backtracking is unnecessary: the data constraint for φ finds a solution if one exists without search (i.e., Theorem 1). In contrast, general constraint solvers need to do this work, which our approach does at compile-time, as part of the solving process at run-time.

Execution of data commands bears similarities with constraint propagation techniques [START_REF] Apt | Principles of Constraint Programming[END_REF], in particular with forward checking [START_REF] Bessière | On forward checking for nonbinary constraint satisfaction[END_REF][START_REF] Mcgregor | Relational consistency algorithms and their application in finding subgraph and graph isomorphism[END_REF]. Generally, in constraint propagation, the idea is to reduce the search space of a given constraint satisfaction problem (csp) by transforming it into an equivalent "simpler" csp, where variables have smaller domains, or where constraints refer to fewer variables. With forward checking, whenever a variable x gets a value v, a constraint solver removes values from the domains of all subsequent variables that, together with v, violate a constraint. In the case of an equality x = y, for instance, forward checking reduces the domain of y to the singleton {v} after an assignment of v to x. That same property of equality is implicitly used in executing our data commands (i.e., instead of representing the domain of a variable and the reduction of this domain to a singleton explicitly, we directly make an assignment).

Our translation from data constraints to data commands may also remind one of classical Gaussian eliminination for solving systems of linear equations over the reals [START_REF] Apt | Principles of Constraint Programming[END_REF]: there too, variables are ordered and values/expressions for some variables are substituted into other expressions. The difference is that we have functions, relations, and our data domain may include other data types, which makes solving data constraints directly via Gaussian elimination at least not obvious. However, Gaussian elimination does seem useful as a preprocessing step for translating certain data constraints to data commands that our current algorithm does not support. Future work should clarify this possibility.

Clarke et al. worked on purely constraint-based implementations of coordinators [START_REF] Clarke | Channel-based coordination via constraint satisfaction[END_REF]. Essentially, they specify not only the transition labels of a ca as boolean constraints but also its state space and transition relation. In recent work, Proença and Clarke developed a variant of compile-time predicate abstraction to improve performance [START_REF] Proença | Data Abstraction in Coordination Constraints[END_REF]. They used this technique also to allow a form of interaction between the constraint solver and external components during constraint solving [START_REF] Proença | Interactive Interaction Constraints[END_REF]. The work of Proença and Clarke resembles ours in the sense that we all try to "simplify" constraints at compile-time. Main differences are that (i) we fully avoid constraint solving and (ii) we consider a richer language of data constraints. For instance, Proença and Clarke have only unary functions in their language, which would have cleared our need for b-graphs.

Fig. 1 :

 1 Fig. 1: Example ca. Semicolons separate input/internal/output ports.

Fig. 2 :

 2 Fig. 2: Reo syntax for the ca in Figure 1. White vertices represent input/output ports; black vertices represent internal ports.

  {φ} skip {φ} {φ[d x := t]} x := t {φ} {φ } P {φ } and φ ⇒ φ and φ ⇒ φ {φ} P {φ } {φ} P {φ } and {φ } P {φ } {φ} P ; P {φ } {φ ∧ φ g } P {φ } {φ} if φ g -> P fi {φ } φ ⇒ φ g and tot {φ} P {φ } tot {φ} if φ g -> P fi {φ }

Fig. 3 :

 3 Fig. 3: Fragment of a digraph for an example precedence relation ≺ L (e.g., without loops and without add(d A , d B ) ≈ d C , for simplicity). An arc ( , ) corresponds to ≺ L . Bold arcs represent a strict partial order extracted from ≺ L .

Fig. 5 :

 5 Fig. 5: Fragment of the b-graph corresponding to the digraph in Figure 3 (e.g., without looping b-arcs and without add(d A , d B ) ≈ d C , for simplicity). Bold barcs represent an arborescence.

  shows a fragment of the b-graph for data constraint φ in (2), page 8. One can straightforwardly compute an arborescence of a b-graph (L ∪ { } , L ) with a graph exploration algorithm reminiscent of breadth-first search. Let arb L ⊆ L denote the aborescence under computation, and let L done ⊆ L denote the set of vertices (i.e., literals in L) that have already been explored; initially, arb L = ∅ and L done = { }. Now, given some L done , compute a set of vertices L next that are connected only to vertices in L done by a b-arc in L . Then, for every vertex in L next , add an incoming b-arc to arb L . 1 Afterward, add L next to 1 If a vertex in Lnext has multiple incoming b-arcs, the choice among them matters not: the choice is local, because every b-arc has only one head (i.e., adding anheaded b-arc to arb L cannot cause another vertex to get multiple incoming b-arcs, which would invalidate the arborescence

  This extra condition means that for every free variable d xi in every literal in L, a d xi ≈ t i literal exists in the linearization. If this condition fails, some places can get a value only through search-exactly what we try to avoid-and not through assignment. In such cases, the data constraint is underspecified, and our translation algorithm is fundamentally inapplicable. Finally, we trivially assume that nil does not occur syntactically in any literal. A formal definition of this precondition appears in the technical report[START_REF] Jongmans | Take Command of Your Constraints![END_REF] Figure

  ). General hypergraphs, whose hyperarcs can have multiple heads, violate this property (i.e., the choice of which hyperarc to add is global instead of local). Computing arborescences of such hypergraphs is np-complete[START_REF] Woeginger | The complexity of finding arborescences in hypergraphs[END_REF], whereas one can compute aborescences of b-graphs in linear time. " shows the ratio of the second over the first. generate both constraint-based coordination code (i.e., generated without our translation) and command-based coordination code (i.e., generated with our translation) for ten coordinators modeled as ca: three elementary primitives from Figures1a and 2a(to see how our optimization affects such basic cases) and seven more complex composites, including those in Figures1b and 2b. See Section 2 for a discussion of these coordinators' behavior. The constraint-based implementations use a custom constraint solver with constraint propagation[START_REF] Apt | Principles of Constraint Programming[END_REF], tailored to our setting of data constraints. The data commands in the generated command-based implementations are imperative Java code, very similar to what programmers would hand-craft (modulo style).

		Constr.	Comm.	×		Constr.	Comm.	×
	Sync	33119333 39800986	1.20	Language2	17278247 24646838	1.43
	Fifo	33050122 41398084	1.25	Language4	4423326 11512506	2.60
	Replicator 17961129 21803913	1.21	Language6	1062306	5294838	4.98
	Example	10573857 12687767	1.20	Language8	194374	1746440	8.98
	Fibonacci	1818671 88947751 48.91	Language10	25649	362050 14.12
	Fig. 6: Preliminary performance results for ten coordinators. Column "Constr."
	shows results for constraint-based implementations (in number of coordination
	steps completed in four minutes); column "Comm." shows restults for command-
	based implementations; column "×

L done . Repeat this process until L next becomes empty. Once that happens, either arb L contains an arborescence (if L done = L) or no arborescence exists. This computation runs in linear time, in the size of the b-graph. See also Footnote 1. Given arb L , the following rules yield a cycle-free precedence relation on L ∪ { }:

Theorem 2 ([14, Theorem 4]). ≺ L as defined by the rules in (5) [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF], pages 9 and 13, is a strict partial order and a large enough subset of ≺ L as defined by the rules in (4)(5)(6), pages 8, 9, and 11, to satisfy the precondition of our translation algorithm in Section 3.3.

(A proof appears in the technical report [START_REF] Jongmans | Take Command of Your Constraints![END_REF].) For instance, the bold arcs in Figure 3 represent the precedence relation for the arborescence in Figure 5.

If a -arborescence of (L ∪ { } , L ) does not exist, every |L|-cardinality subset of L has at least one vertex that is unreachable from . In that case, by the rules in [START_REF] Jongmans | Toward Sequentializing Overparallelized Protocol Code[END_REF], page 11, depends on at least one free variable (otherwise, { } L ). Because no b-graph equivalent of a path [START_REF] Ausiello | Directed Hypergraphs: Problems, Algorithmic Results, and a Novel Decremental Approach[END_REF] exists from to , the other literals in L fail to resolve at least one of 's dependencies. This occurs, for instance, when depends on d y , while L contains no d y ≈ t literal. Another example is a recursive literal d x ≈ t with d x ∈ Free(t): unless another literal d x ≈ t with t = t exists, all its incoming b-arcs contain loops to itself, meaning that no arborescence exists. In practice, such cases inherently require constraint solving techniques to find a value for d x . Nonexistence of a -arborescence thus signals a fundamental boundary to the applicability of our translation algorithm (although more advanced techniques of translating some parts of a data constraint to a data command and leaving other parts to a constraint solver are imaginable and left for future work). Thus, the set of data constraints to which our translation algorithm is applicable contains exactly those (i) whose b-graph has a -arborescence, which guarantees linearizability of the induced precedence, and (ii) that satisfy also the rest of the precondition of our algorithm in Section 3.3.

Preliminary Performance Results

In the work that we presented in this paper, we focused on the formal definition of our translation and its proof of correctness. A comprehensive quantitative evaluation remains future work. Indeed, constructing a set of representative examples, identifying independent variables that may influence the outcome (e.g., number of cores, memory architecture, etc.), setting up and performing the corresponding experiments, processing/analyzing the measurements, and eventually presenting the results is a whole other challenge. Still, presenting an optimization technique and not shedding any light on its performance may leave the reader with an unsatisfactory feeling. Therefore, in this section, we provide preliminary performance results to give a rough indication of our translation's merits.

We extended our most recent ca-to-Java compiler and used this compiler to


Marina Andrić

Rocco De Nicola

Alberto Lluch Lafuente

Replica-based High-Performance Tuple Space Computing

We present the tuple-based coordination language RepliKlaim, which enriches Klaim with primitives for replica-aware coordination. Our overall goal is to offer suitable solutions to the challenging problems of data distribution and locality in large-scale high performance computing. In particular, RepliKlaim allows the programmer to specify and coordinate the replication of shared data items and the desired consistency properties. The programmer can hence exploit such flexible mechanisms to adapt data distribution and locality to the needs of the application, so to improve performance in terms of concurrency and data access. We investigate issues related to replica consistency, provide an operational semantics that guides the implementation of the language, and discuss the main synchronization mechanisms of our prototypical run-time framework. Finally, we provide a performance analysis, which includes scenarios where replica-based specifications and relaxed consistency provide significant performance gains.

Introduction

The scale of parallel and distributed computing systems is growing fast to meet the computational needs of our society, ranging from (big) data-driven analyses to massively distributed services. One of the key points in parallel and distributed computing is the division and communication of data between computational entities. Better performances are achieved with increased data locality and minimized data communication.. Increasing data locality can be easily achieved by replicating data, but this comes of course at a high price in terms of synchronization if replicated data need to be kept consistent. As a matter of fact the trade-off between consistency and performance is one of the big dilemmas in distributed and parallel computing.

The recent years have seen the advent of technologies that provide software engineers and programmers with flexible mechanisms to conveniently specify data locality, communication and consistency to the benefit of their applications. A pragmatical example for large-scale distributed services is the Google Cloud Storage 3 service, that allows users to geographically specify data locality (to reduce cost and speed up access) and provides different consistency levels (e.g. strong and eventual consistency) for different operations (e.g. single data and list operations).

In the realm of parallel computing, one can find several high performance computing languages that offer similar support for designing efficient applications. De-facto standards such as OpenMP4 (for shared memory multiprocessing) and MPI 5 (for message-passing large-scale distributed computing) are being challenged by new languages and programming models that try to address concerns such as the memory address to physical location problem. This is a general concern that needs to be solved when programming scalable systems with a large number of computational nodes. In languages X106 , UPC 7 and Titanium [START_REF] Krishnamurthy | Titanium: A high performance java dialect[END_REF], this problem is solved via the partitioned global address space (PGAS) model. This model is a middle way approach between shared-memory (OpenMP) and distributed-memory (MPI) programming models, as it combines performance and data locality (partitioning) of distributed-memory and global address space of a shared-memory model. In the PGAS model, variables and arrays are either shared or local. Each processor has private memory for local data and shared memory for globally shared data.

Summarizing, two key aspects in the design of distributed and parallel systems and software are data locality and data consistency. A proper design of those aspects can bring significant performance advantages, e.g. in terms of minimization of communication between computational entities.

Contribution. We believe that those two aspects cannot be hidden to the programmer of the high performance applications of the future. Instead, we believe that programmers should be equipped with suitable primitives to deal with those aspects in a natural and flexible way. This paper instantiates such philosophy in the coordination language RepliKlaim, a variant of Klaim [START_REF] De Nicola | Klaim: a kernel language for agents interaction and mobility[END_REF] with first-class features to deal with data locality and consistency. In particular, the idea is to let the programmer specify and coordinate data replicas and operate on them with different levels of consistency. The programmer can hence exploit such flexible mechanisms to adapt data distribution and locality to the needs of the application, so to improve performance in terms of concurrency and data access. We investigate issues related to replica consistency, provide an operational semantics that guides the implementation of the language, and discuss the main synchronisation mechanisms of our implementation. Finally, we provide a performance evaluation study in our prototype run-time system. Our experiments include scenarios where replica-based specifications and relaxed consistency provide significant performance gains.

Structure of the paper. This paper is organised as follows. Section 2 presents RepliKlaim and discusses some examples that illustrate its semantics. Section 3 (processes) A ::= outs(ti)@L | ins(Tι)@ | read(Tι)@ (strong actions) outw(ti)@L | inw(Tι)@ | (weak actions) inu(Tι, L)@ | outu(eti, L)@ (unsafe actions)

N ::= 0 | l :: [K, P ] | N N (networks) K ::= ∅ | eti, L | K, K (repositories)
L ::= | | | L • L (locations) Fig. 1. Syntax of RepliKlaim
provides some details about our prototype implementation and presents a set of performance experiments. Section 4 discusses related works. Section 5 concludes the paper and identifies possible future works.

2 RepliKlaim: Klaim with replicas

We present our language RepliKlaim in this section. We start with the definition of the syntax in Section 2.1 and proceed then with the description of the operational semantics in Section 2.2. Section 2.3 discusses some examples aimed at providing some insights on semantics, implementation and performance aspects, later detailed in Section 3.

RepliKlaim: Syntax

The syntax of RepliKlaim is based on Klaim [START_REF] De Nicola | Klaim: a kernel language for agents interaction and mobility[END_REF]. The main differences are the absence of mobility features (i.e. the eval primitive and allocation environments) and the extension of communication primitives to explicitly deal with replicas.

Definition 1 (RepliKlaim syntax). The syntax of RepliKlaim is defined by the grammar of Fig. 1, where L is a set of locations (ranged over by , , . . . ), U is a set of values (ranged over by u, v, . . . ), V is a set of variables (ranged over by x, y, . . . ), !V denotes the set binders over variables in V (i.e. !x, !y, . . . ), I is a set of tuple identifiers (ranged over by i, i , j, j ), T ⊆ (U ∪ V) * is a set of I-indexed tuples (ranged over by t i , t i , . . . ), ET ⊆ (U * is a set of I-indexed evaluated tuples (ranged over by et i , et i , . . . ), and T T ⊆ (U ∪ V∪!V) * is a set of templates (ranged over by T ι , T ι , . . . , with ι ∈ I ∪ !V).

Networks. A RepliKlaim specification is a network N , i.e. a possibly empty set of components or nodes.

Components. A component :: [K, P ] has a locality name which is unique (cf. well-formedness in Def. 2), a data repository K, and set of processes P .

Components may model a data-coherent unit in a large scale system, where each unit has dedicated memory and computational resources, e.g. an SMP node in a many-core machine.

Repositories. A data repository K is a set of data items, which are pairs of identifier-indexed tuples and their replication information. In particular a data item is a pair et i , L , where t i is a tuple, i is a unique identifier of the tuple, and L is a list of localities where the tuple is replicated. For a data item et i , L with |L| > 1 we say that t i is shared or replicated. We use indexed tuples in place of ordinary anonymous tuples to better represent long-living data items such as variables and objects that can be created and updated. We require the replication information to be consistent (cf. well-formedness in Def. 2). This property is preserved by our semantics, as we shall see.

It is worth to note that a locality in L can appear as or as . The latter case denotes a sort of ownership of the tuple. We require each replicated tuple to have exactly one owner (cf. well-formedness in Def. 2). This is fundamental to avoid inconsistencies due to concurrent weak (asynchronous) retrievals or updates of a replicated tuple. This issue will be explained in detail later.

Processes. Processes are the main computational units and can be executed concurrently either at the same locality or at different localities. Each process is created from the nil process, using the constructs for action prefixing (A.P ), non-deterministic choice (P 1 + P 2 ) and parallel execution (P 1 | P 2 ).

Actions and targets. The actions of RepliKlaim are based on standard primitives for tuple spaces, here extended to suitably enable replica-aware programming. Some actions are exactly as in Klaim. For instance, read(t i )@ is the standard non-destructive read of Klaim.

The standard output operation is enriched here to allow a list of localities L as target. RepliKlaim features two variants of the output operation: a strong (i.e. atomic) one and a weak (i.e. asynchronous) one. In particular, out α (t i )@L is used to place the shared tuple t i at the data repositories located on sites l ∈ L atomically or asynchronously (resp. for α = s, w). In this way the shared tuple is replicated on the set of sites designated with L. In RepliKlaim output operations are blocking: an operation out α (t i )@L cannot be enacted if an i-indexed tuple exists at L. This is necessary to avoid inconsistent versions of the same data item in the same location to co-exist. Hence, before placing a new version of a data item, the previous one needs to be removed. However, we will see that weak consistency operations still allow inconsistent versions of the same data item to co-exist but in different locations.

As in the case of output operations, RepliKlaim features two variants of the standard destructive operation in: a strong input in s and a weak input in w . A strong input in s (T ι )@ retrieves a tuple et i matching T ι at and atomically removes all replicas of et i . A weak input in w (T ι )@ tries to asynchronously remove

P + (Q + R) ≡ (P + Q) + R P + nil ≡ P P + Q ≡ Q + P P | (Q | R) ≡ (P | Q) | R P | nil ≡ P P | Q ≡ Q | P N (M W ) ≡ (N M ) W N 0 ≡ N N M ≡ M M :: [K, P ] ≡ :: [K, nil] :: [∅, P ] Fig. 2. Structural congruence for RepliKlaim
all replicas of a tuple et i matching T ι residing in . This means that replicas are not removed simultaneously. Replicas in the process of being removed are called ghost replicas, since they are reminiscent of the ghost tuples of [START_REF] Rowstron | An efficient distributed tuple space implementation for networks of workstations[END_REF][START_REF] De Nicola | Proving the correctness of optimising destructive and non-destructive reads over tuple spaces[END_REF] (cf. the discussion in Section 4).

RepliKlaim features two additional (possibly) unsafe operations: out u (et i , L)@ puts a data item et i , L at all locations in L, while in u (T ι , L)@ retrieves a tuple et i matching T ι at and does not remove the replicas of et i . These operations are instrumental for the semantics and are not meant to appear in user specifications.

As we have seen, the syntax of RepliKlaim admits some terms that we would like to rule out. We therefore define a simple notion of well-formed network.

Definition 2 (well-formedness). Let N be a network. We say that N is well formed if:

1. Localities are unique, i.e. no two distinct components :: [K, P ], :: [K , P ] can occur in N ; 2. Replication is consistent, i.e. for every occurrence of :: [(K, et i , L ), P ] in a network N it holds that ∈ L and for all (and only) localities ∈ L we have that component is of the form :: [(K , et i , L ), P ]. Note that t is not required to be t since we allow relaxed consistency of replicas. 3. Each replica has exactly one owner, i.e. every occurrence of L has at most one owner location . 4. Tuple identifiers are unique, i.e. there is no K containing two data items et i , L , et i , L . Note that this guarantees local uniqueness; global uniqueness is implied by condition (2).

Well-formedness is preserved by the semantics, but as usual we admit some intermediate bad-formed terms which ease the definition of the semantics.

We assume the standard notions of free and bound variables, respectively denoted by fn(•) and bn(•), as well as the existence of a suitable operation for matching tuples against templates, denoted match(T ι , t i ) which yields a substitution for the bound variables of T ι . Note that ι may be a bound variable to record the identifier of the tuple. As usual, besides axiomatising the essential structure of RepliKlaim systems, the structural congruence allows us to provide a more compact and simple semantics. The axioms of the structural congruence are standard. We just remark the presence of a clone axiom (bottom right) which is similar to the one used in early works on Klaim. In our case, this clone axiom allows us to avoid cumbersome semantic rules for dealing with multiparty synchronisations where the subject component is also an object of the synchronisation (e.g. when a component removes a shared tuple t i that has a replica in itself). The clone axiom allows a component to participate in those interactions, by separating the processes (the subject) from the repository (the object). It is worth to note that this axiom does not preserve well-formedness (uniqueness of localities is violated).

A.P A -→P (ActP) P A -→P P +Q A -→P (Choice) P A -→P P |Q A -→P |Q (Par) P outs(t i )@L ------→P ∀ ∈L. ∃et ,L . et i ,L ∈K N ::[K,P ] Π ∈L ::[K ,P ] -→ N ::[K,P ] Π ∈L ::[(K , et i ,L ),P ] (OutS) P outw (t i )@L -------→P ∈L ∃et ,L . et i ,L ∈K N ::[K,P ] ::[K ,P ] -→ N ::[K,P ] ::[(K , et i ,L ),P |Π ∈(L\ ) outu(et i ,L)@ ] (OutW) P outu (et i ,L)@ --------→P ∃et ,L . et i ,L ∈K N ::[K,P ] -→ N ::[(K, et i ,L ),P ] (OutU) P ins(Tι )@ -------→P ∈L σ=match(Tι,et i ) N ::[K,P ] Π ∈L ::[(K , et i ,L ),P ] -→ N ::[K,P σ] Π ∈L ::[K ,P ] (InS) P inw (Tι )@ -------→P ∈L ∈L σ=match(Tι,et i ) N ::[K,P ] ::[(K , et i ,L ),P ] -→ N ::[K,P σ] ::[K ,P | ∈(L\ ) inu(et i ,L)@ ] (InW) P inu (Tι ,L)@ --------→P σ=match(Tι,et i ) N ::[K,P ] ::[(K , et i ,L ),P ] -→ N ::[K,P σ] ::[K ,P ] (InU) P read(Tι )@ -------→P σ=match(Tι,et i ) N ::[K,P ] ::[(K , et i ,L ),P ] -→ N ::[K,P σ] ::[(K , et i ,L ),P ] (Read)
The operational semantics in Fig. 3 mixes an SOS style for collecting the process actions (cf. rules ActP, Choice and Par) and reductions for the evolution of nets. The standard congruence rules are not included for simplicity. It is worth to remark that the replicas located at the owner are used in some of the rules as a sort of tokens to avoid undesirable race conditions. The role of such tokens in inputs and outputs is dual: the replica must not exist for output to be enacted, while the replica must exist for inputs to be enacted.

N • • • ins Ô Ô read & & ins { { Ns • • • ins Ô Ô read & & ins { { Nw • • • • • inw Ô Ô read & & inw { { read & & inu Ô Ô inu { {
Rule OutS deals with a strong output out(et i )@L by putting the tuple et i in all localities in L. However, the premise of the rule requires a version of data item i (i.e. a tuple et i ) to not exist in the repository of the owner of et i ( ). Rule OutW governs weak outputs of the form out(et i )@L by requiring the absence of a version of data item i. The difference with respect to the strong output is that the effect of the rule is that of creating a set of processes that will take care of placing the replicas in parallel, through the unsafe output operation. Such operation is handled by rule OutU which is very much like a standard Klaim rule for ordinary outputs, except that the operation is blocking to avoid overwriting existing data items.

Rule InS deals with actions in(T ι )@ by retrieving a tuple et i matching T ι from locality , and from all localities containing a replica of it. Rule InW retrieves a tuple et i from an owner of a tuple that has a replica in the target . As a result, processes are installed at that deal with the removal of the remaining replicas in parallel (thus allowing the interleaving of read operations). As in the case of weak outputs, weak inputs resort to unsafe inputs. Those are handled by rule InU, which is like a standard input rule in Klaim.

Finally, rule Read is a standard rule for dealing with non-destructive reads.

RepliKlaim: Examples

We provide here a couple of illustrative examples aimed at providing insights on semantics, implementation and performance aspects.

Concurrent reads and inputs. The following example illustrates three ways of sharing and accessing a tuple and is meant to exemplify the benefit of replicas and weak inputs. The example consists of the networks

Ms • • outs Ô Ô read & & Mw • • • • outw Ô Ô outu Ô Ô read & & read & & Ws • • ins Ô Ô outs & & Ww • • • • • inw Ô Ô inu Ô Ô outw & & inu { { outw & & outu & &
N . = 1 :: [ et i , 1 , in s (et j )@ 1 ] 2 :: [∅, read(et j )@ 1 ] N α . = 1 :: [ et i , { 1 , 2 } , in α (et j )@ 1 ] 2 :: [ et i , { 1 , 2 } , read(et j )@ 2 ]
with α ∈ {s, w}. The idea is that in N a tuple has to be accessed by both 1 and 2 is shared in the traditional Klaim way: it is only stored in one location (namely, 1 ) with no replicas. To the contrary, N α models the same scenario with explicit replicas. The tuple et i is replicated at both 1 and 2 , possibly after some process executed out(et i )@{ 1 , 2 }. Networks N s and N w differ in the way the tuple et i is retrieved by 1 : using strong or weak input, respectively. Fig. 4 depicts the transition systems for the three networks, where the actual description of the reachable states is not provided due to lack of space and due to the simplicity of the example. The transition systems of N and N s are similar but differ in the way the transitions are computed. In N , the input is local to 1 , but the read is remote (from 2 to 1 ), while in N s the input is global (requires a synchronization of 1 and 2 to atomically retrieve all replicas of et i ), and the read is local to 2 . The main point in N w is that the process in 2 can keep reading the ghost replicas of et i even after 1 started retrieving it.

Concurrent reads and outputs. The next example illustrates (see also Fig. 5) the interplay of reads with strong and weak outputs.

M α . = 1 :: [∅, out α (et i )@{ 1 , 2 }] 2 :: [∅, read(et j )@ 1 ]
with α ∈ {s, w}. The idea is that component 1 can output a tuple with replicas in 1 and 2 in a strong or weak manner, while 2 is trying to read the tuple from 1 . In the strong case, the read can happen only after all replicas have been created. In the weak case, the read can be interleaved with the unsafe output.

Concurrent inputs and outputs. The last example (see also Fig. 5) illustrates the update of a data item using strong and weak operations.

W α . = 1 :: [∅, in α (et i )@{ 1 , 2 }.out α (f (et) i )@{ 1 , 2 }] 2 :: [∅, nil]
with α ∈ {s, w}. The idea is that component 1 retrieves a tuple and then outputs an updated version of it (after applying function f ). Relaxing consistency from s to w increases the number of interleavings.

Performance Evaluation

We describe in this section our prototype implementation and present a set of experiments aimed at showing that an explicit use of replicas in combination with weakly consistent operations then provide significant performance advantages.

Implementing RepliKlaim in Klava. Our prototype run-time framework is based on Klava, a Java package used for implementing distributed applications based on Klaim. Klava is a suitable framework for testing our hypothesis as it provides a set of process executing engines (nodes) connected in a network via one of the three communication protocols (TCP, UDP, local pipes). The current implementation of RepliKlaim is based on an encoding of RepliKlaim into standard Klaim primitives. We recall the main Klaim primitives we use in the encoding: in(T )@ destructively retrieves a tuple matching T in location . The operation is blocking until a matching tuple is found; read(T )@ : non-destructive variant of in; out(t)@ : inserts a tuple t into the tuple space located at . The actual encoding is based on the operational semantics presented in Fig. 3, which already uses some operations that are close to those of Klaim, namely the unsafe operations in u and out u . The rest of the machinery (atomicity, etc.) is based on standard synchronisation techniques.

Experiments: Hypothesis. The main hypothesis of our experiments is that better performances are achieved with improved data locality and data communication minimized through the use of replicated tuples and weak operations. Indeed, minimizing data locality can be easily done by replicating data, however it comes at a cost in terms of synchronization if replicated data need to be kept consistent (e.g. when using strong inputs and outputs). As we shall see, our experimental results show how the ratio between the frequencies of read and update (i.e. sequences of inputs and outputs on the same data item) operations affects the performance of three different versions of a program: a traditional one that does not use replicas, and two versions using replicas: one using strong (consistent) operations and another one using weak (weak consistent) operations. We would only like to remark that we had to deviate in one thing from the semantics: while spawning parallel processes in rules InW and OutW to deal with the asynchronous/parallel actions on replicas seems very appealing, in practice performing such operations in sequence showed to be more efficient. Of course in general the choice between parallel and sequential composition of such actions depends on several aspects, like the number of available processors, the number of processes already running in the system and the size of the data being replicated.

Experiments: Configuration of the Scenario. 8 The general idea of the scenario we have tested is that multiple nodes are concurrently working (i.e. performing inputs, reads and outputs) on a list whose elements can be scattered on various nodes. A single element (i.e. the counter) is required to indicate the number of the next element that can be added. In order to add an element to the list, the counter is removed using an input, the value of the counter is increased and the tuple is re-inserted, and then a new list element is inserted. We call such a sequence of input and output operations on the same data item (i.e. the counter) an update operation. Each of the nodes is running processes that perform read or update operations. Both reader and updater processes run in loops. We fix the number of updates to 10, but vary the number of read accesses [START_REF] Li | Making geo-replicated systems fast as possible, consistent when necessary[END_REF]30,50,100,150,200). We consider two variants of the scenario. The first variant has 3 nodes: one node containing just one reader process, another node containing just one updater process and a last one containing both a reader and an updater process. The second variant has 9 nodes, each containing process as in the previous case, i.e. this scenario is just obtained by triplicating the nodes of the previous scenario. The main point for considering these two variants is that we run the experiment in a dual core machine, so that in the first case one would ideally have all processes running in parallel, while this is not the case in the second variant.

Formally, the RepliKlaim nets N we use in our experiments are specified as follows

N . = n i=1 i,1 :: [∅, P 1 ( i,1 )] i,2 :: [∅, P 2 ( i,2 )] i,3 :: [∅, P 1 ( i,3 ) | P 2 ( i,3 )]
where P 1 is an updater process and P 2 is a reader process, both parametric with respect to the locality they reside on. P 1 is responsible for incrementing the counter and adding a new list element, while P 2 only reads the current number of list elements. For the scalability evaluation we compare results for nets obtained when n = 1 and n = 3, meaning that corresponding nets have 3 and 9 nodes respectively. Our aim is to compare the following three alternative implementations of processes P 1 and P 2 which offer the same functionality, but exhibit different performances:

Program noreplicas: this implementation follows a standard approach that does not make use of replica-based primitives. The idea here is that the shared tuple is stored only in one location, with no replicas. The consistency of such model is obviously strong, as there are no replicas. Local access to the shared tuple is granted only to processes running on the specified location, while other processes access remotely. In the begining we assume that one 8 The source code and Klava library are available online at http://sysma.imtlucca.it/wp-content/uploads/2015/03/RepliKlaim-test-examples.rar of the sites has executed out s (counter a )@ 1 which places the counter tuple counter a at place 1 , with a being a unique identifier. Then processes P 1 and P 2 can be expressed as follows:

P 1 (self ) ≡ in s (counter a )@ 1 .out s (f (counter a ))@ 1 .out s (lt acounter )@self .P 1 P 2 (self ) ≡ read(T a )@ 1 .P 2

where f (•) refers to the operation of incrementing the counter and lt refers to the new list element which is added locally after the shared counter had been incremented. Note that we use a as unique identifier for the counter and a counter as unique identifier for the new elements being inserted. Program strongreplicas: The difference between this model and the nonreplicated one is the presence of replicas on each node, while this model also guarantees strong consistency. Concretely, each update of replicated data items is done via operations in s and out s . The formalisation is presented below, after the description of the weak variant of this implementation. Program weakreplicas: In this variant, the replicas are present on each node, but the level of consistency is weak. This means that interleavings of actions over replicas are allowed. However, to make this program closer to the functionality offered by the above ones, we forbid the co-existence of different versions of the same data item. Such co-existence is certainly allowed in sequences of operations like in w (t i )@ .out w (t i )@L as we have seen in the examples of Section 2.3. To avoid such co-existence, but still allow concurrent reads we use an additional tuple that the updaters used as sort of lock to ensure that outputs (reps. inputs) are only enacted once inputs (resp. outputs) on the same data item are completed on all replicas. Of course, this makes this program less efficient than it could be but it seems a more fair choice for comparison and still our results show its superiority in terms of performance.

In the above two replication-based implementations we assume that the counter is replicated on all nodes by executing out α (counter a )@{ 1 , 2 , 3 } with α ∈ {s, w}. In this case the processes are specified as:

P 1 (self ) ≡ in α (counter a )@self.out α (f (counter a ))@{ 1 , 2 , 3 }.
out s (a counter )@self.P 1 P 2 (self ) ≡ read(T a )@self.P 2 where the strong and weak variants are obtained by letting α be s and w, respectively.

Experiments: Data and Interpretation. The results of our experiments are depicted in Fig. 6 and7. The x axis corresponds to the ratio of reads and updates performed by all processes, while the y axis corresponds to the time needed by the processes to complete their computation. We measure the relation between average running time and the ratio between access frequencies. Time is expressed in seconds and presents the average of 15 executions, while the ratio is a number [START_REF] Atkinson | Development and Execution of Array-based Applications in a Cluster Computing Environment[END_REF][START_REF] Balzarotti | The lights tuple space framework and its customization for context-aware applications[END_REF][START_REF] Bettini | Klava: a java package for distributed and mobile applications[END_REF][START_REF] Capizzi | A tuple space implementation for large-scale infrastructures[END_REF][START_REF] Van Der Goot | High Performance Linda using a Class Library[END_REF][START_REF] Li | Making geo-replicated systems fast as possible, consistent when necessary[END_REF]. The results obtained for programs noreplicas, strongreplicas and weakreplicas are respectively depicted in blue, green and red.

It can be easily observed that when increasing the ratio the weakreplicas program is the most efficient. This program improves over program noreplicas only after the ratio of reading operations reaches a certain level that varies from the two variants used (3 and 9 nodes). The variant with 9 nodes requires a higher ratio to show this improvement, mainly due to the fact that the 12 processes of the scenario cannot run in parallel in the dual-core machine we used. Note that strongreplicas offers the worst performance. Indeed, preserving strong consistency in presence of replicas is unfeasible in practice because it requires a great deal of synchronization.

Related Works

Many authors have investigated issues related to the performance of tuple space implementations and applications of tuple space coordination to large-scale distributed and concurrent systems (cloud computing, high-performance computing, services, etc.). We discuss here some representative approaches that are closely related to our work and, in part, served as inspiration.

One of the first performance improvements for tuple-space implementations was the ghost tuple technique, originally presented in [START_REF] Rowstron | An efficient distributed tuple space implementation for networks of workstations[END_REF] and later proven to be correct in [START_REF] De Nicola | Proving the correctness of optimising destructive and non-destructive reads over tuple spaces[END_REF]. The technique applies to Linda-like languages used in a distributed setting where local tuple replicas are used to improve local operations. Ghost tuple is a local replica of a tuple being destructively read (by a Linda in) operation. The ghost tuple technique allows the non-destructive read of those local replicas (by a Linda read operation). This technique is very similar to our idea of relaxing consistency in tuple space operations. In particular, our local replicas can be seen as ghost tuples as we have mentioned in several occasions in the paper. As a matter of fact, the ghost tuple technique is one of our main sources of inspiration.

Another seminal work considering performance issues in tuple space coordination was the introduction of asynchronous tuple space primitives in Bonita (asynchronous Linda) [START_REF] Rowstron | Using asynchronous tuple-space access primitives (BONITA primitives) for process co-ordination[END_REF]. This work provided a practical implementation and an illustrative case study to show the performance advantages of asynchronous variants of tuple space primitives for coordinating distributed agents. A thorough theoretical study of possible variants of tuple space operations was later presented in [START_REF] Busi | Comparing three semantics for linda-like languages[END_REF]. In particular, the authors study three variants for the output operation: an instantaneous output (where an output can be considered as instantaneous creation of the tuple), and ordered output (where a tuple is placed in the tuple space as one atomic action) and an unordered output (where the tuple is passed to the tuple space handler and the process will continue, the tuple space handler will then place the tuple in the tuple space, not necessarily respecting order of outputs). A clear understanding of (true) concurrency of tuple space operations was developed in [START_REF] Busi | A truly concurrent view of linda interprocess communication[END_REF], where the authors provide a contextual P/T nets semantics of Linda. All these works have inspired the introduction of the asynchronous weak operations in RepliKlaim.

Performance issues have been also considered in tuple space implementations. Besides Klaim implementations [START_REF] Bettini | Klava: a java package for distributed and mobile applications[END_REF][START_REF] Bettini | Implementing mobile and distributed applications in x-klaim[END_REF], we mention GigaSpaces [START_REF]Gigaspaces technologies ltd[END_REF], a commercial tuple space implementation, Blossom [START_REF] Van Der Goot | High Performance Linda using a Class Library[END_REF], a C++ high performance distributed tuple space implementation, Lime [START_REF] Murphy | LIME: A coordination model and middleware supporting mobility of hosts and agents[END_REF], a tuple space implementation tailored for ad-hoc networks, TOTA [START_REF] Mamei | Programming pervasive and mobile computing applications: The TOTA approach[END_REF], a middleware for tuple-based coordination in multi-agent systems, and PeerSpace [START_REF] Busi | Data-driven coordination in peer-to-peer information systems[END_REF] a P2P based tuple space implementation. Moreover, tuple space coordination has been applied and optimised for a large variety of systems where large-scale distribution and concurrency are key aspects. Among other, we mention large-scale infrastructures [START_REF] Capizzi | A tuple space implementation for large-scale infrastructures[END_REF], cluster computing environments [START_REF] Atkinson | Development and Execution of Array-based Applications in a Cluster Computing Environment[END_REF], cloud computing systems [START_REF] Hari | Tuple Space in the Cloud[END_REF], grid computing systems [START_REF] Li | Comet: a scalable coordination space for decentralized distributed environments[END_REF], context-aware applications [START_REF] Balzarotti | The lights tuple space framework and its customization for context-aware applications[END_REF], multi-core Java programs [START_REF] Gudenkauf | Space-based multi-core programming in java[END_REF], and high performance computing systems [START_REF] Jiang | Dtupleshpc: Distributed tuple space for desktop high performance computing[END_REF]. As far as we know, none of the above mentioned implementations treats replicas as first-class programming citizens.

Another set of works that are worth considering are recent technologies for high performance computing. Among them we mention non-uniform cluster computing systems, which are built out of multi-core SMP chips with non-uniform memory hierarchies, and interconnected in horizontally scalable cluster configurations such as blade servers. The programming language X10, currently under development, is intended as object-oriented language for programing such systems. A recent formalization of some X10 features can be found in [START_REF] Crafa | Semantics of (resilient) X10[END_REF]. The main concept of X10 is a notion of place which is a collection of threads (activities) and data, and it maps to a data-coherent unit of a large system (e.g. SMP node). In X10 the programmer makes the initial distribution of shared data which is not changed throughout the program execution. Each piece of shared data maps to a single place, and all remote accesses are achieved by spawning (asynchronous) activities. In our language, such concept of place would correspond to a single node. We believe that the concept of replicas introduced in RepliKlaim, can be suitable for modeling high-performance programming using X10-like programming languages.

Conclusion

We have presented the tuple-based coordination language RepliKlaim, which enriches Klaim with primitives for replica-aware coordination. RepliKlaim allows the programmer to specify and coordinate the replication of shared data items and the desired consistency properties so to obtain better performances in large-scale high performance computing applications. We have provided an operational semantics to formalise our proposal as well as to guide the implementation of the language, which has been encoded into Klava [START_REF] Bettini | Klava: a java package for distributed and mobile applications[END_REF], a Java-based implementation of Klaim. We have also discussed issues related to replica consistency and the main synchronization mechanisms of our implementation. Finally, we have provided a performance evaluation study in our prototype run-time sys-tem. Our experiments include scenarios where replica-based specifications and relaxed consistency provide significant performance gains.

We plan to enrich our performance evaluation to consider large-scale distributed systems since our focus so far has been on local concurrent systems. Moreover, we would like to compare our implementation against existing tuple space implementations (cf. the discussion in Section 4). We may also consider other forms of consistency beyond strong and weak, as advocated e.g. in [START_REF] Terry | Replicated data consistency explained through baseball[END_REF][START_REF] Brewer | CAP twelve years later: How the "rules" have changed[END_REF], and to understand if there are automatic ways to help the programmer decide when to use which form of consistency as done, e.g. in [START_REF] Li | Making geo-replicated systems fast as possible, consistent when necessary[END_REF]. Another future work we plan to pursue is to apply our approach to the Scel language [START_REF] De Nicola | A formal approach to autonomic systems programming: The SCEL language[END_REF]. One characteristic difference between Scel and Klaim is that the target of tuple operations can be specified by a predicate on the attributes of components. This provides a great flexibility as it allows to use group-cast operations without explicitly creating groups, called ensembles in Scel. In many applications creating replicas would be a convenient mechanism to share information among groups. However, the dynamicity of ensembles, since components change attributes at run-time and those join and leave ensembles arbitrarily, poses some challenges on the semantics and implementation of shared data items that need to be investigated.

  P ::= nil | A.P | P + P | P | P

Fig. 3 .

 3 Fig. 3. Operational semantics of RepliKlaim

Fig. 4 .

 4 Fig. 4. Concurrent reads and inputs with no replicas (left), replicas and strong input (center) and weak input (right).

Fig. 5 .

 5 Fig. 5. Transitions for Ms (concurrent read and strong output), Mw (concurrent read and weak output), Ws (concurrent strong input and strong output) and Ww (concurrent weak input and weak output).

Fig. 6 .

 6 Fig. 6. Comparing three strategies in a scenario with 3 nodes

Fig. 7 .

 7 Fig. 7. Comparing three strategies in a scenario with 9 nodes

https://cloud.google.com/storage/

www.openmp.org/

http://www.open-mpi.org/

x10-lang.org

upc.lbl.gov