Keywords: Programmation synchrones, répartition automatique, systèmes de type

Un système de types pour la répartition automatique de programmes flot de données synchrones d'ordre supérieur Résumé : Ce rapport traite de la conception de systèmes répartis au moyen de langages flot de données synchrones. La conception modulaire de tels systèmes comprend deux préoccupations différentes, la modularité fonctionnelle et la modularité d'architecture. Ces deux préoccupations pouvant s'avérer orthogonales, nous proposons une solution intégrée dans un langage de programmation, par son extension avec des primitives de répartition. Ces primitives permettent de programmer un système réparti entier avec un seul et même langage, ainsi que la description de l'architecture et l'expression de la localisation de certains flots ou calculs sur cette architecture. Une sémantique répartie est dans un premier temps proposée comme formalisation de l'exécution répartie de programmes synchrones. Ensuite, nous proposons un système de types à effets permettant d'inférer la localisation des calculs ou des flots non annotées du programme, ainsi que d'assurer à la compilation la consistance des annotations de répartition fournies par le programmeur. Finalement, une opération de projection dirigée par les types est définie. Cette opération permet d'obtenir automatiquement, à partir d'un seul programme synchrone annoté, un programme local destiné à être exécuté par chaque ressource de calcul déclarée dans l'architecture. Ce système de type, ainsi que l'opération de projection, ont été implémentées dans le compilateur du langage Lucid Synchrone.

Introduction

Synchronous programming languages [START_REF] Benveniste | The synchronous languages twelve years later[END_REF] are frequently used in the industry for the design of real-time embedded systems. Such languages define deterministic behaviors and lie on formal semantics, making them suitable for the design and implementation of safety critical systems. They are used, for example, in critical domains such as automotive, avionics, or nuclear industry.

Most of the systems designed with synchronous languages are centralized systems. The parallelism expressed in these languages is a functional one whose purpose is to ease the design process by providing ideal timing and concurrency constructs to the designers. A synchronous program is then compiled into a sequential program emulating the parallel execution of the functional parallel branches. This sequential program is executed on a single computing resource. However, most embedded systems are composed of several computing resources (named "locations"). There are many reasons such as performance, dedicated actuators or sensors drivers, or adaptivity of the locations to the tasks they are assigned to (e.g., pure computing tasks vs control tasks). We call this the execution, or physical parallelism. This paper addresses the problem of mapping the functional parallelism onto the physical one, in a modular way.

Programs of a distributed system can be designed separately; but it occurs that in complex and multifunctional embedded systems, functionalities are frequently independent of the hardware architecture, implying conflicts between architecture and functional modularity. Thus, one functionality can use several locations and one location can be involved in several functionalities. As a result, programming separately each location compromises the modularity and is error-prone. This situation occurs within several industrial areas, among which automotive embedded systems, and software-defined radio [START_REF] Mitola | The software radio architecture[END_REF].

Within this context, our motivation is to introduce distribution primitives in a synchronous dataflow language allowing the annotation of a synchronous program without altering its semantics. These annotations allow the programmer to state on which location some values are located or computed. We then use a type and effects system [START_REF] Talpin | Polymorphic type, region and effect inference[END_REF], named spacial type system hereafter, to infer modularly the localization of non-annotated values. Finally, a projection operation allows us to obtain automatically, from a complete typed program, the local program to be executed on each location.

Our paper is organized as follows: in Section 2, we expose the context and motivations of this work. The primitives added to our language will be presented in Section 2.2, the spacial type system in Section 2. [START_REF] André | Software implementation of synchronous programs[END_REF], some examples in Section 2.4, and an application in Section 2.5. Section 3 will then present the semantics, and the formalization of the spacial type system. Section 4 shows the type-based distribution method. Finally, related work and discussion about the solution will be exposed in Section 5.

Motivations and Overview

Distribution of Synchronous Programs

Dataflow languages, commonly used to describe block-diagram systems, express the manipulation of infinite streams of values as primitive values. Consequently, the notation 1 represents the infinite sequence 1, 1, ... (in the following, we will denote by x i the ith value of the stream x). In the same way, int stands for the type of infinite sequences of integers. In this context, functions (called nodes hereafter) are stream functions (e.g., int → int stands for the type of functions from integer streams to integer streams). Combinatorial functions are implicilty lifted to apply pointwise to their arguments (e.g., if x = (x i ) i∈IN and y = (y i ) i∈IN are two integer streams, (x + y) = (x i + y i ) i∈IN .

The classical compilation method involves compiling a synchronous program into one function f , which computes the values of outputs, and updates the system's state, from the values of inputs and the current state. This function f is then embedded inside a periodic execution loop [START_REF] André | Software implementation of synchronous programs[END_REF]. We will adapt this classical compilation scheme to a distributed framework: the result of the compilation of a distributed system will consist of n functions f i , one for each location i, which will compute the values of outputs, communication channels, and local state, from the values of inputs, other incoming communication channels, and the current local state.

Language-based Distribution

We consider functional distribution: distribution is not achieved for the sake of performance but because the system described is intrinsically distributed. The distribution is driven by the fact that some functions have a meaning only at some specific locations and not at others. We can think, e.g., of a function returning the value of a physical sensor and which has to be executed where the sensor is. Therefore, locations will be defined by the functionalities they provide.

Designing such distributed systems is non-trivial, since problems such as the scheduling of communications or the type consistency of the communicated data arise. The usual method, using architecture languages such as AADL [START_REF]Architecture analysis & design language[END_REF], involves INRIA describing the system's architecture by partitioning it in subsystems. Each subsystem can then be defined separately, possibly with different languages.

However, in the case of tightly dependent subsystems, where some conflicts between architectural and functional modularity can occur, it is more efficient and less error-prone to define the system as a whole, together with architectural annotations [START_REF] Girault | A survey of automatic distribution method for synchronous programs[END_REF]. Our contribution consequently involves providing language primitives, to allow the programmer to describe the hardware architecture, and to express where some values are located, i.e., on which location some computations are performed.

The architecture is described by the explicit declaration of the set of existing locations and the links between them. At this point, locations are symbolic: the declaration of a location introduces a symbolic name, which will then be used to express the fact that a stream is computed or available at this symbolic location. We define in Section 4.4 a projection operation, which operates w.r.t. a symbolic name, and which produces a single non-distributed synchronous program to be executed at the physical location represented by this symbolic name.

The declaration of a physical location A follows the syntax: loc A. The existence of a link from A to B is stated by: link A to B. Note that we distinguish communication links from communication channels, introduced in Section 3.4: communication links, specified by the primitive link, state the possibility of communications from one location to another. In contrast, actual channels used by the distributed system are inferred by the type system.

The statement e at A means that every value used in the expression e (streams and nodes) will be located at A. The programmer does not need to express the localization of every value. A type system is provided, whose double function is to check the validity of the localization expressed in regard to the architecture (w.r.t. existing communication links), and to infer the localization of non-explicitly located values.

For instance, the node f given below consists of two computations g and h, respectively located by the programmer on locations A and B, thanks to the at A and at B annotations. node f(x) = z with y = g(x) at A and z = h(y) at B; Communications are abstracted, and thus not expressed by the programmer, neither technically, nor concerning their localization inside the code. The technical expression of communications are let to the further phase of integration on actual RR n°6378 architecture: our method only deal with inferring localization of these communications, and their coherence throughout the distributed code. We assume for now that communications can occur at any localization, and can concern any value entirely concealed within a location (i.e., not the distributed data structures, like distributed pairs). Such choice concern a compromise, from a programmer point of view, between no control at all (communications are possible everywhere) and absolute control (the programmer expresses every communication). We will currently assume that communications can occur everywhere in the code, and show later how this can be refined.

A Type System for the Automatic Distribution

The main difficulty of synchronous dataflow programs distribution lies in the preservation of the control flow. Usually, such programs are inlined before distribution [START_REF] Caspi | Automatic distribution of reactive systems for asynchronous networks of processors[END_REF]: as a result, the control flow is materialized by classic control structures such as if/then/elses. We place ourselves in a functional framework, where for the sake of modularity, functions can neither be inlined nor analyzed dependently of their calling context. Hence, to preserve the coherence of the control flow on all the locations, we must place on each location, along with functions defined on it, the functions containing the calls to these functions, and so on. This also allows us to preserve higher-order features, hence allowing the expression of dynamic reconfiguration of nodes by application of other nodes as inputs.

Consequently, the complete control flow of the program cannot be built for analysing its consistency. Hence, type systems are provided so as to perform such an analysis. Besides the classical type system used for data consistency analysis, we provide a special type system dedicated to the distributed execution of the program. We call it a spacial type system and, when clear from context, we shall simply refer to it as a type system (since this paper does not address classical typing). This spacial type system describes the localization of streams, and a type-directed approach is followed to achieve code distribution.

The motivation for using a type system is to achieve type inference: in order not to force the programmer to specify everything (i.e., the localization of each stream), spacial types will be inferred from the available spacial annotations in the source. The spacial type system also checks the consistency of these annotations with the given architecture. Spacial consistency means, e.g., that applying a node located on a location to a stream located elsewhere is not correct. As we are in a functional context, spacial types will be inferred for each defined node modularly. The type system presented is a type and effects system [START_REF] Talpin | Polymorphic type, region and effect inference[END_REF].

INRIA

A typed program is then automatically distributed by the compiler, by extracting, for each declared location, one program strictly composed of computations to be performed on this location, as well as added communications from and to other locations in the form of added inputs and outputs.

The spacial type of a stream is the location where this stream is located. In the case of a stream whose values are communicated via a channel from one location to another, its spacial type is a set: it is the set of locations where the stream will be available. The spacial type of a node f is written t i -S → t o , where t i and t o are respectively the spacial types of f 's inputs and outputs, and S is the set of locations involved in the computation of f . This set of locations can be larger than the union of t i and t o 's sets of locations, since the computation of f can involve intermediary locations.

Examples

All the examples below assume the architecture declaration:

loc A; loc B; link A to B;
The first example comprises a conditional control structure, allowing a node f(x) to be computed, either at A, or at B, according to the value of its input m. We assume that f is of spacial type ∀δ.c at δ -{δ} → c at δ. The values defined in the two branches of the if have to be of the same type, i.e., at the same location. Furthermore, the if/then/else structure has to be duplicated on A and B, so as to be able to decide, at both locations, whether to apply f or not. Both values m and x must also be available on both locations. As the only existing link in the architecture is from A to B, the only way to resolve such constraints is to locate m and x at A, and the node output at B. The spacial type of the node g is therefore:

c at A × c at A -{A, B} → c at B
It can be noted here that this node cannot be used within a located declaration. The program below will be rejected by our type system. node g'(m,x) = y with y = g(m,x) at A

The second example is a sequence of three nodes f1, f2 and f3, each assumed to be of spacial type ∀δ.c at δ -{δ} → c at δ. f1 and f3 are localized by the programmer, respectively on A and B. f2 is not explicitely localized. node g(x) = y3 with y1 = f1(x) at A and y2 = f2(y1) and y3 = f3(y2) at B This node will be given the spacial type c at A -{A, B} → c at B. As the localization of computations has to be done modularly, a spacial type for f2 will be given once, among the two possibilities c at A -{A} → c at A and c at B -{B} → c at B.

In contrast, since there is no communication link from B to A, the following node will be rejected by the type system: node g(x) = y3 with y1 = f1(x) at B and y2 = f2(y1) and y3 = f3(y2) at A

The fourth example involves a higher-order node: the node h takes as input two nodes f and g, and an input x, and applies f to x at the location A, and then g to the result of the first application at the location B. node h (f,g,x) = z with y = f(x) at A and z = g(y) at B

The spacial type of h is then:

∀α, β, γ. (α at A -{A} → β at A) ×(β at B -{B} → γ at B) ×(α at A) -{A, B} → γ at B
The fifth example is the same higher-order node, but without any annotations:

INRIA node h (f,g,x) = z with y = f(x) and z = g(y)

The spacial type of h is then:

∀α, β, γ.∀δ. (α at δ -{δ} → β at δ) ×(β at δ -{δ} → γ at δ) ×(α at δ) -{δ} → γ at δ
As each node is projected to specialized code for each symbolic location, when no annotation is provided, we must enforce each instance of the node to be executed at one single location; this location can be any symbolic location, and is also generalized.

Finally, a node, for more modularity, can be defined with local locations. These new locations are introduced as a list between [. . .], can then be used within the node. This higher-order node uses two location variables δ 1 and δ 2 :

node h [δ 1 , δ 2 ] (f,g,x) = z with y = f(x) at δ 1 and z = g(y) at δ 2 h receives then the spacial type:

∀α, β, γ.∀δ 1 , δ 2 : {δ 1 δ 2 }. (α at δ 1 -{δ 1 } → β at δ 1 ) ×(β at δ 2 -{δ 2 } → γ at δ 2 ) ×(α at δ 1 ) -{δ 1 , δ 2 } → γ at δ 2
The set of constraints ({δ 1 δ 2 }) is inferred from the links required by the node. These constraints are resolved, with the actual architecture, when this node is instantiated. A constraint δ δ is resolved, either by stating δ = δ = s, either with two locations s and s such that there exists a communication link from s to s in the local architecture.

Thus, the node h can be instantiated these two ways (assuming the existence of two nodes f and g, both of spacial type ∀δ.c at δ -{δ} → c at δ):

y1 = h (fat A,gat A,x1) and y2 = h (fat A,gat B,x2)
We can observe than an arrow type appearing on the left of another arrow type cannot comprise more than one location. This is caused by the form taken by the distribution: since the projection operation on one node is performed on locations, and not sets of locations, we cannot handle effect variables, as it is the case in other type and effect systems.

Application

As a concrete example, we consider the definition of a reception channel of a software radio. A software radio, or software-defined radio, is a radio in which components usually defined as hardware, e.g., demodulation or filter components, are defined as software [START_REF] Mitola | The software radio architecture[END_REF]. This allows in particular the reconfiguration, possibly dynamic, of these components.

Consider a reception channel composed of three main components: a pass-band filter allowing the selection of the carrier wave, a demodulator component, and a component allowing the analysis of the received signal, e.g., an error-correction function. For the sake of performances, these components are usually implemented on different architectural elements: the pass-band filter on a FPGA, the demodulator on a digital signal processor (DSP), and the error correction on a general-purpose processor (GPP).

Each component of this reception channel could easily be defined separately. But in the case of software-defined radio, the system must support either several standards, or several functionalities [START_REF] Roy | Software-defined radio -basics and evolution to cognitive radio[END_REF]. In other word, there is a strong motivation for dynamicity.

Let us study the case of a multichannel reception system that supports the two mobile standards GSM and UMTS:

• The GSM standard involves a filter for 1800 MHz frequencies, a GMSK demodulator, and a CRC / convolutional error correction module.

• The UMTS standard involves a 2 GHz filter, a QPSK demodulator, and a CRC / convolutional / turbo codes error correction module.

Figure 1 shows an implementation of this reception channel on a system composed of three hardware components: a FPGA dedicated to the execution of the two pass-band filters, a DSP for the demodulation functions, and a GPP for error-correction modules and for the control of the whole system, i.e., in this case, the switch between the two channels. This system has one input x, the radio signal from the antenna. y denotes the output signal of the system, i.e., the decoded and corrected information received INRIA by the channel. From this value, a function gsm_or_umts (noted g on Figure 1 for the sake of brevity g(y) g(y)

Figure 1: Functional model of a multichannel software radio.

In a classical context, designing this multichannel software radio would be performed by separately programming each of the three hardware components, which raises two problems:

1. There is no guarantee that the components interact as specified: i.e., the 1800 filter with the GMSK demodulator, and so on. This requires the MUX function to be duplicated on the three computing resources, so as to guarantee the correction of the system. This situation compromises the modularity of the system.

2. Each of the two channels corresponds to an independent software entity. Programming independently each hardware component leads to the separate design, at least from some point of the design flow, of closely related software components (e.g., filter and demodulator of the same channel).

For the sake of modularity, this system would be better designed by considering the channels independently, and not the hardware components. This situation claims for adding primitives allowing to express the localization of streams directly in the language. Such primitives should allow the programming of software components independently of the architecture, handled as a separate concern. Thus, consistency analysis such as data typing could be performed on the global program: communication channels could be typed and the data consistency of the whole system could be checked. This way, inconsistencies due to serialisation could be detected at compilation time.

Figure 2 shows the implementation of this multichannel software radio, with the extended language introduced in preceding sections. This implementation strictly node channel(filter,demod,crc,x) = y with f = filter(x) at FPGA and d = demod(f) at DSP and y = crc(d) at GPP node multichannel_sdr(x) = y with c = gsm_or_umts(y) at GPP in and if (true fby c) then y = channel(filter_1800,gmsk,conv,x) else y = channel(filter_2000,qpsk,turbo,x)

Figure 2: Multichannel software radio implementation follows the architecture of the system described in Figure 1. It shows the declaration of three symbolic locations (FPGA, DSP, and GPP). We assume that all filter, demodulation, and correction functions are local ones, i.e., they are of spacial type ∀δ.c at δ -{δ} → c at δ. Since the conditional construct comprises declarations that have to be executed on the set of locations {FPGA, DSP, GPP}, c is thus inferred to be communicated to these locations. The conditional if/then/else is evaluated with the value of c at the previous instant (the definition of fby is:

(xfbyy) i = x 0 if i = 0, y i-1 else
). The distribution of this example will put a copy of this if/then/else on these three locations. Finally, the expression true fby c will be computed at GPP, since the result of this expression has to be communicated to the three locations where the conditional construct will be duplicated. By the same reasoning, we can infer that the spacial type of x is FPGA, and the one of y is GPP. As a result, the spacial type of the node multichannel_sdr is:

(c at FPGA) -{FPGA, DSP, GPP} → (c at GPP) INRIA 3 Formalization
This section is organized as follows: we first define a synchronous dataflow core language in Section 3.1 and give it its centralized semantics (Section 3.2) and its distributed semantics (Section 3.3). The centralized semantics is considered to be the reference semantics and we only consider programs which reacts with respect to this semantics. Programs that do not react (e.g., for typing or causality reasons) are assumed to be rejected by other means [START_REF] Colaço | Towards a Higher-order Synchronous Data-flow Language[END_REF][START_REF] Cuoq | Modular Causality in a Synchronous Stream Language[END_REF]. The distributed semantics allows us to give a meaning to location annotations. A spacial type system is then presented in Section 3.4. It is used to both reject programs which cannot be distributed and to annotate every expression from the source code with explicit locations. These annotations are then used by a type-directed projection operation which produces a program for each location (Section 4.4).

The Core Language Syntax

A program is made of an architecture description (A), a sequence of node definitions (d) and a main set of equations (D).

An architecture description is a set of declarations of locations (loc A) or links (link A to A) which state the existence of a communication link from one location to another. A location s is either a location variable δ, or a location constant A.

A node definition is composed of an expression and a set of equations. A set of local locations {δ 1 , . . . , δ n } can be associated as location parameters of a node definition (node f [δ 1 , . . . , δ n ](x) = e with D).

Definitions D are either single equations (x = e), definitions naming the result of an application (x = x(e)), parallel declarations (D and D), or alternative declarations (if e then D else D).

An expression e may be an immediate value (i), a variable (x), a pair construction (e, e), a binary combinatory operation (op(e, e), where op can be (+), (-),. . . ), an initialized delay (e fby e), an access function (fst e and snd e), or an expression annotated with an explicit location s (e at s).

P ::= A;d;D A ::= A;A | loc A | link A to A s ::= δ | A d ::= node f [δ 1 , . . . , δ n ](x) = e

The Centralized Synchronous Semantics

The purpose of the centralized semantics is to serve as a reference semantics. This semantics does not take into account distribution primitives. We first introduce auxiliary definitions. A value is either an immediate constant (i), a pair or a function. A sequence of location parameters δ is associated to functions.

v ::= i | (v, v) | δλx.e with D R ::= [v 1 /x 1 , . . . , v n /x n ]
An environment R associates values to names and assumes that names are pairwise distinct (for all i = j, x i = x j ).

Given a sequence d of node definitions node f i [ δ i ](x i ) = e i with D i , an initial global environment R d is defined, holding λ-values of each f i . This initial environment will be given as input of the main program.

R d = [λx 1 .e 1 with D 1 /f 1 , . . . , λx n .e n with D n /f n ]
The synchronous centralized semantics is defined by mean of two reaction predicates. R e The rules for the reaction predicates are given in Figure 3. An immediate value emits itself and rewrites to itself (rule Imm). A variable emits its current value as it is present in the reaction environment (rule Inst). An initialized delay e 1 fby e 2 emits the first value of e 1 , then the previous value of e 2 (rule Fby). An operation is performed pointwisely on immediate values (rule Op). Pair construction and destruction follow classical rules (rules Pair, Fst and Snd). Note that locations are not taken into account here (rule At): annotations added by the programmer does not alter the centralized semantics of the program (i.e., its functionality). An INRIA equation x = e emits the reaction environment defining x (rule Def). A sequential function application is replaced by its body and argument definition (rule App). The rule And states that parallel equations are mutually recursive. The rule Let stands for sequential definitions. A conditional statement executes its first branch if its condition is true (rule If-1) and its second branch otherwise (rule If-2)

The Distributed Synchronous Semantics

The distributed semantics also operates on a program P = A;d;D, but takes into account the architecture description and the explicit locations. However, it remains a synchronous semantics in the sense that the desynchronization due to the insertion of communications is not accounted for. It defines a spacialized execution: the values v emitted by expressions are now distributed values, i.e., they are annotated with location informations stating how these values are distributed on the architecture.

v ::= dv at s dv ::= i | (v, v) | Λ δ.λx.e with D R ::= [v 1 /x 1 , . . . , vn /x n ] s ::= A | G ::= S, L
A location s stands either for a single location A or a special value abstracting a set of locations. The following definition of holds:

s s = s s = s =
From this definition of distributed values, we can observe that only a subset of such values are meaningful: for distributed pairs, the values (dv at A, dv at A) at A (i.e., a centralized pair) and (dv at A, dv at B) at (a distributed pair) are meaningful, whereas no meaning can be associated to the distributed value (dv at A, dv at B) at A. The meaningful values are defined as well-formed values: a distributed value v is well-formed iff:

• either v = i at A or v = λx.e with D at A;

• or, v = (dv 1 at s 1 , dv 2 at s 2 ) at s, where (dv i at s i ) i=1,2 are well-formed, and

s = s 1 s 2 .
The operator loc(•) gathers the set of locations from a distributed value: This operator extends straightforwardly to reaction environments. The distributed semantics is defined by means of two predicates refined from their centralized versions. R e 1 v -→ e 2 states that in the distributed reaction environment R, the expression e 1 emits the distributed value v and rewrites into e 2 . represents the set of locations involved in the computation of v. The predicate for declarations is defined as well.

loc(i at s) = {s} loc(λx.e with D at s) = {s} loc((v 1 , v2 ) at s) = loc(v 1 ) ∪ loc(v 2 ) (Imm) R i i - → i (Inst) R, [v/x] x v -→ x (Fby) R e 1 v1 -→ e 1 R e 2 v2 -→ e 2 R e 1 fby e 2 v1 -→ v 2 fby e 2 (Op) R e 1 i1 -→ e 1 R e 2 i2 -→ e 2 i = op(i 1 , i 2 ) R op(e 1 , e 2 ) i - → op(e 1 , e 2 ) (Pair) R e 1 v1 -→ e 1 R e 2 v2 -→ e 2 R (e 1 , e 2 ) (v1,v2) ----→ (e 1 , e 2 ) (Fst) R e (v1,v2) ----→ e R fst e v1 -→ fst e (Snd) R e (v1,v2) ----→ e R snd e v2 -→ snd e (At) R e v -→ e R e at s v -→ e at s (Def) R e v -→ e R x = e [v/x] ---→ x = e (App) R(f ) = λy.e with D R x = e and y = e and D R -→ D R x = f (e ) R -→ D (And) R, R 2 D 1 R1 --→ D 1 R, R 1 D 2 R2 --→ D 2 R D 1 and D 2 R1,R2 ----→ D 1 and D 2 (If-1) R e true ---→ e R D 1 R -→ D 1 R if e then D 1 else D 2 R -→ if e then D 1 else D 2 (If-2) R e false ---→ e R D 2 R -→ D 2 R if e then D 1 else D 2 R -→ if e then D 1 else D 2
We note S the set of declared constant locations, and L ⊆ S×S the set of declared communication links. The relation L defines the possibility of communications, and not the actual existence of communication channels, which will be inferred by the refined version of the type system. G denotes an architecture graph, composed of a set of locations S, and a set of links L between these locations.

An architecture description A defines an architecture graph G: the notation G A : G means that given the architecture graph G, A defines the new architecture graph G . The rules Arch, Def-Loc and Def-Link define this predicate:

(Arch) S, L A 1 : S 1 , L 1 S 1 , L 1 A 2 : S 2 , L 2 S, L A 1 ;A 2 : S 2 , L 2 (Def-Loc) S, L loc A : S ∪ {A}, L (Def-Link) A 1 , A 2 ∈ S S, L link A 1 to A 2 : S, L ∪ {A 1 → A 2 }
For clarity reasons, we assume that the graph G defined by an architecture is global for subsequent semantic rules. The annotated execution of a program P is denoted Ŝin P : Ŝout , meaning that under a sequence of input environments Ŝin = R1 . R2 . . ., the program P = A;d;D produces a sequence of output environments Ŝout = R 1 . R 2 . . . such that:

∅, ∅ A : G Rd , hd( Ŝin ), hd( Ŝout ) D hd( Ŝout)
-----→ D tl( Ŝin ) A;d;D : tl( Ŝout ) Ŝin A;d;D : Ŝout Where, as for the centralized semantics, Rd defined from the sequence of node defi-

nitions d = node f i [ δ i ](x i ) = e i with D i as: Rd = [Λ δ 1 .λx 1 .e 1 with D 1 /f 1 , . . . , Λ δ n .λx n .e n with D n /f n ]
The rules for the predicates R e An immediate value can be emitted anywhere (rule Imm). Rule Inst defines the instantiation. A distributed value can be communicated from location s to location s if there exists a communication link from s to s (rule Comm). A binary operation can be performed only on immediate values located on the same location A; the result is located on A as well (rule Op). An annotated expression must involve at most the location stated for its computation (rule At). An application involves choosing a set of constant locations, and replacing location parameters by these locations in the expression and the declaration (rule At). The other rules state that the computation of a statement involves the union of the locations involved for the computation of its compounds.

Lemma 1 states that in a well-formed environment, a program reacts only by emitting well-formed values.

Lemma 1. For all D, D , R, R such that R D R -→ D , if R is well-formed, then R is well-formed.
Proof. By induction on the structure of the expression or declaration. The proof lies on the definitions of well-formed values, and the operation:

• if a value (v 1 , v2 ) at s is well-formed, then v1 and v2 are well-formed (case e = fst e or e = snd e ) ;

• if two values dv 1 at s 1 and dv 2 at s 2 are well-formed, then the value:

(dv 1 at s 1 , dv 2 at s 2 ) at s 1 s 2 is well-formed (case e = (e 1 , e 2 )) ;

INRIA (Imm) R i i at s ----→ i (Inst) R, [v/x] loc(v) x v -→ x (Comm) R e dv at s -----→ e (s, s ) ∈ L R ∪{s } e dv[s /s] at s --------→ e (Fby) R 1 e 1 v1 -→ e 1 R 2 e 2 v2 -→ e 2 R 1∪ 2
e 1 fby e 2 v1 -→ |v 2 | fby e 2 (Op) R 1 e 1 i1 at A -----→ e 1 R 2 e 2 i2 at A -----→ e 2 i = op(i 1 , i 2 ) R 1∪ 2
op(e 1 , e 2 ) • rule Comm applies only on values of the form dv at s, where s = . For any s = , if dv at s is well-formed, then dv[s /s] at s is well-formed.

i at A ----→ op(e 1 , e 2 ) (Pair) R 1 e 1 dv1 at s1 ------→ e 1 R 2 e 2 dv2 at s2 ------→ e 2
R -→ D R x = f (e ) R -→ D (And) R, R2 1 D 1 R1 --→ D 1 R, R1 2 D 2 R2 --→ D 2 R 1∪ 2 D 1 and D 2 R1, R2 ----→ D 1 and D 2 (If-1) R e true at s ------→ e R D 1 R -→ D 1 ∀s ∈ , s s R ∪ if e then D 1 else D 2 R -→ if e then D 1 else D 2 (If-2) R e false at s ------→ e R D 2 R -→ D 2 ∀s ∈ , s s R ∪ if e then D 1 else D 2 R -→ if e then D 1 else D 2
Lemma 2 states that if a program reacts with the distributed semantics, then it reacts with the centralized one and produces the same values. The proof is left in appendix.

Lemma 2. For all D, D , R, R , if R D R -→ D , then there exists R, R such that R = | R|, R = | R | and R D R -→ D .

Spacial Types

For the sake of clarity, we first present a simplified version of the type system. For the projection, we will need a refinement of this first version to take communication channels into account (see Section 4.3).

The syntax of spacial type expressions is:

σ ::= ∀α 1 , . . . , α n .∀δ 1 , . . . , δ n : C.t t ::= c | α | t at s | t -→ t | t × t ::= {s 1 , . . . , s n } s ::= δ | A H ::= H at A | [x 1 : σ 1 , . . . , x n : σ n ] C ::= {s 1 s 1 , . . . , s n s n }
We note H the spacial typing environments. H at A denotes a located environment, i.e., a typing environment from which every spacial type will be forced to represent a value entirely located on A.

We distinguish spacial type schemes (σ), which can be quantified, from simple spacial types (t). A set of constraints C can be associated to quantification of location variables (∀δ 1 , . . . , δ n : C.t). We note ∀δ 1 , . . . , δ n .t the scheme ∀δ 1 , . . . , δ n : ∅.t. A simple spacial type can be either a stream type (c), a type variable (α), a located type (t at s), a node type (s -→ s), or a pair type (s × s).

denotes sets of locations.

C is a set of constraints between locations. A constraint s 1 s 2 means that either s 1 = s 2 , or there exists a communication link from s 1 to s 2 . Conversely, a declaration of communications links L leads to the set of constraints constr(L). constr(L) = {s s |(s, s ) ∈ L} A value of spacial type t at s is a value located on s. A value of spacial type t 1 -→ t 2 is a node whose input is of spacial type t 1 , whose output is of spacial type t 2 , and whose computation involves the set of locations .

The following equalities stand for spacial types:

(t 1 × t 2 ) at s = (t 1 at s) × (t 2 at s) (t 1 -{s} → t 2 ) at s = (t 1 at s) -{s} → (t 2 at s) t at s at s = t at s t 1 = t 1 t 2 = t 2 (t 1 × t 2 ) = (t 1 × t 2 ) t 1 = t 1 t 2 = t 2 t 1 -→ t 2 = t 1 -→ t 2 A spacial type t is well-formed iff ∀t , s 1 , s 2 , t = t at s 1 at s 2 ⇒ s 1 = s 2 .
The instanciation mechanism ensures the localization of a type instantiated from a located environment:

(t[t 1 /α 1 , . . . , t n /α n , s/δ], C[s 1 /δ 1 , . . . , s m /δ m ]) ≤ ∀α 1 . . . α n ∀δ 1 . . . δ m : C.t (t at s, C) ≤ (H at s)(x) ⇔ (t at s, C) ≤ H(x)
A type t can be generalized w.r.t. a typing environment H and local locations S = {δ 1 , . . . , δ p } to a type scheme ∀α 1 , . . . , α n .∀δ 1 , . . . , δ p : C.t, provided that the set of location variable generalized {δ 1 , . . . , δ p } is not free in H, and matches with the local architecture. Generalization w.r.t. an empty local architecture allows the introduction of at most one location variable, with no constraint. This means that a node, without any location constraint given by the programmer, will receive a type of the form ∀α 1 , . . . , α n .∀δ.(t at δ), meaning that this node is available and computable at any unique location δ.

We note respectively FLV(t) and FTV(t) the set of free location variables and free type variables of the type t. FLV and FTV are straightforwardly extended to typing environments.

A set of constraints C is compatible with a set of communication links L, noted

L |= C, iff s s ∈ C ∧ s = s ⇒ (s, s ) ∈ L.
Before presenting our spacial type system, we introduce the following notations:

• For a program P , the notation P : t means that the program P is of spacial type t.

INRIA

• For declarations (resp. expressions), the notation H|G D : H / (resp. H|G e : t/ ) means that, in the spacial type environment H and the architecture graph G, the declaration D (resp. the expression e) defines a new environment H (resp. is of spacial type t), and its computation involves the set of locations .

The function locations(•) gives the set of locations involved in the spacial type given as argument. It is defined as:

locations(t 1 × t 2 ) = locations(t 1 ) ∪ locations(t 2 ) locations(t 1 -→ t 2 ) = locations(t at s) = {s}
The top-level declaration of a program is typed from the initial environment H 0 , defined as:

H 0 =       • fby • : ∀α.∀δ.α at δ × α at δ -{δ} → α at δ, fst • : ∀α, β.∀δ.α at δ × β at δ -{δ} → α at δ, snd • : ∀α, β.∀δ.α at δ × β at δ -{δ} → β at δ, (+) : ∀δ.c at δ × c at δ -{δ} → c at δ, . . .      
Our spacial type system is formally defined by the axioms and inference rules shown in Figure 6.

Typing a program involves building an architecture graph from the architecture description, and then using it to type the nodes and the main declarations (rule Prog).

An immediate value can be used on any location (rule Imm). Type schemes can be instantiated (rule Inst). Typing a pair involves stating that this pair has to be evaluated on the union of the sets of locations on which each member of the pair has to be evaluated (rule Pair). Typing a located expression (e at A) involves building a located typing environment (rule At). Communications are expressed as subtyping (rule Comm).

The spacial type of a node is composed of the spacial types of its inputs, the expression computed by this node, and the set of locations involved in this computation The type of a node is generalized w.r.t. the set of sites and links introduced by this architecture (rule Node).

Typing an equation x = e involves building a singleton typing environment (rule Def). Rule App states that an application must be evaluated on the union of the set of locations where the node f and its argument e must be evaluated, and the set of locations 1 involved in the computation of the node f . Parallel and sequential declarations involve, for their computations, the union of the sets and of locations involved in the computation of their compounds (rules And and Let). Finally, typing an if/then/else declaration involves locating the condition expression on a location s, and adding constraints that every location involved in declarations D 1 and D 2 must be accessible from s (rule If).

} L ⊆ L ∪ ({δ 1 , . . . , δ n } × S) ∪ (S × {δ 1 , . . . , δ n }) {α 1 , . . . , α m } = FTV(t) -FTV(H) C = constr(L \ L) σ = ∀α 1 , . . . , α m .∀δ 1 , . . . , δ n : C.t -1 ∪ 2 → t 1 H|G node f [δ 1 , . . . , δ n ](x) = e with D : [σ/f ]/ 1 ∪ 2 (Def
A set of locations is related to an abstract location, as defined in Section 3.3, by:

= s if = {s} else.
We denote by v : t the fact that the distributed value v has spacial type t:

s = dv at s : c at s v1 : t 1 v2 : t 2 (v 1 , v2 ) : t 1 × t 2
We denote by R : H the type compatibility between R and H:

R : H ⇔ ∀x ∈ dom( R), x ∈ dom(H) ∧ ∃(t, C) s.t. (t, C) ≤ H(x) ∧ R(x) : t
Theorem 1 states that if a program reacts with the centralized semantics, and is accepted by the spacial type system, then there exists a spacialized execution such that the distributed values of this execution are equal to the centralized ones. The spacial types are preserved by this spacial execution. The proof is in appendix.

Implementation

The spacial type system presented in the previous section lies on a subtyping mechanism. It corresponds to the case when communications can occur anywhere in the code. This situation raises two problems. The first one is that the implementation of type systems with subtyping mechanism is costly: usual algorithms involve the systematic application of the subtyping rule. The second one is that this choice leads to a situation where the programmer has no control on where the communications can occur. These problems, though orthogonal, can be addressed together: giving some control to the programmer means restricting the points where subtyping can be applied. We show here how to refine our type system in order to address these two problems.

We restrain communicated values to be variables introduced by equations (x = e). Thus, within the program given in Section 2.2, only y and z can be communicated from one location to another. Then, we can use a generalization mechanism to infer communication constraints, instead of inferring them by subtyping. This corresponds to restricting the subtyping mechanism at instantiation points.

The refined type system, noted H|G i e : t/ , involves the suppression of the rule Comm and the modification of the rule Def as follows:

(Def)
H|G i e : t at s/ H|G i x = e : [∀δ : {s δ}.t at δ/x]/

Typing an equation x = e involves locating the result of e on a location s, and building a typing environment allowing x to be on any location accessible from s (x : ∀δ : {s δ}.t at δ) (rule Def). The other rules remain the same.

We then show the correction of the refinement, i.e., that every program accepted by the refined type system is accepted by the original type system.

Theorem 2 (Refined type system correction). For all H, H , D, G, , if H|G i D : H / , then H|G D : H / .

Proof. By induction on the structure of D and e. Whenever the rule Inst of the refined type system can be applied, we can apply the rule Inst, then the rule Comm, of the original type system. This refined type system has been implemented in the compiler of Lucid Synchrone.

Distribution

Principle

Once programs have been typed, every expression is annotated with a location that specifies where it has to be computed. Communications are inserted when a value is INRIA produced at a location and used at another. From this typed program, the compiler produces several new programs -one for every location s -erasing the code that is not necessary at this location s. The run-time we have chosen is a classical one for globally asynchronous locally synchronous (GALS) systems: communications are done through FIFOs.

We show below the result of the projection of f on A and B, noted respectively f_A and f_B. The distribution of this node will involve adding a communication between these two computations. This communication will take the form of an additional output (named here c_y) on f_A, together with an additional input on f_B. Here, c_y holds the value y, computed on A and used on B. Original inputs and outputs are not suppressed: () denotes an irrelevant value which will not be used on the current location. It is used here to replace the output z, whose computation is suppressed at A. node f_A(x) = ((),c_y) with c_y = g(x)

node f_B(x,c_y) = z with z = h(c_y)

The semantically equivalent distributed system is then obtained by connecting the input and output c_y, holding the communicated value y. The program below shows the distributed execution, using a FIFO materialized by send/receive primitives, of the result of the projection of the program y = f(x).

(y_A,c_y) = f_A(x); receive(c_y); send(c_y) y_B = f_B((),c_y)

Example

The result of the projection of the two nodes of the Section 2.5 on the location DSP is given on Figure 7. The projection of the channel node shows that the node applications of filter and crc have been removed, and that a new input c1 (holding the value of f) and a new output c2 (holding the value of d) have been added. This implies the addition, on the projection of the multichannel_sdr node, of two new inputs (c2 and c3) and two new outputs (c4 and c5), one for each channel instance.

The new input c1 of the projected multichannel_sdr node holds the value c.

node channel(filter,demod,crc,x,c1) = ((),c2) with d = demod(c1) and c2 = d node multichannel_sdr(x,s,c1,c2,c3) = (y,c4,c5) if c1 then (y,c4) = channel(filter_1800,gmsk,conv,x,c2) else (y,c5) = channel(filter_2000,qpsk,turbo,x,c3)

Figure 7: Result of the projection on DSP

Channel Inference

We define now a refined type system, allowing the inference of communication channels. These channels will be used for the projection, and have been omitted in the first type system for the sake of clarity.

A channel is a location pair associated with a name, noted A 1 n → A 2 : n is the name of the channel, A 1 its source location, and A 2 its destination location. The set of channel names is ordered, so as to keep consistence of inputs and outputs added, from the node definition to node instances. T denotes sets of channels. The union of sets of channels, noted T 1 T 2 , is defined iff channel names in T 1 and T 2 are disjoint.

A channel can be renamed: we note by s r(n) → s the channel s n → s renamed by the function r. Given two channel sets T and T , we note T ∼ = T the fact that T is equal to T modulo a monotone renaming of its channels (i.e., the order between these channels is the same in T and T ):

T ∼ = T ⇔ ∃r s.t. r monotone and T = {s r(n) → s |s n → s ∈ T }
The Figures 8 and9 shows our refined type system: H|G e : t/ /T means that, in the typing environment H, the expression e has spacial type t, and its computation involves the set of locations and the set of communication channels T . Channels are added for each communication (rule Comm-C), and for application of nodes which need internal channels (rule App-C). For applications, we have to rename channels, with a renaming preserving the name order. Thus, we can instanciate nodes several times, adding each time new channel names as inputs and outputs INRIA when the projection will be performed. The other rules only perform the disjoint unions (w.r.t. channel names) of sets of channels. The rules defining the program types and the architecture remain the same and are not repeated.

(Imm-C) H|G i : c at s/{s}/∅ (Inst-C) (t, C) ≤ (H(x)) L |= C H| S,

Projection

We will now define a type-directed operation of projection of an expression on a location A. This operation is defined separately, as it has to be performed on an already annotated program: links between values of each projected program are defined by the channels inferred by the type system. The projection of a declaration D on a location A is noted H|G D : H / /T A =⇒ D , and results in a new declaration D , containing only the computations to be performed on A. The projection of an expression e, of spacial type t, on a location A, is noted H|G e : t/ /T A =⇒ e /D, and results in a new expression e , as well as a declaration D, containing channels outputs to be defined. A channel named n in an environment channel will be introduced as the variable c n as input or output of the target program, c assumed to be of different name space than other variables of the source program.

We denote by the empty declaration, and by () a value which will never be used (i.e., void). For any declaration D, D and = and D = D. For any expression e, we have (() e) = (e ()) = (). Also, we note T ↑ A (resp. T ↓ A) the set of channels with origin (resp. destination) A:

(Node-C) H, x : t, H 1 | S , L D : H 1 / 1 /T 1 H, x : t, H 1 | S , L e : t/ 2 /T 2 S = S ∪ {δ 1 , . . . , δ n } L ⊆ L ∪ ({δ 1 , . . . , δ n } × S) ∪ (S × {δ 1 , . . . , δ n }) {α 1 , . . . , α m } = FTV(t) -FTV(H) C = constr(L \ L) σ = ∀α 1 , . . . , α m .∀δ 1 , . . . , δ n : C.t -1 ∪ 2 /T 1 T 2 → t 1 H|G node f [δ 1 , . . . , δ n ](x) = e with D : [σ/f ]/ 1 ∪ 2 /∅ (Def-C) H|G e : t/ /T H|G x = e : [t/x]/ /T (App-C) H|G f : t 1 -1 /T 1 → t 2 / 2 /T 2 H|G e : t 1 / 3 /T 3 T 1 ∼ = T 1 H|G x = f (e) : [t 2 /x]/ 1 ∪ 2 ∪ 3 /T 1 T 2 T 3 (And-C) H|G D 1 : H 1 / 1 /T 1 H|G D 2 : H 2 / 2 /T 2 H|G D 1 and D 2 : H 1 , H 2 / 1 ∪ 2 /T 1 T 2 (Let-C) H|G D 1 : H 1 / 1 /T 1 H, H 1 |G D 2 : H 2 / 2 /T 2 H|G let D 1 in D 2 : H 2 / 1 ∪ 2 /T 1 T 2 (If-C) H|G e : c at s/ /T H|G D 1 : H / 1 /T 1 H|G D 2 : H / 2 /T 2 C = {s s |s ∈ 1 ∪ 2 } L |= C H|G if e then D 1 else D 2 : H / ∪ 1 ∪ 2 /T T 1 T 2 channels(C)
T ↑ A = {A n → A ∈ T } T ↓ A = {A n → A ∈ T }
The projection rules are given in Figures 10 and11.

Channels are used at communication points. If an expression e is send from A to A through the channel A n → A , then:

INRIA

• for the projection on A, the communication involves sending a value: the resulting expression is void, and we add the definition of the channel c n as the result of the projection of e on A (rule Comm-P-From);

• for the projection on A , the communication involves receiving a value: the resulting expression is the channel holding this value (rule Comm-P-To).

Finally, if A does not appear in the set of locations involved in its computation, then the expression can be suppressed on A (rule Suppr-P). Projections of a pair consist in the projection of its compounds (rule Pair-P).

The projection of a located declaration and parallel declarations involves the projection of its compound (rules At-P and And-P).

The projections of applications and node definitions involve adding to the inputs and outputs of the node, the channels used by this node (rules App-P and Node-P). Nodes with local architecture are assumed to be inlined. The relevance of the name order appears here, as the order of the added inputs and outputs must be consistent with every instances of these nodes, and for every projection.

Projection of a conditional is divided in two rules:

• one for the projection on a location where the conditional expression is computed: this first rule shows the definition of every channel needed to send this value to other locations where the conditional will be evaluated (rule If-P-From);

• one for the projection on a location where the conditional expression has to be received: this expression is then replaced by the name of the channel holding this value (rule If-P-To).

Lemma 3 states that a program accepted by the spacial type system can always be projected on every location of the architecture. Lemma 3. For all H, H , D, , T , if H|G D : H / /T then ∀A ∈ S, ∃D s.t.

H|G D : H / /T A =⇒ D .
Proof. Since the projection operation is type-directed, a projection rule can always be applied from the equivalent one of the type system. The property trivially holds.

The global meaning of a distributed program is then defined by the parallelization of its projected declarations.

(Imm-P) We note S = {A 1 , . . . , A n } the set of defined constant locations where the source declarations are projected. The global meaning of a declaration D, projected on the locations S, is then defined by: D 1 and . . . and D n where ∀i, H|G D : H / /T

H|G i : c at s/{s}/∅ A =⇒ i/ (Inst-P) (t, C) ≤ (H(x)) L |= C H|G x : t/ /∅ A =⇒ x A / (
H, x : t, H 1 |G D : H 1 / 1 /T 1 A =⇒ D H, x t , H 1 |G e : t/ 2 /T 2 A =⇒ e /D e T 1 T 2 ↑ A = {A n1 → A 1 , . . . , A np → A p } T 1 T 2 ↓ A = {A m1 → A 1 , . . . , A mq → A q } n i < n i+1 m i < m i+1 H|G node f (x) = e with D : [gen H (t -1 /T 1 T 2 → t 1 )/f ]/ 1 ∪ 2 /∅ A =⇒ node f A (x,
H|G f : t 1 -1 /T 1 → t 2 / 2 /T 2 A =⇒ f /D 1 H|G e : t 1 / 3 /T 3 A =⇒ e /D 2 T 1 ∼ = T 1 T 1 ↑ A = {A n1 → A 1 , . . . , A np → A p } T 1 ↓ A = {A 1 m1 → A, . . . , A q mq → A} n i < n i+1 and m i < m i+1 H|G x = f (e) : [t 2 /x]/ 1 ∪ 2 ∪ 3 /T 1 T 2 T 3 A =⇒ (x, c m1 , . . . , c mq ) = f (e , c
H|G D 1 : H 1 / 1 /T 1 A =⇒ D 1 H|G D 2 : H 2 / 2 /T 2 A =⇒ D 2 H|G D 1 and D 2 : H 1 , H 2 / 1 ∪ 2 /T 1 T 2 A =⇒ D 1 and D 2 (If-P-From) H|G e : c at s/ /T A =⇒ e /D H|G D 1 : H / 1 /T 1 A =⇒ D 1 H|G D 2 : H / 2 /T 2 A =⇒ D 2 C = {s s |s ∈ 1 ∪ 2 } L |= C T = channels(C) T ↑ A = {A n1 → A 1 , . . . , A np → A p } x ∈ dom(H) H|G if e then D 1 else D 2 : H / ∪ 1 ∪ 2 /T T 1 T 2 channels(C) A =⇒ x =
1 : H / 1 /T 1 A =⇒ D 1 H|G D 2 : H / 2 /T 2 A =⇒ D 2 C = {s s |s ∈ 1 ∪ 2 } L |= C T = channels(C) T ↓ A = {A n → A} H|G if e then D 1 else D 2 : H / ∪ 1 ∪ 2 /T T 1 T 2 channels(C) A =⇒ if c n then D 1 else D 2
A i =⇒ D i
In order to relate a target program with its source, we define a relation on values, denoted

• • • •, such that v A t v
means that the value v , emitted from an expression of type t, represents the value v at the location A. We have:

v = v v A t at A v A = A () A t at A v v 1 A t 1 v 1 v 2 A t 2 v 2 (v 1 , v 2 ) A t 1 ×t 2 (v 1 , v 2 )
We can then relate two reaction environments R and R

Discussion

Related Work

Various solutions have emerged in order to use synchronous languages for the design of distributed systems [START_REF] Girault | A survey of automatic distribution method for synchronous programs[END_REF]. Some of them operate on a compiled model of the program, by "coloring" atomic instructions with localization informations, inferred from inputs and outputs locations [START_REF] Caspi | Automatic distribution of reactive systems for asynchronous networks of processors[END_REF]. The whole program is first compiled into an intermediate sequential format, on which the distribution is then applied. This format consists of a sequence of atomic instructions, representing one computation

INRIA

step of new values carried on each stream. Then, the distribution involves placing each instruction onto one or several locations, taking into account the consistency of the control flow on each location. Another approach is to directly annotate the source program with locations, so as to define the localization of each variable of the program: the distribution is then performed with regard to these annotations. This approach has been applied to Signal [START_REF] Aubry | On the desynchronization of synchronous applications[END_REF] as well as Lustre [START_REF] Caspi | From Simulink to Scade/Lustre to TTA: A layered approach for distributed embedded applications[END_REF]. In both cases, the correction of the distribution algorithm has been proved [START_REF] Caillaud | Distributing automata for asynchronous networks of processors[END_REF][START_REF] Maffeïs | Ordonnancements de graphes de flots synchrones ; Application à la mise en oeuvre de Signal[END_REF], meaning that the combined behavior of the distributed fragments has the same functional and temporal semantics as the initial centralized program. The originality of our method resides in the fact that we use a spacial type system to check the consistency of the distribution specifications inserted by the programmer, and that we perform modular distribution, allowing the expression of higher-order features, applied for instance to dynamic reconfiguration of nodes by application of other nodes as inputs. Since a Kahn semantics can be given to our language, the semantical equivalence between the source program and the synchronous product of the fragments resulting from the projection is sufficient to describe an asynchronous distribution. While the language presented has higher-order features, this method can easily be applied to other language with comparable semantics such as Lustre. In contrast, more general frameworks such as Signal cannot be addressed here for this reason.

Several approaches have been considered to solve the problem of data consistency of distributed programs. A translation operation is presented in [START_REF] Neubauer | From sequential programs to multi-tier applications by program transformation[END_REF], as well as an effect type system, in order to automatically obtain a multi-tier application from an annotated source program. Our proposition differs by the fact that our type system is not only a specification, but also consists in what the authors called "location analysis", thus allowing us to perform this analysis in a modular way, and on a program comprising higher-order features. Type systems have been used to ensure memory consistency [START_REF] Talpin | Polymorphic type, region and effect inference[END_REF], or for pointer analysis within a distributed architecture [START_REF] Liblit | Type systems for distributed data structures[END_REF]. The Acute language [START_REF] Sewell | Acute: High-level programming language design for distributed computation[END_REF] is an extension of OCaml with typed marshalling. Communication channels between two Acute programs can also be considered as typed, as the type of marshalled and unmarshalled data are dynamically verified, at execution time. The consistency considered is between separately-built programs, whereas our approach is to consider the programming of a distributed system as one global program, allowing global static verifications. Finally, Oz and its distributed extension [START_REF] Bal | Programming languages for distributed computing systems[END_REF] proposes a way to separate the functionality of a distributed application and its distribution structure, by allowing the programmer to give a different distributed semantics to every different object of a program. This language aims at loosely coupled distributed systems without architecture constraints, whereas our approach concerns strongly coupled architecture, and we aim to ensure the consistency of the distribution w.r.t. one architecture, given the communication constraints.

Conclusion and Future Work

We have proposed a spacial type system to solve the problem of automatic distribution of dataflow programs. It is based on a core dataflow language, which we have extended with distribution primitives to allow the programmer to specify, on one hand his/her target distributed architecture, and on the other hand where some nodes and/or variables are to be located. The underlying philosophy is the functional distribution, meaning that some functionalities of the program must be computed at some precise location because they require some specific sensors, actuators, and/or computing resources that are available only at this location. In this context, we use type inference to decide at which location each node must be computed, and at which points in the program communication primitives must be inserted. The compilation of a correctly spacially typed program produces one program for each computing location specified by the programmer. We use abstract communication channels to exchange a value between two locations and to synchronize them. Compiling each program and linking with a dedicated library implementing those communication channels then gives one binary code for each location. The refined version of the type system, as well as the operation projection, has been implemented in the compiler of Lucid Synchrone [START_REF]Lucid synchrone[END_REF].

Future work mainly involves allowing the description of more complex architectures, with hierarchical locations or communication masking (e.g., MPSoCs): our proposal of architecture constraints is not sufficient to catch the complexity of actual architecture of distributed embedded systems. Yet, our current constraints show the interest of a type system for checking the consistency of a distributed program w.r.t. such constraints.

A Proofs

INRIA

A.2 Type system correction

The proof of the theorem 1 is based upon the following lemmas. The first states that the set of locations needed for the computation of an expression typed from a typing environment located on A is the singleton {A}. Proof. From the definition of the instantiation, for all H, A, x, C, t such that (t, C) ≤ (H at A)(x), ∃t , such that t = t at A. Thus locations(t) = {A}.

The lemma is then proved by induction on the structure of e. The other rules only perform union of location sets from the spacial types of compounds of e, thus the property holds.

The following lemma is the equivalent of the theorem 1 for expressions: Proof. By induction on the structure of the typing derivation tree of e. For each applied rule of the type system, we can apply a matching rule of the distributed semantics.

The induction operates on the last applied rule of the type system. Case of rule Imm: e = i. Let s such that H|G i : c at s/{s}. For any R, R such -→ e 2 .

that | R| = R, R i i - → i ⇒ R {s} i i at
• By induction hypothesis, there exists R, v1 , v2 such that R -→ e 2 , v1 : t 1 and v2 : t 2 . Let v1 = dv 1 at s 1 and v2 = dv 2 at s 2 .

• Then, rule Pair applies: R

1 ∪ 2 (e 1 , e 2 ) (v 1 ,v 2 ) at s 1 s 2 ----------→ (e 1 , e 2 ), 1 ∪ 2 = s 1 s 2 and ((v 1 , v2 ) at s 1 s 2 ) : (t 1 × t 2 ).
Case of rule Fst: e = fst e 1 .

• From the definition of H 0 , H|G e : t/ iff ∃s 1 , s 2 , t 1 , t 2 such that H|G e 1 :

(t 1 at s 1 , t 2 at s 2 )/{s 1 , s 2 }.

• From rule Fst of the centralized semantics, R fst e

1 v 1 -→ fst e 1 iff ∃v 2 , R e 1 (v 1 ,v 2 )
----→ e 1 .

• By induction hypothesis, there exists R, v such that

R {s 1 ,s 2 } e 1 v - → e 1 . |v| = (v 1 , v 2 ) then ∃v 1 , v2 , s such that v = (v 1 , v2 ) at s . • Applying rule Fst: R {s 1 ,s 2 } fst e 1 v1
-→ fst e 1 . v : t 1 × t 2 , then v1 : t 1 .

Case of rule Snd (same as rule Fst): e = snd e 1 .

• From the definition of H 0 , H|G e : t/ iff ∃s 1 , s 2 , t 1 , t 2 such that H|G e 1 :

(t 1 at s 1 , t 2 at s 2 )/{s 1 , s 2 }.

• From rule Snd of the centralized semantics, R snd e

2 v 2 -→ snd e 2 iff ∃v 1 , R e 2 (v 1 ,v 2 ) ----→ e 2 .
• By induction hypothesis, there exists R, v, s such that

R {s 1 ,s 2 } e 2 v - → e 2 . |v| = (v 1 , v 2 ) then ∃v 1 , v2 , s such that v = (v 1 , v2 ) at s . • Applying rule Snd: R {s 1 ,s 2 } snd e 1 v1 -→ snd e 1 . v : t 1 × t 2 , then v2 : t 2 .

INRIA

Case of rule Fby: e = e 1 fby e 2 .

• From the definition of H 0 , H|G e : t/ iff H|G e 1 : t/ and H|G e 2 : t/ .

• From rule Fby of the centralized semantics, R e 1 fby e 2 Case of rule At: e = e 1 at s.

• H|G e 1 at s : t/ iff H at s|G e 1 : t/ .

• R e 1 at s v -→ e iff ∃e 1 , e = e 1 at s and R e 1 v -→ e 1 .

• By induction hypothesis, there exists R, v,

s such that R e 1 v - → e 1 , | R| = R, |v| = v, R : H, v : t.
• From lemma 4, = {s}.

• Applying rule At:

R {s} e 1 at s v -→ e 1 at s.

Case of rule Comm.

• H| S, L e : t at s / iff there exists such that = ∪ {s}, H| S, L e : t at s/ and L |= s s .

• R e v -→ e .

• By induction hypothesis, there exists R, v, s such that R e • H|G x = e : H / iff ∃s, t, H = [∀δ : {s δ}.t at δ/x] and H|G e : t at s/ . • H|G f : • By induction hypothesis, ∃ R, R such that R x = e • From rule Inst of spacial type system, H|G f : t 1 -1 → t 2 / 2 iff 2 = locations(t 1 -1 → t 2 ) = 1 .

• R x = e R -→ D iff ∃e , v, D = (x = e ), R = [v/x], and R e v -→ e . • By application of lemma 5, ∃ R, v such that R e v -→ e , | R| = R, R : H, |v| = v, v : t at s. • Applying rule Def: R x = e [v/x] ---→ x = e . |[v/x]| = [v/x] = R, [v/x] : [∀δ : {s δ}.t at δ/x] since v : t at s. Case D = (x = f (e)). • H|G x = f (e) : H / iff ∃s, t 1 , t 2 , 1 , 2 , 3 such that = 1 ∪ 2 ∪ 3 , H = [t 2 /x], H|G f : t 1 -1 → t 2 /
t 1 -1 → t 2 / 2 iff

INRIA

• Then, = 1 ∪ 3 = .

Case D = D 1 and D 2 .

• H|G D 1 and D 2 : H / iff ∃H 1 , H 2 , 1 , 2 such that = 1 ∪ 2 , H|G D 1 :

H 1 / 1 and H|G D 2 : H 2 / 2 .

• R D 1 and

D 2 R -→ D iff ∃R 1 , R 2 , D 1 , D 2 such that R.R 2 D 1 R 1 --→ D 1 and R.R 1 D 2 R 2 --→ D 2 .
• By induction hypothesis, ∃ R, R1 , R2 such that -R. R2

1

D 1 R1 --→ D 1 , -R. R1 2 D 2 R2 --→ D 2 , -| R| = R, | R1 | = R 1 , | R2 | = R 2 ,
-R : H, R1 : H 1 , R2 : H 2 .

• Applying rule And: R -Case v = false: same as case v = true.

A.3 Projection correction

The proof of the theorem 3 is based on the following lemma, stating that if the projection of an expression e on every location A i is the couple e i /D • H|G D : H / /T iff ∃t 1 , t 2 , 1 , 2 , 3 , T 1 , T 1 , T 2 , T 3 ,such that:

RR n°6378

  node g(m,x) = z with if m then let y = f(x) at A in z = y else let y = f(x) at B in z = y

  with D | d;d D ::= x = e | x = x(e) | D and D | if e then D else D e ::= i | x | (e, e) | op(e, e) | e fby e | fst e | snd e | e at s

1 v- → e 2 1 R-→ D 2

 1212 states that in the reaction environment R, the expression e 1 emits the value v and rewrites into the new expression e 2 . The predicate R D states that in the reaction environment R, the declaration D 1 defines the reaction environment R and rewrites into D 2 . The centralized execution of a program P is denoted S in P : S out , meaning that under a sequence of input environments S in = R 1 .R 2 . . ., the program P = A;d;D produces a sequence of output environments S out = R 1 .R 2 . . . such that (denoting hd(R.S) = R and tl(R.S) = S): R d , hd(S in ), hd(S out ) D hd(Sout) -----→ D tl(S in ) A;d;D : tl(S out ) S in A;d;D : S out

Figure 3 :

 3 Figure 3: Centralized synchronous semantics

  1 v -→ e 2 and R D 1 R -→ D 2 are given in Figures ?? and 5.

R 1 ∪ 2 (e 1 , e 2 )Figure 4 :

 12124 Figure 4: Distributed synchronous semantics (expressions)

Figure 5 :

 5 Figure 5: Distributed synchronous semantics (equations)

Theorem 1 (

 1 Correction). For all D, D , H, H , R, R , G, if H|G D : H / and R D R -→ D , then there exists R, R such that R D R -→ D , R : H, R : H , | R| = R and | R | = R .

Figure 9 :

 9 Figure 9: Refined type system, with communication channels (equations)

(H|G e 1 : t 1 / 1 /T 1 A=⇒ e 1 /D 1 H|G e 2 : t 2 / 2 /T 2 A=⇒ e 2 /D 2 H|G e 1 , e 2 : t 1 × t 2 / 1 ∪ 2 /T 1 T 2 A=⇒ e 1 , e 2 /D 1 and D 2 Figure 10 :

 1111122222121212212210 Figure 10: Rules for the projection operation (expressions)

  c m1 , . . . , c mq ) = (e , c n1 , . . . , c np ) with D and D e (At-P) H at A|G D : H / /T A =⇒ D H|G D at A : H / /T A =⇒ D (Def-P) H|G e : t/ /T A =⇒ e /D H|G x = e : [t/x]/ /T A =⇒ x A = e and D (App-P)

2 (

 2 n1 , . . . , c np ) and D 1 and D And-P)

2 (

 2 e and c n1 = x and . . . and c np = x and if x then D 1 else D If-P-To) H|G e : c at s/ /T A =⇒ e /D H|G D

Figure 11 :

 11 Figure 11: Rules for the projection operation (equations)

  p w.r.t. a typing environment H: R H ∼ = R p iff ∀x ∈ dom(R), ∀A ∈ S, R(x) A H(x) R p (x A ) Theorem 3 states that the projection operation is correct, i.e., the projection of a source program D into D i (for every location A i ) defines a new target program D 1 and . . . and D n , which is semantically equivalent, taking into account spacial types' values, with the source declaration D. Theorem 3 (Correction of the declarations projection). For all H, H , D, D , , T , D i , R, R , if R D R -→ D , H|G D : H / /T and ∀i, H|G D : H / /T A i =⇒ D i , then there exists R p , R p , D p , D p such that D p = D 1 and . . . and D n , R H ∼ = R p , R p D p R p --→ D p , and R H ∼ = R p .

A. 1

 1 Distributed and centralized semantics (Lemma 2). The proof lies in the extension of the | • | operator to the predicates R e v -→ e and R D R -→ D . For each rule of the distributed semantics, we can replace the predicate R e v -→ e by | R| e |v| -→ e and R D R -→ D by | R| D | R | --→ D to obtain an equivalent centralized semantics.

Lemma 4 .

 4 For all H, A, G, D, H , , if H at A|G D : H / then = {A}.

Lemma 5 (

 5 Correction for expressions). For all e, e , H, G, t, , R, v, if H|G e : t/ and R e v -→ e , then there exists R, v such that R e v -→ e , R : H, v : t, | R| = R and |v| = v.

  s ---→ i and i at s : c at s. Case of rule Inst: e = x. Let H, L, S, t, such that H| L, S e : t/ . Let R, v, e such that R e v -→ e . • Case | | > 1. For all R such that | R| = R and R : H, then there exists dv such that R(x) = dv at . Then the rule Inst applies: R, [dv at /x] x dv at -----→ x. Moreover, |dv at | = v since | R| = R, and dv at : t since R : H. • Case | | = 1 ( = {s} = locations(t)). For all R such that | R| = R and R : H, then there exists dv such that R(x) = dv at s. The rule Inst applies: R, [dv at s/x] {s} x dv at s ----→ x. Case of rule Pair: e = (e 1 , e 2 ).

v-→ e iff ∃v 1 1 -→ e 1 and R e 2 v 2 -→ e 2 .• 1 v1-→ e 1 , R e 2 v2-→ e 2 , 2 v1-→ |v 2 |

 1112212222 , v 2 , e 1 , e 2 such that v = v 1 , e = v 2 fby e 2 , R e 1 v By induction hypothesis, there exists R, v1 , v2 such that R e |v 1 | = v 1 , |v 2 | = v 2 , v1 : t and v2 : t. • Applying rule Fby: R e 1 fby e fby e 2 .

1 v - → e 1 ,

 1 | R| = R, |v| = v, R : H, v : t at s. • Applying rule Comm: R ∪{s} e 1 at s R -→ e 1 at s. (Theorem 1). By induction on the structure of D. Case D = (x = e).

  [START_REF]Architecture analysis & design language[END_REF] and H|G e :t 1 / 3 . • R x = f (e) R -→ D iff ∃e 1 , D 1 such that R(f ) = λy.e 1 with D 1 and R x = e 1 and y = e and D 1 R -→ D .

1 and y = e and D 1 R 1 R11- 12 x = e 1 [

 11121 -→ D , | R| = R, | R | = R , R : H, R : H . • Applying rule App: R x = f (e) R -→ D . • R x = e 1 and y = e and D 1 R -→ D iff there exists R11 , v12 , v3 , e , D 1 , e 1 such that-R.[v 12 /x, v3 /y] D -→ D 1 , -R. R11 .[v 3 /y] v 12 /x] ----→ x = e 1 , -R. R11 .[v 12 /x] 3 y = e [v 3 /y] ---→ y = e .• By induction, 11 = 11 , 12 = 12 , and 3 = 3 . Then = 1 ∪ 3 .

1 ∪ 2 D 1 1 R-→ D 1 1 D 1 R-→ D 1 , 1 if e then D 1 else D 2 R

 1211111112 and D 2 R1 . R2 ----→ D 1 and D 2 . ( R1 . R2 ) : (H 1 .H 2 ) and | R1 . R2 | = R 1 .R 2 . Case D = if e then D 1 else D 2 . • H|G if e then D 1 else D 2 : H / iff there exists s, , 1 , 2 such that = ∪ 1 ∪ 2 , H|G e : c at s/ , H|G D 1 : H / 1 , H|G D 2 : H / 2 and ∀s ∈ 1 ∪ 2 , s s . • R if e then D 1 else D 2 R -→ D iff there exists e such that R e v -→ e , with v = true or v = false. -Case v = true: there exists D 1 such that R D and D = if e then D 1 else D 2 . * By induction hypothesis, ∃ R, R such that R e true at s ------→ e , R | R| = R, R : H, | R | = R , R : H . * Applying rule If-1: R ∪ -→ if e then D 1 else D 2 .

1 A 2 A 1 R 1 R

 1211 i A c at s i. Case of rule Inst: e = x. Then, R x v -→ x. H|G x : t/ /T , then, ∃C, S, L such that G = S, L , (t, C) ≤ H(x) and L |= C. Then the rule Inst-P applies: for all A, H|G x : t/ A =⇒ x A . Let D p = , R p = ∅ and vA = R p (x A ). R p x A v A -→ x A , and v A A t v since R H ∼ = R p .Case of rule Pair: e = (e 1 , e 2 ). By induction, and the fact that H|G e : t/ /T iff∃ 1 , 2 , T 1 , T 2 , t 1 , t 2 such that = 1 ∪ 2 , T = T 1 T 2 , t = t 1 ×t 2 ,H|G e 1 : t 1 / 1 /T 1 and H|G e 2 : t 2 / 2 /T 2 . Then for a site A, H|G e 1 : t 1 / 1 /T =⇒ e 1 /D 1 and H|G e 2 : t 2 / 2 /T =⇒ e 2 /D 2 , there exists R p, R p1 , R p2 , such that R p D p21 ---→ D 1 , R p D 2 R p2 --→ D 2 , and dom(R p1 ) ∩ dom(R p2 ) = ∅. Then, taking R p = R p1 .R p2 , R p D 1 and D 2 R p --→ D1 and D 2 , and there exists v such that R p , R p (e 1 , e 2 ) v -→ (e 1 , e 2 ). Case of rules Fst and Snd: e = fst e and e = snd e : direct induction. Case of rule Comm: H|G e : t/ /T iff ∃t , A, A , T , n such that the architecture allows the communication from A to A , t = t at A , T = T {A n → A }, and H|G e : t at A 1 / /T . INRIA By induction hypothesis, for every location A i , there exists e i , D i such that H|G e : t at A/ /T A i =⇒ e i /D i . Let D p = D 1 and . . . and D n , D p and R p such thatR p D p R p --→ D p . For each i, let v i , e i such that R p , R p e i v i-→ e i .• If A i = A, then by induction hypothesis, v i A i t at A v. By application of the rule Comm-From, H|G e :t at A / ∪ {A }/T {A n → A } A i =⇒ ()/D i and c n = e i . Then, as A i = A , () A i t at A v. • If A i = A ,then by application of the rule Comm-To, H|G e : t at A / ∪ {A }/T {A n → A } A i =⇒ c n /D i . From rule Comm-From, ∃v p , e p such that D p = D p and c n = e p , Theorem 3. By induction on the structure of D. Case D = D 1 at A. Direct induction. Case D = (x = e). • R D R -→ D iff there exists e , v, D = (x = e ), R = [v/x], and R e v -→ e . • H|G x = e : H / iff ∃s, t, H = [∀δ : {s δ}.t at δ/x] and H|G e : t at s/ . • Let {A 1 , . . . , A n } = S. For all i, H|G D : H / /T A i =⇒ D i iff there exists e i , D i such that H|G e : t at s/ /T A =⇒ e i /D i . • Let R p such that R p H ∼ = R. By application of lemma 6, there exists v i , e i , D e , D e , R e , D e = D 1 and . . . and D n , R p D e R e --→ D e , R p , R e e i v i -→ e i and v i A i t at s v. • Then, by application of rule Def-P, taking D i = (x A i = e i ) and D i , and D p = D 1 and . . . and D n and R p = R e .[v 1 /x A 1 , . . . , v n /x An ], R p D p R p --→ D p . Case D = (x = f (e)). • R D R -→ D iff there exists e 1 , D 1 such that R(f ) = λy.e 1 with D 1 and R x = e 1 and y = e and D -→ D .

  ), local at GPP, computes what channel will be used at next instant. In this figure, each location is graphically represented by a gray box.

	FPGA	DSP	GPP
	filter_1800	dem_GMSK	CRC/conv
	x		MUX	y
	filter_2000	dem_QPSK	CRC/turbo

  H|G e 1 : t 1 / 1 H|G e 2 : t 2 / 2 H|G (e 1 , e 2 ) : t 1 × t 2 / 1 ∪ 2

	(Prog)
		∅, ∅	A : G	H 0 |G d : H/	H, H 1 |G D : H 1 /
					A;d;D : H 1
	(Imm) H|G i : c at s/{s}	(Inst) (t, C) ≤ (H(x)) H| S, L x : t/ locations(t) L |= C
			(Pair)
	(At)				(Comm)
	H at s| S, L	e : t/	s ∈ S	H| S, L	e : t at s/	L |= s s
	H| S, L	e at s : t/		H| S, L

e : t at s / ∪ {s } (Node) H, x : t, H 1 | S , L D : H 1 / 1 H, x : t, H 1 | S , L e : t/ 2 S = S ∪ {δ 1 , . . . , δ n

  : H 1 / 1 H|G D 2 : H 2 / 2 H|G D 1 and D 2 : H 1 , H 2 / 1 ∪ 2 |G D 2 : H 2 / 2 H|G let D 1 in D 2 : H 2 / 1 ∪ 2

	)	(App)
	H|G e : t/	H|G f : t 1 -1 → t 2 / 2	H|G e : t 1 / 3
	H|G x = e : [t/x]/	H|G x = f (e) : [t 2 /x]/ 1 ∪ 2 ∪ 3
	(And) H|G D 1 (Let) H|G D 1 : H 1 / 1 H, H 1 (If)
		H|G e : c at s/
	H|G D 1 : H / 1	H|G D

2 : H / 2 L |= {s s |s ∈ 1 ∪ 2 } H|G if e then D 1 else D 2 : H / ∪ 1 ∪ 2

Figure 6: Spacial type system INRIA

  H|G e 1 : t 1 / 1 /T 1 H|G e 2 : t 2 / 2 /T 2 H|G (e 1 , e 2 ) :t 1 × t 2 / 1 ∪ 2 /T 1 T 2

			L	x : t/ locations(t)/∅
	(Pair-C)
	(At-C)	(Comm-C)
	H at A|G e : t/ /T	H| S, L	e : t at s/ /T	L |= s s
	H|G e at A : t/ /T	H| S, L

e : t at s / ∪ {s }/T {s n → s } Figure 8: Refined type system, with communication channels (expressions)

•

  H|G e : t/ iff ∃ 1 , 2 , t 1 , t 2 such that H|G e 1 : t 1 / 1 , H|G e 2 : t 2 / 2 , t = t 1 × t 2 and = 1 ∪ 2 . iff ∃v 1 , v 2 , e 1 , e 2 such that v = (v 1 , v 2 ), e = (e 1 , e 2 ), R e 1

	• R (e 1 , e 2 ) v 1 -→ e 1 and R e 2	v 2

v

-→ e

  ∃H 1 , 11 , 12 such that 1 = 11 ∪ 12 , H.[y : t 1 ]|G D 1 : H 1 / 11 and H.[y : t 1 ].H 1 |G e 1 : t 2 / 12 .

  i , then the semantical relation between e and e i is established by evaluating e i in a reaction environment emitted by D 1 and . . . and D n . This equivalence relation depends upon the spacial type of e. Lemma 6 (Projection correction (expressions)). For all H, e, v, e , t, , T , e i , D i , R, if R e H|G e : t/ /T and ∀i, H|G e : t/ /T A i =⇒ e i /D i , then for all R p R p , there exists v i , e i , D p , D p , R p such that D p = D 1 and . . . and D n , D p , dom(R p ) = {c n |∃A, A , A Proof. By induction on the structure of the typing derivation tree of e. Let H, e, v, e , t, , T , e i , D i , R, R p , such R e =⇒ e i /D i Case of rule Imm: e = i. Then, R i

	such that R
	R p v i	D p t v. A i	R p --→ n → A ∈ T }. R p , R p	e i	v i -→ e i and
			A i

v -→ e , H ∼ = v -→ e , H|G e : t/ /T and ∀i, H|G e : t/ /T i -→ i. For all H, G, s, A, H|G i : c at s/{s}/∅ A =⇒ i/ . Let D p = and R p = ∅. For all R p , R i

RR n°6378

Acknowledgments. We gratefully thank Jean-Pierre Talpin for constructive discussions.

-H|G e : t 1 / 3 /T 3 , -H = [t 2 /x].

• Let {A 1 , . . . , A n } = S. For all i,

-From rules Inst-P-Here and Node-P, f = f A i and f A i is defined by

-By application of lemma 6, there exists v i , e i , D e , D e , R e , D e = D 1 and . . . and D n ,

-From the fact that the renamings of channels are monotone, the application of the semantics on each projection keeps the consistency of the communicated values between each projected node and its projected instantiation.

INRIA


St Éphane Durand
email: stephane.durand@inria.fr

Federica Garin
email: federica.garin@inria.fr

Bruno Gaujal
email: bruno.gaujal@inria.fr

Efficiency of Best Response Dynamics with High Playing Rates in Potential Games *

Keywords: F.7 [Theory of Computation]: Theory and algorithms for application domains-Algorithmic game theory and mechanism design Potential Games, Best Response Dynamics, Distributed Algorithms, Markov Chains

In this paper we design and analyze distributed best response dynamics to compute Nash equilibria in potential games. This algorithm uses local Poisson clocks for each player and does not rely on the usual but unrealistic assumption that players take no time to compute their best response. If this time (denoted δ) is taken into account, distributed best response dynamics (BRD) may suffer from overlaps: one player starts to play while another player has not changed its strategy yet. An overlap may lead to a decrease of the potential but we can show that they do not jeopardize eventual convergence to a Nash equilibrium. Our main result is to use a Markovian approach to show that the average execution time of the algorithm E[TBRD] can be bounded: 2δn log n/ log log n + O(n) ≤ E[TBRD] ≤ 4e γ δn log n/ log log n+O(n), where γ is the Euler constant, n is the number of players and δ is the time taken by one player to compute its best response. These bounds are obtained by using an asymptotically optimal playing rate λ. Our analytic bound shows that 2δ λ = log log n -log C, where C is a constant. This induces a large probability of overlap (p = 1 -C/ log 1/2 n). In practice, numerical simulations also show that using high playing rates is efficient, with an optimal probability of overlap popt ≈ 0.78, for n up to 250. This shows that best response dynamics are unexpectedly efficient to compute Nash equilibria, even in a distributed setting.

POTENTIAL GAMES

A game G def = G(N , A, u) is a triplet consisting of: A finite set of players N = {1, . . . , n}; A finite set A of actions (or pure strategies) ; The set of actions profiles or states of the game is A n and the players' payoff functions u k : A n → R.

The best response correspondence BR k (x) is the set of actions maximizing the payoff for player k under state x:

BR k (x) def = arg max α k ∈A u k (α k ; x -k ) .
A Nash equilibrium (Nash equilibrium (NE)) is a fixed point of this correspondence, i.e., a profile x * such that x * k ∈ BR k (x * ) for every player k.

Definition 1 (Potential games).

A game is a (best response) potential game [START_REF] Voorneveld | Best-response potential games[END_REF] if there exists a function Φ :

A n → R such that for any player k and action profile x

BR k (x) = arg max α k ∈A Φ(α k , x -k ) .
The main property of best response in potential games is that each time a player plays its best response, the potential increases. This implies that repeating this for all players will eventually lead to a configuration where the potential cannot be improved, hence a Nash Equilibrium.

EXECUTION TIME OF DISTRIBUTED BEST RESPONSE DYNAMICS

We consider an algorithmic version of Best Response called Best Response Dynamics (BRD) in the following.

A revision sequence is an infinite sequence of players chosen according to some rule. The round robin sequence, i.e., the cyclic sequence 1, [START_REF] Durand | Complexity and optimality of the best response algorithm in random potential games[END_REF]. Here, we consider a distributed version of the best response dynamics, given in Algorithm 1, where players act according to individual Poisson clocks with rate λ/n.

• • • , n, 1, • • • , n, 1, • • • has been studied in
Let δ be the time taken by any player to compute its best response. If two players become active during a time interval smaller than δ, their plays overlap: one player starts to play before the previous one has yet updated its state. This implies that the best response of the second player may be corrupted. This may lead to a potential decrease. Convergence to a Nash equilibrium still holds with probability one: Using the Borel Cantelli Lemma, a sequence of plays of arbitrary length and with no overlap will eventually occur. Of course it may take a very long time before such an event occurs. We show next that this is not the case. On the contrary, the average execution time is surprisingly small: convergence occurs before all players have played 4 times. Theorem 1. Under rate λ, the overlap probability is p = 1 -e -δλ and the expected execution time satisfies

E[TBRD] ≤ e λp n log(n) + C 1 -p n + n p + n 2p-1 p(1 -p) ,
where C is a constant, and E[TBRD] ≥ n log(n)/λ. Choosing an adequate global playing rate 2δ λ = log(log(n)) -log(C), inducing an overlap probability p = 1 -

C log 1/2 (n) , the average execution time of BRD satisfies 2 δn log(n) log(log(n)) (1+o(1)) ≤ E[TBRD] ≤ 4e γ δn log(n) log(log(n)) (1+o(1))
where γ is the Euler constant .

MARKOVIAN APPROXIMATION

The direct analysis of the behavior of BRD is difficult because, over time, more and more states have been visited by the algorithm. Thus, its behavior is non-homogeneous in time. We introduce two successive simplifications whose behavior can be compared (using two different coupling schemes) with the best response dynamics over a potential game with n players.

Under the Intersection-Free approximation (IFA), every time a new player who is not satisfied (in other words, a player not in L) has to compute its best response in a state (say x), it compares Φ(x) with the potential of its other strategies, as for the original BRD. In IFA, however, we will assume that none of these states have yet been visited during the previous steps of the algorithm. Under BRD, there is a chance that some of these states have already been visited. Under BRD, the potentials of all states is generated first, and the game is played given these values of the potentials. Under IFA, each time a state is (re)visited, its iid potential is (re)generated. Using an appropriate coupling between BRD and IFA, the expected convergence time of brd (ET brd ) and of ifa (ET if a ) verify: ET brd ≤ c1ET if a , for some constant c1.

We next construct the restart approximation (RST) by considering that whenever an overlap occurs, the potential is reset to a uniform potential in [0, 1], disregarding the previously obtained potentials. In other words, we restart from step 0. Again a coupling technique can be used to show that the time to reach a Nash equilibrium under RST is stochastically larger than under IFA.

The construction of the restart approximation ensures that the future behavior of the system only depends on its current state, namely the current potential and the list of satisfied players. Therefore, the convergence time of (RST) can be evaluated by modeling its behavior by a Markov chain over a hybrid state space (with a continuous and a discrete component). The expected hitting time of a Nash equilibrium for this Markov chain satisfies a Poisson equation. This Poisson equation can be transformed into an ordinary differential equation with an implicit initial condition whose solution can be computed in integral form. The derivation of the asymptotic behavior of this solution in n (the number of players) leads to Theorem 1.

SENSITIVITY TO λ

We have simulated the behavior of BRD over a large number of potential games whose potentials are generated uniformly over all possible potentials. These simulations are carried to assess tightness of our bound and to study the sensitivity of BRD to the value of its unique parameter λ. Our experiments show that λopt does not depend on n: for any n, 1/δλopt ≈ 0.63 implying popt ≈ 0.77. However it was very hard to get a good precision on λopt. Even if these experiments took several days of computations over a modern desktop computer, with 1000 runs for each couple (n, λ), our accuracy on the optimal value of λopt(n) is between 5% and 10%, depending on the value of n.

Algorithm 1 :

 1 Distributed BRD (for player k) 1 Input: Game utilities (u k (•)); Initial state (x := x(0)); 2 Initialize t := 0; List of satisfied players L := ∅; 3 Local clock, ticking w.r.t. a Poisson process with rate λ/n; 4 while size(L) = n do 5 On each tick of the local clock 6 if k ∈ L then 7 if x k = BR k (x) then 8 L := L ∪ {k} 9 else 10 x k := BR k (x); L := {k} Randomization. In the following we will randomize over the potential games over which Best Response Dynamics (BRD) is used. Since the behavior of BRD only depends on the potential function, we randomize directly over the potential Φ.

Figure 1 :

 1 Figure 1: Mean execution time of distributed BRD with 100 players (with 95% confidence intervals), as a function of the expected time between two plays (inverse of the playing rate), in log-log scale. Comparison with the analytic asymptotic bound

* This work has been partially supported by the LabEx PERSYVAL-Lab