Antoniu Pop

Albert Cohen

Control-Driven Data Flow

Keywords: Model of computation, operational semantics, programming languages, data-ow, stream computing, parallel programming. Control-Driven Data Flow Modèle de calcul, sémantique opérationnelle, langages de programmation, ot de données, calcul par streams, programmation parallèle

This paper presents CDDF, a model of computation underpinning the formal semantics of a number of parallel programming languages. CDDF integrates control ow elements for the dynamic construction of task graphs, and data ow elements to express dependent computations and to decouple these using unbounded streams (Kahn process networks). It is a common ground to dene the formal semantics of imperative programming languages with dynamic task creation, as well as data-ow or concurrent functional languages, as a special case of more general dependent task languages with channels or streams. We prove essential properties for languages tting this model of computation, including deadlock-freedom, functional and deadlock determinism, and serializability. We also compare the model's hypotheses with Cilk's strictness and the Kahn principle.

Introduction and Related Work

The principal motivation for research into data-ow models comes from the incapacity of the von Neumann architecture to exploit massive amounts of ne-grain parallelism. The early data-ow architectures [START_REF] Dennis | A preliminary architecture for a basic data ow processor[END_REF][START_REF] Davis | The architecture and system method of DDM1: A recursively structured data driven machine[END_REF][START_REF] Watson | A practical data ow computer[END_REF] avoid the von Neumann bottlenecks by only relying on local memory and replacing the global program counter by a purely data-driven execution model, executing instructions as soon as their operands become available. Programmer productivity is another important motivation: debugging concurrent applications with low level threads is a daunting task, mostly because of the non-deterministic nature of races and deadlock-related errors. Data-ow languages closely follow the hardware model: the execution is explicitly driven by data dependences rather than control ow [START_REF] Johnston | Advances in dataow programming languages[END_REF]. Data-ow languages oer functional and parallel composition of parallel programs preserving functional determinism. Recent data-ow architectures, execution models, and languages rely on the same principles, albeit at a coarser grain, executing sequences of instructions, or data-ow threads, instead of single instructions.

Among the most notable data-ow languages, Lucid [START_REF] Ashcroft | Lucid, a Nonprocedural Language with Iteration[END_REF] relies on the next keyword within loops to achieve a similar eect to advancing in a stream of data, by consuming or producing in a channel, or, in the synchronous languages domain, to the advancement of clocks on signals.

Sisal [START_REF] Gaudiot | The Sisal Model of Functional Programming and its Implementation[END_REF] explicitly introduces the notion of stream, which is naturally very close to lists. If stream processing systems are understood as the parallel implementation of stream transformers, which is the functional interpretation of a process network mapping a set of input streams to a set of output streams, then any functional language can be used for stream programming. This corresponds to the lazy interpretation of functional languages; see [START_REF] Caspi | Synchronous Kahn networks[END_REF] for a Haskell [START_REF] Hudak | Report on the programming language Haskell: a non-strict, purely functional language version 1.2[END_REF] implementation of Lucid Synchrone [START_REF] Caspi | Real-Time Systems: Models and verication Theory and tools, chapter Synchronous Functional Programming with Lucid Synchrone[END_REF]. First-class streams of data improve expressiveness for a variety of communication and concurrency patterns such as broadcast, delays, and sliding windows. This was observed by data-ow computing pioneers, who designed I-structures as unbounded streams of futures to alleviate some of the overheads of a pure data-ow execution model [START_REF] Arvind | I-structures: Data structures for parallel computing[END_REF] Kahn process networks (KPN) [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] capture the essence of stream computing. Processes communicate through unbounded FIFO channels, write operations are non-blocking, and read operations wait until sucient data is available. Assuming processes are deterministic, a key property of this model is that the network as a whole is also functionally deterministic by composition. In his survey [START_REF] Stephens | A survey of stream processing[END_REF] of stream processing, Stephens classies stream processing systems based on three criteria: synchrony, determinism and the type of communication channel. Fundamentally, stream-based models of computation all share the same structure, which can generally be represented as a graph, where computing nodes are connected through streaming edges. However, cyclic networks can lead to deadlocks or unbounded growth of in-ight data, which has spurred the development of a restricted form of Kahn Process Networks, Cyclo-Static Data-Flow (CSDF) [START_REF] Lee | Static scheduling of synchronous data ow programs for digital signal processing[END_REF][START_REF] Bilsen | Cyclo-Static Data Flow[END_REF]. While processes in KPNs execute asynchronously and can produce or consume variable amounts of data, CSDF processes have a statically dened behaviour. With rates of production and consumption known at compile time, it is possible to statically decide whether the execution is free of deadlocks and to statically schedule the execution. It can also guarantee the absence of resource deadlocks when executing on bounded memory, a realistic restriction. StreamIt is a recent instantiation of CSDF, building on the strong static restrictions of the underlying model to enable aggressive compiler optimizations, it achieves excellent performance and performance portability across a variety of targets [START_REF] Gordon | Exploiting coarse-grained task, data, and pipeline parallelism in stream programs[END_REF] for a restricted set of benchmarks that properly map on this model. On the other hand, data-ow synchronous languages such as Lustre [START_REF] Halbwachs | The synchronous data ow programming language LUSTRE[END_REF] have been widely adopted in the certied design ow of reactive control applications. They oer determinism, deadlock-freedom, bounded reaction time and memory. Unlike CSDF, they are not restricted to periodic activations and communications.

no strongly connected components. Section 5 proves that all CDDF programs benet from functional and deadlock determinism. Section 6 shows that stream communication provides a very strong form of consistency, strict consistency, and proves necessary and sucient conditions for two forms of serializability. Section 7 summarizes the properties of CDDF programs and the conditions required to prove that such properties hold. Finally, Section 8 concludes this paper. Due to space constraints, proofs are made available as auxiliary material.

2 Denitions and Notations Informally, a programming paradigm implementing the CDDF model of computation is built around three key concepts: a control program, streams and tasks. The control program is, for example, the main program in OpenMP or Cilk and is responsible for spawning tasks, with an explicit specication of task dependences, at the spawning point, in the form of data produced or consumed on streams. CDDF tasks are a simple form of communicating coroutines: like data-ow threads, they run to completion (no synchronization once a task starts executing) and communicate through point-to-point data copying, using streams exclusively. The latter restriction is meant to avoid considerations on the memory model: shared-memory communications and in-place updates are not disallowed, but their semantics is not covered by CDDF and must be described separately for languages providing such options. Furthermore, we rely on the following simplifying assumptions to focus the presentation on the core concepts and results: [START_REF] Alglave | Fences in Weak Memory Models[END_REF] the memory space is unbounded, which allows us to model stream accesses in (dynamic) single assignment; and (2) the control program is a deterministic sequential process. Lifting these assumptions is out of the scope of the paper [START_REF] Pop | Leveraging Streaming for Deterministic Parallelization: an Integrated Language, Compiler and Runtime Approach[END_REF].

In this section, we rst present the key concepts underpinning the CDDF model, then we introduce a simple example of a programming language, ImpStream, that serves to illustrate the style and expressiveness of programming models implementing CDDF. The rest of the section is dedicated to the execution model enabled under CDDF and the characterization of the dierent deadlock types that can occur.

CDDF Program Structure

Our model in centered on the description of communication patterns in streams and on the expression of the scheduling constraints resulting from data dependences on streams. Streams are unbounded and indexed in the set of natural numbers: Denition 1 (Stream). A stream s is a partial function mapping indexes in N to (possibly typed) values. Let S denote the innite set of streams. At any state of the execution of a CDDF program, stream are only dened on a nite subset of indexes, but the domains of streams are generally unbounded. Denition 2 (Stream access). We distinguish between read accessesRand write accesses W to streams. A stream access is a triple (u, s, i) where u ∈ {R, W }, s is a stream in S and i is an index in N.

The semantics of a read stream access (R, s, i) is to return the value s(i), which may be undened if the index i does not belong to the domain of stream s.

The semantics of a write stream access (W, s, i) is to return a new stream s ′ , identical to s except that its index i is mapped to a new value (we will see, in Lemma 12, that i cannot already belong to the domain of s, corresponding to a dynamic single assignment property). The actual value does not matter at the level of abstraction of the CDDF model. Let X denote the set of all stream accesses:

X = {R, W } × S × N
Contrary to existing streaming models, we do not give much importance to the notion of a repetitive lter or process, corresponding to the iterative creation of tasks applying the same work function to a given set of input and output streams. As our model is inherently dynamic, it tends to be less focused on regular communication patterns. Instead, our abstraction only keeps the notion of task activation, in the form of one execution of a work function. Task activations are the fundamental and atomic unit of work. 1 As work functions can be called with dierent input and output streams, they cannot constitute or fully identify lters/processes.

We further abstract the notion of task activation to only consider the stream accesses necessary for the task activation's execution, irrespectively of the work function applied. Denition 3 (Task activation). A task activation a is dened by the set of stream accesses it uses to read and write data in streams:

a ⊂ X
The set A of task activations is the powerset of X :

A = P(X )
This view is entirely focused on the streams and stream indexes that are read and written during the execution of the task activation. This represents the minimal information to characterize the data dependences between task activations. Denition 4 (Input and output streams). We say that a stream s ∈ S is an input (resp. output) stream to a task activation a ∈ A and we write s ∈ I(a) (resp. s ∈ O(a)) if the task activation a contains a read (resp. write) access to stream s:

I(a) = {s ∈ S | ∃i ∈ N, (R, s, i) ∈ a} O(a) = {s ∈ S | ∃i ∈ N, (W, s, i) ∈ a}
The core of our model is the control program , which dynamically and deterministically attributes indexes to data stored by every task activation in its output streams. We refer to the attribution of stream indexes to task activations as the schedule of stream access.

As we are not interested in the semantics of the underlying programming language, we only require the execution of the program to be non-blocking aside from synchronization barriers. We model the control program by its execution trace where we only keep two types of operations: task activation points and barriers. All other operations are omitted from the trace.

Activation points can be thought of as task spawn calls and their evaluation results in the creation of new task activations. The barrier's informal semantics is to stall the control program until the completion of all task activations it produced up to the barrier. Denition 5 (Activation point). An activation point π is a statement of the control program that generates a task activation. We do not care about the precise work associated with this task activation, but only about the eect on its input and output streams. We thus abstract an activation point as a nite set of descriptors of its stream accesses:

π ⊂ (u, s, b, h) ∈ {R, W } × S → N × N
where each descriptor is a function from (u, s) to (b, h), u determines if the task activation will consume from or produce to stream s, b is the burst, or number of data items produced or consumed, and h is the horizon, which is the amount of data accessed in the stream. The horizon is greater than or equal to the burst; when strictly greater it allows read accesses ahead into the stream, which is also called a peek operation in related work.

The set of valid activation points for any control program is dened as:

Π = π ∈ P {R, W } × S → N 2 | (R, s, b, h) ∈ π ⇒ b h ∧ (W, s, b, h) ∈ π ⇒ b = h
The restrictions on valid activation points are meant to prevent read descriptors from discarding data, in the case where the burst would be greater than the horizon, and write descriptors from both publishing uninitialized stream locations or writing ahead, which would break the single-assignment property on stream accesses. Without loss of expressiveness, we also disallow multiple read (resp. write) accesses to the same stream at a given activation point.

The semantics of the control program is operationally dened as a transition system. We use partial execution traces to label the program states. These states are ordered by prex inclusion on traces, relying on the sequential hypothesis on the control program. Denition 6 (Control program trace). The execution trace of the control program is a possibly innite word on Π ∪ {barrier}. The set K of partial execution traces recognized by the control program's transition system is dened as:

K = (π + barrier) *
Using the notations above, we can dene the state of a CDDF program as its (partial) execution trace and two sets of task activations, one for already executed activations and the other for outstanding task activations. Denition 7 (CDDF program state). We dene the set Σ of possible program states:

Σ ⊂ K × P(A) 2 A state σ = (k e , A e , A o ) ∈ Σ of
ξ(k, π) (u, s, i) ∈ X | ∃(u, s, b, h) ∈ π ∧ i ∈ α, α + h , where α = π ′ ∈k (u,s,b ′ ,h ′ )∈π ′ b ′

RR n°8015

For the new task activation generated by the control program at a given activation point, ξ determines the location of data produced or consumed on each stream. The activation point is identied by its (partial) trace k at and activation point π. It relies on the past activation points that were executed by the control program, summing the bursts b ′ of all activations with the same operation type u on the same stream s. As the burst is the amount of data produced or consumed by a task activation, it determines the shift inside the stream required for the activation. The sum α of all such shifts along the execution of the control program determines the indexes of the stream accesses of the new task activation.

Our model is centered around the data schedule computed by the control program. To ensure that our results are general, not limited to any given class of applications, we make no assumption on the future of the control program. In the absence of any information on the oracle function Ω, which we assume deterministic, but not determinate, we abstract the union of all possible futures of the control program, and therefore of the possible future stream accesses. For technical reasons that will become clear in the remainder, we choose to represent this abstraction as a special task activation, the continuation activation. Its role is to capture and aggregate all of the stream accesses that can still be scheduled by any possible continuation of the control program. In a given state σ = (k e , A e , A o ), the past of the control program is dened by the partial trace k e . For this reason, the continuation activation is constructed as the result of a function C : K → P(X ) that maps a partial trace k ∈ K into a set of stream accesses in X . This approach ensures that there are no hidden assumptions on the control program, and therefore guarantees the generality of our proofs. Denition 9 (Continuation activation). In all CDDF program states σ = (k e , A e , A o ), the continuation activation C(k e ) is implicitly added to A o . This continuation is dened by:

C(k e ) (u, s, i) ∈ X | i π∈ke (u,s,b,h)∈π b
The initial state of a CDDF program is therefore:

σ init = (ǫ, ∅, {C(ǫ)})
where C(ǫ) = X By construction of the ξ function, this continuation activation contains all stream accesses, and in particular the write accesses, that cannot occur before the control program makes progress, because the control program has not yet scheduled these stream accesses in any task activations. When the control program reaches a barrier, it models all write stream accesses that can only happen after the barrier passes. If for example a write stream access (W, s, i) belongs to the continuation activation and there is an outstanding activation containing (R, s, i), then unless the control program can make further progress, there is an unsatisable ow dependence and hence a deadlock. Proposition 10. The state σ = (k e , A e , A o ) of a CDDF program satises:

a∈Ae∪Ao a = X
This state invariant holds by construction of the continuation activation, which attributes to the continuation, on every stream, each stream access not yet scheduled in a task activation generated by the execution of the control program. There is also a (safe) overlap for read accesses as those in C(k e ) start at the sum of bursts on each stream, which can be lower than the highest horizon. This property can also be rewritten as:

∀(u, s, i) ∈ X , ∃a ∈ A e ∪ A o , (u, s, i) ∈ a Inria 2.2
The ImpStream language

To illustrate the semantics of our model, we extend a simple, classical imperative programming language with task parallel constructs that communicate through streams. The resulting language, ImpStream is presented in Figure 1;2 it implements the CDDF model. The underlying language is a very simple, yet Turing-complete, imperative language based on assignments, sequences, conditionals and while loops. In addition to the atoms of the base language, constants cst ∈ Cst and identiers ide ∈ Ide, we need the type of stream access u ∈ {R, W }. To make the relation between ImpStream and CDDF clearer, we reuse the original CDDF notations for activation points π ∈ Π.

(1)

x ∈ X

x ::= ide[expr]

(2) Our extension to the original imperative language consists in adding the last two constructs in rule (6) on Figure 1, providing the task and barrier constructs, and in the addition of rules ( 1) and ( 2), dening a syntax for stream accesses and task activation points. We did not reuse the CDDF notation for rule [START_REF] Alglave | Fences in Weak Memory Models[END_REF] as the type u of stream accesses is implicit from the position of the access as a left-hand side of an assignment or as part of an expression. We therefore use a simpler notation based on a stream identier and an expression computing the stream access index. Furthermore, we simplify the expression of stream access indexes: instead of making the ξ function in CDDF explicit (as dened by the control program), we add an identier (...) : ide to each stream access descriptor in rule [START_REF] Arvind | I-structures: Data structures for parallel computing[END_REF]. This identier denotes the value of α in Denition 8 at the activation point: it corresponds to the lowest stream access index that can be accessed within the task activation on a given stream. This oset is made explicit here for the sake of clarity, but can be entirely handled (and hidden as is the case in OpenStream [START_REF] Pop | Expressiveness and Data-Flow Compilation of OpenMP Streaming Programs[END_REF]) by the compiler and runtime of a CDDF language.

π ∈ Π π ::= ǫ | π, π | (u, ide, expr, expr) : ide (3)
lhs ::= ide | x ( 4
) parm ::= ǫ | expr | parm, parm (5)
To illustrate the semantics of ImpStream, as well as the CDDF concepts introduced in the section above, let us consider the example of the nite impulse response (FIR) lter on Figure 2, computing the moving average over a stream of data. The semantics of this program, while intuitively simple to understand, will be developed along the paper. Informally, the dierent instances of the rst task act as a source lter, producing data on stream istream; the second task contains the main workload, computing the moving average function on data read on stream istream and writing its output on stream ostream; nally the last task consumes the resulting data on ostream and uses it for some computation, denoted by the use function.

We analyse the program on Figure 2 along the three main CDDF concepts: the control program, tasks and streams. The control program is composed of an innite while loop over three task constructs, where only the sets of stream access descriptors task activation points. 3 These descriptors play a key role in declaring how tasks interact with streams: a programming model should prevent, by construction, tasks from performing stream accesses that are not covered by the respective descriptors. 4 This means that the code of a task should not perform any other stream accesses than those belonging to the set resulting from the evaluation of the ξ function. For convenience, ImpStream provides offset variables with each stream access descriptor, which in our current example are all equal to the iteration index of the main loop.

π A = {(W, istream, 1, 1)}, π B = {(R, istream, 1, N ), (W, ostream, 1, 1)} and π C = {(R,
The CDDF execution trace of the control program is the iterated sequence (π A .π B .π C ). The oracle function Ω can therefore be recursively dened here as

Ω(ǫ) = π A then ∀k ∈ K, Ω(k.π A ) = π B , Ω(k.π B ) = π C , Ω(k.π C ) = π A .
The task construct of ImpStream shows the separation between the activation point, which declares the stream memory eects of the task, and the task activation itself, dened by the block of code associated with the task. For a given iteration index i, the evaluation of the activation points π A i , π B i and π C i with the ξ function results in the task activations a A i = {(W, istream, i)}, a B i = {(R, istream, j) i≤j<i+N , (W, ostream, i)} and

a C i = {(R, ostream, i)}.
Stream accesses within tasks use an array-like access syntax, the type of the access (read or write) is implicit from the position as a left-or right-hand side occurrence. By replacing the oset variables by an implicit i induction variable in this program, it is clear that the stream accesses in the task code bodies match the task activations a A i , a B i and a C i as evaluated by the control program's ξ function.

2.3

Ordering Constraints on Task Activation Execution One of the key insights of the CDDF model is the separation of constraints between the control program, which executes a deterministic sequence of activation points, and the execution of task activations. We elaborate, in Section 3.1, on the issue of the order relation induced by Ω on activation points, and therefore by precedence in the control program trace, while in this section we discuss the ordering constraints that need to be enforced on the execution of task activations.

As we see below, the only fundamental order requirement for task activations execution is induced by the enforcement of ow dependences between activations. For a lot of reasons, we choose to over-constrain the execution of task activations, synchronizing over closed prexes of stream indexes: indexes lower than a given threshold become read-only once all producers have moved past that point. This hypothesis has been central in stream computing since the invention of Kahn process networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]. It acknowledges that single-assignment of stream elements must be complemented with a prex closure constraint on the domain of streams, allowing to reason about causality and to derive operational semantics of practical interest. In particular, maintaining closed, single-assignment prexes is essential to enable a provably ecient synchronization scheme [START_REF] Pop | Leveraging Streaming for Deterministic Parallelization: an Integrated Language, Compiler and Runtime Approach[END_REF], barring hardware support like full-empty bits. This constraint also dramatically simplies memory management, facilitating the implementation of bounded windows in active streams as circular buers.

This hypothesis means that our synchronization scheme over-approximates the real scheduling constraint requirements, which brings us to one of the principal issues tackled in this paper: to which extent does this over-approximation induce new programming errors, which we dene as spurious deadlocks below, and what conditions must be satised by a CDDF program to avoid such errors.

To model these constraints, we dene the stream prex order relation and the derived scheduling constraints enforced on the execution of task activations.

Denition 11 (Stream prex order). We dene a binary relation < in P(A 2 ) on task activations (a, a ′ ) ∈ A 2 as:

a < a ′ ∃(s, i) ∈ S × N, ∃j i, (W, s, j) ∈ a ∧ (R, s, i) ∈ a ′
Which means that a ′ reads data in a stream s while a writes in stream s somewhere in the prex of the read accesses of a ′ . Note that this relation is not transitive as any relations a < a ′ and a ′ < a ′′ can arise from dierent streams.

We derive the relation ⋉ ∈ P(A) × A to model our scheduling constraint for the execution of task activations; for an activation a ∈ A and a set A ⊂ A:

A ⋉ a ∀(R, s, i) ∈ a, ∀j ≤ i, ∃a ′ ∈ A, (W, s, j) ∈ a ′
This relation, pronounced a is ready in A, expresses the fact that for a given program state σ = (k e , A e , A o ), if an outstanding task activation a ∈ A o is in a relation A e ⋉ a, then all of its ordering constraints are satised by the already executed activations in A e if and only if there is no task activation a ′′ ∈ A o such that a ′′ < a (recalling the role of C(k e ) ∈ A o as an aggregator of possible futures). As there can only be one single write access operation per stream index, and as Proposition 10 ensures that no write access escapes A e ∪ A o , this relation can be dened more concisely as:

∀a ∈ A e ∪ A o , A e ⋉ a ∀a ′ ∈ A e ∪ A o , a ′ < a ⇒ a ′ ∈ A e
The second version of the denition, relies on the fact that A e and A o are disjoint, which holds by construction of any valid program state, as we show below.

We present on Figure 3, the operational semantics of the execution of CDDF programs, and an overview of the CDDF execution model on Figure 4. We detail the semantics of the execution rules below.

(GEN) The activation generation rule states that the control program can execute an activation point as soon as it is reached by its oracle function, Ω. (GEN)

π := Ω(k e ) π ∈ Π (k e , A e , A o ) -→ (k e .π, A e , A ′ o = A o \ {C(k e )} ∪ {ξ(k e , π), C(K e .π)}) (BAR) A o = {C(k e )} Ω(k e ) = barrier (k e , A e , A o ) -→ (k e .barrier , A e , A o ) (TERM) A o = {C(k e )} Ω(k e ) = ⊤ (k e , A e , A o ) -→ (k e , A e , A o ) (EXEC) A o = {a} ∪ A ′ o A e ⋉ a (k e , A e , A o ) -→ (k e , A e ∪ {a}, A ′ o )
Figure 3: CDDF execution rules. (EXEC) The execution rule states that an outstanding activation a can only be executed once all the activations that need to be scheduled before it, in the stream prex order, are executed, which as we have discussed is modeled by A e ⋉ a. We will see in Lemma 18 that the continuation activation C(k e ) cannot be executed

: ∀σ = (k e , A e , A o ), ¬(A e ⋉ C(k e )).
The execution of a CDDF program consists of a set of possibly concurrent transitions. As depicted on Figure 3, the control program's execution is modeled by the transitions (GEN), (BAR) and (TERM), which are sequentially ordered on the program trace. The execution of task activations, modeled by transition (EXEC), is only ordered by the predicate ⋉. This means that Inria multiple task activations can be ready in any given state of the program, and possibly while the (GEN) transition can also be applied. The concurrent execution of multiple (EXEC) transitions is possible because ⋉ is monotonic: for any set of task activations A and task activations a, a ′ / ∈ A such that A ⋉ a, we also have A ∪ {a ′ } ⋉ a as a direct result from Denition 11. Finally, it is easy to verify that there can be no concurrency between the (BAR) or (TERM) transitions and the (EXEC) transition as their conditions are mutually exclusive, see Lemma 18. We illustrate the CDDF execution model on our running example, the FIR lter on Figure 2. This example assumes that one thread executes the control program, as a sequence of (GEN) transitions, and multiple threads are available to execute task activations, using a greedy scheduler: an (EXEC) transition occurs on the rst available thread. In this application, the task activations (a A i ) i∈N contain no stream read access. For this reason, we deduce that ∀i ∈ N, ∅ ⋉ a A i which means that such task activations are ready for execution as soon as they are generated by the control program. The task activations (a B i ) i∈N each require reading N values on stream istream, produced by task activations (a A j ) i≤j<i+N . However, our over-approximation scheme of dependences over closed prexes enforces the stream prex order relation, which means that the execution of task activation a B i requires that all task activations (a A j ) 0≤j<i+N be already executed. This over-synchronization is represented by the solid (red) arrow on Figure 2 from a A 0 to a B 1 . Similarly, a task activations a C i , which contains a stream read access computed by task activation a B i , requires that all activations (a B j ) 0≤j≤i be executed, corresponding for example to the solid (red) arrow from a B 0 to a C 1 . Serial execution is also possible, by allowing ready (EXEC) transitions to interleave with control program transitions, for example by prioritizing the (EXEC) transition and only executing (GEN), (BAR) or (TERM) transitions when no (EXEC) transition is possible.

Using the execution model of the control program from Denition 8 and the execution rules on Figure 4, we can now prove that our model enforces, by design, a single assignment property on stream accesses.

Lemma 12 (Single assignment of stream accesses). In any given execution of the control program, the write stream accesses belonging to (generated) task activations are exclusive. Formally, in a state σ = (k e , A e , A o ), we have:

∀a, a ′ ∈ A e ∪ A o , ∃(W, s, i) ∈ a ∧ (W, s, i) ∈ a ′ ⇒ a = a ′
Proof. First, we show that the continuation activation cannot contain any write stream access that was scheduled by ξ to any task activation.

Let

a ∈ A e ∪ A o , a = C(k e ).
As the only execution rule that modies A e ∪ A o is the (GEN) rule, on Figure 4, there exists π ∈ k e and a prex k ′ e of k e , noted k ′ e ⊑ k e such that a = ξ(k ′ e , π).

RR n°8015

Let (W, s, i) ∈ a, by Denition 8 of ξ, we have:

∃b, h ∈ N, (W, s, b, h) ∈ π ∧ i ∈ [α, α + h[, α = π ′ ∈k ′ e (u,s,b ′ ,h ′ )∈π ′ b ′
Furthermore, the restrictions imposed on the set of well-formed activation points Π, in Denition 5, requires that b = h, which yields from Denition 9:

C(k ′ e .π) = (u, s ′ , i ′ ) ∈ X | i ′ π ′ ∈k ′ e .π (u,s ′ ,b ′ ,h ′ )∈π ′ b ′ = (u, s ′ , i ′ ) ∈ X | i ′ α + b α + h We deduce that i ′ / ∈ [α, α + h[ and therefore that (W, s, i) / ∈ C(k ′ e .

π).

A similar reasoning allows to show that C is monotonically decreasing:

∀k ′ e ⊑ k e , C(k e ) ⊆ C(k ′ e )
, which nally yields:

∀a ∈ A e ∪ A o , a = C(k e ), (W, s, i) ∈ a ⇒ (W, s, i) / ∈ C(k e )
Finally, we need to prove that the same result holds when a = C(k e ) ∧ a ′ = C(k e ). In this case, both task activations are the result of the application of the (GEN) rule:

∃π, π ′ ∈ k e , ∃k ⊑ k e , ∃k ′ ⊑ k e : a = ξ(π, k) ∧ a ′ = ξ(π ′ , k ′ )
Let us consider k and k ′ satisfying the relation above. The Denition 8 of ξ, yields:

∃b, h ∈ N, (W, s, b, h) ∈ π ∧ i ∈ [α, α + h[, α = p∈k (u,s,β,η)∈p β ∃b ′ , h ′ ∈ N, (W, s, b ′ , h ′ ) ∈ π ′ ∧ i ∈ [α ′ , α ′ + h ′ [, α ′ = p ′ ∈k ′ (u,s,β ′ ,η ′ )∈p ′ β ′
Without loss of generality, assume that k ′ ⊑ k. We further assume, by way of contradiction, that there exists (W, s, i) ∈ a, (W, s, i) ∈ a ′ and a = a ′ . In this case, we directly obtain the stronger relation k

′ .π ′ ⊑ k from (GEN) and a = a ′ . From k ′ .π ′ ⊑ k, we deduce that α ′ + b ′ ≤ α, and the requirements in Denition 5 that b = h and b ′ = h ′ lead to a contradiction: i belongs to the two disjoint intervals [α ′ , α ′ + b ′ [ and [α, α + b[.

Program Progress and Deadlock

Based on the execution rules above, we dene a simple articial measure of program progress that adds the length of the control program trace to the number of executed activations:

|(k e , A e , A o )| = |k e | + |A e |
Note that all rules on Figure 3, except This measure and the denition of program progress could be construed as awed if we do not accept schedules where an innite sequence of (GEN) occurs. Intuitively there is no point in generating an innity of activations if they never get executed, and a bounded memory model would yield a resource deadlock. However, under the current unbounded memory assumption for the CDDF model, we admit such schedules as correct. The resulting denition of deadlock corresponds to the impossibility of progress from a given state.

Ω(k e ) / ∈ Π ∧ A o = {C(k e )} ∧ ∀a ∈ A o , ¬A e ⋉ a
Proof. Denition 14 states that a deadlock occurs when no rule can be red in a given state of the program:

D(σ) ⇔ ¬(GEN) ∧ ¬(BAR) ∧ ¬(TERM) ∧ ¬(EXEC)
From the denition of the execution rules on Figure 3 and using Ω(k e ) = barrier ∧ Ω(k e ) = ⊤ ⇔ Ω(k e ) ∈ Π to merge the conditions for (BAR) and (TERM), we can derive the following equivalence, which simplies in the desired property:

D(σ) ⇔    A o = {C(k e )} ∨ Ω(k e ) ∈ Π ∧ Ω(k e ) / ∈ Π ∧ ∀a ∈ A o : ¬A e ⋉ a

Deadlock Characterization

In order to dene the dierent types of deadlocks that can occur in our model, we rst need to introduce a ow dependence relation on task activations. We will use Bernstein's denition of data dependences [START_REF] Bernstein | Program analysis for parallel processing[END_REF] and adjust it to task activations. As stream accesses are in single assignment and all correct reads come, by denition, after the unique write operation, only read-after-write dependences are possible.

Denition 16 (Task activation dependence relation). We dene the data ow dependence relation between task activations δ ∈ P(A 2 ) using the common denition of ow dependences,

∀(a, a ′ ) ∈ A 2 : a δ a ′ ∃(s, i) ∈ S × N, (W, s, i) ∈ a ∧ (R, s, i) ∈ a ′
As with the stream prex order relation, we derive a relation ∆ ∈ P(A) × A modeling the fundamental scheduling constraint corresponding to a set of task activations A satisfying all ow dependences for the execution of a task activation a:

A ∆ a ∀(R, s, i) ∈ a, ∃a ′ ∈ A, (W, s, i) ∈ a ′
This relation, pronounced A satises the dependences of a, means that write access operations belonging to the task activations in A cover all the read operations in a, so all ow dependences of a are satised by the execution of the task activations in A.

From this denition, it is easy to see that the stream prex order enforced in the CDDF model is more restrictive than necessary. We do not detail the proof of the following proposition, as it directly results from Denitions 11 and 16.

Proposition 17. Flow dependences are subsumed by the stream prex order relation.

∀a, a ′ ∈ A : a δ a ′ ⇒ a < a ′ ∀a ∈ A, ∀A ∈ P(A) : A ⋉ a ⇒ A ∆ a
The second relation in this proposition means that enforcing the stream prex order is sucient to enforce ow dependences in CDDF programs, which is a direct consequence of the rst relation. We also provide the following lemma which guarantees that the continuation activation can never be a candidate for execution, irrespectively of the dependence relation used.

Lemma 18. For a CDDF program in state σ = (k e , A e , A o ), the dependences of the continuation activation, C(k e ), are never satised by

A e ∪ A o \ {C(k e )}.
Proof. The proof of this lemma hinges on two properties: (1) A e ∪ A o \ {C(k e )} is a nite set of task activations, each containing a nite number of write operations by denition of ξ and Π; and

(2) C(k e ) contains an innite number of read stream accesses. All ow dependences associated with read accesses of C(k e ) cannot be satised by a nite number of writes.

The earlier blanket denition of deadlocks can be further rened, based on the source of the deadlock, in three categories: functional deadlocks, insuciency deadlocks and spurious deadlocks. We will respectively note FD(σ), ID(σ) and SD(σ) when a functional, insuciency or spurious deadlock occurs in state σ. We informally dene these deadlock types as follows.

Functional deadlocks occur when all outstanding activations have unsatised ow dependences and the control program cannot make progress. This type of deadlocks corresponds to an algorithmic error, in situations where no schedule preserving ow dependences can exist, for example because of an unsatisable ow dependence cycle.

Insuciency deadlocks occur when the control program cannot make progress, because of a synchronization point or because of its termination, and insucient data has been scheduled to be produced to meet the requirements of consumers in some stream. The control program cannot generate any more task activations that could produce the missing data and there is at least one outstanding task activation that cannot execute. In our model, this happens if an outstanding activation depends on C(k e ) and the control program cannot make progress.

Spurious deadlocks are all remaining deadlocks, which are due to the over-synchronization scheme we enforce rather than a more fundamental issue. While insuciency and functional deadlocks are a program correctness issue, arising from algorithmic errors, which cannot be resolved and are considered to fall under the programmer's responsibility, the presence of spurious deadlocks underscores inconsistencies in our model, induced by the over-synchronization of ow dependences.

A fourth type of deadlocks, resource deadlocks, stem from the limitations of the amount of memory available for stream buers or outstanding activations, so they are naturally absent from this unbounded memory abstraction. Inria

Functional deadlocks

The denition of functional deadlocks is similar to that of CDDF deadlocks. They occur when no progress can be made in a program where only ow dependences (Denition 16) are enforced instead of our over-approximated stream prex order (Denition 11).

Denition 19 (Functional deadlock). A CDDF program is in a functional deadlock in state σ, and we note FD(σ), if no execution rule can apply in that state, replacing rule (EXEC) with:

(EXEC∆)

A o = {a} ∪ A ′ o A e ∆ a (k e , A e , A o ) -→ (k e , A e ∪ {a}, A ′ o )
We can prove the following property of functional deadlock states, using the same reasoning as that of Lemma 15.

Lemma 20 (Functional deadlock state). A CDDF program is in a functional deadlock state σ = (k e , A e , A o ), noted FD(σ), i:

Ω(k e ) / ∈ Π ∧ A o = {C(k e )} ∧ ∀a ∈ A o , ¬A e ∆ a

Insuciency deadlocks

Insuciency deadlocks represent deadlocks where the control program stopped too early and did not generate the task activations necessary for the completion of the existing outstanding task activations, which is why their denition relies on the continuation activation. Note, however, that we primarily use the ow dependence relation rather than the stream prex order, and that there is no equivalence between the corresponding deadlock states. We will get an equivalence once we relax the denition of deadlock states.

Denition 21 (Insuciency deadlocks). A CDDF program is in an insuciency deadlock in

state σ = (k e , A e , A o ), and we note ID(σ), when the control program cannot make progress and all outstanding task activations depend, transitively, on the continuation activation:

Ω(k e ) / ∈ Π ∧ A o = {C(k e )} ∧ ∀a ∈ A o , C(k e ) δ + A o a
We similarly dene insuciency deadlocks on the stream prex order (Denition 11), and we note ID < (σ):

Ω(k e ) / ∈ Π ∧ A o = {C(k e )} ∧ ∀a ∈ A o , C(k e ) < + A o a
Lemma 22. All insuciency deadlocks are functional deadlocks. A CDDF program in a state σ = (k e , A e , A o ) veries:

ID(σ) ⇒ FD(σ)
Proof. The proof relies on Lemma 18, which ensures that the continuation activation is never executable with (EXEC ∆ ):

¬ (A e ∪ A o \ {C(k e )}) ∆ C(k e )
Denition 21 can be rewritten and expanded from the denition of ow dependences,

ID(σ) ⇒ ∀a ∈ A o , C(k e ) δ + A o a : ⇒ ∀a ∈ A o , ∃a ′ ∈ A o , C(k e ) δ * A o a ′ ∧ a ′ δ a ⇒ ∀a ∈ A o , ∃a ′ ∈ A o , ∃(s, i), (W, s, i) ∈ a ′ ∧ (R, s, i) ∈ a ⇒ ∀a ∈ A o , ∃(R, s, i) ∈ a, ∀a ′ ∈ A e , (W, s, i) / ∈ a ′ ⇒ ∀a ∈ A o , ¬ A e ∆ a

Spurious deadlocks

We nally dene spurious deadlocks as non-functional deadlocks.

Denition 23 (Spurious deadlock). A spurious deadlock is a non-functional deadlock. For a state σ = (k e , A e , A o ), we write:

SD(σ) D(σ) ∧ ¬FD(σ)
This is the only type of deadlock that results from our over-approximation of ow dependences (Denition 11) and not from program semantics. Our primary objective is to ensure that we can avoid such deadlocks in CDDF programs.

Weak deadlock states

In many cases, we are able to show that the program will necessarily deadlock in the future of a given state, without knowing precisely when it will deadlock or whether the current state is already a deadlock state. A state from which all execution schedules lead to a deadlock will be called a weak deadlock state. The purpose here is to switch from universal quantiers in the conditions of deadlock states to existential quantiers in the conditions of weak deadlocks.

′ = (k ′ e , A ′ e , A ′ o ) such that: *D(σ ′ ) ∧ |σ| |σ ′ | ∧ k e = k ′ e
We respectively note WD(σ), WFD(σ), WID(σ) and WSD(σ) when the state σ satises the weak deadlock condition respectively for a general deadlock, a functional deadlock, an insuciency deadlock or a spurious deadlock. This denition is entirely directed at simplifying the denition of deadlock states. As we require D(σ ′ ) ∧ k e = k ′ e , we ensure that the control program cannot make further progress and therefore cannot generate new task activations:

Ω(k ′ e ) = Ω(k e ) ∈ {barrier , ⊤}
This condition is very important as it precludes a form of live-lock where only a part of the program is in a deadlock, the remainder progressing possibly indenitely if the program is nonterminating.

It also preserves the continuation activation, as it depends only on the control program trace. As only the (EXEC) rule can apply we have:

A ′ o ⊆ A o
This ensures that |σ ′ | -|σ| is nite, so the maximum number of transitions required to reach a deadlock state is nite.

Weak insuciency deadlock state

This weaker denition of deadlock states allows to reason in terms of local deadlock conditions, using an existential quantier, rather than global conditions, universally quantied over all outstanding task activations. For example, a program is in an insuciency deadlock state only if all outstanding activations depend on the continuation activation, but we show that it is sucient Inria to know that a single outstanding activation depends on the continuation C(k e ), once the control program reaches a barrier, to conclude to a weak insuciency deadlock state. For instance, these weaker conditions allow proving the equivalence of weak insuciency deadlock states when occurring due to the enforcement of ow dependences or of the stream prex order.

Lemma 25 (Weak insuciency deadlock state). A CDDF program state σ = (k e , A e , A o ), veries

WID(σ) ⇔ Ω(k e ) / ∈ Π ∧ ∃a ∈ A o , a = C(k e ) ∧ C(k e ) δ a ⇔ Ω(k e ) / ∈ Π ∧ ∃a ∈ A o , a = C(k e ) ∧ C(k e ) < a
Proof. By Denition 24 there exists

σ ′ = (k ′ e , A ′ e , A ′ o ) such that: WID(σ) ⇒ ID(σ ′ ) ∧ |σ| |σ ′ | ∧ k e = k ′ e
Which can be expanded using Denition 21 for ID(σ ′ ):

Ω(k ′ e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , C(k e ) δ + A ′ o a
Knowing that A ′ o = {C(k e )}, and in any program state

{C(k e )} ∈ A ′ o , there is a ′ ∈ A ′ o , a ′ = C(k e ) ∧ C(k e ) δ a ′ .
As k e = k ′ e , there can be no task activation generation in between the two states of the program, so A ′ o ⊂ A o , and therefore a ′ ∈ A o , which allows us to conclude:

WID(σ) ⇒ Ω(k e ) / ∈ Π ∧ ∃a ∈ A o , a = C(k e ) ∧ C(k e ) δ a
To prove the ⇐ direction, let us consider state o satises C(k e ) δ a, which concludes this second part of the proof. Finally, to prove the equivalence of weak deadlock states dened by either of the δ or < relations, we show that:

σ ′ = (k e , A e ∪ A o \ {C(k e ),
∀a ∈ A o , C(k e ) < a ⇔ C(k e ) δ a
Proposition 17 yields ∀a ∈ A o , C(k e ) < a ⇐ C(k e ) δ a, so we need only prove the reverse in order to conclude this proof. By denition of the stream prex order, C(k e ) < a i:

∃s ∈ S, ∃i, j ∈ N, j i ∧ (W, s, j) ∈ C(k e ) ∧ (R, s, i) ∈ a
From the Denition 9 of the continuation activation, we deduce:

∀s ∈ S, ∃α ∈ N : ∀k ∈ N, (W, s, k) ∈ C(k e ) ⇒ k α
Which allows us to conclude: (W, s, j) ∈ C(k e ) ⇒ j α. As j i, we further deduce that:

(W, s, j) ∈ C(k e ) ⇒ i j α ⇒ (W, s, i) ∈ C(k e )
By denition of the ow dependence relation,

(W, s, i) ∈ C(k e ) ∧ (R, s, i) ∈ a ⇒ C(k e ) δ a.
Note that this equivalence of weak insuciency deadlock states is possible only because we do not require a global condition on the set of outstanding activations. Indeed, the real insuciency deadlock states are possibly dierent when enforcing either of the constraints, but the cause is the same: these deadlocks represent states where insucient data can be produced on some streams, which are lled incrementally and therefore any data missing in the prex of a stream index leads to data missing in the remainder.

We can show that a state σ satises:

ID < (σ) ⇒ WID(σ) ⇐ ID(σ)
This is sucient to say that any insuciency deadlock stems from an unsatisable ow dependence. Even though our over-synchronization scheme may cause the program to deadlock earlier, we do not introduce additional deadlocks.

2.5.6

Weak functional deadlock state

The characterizations of weak functional deadlock states and of general CDDF weak deadlock states are very similar, and their proofs identical, so we present them at the same time. Note that this denition is very general, thanks to the continuation activation modeling the future schedule of data in streams, and encompasses all types of deadlocks.

Lemma 26 (Weak (functional) deadlock state). All deadlocks result from the presence of a cycle between task activations based on the order relation corresponding to the deadlock type.

For a CDDF program in state σ = (k e , A e , A o ), we have:

WD(σ) ⇔ Ω(k e ) / ∈ Π ∧ A o = {C(k e )} ∧ ∃a ∈ A o , a = C(k e ), a < + A o a ∨ C(k e ) < + A o a WFD(σ) ⇔ Ω(k e ) / ∈ Π ∧ A o = {C(k e )} ∧ ∃a ∈ A o , a = C(k e ), a δ + A o a ∨ C(k e ) δ + A o a
Proof. We only present the proof for WD(σ), that of WFD(σ) is identical. We rst show that, in a weak deadlock state, we can always either nd a dependence cycle or a dependence chain starting at C(k e ).

Let us consider σ = (k e , A e , A o ) such that WD(σ) which by denition implies that

∃σ ′ , D(σ ′ ) ∧ k e = k ′
e , and we expand:

∃σ ′ , Ω(k e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , ¬A ′ e ⋉ a
We use Denition 11 of the stream prex order, yielding:

∀a ∈ A ′ o , ∃(R, s, i) ∈ a, ∃j i, ∀a ′ ∈ A ′ e , (W, s, j) / ∈ a ′
Proposition 10 ensures that all stream accesses are covered by an activation in

A ′ e ∪ A ′
o and since (W, s, j) is not present in activations from A ′ e , it necessarily belongs to an activation in A ′ o :

∀a ∈ A ′ o , ∃(R, s, i) ∈ a, ∃j i, ∃a ′ ∈ A ′ o , (W, s, j) ∈ a ′ ⇔ ∀a ∈ A ′ o , ∃a ′ ∈ A ′ o : a ′ < a
We can recursively build a chain ... < a ′′ < a ′ < a by applying this last proposition to a, then a ′ which satises a ′ < a and so on. As A ′ o is a nite set, we deduce that either we stop once we reach the continuation activation or there must be at least one cycle. As A ′ o = {C(k e )}, we can choose a = C(k e ), which concludes the rst part of the proof.

Inria

The proof of the reverse simply requires building a state σ ′ with A ′ o = {C(k e ), a 1 , a 2 , ..., a n }, where a 1 ...a n are the activations forming the cycle or the dependence chain, which is a deadlock state as the cycle or the dependence on the continuation prevents any activation to be executable:

∀a ∈ A ′ o , ∃a ′ ∈ A ′ o , a ′ < a ⇒ ¬ A ′ e ⋉ a 2.
WID(σ) ⇒ WFD(σ) ⇒ WD(σ)
And the denition of spurious deadlocks is preserved:

WSD(σ) ⇔ WD(σ) ∧ ¬WFD(σ)
Proof. The rst part of this proof is a direct result of Lemma 22:

WID(σ) ⇒ ∃σ ′ , ID(σ ′ ) ⇒ FD(σ ′ ) ⇒ WFD(σ)
To prove that WFD(σ) ⇒ WD(σ), we need only consider Lemmas 15 and 20, which respectively provide the characterization of a deadlock and a functional deadlock state.

WFD(σ) ⇒ ∃σ ′ , FD(σ ′ ) ⇒ ∃σ ′ , Ω(k e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , ¬A ′ e ∆ a ⇒ ∃σ ′ , Ω(k e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , ¬A ′ e ⋉ a ⇒ ∃σ ′ , D(σ ′ ) ⇒ WD(σ)
On the third line, we use Proposition 17 which gives A ′ e ⋉a ⇒ A ′ e ∆a or conversely ¬(A ′ e ∆a) ⇒ ¬(A ′ e ⋉ a).

In the remainder of this paper, we analyze the properties of the CDDF model, we provide conditions under which our model does not introduce spurious deadlocks and we prove the serializability and the determinism of CDDF programs.

Stream Causality

This section starts by introducing the notion of stream causality and a characterization of stream causal programs based on the existence of stream causal schedules. In a second step, we prove that CDDF programs that are stream causal, in each state where the control program waits for a barrier, are free of all forms of deadlocks.

Characterization of Stream Causality

As our model is asynchronous, we cannot use a global notion of time as a basis for the denition of causality. Instead, we can use streams as a set of independent local clocks. Each stream can be considered to dene its own time based on access indexes, each task activation representing a synchronization point between the clocks of the streams it writes to and, to a lesser extent, those it reads from. As write accesses to streams are exclusive in our single assignment model, we can dene the Stream Clock (SC) of an activation as its ordered set of write accesses. More importantly, this allows us to dene a precedence relation between task activations producing data in the same stream. This relation is a subset of the total order on activations induced by the control program order.

∀a, a ′ ∈ A e ∪ A o , a sc a ′ ∃s ∈ S, ∃i, j ∈ N, j i ∧ (W, s, j) ∈ a ∧ (W, s, i) ∈ a ′
We extend this relation to order sink task activations 5 with C(k e ). This ensures that the continuation activation is an upper bound:

∀a ∈ A e ∪ A o : a sc C(k e )
This relation is antisymmetric by denition of the activation point evaluation function ξ (Denition 8), as it enforces a consistent schedule of write access indexes in all streams. The underlying order relation is the precedence of activation points in the control program trace: if task activations a, a ′ are the result of the evaluation of activation points π, π ′ , then the order of occurrence of these activation points in the control program trace determines the direction of the precedence relation sc :

a sc a ′ ⇒ π = π ′ ∨ π → π ′
Causality naturally stems from ow dependence chains between task activations. We thus root the denition of stream causality in the compatibility of task activation order with δ + . But satisfying these dependence chains is not sucient in our model. Indeed, dependence chains do not order a given read access (R, s, i) w.r.t. write accesses (W, s, j) j<i occuring in the prex of (W, s, i) on stream s. We dene stream causality in CDDF programs as the absence of time reversal inside dependence chains.

Denition 29 (Stream causality). A CDDF stream s ∈ S is stream causal in a state σ = (k e , A e , A o ) of a program if the stream's local clock progresses forward along all dependence chains:

∀a, a ′ ∈ A e ∪ A o , ¬(a = a ′ = C(k e )), s ∈ O(a) ∩ O(a ′ ) : ¬ a sc a ′ ∧ a ′ δ + A e ∪ A o a
The restriction ¬(a = a ′ = C(k e )) means that we do not check the causality of the barrier itself; this precaution is necessary as C(k e ) sc C(k e ) and C(k e ) δ C(k e ) are always true. This validates our intuition that the continuation activation is inherently non-causal. However, as long as the continuation activation is only found at the end of dependence chains, it does not preclude stream causality.

A CDDF program is stream causal in a state σ if each stream in the program is causal. We note:

SC(σ) ∀a, a ′ ∈ A e ∪ A o , ¬(a = a ′ = C(k e )) : ¬ a sc a ′ ∧ a ′ δ + A e ∪ A o a
Note that stream causality is entirely determined by the schedule of data in streams and not by the execution schedule of task activations. For this reason, the causal nature of a CDDF program state only depends on the control program's trace in that state. This can be seen in Denition 29 where no dierence is made between executed and outstanding activations. As a result, stream causality is well dened for a given program, since the control program itself is deterministic.

A second important remark is that our choice of modeling the behaviour of barriers through the continuation activation is entirely consistent with this denition of stream causality. The stream clock of this activation is greater than that of any task activation generated by the control program, which properly models the possible continuation of the program after the barrier passes. The restriction, in Denition 29, that we do not check the causality of the barrier itself, means that the current state of the program does not allow us to deduce whether its future will or will not be causal.

Stream causality violations represent conicts between ow dependences and stream clocks. To model causal program schedules, we dene the minimal constraints for scheduling functions that respect both forward time in each stream and ow dependences.

Denition 30 (Stream causal schedule). A scheduling function

θ : A → N enforces a stream causal schedule i: ∀(a, a ′ ) ∈ A : a δ + A e ∪ A o a ′ ⇒ θ(a) < θ(a ′ ) a sc a ′ ⇒ θ(a) θ(a ′ )
We use the existence of stream causal schedules, irrespectively of their capacity to enforce the stream prex order, to characterize stream causality in CDDF programs. According to Denition 29, the schedule of the execution of task activations is only constrained by ow dependences, and the forward progress of time on stream clocks. In general, we only need to know whether a stream causal schedule exists, but we do not enforce it on the execution of task activations.

Proposition 31 (Stream Causal CDDF program). A CDDF program is causal in a state σ = (k e , A e , A o ) if and only if the program admits at least one stream causal schedule for task activations belonging to A e ∪ A o .

Proof. We rst prove that program stream causality is necessary to the existence of a stream causal schedule, according to our denitions. Let us assume, by way of contradiction, that the program is not causal in a state σ = (k e , A e , A o ). There exist a, a ′ ∈ A e ∪ A o such that:

¬(a = a ′ = C(k e )) ∧ a sc a ′ ∧ a ′ δ + A e ∪ A o a
Which means that any scheduling function θ enforcing a stream causal schedule in state σ meets the following constraints:

(θ(a) θ(a ′ )) ∧ (θ(a ′ ) < θ(a))
This contradiction allows us to conclude to the impossibility.

Let us consider a scheduling function θ that enforces all ow dependences. This schedule, which is obtained by using the (EXEC ∆ ) transition rule, satises, by denition:

∀a, a ′ ∈ A e ∪ A o : a δ + A e ∪ A o a ′ ⇒ θ(a) < θ(a ′ )
We need to show that this schedule is admissible (i.e. that it can indeed be executed) and that a sc a ′ ⇒ θ(a) θ(a ′ ) is veried in this schedule. We remark that a sc a is always true for activations that contain at least one write access, which is necessarily the case if an activation is the source of a ow dependence, which we inject in Denition 29, deducing that:

∃a ∈ A e ∪ A o , a = C(k e ), a δ + A e ∪ A o a ⇒ ¬SC(σ)
This means that stream causality in a state precludes ow dependence cycles between task activations. Furthermore, as all activations are in a stream clock precedence relation with the continuation activation:

∃a ∈ A e ∪ A o , a = C(k e ), C(k e ) δ + A e ∪ A o a ⇒ ¬SC(σ)
As there can be no cycles and no dependence chains containing the continuation activation, Lemma 26 allows us to conclude that this state is not a weak functional deadlock state, irrespectively of the fact that the control program has reached a barrier or not. This means that this schedule built on (EXEC ∆ ) is able to schedule all task activations in A e ∪ A o . As a side note, this already proves that a CDDF program that is stream causal every time the control program reaches a barrier cannot experience functional deadlocks.

Let us verify that, in a stream causal program state, this schedule is itself stream causal. From the denition of stream causality, we have:

∀a, a ′ ∈ A e ∪ A o , ¬(a = a ′ = C(k e )) : a sc a ′ ⇒ ¬(a ′ δ + A e ∪ A o a)
We deduce that a sc a ′ ⇒ ¬(a ′ δ + A e ∪ A o a) ⇒ ¬(θ(a ′ ) < θ(a)) ⇒ θ(a) θ(a ′ ), which concludes the proof.

A o = {a 1 , a 2 , a 3 } where      a 1 = {(W, s 1 , 0), (R, s 2 , 0} a 2 = {(R, s 1 , 0)} a 3 = {(R, s 1 , 1), (W, s 2 , 0)} Inria
The gure below shows the true dependences δ as well as the additional constraints < on stream prexes. It also marks, for the discussion, the stream clock relation sc between activations a 1 and a 4 .

The following ow dependences are present in this state:

a 4 δ a 3 a 3 δ a 1 a 1 δ a 2
As ow dependences allow the simple schedule (a 3 , a 1 , a 2 ) to complete the execution, considering that a 4 has already been executed, there is no functional deadlock. However, the addition of the stream prex constraint leads to a cycle between activations a 1 and a 3 , and therefore to a deadlock when the control program reaches a barrier:

a 4 < a 3 a 3 < a 1 a 1 < a 2 and a 1 < a 3
The intuition we get from this example is that a stream causality violation, between activations a 4 and a 1 , was the necessary element allowing this spurious deadlock to occur:

a 1 sc a 4 ∧ a 4 δ a 3 δ a 1 ⇒ θ(a 4 ) < θ(a 1 ) θ(a 4 ) ⇒ ¬SC(σ)
Though stream causality is a strong condition that is not decidable at compilation time, it is a semantically important condition for deadlock-freedom, and for some strong forms of serializability, as we will show in Section 6.2.

This shows stream causality is a relaxed form of Cilk strictness [START_REF] Frigo | The implementation of the Cilk-5 multithreaded language[END_REF], which is dened as the absence of transverse dependences between dierent branches of the task creation tree, requiring that all dependences be synchronized by a task's parent. Semantically, strictness means that a task should always be executable (i.e., all its dependences should be satised) at the spawn point. In the CDDF model, this can be understood in a more relaxed way as requiring that all write stream accesses necessary for a task's execution be already scheduled by the control program when it reaches the task's activation point; in other words that all dependences should be forward in the control program, which ensures stream causality in each state of the CDDF program.

Theorem 33. A CDDF program is free of all deadlocks if it is stream causal in each state σ = (k e , A e , A o ) where the control program reaches a barrier or terminates. All states σ satisfy:

SC(σ) ⇒ ¬WD(σ)
Proof. We prove this theorem by showing that SC(σ) ∧ WD(σ) is impossible. Let us assume, by way of contradiction, that σ = (k e , A e , A o ) is such a state.

We rewrite the Denition 11 of the stream prex order in terms of ow dependences and the stream clock relation:

∀a, a ′ ∈ A e ∪ A o , a < a ′ ⇔ ∃(s, i) ∈ S × N, ∃j i, (W, s, j) ∈ a ∧ (R, s, i) ∈ a ′
Proposition 10 yields ∃a ′′ ∈ A e ∪ A o , (W, s, i) ∈ a ′′ , which we add to the expression above to conclude that:

∀a, a ′ ∈ A e ∪ A o , a < a ′ ⇔ ∃a ′′ ∈ A e ∪ A o , a sc a ′′ ∧ a ′′ δ a ′
As the program is causal in this state, Proposition 31 guarantees the existence of at least one stream causal schedule in this state. Let θ be a scheduling function for such a schedule. By Denition 30 of a stream causal schedule, for a, a ′ ∈ A e ∪ A o we have:

a < a ′ ⇒ ∃a ′′ ∈ A e ∪ A o , θ(a) θ(a ′′ ) ∧ θ(a ′′ ) < θ(a ′ ) ⇒ θ(a) < θ(a ′ )
Expanding Lemma 26 for the weak deadlock state σ yields:

∃(a 1 , ..., a n ) ∈ A n o , a 1 = C(k e ), a 1 < ... < a n < a 1 ∨ C(k e ) < a 1 < ... < a n
Where we substitute the scheduling function constraints on <:

θ(a 1 ) < θ(a 2 ) < ... < θ(a n ) < θ(a 1 ) ⇒ θ(a 1 ) < θ(a 1 ) θ(C(k e )) < θ(a 1 ) < ... < θ(a n ) ⇒ θ(C(k e )) < θ(a n )
Both results are contradictory. The rst trivially, the second because a n sc C(k e ) is always true, by Denition 28, so θ(a n ) θ(C(k e )) and θ(C(k e )) < θ(a n ), concluding this proof.

To illustrate the concept of stream causality, let us consider our running example, the FIR application on Figure 2. This program is only causal as long as the control program does not evaluate the rst activation point π B 0 , generating the rst task activation a B 0 . Indeed, let us consider for example that the program reaches a state σ = (k e , A e , A o ) and there exists

i ∈ N such that k e = π A 0 .π B 0 .π C 0 ...π A i-1 .π B i-1 .π C i-1 .π A i .π B i .
We have:

a B i = (R, istream, j) i≤j<i+N , (W, ostream, i)
However, the highest write access index attributed on stream istream belongs to a A i = (W, istream, i) , which means that ∀j ∈ N, i + 1 ≤ j < i + N, (W, istream, j) ∈ C(k e ). We deduce that C(k e ) δ a B i and as a B i sc C(k e ) is always true, we deduce that ¬SC(σ). This does not mean that a deadlock will occur in this program, but rather that this program would only deadlock either at termination if the loop were nite or at any barrier that would be added. In such a case, an insuciency deadlock would occur.

This program can be simply transformed to ensure it is stream causal in each state. Indeed, the main issue is that the task activations a B i , resulting from the second task construct, contain read access indexes in istream that have not been assigned to a producer when π B i is evaluated. Figure 6 shows the stream causal version of this program, where a delay of N data items is introduced on stream istream before the main program loop begins. With this addition, the main program loop can exit at any time, or we can introduce barriers in the control program at any point, without causing a deadlock.

Task Causality

While stream causality is sucient to prove deadlock-freedom, we can prove less restrictive conditions, ensuring that only insuciency deadlocks can occur. In this section, we present two alternative conditions for deadlock-freedom and the formal framework for their analysis. We have avoided, until now, the additional complexity of introducing a denition of tasks in the CDDF model, as they play a secondary role. We use a weak denition of tasks as equivalence classes of task activations, disregarding the work functions.

Denition 34 (CDDF task). A task is an equivalence class in the set of task activations based on the following equivalence relation ∼ ∈ P(A 2 ) dened for (a, a ′ ) ∈ A 2 as:

a ∼ a ′ ∀(u, s, i) ∈ a, ∃i ′ ∈ N, (u, s, i ′ ) ∈ a ′ ∀(u, s, j ′ ) ∈ a ′ , ∃j ∈ N, (u, s, j) ∈ a I(a) = I(a ′ ) ∧ O(a) = O(a ′ )
Two activations are equivalent in this relation i they access exactly the same streams, both for input and for output. The set of tasks in a CDDF program in a state σ = (k e , A e , A o ) is the quotient space of the set of task activations:

T (σ) = (A e ∪ A o \ {C(k e )}) /∼
For a task activation a, we write [a] ∼ its equivalence class on the ∼ relation; it is the CDDF task to which activation a belongs.

Using this denition, we can build the task graph of a program state. We note S(σ) the set of streams used by a program in state σ, dened as the set of streams accessed by any activation in σ:

S(k e , A e , A o ) a∈Ae∪Ao\{C(ke)} I(a) ∪ O(a)
Denition 35 (Task graph). A CDDF program in a state σ = (k e , A e , A o ) can be represented as a directed hypergraph:

H(σ) = T (σ), S(σ)
where tasks are vertices and streams are directed hyperedges connecting a set of producer tasks to a set of consumer tasks.

For a program in state σ and a stream s ∈ S(σ), we dene the sets of producer tasks P (σ, s) and of consumer tasks C(σ, s) as:

P (σ, s) = [a] ∼ ∈ T (σ) | s ∈ O(a) C(σ, s) = [a] ∼ ∈ T (σ) | s ∈ I(a)
Despite the fact that, by denition, C(k e ) is a producer and consumer of each stream, we do not count the continuation activation in any producer or consumer set. This task graph clearly depends on the current state of the control program, and is therefore dynamic.

Task Causality

We derive, from the control program order, a precedence relation on task activations, called task order. The stream access indexes of activations dene a total order on the activations within the task. This order is induced by the denition of the activation point evaluation function ξ and the total order of activation points in the trace of the control program.

Denition 36 (Task order). Task activations belonging to the same task in a program state σ = (k e , A e , A o ) are ordered by the relation t ∈ P(A 2 ), for (a, a ′ ) ∈ A e ∪ A o we dene:

a t a ′ a ∼ a ′ ∧ ∀s ∈ I(a) ∪ O(a), ∃i, j ∈ N, j i, (u, s, j) ∈ a, (u, s, i) ∈ a ′
This relation is transitive as we restrict it to a ∼ a ′ , reexive because we use j i and antisymmetric by construction of task activations in the evaluation function ξ. However, its extension to all task activations is not an order relation as it lacks transitivity. This order relation is very similar to the stream clock relation, sc , that we introduced in the previous section, which was used to dene stream causality. We will use here the task order relation to dene task causality in the same way.

Denition 37 (Task causality). A CDDF task is causal in a state σ = (k e , A e , A o ) of a program if the task's activations appear in task order along all dependence chains:

∀t ∈ T (σ), ∀a, a ′ ∈ t, ¬ a t a ′ ∧ (a ′ δ + A e ∪ A o a)
A CDDF program is task causal in a state σ, and we note T C(σ), i each task in the program is causal in that state.

∀a, a ′ ∈ A e ∪ A o \ {C(k e )}, ¬ a t a ′ ∧ (a ′ δ + A e ∪ A o a)
Note that this denition revisits process monotonicity in Kahn networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], though the related notion of process is slightly dierent from our quotient tasks. Indeed, our denition requires that no ow dependence chain goes back in task order, which would mean that the execution of task activation a ′ enables the latter execution of a. Because a t a ′ , the outputs of a are written in the prex of the outputs of a ′ , so Kahn's monotonicity is preserved if task [a] ∼ is the single consumer and the single producer on its streams. Our denition of task causality generalizes Kahn's monotonicity to cases where other tasks share these streams. At the limit, as stream prexes grow into complete streams, our denition reproduces the Kahn principle: continuity of the communicating processes. 6Furthermore, this property is weaker than stream causality, because the stream clock relation is dened across task activations producing data in a given stream, even if these activations are not in the same task. For a, a ′ ∈ A, we have:

a sc a ′ ⇒ ∃s ∈ S, ∃j i, (W, s, j) ∈ a ∧ (W, s, i) ∈ a ′ ⇒ a ∼ a ′ ⇒ a t a ′
The only exception are sink tasks, that are only consumers, and in which activations are only in a stream clock precedence relation with the continuation activation. We extended the stream clocks relation in that case, but task causality does not allow the same simplication. Indeed, as we have discussed above, the continuation activation does not belong in any task, because tasks are dened as equivalence classes of task activations and the continuation activation is the only activation that has an innite number of input and output streams. For this reason, the continuation activation can never be in a task order relation t with task activations.

Denition 38 (Task causal schedule). A scheduling function

θ : A → N enforces a task causal schedule i: ∀a, a ′ ∈ A : a δ + a ′ ⇒ θ(a) < θ(a ′ ) a t a ′ ⇒ θ(a) θ(a ′ )
Proposition 39 (Task causal CDDF program). A CDDF program is task causal in a state σ = (k e , A e , A o ) that is not a weak insuciency deadlock if and only if the program admits at least one task causal schedule in that state.

Proof. The proof of this proposition is very close to that of Proposition 31, with a simple substitution of relations and properties. The only dierence comes from the fact that contrary to stream clocks, task order does not allow ordering task activations with respect to the continuation activation. This means that the existence of a dependence chain starting at the continuation activation does not allow to conclude to a violation of causality:

∃a ∈ A e ∪ A o , a = C(k e ), C(k e ) δ + A e ∪ A o a ¬T C(σ)
For this reason, the application of Lemma 26 only allows to conclude that, in a task causal state σ, all functional deadlocks are insuciency deadlocks. The existence of the schedule depends on the absence of the weak insuciency deadlock condition C(k e ) δ + A e ∪ A o a.

Even though task causality is not a sucient condition, it constitutes a fair starting point for searching new deadlock-freedom conditions. Furthermore, this condition is weaker than the restrictions of multiple programming models, including Cilk, OpenMP tasks and models based on Cyclo-Static Data-Flow, like StreamIt.

As mentioned above, it is also a slightly weaker version of Kahn's monotonicity, and we show below that unlike Kahn networks where communication channels are always single-producer and single-consumer, we can prove that only insuciency deadlocks can occur in task causal programs where streams can be either multi-producer or multi-consumer, but not both. Theorem 40. A CDDF program can only experience insuciency deadlocks if it is task causal and each stream in the program is either single-producer or single-consumer. For σ = (k e , A e , A o ):

T C(σ) ∧ ∀s ∈ S(σ), |P (σ, s)| = 1 ∨ |C(σ, s)| = 1 ⇒ WID(σ) ∨ ¬WD(σ)
Proof. Let us consider the state σ = (k e , A e , A o ) of a program that satises the hypotheses. We use the results from Lemmas 26 and 25 instead of the denition to characterize weak deadlock states. Merging the two, we obtain:

WD(σ) ⇒ WID(σ) ∨ ∃a ∈ A o , a = C(k e ), a < + A o a
Replacing this expression in the theorem shows that our objective is to prove that no task activation cycle on the stream prex order relation can exist in such states:

T C(σ) ∧ ∀s ∈ S(σ) : |P (σ, s)| = 1 ∨ |C(σ, s)| = 1 ⇒ ¬ ∃a ∈ A o , a = C(k e ), a < + A o a
Let us assume, by way of contradiction, that the program is in a weak deadlock state σ, but not in a weak insuciency deadlock, and therefore that ∃a ∈ A o , a = C(k e ), a < + A o a. As the program is also task causal in this state, it admits a task causal schedule. Let θ be such a schedule. Expanding this cycle yields:

∃a ∈ A o , a = C(k e ), ∃n ∈ N, n > 0, ∃(a 1 , ..., a n ) ∈ A n o : a 1 = a n = a ∧ a 1 < ... < a n
From the denition of the stream prex order, we deduce that:

∀k ∈ [1, n -1], a k < a k+1 ⇒ ∃(s, i) ∈ S × N, ∃j i, (W, s, j) ∈ a k ∧ (R, s, i) ∈ a k+1
The stream s is either single-producer or single-consumer, so we will handle the cases separately.

If |P (σ, s)| = 1, then we look at the producer task activation a k and its equivalence class. Either the precise write operation (W, s, i) belongs to a task activation in this class, or this operation is not yet scheduled and therefore belongs to the continuation activation:

∃a ′ k ∈ [a k ] ∼ , (W, s, i) ∈ a ′ k ∨ (W, s, i) ∈ C(k e )
If the write operation is in the continuation activation, then we would have C(k e ) δ a k+1 , which is a weak insuciency deadlock condition and contradicts the hypothesis. We can therefore assume that (W, s, i) ∈ a ′ k and a ′ k δ a k+1 . We deduce that:

a k t a ′ k ∧ a ′ k δ a k+1 ⇒ θ(a k ) θ(a ′ k ) ∧ θ(a ′ k ) < θ(a k+1 )
We conclude that, in the case of a single-producer stream connecting a k and a k+1 , we have:

a k < a k+1 ⇒ θ(a k ) < θ(a k+1 )
If |C(σ, s)| = 1, then we look at the consumer task activation a k+1 and its equivalence class. As the higher read access operation (R, s, i) has already been scheduled to a task activation, the lower index operation (R, s, j) is guaranteed to have also been scheduled, so we know that:

∃a ′ k+1 ∈ [a k+1 ] ∼ , (R, s, j) ∈ a ′ k+1
We have a k δ a ′ k+1 and a ′ k+1 t a k+1 , which leads to:

θ(a k ) < θ(a ′ k+1 ) ∧ θ(a ′ k+1 ) θ(a k+1 ) ⇒ θ(a k ) < θ(a k+1 )
By aggregating the results of the two cases, we conclude the proof with the contradiction:

a 1 < ... < a n ⇒ θ(a 1 ) < ... < θ(a n ) ⇒ θ(a) < θ(a) Inria 4.

Strongly Connected Components

In the absence of cycles in the program hypergraph, we can show that only insuciency deadlocks can occur and Proposition 27 guarantees such deadlocks are never spurious deadlocks. While this condition may appear restrictive, it is satised by a wide class of streaming applications. Kudlur and Mahlke analyze a dozen such applications in [START_REF] Kudlur | Orchestrating the execution of stream programs on multicore platforms[END_REF] and nd that the pattern never occurs and limit their study to acyclic task graphs.

SCC (H(σ)) = ∅ ⇒ WID(σ) ∨ ¬WD(σ)
Proof. The proof of this theorem derives from Lemma 25, which characterizes a weak insuciency deadlock state, and Lemma 26, characterizing weak deadlock states as dependence cycles. To prove this theorem, we show that:

SCC(H(σ)) = ∅ ∧ ¬WID(σ) ⇒ ¬WD(σ)
Let σ be a CDDF program state where H(σ) contains no cycles and ¬WID(σ). Lemma 25 yields:

¬WID(σ) ⇔ Ω(k e ) ∈ Π ∨ (∄a ∈ A o , a = C(k e ) ∧ C(k e ) < a)
As Ω(k e ) ∈ Π gives ¬WD(σ), we only keep the condition ∄a ∈ A o , a = C(k e ) ∧ C(k e ) < a, which means that C(k e ) cannot appear in any task activation cycle in this state.

We need to show that the absence of cycles in the task graph H(σ) means that there can be no task activation cycles in A e ∪ A o \ {C(k e )}. This is intuitively simple as the program hypergraph is an over-approximation of the communication patterns in task activations where we lose the precise information on stream access indexes.

Let us assume by way of contradiction that there is a cycle of task activations in

A e ∪ A o \ {C(k e )}: ∃a 1 , ..., a n ∈ A e ∪ A o \ {C(k e )} | a 1 < a 2 < ... < a n ∧ a n = a 1
Each stream prex order relation translates, by Denition 11, into:

∀k ∈ [1, n -1] : a k < a k+1 ⇔ ∃(R, s k , i k ) ∈ a k+1 , ∃j k i k , (W, s k , j k ) ∈ a k
From the previous relation, we deduce that the set of streams (s 1 , s 2 , ...s n-1 ) satises:

         (R, s 1 , i 1 ) ∈ a 2 ∧ (W, s 2 , j 2 ) ∈ a 2 (R, s 2 , i 2 ) ∈ a 3 ∧ (W, s 3 , j 3 ) ∈ a 3 ... (R, s n , i n ) ∈ a n = a 1 ∧ (W, s 1 , j 1 ) ∈ a 1 ⇒          C(σ, s 1 ) ∩ P (σ, s 2 ) = {a 2 } = ∅ C(σ, s 2 ) ∩ P (σ, s 3 ) = {a 3 } = ∅ ... C(σ, s n ) ∩ P (σ, s 1 ) = {a 1 } = ∅
This contradicts the hypothesis of no cycles in H(σ) and therefore concludes the proof.

Functional and Deadlock Determinism

One of the most important properties of CDDF, and it is one of the driving design goals, is to guarantee functional determinism. In this section we prove that our model guarantees not only functional determinism, but also that deadlocks occur deterministically, which is highly valuable for productivity in parallel programming environments. We focus in this section on data produced and consumed in streams, which means that functional determinism is dened as producing the same observable output in streams for a given input.

To prove determinism, we make the two following assumptions.

1. We assume that either no shared memory communication happens, or that it does not constitute a source of non-determinism (i.e., no race conditions). This assumption is natural as shared memory communication is only allowed as a convenience under the programmer's responsibility.

2. We assume that a task that declares writing in a stream does indeed dene all of the elements it declares, leaving no undened values in streams. If a task declares producing a given amount of data for a given output stream but writes less than the amount specied, then undened memory locations may be read by consumers, breaking functional determinism guarantees.

Deterministic Data Schedule in Streams

Until now, we have disregarded the work functions of tasks, modeling task activations as a set of stream accesses where the actual data stored inside the stream is unimportant. Work functions are relevant in the current context because determinism concerns both data placement and the data itself. As a common assumption for sequential code, we postulate that all work functions and the control program itself are inherently deterministic. For a given set of stream accesses characterizing a task activation, if the data present in the input streams at the locations of all read accesses is the same, the data written on all output streams at the locations of write accesses will be the same. If the data placement in all streams is deterministic, then the work functions' determinism will be sucient to guarantee functional determinism for the program.

In our model, the schedule of data in streams is entirely determined by the control program. This choice is made in Section 2 specically to guarantee determinism. As the control program is sequential and deterministic, the schedule of data will also be deterministic.

Lemma 42 (Deterministic data schedule). For a given input, the schedule of data is deterministic in all streams of a CDDF program.

Proof. We have modeled the control program's execution, see Denition 8, with the oracle function Ω and the evaluation function ξ that builds task activations from activation points, determining the stream access indexes of each task activation and therefore the data schedule in streams. As both Ω and ξ are deterministic, the former by denition and the latter because it computes a prex sum on a deterministic trace, the construction of stream accesses of task activations is entirely deterministic as well.

5.2

Program Functional Determinism CDDF programs are deterministic by design, relying on a sequential deterministic control program to orchestrate the schedule of data rather than that of the execution.

Theorem 43. CDDF programs are functionally deterministic. More specically, for a given input, the data produced by the program in all streams is the same in a given program state σ, regardless of the execution schedule of task activations. Values in streams prexes are functions of the program state and, in particular, the nal state is a function of the initial state.

Inria

The proof of this theorem is based on Lemmas 42 and 12, on the hypothesis that work functions are deterministic, and on the two assumptions made at the beginning of this section. As Lemma 12 ensures that streams are, by construction, single assignment structures, the only imaginable races would be associated with a read operation occurring before the single write operation to a given stream location. The ordering requirements to avoid races are given by the ow dependence relation δ. As the stream prex order subsumes ow dependence requirements (see Proposition 17), the prex order is stricter than necessary to avoid this type of races. It follows that there are no race conditions in a CDDF programs' stream communication, so this does not constitute a source of non-determinism.

Proof. Let us assume, by way of contradiction, that there is a state σ = (k e , A e , A o ) where two dierent executions can lead to dierent data in some stream location (s, i) ∈ S × N. Let a p ∈ A e be the task activation that produced data at this location, so (W, s, i) ∈ a p . Lemma 42 guarantees that the same task activation produces the data for a given location since this is not dependent on the execution schedule.

As we consider that all work functions are deterministic, the execution of a p can only produce dierent data for location (s, i) if its inputs dier between the two executions. So there exists (R, s ′ , i ′ ) ∈ a p such that the value read by a p at location (s ′ , i ′ ) diers between the two executions.

As a p ∈ A e , the execution rule (EXEC) guarantees that we have A e ⋉ a p . By Denition 11, of the stream prex order, there is another task activation a ′ p ∈ A e such that (W, s ′ , i ′ ) ∈ a ′ p and a p = a ′ p or we would have a functional deadlock, which would contradict the hypothesis that a p ∈ A e .

We can recursively build an innite chain of task activations, causally tracing upstream the source of the inconsistency, and all elements in this chain are in A e , which is a nite set, built by the execution of task activations. We deduce that there must be a cycle in the chain, which once again leads to an impossibility. Any cycle of ow dependences represents a functional deadlock, see Lemma 26, and all activations in the cycle cannot have executed, so they do not belong in A e . This contradiction concludes the proof.

Deadlock Determinism

We can go one step further than proving functional determinism of programs, and show that deadlocks occur deterministically.

Theorem 44 (Deterministic deadlocks). CDDF programs deadlock deterministically: for a given input set, the program either does not deadlock or it deadlocks in the same state in all executions.

To prove this theorem, it is sucient to show that if a CDDF program admits, for a given input, an execution schedule in which a deadlock occurs, then that deadlock state is the maximum state that can and will be reached in all executions.

Proof. Let us consider such a program that deadlocks in state σ = (k e , A e , A o ) with a schedule modeled by a scheduling function θ. Let us now assume, by way of contradiction, that there exists another schedule θ ′ that, irrespectively of deadlocks, allows the program to execute up to a state Case [START_REF] Alglave | Fences in Weak Memory Models[END_REF]:

σ ′ = (k ′ e , A ′ e , A ′ o ) such that |σ| < |σ ′ |.

By denition, this means that

|k e | < |k ′ e |.
As σ is a deadlock state, we know from Lemma 15 that Ω(k e ) / ∈ Π. As we have argued in the proof of Lemma 42, the control program trace is necessarily deterministic for the same input, so |k e | < |k ′ e | implies that k e is a prex of k ′ e . We deduce that Ω(k e ) = barrier, as the trace continues, and therefore that in the schedule θ ′ the program was able to pass the barrier while in schedule θ, it was unable to make further progress.

From Lemma 15, we also know that

A o = {C(k e )}.
As k e is a prex of k ′ e and task activations are created deterministically, we have:

π ∈ k e ⇒ π ∈ k ′ e ⇔ a ∈ A e ∪ A o \ {C(k e )} ⇒ a ∈ A ′ e ∪ A ′ o \ {C(k ′ e )}
In order to pass the barrier all activations in A e ∪ A o \ {C(k e )} must be executed. As in the second execution the barrier has been able to pass, and A o = {C(k e )}, we have:

∃a ∈ A o \ {C(k e )}, a ∈ A ′ e
The rest of the proof is similar with the second case, where we rst prove this same property before continuing. Using the same reasoning as above, we deduce that:

a ∈ A ′ e ∪ A ′ o \ {C(k ′ e )} ⇒ a ∈ A e ∪ A o \ {C(k e )}
We also have:

|A e | < |A ′ e | ⇒ ∃a ∈ A ′ e , a / ∈ A e
From these two expressions we also get the same property as in Case (1):

∃a ∈ A ′ e , a ∈ A o \ {C(k e )}
Cases (1) and ( 2) continued.

The last property we have from Lemma 15 is that ∀a ∈ A o , ¬(A e ⋉ a), which is true in particular for the activation we have been able to nd in both cases:

∃a ∈ A o \ {C(k e )} | a ∈ A ′ e ∧ ¬(A e ⋉ a)
As a ∈ A ′ e , this activation was executed in the second execution schedule, so its dependences were satised by some subset of A ′ e that does not contain a ′ . Let A ′′ e A ′ e be the smallest set of activations such that A ′′ e ⋉ a. As ¬(A e ⋉ a), we deduce that:

∃a ′ ∈ A ′′ e | a ′ < a ∧ a ′ / ∈ A e If a ′ / ∈ A o ∧ a ′ <a
then the barrier was impossible to pass as the deadlock was an insuciency deadlock. If a ′ ∈ A o , then we found the same property that allowed us to continue from cases (1) and ( 2):

∃a ′ ∈ A ′′ e | a ′ ∈ A o \ {C(k e )}
We can recursively apply this reasoning and, as A ′′ e A ′ e , build an innite sequence of strictly decreasing sets of task activations, which is impossible and therefore concludes this proof.

The fact that this particular maximum state is actually reached in all executions is deduced by swapping the role of states in the proof. If any execution cannot reach the state σ, but stops in state σ ′′ instead with |σ ′′ | < |σ|, then the proof can be applied using σ ′′ as the base deadlock state.

Inria

We emphasize that deadlock determinism is only proven under the simplifying assumption of unbounded memory, which ensures that the maximum state can actually be materialized during execution. If the maximum state does not t in the available memory, then the program may experience a resource deadlock before reaching this state; resource deadlocks are not deterministic. This is a dierence with Kahn networks where bounded memory can be simulated with back-pressure channels. Detecting or disproving resource deadlocks in presence of dynamic task creation and barriers requires additional hypotheses and more complex criteria [START_REF] Pop | Leveraging Streaming for Deterministic Parallelization: an Integrated Language, Compiler and Runtime Approach[END_REF], escaping the scope of this paper.

Determinism, Productivity and Portability

An important result of Theorems 43 and 44 is that, when debugging a CDDF program, deadlock reproducibility is absolute. In most parallel programming environments, code instrumentation and debuggers lead to reduced deadlock or race reproducibility. In our model, this cannot happen.

Even more, our model guarantees that if a program experiences a deadlock-free run for a given input set, there can be no deadlocks in that program for the same input set. This is true irrespectively of the underlying architecture, so application testing becomes equivalent to that of sequential applications: changing the level of concurrency (or communication latencies, bandwidth, etc.) of the execution platform does not result in observing new spurious race conditions or deadlocks. A test suite that provides proper code coverage is therefore as ecient for uncovering errors in CDDF programs as it is for nding errors in sequential programs.

Lemma 42 and Theorem 43 further guarantee that stopping the control program (e.g., a breakpoint) will lead to a deterministic whole program state. This property in itself is very useful to facilitate the debugging process. The programmer can rely on this guarantee to deterministically observe the program state by stopping the control program, and allowing the outstanding task activations to execute until quiescence is reached. 7These properties strongly improve the productivity and portability of CDDF based programming models:

Program testing is as eective as for sequential programs, independently of the architecture used for testing.

Errors can be deterministically reproduced, when relying on stream communication.

Deadlocks occur deterministically, on all execution platforms.

Programs can be interrupted deterministically for debugging.

Consistency and Serializability

Current architectures involve increasingly relaxed memory consistency models. This choice is motivated by scalability and eciency concerns, but it makes parallel programming increasingly more complicated. Programmers cannot ignore the consistency issues of shared memory communication. They must understand the memory models of target architectures and rely on memory fences, with varying patterns depending on the architecture [START_REF] Alglave | Fences in Weak Memory Models[END_REF], which makes parallel programming ever more complicated and races more elusive.

Strict Consistency of Stream Communication

Stream computing, and functional programming in general, hide the weak memory ordering issues from developers altogether. Because of the (perceived) single assignment behaviour of stream accesses, and the synchronization mechanisms enforcing ow dependences, all read operations in streams are guaranteed to return the last, and unique, value written at a given index in a stream. This is the strongest possible memory consistency guarantee: strict consistency [START_REF] Herlihy | Axioms for concurrent objects[END_REF].

In the case of CDDF programs, strict consistency is only guaranteed for stream accesses. As our model allows shared memory communication, it is still possible to be aected by relaxed memory consistency issues. Our position is that disallowing shared memory communication is too restrictive and would go against the design philosophy of many programming paradigms. For example, Cilk guarantees strict consistency for Cilk procedure call parameters and return value, and it allows shared memory communication with a relaxed, DAG-consistent memory model. Similarly the OpenMP specication requires users to insert the necessary memory fences, depending on the underlying architecture. We advocate only using shared memory if no stream communication patterns can be substituted.

Serializability of CDDF Programs

Serializability is a very important property for parallel programs as it allows ecient execution on non-concurrent platforms and sequential functional testing. In our case, as discussed in Section 5, the latter is less important because of the strong determinism guarantees our model oers. Nevertheless, sequential execution of CDDF programs is relevant and we need to ensure it is possible. Intuitively, this should mostly be a question of whether there is a possible interference between the implicit synchronization of stream accesses of dierent task activations that would require an interleaving of operations that cannot be achieved in a sequential schedule of the execution of task activations.

Proposition 45 (Serializability). All deadlock-free CDDF programs admit at least one sequential schedule.

Proof. This property is a result of the denition of the execution rules on Figure 3, where the (EXEC) rule aggregates all the dependences of task activations in the ⋉ relation, therefore only allowing the execution of task activations that have all their dependences satised before they can start executing. This means that a task activation behaves atomically, in the sense that it cannot enable the execution of another task activation until all of its own dependences are satised.

Let us consider that, in a CDDF program in a state σ = (k e , A e , A o ), there are two outstanding task activations (a, b) ∈ A 2 o that cannot be serialized, so it is impossible to schedule a before b or b before a. By denition of the scheduling constraints, we have a < + A o b and b < + A o a, which means that there is a cycle a < + A o a and therefore a deadlock according to Lemma 26. This contradicts the deadlock-freedom hypothesis.

A trivial sequential schedule, in an unbounded memory abstraction, consists in running the control program until it reaches a barrier or terminates, then executing all task activations in any order allowed by the ⋉ relation, then repeat until termination.

If we only consider correct programs, so excluding all programs that have functional deadlocks, we can therefore guarantee serializability under the same conditions as spurious deadlockfreedom. However, this type of serialization is more akin to the dynamic scheduling of some ad Inria hoc user-level threads, or bers. This scheme incurs scheduling runtime overhead and disables many compiler optimizations that would apply to a static schedule.

Static serialization, where the sequential schedule is statically dened, is a much more powerful result, but proving the existence of a static serial schedule, let alone providing an automatic way of building it, is much harder in the general case. There is, however, a trivial static schedule for which we can prove a necessary and sucient condition: the control program order. This schedule is semantically important as it directly correlates to Cilk strictness; it is the default serialization strategy of both Cilk and OpenMP.

Theorem 46 (Serializability static schedule). A CDDF program can be sequentially executed in control program order if and only if it is stream causal in each state.

Proof. Given the hypothesis that the program is stream causal in each state, we can add a barrier after each activation point in the control program and this barrier is guaranteed, by Theorem 33, to be able to pass, which means that each newly generated task activation can execute immediately.

Conversely, if the program can execute sequentially, with the execution of each task activation tied to the generation of the task activation, then the program can admit one barrier after each activation point without deadlocking. As the stream clock order is a subset of the order relation dened by the control program order, the execution of task activations was possible in strictly positive stream clock order for all streams in the program, while also respecting ow dependences, which is, by denition, a stream causal schedule. Proposition 31 allows to conclude that the program is stream causal in each state.

Summary of CDDF Properties and Conditions

To give a better idea of the guarantees provided by the CDDF model, we present a summary of these properties and the necessary conditions on Table 7, where D(σ), ID(σ), FD(σ) and SD(σ) respectively mean that the program can experience a deadlock, 8 an insuciency deadlock, a functional deadlock or a spurious deadlock, all relative to a program state σ. The conditions presented range from the weakest to the strongest. Each condition is sucient to ensure spurious deadlock freedom, which is one of our main objectives, as well as functional and deadlock determinism and strict consistency. We describe the conditions, which are presented in an abbreviated form in the table, and we discuss the results below. 1. The rst condition corresponds to Theorem 40. It requires that no stream in the program be multi-producer and multi-consumer (MPMC) in that state and that the program be task causal, T C(σ). As Kahn channels are single-producer single-consumer, the Kahn principle is more restrictive than this condition. Programs meeting these requirements can only experience insuciency deadlocks and benet from serializability when no insuciency deadlocks occur.

2. The second condition, from Theorem 41, requires the hypergraph H(σ) to be free of strongly connected components. This condition corresponds to the common case identied by Kudlur and Mahlke in [START_REF] Kudlur | Orchestrating the execution of stream programs on multicore platforms[END_REF]. It is sucient to avoid all but insuciency deadlocks. It also allows dynamic serializability in the absence of insuciency deadlocks.

3. The third condition requires stream causality of the program state whenever the control program reaches a barrier or terminates. This strong condition is sucient, in Theorem 33, to prove the absence of any type of deadlocks and to ensure serializability in all cases.

As only barrier states need stream causality, this condition is less restrictive than Cilk strictness.

4. Finally, the last and strongest condition, from Theorem 46, requires stream causality SC(σ) in each state σ of the program, providing all of the possible properties, including static control program (CP) order serializability. This condition is a relaxed form of strictness where the constraints only bear on the control program, not on task activation execution.

As a nal note, the two causality conditions, stream and task causality, are alternatives to the Kahn principle when streams can have multiple producers and/or multiple consumers. When restricting CDDF to single-producer single-consumer streams, it is easy to verify that both conditions are equivalent, and also equivalent to the Kahn principle at the limit.

Conclusion

We presented CDDF, a new, general model of computation for stream-computing programs. It is built around the notion of control program, a process that constructs a dynamic, yet deterministic, schedule of data in streams. We proved a set of important properties provided by programs implementing this model, like deadlock-freedom, determinism and serializability. We proved that programming models relying on CDDF can be implemented eciently, allowing to synchronize streams over closed prexes without spurious deadlocks, and exposing excellent productivity features: functional and deadlock determinism, independently of the execution platform, serializability, and strict consistency on streams.

Let us summarize the impact of CDDF on language design. Language constructs matching the native task creation, stream communication and barriers of CDDF inherit its determinism and deadlock-freedom. To ensure the soundness of a new language construct, the designer is only required to prove the absence of spurious deadlocks in the formalization of this construct with the prex ordering on streams; the other properties are important for productivity and for enabling optimizations, but not mandatory for soundness. 9 For any new constructs, such productivity properties as serializability, determinism and strict consistency can be proven using the CDDF formalization and existing proofs as blueprints.

Finally, establishing the strong properties of CDDF involved a few simplifying assumptions, notably unbounded memory, a sequential control program, and the absence of feedback from task activations to the control program. The relaxation of these restrictions will be the topic of a distinct publication.

A Detailed Proofs of CDDF Properties

Proof of Lemma 15. Denition 14 states that a deadlock occurs when no rule can be red in a given state of the program:

D(σ) ⇔ ¬(GEN) ∧ ¬(BAR) ∧ ¬(TERM) ∧ ¬(EXEC)
From the denition of the execution rules on Figure 3 and using Ω(k e ) = barrier ∧ Ω(k e ) = ⊤ ⇔ Ω(k e ) ∈ Π to merge the conditions for (BAR) and (TERM), we can derive the following equivalence, which simplies in the desired property:

D(σ) ⇔    A o = {C(k e )} ∨ Ω(k e ) ∈ Π ∧ Ω(k e ) / ∈ Π ∧ ∀a ∈ A o : ¬A e ⋉ a
Proof of Lemma 22. The proof relies on Lemma 18, which ensures that the continuation activation is never executable with (EXEC ∆ ):

¬ (A e ∪ A o \ {C(k e )}) ∆ C(k e )
Denition 21 can be rewritten and expanded from the denition of ow dependences,

ID(σ) ⇒ ∀a ∈ A o , C(k e ) δ + a : ⇒ ∀a ∈ A o , ∃a ′ ∈ A o , C(k e ) δ * a ′ ∧ a ′ δ a ⇒ ∀a ∈ A o , ∃a ′ ∈ A o , ∃(s, i), (W, s, i) ∈ a ′ ∧ (R, s, i) ∈ a ⇒ ∀a ∈ A o , ∃(R, s, i) ∈ a, ∀a ′ ∈ A e , (W, s, i) / ∈ a ′ ⇒ ∀a ∈ A o , ¬ A e ∆ a
Proof of Lemma 25. By Denition 24 there exists σ

′ = (k ′ e , A ′ e , A ′ o ) such that: WID(σ) ⇒ ID(σ ′ ) ∧ |σ| |σ ′ | ∧ k e = k ′ e
Which can be expanded using Denition 21 for ID(σ ′ ):

Ω(k ′ e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , C(k e ) δ + a Knowing that A ′ o = {C(k e )}, and in any program state {C(k e )} ∈ A ′ o , there is a ′ ∈ A ′ o , a ′ = C(k e ) ∧ C(k e ) δ a ′ .
As k e = k ′ e , there can be no task activation generation in between the two states of the program, so A ′ o ⊂ A o , and therefore a ′ ∈ A o , which allows us to conclude:

WID(σ) ⇒ Ω(k e ) / ∈ Π ∧ ∃a ∈ A o , a = C(k e ) ∧ C(k e ) δ a
∀a ∈ A o , C(k e ) < a ⇔ C(k e ) δ a
Proposition 17 yields ∀a ∈ A o , C(k e ) < a ⇐ C(k e ) δ a, so we need only prove the reverse in order to conclude this proof. By denition of the stream prex order, C(k e ) < a i:

∃s ∈ S, ∃i, j ∈ N, j i ∧ (W, s, j) ∈ C(k e ) ∧ (R, s, i) ∈ a
From the Denition 9 of the continuation activation, we deduce:

∀s ∈ S, ∃α ∈ N : ∀k ∈ N, (W, s, k) ∈ C(k e ) ⇒ k α
Which allows us to conclude: (W, s, j) ∈ C(k e ) ⇒ j α. As j i, we further deduce that:

(W, s, j) ∈ C(k e ) ⇒ i j α ⇒ (W, s, i) ∈ C(k e )
By denition of the ow dependence relation,

(W, s, i) ∈ C(k e ) ∧ (R, s, i) ∈ a ⇒ C(k e )δa.
Proof of Lemma 26. We only present the proof for WD(σ), that of WFD(σ) is identical. We rst show that, in a weak deadlock state, we can always either nd a dependence cycle or a dependence chain starting at C(k e ).

Let us consider σ = (k e , A e , A o ) such that WD(σ) which by denition implies that

∃σ ′ , D(σ ′ ) ∧ k e = k ′
e , and we expand:

∃σ ′ , Ω(k e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , ¬A ′ e ⋉ a
We use Denition 11 of the stream prex order, yielding:

∀a ∈ A ′ o , ∃(R, s, i) ∈ a, ∃j i, ∀a ′ ∈ A ′ e , (W, s, j) / ∈ a ′
Proposition 10 ensures that all stream accesses are covered by an activation in A ′ e ∪ A ′ o and since (W, s, j) is not present in activations from A ′ e , it necessarily belongs to an activation in A ′ o :

∀a ∈ A ′ o , ∃(R, s, i) ∈ a, ∃j i, ∃a ′ ∈ A ′ o , (W, s, j) ∈ a ′ ⇔ ∀a ∈ A ′ o , ∃a ′ ∈ A ′ o : a ′ < a
We can recursively build a chain ... < a ′′ < a ′ < a by applying this last proposition to a, then a ′ which satises a ′ < a and so on. As A ′ o is a nite set, we deduce that either we stop once we reach the continuation activation or there must be at least one cycle. As A ′ o = {C(k e )}, we can choose a = C(k e ), which concludes the rst part of the proof.

The proof of the reverse simply requires building a state σ

′ with A ′ o = {C(k e ), a 1 , a 2 , ..., a n },
where a 1 ...a n are the activations forming the cycle or the dependence chain, which is a deadlock state as the cycle or the dependence on the continuation prevents any activation to be executable:

∀a ∈ A ′ o , ∃a ′ ∈ A ′ o , a ′ < a ⇒ ¬ A ′ e ⋉ a Inria
Proof of Proposition 27. The rst part of this proof is a direct result of Lemma 22:

WID(σ) ⇒ ∃σ ′ , ID(σ ′ ) ⇒ FD(σ ′ ) ⇒ WFD(σ)
To prove that WFD(σ) ⇒ WD(σ), we need only consider Lemmas 15 and 20, which respectively provide the characterization of a deadlock and a functional deadlock state. Proof of Proposition 31. We rst prove that program stream causality is necessary to the existence of a stream causal schedule, according to our denitions. Let us assume, by way of contradiction, that the program is not causal in a state σ = (k e , A e , A o ). There exist a, a ′ ∈ A e ∪ A o such that:

WFD(σ) ⇒ ∃σ ′ , FD(σ ′ ) ⇒ ∃σ ′ , Ω(k e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , ¬A ′ e ∆ a ⇒ ∃σ ′ , Ω(k e ) / ∈ Π ∧ A ′ o = {C(k e )} ∧ ∀a ∈ A ′ o , ¬A ′ e ⋉ a ⇒ ∃σ ′ , D(σ ′ ) ⇒ WD(σ)
¬(a = a ′ = C(k e )), a sc a ′ ∧ a ′ δ + a
Which means that any scheduling function θ, that enforces a causal schedule in this state, meets the following constraints:

(θ(a) θ(a ′ )) ∧ (θ(a ′ ) < θ(a))
This contradiction allows us to conclude to the impossibility. Let us consider a scheduling function θ that enforces all ow dependences. This schedule, which is obtained by using the (EXEC ∆ ) transition rule, satises, by denition:

∀a, a ′ ∈ A e ∪ A o : a δ + a ′ ⇒ θ(a) < θ(a ′ )
We need to show that this schedule is admissible (i.e. that it can indeed be executed) and that a sc a ′ ⇒ θ(a) θ(a ′ ) is veried in this schedule. We remark that a sc a is always true for activations that contain at least one write access, which is necessarily the case if an activation is the source of a ow dependence, which we inject in Denition 29, deducing that:

∃a ∈ A e ∪ A o , a = C(k e ), a δ + a ⇒ ¬SC(σ)
This means that stream causality in a state precludes ow dependence cycles between task activations. Furthermore, as all activations are in a stream clock precedence relation with the continuation activation:

∃a ∈ A e ∪ A o , a = C(k e ), C(k e ) δ + a ⇒ ¬SC(σ)
As there can be no cycles and no dependence chains containing the continuation activation, Lemma 26 allows us to conclude that this state is not a weak functional deadlock state, irrespectively of the fact that the control program has reached a barrier or not. This means that this schedule built on (EXEC ∆ ) is able to schedule all task activations in A e ∪ A o . As a side note, this already proves that a CDDF program that is stream causal every time the control program reaches a barrier cannot experience functional deadlocks.

Let us verify that, in a stream causal program state, this schedule is itself stream causal. From the denition of stream causality, we have ∀a, a ′ ∈ A e ∪ A o :

¬(a = a ′ = C(k e )), a sc a ′ ⇒ ¬(a ′ δ + a)
We deduce that a sc a ′ ⇒ ¬(a ′ δ + a) ⇒ ¬(θ(a ′ ) < θ(a)) ⇒ θ(a) θ(a ′ ), which concludes the proof.

Proof of Theorem 33. We prove this theorem by showing that SC(σ) ∧ WD(σ) is impossible. Let us assume, by way of contradiction, that σ = (k e , A e , A o ) is such a state.

We rewrite the Denition 11 of the stream prex order in terms of ow dependences and the stream clock relation:

∀a, a ′ ∈ A e ∪ A o , a < a ′ ⇔ ∃(s, i) ∈ S × N, ∃j i, (W, s, j) ∈ a ∧ (R, s, i) ∈ a ′
Proposition 10 yields ∃a ′′ ∈ A e ∪ A o , (W, s, i) ∈ a ′′ , which we add to the expression above to conclude that:

∀a, a ′ ∈ A e ∪ A o , a < a ′ ⇔ ∃a ′′ ∈ A e ∪ A o , a sc a ′′ ∧ a ′′ δ a ′
As the program is causal in this state, Proposition 31 guarantees the existence of at least one causal schedule in this state. Let θ be a scheduling function for such a schedule. By Denition 30 of a causal schedule, for a, a ′ ∈ A e ∪ A o we have:

a < a ′ ⇒ ∃a ′′ ∈ A e ∪ A o , θ(a) θ(a ′′ ) ∧ θ(a ′′ ) < θ(a ′ ) ⇒ θ(a) < θ(a ′ )
Expanding Lemma 26 for the weak deadlock state σ yields:

∃(a 1 , ..., a n ) ∈ A n o , a 1 = C(k e ), a 1 < ... < a n < a 1 ∨ C(k e ) < a 1 < ... < a n
Where we substitute the scheduling function constraints on <: θ(a 1 ) < θ(a 2 ) < ... < θ(a n ) < θ(a 1 ) ⇒ θ(a 1 ) < θ(a 1 ) θ(C(k e )) < θ(a 1 ) < ... < θ(a n ) ⇒ θ(C(k e )) < θ(a n )

Both results are contradictory. The rst trivially, the second because a n sc C(k e ) is always true, by Denition 28, so θ(a n ) θ(C(k e )) and θ(C(k e )) < θ(a n ), concluding this proof.

Proof of Proposition 39. The proof of this proposition is very close to that of Proposition 31, with a simple substitution of relations and properties. The only dierence comes from the fact that contrary to stream clocks, task order does not allow ordering task activations with respect to the continuation activation. This means that the existence of a dependence chain starting at the continuation activation does not allow to conclude to a violation of causality:

∃a ∈ A e ∪ A o , a = C(k e ), C(k e ) δ + a ¬T C(σ)
For this reason, the application of Lemma 26 only allows to conclude that, in a task causal state σ, all functional deadlocks are insuciency deadlocks. The existence of the schedule depends on the absence of the weak insuciency deadlock condition C(k e ) δ + a.

Proof of Theorem 40. Let us consider the state σ = (k e , A e , A o ) of a program that satises the hypotheses. We use the results from Lemmas 26 and 25 instead of the denition to characterize weak deadlock states. Merging the two, we obtain:

WD(σ) ⇒ WID(σ) ∨ ∃a ∈ A o , a = C(k e ), a < + a

Inria

Replacing this expression in the theorem shows that our objective is to prove that no task activation cycle on the stream prex order relation can exist in such states:

T C(σ) ∧ ∀s ∈ S(σ) : |P (σ, s)| = 1 ∨ |C(σ, s)| = 1 ⇒ ¬ ∃a ∈ A o , a = C(k e ), a < + a
Let us assume, by way of contradiction, that the program is in a weak deadlock state σ, but not in a weak insuciency deadlock, and therefore that ∃a ∈ A o , a = C(k e ), a < + a. As the program is also task causal in this state, it admits a task causal schedule. Let θ be such a schedule. Expanding this cycle yields: From the denition of the stream prex order, we deduce that:

∀k ∈ [1, n -1], a k < a k+1 ⇒ ∃(s, i) ∈ S × N, ∃j i, (W, s, j) ∈ a k ∧ (R, s, i) ∈ a k+1

The stream s is either single-producer or single-consumer, so we will handle the cases separately.

If |P (σ, s)| = 1, then we look at the producer task activation a k and its equivalence class. Either the precise write operation (W, s, i) belongs to a task activation in this class, or this operation is not yet scheduled and therefore belongs to the continuation activation:

∃a ′ k ∈ [a k ] ∼ , (W, s, i) ∈ a ′ k ∨ (W, s, i) ∈ C(k e )
If the write operation is in the continuation activation, then we would have C(k e ) δ a k+1 , which is a weak insuciency deadlock condition and contradicts the hypothesis. We can therefore assume that (W, s, i) ∈ a ′ k and a ′ k δ a k+1 . We deduce that:

a k t a ′ k ∧ a ′ k δ a k+1 ⇒ θ(a k ) θ(a ′ k ) ∧ θ(a ′ k ) < θ(a k+1 )
We conclude that, in the case of a single-producer stream connecting a k and a k+1 , we have:

a k < a k+1 ⇒ θ(a k ) < θ(a k+1 )
If |C(σ, s)| = 1, then we look at the consumer task activation a k+1 and its equivalence class. As the higher read access operation (R, s, i) has already been scheduled to a task activation, the lower index operation (R, s, j) is guaranteed to have also been scheduled, so we know that:

∃a ′ k+1 ∈ [a k+1 ] ∼ , (R, s, j) ∈ a ′ k+1
We have a k δ a ′ k+1 and a ′ k+1 t a k+1 , which leads to:

θ(a k ) < θ(a ′ k+1 ) ∧ θ(a ′ k+1 ) θ(a k+1 ) ⇒ θ(a k ) < θ(a k+1 )
By aggregating the results of the two cases, we conclude the proof with the contradiction: As Ω(k e ) ∈ Π gives ¬WD(σ), we only keep the condition ∄a ∈ A o , a = C(k e ) ∧ C(k e ) < a, which means that C(k e ) cannot appear in any task activation cycle in this state.

We need to show that the absence of cycles in the task graph H(σ) means that there can be no task activation cycles in A e ∪ A o \ {C(k e )}. This is intuitively simple as the program hypergraph is an over-approximation of the communication patterns in task activations where we lose the precise information on stream access indexes.

Let us assume by way of contradiction that there is a cycle of task activations in This contradicts the hypothesis of no cycles in H(σ) and therefore concludes the proof.

Proof of Lemma 42. We have modeled the control program's execution, see Denition 8, with the oracle function Ω and the evaluation function ξ that builds task activations from activation points, determining the stream access indexes of each task activation and therefore the data schedule in streams. As both Ω and ξ are deterministic, the former by denition and the latter because it computes a prex sum on a deterministic trace, the construction of stream accesses of task activations is entirely deterministic as well.

Proof of Theorem 43. Let us assume, by way of contradiction, that there is a state σ = (k e , A e , A o ) where two dierent executions can lead to dierent data in some stream location (s, i) ∈ S × N. Let a p ∈ A e be the task activation that produced data at this location, so (W, s, i) ∈ a p . Lemma 42 guarantees that the same task activation produces the data for a given location since this is not dependent on the execution schedule.

As we consider that all work functions are deterministic, the execution of a p can only produce dierent data for location (s, i) if its inputs dier between the two executions. So there exists (R, s ′ , i ′ ) ∈ a p such that the value read by a p at location (s ′ , i ′ ) diers between the two executions.

As a p ∈ A e , the execution rule (EXEC) guarantees that we have A e ⋉ a p . By Denition 11, of the stream prex order, there is another task activation a ′ p ∈ A e such that (W, s ′ , i ′ ) ∈ a ′ p and a p = a ′ p or we would have a functional deadlock, which would contradict the hypothesis that a p ∈ A e .

We can recursively build an innite chain of task activations, causally tracing upstream the source of the inconsistency, and all elements in this chain are in A e , which is a nite set, built by the execution of task activations. We deduce that there must be a cycle in the chain, which once again leads to an impossibility. Any cycle of ow dependences represents a functional deadlock, see Lemma 26, and all activations in the cycle cannot have executed, so they do not belong in A e . This contradiction concludes the proof. Case [START_REF] Alglave | Fences in Weak Memory Models[END_REF]:

|k e | < |k ′ e |.
As σ is a deadlock state, we know from Lemma 15 that Ω(k e ) / ∈ Π. As we have argued in the proof of Lemma 42, the control program trace is necessarily deterministic for the same input, so |k e | < |k ′ e | implies that k e is a prex of k ′ e . We deduce that Ω(k e ) = barrier, as the trace continues, and therefore that in the schedule θ ′ the program was able to pass the barrier while in schedule θ, it was unable to make further progress.

From Lemma 15, we also know that A o = {C(k e )}. As k e is a prex of k ′ e and task activations are created deterministically, we have: We also have:

|A e | < |A ′ e | ⇒ ∃a ∈ A ′ e , a / ∈ A e
From these two expressions we also get the same property as in Case (1):

∃a ∈ A ′ e , a ∈ A o \ {C(k e )}
Cases (1) and ( 2) continued.

The last property we have from Lemma 15 is that ∀a ∈ A o , ¬(A e ⋉ a), which is true in particular for the activation we have been able to nd in both cases:

∃a ∈ A o \ {C(k e )} | a ∈ A ′ e ∧ ¬(A e ⋉ a)
As a ∈ A ′ e , this activation was executed in the second execution schedule, so its dependences were satised by some subset of A ′ e that does not contain a ′ . Let A ′′ e A ′ e be the smallest set of activations such that A ′′ e ⋉ a. As ¬(A e ⋉ a), we deduce that:

∃a ′ ∈ A ′′ e | a ′ < a ∧ a ′ / ∈ A e
If a ′ / ∈ A o ∧ a ′ <a then the barrier was impossible to pass as the deadlock was an insuciency deadlock. If a ′ ∈ A o , then we found the same property that allowed us to continue from cases (1) and ( 2):

∃a ′ ∈ A ′′ e | a ′ ∈ A o \ {C(k e )}
We can recursively apply this reasoning and, as A ′′ e A ′ e , build an innite sequence of strictly decreasing sets of task activations, which is impossible and therefore concludes this proof.

The fact that this particular maximum state is actually reached in all executions is deduced by swapping the role of states in the proof. If any execution cannot reach the state σ, but stops in state σ ′′ instead with |σ ′′ | < |σ|, then the proof can be applied using σ ′′ as the base deadlock state.

Proof of Proposition 45. This property is a result of the denition of the execution rules on Figure 3, where the (EXEC) rule aggregates all the dependences of task activations in the ⋉ relation, therefore only allowing the execution of task activations that have all their dependences satised before they can start executing. This means that a task activation behaves atomically, in the sense that it cannot enable the execution of another task activation until all of its own dependences are satised.

Let us consider that, in a CDDF program in a state σ = (k e , A e , A o ), there are two outstanding task activations (a, b) ∈ A 2 o that cannot be serialized, so it is impossible to schedule a before b or b before a. By denition of the scheduling constraints, we have a < + b and b < + a, which means that there is a cycle a < + a and therefore a deadlock according to Lemma 26. This contradicts the deadlock-freedom hypothesis.

A trivial sequential schedule, in an unbounded memory abstraction, consists in running the control program until it reaches a barrier or terminates, then executing all task activations in any order allowed by the ⋉ relation, then repeat until termination.

  the CDDF program can be identied by the (partial) trace k e of the control program, and the sets A e of executed task activations and A o of outstanding task activations. Denition 8 (Control program execution). The abstract execution of the control program is modeled by two functions: (1) an oracle function Ω : K → Π ∪ {barrier} ∪ {⊤}where ⊤ marks the end of the control programabstracts the sequence operator and provides the next operation to be executed by the control program; and (2) the activation point evaluation function ξ : K × Π → A dening how an activation point is evaluated to generate a task activation:

Figure 1 :

 1 Figure 1: Syntax of the ImpStream language.

Figure 2 :

 2 Figure 2: Moving average FIR lter of order N implemented in ImpStream.

Figure 4 :

 4 Figure 4: Overview of CDDF execution model.

Figure 5 :

 5 Figure 5: Greedy execution of the FIR example on Figure 2 on four threads.

  a}, {C(k e ), a}). As {C(k e ), a} ⊂ A o , we deduce that |A e | |A e ∪ A o \ {C(k e ), a}|, which yields: |σ| = |k e | + |A e | |k e | + |A e ∪ A o \ {C(k e ), a}| = |σ ′ | As we know that Ω(k e ) / ∈ Π and both states have the same trace k e , we only need to show that ID(σ ′ ) is true. A ′ o = {C(k e ), a} satises A ′ o = {C(k e )} and the only remaining activation a ∈ A ′

3 . 2

 32 Deadlock-Freedom in Stream Causal CDDF ProgramsWithout any restriction, spurious deadlocks may occur in CDDF programs due to the overapproximation, and therefore over-synchronization, of data dependences. As the model allows absolute freedom in the communication patterns between task activations, we can build a schedule that leads to a state where a CDDF program is in a deadlock, but not in a functional deadlock. This situation occurs, for instance, in the following example. Example 32 (Spurious deadlock in a CDDF program). Let us consider the following ImpStream program, consisting of four task activation points π 1..4 . π1 task (R, s2, 1, 1):offset_2, (W, s1, 1, 1):offset_1 do s1[offset_1] = foo (s2[offset_2]); π2 task (R, s1, 1, 1):offset_1 do use (s1[offset_1]); π3 task (R, s1, 1, 1):offset_1, (W, s2, 1, 1):offset_2 do s2[offset_2] = bar (s1[offset_1]); π4 task (W, s1, 1, 1):offset_1 do s1[offset_1] = ...; The control program's evaluation of these activation points leads to generating four task activations a 1..4 , among which a 4 can directly be executed, leading to a program state σ = (k e , A e , A o ) such that: A e = {a 4 } where a 4 = {(W, s 1 , 1)}

Figure 6 :

 6 Figure 6: Stream causal version of the FIR application on Figure 2.

  |k e | + |A e | < |k ′ e | + |A ′ e |, which leads to the following two relevant cases to handle: (1) traces have dierent lengths, |k e | < |k ′ e |; or (2) the set of executed task activations is dierent, |A e | < |A ′ e |.

Case ( 2 )

 2 : |A e | < |A ′ e |. If at this point |k e | < |k ′ e |, then we just consider this to fall in Case (1), so we consider here that |k e | |k ′ e |.

Figure 7 :

 7 Figure 7: Properties of CDDF programs.

  On the third line, we use Proposition 17 which gives A ′ e ⋉a ⇒ A ′ e ∆a or conversely ¬(A ′ e ∆a) ⇒ ¬(A ′ e ⋉ a).

  ∃a ∈ A o ,a = C(k e ), ∃n ∈ N, n > 0, ∃(a 1 , ..., a n ) ∈ A n o : a 1 = a n = a ∧ a 1 < ... < a n

a 1 <

 1 ... < a n ⇒ θ(a 1 ) < ... < θ(a n ) ⇒ θ(a) < θ(a)Proof of Theorem 41. The proof of this theorem derives from Lemma 25, which characterizes a weak insuciency deadlock state, and Lemma 26, characterizing weak deadlock states as dependence cycles. To prove this theorem, we show that:SCC(H(σ)) = ∅ ∧ ¬WID(σ) ⇒ ¬WD(σ)Let σ be a CDDF program state where H(σ) contains no cycles and ¬WID(σ). Lemma 25 yields:¬WID(σ) ⇔ Ω(k e ) ∈ Π ∨ (∄a ∈ A o , a = C(k e ) ∧ C(k e ) < a)

s 1 , i 1 )

 11 A e ∪ A o \ {C(k e )}: ∃a 1 , ..., a n ∈ A e ∪ A o \ {C(k e )} | a 1 < a 2 < ... < a n ∧ a n = a 1Each stream prex order relation translates, by Denition 11, into:∀k ∈ [1, n -1] : a k < a k+1 ⇔ ∃(R, s k , i k ) ∈ a k+1 , ∃j k i k , (W, s k , j k ) ∈ a kFrom the previous relation, we deduce that the set of streams (s 1 , s 2 , ...s n-1 ) satises:∈ a 2 ∧ (W, s 2 , j 2 ) ∈ a 2 (R, s 2 , i 2 ) ∈ a 3 ∧ (W, s 3 , j 3 ) ∈ a 3 ... (R, s n , i n ) ∈ a n = a 1 ∧ (W, s 1 , j 1 ) ∈ a 1 , s 1 ) ∩ P (σ, s 2 ) = {a 2 } = ∅ C(σ, s 2 ) ∩ P (σ, s 3 ) = {a 3 } = ∅ ... C(σ, s n ) ∩ P (σ, s 1 ) = {a 1 } = ∅

  Proof of Theorem 44. Let us consider such a program that deadlocks in state σ = (k e , A e , A o ) with a schedule modeled by a scheduling function θ. Let us now assume, by way of contradiction, that there exists another schedule θ ′ that, irrespectively of deadlocks, allows the program to execute up to a state σ ′ = (k ′ e , A ′ e , A ′ o ) such that |σ| < |σ ′ |. By denition, this means that |k e | + |A e | < |k ′ e | + |A ′ e |, which leads to the following two relevant cases to handle: (1) traces have dierent lengths, |k e | < |k ′ e |; or (2) the set of executed task activations is dierent, |A e | < |A ′ e |.

π

  ∈ k e ⇒ π ∈ k ′ e ⇔ a ∈ A e ∪ A o \ {C(k e )} ⇒ a ∈ A ′ e ∪ A ′ o \ {C(k ′ e )}In order to pass the barrier all activations in A e ∪ A o \ {C(k e )} must be executed. As in the second execution the barrier has been able to pass, and A o = {C(k e )}, we have:∃a ∈ A o \ {C(k e )}, a ∈ A ′ eThe rest of the proof is similar with the second case, where we rst prove this same property before continuing.Case (2):|A e | < |A ′ e |. Ifat this point |k e | < |k ′ e |, then we just consider this to fall in Case (1), so we consider here that |k e | |k ′ e |. Using the same reasoning as above, we deduce that: a ∈ A ′ e ∪ A ′ o \ {C(k ′ e )} ⇒ a ∈ A e ∪ A o \ {C(k e )}

  The result of its evaluation by ξ is added to A o and the activation point is appended to the existing program trace k e . The old continuation activation, C(k e ) replaced in A o by a new one, C(k e .π). By denition, C(k e .π) ⊂ C(k e ), which models the restriction on the possible futures of the program.

  Program progress). A CDDF program makes progress from state σ if any execution rule can be applied. The resulting state σ ′ satises |σ| < |σ ′ | or the program has terminated.

(TERM), are strictly monotonically increasing the state of the program w.r.t. this measure. Inria Denition 13 (

  Denition 14 (Program deadlock). A CDDF program is in a deadlock state σ, noted D(σ), if no execution rule can make a transition. From this denition and that of the execution rules, we deduce the following property on the state of a deadlocked CDDF program. Lemma 15 (Deadlock state). A CDDF program is in a deadlock state σ = (k e , A e , A o ), D(σ)

if and only if:

  Denition 24 (Weak deadlock state). The state σ = (k e , A e , A o ) of a CDDF program is a weak (*) deadlock state, for any type (*) of deadlock, if there is a state σ

  5.7 Hierarchy of weak deadlock statesBased on Proposition 17 and the Lemmas 25 and 26, we can provide a hierarchy of weak deadlock states. It is important to stress the fact that any given state can satisfy the weak deadlock condition for multiple types of deadlocks, possibly in a completely independent manner. If such is the case, the stronger deadlock property is naturally taken into account.

Proposition 27 (Weak deadlock state hierarchy). Any state σ of a CDDF program satises:

  Denition 28 (Stream clock precedence relation). Task activations writing to at least one common stream in a program state σ = (k e , A e , A o ) are in a reexive and antisymmetric binary relation sc ∈ P(A 2 ):

  Theorem 41. A CDDF program can only have insuciency deadlocks in a state σ = (k e , A e , A o ) if its hypergraph H(σ) contains no strongly connected components (SCC) in that state:

  To prove the ⇐ direction, let us consider state σ ′ = (k e , A e ∪ A o \ {C(k e ), a}, {C(k e ), a}). As {C(k e ), a} ⊂ A o , we deduce that |A e | |A e ∪ A o \ {C(k e ), a}|, which yields: As we know that Ω(k e ) / ∈ Π and both states have the same trace k e , we only need to show that ID(σ ′ ) is true. A ′ o = {C(k e ), a} satises A ′ o = {C(k e )} and the only remaining activation a ∈ A ′ o satises C(k e ) δ a, which concludes this second part of the proof. Finally, to prove the equivalence of weak deadlock states dened by either of the δ or < relations, we show that:

|σ| = |k e | + |A e | |k e | + |A e ∪ A o \ {C(k e ), a}| = |σ ′ |

RR n°8015

In this context, atomicity refers to task activations being run to completion: once a task starts executing, it does not need to wait for external events. Inria

A more pragmatic example of implementation of a CDDF language, OpenStream[START_REF] Pop | A stream-computing extension to OpenMP[END_REF][START_REF] Pop | Expressiveness and Data-Flow Compilation of OpenMP Streaming Programs[END_REF], extends the task constructs in the OpenMP language with streams that t the CDDF model. However, the semantics of such a language is outside the scope of this paper.RR n°8015

Note that the restrictions imposed on the set Π of valid activation points in Denition 5 can be easily veried at runtime or, in static cases, during compilation.

For simplicity, this is not the case in ImpStream; it can be achieved with similar tools as bound checking, or allowed to fall under programmer responsibility in the same way as out-of-bounds array accesses.Inria

Activations that contain no write accesses and would therefore not be in any relation w.r.t. stream clocks.Inria

Lifting the Scott topology to streams, continuity is the monotonicity of stream prex denitions at the limit.Inria

Quiescence occurs when no further progress can be made. The time necessary to reach that point is undecidable, but nite as we have seen in the discussion of weak deadlock states.RR n°8015

This general deadlock case is the union of all sub-cases.RR n°8015

If we consider programs with functional deadlocks to be incorrect.Inria

Inria

InriaRESEARCH CENTRE PARIS -ROCQUENCOURTDomaine de Voluceau, -Rocquencourt B.P. 105 -78153 Le Chesnay Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399