Louis Mandel

Cédric Pasteur

Reactivity of Cooperative Systems: Application to ReactiveML extended version

Keywords: Cooperative scheduling, Type systems, Semantics, Functional languages, Synchronous languages Ordonnancement coopératif, Systèmes de types, Sémantique, Langages fonctionnels, Langages synchrones

Introduction

Most programming languages offer lightweight thread facilities, either integrated in the language like the asynchronous computations [START_REF] Syme | The F# asynchronous programming model[END_REF] of F#, or available as a library like GNU Pth [START_REF] Engelschall | Portable multithreading: The signal stack trick for user-space thread creation[END_REF] for C, Concurrent Haskell [START_REF] Jones | Concurrent Haskell[END_REF] or Lwt [START_REF] Vouillon | Lwt: a cooperative thread library[END_REF] for OCaml. These libraries are based on cooperative scheduling: each thread of execution cooperates with the scheduler to let other threads execute. This enables an efficient and sequential implementation of concurrency, allowing to create up to millions of separate threads, which is impossible with operating system threads. Synchronization also comes almost for free, without requiring synchronization primitives like locks.

The downside of cooperative scheduling is that it is necessary to make sure that threads actually cooperate:

• Control must regularly be returned to the scheduler. This is particularly true for infinite loops, which are very often present in reactive and interactive systems.

• Blocking functions, like operating system primitives for I/O, cannot be called.

The solution to the latter is simple: never use blocking functions inside cooperative threads. All the facilities mentioned earlier provide either I/O libraries compatible with cooperative scheduling or a means to safely call blocking functions. See Marlow et al. [START_REF] Marlow | Extending the Haskell foreign function interface with concurrency[END_REF] for an overview on how to implement such libraries.

Dealing with the first issue is usually the responsibility of the programmer. For instance, in the Lwt manual [START_REF] Dimino | Lwt User Manual[END_REF], one can find: [...] do not write function that may take time to complete without using Lwt [...] The goal of this paper is to design a static analysis, called reactivity analysis, to statically remedy this problem of absence of cooperation points. The analysis checks that the programmer does not forget to cooperate with the scheduler. Our work is applied to the ReactiveML language [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF], which is an extension of ML with a synchronous model of concurrency [START_REF] Benveniste | The synchronous languages twelve years later[END_REF] (Section 2). However, we believe that our approach is generic enough to be applied to other models of concurrency (Section 6.5). The contributions of this paper are the following:

• A reactivity analysis based on a type-and-effect system [START_REF] Lucassen | Polymorphic effect systems[END_REF] in Section 4. The computed effects are called behaviors [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF] and are introduced in Section 3. They represent the temporal behaviors of processes by abstracting away values but keeping part of the structure of the program and are used to check if processes cooperate or not. Exposing concurrency in the language makes it possible to express the analysis easily, which would not have been the case if concurrency had been implemented as a library.

• A novel approach to subeffecting [START_REF] Nielson | Type and effect systems[END_REF], that is, subtyping on effects, based on row polymorphism [START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF] in Section 4.4. It allows to build a conservative extension of the existing type system with little overhead.

• A proof of the soundness of the analysis (Section 4.5): a well-typed program with reactive effects is reactive.

The paper ends with some examples (Section 5), discussion (Section 6) and related work (Section 7). The work presented here is implemented in the ReactiveML compiler 1 and it has already helped detecting many reactivity bugs. The implementation, the source code of the examples and an online toplevel are available at http://reactiveml.org/sas14.

Overview of the approach

ReactiveML extends ML with programming constructs inspired from synchronous languages [START_REF] Benveniste | The synchronous languages twelve years later[END_REF]. It introduces a built-in notion of parallelism where time is defined as a succession of logical instants. Each parallel process must cooperate to let time elapse. It is a deterministic model of concurrency that is compatible with the dynamic creation of processes [START_REF] Boussinot | Reactive C: an extension of C to program reactive systems[END_REF]. Synchrony gives us a simple definition for reactivity: a reactive ReactiveML program is one where each logical instant terminates.

Let us first introduce ReactiveML syntax and informal semantics using a simple program that highlights the problem of non-reactivity. Then we will discuss the design choices and limitations of our reactivity analysis using a few other examples.

A first example

We start by creating a process that emits a signal every timer seconds: In ReactiveML, there is a distinction between regular ML functions and processes, that is, functions whose execution can span several logical instants. Processes are defined using the process keyword. The clock process is parametrized by a float timer and a signal s. Signals are communication channels between processes, with instantaneous broadcast. The process starts by initializing a local reference time with the current time (line 2), read using the gettimeofday function of the Unix module from the standard library. Then it enters an infinite loop (line 3 to 6). At each iteration, it reads the new current time and emits the unit value on the signal s if enough time has elapsed (line 5). The compiler prints the following warning when compiling this process:

W: Line 3, characters 2-115, this expression may be an instantaneous loop

The problem is that the body of the loop is instantaneous. It means that this process never cooperates, so that logical instants do not progress. In ReactiveML, cooperating is done by waiting for the next instant using the pause operator. We solve our problem by calling it at the end of the loop (line 6):

if time' -. !time >= timer then (emit s (); time := time');

pause end

The second part of the program is a process that prints top every time a signal s is emitted. The do/when construct executes its body only when the signal s is present (i.e. it is emitted). It terminates by returning the value of its body instantaneously after the termination of the body. Processes have a consistent view of a signal's status during an instant. It is either present or absent and cannot change during the instant. Once again, this loop can be instantaneous, but this time it depends on the presence of the signal. While the signal s is absent, the process cooperates. When it is present, the body of the do/when executes and terminates instantaneously. So the body of the loop also terminates instantaneously, and a new iteration of the loop is started in the same logical instant. Since the signal is still present, the body of the do/when executes one more time, and so on. This process can also be fixed by adding a pause statement in the loop.

We can then declare a local signal s and put these two processes in parallel. The result is a program that prints top every second:

let process main = signal s default () gather (fun x y -> ()) in run (print_clock s) || run (clock 1. s)
The declaration of a signal takes as arguments the default value of the signal and a combination function that is used to compute the value of the signal when there are multiple emissions in a single instant. Here, the default value is () and the signal keeps this value in case of multiemission. The || operator represents synchronous parallel composition. Both branches are executed at each instant and communicate through the local signal s.

Intuitions and limitations

In the previous example, we have seen the first cause of non-reactivity: instantaneous loops. The second one is instantaneous recursive processes: let rec process instantaneous s = emit s (); run (instantaneous s)

W: This expression may produce an instantaneous recursion

The execution of emit is instantaneous, therefore the recursive call creates a loop that never cooperates. A sufficient condition to ensure that a recursive process is reactive is to have at least one instant between the instantiation of the process and any recursive call. The idea of our analysis is to statically check this condition.

This condition is very strong and is not always satisfied by interesting reactive programs. For instance, it does not hold for a parallel map (the let/and construct executes its two branches in parallel, matching is instantaneous):

let rec process par_map p l = match l with | [] -> [] | x :: l -> let x' = run (p x)
and l' = run (par_map p l) in x' :: l'

W: This expression may produce an instantaneous recursion

This process has instantaneous recursive calls, but it is reactive because the recursion is finite if the list l is finite. As the language allows to create mutable and recursive data structures, it is hard to prove the termination of such processes. For instance, the following expression never cooperates:

let rec l = 0 :: l in run (par_map p l)

Consequently, our analysis only prints warnings and does not reject programs.

ML functions are always considered instantaneous. So they are reactive if and only if they terminate. Since we do not want to prove their termination, our analysis has to distinguish RR n°8549 recursions through functions and processes. This allows us to assume that ML functions always terminate and to issue warnings only for processes. Furthermore, we do not deal with blocking functions, such as I/O primitives, that can also make programs non-reactive. Indeed, such functions should never be used in the context of cooperative scheduling. There are standard solutions for this problem [START_REF] Marlow | Extending the Haskell foreign function interface with concurrency[END_REF]. This analysis does not either consider the presence status of signals. It over-approximates the possible behaviors, as in the following example: The present/then/else construct executes its first branch instantaneously if the signal is present or executes the second branch with a delay of one instant if the signal is absent. This delayed reaction to absence, first introduced by Boussinot [START_REF] Boussinot | Reactive C: an extension of C to program reactive systems[END_REF], avoids inconsistencies in the status of signals. In the example, the signal is absent so the else branch is executed. It means that the recursion is not instantaneous and the process is reactive. Our analysis still prints a warning, because if the signal s could be present, the recursion would be instantaneous.

Finally, we only guarantee that the duration of each instant is finite, not that the program is real-time, that is, that there exists a bound on this duration for all instants, as shown in this example: The server process listens on a signal add to receive both a process p and a signal ack on which to send back results. As it creates one new process each time the add signal is emitted, this program can execute an arbitrary number of processes at the same time. It is thus not real-time, but it is indeed reactive, as waiting for the value of a signal takes one instant (one has to collect and combine all the values emitted during the instant).

The algebra of behaviors

The idea of our analysis is to abstract processes into a simpler language called behaviors, following Amtoft et al. [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF] and to check reactivity on these behaviors. The main design choice is to completely abstract values and the presence of signals. It is however necessary to keep an abstraction of the structure of the program in order to have a reasonable precision.

The behaviors

The algebra of behaviors is given by:3

κ ::= • | 0 | φ | κ || κ | κ + κ | κ; κ | µφ. κ | run κ
Actions that take at least one instant to execute, i.e. surely non-instantaneous actions, such as pause, are denoted •. Potentially instantaneous ones, like calling a pure ML function or emitting a signal, are denoted 0. The language also includes behavior variables φ to represent the behaviors of processes taken as arguments, since ReactiveML has higher-order processes.

Behaviors must reflect the structure of the program, starting with parallel composition. This is illustrated by the following example, which defines a combinator par_comb that takes as inputs two processes q1 and q2 and runs them in parallel in a loop: let process par_comb q1 q2 = loop (run q1 || run q2) end

The synchronous parallel composition terminates when both branches have terminated. It means that the loop is non-instantaneous if either q1 or q2 is non-instantaneous. To represent such processes, behaviors include the parallel composition, simply denoted ||. Similarly, we can define another combinator that runs one of its two inputs depending on a condition c: let process if_comb c q1 q2 = loop (if c then run q1 else run q2) end

In the case of if_comb, both processes must be non-instantaneous. As we want to abstract values, we represent the different alternatives using a non-determinstic choice operator + and forget about the conditions.

It is also necessary to have a notion of sequence, denoted ; in the language of behaviors, as illustrated by the two following processes: let rec process good_rec = pause; run good_rec let rec process bad_rec = run bad_rec; pause

W: This expression may produce an instantaneous recursion

The order between the recursive call and the pause statement is crucial as the good_rec process is reactive while bad_rec loops instantaneously. As it is defined recursively, the behavior κ associated with the good_rec process must verify that κ = •; run κ. The run operator is associated with running a process. This equation can be solved by introducing an explicit recursion operator µ so that κ = µφ. •; run φ. Recursive behaviors are defined as usual:

µφ. κ = κ[φ ← µφ. κ] µφ. κ = κ if φ ∈ fbv (κ)
We denote fbv (κ) the set of free behavior variables in κ. There is no operator for representing the behavior of a loop. Indeed, a loop is just a special case of recursion. The behavior of a loop, denoted κ ∞ (where κ is the behavior of the body of the loop), is thus defined as a recursive behavior by κ ∞ µφ. (κ; run φ).

Reactive behaviors

Using the language of behaviors, we can now characterize the behaviors that we want to reject, that is instantaneous loops and recursions. To formally define which behaviors are reactive, we first have to define the notion of a non-instantaneous behavior, i.e. processes that take at least one instant to execute:

Definition 1 (Non-instantaneous behavior). A behavior is non-instantaneous, denoted κ ↓, if: • ↓ φ ↓ κ1 ↓ κ1; κ2 ↓ κ2 ↓ κ1; κ2 ↓ κ1 ↓ κ1 || κ2 ↓ κ2 ↓ κ1 || κ2 ↓ κ1 ↓ κ2 ↓ κ1 + κ2 ↓ κ ↓ µφ. κ ↓ κ ↓ run κ ↓
Note that function calls are not non-instantaneous. The behavior • is as expected non-instantaneous. The fact that variables are considered non-instantaneous means that any process taken as argument is supposed to be non-instantaneous. The reactivity is then checked when this variable is instantiated with the actual behavior of the process. For the sequential and the parallel composition, only one of the two behaviors have to be non-instantaneous to makes the whole behavior non-instantaneous. For a non-deterministic choice, the two behaviors have to be non-instantaneous to be sure that the behavior is non-instantaneous since only one of the two behaviors will be actually executed. Finally, the instantaneity of a recursive behavior or a run only depends on the instantaneity of their body.

A behavior is said to be reactive if for each recursive behavior µφ. κ, the recursion variable φ does not appear in the first instant of the body κ. This enforces that there must be at least one instant between the instantiation of a process and each recursive call and is formalized in the following definition.

Definition 2 (Reactive behavior). A behavior κ is reactive if ∅ ⊢ κ, where the relation R ⊢ κ is defined by: R ⊢ 0 R ⊢ • φ ∈ R R ⊢ φ R ⊢ κ1 not(κ1 ↓) R ⊢ κ2 R ⊢ κ1; κ2 R ⊢ κ1 κ1 ↓ ∅ ⊢ κ2 R ⊢ κ1; κ2 R ⊢ κ1 R ⊢ κ2 R ⊢ κ1 || κ2 R ⊢ κ1 R ⊢ κ2 R ⊢ κ1 + κ2 R ∪ {φ} ⊢ κ R ⊢ µφ. κ R ⊢ κ R ⊢ run κ
The predicate R ⊢ κ means that the behavior κ is reactive with respect to the set of variables R, that is, these variables do not appear in the first instant of κ and all the recursions inside κ are not instantaneous. The rule for a variable φ checks that φ is not a recursion variable introduced in the current instant. The recursion variables are added to the set R when checking the reactivity of a recursive behavior µφ. κ. In the case of the sequence κ 1 ; κ 2 , we can remove variables from R if κ 1 is non-instantaneous. One can also check from the definition of κ ∞ as a recursive behavior that this definition also implies that the body of a loop is non-instantaneous. The behaviors 0 and • are always reactive. The other rules only checks that sub-expressions are reactive.

Using this definition, we can see for example that the behavior µφ. •; φ is reactive:

φ ⊢ • • ↓ ∅ ⊢ φ φ ⊢ •; φ ∅ ⊢ µφ. •; φ

Equivalence on behaviors

We can define an equivalence relation ≡ on behaviors that will be used to simplify the behaviors. The relation is reflexive, symmetric and transitive closure of the following rules. The operators ; and || and + are idempotent and associative. || and + are commutative (but not ; ). The 0 behavior (resp. •) is the neutral element of ; and || (resp. +). The relation also satisfies the following rules (where op is ; or || or +):

κ 1 ≡ κ 2 µφ. κ 1 ≡ µφ. κ 2 κ 1 ≡ κ 2 run κ 1 ≡ run κ 2 • ∞ ≡ • κ 1 ≡ κ ′ 1 κ 2 ≡ κ ′ 2 κ 1 op κ 2 ≡ κ ′ 1 op κ ′ 2
It is easy to show, for example, that: µφ.

((• || 0); (run φ + run φ)) ≡ µφ. (•; run φ).
An important property of this relation is that it preserves reactivity. It is expressed as follows:

Property 1. if κ 1 ≡ κ 2 and R ⊢ κ 1 then R ⊢ κ 2 .
Proof. By induction on the proof of κ 1 ≡ κ 2 .

RR n°8549

4 The type-and-effect system

The link between processes and behaviors is done by a type-and-effect system [START_REF] Lucassen | Polymorphic effect systems[END_REF], following the work of Amtoft et al. [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF]. The behavior of a process is its effect computed using the type system. After type-checking, the compiler checks the inferred behaviors and prints a warning if one of them is not reactive.

The type system is a conservative extension of the original one of ReactiveML, that is, it is able to assign a behavior to any ReactiveML program that was accepted previously. It is an important feature as we only want to show warnings and not reject programs.

A type system is a simple way to specify a higher-order static analysis. It can be implemented efficiently using classic destructive unification techniques [START_REF] Lee | Proofs about a folklore let-polymorphic type inference algorithm[END_REF].

Abstract syntax

We consider here a kernel of ReactiveML: Values are constants c (integers, unit value (), etc.), pairs of values, signal names n, functions and processes. The language is a call-by-value lambda-calculus, extended with constructs for creating (process) and running (run) processes, waiting for the next instant (pause), parallel definitions (let/and), declaring signals (signal), emitting a signal (emit) and several control structures: the test of presence of a signal (present), the unconditional loop (loop), weak preemption (do/until) and suspension (do/when). The expression do e 1 until s(x) → e 2 executes its body e 1 and interrupts it if s is present. In case of preemption, the continuation e 2 is executed on the next instant, binding x to the value of s. We denote variables that do not appear free in the body of a let and () the unique value of type unit. From this kernel, we can encode most constructs of the language:

v ::= c | (v, v) | n | λx.e |
e 1 ||

Types

Types are defined by:

τ ::= α | T | τ × τ | τ → τ | τ process[κ] | (τ, τ ) event (types) σ ::= τ | ∀φ. σ | ∀α. σ (type schemes) Γ ::= ∅ | Γ, x : σ (environments)
A type is either a type variable α, a base type T (like bool or unit), a product, a function, a process or a signal. The type of a process is parametrized by its return type and its behavior.

The type (τ 1 , τ 2 ) event of a signal is parametrized by the type τ 1 of emitted values and the type τ 2 of the received value (since a gathering function of type τ 1 → τ 2 → τ 2 is applied).

RR n°8549

Types schemes quantify universally over type variables α and behavior variables φ. We denote ftv (τ ) (resp. fbv (τ )) the set of type (resp. behavior) variables free in τ and fv (τ ) = ftv (τ ), fbv (τ ). Instantiation and generalization are defined in a classic way:

σ[α ← τ ] ≤ ∀α. σ σ[φ ← κ] ≤ ∀φ. σ gen(τ, e, Γ) = τ if e is expansive gen(τ, e, Γ) = ∀ ᾱ.∀ φ. τ where ᾱ, φ = fv (τ ) \ fv (Γ) otherwise
Analogously to the treatment of references in ML, we must be careful not to generalize expressions that allocate signals. We use the syntactic criterion of expansive and non-expansive expressions [START_REF] Tofte | Type inference for polymorphic references[END_REF]. An expression is expansive if it can allocate a signal or a reference, in which case its type should not be generalized. Here is an example of program wrong program that would have been accepted if there is no distinction between expansive and non-expansive expressions.

let emit_s = signal s default [] gather (fun x y -> x :: y) in (fun x -> emit x) in emit_s 1 emit_s "error"
The notions of reactivity and equivalence are lifted from behaviors to types. A type is reactive if it contains only reactive behaviors. Two types are equivalent, also denoted τ 1 ≡ τ 2 , if they have the same structure and their behaviors are equivalent.

Typing rules

Typing judgments are given by Γ ⊢ e : τ | κ meaning that, in the type environment Γ, the expression e has type τ and behavior κ. We write Γ ⊢ e : τ | ≡ 0 when the behavior of the expression e is equivalent to 0. The initial typing environment Γ 0 gives the types of primitives:

Γ 0 [true : bool; fst : ∀α 1 , α 2 . α 1 × α 2 → α 1 ; . . .]
The rules defining the type system are given in Figure 1. If all the behaviors are erased, it is exactly the same type system as the one presented in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF], which is itself an extension of the ML type system. We discuss here the novelties of the rules related to behaviors:

• The Process rule stores the behavior of the body in the type of the process, as usual in type-and-effect systems. The presence of the κ ′ behavior and the Mask rule are related to subeffecting and will be discussed in Section 4.4.

• A design choice made in ReactiveML is to separate pure ML expressions, that are surely instantaneous, from processes. For instance, it is impossible to call pause within the body of a function, that must be instantaneous. A static analysis (used for efficient code generation) performed before typing checks this well-formation of expressions, denoted k ⊢ e in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF] and recalled in Appendix A. Requiring the behavior of some expressions, like the arguments of an application or the body of a function, to be equivalent to 0 does not add any new constraint with respect to this existing analysis.

• We do not try to prove the termination of pure ML functions without any reactive behavior.

The App rule shows that we assume that function calls always terminate instantaneously. That is why there is no behavior associated with functions: there are no behaviors on arrow types unlike traditional type-and-effect systems.

equivalent to κ 1 || κ 2 or that await e 1 (x) in e 2 has behavior • ∞ + (•; κ 2 ) ≡ •; κ 2 (reading the value of a signal takes at least one instant).

• The pause operator cannot be encoded using the delay to the reaction to absence as in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF] by: pause signal s default () gather (λx.λy.()) in present s then () else ()

We have chosen to completely abstract values. As in the imprecise example of Section 2.2, we do not consider the fact that the signal s is always absent, so that only the second branch of the present is executed. The consequence is that the behavior computed for this encoding, that is, 0; (0 + (•; 0)) ≡ 0, is the opposite of the expected behavior of pause.

• The loop construct can be encoded as a recursive process by: loop e run ((rec l = λx.process (run x; run (l x))) (process e))

Unlike pause, we could have removed loop from our kernel and used this encoding without affecting the results given by the reactivity analysis. Indeed, by applying the rules here, we have that:

loop : ∀φ. α process[φ] → α ′ process[µφ ′ . run φ; run φ ′ ]
If we assume that Γ ⊢ e : τ | κ, then the behavior of this encoding is: run (µφ ′ . run κ; run φ ′ ). It is not equivalent to κ ∞ in the sense of Section 3.3, but it is reactive iff κ ∞ is reactive, as the run operator does not influence reactivity (see Definition 2).

• The reason why the behavior associated with loop is equal to (0; κ) ∞ and not simply κ ∞ will be explained in Section 4.5. Intuitively, the soundness proof will use an induction on the size of the behaviours and thus requires the behavior of a sub-expression to always be smaller. This also applies for signal and do/when.

• Finally, note that there is no special treatment for recursive processes. We will see in the next section that recursive behaviors are introduced during unification. An example of typing derivation justifying the presence of the run operator will be given in Section 6.1.

Subeffecting with row polymorphism

The typing rule (Process) for the creation of processes intuitively mean that a process has at least the behavior of its body. The idea is to add a free behavior variable to represent other potential behaviors of the process. This subtyping restricted to effects is often referred to as subeffecting [START_REF] Nielson | Type and effect systems[END_REF]: we can always replace an effect with a bigger, i. If the behavior of a process had been exactly equal to the behavior of its body, this expression would have been rejected by the type system. The consequence of the typing rule for processes is that the principal type of an expression process e is always of the form κ + φ where κ is the behavior of e and φ a free variable. The idea to use a free type variable to represent other possible types is reminiscent of Remy's row types [START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF]. It makes it possible to implement subeffecting using only unification, without manipulating constraint sets as in traditional approaches [START_REF] Talpin | The type and effect discipline[END_REF][START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF]. It thus becomes easier to integrate it into any existing ML type inference implementation. For instance, OCaml type inference is also based on row polymorphism [START_REF] Rémy | Using, understanding, and unraveling the OCaml language from practice to theory and vice versa[END_REF], so it would be easy to implement our type system on top of the full language.

We can reuse any existing inference algorithm, like algorithm W or M [START_REF] Lee | Proofs about a folklore let-polymorphic type inference algorithm[END_REF] and add only the following algorithm U κ for unification of behaviors. It takes as input two behaviors and returns a substitution that maps behavior variables to behaviors, that we denote [φ 1 → κ 1 ; φ 2 → κ 2 ; . . . ]. During unification, the behavior of a process is always either a behavior variable φ, a row κ + φ or a recursive row µφ. (κ + φ ′ ). Therefore, the unification algorithm only has to consider these cases:

Uκ(κ, κ) = [] Uκ(φ, κ) = Uκ(κ, φ) = [φ → µφ. κ] if occur check(φ, κ) [φ → κ] otherwise Uκ(κ1 + φ1, κ2 + φ2) = [φ1 → κ2 + φ; φ1 → κ1 + φ], φ fresh Uκ(µφ ′ 1 . (κ1 + φ1), κ2) = Uκ(κ2, µφ ′ 1 . (κ1 + φ1)) = let K1 = µφ ′ 1 . (κ1 + φ1) in Uκ(κ1[φ ′ 1 ← K1] + φ1, κ2)
It should be noted that unification never fails, so that we obtain a conservative extension of ReactiveML type system. This unification algorithm reuses traditional techniques for handling recursive types [START_REF] Huet | A unification algorithm for typed λ-calculus[END_REF]. The last case unfolds a recursive row to reveal the row variable, so that it can be unified with other rows. A downside of our approach is that it introduces one behavior variable for each process, so that the computed behaviors may become very big and unreadable. The purpose of the Mask rule is to remedy this, by using effect masking [START_REF] Lucassen | Polymorphic effect systems[END_REF]. The idea is that if a behavior variable appearing in the behavior is free in the environment, it is not constrained so we can give it any value. In particular, we choose to replace it with •, which is the neutral element of +, so that it can be simplified away.

Comparison with traditional approaches

Usually, subeffecting is not expressed as a syntax directed rule. For instance, in [START_REF] Talpin | The type and effect discipline[END_REF][START_REF] Nielson | Type and effect systems[END_REF], it is defined as (we reuse the notations of our type system for comparison):

Γ ⊢ e : τ | κ κ ⊑ κ ′ Γ ⊢ e : τ | κ ′
The order ⊑ on effects is given by set inclusion when effects are sets [START_REF] Talpin | The type and effect discipline[END_REF] (of regions for example). In our case, it is defined by:

κ 1 ⊑ κ 1 + κ 2 κ 2 ⊑ κ 1 + κ 2 κ 1 ≡ κ 2 κ 1 ⊑ κ 2
In the work of Amtoft et al. [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF], effects must be simple, that is, effects on arrows are syntactically forced to be variables. A constraint set C is added to the type system to keep track of the relations between variables and effects. Subeffecting is then expressed as:

Γ, C ⊢ e : τ | κ Γ, C ∪ {κ ⊑ φ} ⊢ process e : τ process[φ] | 0
These three formulations appear to be equivalent. Indeed, our system and the one of Amtoft et al. [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF] are just syntax-directed versions of the classic approach, where the subsumption rule is mixed with lambda abstractions (or process abstractions in our case).

Proof of soundness

We now present the proof sketch of the soundness of our analysis, that is, that at each instant, the program admits a finite derivation in the big-step semantics of the language and rewrites to a well-typed program with reactive effects.

The big-step semantics of ReactiveML, also called the behavioral semantics in reference to the semantics of Esterel [START_REF] Potop-Butucaru | Compiling Esterel[END_REF], describes the reaction of an expression during an instant i by the smallest signal environment S i (the set of present signals) such that:

e i Ei,bi ---→ Si e i+1
which means that during the instant i, in the signal environment S i , the expression e i rewrites to e i+1 and emits the signals in E i . The boolean b i indicates if e i+1 has terminated. Additional conditions express, for instance, the fact that the emitted values in E i must agree with the signal environment S i . An execution of a program comprises a succession of a (potentially infinite) number of reactions and terminates when the status b i is equal to true. The definition of the semantics was introduced in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF] and is recalled in Appendix B.

A program is reactive if at each instant, the semantics derivation of e i is finite. To prove that, we first isolate the first instant of the behavior of e i , noted fst(κ i ). This function is formally defined by:

fst(0) = fst(•) = 0 fst(φ) = φ fst(run κ) = run (fst(κ)) fst(κ 1 || κ 2 ) = fst(κ 1 ) || fst(κ 2 ) fst(κ 1 + κ 2 ) = fst(κ 1 ) + fst(κ 2 ) fst(κ 1 ; κ 2 ) = fst(κ 1 ) if κ 1 ↓ fst(κ 1 ); fst(κ 2 ) otherwise fst(µφ. κ) = fst(κ[φ ← µφ. κ])
The important property of this function is that if a behavior κ i of e i is reactive (as defined in Section 3.2), then fst(κ i ) is finite. Hence we can prove by induction on the size of fst(κ i ) that the semantics derivation is finite. The soundness theorem is stated as follows: Proof. The proof has two parts. The first part is the proof that the result is well-typed. We use classic syntactic techniques for type soundness [START_REF] Pierce | Types and programming languages[END_REF] on the small-step semantics described in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF].

The proof of equivalence of the two semantics is also given in the same paper. The second part is the proof that the semantics derivation of one instant is finite by induction on the size of the first-instant behavior of well-typed expressions. We only consider one instant because thanks to type preservation, if the theorem is true for one instant, it is true for the following ones. The details of the proof are given in Appendix C.

Examples

We present here the result of the analysis on some examples. These examples can be downloaded and tried at http://reactiveml.org/sas14. Using a type-based analysis makes it easy to deal with cases of aliasing, as in the following example:4 let rec process p = let q = (fun x -> x) p in run q val p: 'a process[rec 'r. (run 'r + .

.)] W: This expression may produce an instantaneous recursion

The process q has the same type as p, and thus the same behavior, so the instantaneous recursion is easily detected. As for objects in OCaml [START_REF] Rémy | Using, understanding, and unraveling the OCaml language from practice to theory and vice versa[END_REF], row variables that appear only once are printed '..'.

The analysis can also handle combinators. For instance, the type system computes the following behavior for the par_comb example of Section 3.1:

let process par_comb q1 q2 = loop run q1 || run q2 end val

par_comb: 'a process['r1] -> 'b process ['r2] -> unit process[rec 'r3. ((run 'r1 || run 'r2); 'r3 + ..)]

There is no warning when defining the combinator because it is not possible to decide its reactivity. Indeed, the synchronous parallel composition terminates when both branches have terminated. It means that the loop is non-instantaneous if either q1 or q2 is non-instantaneous. Formally, the computed behavior is reactive because free behavior variables are considered to be non-instantaneous (see Definition 2). The reactivity is then checked at the instantiation. If we instantiate the par_comb combinator with two anonymous processes, one instantaneous and the other non-instantaneous, then we obtain a process that is indeed reactive, so no warning is printed:

let process p1 = run (

par_comb (process ()) (process (pause))) val p1: unit process[run(rec 'r.(run 0 || run *);'r) + ..]

However, if the two processes are instantaneous, then the loop becomes instantaneous. The behavior that results is obviously non-reactive, so a warning is shown:

let process p2 = run (

par_comb (process ()) (process ())) val p2: unit process[run(rec 'r.(run 0||run 0);'r) + ..)] W: This expression may produce an instantaneous recursion

Here is another more complex example using higher-order functions and processes. We define a function h_o that takes as input a combinator f. It then creates a recursive process that applies f to itself and runs the result:

let h_o f = let rec process p = let q = f p in run q in p val h_o: ('a process[run 'r1 + 'r2] -> 'a process['r1]) -> 'a process[run 'r1 + 'r2]
If we instantiate this function with a process that waits an instant before calling its argument, we obtain a reactive process:

let process good = run (h_o (fun x -> process (pause; run x))) val good: 'a process[run (run (rec 'r1. *; run (run 'r1))) + ..] This is no longer the case if the process calls its argument instantaneously. The instantaneous recursion is again detected by our static analysis: let process pb = run (h_o (fun x -> process (run x))) val pb: 'a process [run (run (rec 'r1. run

run 'r1)) + ..] W: This expression may produce an instantaneous recursion

Another process that can be analyzed is a fix-point operator. It takes as input a function expecting a continuation, and applies it with itself as the continuation. This fix-point operator can be used to create a recursive process:

let rec fix f x = f (fix f) x val fix: (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b let process main = let process p k v = print_int v; run (k (v+1
)) in run (fix p 0) val main: 'a process [(run (rec 'r.

run 'r)) + ..] W: This expression may produce an instantaneous recursion

In the example, the analysis detects the problem of reactivity although there is no explicit recursive process.

where Γ ′ = Γ, p : β process[0 + •]. Thanks to the addition of run, run p now has a behavior equal to run φ. Then, the only way to type the process is to give it the behavior µφ. (run φ + κ ′ ) (where κ ′ is not constrained). This also explains why there is no equivalence rule to simplify a run. For instance, run 0 is not equivalent to 0.

Implementation

The type inference algorithm of ReactiveML has been extended to compute the behaviors of processes, with minimal impact on its structure and complexity thanks to the use of row polymorphism for subeffecting (see Section 4.4). The rules given in Section 3.2 are easily translated into an algorithm for checking the reactivity of behaviors that is polynomial in the size of behaviors. Inference simplifies behaviors during the computation, but does not necessarily compute the smallest behavior possible. For instance, simplifying κ + κ can be costly in some cases, so it only checks simple cases (e.g. if κ = 0 or κ = •).

In practice, the analysis has an impact on the type-checking time but it is negligible compared to the global compilation time. For example on a 1.7GHz Intel Core i5 with 4Go RAM, the compilation of the examples of the ReactiveML distribution (about 5000 lines of code) takes about 0.15s where 0.02s are spent in the type checker (0.005s without the reactivity analysis). Then it takes 3.5s to compile the generated OCaml code.

Handling references

References are not included in the kernel of our language. However, they are relevant as they can be used to encode recursivity, as in the following example that creates a process that loops instantaneously:

let landin () = let f = ref (process ()) in f := process (run !f); !f val landin: unit -> unit process[0 + (rec 'r1. run (0 + 'r1)) + .

.] W: This expression may produce an instantaneous recursion

As our analysis does not have any special case for recursive processes and only relies on unification, it is able to detect such reactivity problems even though there is no explicit recursion.

Evaluation

The analysis is very useful to detect early small reactivity bugs such as the one presented Section 2.1. We have also used the analysis on bigger applications: a mobile ad-hoc network simulator (1800 Source Lines Of Code), a sensor network simulator (1700 SLOC), and a mixed music sequencer (3400 SLOC).

There is no warning for both simulators. For the mixed music sequencer, there are warnings on eleven processes. Eight warnings are due to structural recursions (similar to the example par_map). Most of them come from the fact that the program is a language interpreter defined as a set of mutually recursive processes on the abstract syntax tree. Another warning comes from a record containing a process that is not annotated with a non-instantaneous behavior. The last two warnings are due to loops around the execution of a musical score. In this case, the analysis does not use the fact that the score is a non-empty list.

In all these cases, it was easy for the programmer to check that these warnings were false positives. The last three warnings can be removed by adding a pause in parallel to the potentially instantaneous expressions.

Other models of concurrency

We have already extended our analysis to take into account time refinement [START_REF] Mandel | Time refinement in a functional synchronous language[END_REF]. We believe this work could be applied to other models of concurrency. One just needs to give the behavior • to operations that cooperate with the scheduler, like yield. We are considering an extension to the X10 language,5 where cooperation points could be clocks.

In a synchronous world, the fact that each process cooperates at each instant implies the reactivity of the whole program, as processes are executed in lock-step. In another model, assumptions on the fairness of the scheduler may be required. This should not be a major obstacle, as these hypotheses are already made in most systems, e.g. in Concurrent Haskell [START_REF] Jones | Concurrent Haskell[END_REF]. The distinction between processes and functions is important to avoid showing a warning for all recursive functions.

Related work

The analysis of instantaneous loops is an old topic on which much has already been written, even recently [START_REF] Abel | Well-founded recursion with copatterns[END_REF][START_REF] Jeffrey | Functional reactive programming with liveness guarantees[END_REF][START_REF] Atkey | Productive coprogramming with guarded recursion[END_REF]. It is related to the analysis of productivity and deadlocks in list programs [START_REF] Sijtsma | On the productivity of recursive list definitions[END_REF] or guard conditions in proof assistants [START_REF] Barthe | Type-based termination of recursive definitions[END_REF], etc. Our purpose was to define an analysis that can be used in the context of a general purpose language (mutable values, recursion, etc.). We tried to find a good compromise between the complexity of the analysis and its precision for typical reactive programs written in ReactiveML. The programmer must not be surprised by the analysis and the error messages. We focus here only on directly related work.

Our language of behaviors and type system are inspired by the work of Amtoft et al. [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF]. Their analysis is defined on the ConcurrentML [START_REF] Reppy | Concurrent programming in ML[END_REF] language, which extends ML with message passing primitives. The behavior of a process records emissions and receptions on communication channels. The authors use the type system to prove properties on particular examples, not for a general analysis. For instance, they prove that emission on a given channel always precedes the emission on a second channel in a given program. The idea of using a type-and-effect system for checking reactivity or termination is not new. For instance, Boudol [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF] uses a type-and-effect system to prove termination of functional programs using references, by stratifying memory to avoid recursion through references.

Reactivity analysis is a classic topic in synchronous languages, that can also be related to causality. In Esterel [START_REF] Potop-Butucaru | Compiling Esterel[END_REF], the first imperative synchronous language, it is possible to react immediately to the presence and the absence of a signal. The consequence is that a program can be non-reactive because there is no consistent status for a given signal: the program supposes that a signal is both present and absent during the same instant. This problem is solved by checking that programs are constructively correct [START_REF] Potop-Butucaru | Compiling Esterel[END_REF]. Our concurrency model, inherited from the work of Boussinot [START_REF] Boussinot | Reactive C: an extension of C to program reactive systems[END_REF], avoids these problems by making sure that processes are causal by construction. We then only have to check that loops are not instantaneous, which is called loopsafe by Berry [START_REF] Potop-Butucaru | Compiling Esterel[END_REF]. It is easy to check that an Esterel program is loop-safe as the language is first order without recursion [START_REF] Tardieu | Loops in Esterel[END_REF].

Closer to ReactiveML, the reactivity analysis of FunLoft [START_REF] Amadio | Feasible reactivity in a synchronous π-calculus[END_REF] not only checks that instants terminate, but also gives a bound on the duration of the instants through a value analysis.

The analysis is also restricted to the first-order setting. In ULM [START_REF] Boudol | ULM: A core programming model for global computing[END_REF], each recursive call induces an implicit pause. Hence, it is impossible to have instantaneous recursions, at the expense of expressivity. For instance, in the server example of Section 2.2, a message could be lost between receiving a message on add and awaiting a new message.

The causality analysis of Lucid Synchrone [START_REF] Cuoq | Modular Causality in a Synchronous Stream Language[END_REF] is a type-and-effect system using row types. It is based on the exception analysis defined by Leroy et al. [START_REF] Leroy | Type-based analysis of uncaught exceptions[END_REF]. Both are a more direct application of row types [START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF], whereas our system differs in the absence of labels in rows.

Conclusion

We have presented a reactivity analysis for the ReactiveML language. The idea of the analysis is to abstract processes into a simpler language called behaviors using a type-and-effect system. Checking reactivity of behaviors is then straightforward. We have proven the soundness of our analysis, that is, that a well-typed program with reactive effects is reactive. Thanks in particular to the syntactic separation between functions and processes, the analysis does not detect too many false positives in practice. It is implemented in the ReactiveML compiler and it has been proven very useful for avoiding reactivity bugs. We believe that this work can be applied to other models of cooperative scheduling.

A Well-formation of expressions

In order to separate pure ML expressions from reactive expressions, we define a well-formation predicate denoted k ⊢ e with k ∈ {0, 1}. An expression e is necessarily instantaneous (or combinatorial) if 0 ⊢ e. It is reactive (or sequential in classic circuit terminology) if 1 ⊢ e. The rules defining this predicate are given in Figure 2. The design choices of this analysis, like the fact that pairs must be instantaneous, are discussed in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF].

k ⊢ e means that 1 ⊢ e or 0 ⊢ e, that is, that e can be used in any context. This is true of any instantaneous expressions, as there is no rule with 0 ⊢ e in the conclusion. The important point is that the body of functions must be instantaneous, while the body of a process may be reactive.

B Big-step semantics

The big-step semantics has been introduced in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF]. We recall its definition here since it is used in the soundness theorem of the type system.

B.1 Notations

Signal environment

A signal environment S is a function

S [(d 1 , g 1 , m 1 )/n 1 , . . . , (d k , g k , m k )/n k ]
that maps a signal name n i to a tuple (d i , g i , m i ) where d i is the default value of the signal, g i its combination function and m i is the multi-set of values emitted during the reaction. If the signal n i has the type (τ 1 , τ 2 ) event, then these fields have the following types:

d i : τ 2 g i : τ 1 → τ 2 → τ 2 m i : τ 2 multiset
We denote S d (n i ) = d i , S g (n i ) = g i and S m (n i ) = m i . We also define S v (n i ) = fold g i m i d i where:

fold f ({v 1 } ⊎ m) v 2 = fold f m (f v 1 v 2 ) fold f ∅ v 2 = v
We denote n ∈ S when the signal n is present, that is, when S m (n) = ∅, and n ∈ S otherwise.

Events

An event E is a function mapping a signal name to a multi-set of values:

E [m 1 /n 1 , . . . , m k /n k ]
Events represent the values emitted during an instant. S m is the event associated with the signal environment S.

Operations on signal environments and events

The union of events is the point-wise union, that is, if

E = E 1 ⊔ E 2 , then for all n ∈ Dom(E 1 ) ∪ Dom(E 2 ): E(n) = E 1 (n) ⊎ E 2 (n)
Similarly, the inclusion of events is the point-wise inclusion. We define the inclusion of signal environments by:

S 1 ⊑ S 2 iff S m 1 ⊑ S m 2

B.2 Big-step semantics

At each instant, the program reads inputs I i and produces outputs O i . The reaction of an expression is defined by the smallest signal environment S i (for the relation ⊑) such that:

e i Ei,bi ---→ Si e i+1 where (I i ⊔ E i ) ⊑ S m i (1) O i ⊑ E i (2) S d i ⊆ S d i+1 and S g i ⊆ S g i+1 (3)
(1) The signal environment must contain the inputs and emitted signals.

(2) The outputs are included in the set of emitted signals.

(3) Default values and combination functions are kept from one instant to the next.

The rules defining the relation are given in Figure 3 and Figure 4:

• The rule for pause shows the meaning of the boolean b: if it is false, it means that the expression is stuck waiting for the next instant.

• The let/and construct executes its two branches in parallel until both are terminated (the termination status is tt).

• The present construct executes the then branch immediately if the signal is present, but it executes the else branch on the next instant if it is absent. (Let-Done) • The do/when construct executes its body only if the signal n is present. If the body terminates, that is, if it rewrites to a value v, then the construct also terminates instantaneously and rewrites to the same value.

e 1 E1,tt ---→ S λx. e e 2 E2,tt ---→ S v 2 e[x ← v 2 ] E3,tt ---→ S v e 1 e 2 E1⊔E2⊔E3,tt ---------→ S v v[x ← rec x = v] E,tt ---→ S v ′ rec x = v E,tt ---→ S v ′ e E,tt -
e 1 E1,tt ---→ S v 1 e 2 E2,tt ---→ S v 2 e 3 [x 1 ← v 1 ; x 2 ← v 2 ] E3,b3 -
--→ S v e 1 E1,tt ---→ S v 1 e 2 E2,tt ---→ S v 2 (e 1 , e 2 ) E1⊔E2,tt ------→ S (v 1 , v 2 ) e 1 E1,tt ---→ S v 1 e 2 E2,tt ---→ S v 2 n fresh e[x ← n] E,b --→ S e ′ S(n) = (v 1 , v 2 ,
• The unconditional loop keeps executing its body until that body stops to wait for the next instant, that is, until its termination status b becomes false. In particular, an expression like loop (), where the body always terminates instantaneously, does not have a semantics as it would require an infinite derivation tree.

• emit e 1 e 2 evaluates e 1 into a signal name n and adds the result of the evaluation of e 2 to the multi-set of values emitted on n.

• The declaration of a signal evaluates the default value and combination function, and then evaluates the body after substituting the variable x with a fresh signal name n. In this paper, we have kept implicit the sets of signal names that are used to ensure the freshness of this name (see [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF] for the details).

• The preemption in ReactiveML is weak, that is, a process can only be preempted at the end of the instant. This is reflected by the fact that e 1 is always evaluated, regardless of the status of the signal n. It also means that, when the signal is present, e 2 is executed at the next instant.

C Proof of soundness

The intuition of the proof of soundness (Theorem 2) is that the first instant of a reactive behavior is a finite behavior, without any recursion. We then prove the finiteness of the semantics derivation by induction on the size of behaviors. In the case of a recursive behavior, the first-instant behavior is well-defined only if the behavior is reactive, that is, if the recursion is not instantaneous. Definition 4. A behavior is finite, denoted κ ∈ κ ⋆ , if it does not contain any recursive behavior. The finite behaviors κ ⋆ are defined by:

C.1 First instant of a behavior

κ ⋆ ::= • | 0 | φ | κ ⋆ || κ ⋆ | κ ⋆ + κ ⋆ | κ ⋆ ; κ ⋆ | run κ ⋆
We can now express the most important property of reactive behaviors, that is, that the first instant of a reactive behavior is finite. This property is used in the soundness proof to guaranty that at each instant the reaction is finite since its behavior is finite.

C.2 Soundness

We do not try to prove that functions terminate and we focus completely on processes. We assume that all functions terminate, which is reflected in the App rule of Figure 1 by the fact that the behavior of the application is always the instantaneous behavior 0. This hypothesis is made possible by the syntactic distinction between functions and processes. It must be expressed formally with respect to the big-step semantics before we can show soundness. To do so, we reuse the predicate 0 ⊢ e which is defined in Appendix A and means that the expression e is surely instantaneous.

Hypothesis 1 (Function calls always terminate). For any expression e such that 0 ⊢ e, there exists a finite derivation Π and a value v such that:

Π e E,tt ---→ S v
We first need to prove the soundness of our definition of non-instantaneous behavior, as expressed in the following lemma: Proof. By induction on the derivation of the big-step semantics.

We can now prove the soundness theorem.

Proof. The proof has two parts. The first part is the proof that the result is well-typed. We use classic syntactic techniques for type soundness [START_REF] Pierce | Types and programming languages[END_REF] on the small-step semantics described in [START_REF] Mandel | ReactiveML: a reactive extension to ML[END_REF].

The proof of equivalence of the two semantics is also given in the same paper. The second part is the proof that the semantics derivation of one instant is finite by induction on the size of the first-instant behavior of well-typed expressions. We only consider one instant because thanks to type preservation, if it is true for one instant, it is true for the following ones.

• Case e 1 e 2 and rec x = v: By Hypothesis 1.

• Case run e: We know that 0 ⊢ e and run e is well-typed. The expression e rewrites to a value by Hypothesis 1, that is necessarily of the form process e 1 because it is the only kind of value that can have type τ process We can apply the induction hypothesis as the first-instant behavior of e 1 , i.e. fst(κ), is smaller than the first-instant behavior of run (process e 1 ), which is also the first-instant behavior of run e because e and process e 1 have the same type (by subject reduction). Indeed, we have: fst(run (κ + κ ′ )) = run (fst(κ)) + run (fst(κ ′ ))

Using the induction hypothesis, we can build the complete derivation of run e:

2

 2 let process clock timer s = let time = ref (Unix.gettimeofday ()) in loop let time' = Unix.gettimeofday () in if time' -. !time >= timer then (emit s (); time := time') end

  [START_REF] Dimino | Lwt User Manual[END_REF], characters 2-78, this expression may be an instantaneous loop

  let rec process imprecise = signal s default () gather (fun x y -> ()) in present s then () else (* implicit pause *) (); run imprecise W: This expression may produce an instantaneous recursion

  let rec process server add = await add(p, ack) in run (server add) || let v = run p in emit ack v

  process e e ::= x | c | (e, e) | λx.e | e e | rec x = v | process e | run e | pause | let x = e and x = e in e | signal x default e gather e in e | emit e e | present e then e else e | loop e | do e until e(x) → e | do e when e

Theorem 2 (e

 2 Soundness). If Γ ⊢ e : τ | κ and τ and κ are reactive and we suppose that function calls terminate, then there exists e ′ such that e ′ and Γ ⊢ e ′ : τ | κ ′ with κ ′ reactive.

k ⊢ x k ⊢ c 0 ⊢ e 1 00 ⊢ e 1 0 ⊢ e 2 k ⊢ emit e 1 e 2 0 ⊢ e 1 ⊢ e 1 1 ⊢ e 2 1 ⊢Figure 2 :

 1122112 Figure 2: Well-formation rules

2 b 1 ∧

 21 b 2 = ff let x 1 = e 1 and x 2 = e 2 in e 3 E1⊔E2,ff ------→ S let x 1 = e ′ 1 and x 2 = e ′ 2 in e 3

3 let x 1 = e 1 and x 2 = e 2 in e 3 E1⊔E2⊔E3 1 present e then e 1 else e 2 E⊔E1present e then e 1 else e 2 E

 3123122 Figure 3: Big-step semantics

m) signal x default e 1 gather e 2 1 do e 1 1 do e 1 2 Figure 4 :

 2111124 Figure 4: Remaining rules for the big-step semantics

Definition 3 .

 3 The first-instant of a behavior, denoted fst(κ) is the part of the behavior that corresponds to the execution of the first instant of the corresponding process. It is formally defined by:fst(0) = fst(•) = 0 fst(φ) = φ fst(run κ) = run (fst(κ)) fst(κ 1 || κ 2 ) = fst(κ 1 ) || fst(κ 2 ) fst(κ 1 + κ 2 ) = fst(κ 1 ) + fst(κ 2 ) fst(κ 1 ; κ 2 ) = fst(κ 1 ) if κ 1 ↓ fst(κ 1 ); fst(κ 2 ) otherwise fst(µφ. κ) = fst(κ[φ ← µφ. κ])

Property 3 .

 3 If κ is reactive (Definition 2), then fst(κ) is a finite behavior, i.e. ∅ ⊢ κ ⇒ fst(κ) ∈ κ ⋆ .Proof. By induction on the structure of behaviors.

Lemma 4 .

 4 An expression whose behavior is not instantaneous never reduces instantaneously:Γ ⊢ e : τ | κ ∧ κ ↓ ∧ e

e 1

 1 [κ]. So there exists Π such that Π e Then, we can construct the following type derivation: Γ ⊢ e 1 : τ | κ Γ ⊢ process e 1 : τ process[κ + κ ′ ] | 0 Γ ⊢ run (process e 1 ) : τ | run (κ + κ ′ )

1 •

 1 Case pause: The derivation is already finite.• Case present e then e 1 else e 2 : As in the first case:

  e. less precise, one. It allows to assign a behavior to any correct ReactiveML program. For instance, it is possible to build a list of two processes with different behaviors (the • behavior is printed '*' and behavior variables φ are denoted 'r):

	let process p1 = ()
	val p1: unit process[0 + 'r1]
	let process p2 = pause
	val p2: unit process[* + 'r2]
	let l = [p1; p2]
	val l: unit process[0 + * + 'r] list
	RR n°8549

http://www.reactiveml.org RR n°8549

The vocabulary is the one of synchronous languages, not the one of FRP.RR n°8549

Precedence of operators is the following (from highest to lowest): run, ;, +, || and finally µ. For instance: µφ. κ 1 || run κ 2 + •; κ 3 means µφ. (κ 1 || ((run κ 2 ) + (•; κ 3 ))).RR n°8549

RR n°8549

τ ≤ Γ(x) Γ ⊢ x : τ | 0 τ ≤ Γ 0 (c) Γ ⊢ c : τ | 0 Γ ⊢ e 1 : τ 1 | ≡ 0 Γ ⊢ e 2 : τ 2 | ≡ 0 Γ ⊢ (e 1 , e 2 ) : τ 1 × τ 2 | 0 Γ, x : τ 1 ⊢ e : τ 2 | ≡ 0 Γ ⊢ λx.e : τ 1 → τ 2 | 0 (App) Γ ⊢ e 1 : τ 2 → τ 1 | ≡ 0 Γ ⊢ e 2 : τ 2 | ≡ 0 Γ ⊢ e 1 e 2 : τ 1 | 0 Γ, x : τ ⊢ v : τ | ≡ 0 Γ ⊢ rec x = v : τ | 0 (Process) Γ ⊢ e : τ | κ Γ ⊢ process e : τ process[κ + κ ′ ] | 0 Γ ⊢ e : τ process[κ] | ≡ 0 Γ ⊢ run e : τ | run κ Γ ⊢ pause : unit | • Γ ⊢ e 1 : τ 1 | κ 1 Γ ⊢ e 2 : τ 2 | κ 2 Γ, x 1 : gen(τ 1 , e 1 , Γ), x 2 : gen(τ 2 , e 2 , Γ) ⊢ e 3 : τ | κ 3 Γ ⊢ let x 1 = e 1 and x 2 = e 2 in e 3 : τ | (κ 1 || κ 2 ); κ 3 Γ ⊢ e 1 : τ 2 | ≡ 0 Γ ⊢ e 2 : τ 1 → τ 2 → τ 2 | ≡ 0 Γ, x : (τ 1 , τ 2 ) event ⊢ e : τ | κ Γ ⊢ signal x default e 1 gather e 2 in e : τ | 0; κ Γ ⊢ e : (τ 1 , τ 2 ) event | ≡ 0 Γ ⊢ e 1 : τ | κ 1 Γ ⊢ e 2 : τ | κ 2 Γ ⊢ present e then e 1 else e 2 : τ | κ 1 + (•; κ 2 ) Γ ⊢ e 1 : (τ 1 , τ 2 ) event | ≡ 0 Γ ⊢ e 2 : τ 1 | ≡ 0 Γ ⊢ emit e 1 e 2 : unit | 0 Γ ⊢ e : τ | κ Γ ⊢ loop e : unit | (0; κ) ∞ Γ ⊢ e 1 : τ | κ 1 Γ ⊢ e : (τ 1 , τ 2 ) event | ≡ 0 Γ, x : τ 2 ⊢ e 2 : τ | κ 2 Γ ⊢ do e 1 until e(x) → e 2 : τ | κ 1 + (•; κ 2 ) Γ ⊢ e 1 : τ | κ Γ ⊢ e : (τ 1 , τ 2 ) event | ≡ 0 Γ ⊢ do e 1 when e : τ | κ + • ∞ (Mask) Γ ⊢ e : τ | κ φ ∈ f bv(Γ, τ ) Γ ⊢ e : τ | κ[φ ← •]Figure 1: Type-and-effect rules • In the case of present e then e 1 else e 2 , the first branch e 1 is executed immediatelyif the signal e is present and the second branch e 2 is executed at the next instant if it is absent. This is reflected in the behavior associated with the expression. Similarly, for do e 1 until e(x) → e 2 , the expression e 2 is executed at the instant following the presence of e.• The encoding of primitives given earlier yields the expected behaviors. For example, consider the case of e 1 ; e 2 :Γ ⊢ e 1 :τ 1 | κ 1 Γ ⊢ () : unit | 0 Γ ⊢ e 2 : τ 2 | κ 2 Γ ⊢ let =e 1 and = () in e 2 : τ 2 | (κ 1 || 0); κ 2 Γ ⊢ e 1 ; e 2 : τ 2 | (κ 1 || 0); κ 2It is easy to show that (κ 1 || 0); κ 2 ≡ κ 1 ; κ 2 . We can also show that e 1 || e 2 has a behavior RR n°8549

Some behaviors are simplified using the extension described in Appendix D.RR n°8549

Discussion6.1 The run operatorSo far, we have not justified the presence of the run operator in the language of behaviors. It is there to ensure that, even after adding simplification to the type system, the behavior associated with a recursive process is always a recursive behavior, that is, µφ. κ with φ ∈ fbv (κ).Suppose that we remove the run operator from the language of behaviors. Now, consider the process rec p = process (run p). In the type system without run, we could give it the instantaneous behavior 0 and miss the instantaneous recursion:Equiv Γ ′ ⊢ S p : β process[0 + •] | 0 Γ ′ ⊢ S run p : β | 0 + • 0 + • ≡ 0 Γ ′ ⊢ S run p : β | 0 Γ ′ ⊢ S process (run p) : β process[0 + •] | 0 Γ ⊢ S rec p = process (run p) : β process[0] | 0 RR n°8549

http://x10-lang.org/ RR n°8549

RR n°8549RESEARCH 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

Acknowledgments

This work would not have been possible without previous experiments made with Florence Plateau and Marc Pouzet. Timothy Bourke helped us a lot in the preparation of this article. We are grateful for the proofreading and discussions with Guillaume Baudart and Adrien Guatto. Finally, we also thank the reviewers for there numerous comments and suggestions.

The typing rule is:

There are then two cases depending on the status of n:

-If n ∈ S: We notice that fst(κ 1 +(•; κ 2 )) = fst(κ 1 )+0 so we can apply the induction hypothesis on the first-instant behavior of e 1 and conclude.

-If n ∈ S: The derivation is finite.

• Case do e 1 when e 2 : We can use the same reasoning. It is interesting to note that the behavior associated with the expression, i.e. κ + • ∞ , is not equal to the behavior of the body, as one might expect, so that we can apply the induction hypothesis.

• Case let x 1 = e 1 and x 2 = e 2 in e: When we compute the first instant of a sequence, there are two possible cases:

-

From (κ 1 || κ 2 ) ↓, we get that either κ 1 ↓ which implies that b 1 = ff , or κ 2 ↓ which implies that b 2 = ff using Lemma 4. So we are sure that b 1 ∧ b 2 = ff . We can then apply the induction hypothesis on e 1 and e 2 using the rule Let-Par.

-Otherwise, we have that

We can apply the induction hypothesis on e 1 , e 2 and e 3 using either Let-par or Let-Done depending on the values of b 1 and b 2 .

• Case loop e: We have that fst((0; κ)) = 0; fst(κ), so we can apply the induction hypothesis on e. As the behavior (0; κ) ∞ is reactive, we know that κ ↓. By applying Lemma 4, we get that b = ff , so we reconstruct the complete derivation for e using the Loop-Stuck rule.

D Simplifying behaviors

The behaviors computed by the type system of Section 4 are very big. For instance, the behavior associated with the timer example is ((0 || 0); (0 + (0; 0))) ∞ . This behavior is unnecessarily detailed and as big as the source program. It is, however, equivalent to 0 ∞ . We would like to use the equivalence relation on behaviors (defined in Section 3.3) in our type system to reduce the size of the computed behaviors. This can be expressed as a new typing rule, that allows to simplify behaviors at any time using the equivalence relation. We denote ⊢ S the type system augmented with the new rule:

RR n°8549

In order to use this rule, we have to show that it is admissible, that is, that it does not change the set of accepted programs. This is ensured by the fact that the equivalence relation preserves reactivity (Property 1), which is one of the conditions requested by the soundness proof. Hence, an expression of type τ and of behavior κ has also type τ ′ and behavior κ ′ if τ ′ is equivalent to τ and κ ′ to κ ′ . The immediate consequence of this property is that the augmented type system is also sound. We can also simplify some rules by combining the original rule with the Equiv rule: