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

Sean Halle

Farhad Arbab
email: farhad]@cwi.nl

Automata-based Optimization of Interaction Protocols for Scalable Multicore Platforms

Multicore platforms offer the opportunity for utilizing massively parallel resources. However, programming them is challenging. We need good compilers that optimize commonly occurring synchronization/ interaction patterns. To facilitate optimization, a programming language must convey what needs to be done in a form that leaves a considerably large decision space on how to do it for the compiler/run-time system. Reo is a coordination-inspired model of concurrency that allows compositional construction of interaction protocols as declarative specifications. This form of protocol programming specifies only what needs to be done and leaves virtually all how -decisions involved in obtaining a concrete implementation for the compiler and the run-time system to make, thereby maximizing the potential opportunities for optimization. In contrast, the imperative form of protocol specification in conventional concurrent programming languages, generally, restrict implementation choices (and thereby hamper optimization) due to overspecification. In this paper, we use the Constraint Automata semantics of Reo protocols as the formal basis for our optimizations. We optimize a generalization of the producer-consumer pattern, by applying CA transformations and prove the correctness of the transforms.

Introduction

Context. Coordination languages have emerged for the implementation of protocols among concurrent entities (e.g., threads on multicore hardware). One such language is 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 language for compositional construction of connectors (i.e., custom synchronization protocols). Figure 1a shows an example. Briefly, a connector consists of one or more edges (henceforth referred to as channels), through which data items flow, and a number of nodes (henceforth referred to as ports), on which channel ends coincide. The connector in Figure 1a contains three different channel classes, including standard synchronous channels (normal arrows) and asynchronous channels with a buffer of capacity 1 (arrows decorated with a white rectangle, which represents a buffer). Through connector composition (the act of gluing connectors together on their shared ports), programmers can construct arbitrarily complex connectors. As Reo supports both synchronous and asynchronous channels, connector composition enables mixing synchronous and asynchronous communication within the same specification. Especially when it comes to multicore programming, Reo has a number of advantages over conventional programming languages with a fixed set of low-level synchronization constructs (locks, mutexes, etc.). Programmers using such a conventional language have to translate the synchronization needs of their protocols into the synchronization constructs of that language. Because this translation occurs in the mind of the programmer, invariably some context information either gets irretrievably lost or becomes implicit and difficult to extract in the resulting code. In contrast, Reo allows programmers to compose their own synchronization constructs (i.e., connectors) at a high abstraction level to perfectly fit the protocols of their application. Not only does this reduce the conceptual gap for programmers, which makes it easier to implement and reason about protocols, but by preserving all relevant context information, such user-defined synchronization constructs also offer considerable novel opportunities for compilers to do optimizations on multicore hardware. This paper shows one such occasion.

Additionally, Reo has several software engineering advantages as a domainspecific language for protocols [START_REF] Jongmans | Modularizing and Specifying Protocols among Threads[END_REF]. For instance, Reo forces developers to separate their computation code from their protocol code. Such a separation facilitates verbatim reuse, independent modification, and compositional construction of protocol implementations (i.e., connectors) in a straightforward way. Moreover, Reo has a strong mathematical foundation [START_REF] Jongmans | Overview of Thirty Semantic Formalisms for Reo[END_REF], which enables formal connector analyses (e.g., deadlock detection, model checking [START_REF] Kokash | Reo+mCRL2: A framework for modelchecking dataflow in service compositions[END_REF]).

To use connectors in real programs, developers need tools that automatically generate executable code for connectors. In previous work [START_REF] Jongmans | Reo: A Dataflow Inspired Language for Multicore[END_REF], we therefore developed a Reo-to-C compiler, based on Reo's formal semantics of constraint automata (ca) [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]. In its simplest form, this tool works roughly as follows. First, it extracts from an input Xml representation of a connector a list of its primitive constituents. 1 Second, it consults a database to find for every constituent in the list a "small" ca that formally describes the behavior of that particular constituent. Third, it computes the product of the ca in the constructed collection to obtain one "big" ca describing the behavior of the whole connector. Fourth, it feeds a data structure representing that big ca to a template. Essentially, this template is an incomplete C file with "holes" that need be "filled". The generated code simulates the big ca by repeatedly computing and firing eligible transitions in an event-driven fashion. It runs on top of Proto-Runtime [START_REF] Halle | A Study of Frameworks for Collectively Meeting the Productivity, Portability, and Adoptability Goals for Parallel Software[END_REF][START_REF] Halle | A Mutable Hardware Abstraction to Replace Threads[END_REF], an execution environment for C code on multicore hardware. A key feature of Proto-Runtime is that it provides more direct access to processor cores and control over scheduling than threading libraries based on os threads, such as Pthreads [START_REF] Butenhof | Programming with POSIX Threads[END_REF].

Problem. Figure 1a shows a connector for a protocol among k = 3 producers and one consumer in a producers-consumer benchmark. Every producer loops through the following steps: (i) it produces, (ii) it blocks until the consumer has signaled ready for processing the next batch of productions, and (iii) it sends its production. Meanwhile, the consumer runs the following loop: (i) it signals ready, and (ii) it receives exactly one production from every producer in arbitrary order. We compared the ca-based implementation generated by our tool with a hand-crafted implementation written by a competent C programmer using Pthreads, investigating the time required for communicating a production from a producer to the consumer as a function of the number of producers.

Figure 1b shows our results. On the positive side, for k ≤ 256, the ca-based implementation outperforms the hand-crafted implementation. For k = 512, however, the Pthreads-based implementation outperforms the generated implementation. Moreover, the dotted curve looks disturbing, because it grows morethan-linearly in k: indeed, the ca-based implementation scales poorly. (We skip many details of this benchmark, including those of the Pthreads-based implementation, and the meaning/implications of these experimental results. The reason is that this paper is not about this benchmark, and its details do not matter. We use this benchmark only as a concrete case to better explain problems of our compilation approach and as a source of inspiration for solutions.) Contribution. In this paper, we report on work at improving the scalability of code generated by our Reo-to-C compiler. First, we identify a cause of poor scalability: briefly, computing eligibility of k transitions in producers-consumerstyle protocols (and those generalizations thereof that allow any synchronization involving one party from every one of groups) takes O(k) time instead of O(1), of which the Pthreads-based implementation shows that it is possible. Second, to familiarize the reader with certain essential concepts, we explain a manual solution (in terms of Reo's ca semantics) that achieves O(1). Third, we propose an automated, general solution, built upon the same concepts as the manual We formalize this automated solution and prove it correct. Although inspired by our work on Reo and formulated in terms of ca, we make more general contributions beyond Reo and ca, better explained in our conclusion.

AB , d(A) = d(B) AB , (a) LossySync AZBC , d(A) = d(Z) BZAC , d(B) = d(Z) CZAB , d(C) = d(Z) (b) Merger3 AHZBY , d(A) = d(H) = d(Z) AHYBZ , d(A) = d(H) = d(Y) BHZAY , d(B) = d(H) = d(Z) BHYAZ , d(B) = d(H) = d(Y) (c) Hourglass
We organized the rest of this paper as follows. In Section 2, we explain ca. In Section 3, we analyze how the Pthreads-based implementation avoids scalability issues and how we can export that to our setting. In Sections 4-6, we automate the solution proposed in Section 3. Section 7 concludes this paper. Definitions and detailed proofs appear in the appendix of a technical report [START_REF] Jongmans | Automata-based Optimization of Interaction Protocols for Scalable Multicore Platforms[END_REF].

Although inspired by Reo, we can express our main results in a purely automata-theoretic setting. We therefore skip a primer on Reo [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Arbab | Puff, The Magic Protocol[END_REF].

Constraint Automata

Constraint automata are a general formalism for describing systems behavior and have been used to model not only connectors but also, for instance, actors [START_REF] Sirjani | Compositional Semantics of an Actor-Based Language Using Constraint Automata[END_REF]. Figure 2 shows examples. 2,3 In the context of this paper, a ca specifies when during execution of a connector which data items flow where. Structurally, every ca consists of finite sets of states, transitions between states, and ports. States represent the internal configurations of a connector, while transitions describe its atomic execution steps. Every transition has a label that consists of two elements: a synchronization constraint (sc) and a data constraint (dc). An sc is a propositional formula that specifies which ports synchronize in a firing transition , where data items flow); a dc is a propositional formula that (under)specifies which particular data items flow where. For instance, in Figure 2a, the dc d(A) = d(B) means that the data item on A equals the data item on B; the dc means that it does not matter which data items flow. Let Port denote the global set of all ports. Formally, an sc is a word ψ generated by the grammar in Figure 3a, while a dc is a word φ generated by the grammar in Figure 3b.

Figure 3a generalizes the original definition of scs as sets of ports interpreted as conjunctions [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF] (shortly, we elaborate on the exact correspondence). Operator is a uniqueness quantifier: (Ψ ) holds if exactly one sc in Ψ holds. Also, we remark that predicate Eq(P ) is novel. It holds if equal data items are distributed over all ports in P . In many practical cases-but not all-we can replace a dc of the shape d(p 1 ) = d(p 2 ) with Eq(P ) if {p 1 , p 2 } ⊆ P . In the development of our optimization technique, Eq(P ) plays an important role (see also Section 7).

Let Data denote the set of all data items. Formally, we interpret scs and dcs over distributions of data over ports, δ : Port Data, using relations |= sc and |= dc and the corresponding equivalence relations ≡ sc and ≡ dc . Their definition for negation, disjunction, and conjunction is standard; for atoms, we have:

δ |= sc p iff p ∈ Dom(δ) δ |= dc Eq(P ) iff |Img(δ| P )| = 1 δ |= dc d(p 1 ) = d(p 2 ) iff δ(p 1 ) = δ(p 2 ) Let ({ψ 1 , . . . , ψ k }) and ({ψ 1 , . . . , ψ k }) abbreviate ψ 1 + • • • + ψ k and ψ 1 • • • ψ k , let
SC denote the sets of all scs, and let SC(P ) and DC(P ) denote the sets of all scs and all dcs over ports in P .

A constraint automaton is a tuple (Q , P , -→ , ı) with Q a set of states, P ⊆ Port a set of ports, -→ ⊆ Q × SC(P ) × DC(P ) × Q a transition relation labeled with sc, dc -pairs of the form (ψ , φ), and ı ∈ Q an initial state.

A distribution δ represents a single atomic execution step of a connector in which data item δ(p) flows on port p (for all ports in the domain of δ). A ca α accepts streams (i.e., infinite sequences) of such distributions. Every such a stream represents one possible infinite execution of the connector modeled by α. Intuitively, to see if α accepts a stream σ, starting from the initial state, take the first element σ(0) from the stream, check if α has a (ψ , φ)-labeled transition from the current state such that σ(0) |= sc ψ and σ(0) |= dc φ, and if so, make this transition, remove σ(0) from the stream, and repeat.

Our ca definition generalizes the original definition of ca still play a role in the development of our optimization technique: all input ca that this technique operates on are original. Therefore, we make more precise what "originality" means. First, let a P -complete product be a product of either a positive or a negative literal for every port in P . Intuitively, a P -complete product specifies not only which ports participate in a transition, but it also makes explicit which ports idle in that transition. Let cp(P , P + ) denote a Pcomplete product with positive literals P + ⊆ P . Then, we call an sc ψ original if a set P + exists such that cp(P , P + ) ≡ ψ (originally, set P + would be the sc); we call a ca original if it has only original scs. All ca in Figure 2 are original.

We adopt bisimilarity on ca as behavioral congruence, derived from the definition for original ca of Baier et al. [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]. Roughly, if α and β are bisimilar, denoted as α ∼ β, α can simulate every transition of β in every state and vice versa (see Definition 32 in [11, Appendix A]). Now, recall our producers-consumer benchmark in Section 1. Figure 2b shows the ca for the connector in Figure 1a. 4 Generally, for an arbitrary number of producers k, the corresponding ca α k has k transitions. Consequently, in the worst case, the handler in the generated alpha k code performs k checks in every event handling round, which takes O(k) time. Figure 1b shows this as a morethan-linear increase in execution time for the dotted curve. 5 The Pthreads-based implementation, in contrast, uses a queue for lining up available productions. To receive a production, the consumer simply dequeues, which takes only O(1) time (ignoring, for simplicity, the overhead of synchronizing queue accesses). Figure 1b shows this as a linear increase in execution time for the continuous curve.

Intuitively, by checking all transitions to make the consumer receive, the generated ca-based implementation performs an exhaustive search for a particular producer that sent a production. In contrast, by using a queue, the Pthreadsbased implementation avoids such a search: the queue embodies that in this protocol, it does not matter which particular producer sent a production as long as some producer has done so (in which case the queue is nonempty). The producers are really indistinguishable from the perspective of the consumer. Thus, to improve the scalability of code generated by our tool, we want to export the idea of "using queues to leverage indistinguishability" to our setting.

Figure 4b shows a first attempt at achieving this goal: we introduce a manual transformation h that takes alpha as input and hacks together a new piece of code beta, which should (i) behave as alpha, (ii) demonstrate good scalability, and (iii) use queues. For instance, in our producers-consumer example (k = 3), h works roughly as follows. First, h replaces the event variable in the data structure for every port p ∈ {A, B, C, Z} with an eventQueue variable that points to a queue of pending events. In this new setup, to perform an i/o operation, the environment enqueues an eventQueue, while handler code tests eventQueues for nonemptiness to check scs, peeks eventQueues to check dcs, and dequeues eventQueues to fire transitions. Subsequently, h adds initialization code to alpha to ensure that the eventQueue variables of ports A, B, and C all point to the same shared queue, while the eventQueue variable for port Z points to a different queue. Here, h effectively exploits the indistinguishability property of producers by making the ports that those producers use indistinguishable in our setting. Finally, h updates the handler code such that it processes the shared queue only Fig. 5: Per-interaction overhead for the Pthreads-based implementation (continuous line; squares), the pre-optimized ca-based implementation (dotted line; diamonds), and the optimized, h-transformed ca-based implementation (dashed line; triangles) of the producers-consumer scenario in Figure 1 once per event handling round instead of thrice (i.e., once for every transition). From an automata-theoretic perspective, h replaces the implementation of the three "physical" transitions with an implementation of one merged "virtual" transition. When the handler fires this virtual transition at run-time, it actually fires one of the three physical transitions.

Property (iii) holds of the piece of code beta resulting from applying h to alpha as just described. Figure 5 shows that also property (ii) holds. The dashed curve in Figure 5a shows execution times of h-transformed code of the ca-based implementation in the producers-consumer benchmark. The h-transformed code scales much better than the original code. Additionally, Figure 5b shows execution times of the producers-consumer benchmark without a barrier (i.e., producers send productions whenever they want). In this variant, h achieves even better results: it transforms a poorly scalable program into one that scales perfectly. 6 Establishing property (i), however, is problematic. Although we can informally argue that it holds, proving this-formally showing the equivalence of two concurrent C programs-seems prohibitively complex. That aside, the manual nature of h makes its usage generally impractical, and it seems extremely difficult to automate it: an automated version of h would have to analyze C code to recover relevant context information about the protocol, which is not only hard but often theoretically impossible. Similarly, it seems infeasible to write an 6 Of course, in many cases and for many applications, a purely asynchronous producers-consumer protocol without a barrier, as in Figure 5b, suffices. The reason that we initially focused on a producers-consumer protocol with a barrier, which is also useful yet in other applications, is that its mix of synchrony and asynchrony makes it a harder, and arguably more interesting, protocol to achieve good scalability for. Comparing the results in Figures 5a and 5b also shows this.

AB , Eq({A , B}) AB , (a)

LossySync AZBC + BZAC + CZAB , Eq({A , B , C , Z}) (b) Merger3 AHZBY + AHYBZ + BHZAY + BHYAZ , Eq({A , B , H , Y , Z}) (c) Hourglass
Fig. 6: Application of transformations f 1 to the ca in Figure 2 optimizing compiler able to transform, for instance, less scalable Pthreads-based implementations of the producers-consumer scenario (without queues) into the Pthreads-based implementation (with queues) used in our benchmark. The inability of compilers for lower-level languages to do such optimizations seems a significant disadvantage of using such languages for multicore programming. We therefore pursue an alternative approach, outlined in Figure 4c: we introduce a transformation f that takes ca α as input-instead of the low-level C code generated for it-and transforms it into an equivalent automaton β, a variant of α with merged transitions (cf. transformation h, which implicitly replaced the implementation of several physical transitions with one virtual transition). Crucially, α still explicitly contains all relevant context information about the protocol, exactly what makes f eligible to automation. In particular, to merge transitions effectively, f carefully inspects transition labels and takes port indistinguishability into account. The resulting merged transitions have an "obvious" and mechanically obtainable implementation using queues. A subsequent transformation g 2 , from β to beta, performs this final straightforward step.

We divide transformation α

Transformation f 1 : Preprocessing

Transformation f 1 aims at merging transitions t 1 , . . . , t k into one transition (q , ψ , Eq(P ) , q ), where ψ = ({ψ 1 , . . . , ψ k }). It consists of two steps.

In the first step, transformation f 1 replaces dcs on transitions of α = (Q , P , -→ , ı) with Eq(P ), as follows. Because α is an original ca (our current code generator can handle only original ca), every sc in α is an original sc: for every transition label (ψ , φ), a set of ports P + exists such that cp(P , P + ) ≡ ψ. Now, for every product in disjunctive normal form (dnf) of φ, transformation f 1 constructs a graph with vertices P + and an edge (p 1 , p 2 ) for every d(p 1 ) = d(p 2 ) literal. Because cp(P , P + ) ≡ ψ, if the resulting graph is connected, the product of the d(p 1 ) = d(p 2 ) literals is equivalent to Eq(P ). Thus, f 1 replaces every transition label (ψ , φ) in α with an equivalent label (ψ , φ ), where φ denotes the modified dnf of φ, with Eq(P ) for every product of d(p 1 ) = d(p 2 ) literals if those literals induce a connected graph. Let α denote the resulting ca. We can prove that α ∼ α holds (see Lemma 16 in [11, Appendix A]).

In the second step, transformation f 1 merges, for every pair of states (q , q ), all transitions from q to q labeled by dc φ into one new transition. (The individual transitions differ only in their sc.) Every resulting transition has as its sc the sum of the scs of the individual transitions. Figure 6 shows examples. We denote the resulting ca by f 1 (α). The following proposition holds, because choices between individual transitions in α are encoded in f 1 (α) by sum-scs of merged transitions. Consequently, α and f 1 (α) can simulate each other's steps.

Proposition 1. f 1 (α) ∼ α 5 Transformation f 2 :

Constructing Hypergraphs

Every merged transition resulting from the previous preprocessing transformations can perhaps be implemented using queues along the same lines as transformation h (see Section 3). In the first place, this depends on the extent to which ports in a merged transition are indistinguishable: no indistinguishable ports means no queues. Second, the sc of a merged transition should make port indistinguishability (i.e., queues), if present, apparent and mechanically detectable. The scs of transitions in f 1 (α) fail to do so. For instance, we (hence a computer) cannot directly derive from the syntax of sc AZBC + BZAC + CZAB in Figure 6b that its transition has a scalable implementation with queues. In contrast, the equivalent sc ({A , B , C}) • Z makes this much more apparent. From this sc, we can "obviously" (and mechanically by transformation g 2 in Figure 4c) conclude that ports A, B, and C may share the same queue, from which exactly one element is dequeued per firing, because they are indistinguishable indeed: intuitively, if δ |= sc ({A , B , C}) • Z, we cannot know which one of A, B, or C holds, unless we inspect δ. Thus, beside automatically detecting indistinguishable ports in a transition, to actually reveal them as queues, we additionally need an algorithm for syntactically manipulating that transition's sc. We formulate both these aspects in terms of a per-transition hypergraph [START_REF] Bretto | Hypergraph Theory: An Introduction[END_REF]. Working with hypergraph representations simplifies our reasoning about, and manipulation of, scs modulo associativity and commutativity. We compute hypergraphs as follows.

Let α = (Q , P , -→ , ı) be an original ca as before, and let (q , ψ , φ , q ) be a (merged) transition in f 1 (α). Because α is an original ca and by the construction of f 1 (α), we know that ψ is a sum of P -complete products of ports (e.g., Figure 6). Because every single port p is equivalent to ({p}), transformation f 2 can represent ψ as a set E of sets E of sets V : E represents the outer sum, every E represents a P -complete product (E includes/excludes every positive/negative port), and every V represents an inner exclusive sum. For instance, {{{A} , { Z}} , {{B} , {Z}} , {{C} , {Z}}} represents the sc of the transition in Figure 6b. Transformation f 2 considers E as the set of hyperedges of a hypergraph over the set of vertices ℘(Port(ψ)), where Port(ψ) denotes the ports occurring in ψ (i.e., every vertex is a set of ports). Formally, f 2 computes a function graph. Let Graph denote the set of all hypergraphs with sets of ports as vertices. Fig. 7: Hypergraphs for the transitions of the ca in Figure 6 (The side condition states just that ψ is a sum of P -complete products of ports.) Figure 7 shows example hypergraphs (without unconnected vertices).

We define the meaning of a hypergraph as a sum of products of exclusive sums, where every product corresponds to a hyperedge. Such a product consists of exclusive sums of positive ports (one for each vertex in the hyperedge), and it consists of negative ports (one for every port outside the vertices in the hyperedge). We can show that graph is an isomorphism (i.e., graph(ψ) is a sound and complete representation of ψ). In summary, transformation f 2 computes graph for every merged transition in f 1 (α) and stores each of those graphs in a set Γ (indexed by transitions).

Hypergraphs as introduced are generic representations of synchronization patterns, isomorphic to but independent of scs in ca. This reinforces that our optimization approach, transformation f , is not tied ca but a generally applicable technique when relevant context information is available.

Transformation f 3 : Manipulating SCs

Transformation f 3 aims at making all indistinguishable ports (hence queues) in scs on (merged) transitions in f 1 (α) apparent by analyzing and manipulating the hypergraphs in Γ , computed by transformation f 2 . It consists of two steps.

In the first step, transformation f 3 computes the indistinguishable ports under every transition t = (q , ψ , φ , q ) in f 1 (α). We call the ports in a set I indistinguishable under t if for every distribution δ such that δ |= sc ψ and |I ∩ Dom( δ)| = 1, we cannot deduce from δ| P \I which particular port in I is satisfied by δ.

An example appeared in the first paragraph of Section 5. In an implementation with a queue shared among the ports in I, this means that whenever t fires, we know that exactly one port in I participated in the transition but not which one, even if we know all other participating ports (i.e., those outside I).

By analyzing hypergraph γ t ∈ Γ for the sc ψ of t, transformation f 3 computes maximal sets of indistinguishable ports under t (larger sets of indistinguishable ports means larger queues means better scalability), as follows. Recall from Section 5 that γ t represents a sum (hyperedge relation) of P -complete products (hyperedges) of singleton exclusive sums (vertices). To understand how port indistinguishability displays in γ t , suppose that ports p 1 , p 2 ∈ P are indistinguishable, and let δ be a distribution such that δ |= sc γ t . Because γ t 's hyperedge relation E represents a sum of P -complete products, exactly one hyperedge E ∈ E exists such that δ satisfies E P . Then, because |{p 1 , p 2 }∩Dom(δ)| = 1, a vertex V ∈ E exists such that p 1 ∈ V or p 2 ∈ V . 8 In fact, because every hyperedge consists of singleton vertices, either {p 1 } ∈ E or {p 2 } ∈ E. Now, by inspecting δ| P \{p1,p2} , we can infer the other vertices in E, beside either {p 1 } or {p 2 }. Let E denote this set of vertices, and observe that either

E = E 1 = E {{p 1 }} or E = E 2 = E {{p 2 }}.
Because both options are possible, E necessarily includes both E 1 and E 2 , and importantly, E 1 and E 2 are equal up to p 1 and p 2 .

Generalizing this example from {p 1 , p 2 } to arbitrarily sized sets I, informally, the ports in I are indistinguishable if every port in I is involved in the same hyperedges as every other port in I up to occurrences of ports in I. The following definitions make this generalization formally precise. First, we introduce a function Edge that determines for a port p which hyperedges in E include p. (In fact, Edge(p , E) contains all such hypergedges up to occurrences of vertices with p.) Then, we define a function that computes maximal sets of ports with the same set Edge(p , E). Importantly, yields a partition of the set of ports in vertices connected by E, denoted by Port(E). Henceforth, we therefore call every maximal set of indistinguishable ports computed by a part.

Definition 3. Edge : Port × ℘ 2 (Ver) → ℘ 2 (Ver) denotes the function from port, set of hyperedges -pairs to sets of hyperedges defined as:

Edge(p , E) = {W | W = E \ {V } and p ∈ V ∈ E ∈ E} Definition 4. : ℘ 2 (Ver) → ℘ 2 (Port)
denotes the function from sets of hyperedges to sets of sets of ports defined as:

(E) = {P | P ∈ ℘ + (Port(E)) and p ∈ P iff T = Edge(p , E) for all p } Lemma 1. (Lemma 12 in [11, Appendix A]) 1.
(E) = Port(E) 2. P 1 = P 2 and P 1 , P 2 ∈ (E) implies P 1 ∩ P 2 = ∅ 8 Otherwise, if p1 , p2 / ∈ V for all V ∈ E, the P -complete product represented by E contains p 1 and p 2 such that δ |= sc p1 and δ |= sc p2. This contradicts the assumption

|{p1 , p2} ∩ Dom(δ)| = 1, which implies either δ |= sc p1 or δ |= sc p2. Edge(A , E) = {{{Z}}} Edge(B , E) = {{{Z}}} Edge(C , E) = {{{Z}}} Edge(Z , E) = {{{A}} , {{B}} , {{C}}} (E) = {{A , B , C} , {Z}} (a) Merger3 Edge(A , E) = {{{H} , {Y}} , {{H} , {Z}}} Edge(B , E) = {{{H} , {Y}} , {{H} , {Z}}} Edge(H , E) = {{{A} , {Y}} , {{A} , {Z}} , {{B} , {Y}} , {{B} , {Z}}} Edge(Y , E) = {{{A} , {H}} , {{B} , {H}}} Edge(Z , E) = {{{A} , {H}} , {{B} , {H}}} (E) = {{A , B} , {H} , {Y , Z}} (b) Hourglass
Fig. 8: Maximal sets of indistinguishable ports of the hypergraphs in Figure 7 In summary, in the first step, transformation f 3 computes maximal sets of indistinguishable ports in every merged transition t = (q , ψ , φ , q ) by applying to hyperedge relation E in hypergraph γ t for ψ. Figure 8 shows examples.

In the second step, f 3 manipulates E of every hypergraph γ t such that afterward, every vertex in every hyperedge in E is a part in (E). Importantly, every vertex V ∈ E ∈ E such that V ∈ (E) represents not just any -formula but one of indistinguishable ports. Consequently, in the meaning of the manipulated γ t , indistinguishable ports become apparent as inner -formulas as in the example in the first paragraph of Section 5.

For manipulating hyperedge relation E, we introduce an operation that combines two combinable hyperedges into one in a semantics-preserving way. Roughly, we call two distinct hyperedges

E 1 , E 2 ∈ E combinable if we can select disjoint vertices V 1 , V 2 ∈ E 1 ∪ E 2 such that E 1 and E 2 are equal up to inclusion of V 1 and V 2 . We denote this property as (E 1 , V 1 ) E (E 2 , V 2 )
. Applied to combinable hyperedges E 1 and E 2 , operation removes E 1 and E 2 from E and adds their combination

E † = {V 1 ∪ V 2 } ∪ (E 1 ∩ E 2
) to E. Formally, we have the following. Let Ver denote the set of all vertices. Definition 5. ⊆ (℘(Ver) × Ver) × (℘(Ver) × Ver) × ℘ 2 (Ver) denotes the relation on tuples consisting of two sets of hyperedge, vertex -pairs and a set of hyperedges defined as:

(E 1 , V 1 ) E (E 2 , V 2 ) iff   E 1 , E 2 ∈ E and E 1 = E 2 and V 1 ∩ V 2 = ∅ and E 1 = (E 2 \ {V 2 }) ∪ {V 1 } and E 2 = (E 1 \ {V 1 }) ∪ {V 2 }   Definition 6. : (℘(Ver) × Ver) × (℘(Ver) × Ver) × ℘ 2 (Ver)
℘ 2 (Ver) denotes the partial function from tuples consisting of two hyperedge, vertexpairs and a set of hyperedges to sets of hyperedges defined as:

(E 1 , V 1 ) E (E 2 , V 2 ) = E \ {E 1 , E 2 }) ∪ {{V 1 ∪ V 2 } ∪ (E 1 ∩ E 2 )} if (E 1 , V 1 ) E (E 2 , V 2 ) Lemma 2. (Lemma 8 in [11, Appendix A]) (E 1 , V 1 ) E (E 2 , V 2 ) implies (V , E) ≡ sc (V , (E 1 , V 1 ) E (E 2 , V 2 ))
Transformation f 3 uses operation in the algorithm for combining hyperedges in Figure 9. Essentially, as long as vertices V 1 and V 2 exist such that the while (X , V1) E (Y , V2) and V1 ∪ V2 ⊆ P and P ∈ (E)

for some X , Y , V1 , V2 , P do while (E1 , V1) E (E2 , V2) for some E1 , E2 do E := (E1 , V1) E (E2 , V2) Fig. 9: Algorithm for combining hyperedges

A H Y B Z =⇒ A H Y B Z Y, Z =⇒ A H B Y, Z =⇒ H A, B Y, Z
Fig. 10: Evolution of the hypergraphs in Figure 7b ports in V 1 ∪ V 2 are indistinguishable (as computed by ), the algorithm combines all combinable hyperedges that include V 1 and V 2 . For instance, Figure 10 shows the evolution of the hypergraph in Figure 7b during the run of the algorithm in which it first selects Y and Z as V 1 and V 2 and afterward A and B. (In another run, the algorithm may change this order to obtain the same result.) Let E in and E out denote the sets of hyperedges before and after running the algorithm. To consider the algorithm correct, E out must satisfy two properties: it should represent an sc equivalent to the sc represented by E in (i.e., the algorithm is semantics-preserving), and every vertex in every hyperedge in E out should be a part in (E in ) (i.e., the algorithm effectively reveals indistinguishability). We use Hoare logic to prove these properties [START_REF] Hoare | An Axiomatic Basis for Computer Programming[END_REF][START_REF] Apt | Verification of Sequential and Concurrent Programs[END_REF]. In particular, we can show that the triple {Pre} A {Post} holds, where A denotes the algorithm in Figure 9. Precondition Pre states that γ t = (V , E in ) is a hypergraph (for the sc of transition t) such that every port in a connected vertex inhabits at most one connected vertex, and such that every connected vertex is nonempty. The definition of graph in Definition 1 implies these conditions. (However, because its precondition is more liberal, the algorithm is more generally applicable.) The postcondition Post states that correctness as previously formulated holds. Formally:

(V , E out ) = (V , E in ) and E ∈ E out implies E ⊆ (E in )
for all E

Figure 11 shows the algorithm annotated with assertions for total correctness. By the axioms and rules of Hoare logic, this proof is valid if we can prove that for all six pairs of consecutive assertions, the upper assertion implies the lower one. For brevity, below, we discuss some salient aspects. First, the algorithm terminates, because (i) every iteration of the outer loop consists of at least one iteration of the inner loop, for X = E 1 and Y = E 2 , (ii) in every iteration of the inner loop, E decreases by one, and (iii) E is finite. Second, the algorithm is semantics-preserving by Lemma 2. The main challenge is proving that the algorithm is also effective. A notable step in this proof is establishing the property labeled Interm from Inv 2 (the invariant of the inner 11: Algorithm for combining hyperedges with assertions for total correctness loop) and not Cond 2 (the negation of the inner loop's condition). Informally, Interm states that if F denotes the hyperedge relation before running the inner loop, we have E = F \ (F 1,2 ) ∪ F † after running the inner loop. Here, F 1,2 contains all hyperedges from F that include V 1 or V 2 , while F † denotes all new hyperedges added by during the loop. This property subsequently enables us to prove Inv 1 (the invariant of the outer loop), which among other properties states (E in ) = (E). Consequently, to prove the algorithm's effectiveness, it suffices to show that E ∈ E out implies E ⊆ (E out ) (for all E).

Theorem 2. (Theorem 4 in [11, Appendix A]) {Pre} A {Post}

In summary, in the second step, for every (merged) transition t = (q , ψ , φ , q ) in f 1 (α), transformation f 3 manipulates hypergraph γ t to γ t by running the algorithm in Figure 9, given the maximal sets of indistinguishable ports computed in f 3 's first step with . Afterward, f 3 replaces ψ in t with γ t , which by the correctness of the algorithm is equivalent to γ t and has made indistinguishable ports (hence queues) apparent. We denote the resulting transition relation by (f 3 •f 1 )(-→) and the resulting ca by (f 3 •f 1 )(α). Because ψ ≡ sc γ t ≡ sc γ t for all transitions t in f 1 (α), the following proposition follows from Lemma 16 in [11, Appendix A]. Together, Propositions 1 and 2 imply that transformation f is semantics-preserving.

Proposition 2. (f 3 • f 1 )(α) ∼ f 1 (α)
We end with some examples in Figure 12. Transformation f 3 has not had any effect on the LossySync ca, so its implementation does not benefit from queues (no indistinguishable ports), as expected. The Merger 3 and Hourglass ca, in contrast, have changed significantly. In the sc of Merger 3 , we can now clearly recognize one queue for ports A, B, and C and one queue for port Z (cf. transformation h in Section 3); similarly, in the sc of Hourglass, we can now clearly recognize one queue for ports A and B and one queue for ports Y and Z.

AB , Eq({A , B}) AB , (a) LossySync ({A , B , C}) • Z , Eq({A , B , C , Z}) (b) Merger3 ({A , B}) • H • ({Y , Z}) , Eq({A , B , H , Y , Z}) (c) Hourglass
Fig. 12: Application of transformation f 3 to the ca in Figure 6 Applied to Merger 3 , transformation f optimizes a multiple-producer-singleconsumer protocol. More abstractly, in this case, f optimizes a protocol among two groups of processes, X 1 (producers) and X 2 (consumer), such that |X 1 | = 3 and |X 2 | = 1 and all processes in X 1 are indistinguishable to all processes in X 2 and vice versa. Generally, f can optimize protocols among n groups of processes X 1 , . . . , X n such that for all 1 ≤ i , j ≤ n, all processes in X i are indistinguishable to all processes in X j and vice versa. For instance, applied to Hourglass, f optimizes a protocol among three groups of processes such that

|X 1 | = |X 3 | = 2 and |X 2 | = 1.
After having applied transformation f , the automatic generation of actual implementations is straightforward (i.e., transformation g 2 in Figure 4c). The resulting code is, in fact, exactly the same as the code that results from manually applying transformation h as in Section 3 (and consequently, it has the same performance): instead of checking an event structure for every port as preoptimized code does, optimized code checks one eventQueue structure for every maximal set of indistinguishable ports, which transformation f has made explicit as -formulas in scs (and are thus easy to detect in the f -transformed ca). As such, optimized code checks the sc of all transitions in the pre-transformation ca that differ only in indistinguishable ports (before applying f ) at the same time. For k such transitions, consequently, an unscalable exhaustive O(k) search is optimized to perfectly scalable O(1) queue operations. Thus, with respect to Figure 4c, the fully mechanical transformation g

2 • f = g 2 • f 3 • f 2 • f 1
yields the same code and scalability as the partially manual transformation h • g 1 .

Concluding Remarks

In this paper, we analyzed scalability issues of the code generated by our Reoto-C compiler, we explained a manual solution, and we studied the various steps of a mechanical procedure for transforming a ca α to an equivalent ca β, which makes port indistinguishability (hence queues) maximally apparent, using the -operator. Our tool can use this mechanical procedure to generate code for α via β with good scalability. In particular, whereas unoptimized code generated for α requires O(k) time to compute eligibility of k transitions-essentially an exhaustive search-the optimized code generated for β requires only O(1) time: all maximal sets of indistinguishable ports (explicit in β as a -formulas in scs) in the implementation share the same queue, which optimizes the unscalable O(k) search to perfectly scalable O(1) queue operations.

Although inspired by our work on a Reo compiler and formulated generally in terms of ca, we make contributions beyond Reo and ca. The synchronization pattern that we identified and optimized is common and occurs in many classes of protocols and their implementation, regardless of the particular language. Therefore, compilers for other high-level languages may use the same approach as explained in this paper to similarly optimize code generated for programs in those languages. In fact, this paper led to adding new features to Proto-Runtime to enable our optimization technique, thereby facilitating efficient implementation of our f -transformed ca. Importantly, these new features in Proto-Runtime can now benefit other languages implemented on top of Proto-Runtime as well.

Automatically performing our optimization directly on low-level code such as C (instead of on ca) is extremely complex, if not impossible. This shows that using higher-level languages (that preserve relevant context information about protocols) for multicore programming can indeed be advantageous for performance, a significant general observation in language and compiler design for multicore platforms. Indeed, the work presented in this paper serves as evidence that it is possible not only to specify interaction protocols at a higher level of abstraction (than locks, mutex, semaphores, message exchanges, etc.) but also automatically compile and optimize such high-level specifications down to executable code. Such higher-level specifications convey more of the intention behind the protocol, which gives more room for a compiler/optimizer to find and apply efficient implementation alternatives. Lower-level, more imperative, specifications of interaction protocols either lose or obscure the intentions behind protocols and seriously constrict the ability of compilers/optimizers to find efficient implementation alternatives. See [START_REF] Jongmans | Automata-based Optimization of Interaction Protocols for Scalable Multicore Platforms[END_REF] for related work on high-level approaches to multicore programming.

This paper makes primarily conceptual and theoretical contributions, and we used performance figures only to motivate and explain the development of our optimization technique. An in-depth study of the use of this technique in practice, including more benchmarks and experiments with different kinds of protocols and contexts, is our next objective, now that we know that the technique is correct. As part of this future work, we will also extend our current, limited proof-of-concept implementation (used in obtaining the data for Figure 5) to a full implementation. We end with the following remarks. Indistinguishability of data. Transformation f effectively merges transitions with labels of the form (ψ , Eq(P )). The reason is that the ports in Eq(P ) are indistinguishable from a data perspective. (Whether those ports are also indistinguishable in ψ is exactly what transformation f 3 investigates.) Detecting port indistinguishability in arbitrary dcs so as to improve the applicability of f seems an interesting and important future challenge.

Guarded automata. Our scs, as arbitrary propositional formulas, seem similar to guards on transitions in the guarded automata used by Bonsangue et al.

for modeling connector behavior [START_REF] Bonsangue | A model of context-dependent component connectors[END_REF]. The intuitive meaning of such guards, however, significantly differs: guards specify a constraint on the environment, while scs specify a constraint on an execution step. (In fact, transition labels of guarded automata carry both a guard and an sc.)

Model-based testing. We skipped an explanation of the actual code generation process (i.e., transformation g 2 in Figure 4), dismissing it as "straightforward" and "obviously correct". An interesting line of work to better substantiate the latter statement is to have our tool generate not only executable code but also test cases derived from the input ca. Kokash et al. have already worked on such model-based testing for ca in a different context [START_REF] Kokash | Input-output Conformance Testing for Channel-based Service Connectors[END_REF].

Fig. 1 :

 1 Fig. 1: Producers-consumer benchmark

Fig. 2 :

 2 Fig. 2: Example ca, called LossySync, Merger 3 and Hourglass

p

  ::= any element from Port Ψ ::= any set of scs a ::= 0 | 1 | p ψ ::= a | ψ | ψ + ψ | ψ • ψ | (Ψ ) (a) Synchronization constraints p ::= any element from Port P ::= any subset of Port b ::= ⊥ | | Eq(P ) | d(p) = d(p) φ ::= b | ¬φ | φ ∨ φ | φ ∧ φ (b) Data constraints

Fig. 3 :

 3 Fig. 3: Syntax

[ 7 ]Fig. 4 :

 74 Fig. 4: Code generation diagrams

  Execution time in thousands of cycles (b) Without barrier

f

  --→ β into a number of constituent transformations α f1 --→ β f2 --→ (β , Γ ) f3 --→ β, discussed in detail in the following sections.

Definition 1 .

 1 graph : SC Graph denotes the partial function from scs to hypergraphs defined as: 7 graph(ψ) = (℘(Port(ψ)) , E E = {V | V = {p} and p ∈ P + } and P + ⊆ Port(ψ) and P + ∈ P )if ψ = ( ψ ψ ≡ sc cp(Port(ψ) , P + ) and P + ⊆ Port(ψ) and P + ∈ P ) for some P

Definition 2 .

 2 • : (℘(Ver) × ℘(Port)) ∪ Graph → SC denotes the function from hyperedge, set of ports -pairs and hypergraphs to scs defined as: E P = ({ψ | ψ = (V ) and V ∈ E} ∪ {ψ | ψ = p and p ∈ P \ ( E)}) (V , E) = ({ψ | ψ = E V and E ∈ E}) Theorem 1. (Theorem 3 in [11, Appendix A]) ψ ≡ graph(ψ)

  V1) E (Y , V2) and V1 ∪ V2 ⊆ P and P ∈ (E) for some X , Y , V1 , V2 , P do Inv1 and Cond1 and |E| = z1 Inv2 while (E1 , V1) E (E2 , V2) for some E1 , E2 do Inv2 and Cond2 and |E| = z2 Inv2[E := (E1 , V1) E (E2 , V2)] and (|E| < z2)[E := (E1 , V1) E (E2 , V2)] E := (E1 , V1) E (E2 , V2) Inv2 and |E| < z2 Inv2 and not Cond2 Inv2 and Interm and |E| < z1 Inv1 and |E| < z1 Inv1 and not Cond1 Post

Fig.

  Fig. 11: Algorithm for combining hyperedges with assertions for total correctness

Programmers can use the Ect plugins for Eclipse (http://reo.project.cwi.nl) to draw connectors such as the one in Figure1a, internally represented as Xml.

The LossySync ca models a connector with one input port A and one output port B. It repeatedly chooses between two atomic execution steps (constrained by availability of pending i/o operations): synchronous flow of data from A to B or flow of data only on A (after which the data is lost, before reaching B). The Merger3 ca models a connector with three input ports A, B, and C and one output port Z. It repeatedly chooses between three atomic execution steps: synchronous flow of data from A to Z, from B to Z, or from C to Z. Finally, the Hourglass ca models a connector with two input ports A and B, one internal port H, and two output ports Y and Z. It repeatedly chooses between four atomic execution steps: synchronous flow of data from A via H to Y, from A via H to Z, from B via H to Y, or from B via H to Z.

We show only single state ca for simplicity. Generally, a ca can have any finite number of states, and the results in this paper are applicable also to such ca.

Enhancing Scalability: Problem and SolutionWe study the scalability of code generated by our compiler using Figure

We start with Figure4a, which summarizes the code generation process of our current tool: given an original ca α (computed for the connector to generate code for), it generates a piece of code alpha by applying transformation g 1 .Essentially, alpha consists of an event-driven handler, which simulates α. This handler runs concurrently with the code of its environment (i.e., the code of the entitites under coordination), whose events (i.e., i/o operations performed on ports) it listens and responds to, as follows. Whenever the environment performs an i/o operation on a port p, it assigns a representation of that operation to an event variable in a data structure for p (also generated by transformation g 1 and part of alpha). This causes the handler to start a new round of simulating α. Based on the state of α that the handler at that point should behave as, the handler knows which transitions of α may fire. Which of those transitions actually can fire, however, depends also on the pending events that previously occurred (i.e., the pending i/o operations on ports). To investigate this, the handler checks for every transition that may fire if the pending events (including the new one) can constitute a distribution δ that satisfies the transition's label. If so, the handler fires the transition: it distributes data over ports according to δ, and the events involved dissolve. Otherwise, if no transition can fire, all events remain for the next round, and the handler goes dormant.

To be precise, the ca in Figure2bdescribes the behavior of one of the synchronous regions of the connector in Figure1a(i.e., a particular subconnector of the whole). This point is immaterial to our present discussion, however, and ignoring it simplifies our presentation without loss of generality or applicability.

The growth is more-than-linear instead of just linear because of the barrier in the protocol. When producer P is ready to send its (i + 1)-th production, the consumer may not yet have received the i-th production from all other producers. Then, P must wait until the consumer signals ready (i.e., the barrier). In the worst case, however, the consumer has received an i-th production only from P such that P has to wait (k -1) • O(k) time. Afterward, it takes another O(k) time for P to send its (i + 1)-th production. Consequently, sending the (i + 1)-th production takes k • O(k) time, and the complexity of sending a production lies between O(k) and O(k 2 ).


Benjamin Morandi

Sebastian Nanz

Bertrand Meyer

Safe and Efficient Data Sharing for Message-Passing Concurrency

Message passing provides a powerful communication abstraction in both distributed and shared memory environments. It is particularly successful at preventing problems arising from shared state, such as data races, as it avoids sharing in general. Message passing is less effective when concurrent access to large amounts of data is needed, as the overhead of messaging may be prohibitive. In shared memory environments, this issue could be alleviated by supporting direct access to shared data; but then ensuring proper synchronization becomes again the dominant problem. This paper proposes a safe and efficient approach to data sharing in message-passing concurrency models based on the idea of distinguishing active and passive computational units. Passive units do not have execution capabilities but offer to active units exclusive and direct access to the data they encapsulate. The access is transparent due to a single primitive for both data access and message passing. By distinguishing active and passive units, no additional infrastructure for shared data is necessary. The concept is applied to SCOOP, an object-oriented concurrency model, where it reduces execution time by several orders of magnitude on data-intensive parallel programs.

Introduction

In concurrency models with message passing, such as the Actor model [START_REF] Hewitt | A universal modular ACTOR formalism for artificial intelligence[END_REF], CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], and others [START_REF] Coulouris | Distributed Systems: Concepts and Design[END_REF], a computational unit encapsulates its own private data. The units interact by sending synchronous or asynchronous messages. These concurrency models are implementable in environments with and without shared memory. Based on these models, several languages and libraries support message passing, e.g., Erlang [START_REF]Erlang/OTP system documentation[END_REF], Ada [16], MPI [START_REF]Message Passing Interface Forum: MPI: A message-passing interface standard[END_REF], and SCOOP [START_REF] Nienaltowski | Practical framework for contract-based concurrent objectoriented programming[END_REF].

To operate on shared data, a client must send a message to the supplier encapsulating that data. In environments with shared memory, however, the client could access this data directly and avoid the messaging overhead. The difficulty is to prevent data races and to combine the data access primitives with the messaging primitives in a developer-friendly way.

Some languages and libraries [START_REF]Erlang/OTP system documentation[END_REF]16,[START_REF]Message Passing Interface Forum: MPI: A message-passing interface standard[END_REF][START_REF] Schill | Handling parallelism in a concurrency model[END_REF] have already combined mutually exclusive shared data with message passing and observed performance gains on shared memory systems. However, as discussed in Section 6, these approaches either impose restrictions on the shared data or do not provide unified primitives for data access and message passing. As a consequence of the latter limitation, programmers are required to change their code substantially when switching from messaging to shared data or vice versa.

To close this gap, this paper proposes passive computational units for safe and efficient data sharing in message-passing models implemented on shared memory. A passive unit is a supplier stripped from its execution capabilities. Its only purpose is to provide a container for shared data and exclusive access to it. The passive unit can contain any data that is containable by a regular supplier. A client with exclusive access uses existing communication primitives to operate on the data; instead of sending a message, these primitives access the data directly. By overloading the primitives' semantics, programmers only need to change few lines of code to set a unit passive. Furthermore, passive units are implementable with little effort as existing supplier infrastructure can be reused.

This paper develops this concept in the context of SCOOP [START_REF] Meyer | Object-Oriented Software Construction[END_REF][START_REF] Nienaltowski | Practical framework for contract-based concurrent objectoriented programming[END_REF], an objectoriented concurrency model based on message passing, where processors encapsulate objects and interact by sending requests. The implementation of the concept is shown to reduce execution time by several orders of magnitude on data-intensive parallel programs.

The remainder of this paper is structured as follows. Section 2 introduces a running example. Section 3 develops the concept of passive processors informally, and Section 4 develops it formally. Section 5 evaluates the efficiency, and Section 6 reviews related work. Finally, Section 7 discusses the applicability to other concurrency models and concludes with an outlook on future work.

Pipeline System

A pipeline system serves as the running example for this paper. The pipeline parallel design pattern [START_REF] Mattson | Patterns for Parallel Programming[END_REF] applies whenever a computation involves sending packages of data through a sequence of stages that operate on the packages. The pattern assigns each stage to a different computational unit; the stages then synchronize with each other to process the packages in the correct order. Using this pattern, each stage can be mapped for instance to a CPU core, a GPU core, an FPGA, or a cryptographic accelerator, depending on the stage's computational needs.

The pipeline pattern can be implemented in SCOOP (Simple Concurrent Object-Oriented Programming) [START_REF] Meyer | Object-Oriented Software Construction[END_REF][START_REF] Nienaltowski | Practical framework for contract-based concurrent objectoriented programming[END_REF]. The starting idea of SCOOP is that every object is associated with a processor, called its handler. A processor is an autonomous thread of control capable of executing actions on objects. An object's class describes its actions as features. An entity x belonging to a processor can point to an object with the same handler (non-separate object), or to an object on another processor (separate object). In the first case, a feature call x.f on the target x is non-separate: the handler of x executes the feature synchronously. In the second case, the feature call is separate: the handler of x, i.e., the supplier, executes the call asynchronously on behalf of the requester, i.e., the client. The possibility of asynchronous calls is the main source of concurrent execution. The asynchronous nature of separate feature calls implies a distinction between a feature call and a feature application: the client logs the call with the supplier (feature call) and moves on; only at some later time will the supplier actually execute the body (feature application).

In the SCOOP pipeline implementation, each stage and each package is handled by its own processor, ensuring that stages can access the packages in parallel. Each stage is numbered to indicate its position in the pipeline; it receives this position upon creation: The process feature takes a package as an argument. The keyword separate specifies that the package may be handled by a different processor than the stage; without this keyword, the package must be handled by the same processor. To ensure exclusive access, a stage must first lock a package before accessing it. In SCOOP, such locking requirements are expressed in the formal argument list: any target of separate type within the feature must occur as a formal argument; the arguments' handlers are locked for the duration of the feature execution, thus preventing data races. In process, package is a formal argument; hence the stage has exclusive access to the package while executing process.

To process each package in the right order, the stages must synchronize with each other. For this purpose, each package has two features is processed and set processed to keep track of the stages that already processed the package. The synchronization requirement can then be expressed elegantly using a precondition (keyword require), which makes the execution of a feature wait until the condition is true. The precondition in process delays the execution until the package has been processed by the previous stage.

The SCOOP concepts require execution-time support, known as the SCOOP runtime. Each processor is protected through a lock and maintains a request queue of requests resulting from feature calls of other processors. When a client executes a separate feature call, it enqueues a separate feature request to the supplier's request queue. The supplier processes the feature requests in the order of queuing. A non-separate feature call can be processed without the request queue: the processor creates a non-separate feature request and processes it right away using its call stack.

A client makes sure that it holds the locks on all suppliers before executing a feature. At the end of the feature execution, the client issues an unlock request to each locked processor. Each locked processor unlocks itself as soon as it processed all previous feature requests.

Passive Processors

The pipeline system from Section 2 showcases an important class of concurrent programs, namely those that involve multiple processors sharing data. In SCOOP, it is necessary to assign the data to a new processor. For frequent and short read or write operations this becomes problematic:

1. Each feature call to the data leads to a feature request in the request queue of the data processor, which then picks up the request and processes it on its call stack. This chain of actions creates overhead. For an asynchronous write operation, the overhead outweighs the benefit of asynchrony. For a synchronous read operation, the client not only waits for the data processor to process the request, it also gets delayed further by the overhead. 2. The data consumes operating system resources (threads, processes, locks, semaphores) that could otherwise be freed up.

On systems with shared memory, the clients can directly operate on the data, thus avoiding the overhead. This frees most of the operating system resources attached to the data processor. Before accessing shared data, a client must ensure its access is mutually exclusive; otherwise, data races can occur. For this purpose, shared data must be grouped, and each group must be protected through a lock.

Since SCOOP processors offer this functionality already along with execution capabilities, one can use processors, stripped from their execution capabilities, to group and protect shared data. This insight gives rise to passive processors:

Definition 1 (Passive processor). A passive processor q does not have any execution capabilities. Its lock protects the access to its associated objects. A client p holding this lock uses feature calls to operate directly on q's associated objects. While operating on these objects, p assumes the identity of q. Processor q becomes passive when another processor sets it as passive. When q is not passive, it is active. Processor q becomes active again when another processor sets it as active. It can only become passive or active when unlocked, i.e., when not being used by any other processor.

When a processor p operates on the objects of a passive processor q, it assumes q's identity. For example, if p creates a literal object or another nonseparate object, it creates this object on q and not on itself; otherwise, a nonseparate entity on q would reference an object on p.

Besides safe and fast data sharing, passive processors have further benefits:

-Minimal user code changes. The feature call primitive unifies sending messages to active processors and accessing shared data on passive processors, ensuring minimal code changes to set a processor passive or active. With respect to SCOOP's type system [START_REF] Nienaltowski | Practical framework for contract-based concurrent objectoriented programming[END_REF], the same types can be used to type objects on passive and active processors. The existing type system rules ensure that no object on a passive processor can be seen as non-separate on a different processor, thus providing type soundness. -Minimal compiler and runtime changes. To implement passive processors, much of the existing infrastructure can be reused. In particular, no new code for grouping objects and for locking request queues is required.

package processor (active) Fig. 1: A stage processor processes a package. The stage object, handled by the left-hand side processor, has a separate reference (depicted by an arrow) to the package object, handled by the right-hand side processor. The package object references a non-separate record object to remember the processing history.

In the pipeline system, each package can be handled by a passive processor rather than an active one. To achieve this, it suffices to set a package's processor passive after its construction. The following code creates a package on a new passive processor and asks the stages to process the package.

No other code changes are necessary. The existing feature calls to the packages automatically assume the data access semantics. Furthermore, a stage can still use separate PACKAGE as the type of a package because the stage is still handled by a different processor than the package. Similarly, a package can still use the type RECORD for its record because the package still has the same handler as the record.

Figure 1 illustrates the effect of the call to set passive. In Figure 1a, active package processors have a call stack, a request queue, and a stack of locks. The stage processors send asynchronous (see put) and synchronous (see item) feature requests. In Figure 1b, passive package processors do not have any execution capabilities. Therefore, the stage processors operate directly and synchronously on the packages, thus making a better use of their own processing capabilities rather than relaying all operations to the package processors.

Formal Specification

This section provides a structural operational semantics for the passive processor mechanism and shows that setting a processor passive or active preserves the execution order of called features.

State Formalization Let Ref be the type of references, let Proc be the type of processors, and let Entity be the type of entities. A state σ is then a 6-tuple (σ h , σ l , σ o , σ i , σ f , σ e ) of functions: σ f : Proc → Proc maps each processor p to the handler of the object on which p currently operates. Normally σ f (p) = p, but when operating on the objects of a passive supplier q, then σ f (p) = q. σ e : Proc → Stack [Map[Entity, Ref ]] maps each processor to its stack of entity environments.

Execution Formalization An execution is a sequence of configurations. Each configuration of the form p 1 :: Figure 2 shows the transition rules. A processor q becomes passive when a processor p executes the set passive instruction (see Set Passive) with an entity e that evaluates to a reference r on q. Processor q becomes active again when a processor p executes the set active instruction (see Set Active). Processor q can only become passive or active when q is unlocked, guaranteeing that q is not being used by any other processor.

s p1 | . . . |
To perform a feature call e t .f (e a ) (see call rules) a client p evaluates the target (see r t ) and the arguments (see r a ). It then looks at the handler q of the target. If q is different from p and not passive, p creates a feature request (see apply) and appends it to the end of q's request queue. If q is p or if q is passive, then p itself immediately processes the feature request.

To process a feature request (see Apply), a processor p first determines the missing locks q as the difference between required locks and already obtained locks. It only proceeds when all missing locks are available, in which case it obtains these locks. It also adds a new entity environment and updates σ f with the target handler, i.e., p for non-passive calls or the handler of the target for passive calls. Processor p then executes the feature body and cleans up (see Revert). It releases the obtained locks, restores σ f , and removes the top entity environment. The locked suppliers unlock themselves asynchronously once they are done with the issued workload (see Unlock).

To execute a creation instruction create e t .f (e a ) (see creation rules), a processor p looks at the type of the target e t . If the type is separate, i.e., its declaration has the separate keyword, p creates an active and idle processor q with a new object referenced by r t . It then locks that processor, performs the creation call (see call rules), and cleans up. If the type of e t is non-separate, i.e., no separate keyword, p creates a new object on the handler on whose objects p currently operates on, i.e., σ f (p). In case σ f (p) = q = p, it is important to create the new object on q rather than on p; otherwise the non-separate entity e t on q would point to an object not on q, thus compromising the soundness of the type system.

We embedded the transition rules from Figure 2 into the comprehensive formal specification for SCOOP [START_REF]SCOOP executable formal specification repository[END_REF], implemented in Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF]. This specification = σe(p).top.val (ea) q = σ h (rt) p = q ∨ σi(q) p :: et.f (ea); sp, σ → p :: apply(rt, f, ra); sp, σ

Apply q def = σ h (ra) \ (σo(p).flat ∪ {p}) q∈q ¬σ l (q) p :: apply(rt, f, ra); sp, σ → p :: f.body; revert(q, σ f (p), true); sp, (σ h , σ l [q → true], σo[p → σo(p).push(q)], σi, Fig. 2: Transition rules uses σ f (p) also in other situations where p performs an action on behalf of a passive processor, namely to create literals, to set the status of a once routine (a routine only executed once), and to import and copy object structures. We used the specification to test [START_REF] Morandi | Prototyping a concurrency model[END_REF] the passive processor mechanism against other SCOOP aspects and used the results to refine the specification.

σ f [p → σ h (rt)],
::, (σ h [rt → q], σ l [q → true], σo[p → σo(p).push({q})][q → ()], σi[q → false], σ f [q → q], σe[p → σe(p).update(et → rt)][q → ()]) Non-

Order Preservation

The formal semantics can be used to prove Theorem 1, stating that a supplier can always be set passive or active without altering the sequence in which called features get applied. This property enables developers to use the same reasoning in determining a feature's functional correctness, irrespective of whether the suppliers are passive or active. Lemma 1 is necessary to prove Theorem 1.

Lemma 1 (Action queue order preservation). Let p be a processor with statements s 1 , . . . , s l in its action queue. In a terminating program, p will execute s 1 , . . . , s l in the sequence order.

Proof. The transition rules in Figure 2 only allow p to execute the leftmost statement and then continue with the next one. Since none of the rules delete or shuffle any statements, and since p's program is terminating, p must execute s 1 , . . . , s l in the sequence order.

Theorem 1 (Feature call order preservation). Let p be a processor that is about to apply a feature f in a terminating program. Let q be the processors that p locks to apply f . For each q ∈ q, regardless whether it is passive or active, the feature requests for q, resulting from feature calls in f 's body, will be processed in the order given by f 's body.

Proof. Processor p first inserts f 's instructions s 1 , . . . , s l into its action queue (see Apply). Lemma 1 states that processor p executes all of these instructions in code order. Hence, the proof can use mathematical induction over the length l of f 's body. In the base case, i.e., l = 0, p did not execute any instructions; hence, the property holds trivially. For the inductive step, the property holds for l = i -1; the proof needs to show that the property holds for l = i. Consider the instruction s i at position i:

s i is set passive or set active. Processor p does not change any action queues (see Set Passive and Set Active); the property is preserved. s i is a separate feature call to a passive processor q. Processor p processes the resulting feature request (see Non-Separate/Passive Call). Processor q must already have been passive during earlier calls because a processor cannot be set passive when it is locked (see Apply and Set Passive). Hence, processor p must have processed all requests from earlier calls. Because of the induction hypothesis, it must have done so in the order given by the code. Consequently, processing the request for s i now preserves the property for q. Because of the induction hypothesis, the configuration after s i-1

satisfied the property for all other suppliers in q; Lemma 1 guarantees that these processors will execute their statements in the same order even after s i , thus the property is preserved. s i is a separate feature call to an active processor q. Processor q must already have been active during earlier calls because a processor cannot be set active when it is locked (see Apply and Set Active). Processor p executes a separate call (see Separate Call) to add a feature request to the end of q's action queue. Because of the induction hypothesis, q must either have processed all requests from earlier calls in the code order, or some of these requests must be scheduled in q's action queue, to be executed in code order. In either case, adding a feature request for s i to the end of the action queue preserves the property for q (see Lemma 1). As in the passive case, Lemma 1 guarantees that the property is preserved for all other suppliers in q as well. s i is a non-separate feature call. Regardless of the suppliers' passiveness, p executes a non-separate feature call (see Non-Separate/Passive Call). Lemma 1 guarantees that the property is preserved for all q in q. s i is a separate creation instruction. Regardless of the suppliers' passiveness, p executes a separate feature call (see Separate Creation), adding a new feature request to a new processor. Lemma 1 guarantees that the property is preserved for all q in q. s i is a non-separate creation instruction. Regardless of the supplier's passiveness, p executes a non-separate feature call (see Non-Separate Creation). Lemma 1 guarantees that the property is preserved for all q in q.

5 Evaluation

The pipeline system from Section 2 is a good representative for the class of programs targeted by the proposed mechanism: multiple stages share packages of data. This section experimentally compares the performance of the pipeline system when implemented using passive processors, active processors, and low-level synchronization primitives; the latter two are the closest competing approaches.

To this end, we extended the SCOOP implementation [9] with passive processors.

Comparison to Active Processors

A low-pass filter pipeline is especially suited because it exhibits frequent and short read and write operations on the packages, each of which represents a signal to be filtered. The pipeline has three stages: the first performs a decimation-intime radix-2 fast Fourier transformation [START_REF] Jones | Decimation-in-time (DIT) radix-2 FFT[END_REF]; the second applies a low-pass filter in Fourier space; and the third inverses the transformation. The system supports any number of pipelines operating in parallel and splits the signals evenly. Table 1 shows the average execution times of various low-pass filter systems processing signals of various lengths. The experiments have been conducted on a 4 × Intel Xeon E7-4830 2.13 GHz server (32 cores) with 256 GB of RAM running Windows Server 2012 Datacenter (64 Bit) in a Kernel-based Virtual Machine on Red Hat 4.4.7-3 (64 Bit). A modified version of EVE 13.11 [9] compiled the programs in finalized mode with an inline depth of 100. Every data point reflects the average execution time over ten runs processing 100 signals each. Using ten pipelines, it took nearly ten hours to compute the average for active signals of length 16384; thus we refrained from computing data points for bigger lengths. Fig. 3: The speedup of passive processors over active processors Figure 3 visualizes the data. The upper three curves belong to the active signal processors. The lower curves result from the passive processors and a sequential execution. As the graph indicates, the passive processors are more than two orders of magnitude faster than the active ones. In addition, with increasing number of pipelines, the passive processors become faster than the sequential program. In fact, two pipelines are enough to have an equivalent performance. The overhead is thus small enough to benefit from an increase in parallelism. In contrast, active processors deliver their peak performance with around five pipelines but never get faster than the sequential programs.

Comparison to Low-Level Synchronization Primitives

Figure 4 and Table 1 compare pipelines with passive processors to pipelines based on low-level synchronization primitives. In the measured range, the passive processors are between 3.7 to 5.4 times slower. As the signal length increases, the slowdown tends to becomes smaller. With more pipelines, the slowdown also tends to decrease at signal lengths above 8192. The two curves for sequential executions show that a slowdown can also be observed for non-concurrent programs. The slowdown is the consequence of SCOOP's programming abstractions. Compare the following thread-based stage implementation to the SCOOP one from Section 2. Besides the addition of boilerplate (inherit clause, redefinition of execute), this code exhibits some more momentous differences. First, the threadbased stage class implements a work queue: it has an attribute to hold the packages and a loop in execute to go over them. In SCOOP, request queues provide this functionality. Second, each thread-based package has a mutex and a condition variable for synchronization. To process a package, stage i first locks the mutex and then uses the condition variable to wait until stage i -1 has processed the package. Once stage i -1 is done, it uses the condition variable to signal all waiting stages. Only stage i leaves the loop. In SCOOP, wait conditions provide this kind of synchronization off-the-shelf. We expect the cost of wait conditions and other concepts to drop further as the implementation matures.

Other Applications

A variety of other applications could also profit from passive processors. Object structures can be distributed over passive processors. Multiple clients can thus operate on dynamically changing but distinct parts of these structures while exchanging coordination messages. For example, in parallel graph algorithms, the vertices can be distributed over passive processors. In producer-consumer programs, intermediate buffers can be passive. Normally, about half of the operations in producer-consumer programs are synchronous read accesses. Without the messaging overhead, the consumer can execute these operations much faster than the buffer. Passive processors can also be useful to handle objects whose only purpose it is to be lockable, e.g., forks of dining philosophers, or to encapsulate a shared state, e.g., a robot's state in a controller.

Several languages and libraries combine shared data with message passing. In Ada [16], tasks execute concurrently and communicate during a rendezvous: upon joining a rendezvous, the client waits for a message from the supplier, and the supplier synchronously sends a message to the client. The client joins a rendezvous by calling a supplier's entry. The supplier joins by calling accept on that entry. To share data, tasks access protected objects that encapsulate data and provide exclusive access thereon through guarded functions, procedures, and entries. Since functions may only read data, multiple function calls may be active simultaneously. In contrast, passive processors do not support multiple readers. However, unlike protected objects, passive processors do not require new data access primitives. Furthermore, passive processors can become active at runtime.

Erlang [START_REF]Erlang/OTP system documentation[END_REF] is a functional programming language whose concurrency support is based on the actor model [START_REF] Hewitt | A universal modular ACTOR formalism for artificial intelligence[END_REF]. Processes exchange messages and share data using an ets table, providing atomic and isolated access to table entries. A process can also use the Mnesia database management system to group a series of table operations into an atomic transaction. While passive processors do not provide support for transactions, they are not restricted to tables.

Schill et al. [START_REF] Schill | Handling parallelism in a concurrency model[END_REF] developed a library offering indexed arrays that can be accessed concurrently by multiple SCOOP processors. To prevent data races on an array, each processor must reserve a slice of the array. Slices support fine-grained sharing as well as multiple readers using views, but they are restricted to indexed containers. For instance, distributed graphs cannot be easily expressed.

A group of MPI [START_REF]Message Passing Interface Forum: MPI: A message-passing interface standard[END_REF] processes can share data using the remote memory access mechanism and its passive target communication. The processes collectively create a window of shared memory. Processes access a window during an epoch, which begins with a collective synchronization call, continues with communication calls, and ends with another synchronization call. Synchronization includes fencing and locking. Locks can be partial or full, and they can be shared or exclusive. Passive processors neither offer fences nor shared locks; they do, however, offer automatic conditional synchronization based on preconditions. MPI can also be combined with OpenMP [START_REF]OpenMP Architecture Review Board: OpenMP application program interface[END_REF]. Just like MPI alone, this combination does not provide unified concepts. Instead, it provides distinct primitives to access shared data and to send messages. Uniformity also distinguishes passive processors from further approaches such as [START_REF] Gustedt | Data handover: Reconciling message passing and shared memory[END_REF].

Several studies agree that performance gains can be realized if the setup of a program with both message passing and shared data fits the underlying architecture. For instance, Bull et al. [START_REF] Bull | Performance evaluation of mixed-mode OpenMP/MPI implementations[END_REF] and Rabenseifner et al. [START_REF] Rabenseifner | Hybrid MPI/OpenMP parallel programming on clusters of multi-core SMP nodes[END_REF] focus on benchmarks for MPI+OpenMP. Dunn and Meyer [START_REF] Dunn | Parallel QR factorization for hybrid message passing/shared memory operation[END_REF] use a QR factorization algorithm that can be adjusted to apply only message passing, only shared data, or both.

A number of approaches focus on optimizing messaging on shared memory systems instead of combining message passing with shared data. Gruber and Boyer [START_REF] Gruber | Ownership-based isolation for concurrent actors on multicore machines[END_REF] use an ownership management system to avoid copying messages between actors while retaining memory isolation. Villard et al. [START_REF] Villard | Proving copyless message passing[END_REF] and Bono et al. [START_REF] Bono | Typing copyless message passing[END_REF] employ static analysis techniques to determine when a message can be passed by reference rather than by value. Buntinas et al. [START_REF] Buntinas | Implementation and evaluation of sharedmemory communication and synchronization operations in MPICH2 using the Nemesis communication subsystem[END_REF], Graham and Shipman [START_REF] Graham | MPI support for multi-core architectures: Optimized shared memory collectives[END_REF], as well as Brightwell [START_REF] Brightwell | Exploiting direct access shared memory for MPI on multi-core processors[END_REF] present techniques to allocate and use shared memory for messages.

Conclusion

Passive processors extend SCOOP's message-passing foundation with support for safe data sharing, reducing execution time by several orders of magnitude on data-intensive parallel programs. They are useful whenever multiple processors access shared data using frequent and short read or write operations, where the overhead outweighs the benefit of asynchrony. Passive processors can be implemented with minimal effort because much of the existing infrastructure can be reused. The feature call primitive unifies sending messages to active processors and accessing shared data on passive processors. Therefore, no significant code change is necessary to set a processor passive or active. This smooth integration differentiates passive processors from other approaches. The concept of passive computational units can also be applied to other message-passing concurrency models. For instance, messages to passive actors [START_REF] Hewitt | A universal modular ACTOR formalism for artificial intelligence[END_REF] can be translated into direct, synchronous, and mutually exclusive accesses to the actor's data.

Passive processors currently do not offer shared read locks, which allow multiple clients to simultaneously operate on a passive processor. Shared read locks require features that are guaranteed to be read-only. Functions could serve as a first approximation since they are read-only by convention. Further, passive processors are not distributed yet. Because frequent remote calls are expensive, implementing distributed passive processors requires an implicit copy mechanism to move the supplier's data into the client's memory.

class

  STAGE create make feature position: INTEGER --The stage's position in the pipeline. make (new position: INTEGER) --Create a stage at the given position. do position := new position end process (package: separate PACKAGE) --Process the package after the previous stage is done with it. require package.is processed (position -1) do do work (package) --Read from and write to the package. package.set processed (position) --Set the package processed. end end

-

  σ h : Ref → Proc maps each reference to its handler. σ l : Proc → Boolean indicates which processors are locked. σ o : Proc → Stack [Set[Proc]] maps each processor to its obtained locks. σ i : Proc → Boolean indicates which processors are passive.

=

  σe(p).top.val (e) q def = σ h (r) ¬σ l (q) p :: set passive(e); sp, σ → p :: sp, (σ h , σ l , σo, σi[q → true], σ f , σe)Set Active r def = σe(p).top.val (e) q def = σ h (r) ¬σ l (q) p :: set active(e); sp, σ → p :: sp, (σ h , σ l , σo, σi[q → false], σ f , σe) Separate Call rt def = σe(p).top.val (et) ra def = σe(p).top.val (ea) q = σ h (rt) p = q ∧ ¬σi(q) p :: et.f (ea); sp | q :: sq, σ → p :: sp | q :: sq; apply(rt, f, ra), σ Non-Separate/Passive Call rt def = σe(p).top.val (et) ra def

Fig. 4 :

 4 Fig. 4: The slowdown of passive processors over EiffelThread

class

  STAGE inherit THREAD create make feature position: INTEGER --The stage's position in the pipeline. packages: ARRAY[PACKAGE] --The packages to be processed. make (new position: INTEGER; new packages: ARRAY[PACKAGE]) --Create a stage at the given position to operate on the packages. do position := new position ; packages := new packages end execute --Process each package after the previous stage is done with it. do across packages as package loop package.mutex.lock --Lock the package. --Sleep until previous stage is done; release the lock meanwhile. from until package.is processed (position -1) loop package.condition variable.wait (package.mutex) end process (package) --Process the package. package.condition variable.broadcast --Wake up next stage. package.mutex.unlock --Unlock the package. end end process (package: PACKAGE) --Process the package. do do work (package) --Read from and write to the package package.set processed (position) --Set the package processed. end end

  p n :: s pn , σ is an execution snapshot consisting of the schedule, i.e., the call stacks and the request queues of processors p 1 , . . . , p n , and the state σ. The call stack and the request queue of a processor are also known as the action queue of the processor. The commutative and associative parallel operator | keeps the processors' action queues apart. Within an action queue, a semicolon separates statements. Statements are either instructions, i.e., program elements, or operations, i.e., runtime elements. The following overview shows the structure of statements, instructions, and operations. The elements e t , e, and all items in e a are entities of type Entity. The element r t and all items in r a are references of type Ref . The element f of type Feature denotes a feature where f.body returns the feature's body. Lastly, q 1 , . . . , q n and w are processors of type Proc, and x is a flag of type Boolean.

	s in | op
	in
	et.f (ea) |	Call a feature.
	create et.f (ea) |	Create an object.
	set passive(e) |	Set the handler of the referenced object passive.
	set active(e)	Set the handler of the referenced object active.
	op
	apply(rt, f, ra) |	Apply a feature.
	revert({q1, . . . , qn}, w, x) |	Finish a feature application or an object creation.
	unlock	Unlock a processor.

Table 1 :

 1 Average execution times (in seconds) of various low-pass filter systems with various signal lengths.

	configuration		2048 4096	8192 16384 32768 65536 131072 262144 524288
	sequential, SCOOP		1.00 1.66	3.22	6.35 12.71 26.19 55.05 120.37 272.38
	sequential, thread		0.62 1.09	2.19	4.66 9.57 20.23 41.45 93.40 213.59
	1 pipeline, active	337.55 682.29 1456.67 2875.23	-	-	-	-	-
	1 pipeline, passive		1.64 2.72	5.02 10.99 24.68 55.29 118.30 247.29 533.83
	1 pipeline, thread		0.31 0.58	1.16	2.44 5.26 11.11 23.59 53.24 122.00
	2 pipelines, passive		1.19 1.77	3.05	6.35 14.19 29.82 60.24 124.99 263.96
	3 pipelines, passive		1.07 1.47	2.34	4.71 9.87 20.65 41.78 85.72 185.19
	5 pipelines, active 231.25 496.68 1048.95 2192.53	-	-	-	-	-
	5 pipelines, passive		0.87 1.23	1.86	3.27 6.35 13.50 27.17 55.95 117.12
	5 pipelines, thread		0.16 0.23	0.40	0.74 1.53 3.05	6.30 13.76 31.82
	10 pipelines, active 334.93 726.83 1549.01 3322.70	-	-	-	-	-
	10 pipelines, passive 0.84 1.08	1.38	2.36 4.13 8.28 16.89 35.13 76.64
	10 pipelines, thread		0.16 0.22	0.33	0.59 1.08 2.09	4.26	9.21 20.93
		1000
	average	100
	execution time (s)
		10
		1
		2048	4096	8192	16384	32768	65536		131072	262144	524288
							signal length
			1 pipeline, active		5 pipelines, active	10 pipelines, active
			sequential		1 pipeline, passive	2 pipelines, passive
			3 pipelines, passive		5 pipelines, passive	10 pipelines, passive

create package.make (data, number of stages) ; set passive (package) stage 1.process (package) ; ... ; stage n.process (package)

Acknowledgments

We thank Eiffel Software for valuable discussions on the implementation. The research leading to these results has received funding from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC Grant agreement no. 291389.