Frédéric Boussinot
email: frederic.boussinot@sophia.inria.fr

Frederic Dabrowski
email: frederic.dabrowski@irisa.fr

Frederic Dabrowski

Formalisation

Frédéric Dabrowski

Formalisation of FunLoft

Introduction

FunLoft is an experimental programming language mainly concerned with three topics: concurrency, resource control, and safety. Concurrency basically means the use of threads. Resources that are intended to be controlled are the memory and the CPU. Safety basically means absence of problematic concurrent accesses to shared data, called data-races. The objective of FunLoft is however larger than to combine concurrency, resource control, and safety: first, the language proposes a particular form of concurrency, intended to improve standard concurrency frameworks based on preemptive threads (Java threads or Pthreads [START_REF] Nichols | Pthreads Programming[END_REF]).

Second, FunLoft allows users to benefit from real parallelism (in particular, the one offered by multi-core machines) even in the case of the programming of an unique application. Third, efficiency is an important concern, that was present all along the language design.

The FunLoft language [START_REF]FunLoft[END_REF] is based on the FairThread model [START_REF] Boussinot | FairThreads: Mixing Cooperative and Preemptive Threads in C[END_REF] for concurrency aspects, on the PACT language [START_REF] Dabrowski | Programmation réactive synchrone -Langage et contrôle des ressources[END_REF] for safety concerns, and on the Synchronous π-calculus model [START_REF] Amadio | A Synchronous pi-Calculus[END_REF] for resource control aspects.

Overview of FunLoft

A program in FunLoft is a list of definition of variables, types, functions, and module, in a syntax inspirated from ML. In order to be executed, a program must contain the definition of a module named main which is the program entrypoint. A variable is a name to which a value is associated. Amongst the values are the standard ones (booleans and integers, for example), the values created from type definitions, and the threads, the events, and the schedulers.Type definitions introduce structured data built from union and concatenation of others types. Types can be recursively defined, to define data with variable sizes (lists, for example). Functions are first-order only: they cannot take functions as parameters, nor return functions; moreover it is not possible to define local or anonymous functions. Functions can be recursively defined; however, recursion is checked for termination, in a sense explained below, and thus function calls always terminate.

Modules Modules are templates from which threads, called instances, are created. A module can have parameters which define corresponding parameters of its instances. Arguments provided when an instance is created are associated to these parameters. A module can also have local variables, new fresh instances of which are automatically created for each thread created from it. As opposite to functions, modules cannot be recursively defined. The body of a module is basically a sequence of instructions executed by its instances. There are two types of instructions: atomic instructions and non-atomic ones. Atomic instructions are logically run in one single step. Function calls belong to this kind of instructions. Execution of non-atomic instructions may need several steps up to completion. This is typically the case of the instruction which waits for an event to be generated (see below). Execution steps of non-atomic instructions are interleaved, and can thus interfere during execution.

Schedulers A scheduler defines a portion of the memory sharable by the threads linked to it. A special scheduler (the implicit scheduler) is automatically launched by each executable program and a thread created from the main module is run in it. The basic task of a scheduler is to control execution of the threads linked to it. The scheduling is cooperative: linked threads have to return the control to the scheduler to which they are linked, in order to let other threads execute. Leaving the control can be either explicit, with the instruction cooperate, or implicit, by waiting for an event which is not present. All linked threads are cyclically considered in turn by the scheduler until all of them have reached a cooperation point (cooperate, or waiting instructions). Then, and only then, a new cycle can start. Cycles are called instants. A scheduler thus define an automatic synchronization mechanism which forces the threads linked to it to run at the same pace: all the threads must have finished their execution for the current instant, before the next instant can start. Note that the same thread can receive the control from the scheduler several times during the same instant; this is for example the case when the thread waits for an event which is generated by another thread later in the same instant. In this case, the thread receives the control a first time and then blocks, waiting for the event. The control goes to the others threads, and returns back to the first thread after the generation of the event. At creation, each thread is linked to one scheduler (by default, the implicit scheduler). Several schedulers can be defined and simultaneously running in the same program. Schedulers thus define synchronized areas in which threads execute in cooperation. Basically, schedulers run autonomously, in a preemptive way under the supervision of the OS (of course, this has a meaning only in the context of a preemptive OS). During their execution, threads can unlink from the scheduler to which they are currently linked, and become free from any scheduler synchronization. Such free unlinked threads are, like schedulers, run by kernel threads under supervision of the OS. There is a way to define synchronised schedulers that share the same instants.

Communication and Synchronisation

The simpler way for threads to communicate is of course to use shared variables. For example, a thread can set a boolean variable to indicate that a condition is set, and the other threads can test the variable to know the status of the condition. This basic pattern works well when all threads accessing the variable are linked to the same scheduler. Indeed, in this case atomicity of the accesses to the variable is guaranteed by the cooperativeness of the scheduler. A general way to protect a data from concurrent accesses is thus to associate it with a scheduler to which threads willing to access the data should first link to. Events are synchronizing data basically used by threads to avoid busy-waiting on conditions. An event is always associated to a scheduler (by default, the implicit scheduler) which is in charge of it during all its lifetime. An event is either present or absent during each instant of the scheduler which manages it. It is present if it is generated by the scheduler at the beginning of the instant, or if it is generated by one of the thread executed by the scheduler during the instant; it is absent otherwise. The presence or the absence of an event can change from an instant to another, but all threads always "see" presence or absence of events in the same way, independently on the order in which the threads are scheduled. This is what is meant by saying that events are broadcast. Values can be associated to event generations; they are collected during each instant and their collection as a list becomes available at the next instant.

Events are shared by synchronised schedulers, which is possible because syn-chronised schedulers themselves share instants. All works as if declaring an event in one of the synchronised scheduler automatically declares a corresponding event in the other synchronised schedulers. Moreover, each generation of one of these event is also automatically transmitted to all the associated events.

Memory Model

The memory is divided in several parts:

• A private memory for each thread. This memory is initialised when the thread is created, form the parameters and the local variables of the module from which the thread is created. The system checks that no other thread can have access to this private memory.

• A private memory for each scheduler. This memory can only be accessed by the thread linked to the scheduler. The system checks that it is inaccessible from unlinked threads, or from threads linked to another scheduler.

Thus, there exist no global variable shared by distinct schedulers, and a variable that is shared by distinct threads belongs to a unique scheduler and can only be accessed by the threads linked to the scheduler. This is the way data-races are absent from FunLoft.

Overview of Static Analysis

Several properties are statically checked in FunLoft:

• Functions always terminate (despite the fact that they can be recursively defined).

• Linked threads always cooperate(despite that they are allowed to never terminate).

• The memory model described above is actually respected.

• The number of simultaneously living threads always stays under control (despite the fact that threads can be dynamically created).

• No reference is allowed to increase in an uncontrolled way.

One thus gets a concurrent language in which programs are proved to be free from data-races and memory leaks.

For linked threads, the model guarantees the logical atomicity of the sequence of two instructions. If a thread contains the sequence A;B then no other thread can logically insert itself between A and B, even if this is physically possible.

To end the overview of FunLoft, we introduce its syntax by means of examples of programs that are statically accepted or rejected.

Instantaneous Loops Here is the definition of a correct module m which at each instant prints a message given as argument and cooperates: let module m (msg) = while true do begin print_string (msg); cooperate end

On the contrary, the following module is incorrect as it does not cooperate:

let module m (msg) = while true do print_string (msg)

Linking a thread instance of it to a scheduler would prevent from execution all other threads linked to the scheduler. This module is said to have an instantaneous loop. This point will be discussed in section 4.

Data Races

The following program is correct: atomicity of the assignment is guaranteed because the two threads created are executed cooperatively. A data-race (on r) is thus impossible: Indeed, the two threads are mapped on two native treads which are under the control of the OS. Thus, one has no guarantee of atomic access to r, which introduces a possibility of data-race.

A loss of atomicity also appears in the following program, where r is accessed by two threads linked to two distinct schedulers (s and the implicit scheduler): Transmission of private reference In the following example, the reference r created in m is necessarilly private, because it is read while unlinked. Thus, it should not be accessible from the public reference g. But this access is made possible by the assignement g:=r, and the program is thus incorrect:

let g = ref ref 0 let module m () = let r = ref 0 in begin unlink !r; g:=r; end
Note that, if this program were accepted, it would be very easy to define a context that would produce a data-race.

Number of threads

Situations were the number of threads to be executed (the living threads) is always increasing should be forbidden. This is for example the case with the following program:

while true do begin thread m (); cooperate; end Indeed, suppose m never terminates, then the number of living threads would be incremented at each instant, which would eventually leads to a memory overflow. The program should thus be rejected.

Note however that the program becomes acceptable if synchronous thread creation (run primitive) replaces asynchronous creation:

while true do begin run m (); cooperate; end Assuming that the number of threads which can be created by m is bounded by n, one is sure that the loop will never create more than n simultaneously living threads.

Size of data

To control the size of references basically means to forbid the use of references as accumulators. Typical example of accumulator is: The content of the reference r is a list whose length becomes more and more larger. Execution of this program will eventually lead to a memory overflow.

Note that the accumulation phenomenon may involve several references, as in:

let r1 = ref Nil let r2 = ref Nil let module m (r1,r2) =
while true do begin r1 := Cons (0,!r2); cooperate; end let module main () = begin thread m (r1,r2); thread m (r2,r1); end

Structure of the Report

One first considers in section 2 a basic formalism, without data, covering thread creation, execution, joining, and migration. Scheduler synchronisation is also treated in this basic fragment. One gives an operational semantics for the basic formalism. Data and references are introduced ins section 3. Data and functions to manipulate them are considered at an abstract level, without polymorphism. The issue of instantaneous loops is considered in section 4. A type system to eliminate data-races is given in section 5. Section 6 describes a variant of the operational semantics in which violations of the memory model appear explicitely. A well-typed program never leads to such violations. Inference of reference status is considered in section 7. A program for which one can infer a coherent information is proved well typed, thus free from data-races. Resource control is considered in section 8. This section contains two type systems: one for memory stratification, and the other to control the number of simultaneously living threads. Section 9 overview the issue of termination detection of functions. Events are introduced in section 10 which describes the changes induced in the operational semantics and the static analysis. Several features not yet formalised are considered in section 11. Finally, related work is described in section 12.

Basic Fragment

In a first step, one considers a basic fragment which only captures thread creation, schedulers synchronisation, and migration. The join primitive of FunLoft is considered under the restricted form of a run statement which creates a thread and waits for the termination of all the threads transitively created. The unlinking of a thread is seen as the migration to a new anonymous scheduler dedicated to its execution.

One considers an enumerable set of scheduler names, augmented with the special symbol for anonymous schedulers:

S name ::= { } ∪ {l 1 , l 2 , • • •}.
The syntax of the basic fragment is: • 0 is the terminated program.

Syntax P ::= 0 | A |
• µA.P is the recursive definition of P , with A as recursion variable.

• P 1 ; P 2 is the sequence of P 1 , followed by P 2 . The program P 2 starts when P 1 terminates.

• P @l is the migration to the scheduler l for running P . After P termination, the inverse migration takes place. P @ is the execution of P as unlinked.

• thread P creates a new thread running P and terminates instantly.

• runP creates a new thread running P and terminates when all the threads transitively created by P , or by threads created by it, are terminated.

• cooperate terminates execution for the current instant; execution restarts in sequence from the cooperate instruction at the next instant.

Threads A thread is a couple (t, P ) where t is a thread name. One notes the thread (t, P ) by P t .

Scheduler A scheduler is a triple: S ::=< L, L ′ > n where L is a list of active threads, L ′ is a list of threads to be considered at the next instant, and n is a scheduler name. Schedulers with name are called anonymous schedulers. Actually, there are two kinds of elements in L ′ :

• standard threads of the form P t ;

• guarded threads of the form t ↑ P t ′ meaning that termination of thread t and of all its descendants (threads transitively created by t) is required to continue execution of P t ′ .

If X is a list of threads, one notes x • X the list with head x and tail X.

One supposes that there exists an equivalence relation over schedulers: the relation of synchronisation. If S is a scheduler, the equivalence class of S (the maximal set of schedulers that are transitively synchronised with S) is noted S. From the language definition, anonymous schedulers cannot be synchronised with others schedulers (unlinked threads are autonomous).

Evaluation Context An evaluation context has form:

E ::= [ ] | E@n
< ∅, L ′ >n↓ T eoi < X, Y >n
where X is the list of threads obtained from elements of L ′ which are standard threads or are threads guarded by terminated nodes, and Y is the sublist of L ′ of elements guarded by non-terminated nodes:

• X is the list of threads extracted from elements of L ′ verifying the predicate:

Q(e) ≡ e = P t ∨ (e = t ↑ P t ′ ∧ over T (t))
• Y is the sub-list of elements of L ′ verifying the predicate:

R(e) ≡ e = t ↑ P t ′ ∧ ¬ over T (t)

Global Rules A thread executes in the scheduler to which it is linked:

P → P ′ E n C[< E[P ]t • L, L ′ >n], T → C[< E[P ′ ]t • L, L ′ >n], T
Synchronised schedulers all synchronise, in one unique step, at the end of each instant:

Si ↓ T eoi S ′ i Si ∈ c S1 = {S1, . . . , S k } C[S1] . . . [S k ], T → C[S ′ 1 ] . . . [S ′ k ], T
Migration to a specific scheduler extracts the thread from the source scheduler and places it into the target scheduler:

E l n = l C[< E[P ]t • L, L ′ >n][< L1, L2 > l ], T → C[< L, L ′ >n][< L1, L2 • E[P ]t > l ], T
The unlinking of a thread is seen as the migration to a new anonymous scheduler dedicated to its execution:

E C[< E[P ]t • L, L ′ > l ], T → C[< L, L ′ > l ][< E[P ]t, ∅ > ], T (1)
Local Rules In the recursive definition of P , the recursion variable is substituted by its definition:

µA.P → P [µA.P/A]
When the left part of a sequence is terminated, then the control goes to the right part: 0; P → P Thread Rules Terminated threads are eliminated from the scheduler to which they are linked:

C[< 0t • L, L ′ >n], T → C[< L, L ′ >n], T ′
where T ′ is T in which the state of t is set to terminated. An asynchronous thread creation puts the new created thread in the list of thread to be considered at next instant:

E l C[< E[thread P ]t • L, L ′ > l ], T → C[< E[0]t • L, L ′ • (P @l) t ′ > l ], T ′ (2)
where t ′ is a new node and

T ′ = T ∪ {t → t ′ }.
Synchronous thread creation is similar to asynchronous thread creation, except that the new created thread is guarded by termination of the initial thread:

E l C[< E[run P ]t • L, L ′ > l ], T → C[< L, L ′ • (P @l) t ′ • t ′ ↑ E[0]t > l ], T ′ (3)
where t ′ is a new node and

T ′ = T ∪ {t → t ′ }.
Cooperation Rule Cooperation terminates execution for the current instant and transfers the continuation in the list of threads to be executed at next instant:

E l C[< E[cooperate]t • L, L ′ > l ], T → C[< L, L ′ • E[0]t > l ], T (4)
Errors There are several situation where no rule apply to a given program. These situations are considered as errors:

• Migration to a scheduler which does not exist.

• Unlinking while already unlinked (rule 1; for example in: (P @ )@ ).

• Thread creation while unlinked (rules 2 and 3).

• Cooperation while unlinked (rule 4).

In the rest of the text, programs are supposed to be free from these errors (they are rejected either directly by the syntax, or by an elementary typing not considered here).

In a second step, one extends the previous basic fragment with data and references to hold them. Data are either basic data (e.g. booleans) or structured data belonging to inductive data types. An inductive data type is defined by a list of constructors. For example, the type intlist of lists of integers is defined by: type intlist = N il | Cons of int * intlist which introduces two constructors N il and Cons. A specific matching instruction is used to decompose data of inductive types, according to the way they have been built.

Functions are defined for data processing. Functions are first-order (no function as parameter; no function returned). One makes a strong assumption: function calls always terminate instantly, independently of the values of the actual parameters. An example of function is the one that returns the length of a list of integers.

One considers modules which are defined by definitions of the form A(x) = P , where the notation x is a short-hand for the (possibly empty) list x 1 , • • • , x n . Variables x are the module parameters which can appear in the module body P . Recursivity is forbidden in module definitions but a loop instruction is provided to define cyclic behaviours. • thread A(e), where A is defined by A(x) = P , creates a new thread running P with parameters x given values e, and terminates instantly. run A(e) is similar, but waits for termination of P and of all the threads transitively created by it.

Syntax

• The definition let x = e in P associates the value of e to the variable x in P .

• The assignment e 1 := e 2 assigns the value of e 2 to the reference denoted by e 1 .

• Instruction [e ⊲ p]P 1 , P 2 is an attempt to decompose the value denoted by e following the pattern p. If the decomposition is possible (one supposes, then, that it is unique), then P 1 is run in the environment resulting from the decomposition. Otherwise, P 2 is run.

• The loop while e do P executes P cyclically while the expression e is true.

A reference creation extends the heap with a new fresh location:

e, H ⇓ v, H ′ r ∈ Dom(H ′ ) ref e, H ⇓ r, H ′ ⊕ [r\v]
Evaluation of a location returns it:

r, H ⇓ r, H
Dereferencing a reference returns its content:

e, H ⇓ r, H ′ !e, H ⇓ H ′ (r), H ′
Global Rules There are no real changes for the global rules, except the introduction of the heap.

P, H → P ′ , H ′ E n C[< E[P ]t • L, L ′ >n], T , H → C[< E[P ′ ]t • L, L ′ >n], T , H ′ (5) Si ↓ T eoi S ′ i Si ∈ c S1 = {S1, . . . , S k } C[S1] . . . [S k ], T , H → C[S ′ 1 ] . . . [S ′ k ], T , H E l n = l C[< E[P ]t • L, L ′ >n][< L1, L2 > l ], T , H → C[< L, L ′ >n][< L1, L2 • E[P ]t > l ], T , H E C[< E[P ]t • L, L ′ > l ], T , H → C[< L, L ′ > l ][< E[P ]t, ∅ > ], T , H
Local Rules The heap is introduced in the rule for the sequence instruction:

0; P, H → P, H
The binding instruction is standard:

e, H ⇓ v, H ′ let x = e in P, H → P [x\v], H ′
An assignement changes the heap and rewrites in 0:

(e1, e2), H ⇓ (r, v), H ′ e1 := e2, H → 0, H ′ [r\v]
There are two cases for the matching instruction, depending on the possibility to match the value of the expression with the pattern (the matching is possible if there exists a substitution σ which applied to the pattern gives the value):

e, H ⇓ v, H ′ ∃σ.σ(p) = v [e ⊲ p]P1, P2, H → σ(P1), H ′ e, H ⇓ v, H ′ ∃σ.σ(p) = v [e ⊲ p]P1, P2, H → P2, H ′
A loop first evaluates the controlling expression and terminates when the returned value is false:

Thread Rules Thread rules are very similar to the ones of the basic fragment:

C[< 0t • L, L ′ >n], T , H → C[< L, L ′ >n], T ′ , H E l e, H ⇓ v, H ′ C[< E[thread A(e)]t • L, L ′ > l ], T , H → C[< E[0]t • L, L ′ • (P [x\v]@l) t ′ > l ], T ′ , H ′ (7) E l e, H ⇓ v, H ′ C[< E[run A(e)]t • L, L ′ > l ], T , H → C[< L, L ′ • (P [x\v]@l) t ′ • t ′ ↑ E[0]t > l ], T ′ , H ′ (8)
Cooperation Rule The cooperation rule is the same, except introduction of the heap:

E l C[< E[cooperate]t • L, L ′ > l ], T , H → C[< L, L ′ • E[0]t > l ], T , H
Errors Two new possibilities of errors appear:

1. Incomplete match instructions (there are uncovered cases), or match instructions with not disjoint cases.

2. Loop instructions in which the body does not converge; then, no rewriting exists. This kind of error is called "instantaneous loop" in synchronous languages, such as Esterel [START_REF] Berry | The Esterel Synchronous Programming Language: Design, Semantics, Implementation[END_REF]. Elimination of instantaneous loops is considered in section 4.

In the following, programs are supposed to be free from the first kind of errors, according to a syntax analysis which, for simplicity, is not described here.

Instantaneous Loops

One types programs by Pb, where b is a boolean indicating the possible instantaneous termination of P . One notes Ptrue if P can terminate instantly, and Pfalse when P never terminates instantly.

Always Instantly Terminating

0 -true e1 := e2 -true thread A(e) -true Never Instantly Terminating cooperate -false run A(e) -false Sequence P1 -b1 P2 -b2 P1; P2 -b1 ∧ b2 Match P1 -b 1 P2 -b 2 [e ⊲ p]P1, P2 -b1 ∨ b2

Variable and Migration

P -b let x = e in P -b P -b P @n -b
Loop The body of a loop should never terminate instantly. The whole loop however can terminate instantly (the controling expression could be false): Pfalse while e do Ptrue Proposition 1 Let P a program such that Pb. Then, for all H, there exist P ′ and H ′ such that P, H → P ′ , H ′ and b = false implies P ′ = 0.

As a consequence, if Pb then no instantaneous loop can appear during execution of P (application of the recursive rule 6 cannot cycle). Thus Pb means that P is free from instantaneous loops.

Type System for Atomicity

One now considers typing with the objective to detect data-races.

Data types are either the unit type (whose only value is noted "()"), type names (denoting basic types or inductively defined types) or reference types of the form τ ref n with n ∈ S name . Type τ ref is the type of private references; a private reference should only be accessed by the thread which has created it. Type τ ref l is the type of public references which are shared by all the threads linked to the scheduler l. Types are defined by: τ ::= () | t | τ ref n A typing environment Γ is a possibly empty list of elements of the form x : τ , where x is a type variable: Γ ::= x 1 : τ 1 , • • • , x n : τ n An effect F is a set of scheduler names; l ∈ F denotes an access to a reference belonging to scheduler l. The auxiliary function actual is defined by actual( ) = ∅, and actual(l) = {l}. Type judgments have the form Γ ⊢ P : F , for programs, and Γ ⊢ e : τ, F , for expressions.

One says that a type τ is public, noted public(τ ), if τ is not of the form τ ′ ref .

The type information associated with a function f is noted f : τ → τ ′ /F to indicate that the function has parameters of types τ , returns a value of type τ ′ , and produces effect F . For example, the type int ref l → int/{l} is a possible type for a function defined by let f (x) =!x. Note that polymorphism (parametric types) is not considered here.

The type information associated with a module A is noted A : τ → ()/F to indicate that the module has parameters of types τ and produces effect F (modules do not return values or, alternatively, they return "()").

Type System

Programs The termination instruction has no effect:

Γ ⊢ 0 : ∅
The effects of the control expression and of the body are collected in a loop:

Γ ⊢ P : F1 Γ ⊢ e : bool, F2 Γ ⊢ while e do P : F1 ∪ F2
The effects of the two components of a sequence are collected:

Γ ⊢ Pi : Fi Γ ⊢ P1; P2 : ∪Fi
No effect is allowed when unlinked. The only effect allowed when linked to an explicit scheduler is the access to references belonging to the scheduler:

Γ ⊢ P : F F ⊆ actual(n) Γ ⊢ P @n : ∅
In a thread creation, parameters should be public. The effect of the creation is the collection of the effects of the actual parameters:

A : τ → ()/F Γ ⊢ ei : τi, Fi public(τi) Γ ⊢ thread A(e) : ∪Fi
Synchronous and asynchronous thread creations are treated exactly in the same way:

Expressions Variables can have any type:

Γ ∪ x : τ ⊢ x : τ, ∅
Effects of parameters and effect of the function are collected in a function call:

f : τ → τ ′ /F Γ ⊢ ei : τi, Fi Γ ⊢ f (e) : τ ′ , F ∪ Fi
Constructors have no effect except those of their arguments:

C : τ → t/∅ Γ ⊢ ei : τi, Fi Γ ⊢ C(e) : t, ∪Fi
For a public reference, the type of its initial value should be public:

Γ ⊢ e : τ, F n = ⇒ public(τ ) Γ ⊢ refne : τ refn, F
Dereferencing a reference adds to the effect the scheduler associated with the reference:

Γ ⊢ e : τ refn, F Γ ⊢ !e : τ, F ∪ actual(n)

Private References

In a well-typed program, a thread cannot access the private references belonging to another thread. To prove this, one introduces the notion of a coherent heap and shows that coherency is preserved by reductions. Communicating a private reference to an other thread needs, at some state, the heap to be incoherent, which gives the result.

A heap H is coherent if no public reference points on a private one: H(r l ) = r ′ n implies n = . First, one proves the following proposition: Proposition 2 Heap coherency is preserved through evaluation.

Let e be a closed expression and suppose

H is coherent. If ⊢ e : τ, F and e, H ⇓ v, H ′ , then H ′ is coherent.
Expression e cannot be a variable or a reference as it would not be closed.

Consider reference creation. Suppose ⊢ ref n e : τ ref n , F and e, H ⇓ v, H ′ r ∈ Dom(H ′ ) refne, H ⇓ r, H ′ ⊕ [r\v]
One has ⊢ e : τ, F . By induction, H ′ is coherent. Let

H ′′ = H ′ ⊕ [r\v]
. Suppose H ′′ is not coherent. This means that n = and H ′′ (r n ) = v = r ′ . But, then τ = τ ′ ref which would contradict the fact that public(τ ). Thus, H ′′ is coherent.

The other cases (dereferencing, function call, and constructor call) are immediate.

Heap coherency is also preserved through reduction: if H is coherent, P, H → P ′ , H ′ , and ∅ ⊢ P : F , then H ′ is coherent (the proof is concerned only with assignment; the result comes from the preservation of the type of the left part).

Finally, heap consistency is preserved by system reductions (immediate, from previous cases).

As consequence of heap coherency preservation, a private reference of a thread cannot be shared. Indeed, for a thread to give access to a private reference to another thread means either to pass it as parameter (which is impossible because parameters have to be public), or to copy the private reference into a public reference, which leads to an incoherent heap.

Controlled Execution Semantics

One defines a variant of the execution semantics of section 3 in which accesses to references are controlled, in the sense that "wrong" accesses, leading to possibilities of data-races, produce errors (no rule apply).

Expressions An owner is associated to each reference value. There are two cases: either the owner is a scheduler name which means that the reference is public, that is, sharable by the threads linked to the scheduler; either the owner is a thread name which means that the reference is private to this thread, and thus can only be accessed by it. Expressions are defined by: Executing Thread and Current Scheduler Rules 5, 7, and 8 are those in which expressions are evaluated and programs are reduced in a given context. They have the shape:

C[< E[• • •] t , • • • > n ], T , H → C[• • •],
T ′ , H ′ Actually, t is the executing thread, and n is the current scheduler (possibly , when t is unlinked). Rules are, if needed, prefixed by ⊢ t l when there are used by these 3 rules.

Operational Semantics

Evaluation of Expressions Creation of a public reference in a scheduler l extends the heap with a new fresh location created in l. Creation is impossible if the current scheduler is different from l:

⊢ t l e, H ⇓ v, H ′ r l ∈ Dom(H ′ ) ref l e, H ⇓ r l , H ′ ⊕ [r l \v]
Creation of a private reference (with ) creates a reference the owner of which is the executing thread. Creation is possible independently of the fact that the thread is linked or unlinked:

⊢ t n e, H ⇓ v, H ′ rt ∈ Dom(H ′ ) ref e, H ⇓ rt, H ′ ⊕ [rt\v]
Evaluation of a direct reference returns it:

rn, H ⇓ rn, H Dereferencing a reference is only possible if it is performed in the correct context: if the reference is private, the thread must be the owner of the reference:

⊢ t n e, H ⇓ rt, H ′ !e, H ⇓ H ′ (rt), H ′
Deferencing a private reference is impossible by a thread not owning it. Dereferencing does not depend of the state linked or unlinked of the thread. If the reference is public, then it should belong to the current scheduler:

⊢ t l e, H ⇓ r l , H ′ !e, H ⇓ H ′ (r l ), H ′
Local Rules The rules for assignment are very similar to the rules for deferenciation:

⊢ t l (e1, e2), H ⇓ (r l , v), H ′ e1 := e2, H → 0, H ′ [r l \v] ⊢ t n (e1, e2), H ⇓ (rt, v), H ′ e1 := e2, H → 0, H ′ [rt\v]
Errors Actually, an execution error is encountered (no rule apply) in two cases:

• a private reference is accessed (dereferenced or assigned) by a thread distinct from the owner of the reference;

• a public reference is accessed by a thread unlinked or not linked to the scheduler to which the reference belongs.

The correction property can now be stated:

Proposition 3 If a program P is well-typed then there is no execution error for P in the controlled semantics.

Absence of Data-races

In a well-typed program, data-races cannot occur. First, a thread linked to a scheduler cannot access a reference belonging to another scheduler. Second, an unlinked thread can only access its private memory. These properties basically result from the typing rule:

Γ ⊢ P : F F ⊆ actual(n) Γ ⊢ P @n : ∅
If n = , then effect should be empty, thus only private references are accessible. By previous section, these private reference are those of the executing thread.

If n = l, then the only accessible references are the private ones or the public references belonging to scheduler l. As previously, private references accessed belong to the executing thread. Thus, when a thread is unlinked, it can only have access to its private references, and when a thread is linked to a scheduler it can only have access to the its private reference and to the public references of the scheduler. In all cases, no data-race can occur.

Inference System

In this section, we present an inference system to infer the status (private or public, that is belonging to a scheduler) of references.

One defines scheduler variables α, β, • • • and labels each reference creation with a scheduler variable; thus, reference creations get the form: ref α e. All the introduced labels are supposed to be distinct.

One assumes that functions have been correctly typed in a first phase. Types have the shape f : ∀α.τ → τ ′ /F where α are the scheduler variables appearing in τ . For example the type ∀α.int ref α → int/{α} is a possible type for let f (x) = !x. Note that, here, we consider polymorphism only at the level of scheduler variables, not at the data-type level. For example, the previous function f could as well be given type ∀α.bool ref α → bool/{α}.

Inference for programs has the form Γ |= P : F, C with C a set of constraints of the form (x = y), (x = y), or (x ≤ y), where x and y are scheduler variables or scheduler names (the set S name ). Inference for expressions has the form Γ |= e : τ, F, C, where τ is the type of expression e.

The inference process produces a set C of constraints that must be consistent: there should exist a function σ extending the identity on S name and associating with each scheduler variable an element of S name such that:

• (x = y) ∈ C ⇒ σ(x) = σ(y) • (x = y) ∈ C ⇒ σ(x) = σ(y) • (x ≤ y) ∈ C ⇒ σ(x) = ∨ σ(x) = σ(y) Γ |= e : τ, F, C Γ |= refαe : τ ref β , F, C ∪ {(α = β)} ∪ P ropagate(β, τ ) Γ |= e : τ refα, F, C Γ |= !e : τ, F ∪ {α}, C

Coherency

Coherence of type inference can be stated as:

Proposition 4 Suppose that Γ |= P : F, C. If C is consistent, then σ(Γ) ⊢ σ(P ) : σ(F ), for all σ unifier of C.
Proof by induction on the structure of P .

Nothing One has Γ |= 0 : ∅, ∅. As Γ ⊢ 0 : ∅, then for all σ, one has σ(Γ) ⊢ σ(0) : σ(∅). The same arguments hold for cooperate.

Sequence Let us suppose:

Γ |= Pi : Fi, Ci Γ |= P1; P2 : ∪Fi, ∪Ci
with ∪C i coherent and σ a unifier of ∪C i . By induction, as each C i is coherent and as σ is a unifier of each C i , one has σ(Γ) ⊢ σ(P i ) : σ(F i ). This implies σ(Γ) ⊢ σ(P 1 ; P 2 ) : σ(F 1 ∪F 2 ) because σ(P 1 ; P 2 ) = σ(P 1 ); σ(P 2 ) and σ(F

1 ∪F 2 ) = σ(F 1 ) ∪ σ(F 2 ).
Very similar arguments hold for while, match, and for function and constructor calls.

Let Let us suppose: Very similar arguments hold for assignment.

Migration Let us suppose:

Γ |= P : F, C Γ |= P @n : ∅, C ∪ {(α ≤ n) / α ∈ F } Let C ′ = C ∪ {(α ≤ n) / α ∈ F } and suppose C ′ coherent
and σ is a unifier of C ′ . By induction, one has σ(Γ) ⊢ σ(P ) : σ(F ) because C is coherent and σ is also a unifier of C. For all α ∈ F , one has σ(α) ≤ n, thus σ(F ) ⊆ { , n}, which implies the result σ(Γ) ⊢ σ(P @n) : σ(∅). Let us now consider the other case, where n = l. In addition, one must show that public(σ(τ )) which means that σ(τ ) is not of the form τ ′ ref . Let us suppose that this is not the case and that one has σ(τ

) = τ ′ ref . Then, P ropagate(β, τ ) implies σ(β) = which contradicts n = σ(α) = σ(β) = l.
Thus, one has public(σ(τ )) which entails the result.

Thread Creation Let us suppose:

A : τ → ()/F0 Γ |= ei : τi, Fi, Ci Γ |= thread A(e) : ∪Fi, ∪Ci ∪ N otP riv(τi)
Let C ′ = ∪C i ∪ N otP riv(τ i ) and suppose C ′ coherent and σ a unifier of C ′ . By induction, one has, for all i, σ(Γ) ⊢ σ(e i ) : σ(τ i ), σ(F i ).

Let us prove that public(σ(τ i )). If σ(τ i ) is not of the form τ ′ ref n then this is true by definition of public. So, suppose σ(τ i ) = τ ′ ref n . Then there exists α and τ ′′ such that σ(α) = n and τ i = τ ′′ ref α . As σ unifies N otP riv(τ i ), n = σ(α) = , and thus public(σ(τ i )). In both cases, one has σ(Γ) ⊢ thread A(σ(e)) : ∪σ(F i ).

The run instruction is treated in exactly the same way.

Minimality

One now considers the set U nif of unifiers of a set C of constraints infered from a program P . Each unifier σ ∈ U nif is a function that assigns in a consistent way a scheduler name, l or , to each scheduler variable α appearing in C. One orders elements of U nif by pointwise extension of the relation ≤ defined by:

n 1 ≤ n 2 if n 1 = or n 1 = n 2 .
Proposition 5 If U nif = ∅ then it has a minimal element.

C and the number of scheduler names appearing in P are finite, so U nif is also finite. One build the minimal element, by considering in turn the scheduler variables α 1 , . . . , α n appearing in C.

Step 0: Let result the function such that ∀α i .result(α i ) = , and let index = 0. Step 3: Return result as the minimal element of U nif .

Correction of the algorithm relies on the following:

Proposition 6 Consider σ ∈ U nif and suppose σ(α) = l for some α in C. Let σ ′ = σ[α\ ]. If σ ′ ∈ U nif , then ∀γ ∈ U nif.γ(α) = l.
Indeed, σ(α) = l comes from an application of the following rule (this is the only way to introduce explicit scheduler names of the form l in constraints):

Γ |= P ′ : F, C ′ Γ |= P ′ @l : ∅, C ′ ∪ ≤ l) / α ∈ F } with C = C ′ ∪ {(α ≤ l) / α ∈ F }.
By recurrence, let θ the minimal unifier of C ′ infered from P ′ . If θ(α) = , then θ is also the minimal unifier for C. If θ(α) = l ′ , then by recurrence all unifiers of C ′ , and hence all unifiers of C, assign to α the same value, which leads to l ′ = l.

Resource Control

The goal is now to control the size of the heap used by a program. There are actually two sub-goals: first, to control the size of the data stored in references; second, to control the number of references accessible by the program. Here, to control basically means to get a bound depending only on the size of the program input. To simplify, one considers that the program input is initially stored in the heap.

One assigns to each reference a level which is an integer (levels will always appear as superscripts). The syntax of expressions becomes:

e ::= x | r k | f (e) | C(e) | ref k e | !e
In the reference value r k , k is the level of r. A level is also associated to reference creations: all references created by evaluation of ref k e have level k. The rule for reference creation becomes:

e, H ⇓ v, H ′ r k ∈ Dom(H ′ ) ref k e, H ⇓ r k , H ′ ⊕ [r k \v]

Type System for Stratification

Type judgments now have the form Γ ⊢ P : R, W, G for programs, and the form Γ ⊢ e : τ, R, W, G for expression. In these forms, R is the set of levels of possibly read references, W is the set of levels of possibly written references, and G is the graph of reference accesses. In G, nodes are levels and an arc from r to w means

Γ ⊢ e : τ, R, W, G Γ ⊢ ref k e : τ ref k , R, W, G Γ ⊢ e : τ ref k , R, W, G Γ ⊢ !e : τ, R ∪ {k}, W, G
Stratification Let P a well-typed program such that ∅ ⊢ P : R, W, G. One says that P is stratified if G is acyclic. In this case, levels can be partitionned in strates.

For each value v of type τ one defines the size of v in the heap H, noted |v| H , by:

• If τ is a basic type (unit, int, bool,...), then |v| H = 1. • If τ = τ ′ ref, then |v| H = 1 + |H(v)| H . • If τ = t an inductive type and v = C(v 0 , . . . , v n ), then |v| H = 1 + |H(v 0 )| H + • • • + |H(v n )| H .
One notes max(H) the maximum of the sizes of all the data stored in H:

max(H) = max{|H(r)| H /r ∈ Dom(H)}.
The size of references created by a stratified program is bounded and the bound only depends on the size of the program input: Proposition 7 Let P a stratified program. Then, there exists a function f P such that, whenever P,

H → P 1 , H 1 → P 2 , H 2 → • • •, then max(H i ) < f P (max(H)) for all i.

Type System for Living Threads

One defines a type system to insure that the number of living threads remains bounded. Actually, one only needs to avoid asynchronous thread creation in loops. The system is very simple: The last rule rejects loops whose body can create an asynchronous thread.

Proposition 8 Let P be a stratified program such that P ⊲ b. Then, the number of living threads is bounded and the bound only depends on the size of the program input.

Bounded Memory

References are dynamically created when an expression of the form ref e is evaluated. Thus, the number of created references can be unbound, as for example in the following program where a reference is created at each instant: while true do begin ref 0; cooperate end However, the number of references accessible by a given thread remains finite and bound by a value which can be extracted from the syntax (the number of let instructions). For example, in the previous example, no reference is actually accessible by the executing thread (references can be immediately garbage collected, as soon as they are created).

Thus, in a stratified program, the number of living threads, the number of references accessible by each thread, and the size of each reference are all bound by a value depending on the program input. As a consequence, the total size of the heap (the sum of the sizes of all accessible references) is bound by a value depending on the program input, provided the program is stratified.

Proposition 9 Let P be a stratified program such that P ⊲ b. Then, the memory used by P is bounded and the bound only depends on the size of the program input.

Detection of Function Termination

FunLoft allows users to define functions. However, the termination of functions is tested and mandatory. Indeed, a linked thread calling a non-terminating function would get stuck executing it and it would prevent the other threads linked to the same scheduler to get the control. For that purpose, loops are forbidden and recursivity is controlled. More precisely, the syntax of function bodies is: The definition of the function length is correct; indeed, there is only one sequence of calls starting from the initial call length (x) and reaching the call length (t). As x matches I cons (h,t), t is a strict sub-term of x. Thus, no infinite sequence of calls of length can exists, as the size of the parameter decreases at each call.

F ::= x | r | f (
More precisely, one says that the size of a parameter p is smaller than the size of a parameter q if p is a sub-term of q. For lists of parameters, one extends "lexicographically" the notion of size. Finally, in a complete sequence of calls (starting and ending on the same function), one checks that at each step parameters are strictly decreasing. Thus, any function call is forced to terminate after a finite number of recursive calls.

In the present version of FunLoft, recursivity can only concern parameters of inductive types. The following definition, in which recursivity concerns a parameter of integer type, is thus rejected:

let fact (n) = if n = 0 then 1 else n*fact (n-1)
Note that detection of termination of functions is an independent issue which does not interfere with previous issues such as the control over the number of simultaneously living threads. This does not remain true when creation of threads by functions is allowed; for simplicity, we do not consider this feature here.

Detection of termination of functions, as presently done in FunLoft, is a topics that should certainly be improved in further versions of the language. For example, in a sequence of calls leading from a function definition to a call of the same function, one could accept that some calls keep the parameters unchanged, provided there exists at least one call that strictly decreases the parameters size.

Events

One now introduces events which are used both for thread synchronisation and for thread communication. Previous syntax for expressions and programs is extended by: e ::= • event declares a new fresh event. Events are denoted by s.

• pre s is the list of values generated with S during previous instant.

• generate e 1 , e 2 generates the event denoted by e 1 and adds the value denoted by e 2 to the list of current values of e 1 .

• await e blocks the control until the event denoted by e is generated.

• get all e 1 in e 2 blocks the control during the current instant and collects during it the values generated for the event denoted by e 1 . The list of collected values is assigned to the reference denoted by e 2 and become available at next instant.

Operational Semantics

An environment of events maps events to list of values. One considers couples of environments of events E c , E p , where E c (s) is the list of values generated for the event s during the current instant, and E p (s) stores the list of values that have been generated for s during the previous instant. One notes ∅ the environment undefined for each event, and N il list the empty list. One defines a predicate which tests in an environment the absence of value associated to a givent event. This predicate will be used to test if an event has already been generated during the current instant: present(s, E) ⇔ E(s) = N il list.

Event Creation An event creation extends the event environment with a new fresh location:

s ∈ Dom(E) event, H, Ec, Ep ⇓ s, H, Ec ⊕ [s\N il list], Ep
Evaluation of an event returns it:

s, H, Ec, Ep ⇓ s, H, Ec, Ep
The expression pre s returns the list of values generated with s during the previous instant (the empty list, if there was no generation at all).

pre s, H, Ec, Ep ⇓ Ep(s), H, Ec, Ep Event Generation The generation of an event adds the value generated to the list of current values:

(e1, e2), H, Ec, Ep ⇓ (s, v), H ′ , E ′ c , E ′ p generate e1, e2, H, Ec, Ep → 0, H ′ , E ′ c [s\Cons list(v, E ′ c (s))], E ′ p
Await Awaiting an event which is not present (not previously generated during the current instant) transfers the executing thread in the waiting list:

e, H, Ec, Ec ⇓ s, H ′ , E ′ c , E ′ c ¬present(s, E ′ c ) C[< E[await e]t • L, L ′ > l ], H, Ec, Ep → C[< L, L ′ • E[await s]t > l ], H ′ , E ′ c , Ep
Awaiting an already generated event has no effect:

e, H, Ec, Ep ⇓ s, H ′ , E ′ c , E ′ p present(s, E ′ c ) await e, H, Ec, Ep → 0, H ′ , E ′ c , E ′ p
It is possible to resume execution of a waiting thread if the awaited event is present. This rule is used to resume execution of threads waiting for an event which becomes generated.

present(s, Ec) C[< L, L ′ • E[await s]t • L ′′ > l ], T , H, Ec, Ep → C[< L • E[0]t, L ′ • L ′′ > l ], T , H, Ec, Ep
Get all values The way to get the values of an event generated during the previous instant is in FunLoft to use the get all values which is actually expressible through the pre operator:

(e1, e2), H, Ec, Ep ⇓ (s, r), H ′ , E ′ c , E ′ p C[< E[get all e1 in e2]t • L, L ′ > l ], T , H, Ec, Ep → C[< L, L ′ • E[r := pre s]t > l ], T , H ′ , E ′ c , E ′ p
Termination Relation One defines a predicate to test if there is no thread waiting for a present event. The ↓ E term predicate is defined by:

↓ E term S = false ⇔ S =< L, L ′ • E[await s] • L ′′ >n ∧ present(s, E)
The end of instant is now defined as the moment where no thread remains to be executed nor is bloqued on a present event. At the end of each instant, the current environment is saved in the previous environment, before being reset:

Si ↓ Ec term Si ↓ T eoi S ′ i Si ∈ c S1 = {S1, . . . , S k } C[S1] . . . [S k ], T , H, Ec, Ep → C[S ′ 1 ] . . . [S ′ k ], T , H, ∅, Ec

Stratification

Events should participate to stratification as well as references. For example, the following module should be rejected as it violates stratification: By accepting it, one would cyclically store in the reference r a list of lists with increasing size, which is clearly a memory leak.

Communication Between Schedulers

In FunLoft, an event is associated to one unique scheduler, or to an area of synchronised schedulers. The case of an unique scheduler will be considered as a special case of an area with only one element. There should be impossible to remotely generate events when schedulers are not synchronised: Indeed, the number of generations to be stored is not bounded (it actually depends on the relative speed of the two schedulers) which is a potential source of memory leak.

However, use of events becomes possible between synchronised schedulers because the schedulers share the same instants; the following program is thus correct: let s1 = scheduler and s2 = scheduler let e = event let module wait () = link s1 do await e let module gen () = link s2 do generate e

Choice of Primitives

The pre operator is powerful enough to express the get all values primitive of FunLoft. Indeed, the instruction get all values s in r is equivalent to the sequence begin cooperate; r:=pre s end.

However, there is a difference at implementation level: without an analyse to determine the absence of execution of pre, the list of values generated during an instant must be stored in order to be available at the next instant. This is not the case with the primitive get all values: the list of previously generated values needs to be constructed only when the primitive is executed.

Actually, FunLoft also proposes the primitive for all values with the syntax for all values s with x -> e interpreted as: for each value generated for event s during the current instant, evaluate the expression e, in which the variable x is bound to the generated value. Thus, the call-back e is immediately evaluated during the current instant for each generation, as soon as it occurs. Like with get all values, one has to wait for next instant for termination, in order to be sure that all generations have been processed, but now reactions to generations are immediate. Two points are to be noted:

• Implementation is made easier, as no list of generated values is built.

• Stratification forbids the implementation of get all values using the primitive for all values as the number of values generated during an instant for a given event is not statically known.

Complete Language

Several features of FunLoft are missing from the present formalisation:

• Possibility for functions to create new (asynchronous) threads and to generate events.

• Finite loops (repeat), and infinite loops (loop).

• Arrays of references.

• Instruction to force a thread to definitively terminate (also, to suspend/resume a thread).

• Embedding of references in inductive data type.

We are now considering these features in turn.

Threads Created by Function Asynchronous thread creations are FunLoft expressions. The type system of 8.2 should thus be extended to expressions, to trace asynchronous thread creation (actually, this is implemented as a supplementary effect added to the standard type system). For example, in the following code, the type information produced for function f indicates an effect of thread creation, which is used to reject the definition of the module m1: The number of threads created depends on the parameter of the function f. As the size of the parameter is bounded, the number of created threads is also bounded.

Events Generated by Function In FunLoft, event generations are considered as expressions. Events can therefore be generated by functions. This has two consequences:

• One has to define a new effect denoting event generation. This effect is associated to functions that generate events. It will be used for stratification checking (see 10.2).

• In for all values (see 10.4) one has to verify the absence of effect denoting an event generation in the call-back expression. Indeed, a cyclic evaluation could occur if the evaluation of a call-back would lead to the re-generation of the awaited event, as in for all values s with x do generate s.

Finite Loops FunLoft introduces finite loops under the form of repeat instructions. Finite loops can occur both in functions and in modules. They cannot introduce cyclic behaviours, and they terminate instantly, provided their body also terminate instantly. The operational semantics (for simplicity, events are not considered) is:

e, H ⇓ n, H ′ n ≤ 0 repeat e do P, H → 0, H ′ e, H ⇓ n, H ′ n ≥ 1 P, H → P ′ , H ′ repeat e do P, H → P ′ ; repeat n -1 do P, H ′

In repeat e do P, the expression e needs not to be static (computable at compile time).

The factorial function considered in section 9 can be coded using the repeat primitive:

let fact (n) = let res = ref 1 in let count = ref n in begin
repeat n do begin res:=!res*!i; i-end; !res end Note that stratification is not violated because the type of the values stored in the reference res is not inductive (it's int).

Infinite Loops Infinite loops never terminate. Actually, the infinite loop loop p is operationally equivalent to while true do p. By defining an infinite loop, the programmer tells the system that the loop never terminates, and this information can be used by the type system to detect instantaneous loops.

The typing of infinite loops in the system of section 4 is thus:

P -false loop P -false
Arrays Arrays of references are definable in FunLoft. The syntax is ref [n] v which creates an array of n references all intialised with v. The expression n needs not to be static. Elements of arrays are usually processed in turn with the aid of finite loops.

The element of index i in an array a is noted a[i]. Indexing is made modulo the array size; this forbids run-time out-of-bounds errors. Thus, in FunLoft, arrays are basically circular buffers.

Arrays are treated exactly as if they were single references for stratification and elimination of data-races. For example, the following code is rejected, despite the fact that no data-race actually occurs: let s1 = scheduler let s2 = scheduler let array = ref [START_REF]Reactive Programming[END_REF] 0 let module first () = link s1 do array[0]:=1 let module second () = link s2 do array [START_REF]FunLoft[END_REF]:=2

The type system is not able to detect the disjointness of the two parts of the array accessed by the two modules. Note that the program is also rejected if the two schedulers are synchronised.

Controlling Threads In FunLoft there is the possibility to kill a thread, by executing a stop instruction. A thread can be also suspended and resumed, with the suspend, resume instructions. These instructions have no effect on unlinked threads. To formalise these instructions does not present any difficulty and is left to the reader. which defines lists of integer references.

The type system for atomicity described in section 5 must be adapted to take in account the possibility to embedd references into types. Basically, one needs to change the definition of a public type: a user-defined type is public iff it does not embedd any private reference and if it is build only from public types.

Polymorphism FunLoft allows polymorphism both at data type level and at function level. Fo example, the following function defines the polymorphic identity: let id (x) = x. Type inference has to be performed in presence of polymorphism. For example, the function id receives type ∀α.α → α.

At data level, types can have parameters, as in:

type 'a list = Nil_list | Cons_list of 'a * list which defines the list of elements of the parametric type 'a.

As usual in presence of polymorphism (in OCaml [START_REF]The Objective Caml System[END_REF], for example), one has to control variable generalisation. More precisely, if the system assigns to a variable an incomplete parametric reference, array, or event type (i.e. a type in which parameters remains), then this variable should not be used in contexts where the parameter receives several distinct types. One says that such a variable is not generalisable. For example, consider:

type 'a cell_data = Undef | Cell of 'a let x = ref Undef let f (v) = let z = !x in match z with Cell (c) -> x := Cell (v) | default -> ()
The type of x is not complete (one does not know what is 'a) and x is thus not generalisable. The function f has an effect which is to assign to x a value given in parameter. The following function is erroneous as it first sets the parameter 'a of x to the boolean type, then to the integer type:

let g () = begin f (true); f (1); end
The problem is similar with events, and the following program is also rejected (e is not generalisable, but used in two distinct contexts): let e = event let f1 (x) = generate e with x let g () = begin f1 (true) f1 (1); end

Related Work

Synchronous Reactive Programming Considering concurrency, FunLoft finds its roots in reactive programming [START_REF]Reactive Programming[END_REF] which is itself issued from the activity developped around synchronous languages [START_REF] Benveniste | The Synchronous Approach to Reactive and Real-Time System[END_REF].

Synchronous languages, such as Esterel [START_REF] Berry | The Esterel Synchronous Programming Language: Design, Semantics, Implementation[END_REF] and Lustre [START_REF] Caspi | Lustre: A Declarative Language for Programming Synchronous Systems[END_REF], put the focus on the validation of programs by means of formal methods. They consider static systems in which dynamic creation of concurrent entities is not allowed. The synchronous language Lucid Synchrone [START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and Reference Manual[END_REF] is an exception because it allows recursive definitions.

Synchronous languages are generally build on top of a "base-language", in which are defined data and elementary processings on them. In Esterel, for example, the base-language is C, while in Lucid Synchrone this is Ocaml. Considering resource control, synchronous languages provide means (for example, the "clock-calculus" of Lustre) to assure that execution will run in bounded memory, provided actions performed in the base-language are proved to run in bounded memory. Thus, unlike FunLoft, no synchronous language gives complete (that is, including the base-language) ways to control resources.

The ReactiveML [START_REF] Mandel | ReactiveML, a Reactive Extension to ML[END_REF] library introduces reactive programming in Objective Caml. ReactiveML is as safe as ML. There is no equivalent of unlinked threads in ReactiveML. Moreover, all concurrent activities defined in ReactiveML share the same instants which makes the implementation on multi-processors architectures problematic.

Thread Based Frameworks The Gnu-Pth [START_REF] Engelschall | Portable Multithreading[END_REF] thread library designed for Unix platforms provides cooperative scheduling in the context of POSIX/ANSI-C. Blocking I/O primitives have been rewritten in order to work in a cooperative scheduling. This differs from our proposal which gives users the freedom to safely code some more elaborated behaviors by escaping the cooperating scheduling.

Moreover, Gnu-Pth, being totally cooperative, has difficulties to fully benefit from multi-cores.

The FairThreads model defines a framework to mix cooperative and preemptive threads in C [START_REF] Boussinot | FairThreads: Mixing Cooperative and Preemptive Threads in C[END_REF], Java [START_REF] Boussinot | Java Fair Threads[END_REF], or Scheme [START_REF] Serrano | Scheme Fair Threads[END_REF]. This approach is at the basis of our but it is not concerned nor by safety nor by ensuring that the preemptive level does not interfere with the cooperative one, thus suffering of the usual issues encoutered with preemptive threads.

Cyclone

The Cyclone [START_REF] Trevor | Cyclone: A Safe Dialect of C[END_REF] language proposes a safe variant of C by limiting the use of pointers. Technically, regions are used in order to control that a pointer is not used outside its definition scope. An extension of Cyclone to multithreading is proposed in [START_REF] Grossman | Type-safe Multithreading in Cyclone[END_REF]. The main difference with our approach is that only preemptive threads are considered, controlled by locks and with possibilities of deadlocks. However, no implementation seems to exist yet for the multithreaded extension of Cyclone.

Atomicity In [START_REF] Flanagan | Types for Safe Locking[END_REF], a static analyse close to a type and effect system is considered; it focuses on the issue of ensuring the atomicity of programs by means of locks in the framework of a language providing preemptive threads. Although our programming approach differs, the notion of singleton type introduced there seems promising to us as it might be a way to consider the dynamic creation of schedulers. In particular, we'll try to combine it with the notion of region local to a piece of code which is considered in type and effect system to ensure that some memory locations do not escape from their initial scopes. However, it is at the moment not clear to us that such a method would apply as well as the one we use for separating private areas here. Indeed, when using external function, the notion of scope associated to a piece of code might not be as expressive as the notion of scope associated with a thread that we are currently using.

More recently, the problem of atomicity has also been considered for Java methods in [START_REF] Flanagan | A Type and Effect System for Atomicity[END_REF].

A first version of the type system for atomicity described here for FunLoft has been presented in [START_REF] Dabrowski | Cooperative Threads and Preemptive Computations[END_REF].

Separation Logics Separation Logic [START_REF] Reynolds | Separation Logic: a Logic for Shared Mutable Data Structures[END_REF][START_REF] O'hearn | Resources, Concurrency, and Local Reasoning (Abstract)[END_REF] offers means to ensure the disjointness of several parts of the memory which might be safely accessed concurrently. It is not clear to us, however, how it could apply to FunLoft, which allows dynamic allocation of memory locations and dynamic creation of threads.

Synchronous-π-calculus Recently, has been proposed the Synchronous-πcalculus [START_REF] Amadio | A Synchronous pi-Calculus[END_REF] (Sπ-calculus) which considers reactive programming from a process calculus point of view. The Sπ-calculus is a synchronous π-calculus which is based on the SL model [START_REF] Boussinot | The SL Synchronous Language[END_REF]. The latter is a relaxation of the Esterel model where the reaction to the absence of a signal within an instant can only happen at the next instant. This is exactly the event model on which FunLoft stands.

The Sπ-calculus basically differs from FunLoft in that references are absent from it.

In [START_REF] Amadio | Feasible Reactivity for Synchronous Cooperative Threads[END_REF] is considered the way to control resources for a formalism which is very close to the Sπ-calculus. Actually, polynomial bounds are produced, which is much more realistic than unconstrained ones that are considered in FunLoft.

Conditions to get deterministic behaviours in the Synchronous-π-calculus are studied in [START_REF] Amadio | Determinacy in a Synchronous pi-Calculus[END_REF] which proposes a typing system that guarantees determinacy. The accent on determinism is also put in the SHIM formalism [START_REF] Tardieu | Scheduling-independent threads and exceptions in SHIM[END_REF].

PACT Partially Cooperative Threads (PACT) is a formalism very close to FunLoft, introduced in F. Dabrowski's thesis [START_REF] Dabrowski | Programmation réactive synchrone -Langage et contrôle des ressources[END_REF]. The type system for atomicity of section 5 is presented and fully proved for PACT. PACT does not makes the difference function/module, and thus allows to recursively define behaviours that do not immediately terminate. In the present version, PACT does not considers synchronised schedulers, nor the join primitive of FunLoft.

Conclusion

One has first considered the basic formalism, without data, covering thread creation, execution, joining, and migration. Scheduler synchronisation is also treated in this basic fragment. Technically, we have introduced a tree environment to reflect the living state of threads, and an end-of-instant relation to synchronise schedulers.

Then, data and references are introduced. Data and functions to manipulate them are considered at an abstract level, without polymorphism. A type system has been given together with a variant of the operational semantics. A region is associated to each reference. The result is the absence of data-races for welltyped programs of this fragment.

Then, we have considered type inference. The goal was to infer the previous regions. Polymorphism is only present at the region level, not at data-type level. The purpose is thus to infer the regions for programs supposed to be correct at the data-type level. When inference is possible, one can deduce that no data-race occur at execution. Finally, we have introduced events and show the changes induced in the operational semantics and in the type system.

The split in several fragments has had the advantage to isolate issues. For example, the issue of termination detection of functions is orthogonal to the one of avoiding data-races. Thus, termination detection can be postponed to the processing of functions. An other advantage is to avoid to immediately consider recursive definitions in their full generality; actually, recursive definitions are a real issue only for detection of function termination.

One has a strong result: correct FunLoft programs are proved free from data-races and from memory leaks. They are also safe in the sense that no error should occur at execution time (provided memory is sufficient). 1Two questions seem legitimate at that point:

1. Is the existence of bounds sufficient in practice?

2. What programs are ruled out, and what programs pass the filter of the static analysis?

Bounds In FunLoft, only is proved the existence of bounds for the memory used and for the CPU consumed. These bounds depend on the size of the program input. But the infered bounds may be unrealistic. Actually, one can for example get exponential bounds, like in:

type tree = L of int | T of tree * tree let module map_on_leaf (t) = match t with L (n) -> thread leaf_processing (n) | T (t1,t2) -> begin map_on_leaf (t1); map_on_leaf (t2); end end let module tree_processing () = let t = ref L (0) in while true do begin t:=get_tree (); run map_on_leaf (!t); end

In this example, the loop stays bloqued on the run instruction until all the threads created for processing the leaves of the tree t are terminated. At each cycle, the number of created threads depends on the number of leaves of t. As the size of t (the number of calls of constructors in it) is bounded, this number is also bounded, like is the number of active threads in the system. However, the bound exponentially depends on the size of t.

Using the repeat instruction can also lead to huge unrealistic bounds. For example, repeat n do thread m () could create N threads, where N is the larger storable integer! Thus, existence of bounds should be considered just as a first step in direction of a fully satisfactory resource control.

Expressivity Consider a program which stores a list of requests all along the passing of instants, and which starts to process the requests when a triggering event becomes present. The need to store an unbounded number of requests, even if each request is of bounded size, is clearly contradictory with the existence of a bound on the memory consumed. Such a program is thus not implementable in FunLoft (technically, it should be rejected because of stratification violation). Actually, only finite versions of the program are implementable, in which is defined a maximum of requests that can be stored (for example, in an array). Note however that this maximum can be totally unrealistic (it could be the maximal integer storable in memory; see previous paragraph). A standard solution is to define a static pool of threads, each of them cyclically processing requests. FunLoft does not force the programmer to use such a solution, and allows him to dynamically create threads, one for each request.

The code to implement cellular automata is described in [START_REF]FunLoft[END_REF] and the distribution of the software contains several examples, among them a prey/predator system in which new preys are cyclically injected as soon as old ones have all been killed.

More examples are to be tried with FunLoft to get a clearer response to the second question. Note however, that one is able in FunLoft to get use at language level of the several cores of a multi-core architecture.

  let r = ref 0 let module m (n) = r:=n let module main () = begin thread m (1); thread m (2); end On the contrary, the following program is incorrect because the reference r is accessed by a thread linked to the implicit scheduler, and also by an unlinked thread: let r = ref 0 let module m (n) = r:=n let module main () = begin unlink thread m (1); thread m (2); end

  The syntax of programs becomes: P ::= 0 | P ; P | P @n | thread A(e) | run A(e) | cooperate | let x = e in P | e := e | [e ⊲ p]P, P | while e do P Differences with previous syntax are:

  e ::= x | r o | f (e) | C(e) | ref n e | !e In reference r o , o is the owner of the reference.

Γ

  |= e : τ, F1, C1 Γ ∪ x : τ |= P : F2, C2 Γ |= let x = e in P : ∪Fi, ∪Ci with ∪C i coherent and σ a unifier of ∪C i . By induction, one has σ(Γ) ⊢ σ(e) : σ(τ ), σ(F 1 ) and σ(Γ ∪ x : τ ) ⊢ σ(P ) : σ(F 2 ). Then, one has σ(Γ) ∪ x : σ(τ ) ⊢ σ(P ) : σ(F 2 ), which implies the result σ(Γ) ⊢ let x = σ(e) in σ(P ) : σ(F 1 ∪ F 2 ). Dereferencing Let us suppose: Γ |= e : τ refα, F, C Γ |= !e : τ, F ∪ {α}, C with C coherent and σ a unifier of C. By induction, one has σ(Γ) ⊢ σ(e) : σ(τ ref α ), σ(F ). Let n = σ(α). One has σ(Γ) ⊢ σ(e) : σ(τ ) ref n , σ(F ). This implies σ(Γ) ⊢ !σ(e) : σ(τ ), σ(F )∪{n} and finally σ(Γ) ⊢ σ(!e) : σ(τ ), σ(F ∪{α}).

  Let C ′ = C ∪ {(α = β)} ∪ P ropagate(β, τ ) and suppose C ′ coherent and σ an unifier of C ′ . Let n = σ(α). By induction, one has σ(Γ) ⊢ σ(e) : σ(τ ), σ(F ) because C is coherent and σ is also a unifier of C. Let us suppose n = . Then, one has σ(Γ) ⊢ ref n σ(e) : σ(τ ) ref n , σ(F ), and thus σ(Γ) ⊢ σ(ref α e) : σ(τ ref β ), σ(F ) because, as C ′ is coherent, n = σ(β).

Step 1 :

 1 if index = n then goto Step 3. Otherwise, increment index := index + 1, then search for an element σ ∈ U nif such that σ(α index ) = l. If no such σ can be found, then goto Step 1. Else, consider σ ′ = σ[α index \ ]. If σ ′ ∈ U nif , then goto Step 1. Otherwise, change result by result := result[α index \l] and goto Step 1.

  0 ⊲ false e1 := e2 ⊲ false thread A(e) ⊲ true cooperate ⊲ false run A(e) ⊲ false P1 ⊲ b1 P2 ⊲ b2 P1; P2 ⊲ b1 ∨ b2 P1 ⊲ b 1 P2 ⊲ b 2 [e ⊲ p]P1, P2 ⊲ b1 ∨ b2 P ⊲ b let x = e in P ⊲ b P ⊲ b P @n ⊲ b P ⊲ false while e do P ⊲ false

  e) | C(e) | ref e | !e | F ; F | let x = e in F | e := e | [e ⊲ p]F, F An example of function definition is: length(x) = [x ⊲ Cons(h, t)]plus int(1, length(t)), 0 which in real syntax should be written: let length (x) = match x with Cons_list (h,t) -> 1+length (t) | default -> 0

  ... | event | s | pre s P ::= ... | generate e, e | await e | get all e in e

  let head (l) = match l with Nil_list -> Nil_list | Cons_list (a,m) -> a end let module m (e) = let r = ref Nil_list in loop begin generate e with Cons_list (0,head (!r)); get_all_values e in r; end

  Note that one gets a new relation between thread creation and data processing. For example, consider:let nat = Z | S of nat let f (n) =match n with S (m) -> begin thread m0 (); f (m); end | default -> ()

  µA.P | P ; P | P @n | thread P | run P | cooperate More precisely:

  Creation Tree One notes T the tree that records the created threads and their state (terminated or not); in this tree, an arc from t to t ′ means that t ′ has been created by t. Using T , one can determine if a thread is terminated or not, and if all threads created from it are terminated or not. This information is useful for the treatment of the run primitive. One notes over T (t) if t is a terminated node of the tree T and if all its decendants are also transitively terminated. Note that in the sequel, T is always growing: nodes are never removed from it. When t is a node of T and t ′ is a new name not appearing in T , one notes T ∪ {t → t ′ } the tree in which the node t ′ is added as a new son of t.

		| E; P
	The predicate E	n is true if n appears in E and is the left-most (most intern)
	scheduler name in it (for example, [ ]@n 1 @n 2	n 1 ).
	Global Context A global context has form: C ::= [ ] | (C|C) | S
	End of Instant Relation The ↓ T eoi relation is defined by:

  H ⇓ false, H ′ while e do P, H → 0, H ′ Otherwise, the loop rewrites in a sequence: e, H ⇓ true, H ′ P, H ′ → P ′ , H ′′ while e do P, H → P ′ ; while e do P, H ′′

e,

A : τ → ()/F Γ ⊢ ei : τi, Fi public(τi) Γ ⊢ run A(e) : ∪FiThe cooperation instruction has no effect:Γ ⊢ cooperate : ∅The body of a variable definition is analysed in a context in which the variable is defined; the effect combines the effect produced by the initial value of the variable with the effect of the body:Γ ⊢ e : τ, F1 Γ ∪ x : τ ⊢ P : F2 Γ ⊢ let x = e in P : F1 ∪ F2Assignment to a reference adds to the effect the scheduler associated with the reference:Γ ⊢ e1 : τ refn, F1 Γ ⊢ e2 : τ, F2 Γ ⊢ e1 := e2 : F1 ∪ F2 ∪ actual(n)Effects of the two alternatives of a matching statement are collected in the final effect: Γ ⊢ e : τ, F0 Γ ∪ p : τ ⊢ P1 : F1 Γ ⊢ P2 : F2 Γ ⊢ [e ⊲ p]P1, P2 : F0 ∪ F1 ∪ F2

Such a function σ is said to be a unifier of C. One defines two functions N otP riv and P ropagate by:• N otP riv(τ ref α ) = {(α = )}, and N otP riv(τ ) = ∅ otherwise.• P ropagate(α, τ ref β ) = {(α ≤ β)} and P ropagate(α, τ ) = ∅ otherwise.We now give the inference system.Programs Γ |= 0 : ∅, ∅ Γ |= Pi : Fi, Ci Γ |= P1; P2 : ∪Fi, ∪Ci Γ |= P : F, C Γ |= P @n : ∅, C ∪ {(α ≤ n) / α ∈ F } A : τ → ()/F Γ |= ei : τi, Fi, Ci Γ |= thread A(e) : F ∪ Fi, ∪Ci ∪ N otP riv(τi) A : τ → ()/F Γ |= ei : τi, Fi, Ci Γ |= run A(e) : F ∪ Fi, ∪Ci ∪ N otP riv(τi) Γ |= cooperate : ∅, ∅

Γ |= e : τ, F1, C1 Γ ∪ x : τ |= P : F2, C2 Γ |= let x = e in P : ∪Fi, ∪Ci Γ |= e1 : τ refα, F1, C1 Γ |= e2 : τ, F2, C2 Γ |= e1 := e2 : ∪Fi ∪ {α}, ∪Ci Γ |= e : τ, F0, C0 Γ ∪ p : τ |= P1 : F1, C1 Γ |= P2 : F2, C2 Γ |= [e ⊲ p]P1, P2 : ∪Fi, ∪Ci Γ |= e : bool, F1, C1 Γ |= P : F2, C2 Γ |= while e do P : ∪Fi, ∪Ci Expressions Γ ∪ x : τ |= x : τ, ∅, ∅ f : τ → τ ′ /F Γ |= ei : τi, Fi, Ci Γ |= f (e) : τ ′ , F ∪ Fi, ∪Ci C : τ → t/∅ Γ |= ei : τi, Fi, Ci Γ |= C(e) : t, ∪Fi, ∪Ci

that the content of a reference of level r is possibly transfered to a reference of level w.The notation Dep(A, B) denotes the graph whose set of nodes is A ∪ B and in which there is an arc from each element of B to each element of A.Programs Γ ⊢ 0 : ∅, ∅, ∅ Γ ⊢ P : R1, W1, G1 Γ ⊢ e : bool, R2, W2, G2,Γ ⊢ while e do P : ∪Ri, ∪Wi, ∪GiΓ ⊢ Pi : Ri, Wi, Gi Γ ⊢ P1; P2 : ∪Ri, ∪Wi, ∪Gi Γ ⊢ P : R, W, G Γ ⊢ P @n : R, W, G A : τ → ()/R, W Γ ⊢ ei : τi, Ri, Wi, Gi Γ ⊢ thread A(e) : R ∪ Ri, W ∪ Wi, ∪Gi ∪ Dep(W, ∪Ri) A : τ → ()/R, W Γ ⊢ ei : τi, Ri, Wi, Gi Γ ⊢ run A(e) : R ∪ Ri, W ∪ Wi, ∪Gi ∪ Dep(W, ∪Ri) Γ ⊢ cooperate : ∅, ∅, ∅Γ ⊢ e : τ, R1, W1, G1 Γ ∪ x : τ ⊢ P : R2, W2, G2 Γ ⊢ let x = e in P : ∪Ri, ∪Wi, ∪Gi ∪ Dep(W2, R1)

Γ ⊢ e1 : τ ref k , R1, W1, G1 Γ ⊢ e2 : τ, R2, W2, G2 Γ ⊢ e1 := e2 : ∪Ri, ∪Wi ∪ {k}, ∪Gi ∪ Dep({k}, R2) Γ ⊢ e : τ, R0, W0, G0 Γ ∪ p : τ ⊢ P1 : R1, W1, G1 Γ ⊢ P2 : R2, W2, G2 Γ ⊢ [e ⊲ p]P1, P2 : ∪Ri, ∪Wi, ∪Gi Expressions Γ ∪ x : τ ⊢ x : τ, ∅, ∅, ∅ f : τ → τ ′ /R, W Γ ⊢ ei : τi, Ri, Wi, Gi Γ ⊢ f (e) : τ ′ , R ∪ Ri, W ∪ Wi, ∪Gi ∪ Dep(W, ∪Ri) C : τ → t/∅, ∅ Γ ⊢ ei : τi, Ri, Wi, GiΓ ⊢ C(e) : t, ∪Ri, ∪Wi, ∪Gi

Safety in FunLoft is also related to the capture of divide-by-zero errors; we do not go in deeper details here.