Hernán Melgratti

Christian Roldán

A Formal Analysis of the Global Sequence Protocol

The Global Sequence Protocol (GSP) is an operational model for replicated data stores, in which updates propagate asynchronously. We introduce the GSP-calculus as a formal model for GSP. We give a formal account for its proposed implementation, which addresses communication failures and compact representation of data, and use simulation to prove that the implementation is correct. Then, we use the GSP-calculus to reason about execution histories and prove ordering guarantees, such as read my writes, monotonic reads, causality and consistent prefix. We also prove that GSP extended with synchronous updates provides strong consistency guarantees.

Introduction

Cloud infrastructures provide data storages that are virtually unlimited, elastic (i.e., scalable at run-time), highly available and partition tolerant. This is achieved by replicating data over multiple servers. A client may perform update and read operations over any of these replicas and the store is responsible for keeping them synchronised. However, it is known (CAP theorem [START_REF] Gilbert | Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services[END_REF]) that any system cannot simultaneously provide availability, partition tolerance, and consistency. Thus, one of these properties has to be discarded. Today's popular data storages, such as Dynamo [START_REF] Decandia | Dynamo: amazon's highly available key-value store[END_REF] and Cassandra [START_REF] Lakshman | Cassandra: a decentralized structured storage system[END_REF], ensure availability and offer weaker notions of consistency, called eventual consistency. Roughly, eventual consistency guarantees that all updates will be delivered to the different replicas, which will eventually converge to the same state [START_REF] Bailis | Eventual consistency today: limitations, extensions, and beyond[END_REF]. The storages adopt different strategies to achieve eventual consistency, which impact on the guarantees provided by the system, i.e., on the kind of inconsistencies or anomalies that are allowed to happen. For instance, a storage may resolve automatically conflicts introduced be concurrent updates (e.g., by using timestamps or causality) or may leave the problem to applications that read the database (like in Cassandra). In this way, the consistency model supported by a data store becomes crucial when writing applications.

Consequently, there has been a growing interest on establishing programming abstractions to help developers to deal with eventual consistent stores. For instance, commutative replicated data types [START_REF] Shapiro | Conflict-free replicated data types[END_REF] and cloud types [START_REF] Burckhardt | Cloud types for eventual consistency[END_REF] provide programmers with suitable data type abstractions that encapsulate issues related to eventual consistency. Recent proposals advocate declarative approaches for programming with eventual consistency, e.g., to automatically select the consistency level required from a store provided with a consistency contract for the application [START_REF] Sivaramakrishnan | Declarative programming over eventually consistent data stores[END_REF] or to prove that a given consistency level is adequate for preserving some data invariant [START_REF] Gotsman | Cause i'm strong enough: reasoning about consistency choices in distributed systems[END_REF]. With similar aims, the Global Sequence Protocol (gsp) [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF] proposes an operational model to reason about applications running on top of replicated stores. Basically, the state of a store is represented as the sequence of updates that have led to it. Clients have their own copy of the state which they operate upon: each read and write operation has immediate effect over the local state and the system propagates changes to make all replicas consistent using a reliable total order broadcast protocol (rtob). The rtob protocol guarantees that all messages are delivered in the same total order to all clients. Replicas rely on the order generated by rtob to converge to the same state. In the very basic model, called core gsp, each client interacts with its local state by performing read and write operations. Albeit simple, this model introduces some subtleties when programming because it does not ensure read stability (i.e., two successive reads may return different values) nor atomicity of several updates (i.e., another client may partially observe the effects of a sequence of updates). To overcome these limitations, three synchronisation primitives, namely pull, push and confirmed, allow programmers to control the propagation of changes. It has been shown that this model can be implemented so to handle communication failures and to represent updates efficiently by using two type of objects: states and deltas. Both models, i.e. the idealised one and its implementation, have been defined in terms of a reference implementation.

In this paper, we propose a formal account for each model: the gsp and igsp calculi ( § 2 and § 3). We prove that the behaviour of a program running over igsp can be observed over the idealised model. Technically, we show that each igsp system can be simulated by the corresponding gsp system ( § 4). Then, we study and prove the consistency guarantees ensured by gsp. We rely on the characterisation of consistency guarantees in terms of abstract histories proposed in [START_REF] Burckhardt | Principles of eventual consistency[END_REF]. Abstract histories capture the visibility relation between actions and the arbitration order of updates in the system. Then, a wide-spectrum of consistency models can be characterised in terms of these two relations. In § 5, we show how to operationally associate abstract histories to concrete computations and prove that gsp enjoys properties such as Monotonic Read, Causal Visibility and Consistent prefix, among others. Finally, in § 6 we study the extension of gsp with synchronous write operations, which ensures strong consistency.

Global Sequence Protocol Calculus

Syntax

Clients interact with a store by performing operations in U ∪ R: an element in U denotes an update operation, while one in R stands for a read operation. No operation can simultaneously read and update a store, therefore we assume U ∩ R = ∅. We write u, u , u , . . . for updates and r, r , r , . . . for reads. The state of a store is represented by a sequence of updates. For technical convenience (particularly in § 5), we distinguish different executions of the same operation. Formally, stores associate each update with a fresh event identifier.

We assume a set V of event identifiers v, v 0 , . . . , v ,. . . and write u v for the update u associated with the event v.

We use u to denote sequences of decorated updates and u for an atomic block of updates. We write b for a sequence of blocks. We denote the empty sequence with and use the usual operations on sequences such as b[i] to denote the i-th element of b, b[i..j] for the subsequence of b from position i to j, |b| for its length and b \ b for the relative complement of b in b . Additionally, b stands for the plain sequence of updates in b (i.e., without any separation in blocks).

We rely on the countable sets X of program variables x, x , . . . and I of client identifiers i, i , . . . , i 1 , . . .. Definition 2.1 (GSP Language). The set of gsp terms is given by the grammar in Fig. 1.

A gsp system N consists of a store and zero or more clients. The global store S is completely defined by its state, which consists of a sequence of blocks. The term P, u T , b S , b P , k, j i stands for a client identified by i and engaged on the execution of the program P . The remaining elements are used to describe the state of the local replica: u T contains the updates that have been made locally and are part of an unfinished block; b S models the communication buffer, which keeps all blocks completed by the client but not received by the global store; b P is the pending buffer, which contains all completed blocks that are unconfirmed by the global store. For simplicity, we do not have an explicit replica of the global store in each client; we use instead a natural number k to indicate the portion of the global state that is known to the client. Specifically, the client i knows the sequence S[0..k -1]. Similarly, j indicates the number of updates received by the client that have not been added to the local replica, i.e., the client has received the updates contained in the segment S[k..k + j -1].

A program P is built as a sequence of operations that interacts with the store: read(r), update(u), pull, push, confirmed (we postpone their description until § 2.2). A program let x = . . . in P introduces a bound variable whose scope is P . The definition of free variables of a program is standard. We say that a process P is closed when it does not contain free variables. We keep the language for programs simple. We remark that this choice does not affect the results presented in this paper. Actually, we could just have characterised the behaviour of programs as a labelled transition system, but we prefer to have a syntax throughout the presentation.

Definition 2.2 (Well-formedness). A gsp system N = C 0 || . . . ||C m ||S where C l = P l , u Tl , b Sl , b Pl , k l , j l i l for all l ∈ {0, . . . , m} is well-formed if the follow- ing conditions hold 1. i l = i l for all l = l ; 2. k l + j l ≤ |S| for all l; 3. b Pl = u 1 • • • u p • b Sl and for all 1 ≤ x < y ≤ p there exists x , y s.t. S[x ] = u x , S[y ] = u y and k l ≤ x < y ; and 4. u = S • b S0 • • • b Sm • u T0 • • • u Tm , if u[x] = u v , u[y] = u v and x = y then v = v .
We require identifiers to univocally identify clients (1) and every local state to be consistent with the global store, i.e., a client can see at most every message in the store (2), all unconfirmed blocks in b Pl are either in the communication buffer b Sl or in the unseen part of the global store u 1 • • • u p (3). Moreover, an event identifier is associated with a unique update in the system (4). Hereafter, we assume every gsp system to be well-formed.

Operational Semantics

The operational semantics of gsp is given by a labelled transition system over well-formed terms, quotiented by the structural equivalence ≡ defined as the least equivalence such that || is associative, commutative and has 0 as neutral element. The set of actions is given by the following grammar:

λ ::= τ | rd(r) | wr(u v ) | pull | push | cfm
As usual, τ stands for an internal, unobservable action, while the remaining ones correspond to the interaction of a client with the store. A label (λ, i) indicates that the client i performs the action λ. We write

λ -→ i instead of (λ,i) ---→.
We now comment on the inference rules in Fig. 2. When a client performs an update (rule update), the change has only local effects: the sequence of local updates u T is extended with the operation u decorated with a globally fresh identifier v. We remark that decorations are used for technical reasons but they are operationally irrelevant (see § 5).

A client propagates its local changes to the global store by executing push (rule push): all local changes in u T will be transmitted as a block u T , i.e., as an atomic unit. Nevertheless, these changes are not made available immediately The received update is not immediately added to the local replica. Actually, each client explicitly refreshes its local view by executing pull (rule pull). At this time, all previously received updates j are incorporated to the local copy (i.e., k is changed to k + j). Additionally, all pending updates in the new fragment S[k..k + j -1] are remove from b P . The semantics of operations is defined abstractly by the interpretation function rvalue : R × U * → V, i.e., a function that takes a read operation and a sequence of updates and returns a value in some domain V. A read operation r is evaluated over the local state of the client (rule read), i.e., the known prefix of the global store S[0..k -1] and the local updates in b P and u T . The value v is bound to the variable x, and hence all free occurrences of x in the continuation P are substituted by v. A client may perform confirmed to check whether its executed updates are already in the global store: this operation returns true only when the local buffers b P and u T are both empty (rule confirm).

(update) v fresh update(u); P, u T , b S , b P , k, j i || N wr(u v ) ----→ i P, u T • u v , b S , b P , k, j i || N (push) push; P, u T , b S , b P , k, j i || N push ---→ i P, , b S • u T , b P • u T , k, j i || N (send) P, u T , u T • b S , b P , k, j i || C || S τ -→ i P, u T , b S , b P , k, j i || C || S • u T (receive) k + j < |S| P, u T , b S , b P , k, j i || C || S τ -→ i P, u T , b S , b P , k, j + 1 i || C || S (pull) pull; P, u T , b S , b P , k, j i || C||S pull --→ i P, u T , b S , b P \ S[k..k + j -1], k + j, 0 i || C||S (read) rvalue(r, S[0..k -1] • b P • u T ) = v let x = read(r) in P, u T , b S , b P , k, j i || C||S rd(r) ---→ i P {v/x}, u T , b S , b P , k, j i || C||S (confirm) v = (b P • u T == ) let x = confirmed in P, u T , b S , b P , k, j i || N cfm --→ i P {v/x}, u T , b S , b P , k, j i || N
We remark that the operational semantics preserves well-formedness. The gsp model describes an idealised system that abstracts away from several implementation details, such as non-optimised representation of the state and unreliable communication. This section presents a formal model for the implementation proposed in [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF].

Syntax

The implementation of gsp relies on a compact representation for states and updates. Their precise definition highly depends on the datatype of the values handled by the store, but they are characterised in terms of two abstract types: State and Delta, which provides the following operations [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF]: Constants δ ∅ and ∅ denote the empty elements in their respective types. An object δ ∈ Delta describes the effects of a sequence of updates and is built by either appending an update to an existing delta (append) or combining together several deltas (reduce). Operation read is the interpretation function for operations (i.e., the implementation counterpart of function rvalue( , ) used by the idealised model) and apply corresponds to state transformations.

Clients and the global store exchange δ objects to communicate changes. As each single δ may correspond to several update operations, clients send each δ accompanied by its own identifier and a sequence number n. Precisely, clients send rounds, i.e. triples r = i, n, δ . Differently, the global store sends segments seg = δ, f , in which δ is accompanied by a function f ∈ I → N. In this way, the global store confirms all changes from client i until round f(i). To deal with crashes and recovery, the server may send segments of the form s, f , which communicates a complete state instead of a delta object. Definition 3.1 (GSP Language). The set of igsp terms is given by the grammar in Fig. 3.

As for gsp, a system is composed by a global store S and possibly many clients C. A global store is modelled by a tuple s, f, in s , out s containing a state s, a function f to keep track of processed rounds and the communication buffers in s and out s . There are two dedicated buffers for each client i: in s (i) contains the rounds received from i, and out s (i) the segments that have been sent to i.

A client is represented by a term P, s, δ T , δ P , n, r, in c i . As for gsp, i is its identity and P is its program. Note that the language for programs remains unaltered. The component δ T is analogous to u T in the gsp model, i.e., it keeps all local updates until the client performs push. Differently, δ P keeps all finished blocks that have not been sent. The number n identifies the current round. Buffer r keeps all sent rounds that have not been confirmed by the global store (similar to b P in gsp), while in c keeps all received segments (analogous to j).

We also impose the following well-formedness condition on systems.

Definition 3.2 (igsp well-formedness). A igsp system N = C 0 || . . . ||C m ||S with S = s, f, in s , out s and C l = P l , s l , δ Tl , δ Pl , n l , r l , in cl i l for l ∈ {0, . . . , m} is well-formed if the following conditions hold

1. i l = i l for all l = l . 2. dom(in s ) = dom(out s ) ⊆ {0, . . . , m}. 3. i l ∈ dom(out s ) implies in cl = . 4. if i l ∈ dom(out s ) and in cl • out s (i l ) = then either (i) in cl • out s (i l ) = δ 0 , f 0 • • • δ h , f h ; or (ii) in cl • out s (i l ) = s, f 0 • δ 1 , f 1 • • • δ h , f h and f j (i l ) ≤ f k (i l
) for all j < k ∈ {0..h} and f h = f. 5. r l = i 0 , n 0 , δ 0 • • • i r , n r , δ r , n j < n k for all j < k ∈ {0..r} and either (i) δ Pl = δ ∅ , n r ≤ n l and f(i l ) ≤ n l ; or (ii) δ Pl = δ ∅ , n r < n l and f(i l ) < n l .

either

(i) r l = , f(i l ) ≤ n l and if i l ∈ dom(in s ) then in s (i l ) = ; (ii) r l = in s (i l ) = i l , n fst , δ fst • r l and n fst > f(i l ); (iii) r l = r l • i l , n lst , δ lst • in s (i l ) and in cl • out s (i l ) = δ 0 , f 0 • • • δ lst , f lst with f lst (i l ) = n lst ; or (iv) in s (i l ) = , r l = r l • i l , n lst , δ lst and either in cl •out s (i l ) = s, f •seg with f (i l ) ≤ n lst or in cl • out s (i l ) = and f(i l ) ≤ n lst .
We require all clients to have different identifiers [START_REF] Bailis | Eventual consistency today: limitations, extensions, and beyond[END_REF]. Communication channels in the implementation are bidirectional, hence i l ∈ dom(in s ) iff i l ∈ dom(out s ) (2). Moreover, the input buffer of a disconnected client is empty (3). Condition (4) states that s, f can appear only as the first message in the flow from the store and that the store confirms processed rounds in a non-decreasing order. Similarly, clients send rounds with increasing round number [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF]. The last condition [START_REF] Decandia | Dynamo: amazon's highly available key-value store[END_REF] states a coherence requirement between pending rounds and the segments sent by the store, which can only confirm rounds that are pending.

(i-update) update(u); P, s, δ T , δ P , n, r, inc i || N wr(u v ) ----→ i P, s, append(δ T , u), δ P , n, r, inc i || N (i-push) push; P, s, δ T , δ P , n, r,

inc i || N push ---→ i P, s, δ ∅ , reduce(δ P • δ T ), n + 1, r, inc i || N (i-send) δ P = δ ∅ i ∈ dom(ins) r = i, n, δ P inc • outs(i) = s , f • seg P, s, δ T , δ P , n, r, inc i || s , f, ins, outs || C τ -→ i P, s, δ T , δ ∅ , n, r • r , inc i || s , f, ins[i → ins(i) • r ], outs || C (i-receive) outs(i) = seg • seg P, s, δ T , δ P , n, r, inc i || s , f, ins, outs || C τ -→ i P, s, δ T , δ P , n, r, inc • seg i || s , f, ins, outs[i → seg] || C (i-pull1) r = filter(f k (i), r) inc = δ1, f1 . . . δ k , f k pull; P, s, δ T , δ P , n, r, inc i || N pull --→ i P, apply(s, reduce(δ1 • • • δ k )), δ T , δ P , n, r , i || N (i-read)
read(r, apply(s, ∆(r)

• δ P • δ T )) = v let x = read(r) in P, s, δ T , δ P , n, r, inc i || N rd(r) ---→ i P {v/x}, s, δ T , δ P , n, r, inc i || N (i-confirm) v = (r • δ P • δ T == ) let x = confirmed in P, s, δ T , δ P , n, r, inc i || N cfm --→ i P {v/x}, s, δ T , δ P , n, r, inc i || N (i-batch) δ, f = rnds(ins) δ = δ ∅ s = apply(s, δ) ∀i.(outs (i) = outs(i)• δ, f[f ] ∧ins (i) = ) s, f, ins, outs || C τ -→ s , f[f ], ins , outs || C (i-drop-cxn) i ∈ ins i ∈ outs P, s, δ T , δ P , n, r, inc i || s, f, ins, outs || C τ -→ P, s, δ T , δ P , n, r, i || s, f, ins \ i, outs \ i || C (i-accept-cxn) i / ∈ ins i / ∈ outs s, f, ins, outs || C i || C τ -→ s, f, ins[i → ], outs[i → s, f ] || C i || C (i-pull2) inc = s , f0 • δ1, f1 . . . δ k , f k s = apply(s , reduce(δ ∅ • δ1 • • • δ k )) r = filter(f k (i), r) pull; P, s, δ T , δ P , n, r, inc i || s , f, ins, outs || C pull --→ i P, s , δ T , δ P , n, r , i || s , f, ins[i → ins(i) • r ], outs || C

Operational Semantics

As for the idealised model, the operational semantics is given by a labelled transition system over well-formed terms, up-to structural equivalence. We consider a new label τ without any client annotation for transitions associated with changes in the global store and communication failures. The inference rules are in Fig. 4.

Rule (i-update), which is analogous to rule (update), adds the operation u to the temporary block δ T . The decoration v is irrelevant in this model, hence we do not impose any freshness requirement. A client terminates a block by executing push (i-push). At this time, the block δ T is appended to the already terminated blocks in δ P , which will be sent on the next round. Additionally, the block counter n is incremented by 1. By rule (i-send), a client sends changes to the global store. This transition takes place whenever the client is connected (i.e., i ∈ dom(in s )), there are finished blocks in δ P (i.e., δ P = δ ∅ ) and there is no need for resynchronisation (i.e., in c • out s (i) = s , f • seg) 3 . The available blocks are sent within the same round r = i, n, δ P , which contains the number n corresponding to the last finished block. The new round r is added to the corresponding input buffer in the store, i.e., in s (i) is updated to in s (i) • r (where [ → ] is the update operator for functions). Additionally, r is added to the sequence of pending rounds r and the buffer δ P is reset to δ ∅ . Symmetrically, the client i may receive an available segment at any time (ireceive). The new segment seg is removed from the buffer out s (i) of the global store and added to the input buffer of the client. As for the idealised model, all received changes are applied to the local replica when i performs pull. Rule (i-pull 1 ) handles the case in which the connection with the global store has not been previously reset. In such case, all received segments are of the form δ, f . Therefore, the changes δ 1 • • • δ k are applied to the local state s and all rounds confirmed by the received segments are removed from the pending list r. By well-formedness (Def. 3.2,5), it suffices to consider the confirmation f k , which has the greatest confirmation. Hence, all rounds up-to f k (i) are removed from r. This is done by the auxiliary function filter( , ), defined as follows

filter(n, r) = i, n j , δ j • • • i, n k , δ k if r = i, n 0 , δ 0 • • • i, n j , δ j • • • i, n k , δ k , n j-1 ≤ n and n j > n
Rules (i-read) and (i-confirm) are analogous the ones in the gsp calculus. We use ∆( ) for the function that projects a sequence of rounds into the sequence that contains the corresponding δs. The global store changes its state as prescribed by rule (i-batch): it collects all received rounds in in s by using the auxiliary function rnds( ), which builds a unique object δ by appending all available rounds, and a function f that associates each client with the number of the last received round. Let in s be such that dom(in s ) = {i 0 , . . . , i m } and

∀i l ∈ dom(in s ).in s (i l ) = r l • i l , n k l l , δ k l l .
Then, rnds( ) is defined as follows

We now show that igsp is a correct implementation of gsp by proving that N weakly simulates N when N implements N . We use standard simulation but technically we take into account the fact that gsp associates a fresh event identifier to each update while igsp does not. Take →= τ -→ i∈I τ -→ i , ⇒ as the reflexive and transitive closure of →, i.e.⇒=→ * , and

λ = ⇒ i = ⇒; λ -→ i ; ⇒. Definition 4.2 (Simulation). R is an implementation simulation if for all (N, N ) ∈ R we have: 1. If N wr(u v ) ----→ i N then ∃N , w s.t. N wr(u w ) = === ⇒ i N and (N , N ) ∈ R; 2. If N λ -→ i N and λ = wr(u v ), τ then ∃N s.t. N λ = ⇒ i N and (N , N ) ∈ R; 3. If N - → N then ∃N s.t. N ⇒ N and (N , N ) ∈ R;
As usual, we write N N if there exists a simulation R s.t. (N, N ) ∈ R.

Theorem 4.1. If N implements N , then N N . Proof. We show that R = {(N, N ) | N implements N } is a simulation.
We remark that R -1 is not a simulation because the implementation cannot mimic the behaviour in which a client have completed two consecutive blocks (i.e., two push commands) without sending the first block. In gsp it is still possible to interleave the two blocks with blocks sent by other clients but in igsp they are treated as atomic because they will be sent as a unique δ object.

Consistency Guarantees

In this section we study the consistency properties offered by gsp. We rely on the characterisation of properties in terms of abstract executions [START_REF] Burckhardt | Eventually consistent transactions[END_REF], execution histories enriched with information about visibility and arbitration of actions. Definition 5.1. Let N be a well-formed gsp system, an abstract history for N is a tuple A = N , OP, SS, SO, VIS, AR where:

-OP : V → R ∪ U maps events to operations; -SS : I → V associates events with a session (i.e., a client); -SO ⊆ V × V describes the order of operations within a session; -VIS ⊆ V × V indicates whether the effects of an update are visible to a read; -AR ⊆ V × V resolves concurrent update conflicts.

We write ↓ for function/relation restriction. For a given abstract history A, we write U (similarly, R) for the codomain restriction of OP to U (correspondingly, 1. for all i ∈ dom(SS), SS(i) ⊆ dom(OP); 2. (v, w) ∈ SO then exist i ∈ dom(SS) s.t. {v, w} ∈ SS(i).

R), i.e., U = {v | v ∈ OP, OP(v) ∈ U} (R = {v | v ∈ OP, OP(v) ∈ R}).
3. for all i ∈ dom(SS), SO ↓ SS(i) is a total order; 4. VIS ⊆ U × R; 5. AR ⊆ U × U is a prefix order. The above conditions ensure that events in SS are associated with an operation by OP [START_REF] Bailis | Eventual consistency today: limitations, extensions, and beyond[END_REF]. Besides, SO only relates events belonging to the same session [START_REF] Burckhardt | Principles of eventual consistency[END_REF], which are totally ordered within each session [START_REF] Burckhardt | Cloud types for eventual consistency[END_REF]. Differently from the definition in [START_REF] Burckhardt | Principles of eventual consistency[END_REF], we restrict visibility to keep track of dependencies between updates and read events(4). We do not require AR to be a total order but instead to be a prefix order [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF]. In this way the updates in different replicas are arbitrated when they reach the global store. The remaining two conditions require the abstract history to be consistent with the state of the system.

Rules in Fig. 6 provides an operational way to associate abstract executions with gsp computations. Rules (a-update) and (a-read) add new events to the history and corresponds to the execution of a read or update operation by a client. In both cases OP is extended with a new event v (i.e., v / ∈ dom(OP)), which is associated with the corresponding operation (either r or u). The new event v is added to the corresponding session i, and SO is updated to make v the maximal event for the session i. Rule (a-update) amends AR by capturing the fact that all updates that are already in the global state took place before the new event. Rule (a-read) instead augments VIS with the pairs associating the new event with all events that are seen by the read action, namely, the local view of the global state S[0..k i -1] and the local buffers b Pi and u Ti . Rule (a-arb) handles the changes in the state of the global store (due to a send transition in one client) and amends AR by arbitrating (i) the new events by respecting the relative order in which they are added to the store (i.e., {(v i , v j ) | i, j ∈ {0, . . . , n}, i < j}) and (ii) all updates in the local state of the clients after the new ones (i.e., ({v 0 , . . . , v n } × {w | w ∈ U ∀u.u w ∈ S • u}). The remaining transitions of the system are considered as internal changes that do not affect the history and are handled by rule (a-int). The following example shows that the gsp model exhibits the Dekker anomaly, hence it does not enjoy sequential consistency [START_REF] Burckhardt | Principles of eventual consistency[END_REF].

N wr(u v ) ----→ i N v / ∈ dom(OP) OP = OP[v → u] SS = SS[i → SS(i) ∪ {v}] SO = SO ∪ (SS(i) × {v}) AR = AR ∪ ({w | u w ∈ S} × {v}) N , OP, SS, SO, VIS, AR wr(u v ) ----→ i N , OP , SS, SO , VIS, AR (a-read) N rd(r) ---→ i N v / ∈ dom(OP) OP = OP[v → r] SS = SS[i → SS(i) ∪ {v}] SO = SO ∪ (SS(i) × {v}) VIS = VIS ∪ ({w | u w ∈ S[0..k i -1] • b Pi • u T i } × {v}) N , OP, SS, SO, VIS, AR rd(r v ) ----→ i N , OP , SS , SO , VIS , AR (a-arb) S || C λ -→ i S • u || C λ = wr(u v ), rd(r) u = u0 v0 • • • un vn AR = AR ∪ {(vi, vj) | i, j ∈ {0, . . . ,
Example 5.1 (Dekker anomaly). Consider the following system consisting of two clients and the empty store

N = || C 1 || C 2 where C 1 = update(u 1 ); let y = read(r 1 ) in P, , , , 0, 0 i1 C 2 = update(u 2 ); let y = read(r 2 ) in Q, , , , 0, 0 i2
Since the updates are made locally, none of the clients see the update performed by the other and this is the essence of the Dekker anomaly which is ruled out by strong consistency models like sequential consistency or linearizability.

gsp with atomic updates

In this section we study the atomic updates proposed in [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF]. We extend the language of programs as follows: The execution of a program syncUpd(u); P remains blocked until the update u is performed over the global store. This is achieved by continuously pulling (i.e., a busy-waiting) until the updates are confirmed by global store. In order to provide the formal semantics of the language, we consider the following runtime syntax for programs. The operational semantics for the new primitives is given by the rules in Fig. 2. Rule (sync-upd) rewrites each synchronous update as the sequence consisting of an asynchronous update followed by pull and wait. Processes wait continuously checks whether local changes have been confirmed by the global store. As described by rule (wait), it is implemented as a busy-waiting loop that first checks the local buffers by executing confirmed and then performs the conditional jump x (pull; wait); P . If the condition x is true, then it follows as P otherwise it continues as pull; wait, as described by rules (guard-true) and (guard-false).

Single order is characterised, essentially, by imposing arbitration and visibility to coincide [START_REF] Burckhardt | Principles of eventual consistency[END_REF]. Since our definition for AR and VIS makes them disjoint, we use an alternative characterisation of single order guarantee, which disregards the arbitration order of updates that are not observed. Hence, we use the following characterisation for single order: AR; VIS ⊆ VIS and AR -1 ; ¬VIS ⊆ ¬VIS The following result shows that any well-formed gsp system, whose programs are free from asynchronous updates enjoy the single order guarantee.

Conclusions

We have proposed a formal model for the Global Sequence Protocol and its proposed implementation. We use our formal model to provide a simplified proof (that relies on standard simulation) that the proposed implementation is correct. We remark that our proof does not require to exhibit an auxiliary state for the simulation and that several invariants are trivially ensured by the definition of the model (e.g., the fact that clients have a consistent view of the global sequence) and the well-formed conditions imposed over systems. We have formally studied the consistency guarantees ensured by the model by relying on the operational semantics of the calculus to incrementally compute (a relaxed version of) abstract histories. We have also shown how gsp can be used to formally study programming patterns, like synchronous update operations, that provide stronger consistency guarantees at the expenses of efficiency and availability. We plan to use the gsp calculus as a formal basis for developing programming techniques to enable the fine-tuning of consistency levels in applications.

(Fig. 1 .

 1 naturals) j, k, n ∈ N (update) U = {u, u , . . . , u0, . . .} (read) R = {r, r , . . . , r0, . . .} (event) V = {v, v , . . . , v0, . . .} (var) X = {x, x , . . . , x0, . . .} (ids) I = {i, j, i , . . . , i0, . . .} (upd seq) u ::= | u v • u (block seq) b ::= | u T • b (system) N ::=S || C (store) S ::=b (client) C ::=0 | P, u T , b, b, k, j i | C || C (program) P ::= update(u); P | let x = read(r) in P | pull; P | push; P | let x = confirmed in P Syntax of the gsp calculus

Fig. 2 .

 2 Fig. 2. Operational semantics for gsp

Lemma 2 . 1 .

 21 If N is well-formed and N λ -→ i N , then N is well-formed.

Fig. 3 .

 3 Fig. 3. Syntax of the igsp calculus

  δ ∅ : Delta append : Delta × U → Delta reduce : Delta * → Delta ∅ : State apply : State × Delta * → State read : R × State → V

Fig. 4 .

 4 Fig. 4. Operational semantics of igsp

Definition 5 . 2 (

 52 Well-formed history). Let N = C 0 || . . . ||C m ||S be a gsp system where C l = P l , u Tl , b Sl , b Pl , k l , j l i l . A history A = N , OP, SS, SO, VIS, AR is well-formed if the following conditions hold:

6 .

 6 (v, w) ∈ AR iff -S[i] = u v and S[j] = u w and i < j; or u v ∈ S and u w ∈ b Sl • u Tl ; 7. if b Sl • u Tl [i] = u v and b Sl • u Tl [j] = u w and i < j, then (v, w) ∈ SO and{v, w} ∈ SS(i l ).

Lemma 5 . 1 .

 51 Let A be a well-formed history.If A λ -→ i A , then A is well-formed.We use histories to analyse the ordering guarantees offered by the gsp model. (Due to space limitation, we refer the interested reader to see the characterisations provided in[START_REF] Burckhardt | Principles of eventual consistency[END_REF] Ch. 5]).

Theorem 5 . 1 .

 51 If N , ∅, ∅, ∅, ∅, ∅ -→ * i N , OP, SS, SO, VIS, AR then (1) Read My Writes: SO↓ U×R ⊆ VIS (a-update)

PFig. 7 .

 7 Fig. 7. Semantics of gsp with atomic updates

(

  run-time-program) P ::= . . . | wait; P | e (P ); P

Theorem 6 . 1 (

 61 Single Order). Let N be a well-formed system s.t. update(u) does not appear in N . If N , ∅, ∅, ∅, ∅, ∅ -→ * i N , OP, SS, SO, VIS, AR then AR; VIS ⊆ VIS and AR -1 ; ¬VIS ⊆ ¬VIS.

For simplicity we check re-synchronisation by inspecting buffers instead of explicitly adding the condition channel established used in the implementation.

Acknowledgments We thank the anonymous reviewers of Coordination 2016 for their careful reading of our paper and detailed comments.

Research partially supported by UBACyT project 2014-2017 20020130200092BA.

rnds(in

The obtained δ is applied to the current state s and f is updated with f . In addition, the new segment δ, f[f ] is sent to every connected client, i.e., it is added at the end of every buffer out s (i). The input buffers in s (i l ) are emptied because all received rounds have been processed.

The remaining rules deal with connectivity issues: rule (i-drop-cxn) models a disconnection: the buffers out s (i) and in s (i) are removed from the global store and also the input buffer of i is set to . When the client i (re-)establishes its connection (i-accept-cxn), the store creates the buffers for i and sends a segment containing the current state of the store. Rule (i-pull 2 ) is analogous to (i-pull 1 ), but handles the first pull after a reconnection. The first received segment s , f 0 contains a state instead of a delta object. The client uses s instead of its local state to resynchronise. The application of successive segments is analogous to rule (i-pull 1 ). Moreover, the client resends a round r containing all pending segments lost by the server during the disconnection.

The proposed implementation allows for a server to crash, i.e., to close all communication buffers, but we do not model explicitly this behaviour because it can be obtained by applying rule (i-drop-cxn) several times.

Correctness of the Implementation

We now prove that igsp is a correct implementation of gsp. We recall in Fig. 5 the requirements stated in [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF] for the operations provided by the data types State and Delta. Formally, the relation associates delta and state objects with sequences of updates: δ u (similarly, s u) means that δ (correspondingly, s) is a compact representation of u. Then, it is also assumed that s u implies read(r, s) = rvalue(r, u) for any r. Building on the above relation, we define under which conditions a igsp system is an implementation of a gsp system.

for all l ∈ {0, . . . , m}, and N = C 0 || . . . || C m || S a igsp system such that S = s, f s , in s , out s and C l = P l , s l , δ Tl , δ Pl , n l , r l , in cl i l . We say N implements N if the following conditions hold:

and reduce(∆(out

then δ S[x..x ] and δ S[y..y ] with y ≤ x .

The first three conditions are self-explanatory. Condition (4) states that the pending blocks in b Pl correspond either to rounds in the pending list r l or to blocks ready to be sent, i.e., in δ Pl . By condition [START_REF] Burckhardt | Global sequence protocol: A robust abstraction for replicated shared state[END_REF], if a client is synchronised with the store (i.e., i l ∈ dom(in s ) and in c • out s (i l ) = s , f • seg) then all blocks in the sending list b Sl are either rounds that have been sent, i.e., in in s (i l ), or ready blocks in δ Pl . Condition [START_REF] Decandia | Dynamo: amazon's highly available key-value store[END_REF] establishes the relation between the received messages in both models. Basically, the local replica is complete when there are no segments for the client (i). When the first received segment is a delta object (ii), the content in the input buffer in cl corresponds to the received messages in S[k l ..k l + j l -1] and the the output buffer out s (i l ) contains the updates in the sequence S[k l + j l ..|S| -1]. In the remaining two cases, the first segment contains a state. When the segment is in the input buffer of the client (iii), the received state s corresponds to a prefix of the sequence S whose length lies in between of the updates already received by the client in the idealised model, i.e., S[0..t -1] with k ≤ t ≤ k l + j l , while the remaining conditions are analogous to the previous case. Differently, when the first segment is still on the output buffer of the store (iv), s corresponds to a prefix that contains at least all updates in S already known to the client, i.e., t ≥ k l + j l because the store confirmations are monotonic.

Condition [START_REF] Gilbert | Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services[END_REF] states that in any segment δ, f sent by the store, δ corresponds to a contiguous sequence of updates in S, i.e., S[x..x ]. Moreover, all confirmed rounds are also within the prefix S[0..x ].


Kasper Dokter

Sung-Shik Jongmans

Farhad Arbab

Scheduling Games for Concurrent Systems

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

Introduction

A scheduler of a concurrent application is an algorithm that assigns at any time processes of the application to a set of processors to execute them. The processes in a concurrent application interact with each other, which introduces dependencies amongst them. For example, a consumer process cannot execute if it requires data not yet provided by a producer process. Typically, such dependencies induce extra delays that the scheduler needs to avoid. For specific types of applications, like streaming applications [START_REF] Thies | Streamit: A language for streaming applications[END_REF], formal models exist that are aware of the interactions among their processes. Such models are then used to synthesize schedulers that optimize the execution of their applications with respect to a scheduling goal, such as latency or power consumption [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF][START_REF] Jha | Low power system scheduling and synthesis[END_REF]. For general types of applications, like web servers [START_REF] Crovella | Connection scheduling in web servers[END_REF], no a priori detailed information about the interactions among their constituent processes is available to the scheduler. In such cases, a general-purpose round-robin scheduler is typically used to execute the application on the available processors. However, we cannot expect such schedulers to optimize our scheduling goals, because they cannot anticipate the dependencies among application processes.

In this paper, we propose an interaction-aware scheduling framework that enables scheduler synthesis for generic concurrent applications, by explicitly modelling interactions among processes. In particular, this framework consists of two elements: a novel formal model of concurrent applications and a scheduler synthesis approach built on top of this formal model.

We base our formal model of concurrent applications on constraint automata [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF], a general model of concurrency developed by Baier et al. (originally as a formal semantics for the coordination language Reo [START_REF] Arbab | Puff, the magic protocol[END_REF]). Basically, the idea is to model a concurrent application as a set of constraint automata, one for every process in the application. In this approach, every constraint automaton models the behaviour of a process at the level of its interactions with its environment (i.e., other processes). Using a special composition operator, we obtain a interaction-aware model for the entire concurrent application.

The existing theory of constraint automata focuses on processes and their interactions; it does not yet facilitate modelling the amount of work that processes need to carry out. However, such information is essential for scheduling. In this paper, we therefore extend transition labels in constraint automata with a declarative constraint that describes the work that needs to be done as part of a transition. These job constraints essentially generalize simple weights as in weighted automata [START_REF] Droste | Handbook of weighted automata[END_REF], primarily to support true concurrency in composition. We call the resulting extension of constraint automata work automata, and we extend the composition operator on constraint automata to work automata accordingly. Work automata, then, constitute a formal model of concurrent applications in which both interaction among processes and work inside processes can be expressed, in a compositional and general manner.

Next, we use work automata in our interaction-aware scheduler synthesis. Given a formal model of a concurrent application as a set of work automata, our interaction-aware scheduler synthesis approach consists of two steps. In the first step, we use our composition operator on work automata to construct a work automaton for the entire concurrent application. The resulting work automaton models exactly the work of each process and the dependencies between the work. In the second step, we model the scheduler synthesis problem as a token game on a graph played between the scheduler and the application. The scheduler assigns the processes of the application to a heterogeneous set of processors, and the application non-deterministically selects a possible execution of the application. We apply results about the existence and quality of optimal strategies in mean payoff games [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF][START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF] to find schedules that minimize the use of context-switches. Finally, we illustrate that our framework is expressive enough to subsume an established scheduling framework for streaming applications.

The structure of the paper is as follows: In Section 2, we introduce job constraints and define work automata. In Section 3, we define the graph on which a scheduling game is played. In Section 4, we apply our scheduling framework to streaming applications. In Section 5, we conclude and discuss future work.

Concurrent applications

As a starting point, we use a system of communicating automata to model interaction among processes in a concurrent application. To define the scheduling problem for this system of automata, we annotate each transition with an expression that models the workload of that transition. In Section 2.1, we recall the definition of constraint automata. In Section 2.2, we introduce job constraints, which model the work of the processes in a concurrent application. In Section 2.3, we define work automata by adding job constraints to constraint automata. In Section 2.4, we informally discuss the semantics of work automata. In Section 2.5, we extend constraint automata composition to work automata.

Preliminaries on constraint automata

Baier et al. proposed constraint automata to model interaction amongst processes in a concurrent application [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]. A constraint automaton is a tuple A = (Q, P, →), where Q is a set of states, P is a set of ports, called the interface, and → ⊆ Q × 2 P × Q is a transition relation. Informally, A is a labeled transition system with labels, called synchronization constraints, consisting of subsets N ⊆ P. A synchronization constraint N ⊆ P describes the interaction of A with its environment: ports in N synchronize, while ports outside of N block. Note that ∅ ⊆ P models an internal action of the automaton. Originally, in addition to a synchronization constraint, every transition in a constraint automaton carries also a data constraint. Data constraints are logical assertions that specify which particular data items may be observed on the ports that participate in a transition. Because data constraints do not matter in what follows-they address an orthogonal concern-we omit them from the definition for simplicity (technically, thus, we consider port automata [START_REF] Koehler | Decomposing port automata[END_REF]); the work presented in this paper straightforwardly extends to constraint automata with data constraints.

The constraint automaton of an entire application can be obtained by parallel composition of the constraint automata of its processes. For i ∈ {0, 1}, let

A i = (Q i , P i , → i ) be a constraint automaton. The composition A 0 A 1 is de- fined by (Q 0 × Q 1 , P 0 ∪ P 1 , →)
, where → is the smallest relation that satisfies the following rule: if i ∈ {0, 1}, [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]). In other words, a transition τ = ((q 0 , q 1 ), N, (q 0 , q 1 )) ∈ → of the composition is possible if either (1) both restrictions τ | P0 = (q 0 , N ∩ P 0 , q 0 ) and τ | P1 = (q 1 , N ∩ P 1 , q 1 ) are transitions in A 0 and A 1 , or (2) for some i ∈ {0, 1}, the restriction τ | Pi is a transition in A i that is independent of A 1-i , i.e., N ∩ P 1-i = ∅.

τ i = (q i , N i , q i ) ∈ → i , τ 1-i = (q 1-i , N 1-i , q 1-i ) ∈ → 1-i ∪ {(q, ∅, q) | q ∈ Q 1-i } and N 0 ∩ P 1 = N 1 ∩ P 0 , then τ 0 | τ 1 = ((q 0 , q 1 ), N 0 ∪ N 1 , (q 0 , q 1 )) ∈ → (cf., Definition 3.2 in

Job constraints

A system of constraint automata describes only interaction, while the workload of each process remains unspecified. Therefore, we extend transition labels in constraint automata with a work expression that models the amount of work that needs to be done before a transitions fires.

In the simplest of cases, a transition in a constraint automaton models an atomic piece of work, belonging to a single process. In that case, we can straightforwardly model this amount of work as a natural number n ∈ N 0 . However, through (parallel) composition, a transition in a constraint automaton may also model the synchronous firing of multiple transitions (originating from different constraint automata for different processes). In that case, a single natural number fails to express that the work involved by each of these multiple transitions may actually be done in parallel. For instance, for i ∈ {0, 1}, let A i = (Q i , P i , → i ) be a work automaton and τ i = (q i , N i , q i ) ∈ → i a transition that requires n i ∈ N 0 units of work. Suppose that τ 0 and τ 1 synchronize, i.e., N 0 ∩ P 1 = N 1 ∩ P 0 . Intuitively, τ 0 | τ 1 then requires n 0 + n 1 units of work, which may seem to define the composition of work. However, this composition loses the information that A 0 and A 1 may run in parallel and that the n 0 and n 1 units of work are independent of each other. To avoid this loss, we keep the values n 0 and n 1 separate by associating τ i with a job x i that requires n i units of work. We represent the work of τ i as the job constraint x i = n i , and the work of

τ 0 | τ 1 as x 0 = n 0 ∧ x 1 = n 1 .
Although job constraints with equalities (as introduced above) enable us to express parallelism of work between synchronizing transitions, they do not enable us to express parallelism of work between independent transitions (i.e., transitions that do not share any ports). The issue here is that if a transition τ 0 in automaton A 0 fires before an independent transition τ 1 in automaton A 1 fires, A 1 is free to already perform (some) work while τ 0 fires, in anticipation of later firing τ 1 . To model this, we should associate τ 0 with a job constraint that specifies that the work associated with τ 1 can be performed partially. We do this by allowing inequalities in job constraints. For instance, if the job constraint of τ 0 is x 0 = n 0 , while the job constraint of τ 1 is x 1 = n 1 , we define the job constraint of τ 0 | (i.e., the incarnation of τ 0 in the composition of A 0 and A 1 , where denotes an internal action of A 1 ) as

x 0 = n 0 ∧ x 1 ≤ n 1 .
We define the set of job constraints w over a set of jobs J by the grammar

w ::= | x = n | x ≤ n | w 0 ∧ w 1 , (1)
with x ∈ J and n ∈ N 0 . The need for inequalities in w, precludes using weights on transitions in weighted automata [START_REF] Droste | Handbook of weighted automata[END_REF] to represent work.

For notational convenience, we introduce the following terminology regarding a job constraint w over a set of jobs J . Let F, G ⊆ J and n x , m y ∈ N 0 , for all x ∈ F and y ∈ G, such that w is equivalent to x∈F x = n x ∧ y∈G y ≤ m y . We call w saturated, whenever F ∪ G = J . We call w satisfiable, whenever n x ≤ m x , for all x ∈ F ∩ G. If w is satisfiable and x ∈ J , then we define the available work

w x ∈ N 0 ∪ {∞} for job x by w x = n x , if x ∈ F , w x = m x , if x ∈ G \ F ,
and w x = ∞ otherwise. Finally, we define the set of required jobs ρ w ⊆ J by ρ w = F .

Work automata

We now extend the transition labels of constraint automata from Section 2.1 with the job constraints from Section 2.2. Definition 1. A work automaton is a tuple (Q, P, J , →) that consists of a set of states Q, a set of ports P, a set of jobs J , and a transition relation Example 1. One of the simplest non-trivial examples of concurrent systems is the producer-consumer system, shown in Figure 1(a). The producer generates data and puts them into its buffer. The consumer takes these data from the buffer and processes them. We assume that the buffer has capacity 2. We split the system into a buffered producer and a consumer. Figures 1(b) and 1(c) show their respective work automata. States 0, 1 and 2 in Figure 1(b) indicate the amount of data in the buffer. In state 0 or 1, the producer can produce a new datum by finishing 2 units of work of job x. In state 1 or 2, the consumer can take a datum from the buffer by synchronizing on port a, which requires no work on job x. In state 0 in Figure 1(c), the consumer waits for a datum d at port a. When d arrives, the consumer takes it from the buffer, requiring 1 unit of work on job y. In state 1, the consumer processes datum d, requiring 3 units on job z.

→ ⊆ Q × 2 P × Ω J × Q, where Ω J is the set of all satisfiable job constraints over J . Producer Consumer a (a) 0 1 2 ∅, x = 2 {a}, x ≤ 2 ∅, x = 2 {a}, x ≤ 2 (b) Buffered producer A prd . 0 1 {a}, y = 1 ∧ z = 0 ∅, y = 0 ∧ z = 3 (c) Consumer Acon.

Job execution

Let A = (Q, P, J , →) be some fixed work automaton. In this section, we informally introduce the semantics of A. The jobs in a work automaton are executed by a parallel machine M, which consists of a heterogeneous set of processors and a map that represents the execution speed of jobs on processors. Definition 2. A parallel machine is a tuple (M, J , v), where M is a set of processors, J is a set of jobs and v : J × M → N 0 is a map that models the speeds of jobs on processors.

It is the task of a scheduler to assign jobs from a set J to processors in a parallel machine (M, J , v) over J . We model this assignment of jobs to processors by an injective partial map s : M J that represents the scheduled jobs, i.e., s(i) = s(j) implies i = j, for all i, j ∈ M . We write S(M, J ) for the set of all injective partial maps s : M J . We represent the speeds of jobs in J subject to the scheduled jobs s ∈ S(M, J ) by the map v s : J → N 0 , given by v s

(x) = v(x, s -1 (x)) if x ∈ im(s) and v s (x) = 0 otherwise. Here, im(s) = {s(m) ∈ J | m ∈ M } is the image of s.
We represent the current progress of jobs by a map p : J → Q ≥0 , where Q ≥0 is the set of non-negative rational numbers. After executing the scheduled jobs s ∈ S(M, J ) for t ∈ Q ≥0 time, the progress of jobs in J equals p = p + v s • t, where + is pointwise addition and • is multiplication by a scalar, i.e., p

(x) = p(x) + v(x, s -1 (x)) • t if x ∈ im(s) and p (x) = p(x) otherwise.
Example 2. Let k > 0 be a positive integer and J a set of jobs. Then, M k = ({1, . . . , k}, J , v), with v(x, i) = 1 for all x ∈ J and 1 ≤ i ≤ k, models a parallel machine that consists of k identical processors. Any two processors are identical and interchangeable. Therefore, the scheduled jobs s ∈ S(M, J ) depend solely on the image im(s). If s, s ∈ S({1, . . . , k}, J ) and im(s) = im(s ), then v s = v s . Hence, we represent scheduled jobs as a subset J ⊆ J .

Let τ = (q, N, w, q ) be a transition in A and p : J → Q ≥0 be the current progress of jobs. Recall the notation regarding job constraints from Section 2.2. We call a job x finished whenever its progress p(x) equals w x ∈ N 0 ∪ {∞}. We demand that all required jobs x ∈ ρ w finish their available work w x . The automaton A may take a transition τ if the progress of jobs p satisfies the job constraint w (notation: p |= w), i.e., p(x) ≤ w x for all jobs x ∈ J and p(x) = w x for required jobs x ∈ ρ w . Note that for ρ w = ∅, transition τ requires no work, and τ then represents for example the arrival of input data.

Suppose that p |= w and A takes transition τ . Then, the current state of A becomes q and the progress of required jobs resets to zero. Formally, the progress becomes p = ρ w (p), where ρ w : N J 0 → N J 0 is the reset operation associated with ρ w defined as ρ w (p)(x) = p(x) if x / ∈ ρ w and ρ w (p)(x) = 0 otherwise.

Composition

In Section 2.3, we extended constraint automata to work automata. We now extend the composition of constraint automata from Section 2.1 to work automata. Let A 0 and A 1 be two work automata. We want our composition of work automata to conservatively extend the composition of constraint automata. This means that the state space, interface and transition relation (up to job constraints) of the composition are already determined. Since a job x in A i , for i ∈ {0, 1}, is merely a name for a piece of work inside A i , we may rename x to (x, i). This allows us to define the set of jobs of the composition as the disjoint union

J 0 + J 1 = J 0 × {0} ∪ J 1 × {1}. For i ∈ {0, 1}, let τ i = (q i , N i , w i , q i ) be a transition in A i . If N 0 ∩ P 1 = N 1 ∩ P 0 ,
then τ 0 and τ 1 synchronize and give rise to a transition τ 0 | τ 1 = ((q 0 , q 1 ), N 0 ∪ N 1 , w 0 ∧ w 1 , (q 0 , q 1 )). If τ 0 and τ 1 are independent, i.e., N 0 ∩ P 1 = N 1 ∩ P 0 = ∅, then τ 0 and the relaxation (q 1 , ∅, w ≤ 1 , q 1 ) of τ 1 , give rise to a transition τ 0 | τ ≤ 1 = ((q 0 , q 1 ), N 0 , w 0 ∧ w ≤ 1 , (q 0 , q 1 )) in the composition, where w ≤ 1 is the job constraint derived from w 1 by substituting every = with ≤. This substitution is well-defined, because, according to grammar (1), jobs exclusively appear on the left hand side of an equality. Transition τ 0 | τ ≤ 1 represents that τ 0 is taken, while jobs in τ 1 makes arbitrary progress bounded by w 1 . We define the a lift τ ≤ 0 | τ 1 of τ 1 analogously. Finally, if τ 0 00 10 20 01 11 21 is independent of A 1 (i.e., N 0 ∩ P 1 = ∅), then τ 0 gives rise to a transition ((q 0 , q 1 ), N 0 , w 0 ∧ x∈J1 x = 0, (q 0 , q 1 )) in the composition, where τ 0 executes independently of A 1 and all jobs in A 1 block. This blocking means that A 1 needs to wait, unless a transition

∅, x = 2 ∧ y = 0 ∧ z = 0 ∅, x = 2 ∧ y = 0 ∧ z = 0 ∅, x = 2 ∧ y = 0 ∧ z ≤ 3 ∅, x = 2 ∧ y = 0 ∧ z = 0 ∅, x = 2 ∧ y = 0 ∧ z ≤ 3 ∅, x = 2 ∧ y = 0 ∧ z = 0 ∅, x ≤ 2 ∧ y = 0 ∧ z = 3 ∅, x = 0 ∧ y = 0 ∧ z = 3 ∅, x ≤ 2 ∧ y = 0 ∧ z = 3 ∅, x = 0 ∧ y = 0 ∧ z = 3 ∅, x = 0 ∧ y = 0 ∧ z = 3 { a } , y = 1 ∧ z = 0 { a } , y = 1 ∧ z = 0 ∅ , x = 2 ∧ y = 0 ∧ z = 3 ∅ , x = 2 ∧ y = 0 ∧ z = 3
τ 1 in A 1 induces a synchronization τ 0 | τ 1 or τ 0 | τ ≤ 1 .
Definition 3. For i ∈ {0, 1}, let A i = (Q i , P i , J i , → i ) be a work automaton. We define the composition A 0 A 1 of A 0 and A 1 as the work automaton

(Q 0 × Q 1 , P 0 ∪P 1 , J 0 +J 1 , →)
, where → is the smallest relation satisfying the following rule: if i ∈ {0, 1},

τ i = (q i , N i , w i , q i ) ∈ → i , τ 1-i = (q 1-i , N 1-i , w 1-i , q 1-i ) ∈ → 1-i ∪ {(q, ∅, x∈J1-i x = 0, q) | q ∈ Q 1-i } and I := N 0 ∩ P 1 = N 1 ∩ P 0 , then 1. τ 0 | τ 1 = ((q 0 , q 1 ), N 0 ∪ N 1 , w 0 ∧ w 1 , (q 0 , q 1 )) ∈ →; and 2. I = ∅ implies τ 0 | τ ≤ 1 ∈ → and τ ≤ 0 | τ 1 ∈ →, where τ ≤ i = (q i , ∅, w ≤ i , q i ).
Example 3. Figure 2 shows the composition of the work automata from Figures 1(b) and 1(c). A state ij indicates that the buffered producer is in state i and the consumer is in state j. In state 00, the consumer cannot retrieve a datum from the buffer. Hence, the consumer is not allowed to work on job y. The transition from 01 to 11 with job constraint x = 2 ∧ y = 0 ∧ z = 3 is redundant, because the other transition from 01 to 11 has a weaker job constraint x = 2 ∧ y = 0 ∧ z ≤ 3.

Scheduling games

A work automaton can make non-deterministic internal choices, beyond the control of the scheduler. Therefore, we can view the scheduler synthesis problem over a work automaton and a parallel machine as a game that is played between the scheduler and the application modelled by a work automaton. The scheduler assigns jobs to processors and the application executes the running jobs and, whenever possible, makes a perhaps non-deterministically selected transition. We represent this game as a token game played on a graph that we derive from a work automaton and a parallel machine. Every play of this game (i.e., a path in this graph) corresponds to a run of the work automaton. Hence, a strategy in this game corresponds to a schedule of the corresponding concurrent application. In Section 3.1, we recall some basic terminology and known results for games played on graphs. In Section 3.2, we interpret the execution of jobs in a work automaton as a game played on a graph. In Section 3.3, we assign an execution time to every move in a scheduling game. In Section 3.4, we introduce a class of scheduling objectives for both terminating and non-terminating applications. In Section 3.5, we find schedules that minimize the number of context-switches.

Preliminaries on games on graphs

We view scheduler synthesis as a problem of finding optimal strategies in a game played on a graph. Therefore, we recall the basic definitions about these games.

A game arena is a finite directed bipartite leafless graph A. More formally, A is a triple (V, E, ϕ) that consists of a finite set of vertices V , a set of edges → ⊆ V × V such that for all a ∈ V there exists a b ∈ V with (a, b) ∈ E, and a 2-colouring ϕ : V → {0, 1}, i.e., (a, b) ∈ E implies ϕ(a) = ϕ(b), for all a, b ∈ V . Vertices and edges in this graph are called positions and moves. For every a 0 ∈ V , consider the following token game on A between Player 0 and Player 1. Let a 0 be the initial position of the token. Construct an infinite sequence π = (a i ) ∞ i=0 as follows: for all i ≥ 0, Player ϕ(a i ) selects a successor position a i+1 ∈ V , with (a i , a i+1 ) ∈ E, and moves the token from a i to a i+1 . The sequence π is called a play of this game, and plays(A) ⊆ V ω is the set of all such plays in A. A game G is a triple (A, a 0 , f ), where A = (V, E, ϕ) is a game arena, a 0 ∈ V is the initial position, and f : plays(A) → D is a payoff function, where D is some partially ordered set. The goal of Player 0 is to maximize the value f (π), while Player 1 tries to minimize f (π). A strategy σ k for Player k ∈ {0, 1} in a game G is a map

σ k : V * × V k → V 1-k , such that (v, σ k (u, a)) ∈ E for all u ∈ V * and a ∈ V k .
Intuitively, a strategy σ k determines the successor position σ k (u, a) ∈ V 1-k of Player k, based on the history u and the current position a. A strategy σ is called memoryless if and only if σ(u, a) = σ(u , a), for all u, u ∈ V * and a ∈ V . A play π = a 0 a 1 • • • is consistent with a strategy σ k for Player k if and only if for all i ≥ 0 we have that ϕ(a

i ) = k implies a i+1 = σ k (a 0 • • • a i-1 , a i ).
Example 4 (Mean payoff games [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF]). Let A = (V, E, ϕ) be an arena, and let c : E → Z be a weight function. In Section 3.3, we use these weights to represent the execution time of moves. A mean payoff game over A and c is a triple G = (A, a 0 , M c ), where a 0 ∈ V is the starting position, and

M c (a 0 a 1 a 2 • • • ) = lim inf n→∞ 1 n n-1 i=0 c(a i , a i+1 ).
Intuitively, M c computes the 'smallest' average value of the play a 0 a 1 a 2 • • • .

Scheduling arena

We now formulate the problem of scheduling a concurrent application, represented as a work automaton A = (Q, P, J , →), onto a set of heterogeneous processors, represented as a parallel machine M = (M, J , v). The scheduling problem consists of finding an optimal strategy in a game on a graph played by the scheduler (Player 0) and the application (Player 1). Intuitively, the game is played by alternating moves by the scheduler and the application. A scheduler move selects a schedule s ∈ S(M, J ). Recall the notation for job constraints from Section 2.2. An application move selects a transition τ = (q, N, w, q ) that allows scheduled jobs to progress, and then updates the progress p : J → Q ≥0 of the jobs by executing the scheduled jobs s until one of the jobs x ∈ J finishes w x units of work. If after the execution the job constraint w is satisfied, the application makes transition τ . Otherwise, the application makes the 'fictitious' idling transition q := (q, ∅, , q), where q ∈ Q is the current state of the automaton.

We now explain the construction of the game arena in more detail. We want every play of this game to correspond to an run of the associated work automaton. Therefore, we record, in every position of the game, the progress of the jobs and the state of the automaton. We define the positions of the scheduler as pairs (p, τ ), where p : J → Q ≥0 is the progress of jobs and τ = (q, N, w, q ) ∈ → ∪ { q | q ∈ Q} is the transition that is previously taken by the application (i.e., q is the current state of the work automaton). We define the positions of the application as triples [p, q, s], where p : J → Q ≥0 is the progress of jobs, q ∈ Q is the current state of the work automaton and s ∈ S(M, J ) is the set of the scheduled jobs that are selected by the scheduler.

In a position (p, τ ), the scheduler may select any assignment s ∈ S(M, J ) of jobs to processors, which corresponds to selecting a successor position [p, q , s]. For the definition of application moves, we first define enabled transitions. Intuitively, a transition is enabled in position [p b , q b , s] if its source state is q b , its job constraint is potentially satisfiable (i.e., p b (x) ≤ w x , for all x ∈ J ) and all scheduled jobs s can execute (i.e., v s (x) > 0 implies p b (x) < w x , for all x ∈ J ). Definition 4. We call a transition τ = (q, N, w, q ) enabled at a position b = [p b , q b , s] of the application if and only if for all x ∈ J , we have that q = q b , p b (x) ≤ w x , and v s (x) > 0 implies p b (x) < w x . We write E b ⊆ → for the set of all transitions that are enabled at b.

If there is no enabled transition, then the application selects the successor position (p, q ). Otherwise, the application selects any enabled transition λ = (q, N, w, q ) ∈ E b and executes its scheduled jobs, until one of them finishes.

b = [p, q, s] is t b (λ) = min T b (λ) if T b (λ) = ∅ 0 otherwise , where T b (λ) = {t ∈ Q ≥0 | ∃x ∈ J : v s (x) > 0 and p(x) + v s (x) • t = w x }.
After executing the jobs for t b (λ) units of time, the progress of the jobs becomes p + v s • t b (λ), which is defined as

(p + v s • t b (λ))(x) = p(x) + v s (x) • t b (λ), for all x ∈ J . If the job constraint of λ is satisfied (p + v s • t b (λ) |= w)
, the application makes transition λ by selecting position (ρ w (p + v s • t b (λ)), λ), where ρ w resets the progress of all finished jobs ρ w to zero. If the job constraint of λ is not satisfied (p+v s •t b (λ) |= w), the application selects position (p+v s •t b (λ), q ). Definition 6. A scheduling arena A over a work automaton (Q, P, J , →) and a parallel machine

(M, J , v) is a tuple A = (V, E, ϕ), where V = V 0 ∪ V 1 , V 0 = {(p, τ ) | p : J → Q ≥0 and τ ∈ → ∪ { q | q ∈ Q}}, V 1 = {[p, q, s] | p : J → Q ≥0 , q ∈ Q and s ∈ S(M, J )}
are the sets of positions of the scheduler and the application, ϕ(a) = 0 if and only if a ∈ V 0 , and E ⊆ V × V is the largest relation that satisfies the following rule: for all a = (p, τ

) ∈ V 0 and b = [p, q, s] ∈ V 1 we have 1. if τ = (-, -, -, q τ ), then (a, [p, q τ , s]) ∈ E; and 2. if E b = ∅, then (b, (p, q )) ∈ E; and 3. if λ = (q, N, w, q ) ∈ E b , then (a) p + v s • t a (λ) |= w implies (b, (ρ w (p + v s • t a (λ)), λ)) ∈ E; and (b) p + v s • t a (λ) |= w implies (b, (p + v s • t a (λ), q )) ∈ E.
As a scheduling arena A is infinite, it is not an arena as in Section 3.1. The following lemma provides a sufficient condition ensuring that A is locally finite, i.e., only finitely many positions in the A are reachable from any given position. Lemma 1. Let A be a scheduling arena over a work automaton A and a parallel machine (M, J , v). If A has finitely many transitions, all job constraints in A are saturated and all speeds v(x, i) are either zero or u, for some u ∈ N 0 , then only finitely many positions in A are reachable from any given position a ∈ A.

Proof. For every job x ∈ J , define m x = max {w x | w is a job constraint in A}. Since all job constraints are saturated, we have that |J | < ∞ and m x < ∞, for all x ∈ J . Hence, we find α ∈ N 0 such that for every job x ∈ J the progress p a (x) of x at a satisfies αp a (x) ∈ N 0 . Using Definitions 4, 5 and 6, it follows that for every job x ∈ J the progress p b (x) of x at a position b ∈ A reachable from a satisfies p b (x) ∈ {p a (x), 0, 1 α , . . . , αmx-1 α , m x }, for all x ∈ J . We conclude that only finitely many positions in A are reachable from any given position a ∈ A.

Example 5. Consider the work automaton A = ({0}, ∅, {x, y}, {λ, τ, µ}) and parallel machine M 2 , where λ = (0, ∅, x = 1 ∧ y ≤ 1, 0), τ = (0, ∅, x = 5 ∧ y = 0, 0) and µ = (0, ∅, x = 0 ∧ y = 1, 0). Figure 3 shows the scheduling arena over A and M 2 from Example 2 according to Definition 6. A circular position labelled by kα, with k ∈ {0, 1} and α ∈ { 0 , λ, τ, µ}, corresponds to (p, α) ∈ V 0 , with p(x) = 0 and p(y) = k. For k ∈ {0, 1}, a square position labeled by k, kx, ky or kxy corresponds to a position (p, 0, s) ∈ V 1 with p(x) = 0, p(y) = k and im(s) = ∅, im(s) = {x}, im(s) = {y} or im(s) = {x, y}, respectively.

Strategies and classical schedules

From a given work automaton A and parallel machine M, we constructed in Section 3.2 a scheduling arena A. Suppose that the non-deterministic behaviour of A is fully controlled by the scheduler, i.e., there is only one move possible at every position a ∈ V 1 of the application. We now argue that strategies in A naturally correspond to classical schedules of concurrent applications.

Since the application has a unique strategy, every strategy σ 0 of the scheduler induces a play π in A. The following definition assigns an execution time to every move in π, which allows us to represent π as a Gantt chart [START_REF] Gantt | Work, wages, and profits[END_REF].

Definition 7. The execution time t(a, b) of a move (a, b) ∈ E in a scheduling arena A = (V, E, ϕ) is t(a, b) =      t a (λ) if (a, b) ∈ V 1 × V 0 comes from λ ∈ E a 1 if a = [p, q, s] ∈ V 1 and E [p,q,s ] = ∅ = E a for some s 0 otherwise .
The case for t(a, b) = 1 can be seen as a time penalty for selecting s ∈ S(M, J ) that unnecessarily blocks the execution (E [p,q,s] = ∅). Example 6. In the scheduling arena in Figure 3, consider the play π that is given by 0 0 , 0x, 0τ, 0xy, 1λ, 1, 0µ, 0y, 1µ, 1, 0µ, 0y, 1µ, 1y, 1 0 , 1y, . . .. All zeros on the move labels are omitted in this arena. Figure 4(a) shows a Gantt chart representation of π. Note that, since x and y are executed on identical processors M 2 , it is not important on which processor x and y are scheduled.

We conclude that every strategy in A naturally induces a classical schedule of the concurrent application. Conversely, not every classical schedule comes from a strategy in such an arena A. According to Definition 6, scheduling strategies induce only semi-anchored schedules, i.e., a job can start at time t + n, with t ∈ Q ≥0 and 1 ≤ n ∈ N, only if t = 0 or t is a time that some job finishes, and all processors are idle between t and t + n. Figure 4(b) shows a schedule that cannot be represented by a strategy in A. However, shifting the executions of all jobs y to the left transforms Figure 4(b) into an anchored schedule. We now show that this shifting always produces a valid schedule for A. Let S be a (non-semi-anchored) classical schedule, and T ⊆ Q ≥0 be the set of all finish times of jobs in S including zero. Let t s be the start time of a job x with t s / ∈ T , and t f = max {t ∈ T | t ≤ t s } the last time a job in S finishes before t s . Every transition taken by A after t f was already enabled at time t f . Thus, shifting the execution of job x from t s to t f produces a valid schedule.

We call a scheduling objective regular, whenever this shifting operation produces a schedule that is at least as good as the initial schedule. For example, minimizing total execution time is a regular scheduling objective, while scheduling objectives that penalize for jobs that finish 'too early' are not regular.

Scheduling games

In this section, we define payoff functions for games played on scheduling graphs that naturally correspond to regular scheduling objectives.

Let π = a 0 a 1 • • • be a play in a scheduling arena A = (V, E, ϕ). Using Definition 7, we associate with every initial prefix π n = a 0 • • • a n , n ≥ 0, the total execution time t n = n-1 i=0 t(a i , a i+1 ). If our application terminates, then for every play π = a 0 a 1 • • • , the sequence t 0 , t 1 , . . . eventually stabilizes, i.e., t n = t m , for some n and all m ≥ n. Then, t n represents the total execution time of π. If our application does not always terminate, then we cannot associate with every play π its total execution time. An example of such an application is a streaming application (cf., Section 4). A natural scheduling objective in a streaming application is latency minimization at some output port o ∈ P. We define the latency at a port o as the average time between two successive I/O operations on o. To keep track of these I/O operations, we use a map θ o : E → {0, 1}, such that θ o (a, b) = 1 if and only if b = (p, τ ) ∈ V 0 , where τ = (q, N, w, q ) and o ∈ N . For a prefix π n = a 0 • • • a n , n ≥ 0, of π, we define the latency as the ratio between the total execution time t n and the number of I/O operations 1 + n-1 i=0 θ o (a i , a i+1 ). By varying θ : E → {0, 1}, we define the following class of scheduling games, called latency games, wherein Player k maximizes the 'smallest limiting ratio'. Recall the definition of locally finite scheduling arena's from Section 3.2. Definition 8. Let A = (V, E, ϕ) be a locally finite scheduling arena, θ : E → {0, 1} a map, and k ∈ {0, 1}. A latency game G for Player k over A and θ is a tuple G = (A, a 0 , T k θ ), where a 0 is an initial position and

T k θ (a 0 a 1 • • • ) = lim inf n→∞ (-1) k 1 + n-1 i=0 θ(a i , a i+1 ) n-1 i=0 t(a i , a i+1 ), (2)
where t : E → N 0 is the execution time from Definition 7.

Example 7 (Makespan games: T 1 0 ). Let θ be the map 0 : E → {0, 1}, given by 0(a, b) = 0, for all (a, b) ∈ E, and k = 1. The scheduling objective in the latency game over θ and k is given by T 1 0 = lim inf n→∞ -n-1 i=0 t(a i , a i+1 ). Recall from Section 3.1 that Player 0 wants to maximize T 1 0 , which corresponds to minimizing the total execution time -T 1 0 = lim sup n→∞ n-1 i=0 t(a i , a i+1 ).

Example 8 (Context-switches: T 0 1 ). Due to changes in the assignment of jobs to processors, context-switches may occur. Typically, context-switches inflict substantial overhead and their occurrences should be avoided. This scheduling objective can be seen as a latency game, where k = 0 and θ is the map 1 : E → {0, 1}, given by 1(a, b) = 1, for all (a, b) ∈ E. Then, the scheduling objective becomes

T 0 1 = lim inf n→∞ 1 n+1
n-1 i=0 t(a i , a i+1 ), which can be interpreted as maximizing the average time between two consecutive context-switches. Indeed, every move by the application executes all scheduled jobs until at least one of them finishes. The job that finishes should subsequently be descheduled (context-switch), to avoid suboptimal use of compute resources (i.e., idling).

Note that lim n→∞ n+1 n = 1 implies that the scheduling objective T 0 1 coincides with the payoff function of the mean payoff games in Example 4.

Example 9 (Latency at o: T 1 θo ). Let A be a work automaton with a port o ∈ P, and let A = (V, E, ϕ) be a scheduling arena over A and some parallel machine. Using Definition 6, we can identify the moves in the scheduling arena that come from a transition that requires an I/O operation on port o. Thus, let θ o : E → {0, 1} be given by θ o (a, b) = 1 if and only if b = (p, τ ) ∈ V 0 , where τ = (q, N, w, q ) and o ∈ N . The scheduling objective T 1 θo corresponds to maximizing the production rate at port o.

Optimal strategies

In Section 3.4, we viewed the scheduling problem as a game played on a graph. We now take advantage of the fact that these games have been extensively studied in the literature. To do this, we need some terminology about games on graphs. Let G be a game over an arena A, with initial position a 0 ∈ A, and payoff function f : plays(A) → D, for some partially ordered set D of values. A strategy σ k for Player k ∈ {0, 1} secures a value v ∈ D whenever (-1) k f (π) ≥ (-1) k v, for every play π ∈ plays(A) consistent with σ k . Intuitively, this means that if Player k uses strategy σ k then the value f (π) of any resulting play is not worse than v. Now, there exists an optimal strategy for Player k, whenever the maximum value v k (G) = max{(-1) k v | some σ k secures v} exists. The game G is determined, whenever v 0 (G) and v 1 (G) exist and are equal. Proof. For θ = 1, a latency game coincides with a mean payoff game (cf., Example 8). Ehrenfeucht and Mycielski show that mean payoff games are memorylessly determined [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF]. Brim et al. provide a pseudopolynomial time algorithm for finding an optimal memoryless strategy [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF].

In view of Example 8, the result of Theorem 1 shows that there exists an optimal strategy (determinacy) of good quality (memoryless) for maximizing the average time between two consecutive context-switches. For optimal play, the scheduler need not remember earlier scheduling decisions. Moreover, such an optimal strategy can be efficiently computed from the scheduling arena.

Cyclo-static dataflow

In a streaming application, a network of filters transforms an input stream of data into an output stream. Examples of such applications range from video decoding to sorting algorithms. A streaming application can be formally represented by a cyclo-static dataflow (CSDF) graph. Bamakhrama and Stefanov proposed a framework for scheduling CSDF graphs that are annotated with worstcase execution times [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF]. In this section, we argue that our proposed scheduling framework of Section 3 subsumes this scheduling framework for CSDF graphs.

Consider the CSDF graph in Figure 5(a), wherein four filter processes A 1 , A 2 , A 3 and A 4 , called actors, are connected by FIFO buffers. The behaviour of an actor consists of a periodic sequence of execution steps, whose worst-case execution time is represented the value (µ i ) at A i , for i ∈ {1, 2, 3, 4}. In each step, an actor atomically consumes tokens from its input buffers and produces tokens for its output buffers. The production and consumption rates of an actor A i with period n are determined by vectors [x 1 , . . . , x n ] (Section 3.1 in [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF]).

Bamakhrama and Stefanov generate from a CSDF graph with worst-case execution times a strictly periodic task set (Example 3 in [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF]), by determining for every filter A i , a starting time S i ∈ N 0 and a period T i ∈ N 0 such that all required input tokens are available for all execution steps of all actors and all buffers need only a finite capacity throughout the execution. Figure 5(b) shows the strictly periodic task-set of the CSDF graph in Figure 5(a). Bamakhrama and Stefanov then use standard scheduling algorithms for strictly periodic task set to compute a schedule S for this CSDF graph (cf., Section 3.2.2 in [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF]).

Every actor A i , with i ∈ {1, 2, 3, 4}, can be represented as a work automaton over a single job x i , and every buffer can be represented as a work automaton without jobs. Using the composition operator from Section 2.5, we find a work

(2)

(3) (2)
(a) CSFD (Figure 1 in [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF]) automaton A that describes the behaviour of the CSFD graph in Figure 5(a). The behaviour of A is fully under the control of the scheduler. Hence, Section 3.3 shows that, for regular scheduling objectives, the schedule S obtained in [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF] induces a strategy in the scheduling arena A over A and M 4 . We conclude that, for regular scheduling objectives, a schedule induced by an optimal scheduling strategy in a scheduling game is not worse than any schedule found by the scheduling framework proposed by Bamakhrama and Stefanov.

Discussion

We extended constraint automata with job constraints to model the work of processes in a concurrent application. We recognize that scheduling decisions do not completely determine the execution of a concurrent application, and therefore view scheduler synthesis as playing a game on a graph between a scheduler and the application. We introduced a class of natural scheduling objectives, and applied game-theoretic results for mean payoff games to find a scheduling strategy that maximizes the time between subsequent context-switches.

Work automata are similar to timed automata [START_REF] Alur | A theory of timed automata[END_REF]. Clock constraints and clock valuations correspond to job constraints and progress of jobs. Still, there are two main differences between them. First, we reset only required jobs in work automata, while in timed automata clocks can reset at any time. Second, we allow jobs to make progress at different speeds, while clocks in timed automata increment uniformly. Using this clock-speed relaxation, the scheduler controls the execution rate of each job by selecting which jobs to schedule. Using our notion of jobs, it seems possible to represent the execution of a concurrent application on a set of processors by means of hybrid automata [START_REF] Henzinger | The theory of hybrid automata[END_REF] or hybrid constraint automata [START_REF] Chen | A hybrid model of connectors in cyber-physical systems[END_REF]. However, since such a representation convolutes the specification of the application with the specification of the parallel machine, hybrid (constraint) automata are unsuitable for our purpose.

Scheduler synthesis for concurrent applications is similar to controller synthesis for real-time systems [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF][START_REF] Bouyer | Synthesis of optimal strategies using hytech[END_REF][START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], because the non-deterministic behaviour of a real-time system, modeled as a timed automaton [START_REF] Alur | A theory of timed automata[END_REF], is not fully determined by its controller. Therefore, the controller synthesis problem is formulated as a game on the automaton that is played between the controller and an adversary. However, our problem differs from controller synthesis in that scheduler synthesis requires a strong relation between processes and processors.

The size of a composed work automaton for a whole application very quickly becomes too large. Moreover, the size of a scheduling arena is again much larger than that of the work automaton. Nevertheless, an optimal strategy in such an immense game may indeed have a very simple form (like balancing production and consumption rates in buffers). One direction for our future work is to investigate under what conditions it is possible to bypass these exponential blow-ups. The existence of efficient solutions for more restricted scheduling problems (e.g., CSDF applications [START_REF] Bamakhrama | On the hard-real-time scheduling of embedded streaming applications[END_REF]) let us believe that it is possible to find such conditions.

Fig. 1 .

 1 Fig.1. Producer-consumer application (a), and its corresponding system of work automata (b) and (c) with {a} as their interface {x} and {y, z} as their respective job sets.

Fig. 2 .

 2 Fig. 2. Composition A prd Acon of the work automata in Figures 1(b) and 1(c).

Definition 5 .

 5 The time to first completion t b (λ) of an enabled transition λ ∈ E b at a position

Fig. 3 .

 3 Fig. 3. Scheduling arena over a work automaton A from Example 5. Circular positions belong to the scheduler position and square positions belong to the application.

Fig. 4 .

 4 Fig. 4. Play π from Example 6 (a), and a schedule that is not semi-anchored (b).

Theorem 1 .

 1 The latency game for θ = 1 is memorylessly determined, and a memoryless optimal strategy can be found for it inO(|V | 2 • |E| • log(|V | • T ) • T ) time, with T = max (a,b)∈E u • t(a, b) and u the speed of the processors.

A 1 A 2 A 3 A 4 (Fig. 5 .

 12345 Fig. 5. Cyclo-static dataflow model (a) and strictly periodic task set (b).