Gwenaël Delaval
email: gwenael.delaval@inria.fr

Alain Girault
email: alain.girault@inria.fr

Marc Pouzet
email: marc.pouzet@lri.fr

A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs

Keywords: D.1.3 [Programming Techniques]: Concurrent Programming-Distributed programming; D.3.2 [Programming Languages]: Languages Classifications-Concurrent, distributed, and parallel languages Synchronous programming, distribution, type systems, functional programming

We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architectural and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. We also present a distributed semantics to formalize the distributed execution of synchronous programs. Our second contribution is to provide a type system, in order to infer the localization of non-annotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. Our third contribution is to provide a type-directed projection operation to obtain automatically, from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been fully implemented in the compiler of an existing synchronous data-flow programming language.

Motivations

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 the 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 de-Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. LCTES'08, June 12-13, 2008, Tucson, Arizona, USA. Copyright c 2008 ACM 978-1-60558-104-0/08/06. . . $5.00 signers. 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. Yet, most embedded systems are composed of several computing resources (named "locations"), for 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 parallelism. This paper addresses the problem of mapping the functional parallelism onto the execution one, in a modular way. We focus on distributed systems implemented as networks of deterministic processes communicating with FIFOs.

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

Our paper is organized as follows: Section 2 gives an overview of the context, and motivates our method through some examples and one application. Section 3 presents the semantics and the formalization of the spatial type system. Section 4 presents the projection operation, which is our third contribution. Finally, related work and discussion about the solution will be exposed in Section 5.

Overview 2.1 Distribution of Synchronous Dataflow Programs

Synchronous dataflow languages, such as Lustre, Signal, or Lucid Synchrone [START_REF] Benveniste | The synchronous languages twelve years later[END_REF], manipulate infinite streams of values as primitive values: the notation 1 represents the infinite stream 1, 1, ..., while int stands for the type of infinite streams of integers. For any stream x, we note xi its ith value. In this context, functions (called nodes hereafter) are stream functions: e.g., int → int is the type of functions from integer streams to integer streams. Combinatorial functions are implicitly lifted to apply pointwise to their arguments: e.g., if x = (xi)i∈IN and y = (yi)i∈IN are two integer streams, then (x + y) = (xi + yi)i∈IN . Moreover, we use a unitary delay, noted fby, such that (x fby y)i = x0 if i = 0 and yi-1 otherwise.

Such a program is classically compiled into a single 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. Our contribution is to extend this classical compilation scheme to a distributed framework: the result of the compilation of a distributed system will consist of n functions fi, one for each location i, which will compute the values of outputs, communication channels, and lo-cal state, from the values of inputs, other incoming communication channels, and the current local state.

Language-based Distribution

We address functional distribution, not achieved for the sake of performance but because the system is intrinsically distributed. 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, because of problems such as the scheduling of communications or the type consistency of the communicated data. The usual method, using architecture languages like AADL [START_REF]Architecture analysis & design language[END_REF], involves 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 conflicts between architectural and functional modularity can occur, it is less error-prone and more efficient to define the system as a whole, together with architectural annotations. Our first contribution is to provide language primitives to allow the programmer to describe the 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: a location declaration 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.3 a projection operation which produces, for each symbolic name, a single non-distributed synchronous program to be executed at the physical location represented by this symbolic name.

The syntax for declaring the physical location A is loc A. The existence of a communication link from A to B is declared 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 ability to communicate 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 composing its subterms) will be located at A. The programmer does not need to express the localization of every value. Our second contribution is to provide a type and effects system [START_REF] Talpin | Polymorphic type, region and effect inference[END_REF] whose double function is to check the validity of the localization expressed w.r.t. the architecture, 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 place inside the code. The technical expression of communications is left to the further phase of integration on actual architecture: our method only deals with inferring the 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). From a programmer's point of view, this choice is a compromise between no control at all (communications are possible everywhere) and absolute control (the programmer expresses every communication).

A Spatial Type System for Automatic Distribution

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. We provide a special type system dedicated to the distributed execution of the program, as an analysis provided to the programmer to help him ensure the consistency of the distribution specification. We call it a spatial type system and, when clear from context, we shall simply refer to it as a type system. This spatial type system describes the localization of streams, and a type-directed approach is followed to achieve code distribution. 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.

The other 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), spatial types will be inferred from the available spatial annotations in the source. The spatial type system also checks the consistency of these annotations with the given architecture. Spatial 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, spatial types will be inferred for each defined node modularly.

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 spatial 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 spatial type is a set: it is the set of locations where the stream will be available. The spatial type of a node f is written ti -S → to, where ti and to are respectively the spatial 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 ti and to'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 is a sequence of three nodes f1, f2 and f3, each assumed to be of spatial type ∀δ.c at δ -{δ} → c at δ. f1 and f3 are localized by the programmer, respectively on A and B. f2 is not explicitly 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 spatial type c at A -{A, B} → c at B. As the localization of computations has to be done modularly, a spatial 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 Furthermore, it can be noted here that node g cannot be used within a located declaration. The following node will be rejected by our type system: node g'(m,x) = y with y = g(m,x) at A

The second 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 one location, and then g to the result of the first application at another location. This example shows also how a node can be defined with local locations for more modularity. 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 spatial 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, or 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 in these two ways (assuming the existence of two nodes f and g, both of spatial type ∀δ.c at δ -{δ} → c at δ): y1 = h (f at A,g at A,x1) and y2 = h (f at A,g at 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, unlike 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 performance, 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 several functionalities [START_REF]Software-defined radio -basics and evolution to cognitive radio[END_REF]: each of these functionalities must be engineered separately, and then integrated together. Then, there is a conflict between distribution and functional modularity issues.

Let us study the case of a multichannel reception system that supports the two mobile standards GSM and UMTS: the former involves a filter for 1800 MHz frequencies, a GMSK demodulator, and a CRC / convolutional error correction module, while the latter 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 by the channel. From this value, a function gsm_or_umts (noted g on Figure 1 for the sake of brevity), local at GPP, computes what channel will be used at next instant. In this figure, each location is graphically represented by a gray box. 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. Firstly, 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 correctness of the system. This situation compromises the modularity of the system. Secondly, 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 suggests 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.

The code below implements this multichannel software radio, with our extended language. The architecture consists of three locations, FPGA, DSP, and GPP, completely connected: 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)

This implementation strictly 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 spatial 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 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 spatial type of x is FPGA, and the one of y is GPP. As a result, the spatial type of the node multichannel_sdr is:

(c at FPGA) -{FPGA, DSP, GPP} → (c at GPP)

Formalization

We first define a synchronous dataflow core language (Section 3.1), and give 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 that react w.r.t. 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]. The distributed semantics allows us to give a meaning to location annotations. A spatial type system is then presented (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. An expression e may be an immediate value (i), a variable (x), a pair construction (e, e ; pair destruction can be performed by pattern definitions), a binary combinatorial operation (op(e, e), where op can be (+), (-),. . . ), an initialized delay (e fby e), or an expression annotated with an explicit location s (e at s).

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.

= R ′ 1 .R ′ 2 . . . such that: R d , Ri, Ro ⊢ D Ro --→ D ′ Si ⊢ A;d;D ′ : So Ri.Si ⊢ A;d;D : Ro.So
The rules for the reaction predicates are given in Figure 2.

(IMM) R ⊢ i i -→ i (INST) R, [v/x] ⊢ x v -→ x (FBY) R ⊢ e 1 v 1 --→ e ′ 1 R ⊢ e 2 v 2 --→ e ′ 2 R ⊢ e 1 fby e 2 v 1 --→ v 2 fby e ′ 2 (OP) R ⊢ e 1 i 1 -→ e ′ 1 R ⊢ e 2 i 2 -→ e ′ 2 i = op(i 1 , i 2 ) R ⊢ op(e 1 , e 2 ) i -→ op(e ′ 1 , e ′ 2 ) (PAIR) R ⊢ e 1 v 1 → e ′ 1 R ⊢ e 2 v 2 → e ′ 2 R ⊢ (e 1 , e 2 ) (v 1 ,v 2 ) -----→ (e ′ 1 , e ′ 2 ) (AT) R ⊢ e v ′ → e ′ R ⊢ e at s v → e ′ at s (DEF) R ⊢ e (v 1 ,...,vn) -------→ e ′ R ⊢ (x 1 , . . . , xn) = e [v i /x i ] -----→ (x 1 , . . . , xn) = e ′ (APP) R(f ) = λp.e with D R ⊢ p ′ = e and p = e ′ and D R ′ --→ D ′ R ⊢ p ′ = f (e ′ ) R ′ --→ D ′ (AND) R, R 2 ⊢ D 1 R 1 --→ D ′ 1 R, R 1 ⊢ D 2 R 2 --→ D ′ 2 R ⊢ D 1 and D 2 R 1 ,R 2 ----→ 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 Figure 2. Centralized synchronous semantics.
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 e1 fby e2 emits the first value of e1, then the previous value of e2 (rule FBY). An operation is performed pointwisely on immediate values (rule OP). Pair construction follow classical rules (rule PAIR). Locations are not taken into account here (rule AT): annotations added by the programmer do not alter the centralized semantics of the program (i.e., its functionality). An equation p = e emits the reaction environment defining the variables contained in p (rule DEF). A sequential function application is replaced by its body and argument definition (rule APP). Parallel equations are mutually recursive (rule AND). 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 spatialized execution: the values v emitted by expressions are now distributed values, i.e., they are annotated with location information stating how these values are distributed on the architecture: Several values can represent the same distributed value:

v ::= lv at A | (v, v) | Λ δ.
(lv1, lv2) at A = (lv1 at A, lv2 at A)

v1 = v′ 1 v2 = v′ 2 (v1, v2) = (v ′ 1 , v′
2 ) These equalities mean that a local pair (1, 2), localized on the site A, can indifferently be denoted by the distributed values (1, 2) at A or (1 at A, 2 at A). A distributed pair can be, for example, the pair (1 at A, 2 at B) : the first compound is located on A, and the second on B.

The operator loc(•) gathers the set of locations from a distributed value:

loc(i at s) = {s} loc((v1, v2) at s) = loc(v1) ∪ loc(v2)
The operator | • | erases annotations from a distributed value to get a centralized value, and extends straightforwardly to reaction environments:

|i at s| = i |(v1, v2) at s| = (|v1|, |v2|)
The distributed semantics is defined by means of two predicates refined from their centralized versions. R ℓ e1 v -→ e2 states that in the distributed reaction environment R, the expression e1 emits the distributed value v and rewrites into e2. ℓ represents the set of locations involved in the computation of v. The predicate for declarations is defined as well.

We denote by S the set of declared constant locations, and by L ⊆ S × S the set of declared communication links. The relation L defines the ability to communicate, 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, we assume that the architecture graph G is global for subsequent semantic rules. The annotated execution of a program P is Ŝi P : Ŝo, meaning that under a sequence of input environments Ŝi = R1. R2 . . ., the program P = A;d;D produces a sequence of output environments Ŝo = R′ 1 . R′ 2 . . .: The rules for the predicates R ℓ e1 v -→ e2 and R ℓ D1

∅, ∅ ⊢ A : G Rd , Ri, Ro
R′ -→ D2 are given in Figure 3. 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 APP). 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 if a program reacts with the distributed semantics, then it reacts with the centralized one and produces the same values.

Lemma 1. 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 ′ .

Spatial Types

For the sake of clarity, we first present a simplified version of the type system. For projection, we refine this first version to take communication channels into account (Section 4). The syntax of spatial type expressions is: . . , sn ⊲ s ′ n } H is the spatial typing environments. H at A denotes a located environment, i.e., a typing environment from which every spatial type will be forced to represent a value entirely located on A.

(IMM) R ℓ i i at s ---→ i (COMM) R ℓ e dv at s -----→ e ′ (s, s ′ ) ∈ L R ℓ∪{s ′ } e dv[s ′ /s] at s ′ ---------→ e ′ (INST) R, [v/x] loc(v) x v -→ x (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 i 1 at A -----→ e ′ 1 R ℓ 2 e 2 i 2 at A -----→ e ′ 2 i = op(i 1 , i 2 ) R ℓ 1 ∪ℓ 2 op(e 1 , e 2 ) i at A ----→ op(e ′ 1 , e ′ 2 )
(PAIR)

R ℓ 1 e 1 dv 1 at s 1 ------→ e ′ 1 R ℓ 2 e 2 dv 2 at s 2 ------→ e ′ 2 R ℓ 1 ∪ℓ 2 (e 1 , e 2 )
(dv

1 at s 1 ,dv 2 at s 2 ) at s 1 ⊔s 2 --------------------→ (e ′ 1 , e ′ 2 ) (AT) R {s} e v -→ e ′
R {s} e at s v -→ e ′ at s

(DEF) R ℓ e (v 1 ,...,vn) -------→ e ′ R ℓ (x 1 , . . . , xn) = e [v i /x i ] -----→ (x 1 , . . . , xn) = e ′ (APP) R(f ) = Λδ 1 , . . . ,
--→ D ′ R ℓ p ′ = 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 Figure 3. Distributed synchronous semantics.
We distinguish spatial type schemes (σ), which can be quantified, from simple spatial 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 spatial type can be either a node type (tℓ → t), a pair type (t × t), or a located type (tc at s). A located type can be either a stream type (c, such as boolean, integer, etc.), a type variable (α), a local function (tc → tc), or a local pair type (tc × tc). ℓ denotes sets of locations. A location is either a location variable δ, or a location A.

C is a set of constraints between locations. A constraint s1 ⊲ s2 means that either s1 = s2, or there exists a communication link from s1 to s2. Conversely, a declaration of communications links L leads to the set of constraints constr(L) = {s ⊲ s ′ |(s, s ′ ) ∈ L}.

A value of spatial type tc at s is a value located on s. A value of spatial type t1ℓ → t2 is a node whose input is of spatial type t1, whose output is of spatial type t2, and whose computation involves the set of locations ℓ. The following equalities stand:

(tc1 × tc2) at s = (tc1 at s) × (tc2 at s) (tc1 → tc2) at s = (tc1 at s) -{s} → (tc2 at s) t1 = t ′ 1 t2 = t ′ 2 (t1 × t2) = (t ′ 1 × t ′ 2 ) t1 = t ′ 1 t2 = t ′ 2 t1 -ℓ → t2 = t ′ 1 -ℓ → t ′ 2
The instantiation mechanism ensures the localization of a type instantiated from a located environment:

(t[tc1/α1, . . . , tcn/αn, s/δ], C[s1/δ1, . . . , sm/δm]) ≤ ∀α1 . . . αn∀δ1 . . . δm : C.t

(tc at s, C) ≤ (H at s)(x) ⇔ (tc at s, C) ≤ H(x)
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 spatial type system, we introduce the following notations:

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

locations(t1 × t2) = locations(t1) ∪ locations(t2) locations(t1 -ℓ → t2) = ℓ locations(tc at s) = {s}
The top-level declaration of a program is typed from the initial environment H0, defined as:

H0 =
• fby • : ∀α.∀δ.α at δ × α at δ -{δ} → α at δ, (+) : ∀δ.c at δ × c at δ -{δ} → c at δ, . . . Our spatial type system is formally defined by the inference rules shown in Figure 4. 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 spatial type of a node consists of the spatial types of its inputs, the computed expression, and the set of locations involved in this computation (rule NODE). The type of a node is generalized w.r.t. the set of locations and links introduced by this architecture.

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 declarations involve, for their computations, the union of the sets and of locations involved in the computation of their compounds (rule AND). 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 D1 and D2 must be accessible from s (rule IF).

′ /ℓ ∪ {s ′ } (NODE) H, x i : t i , H 1 | S ′ , L ′ ⊢ D : H 1 /ℓ 1 H, x i : t i , H 1 | S ′ , L ′ ⊢ e : t/ℓ 2 S ′ = S ∪ {δ 1 , . . . , δp} L ′ ⊆ L ∪ ({δ 1 , . . . , δp} × S) ∪ (S × {δ 1 , . . . , δp}) {α 1 , . . . , αm} = FTV(t) -FTV(H) C = constr(L ′ \ L) σ = ∀α 1 , . . . , αm.∀δ 1 , . . . , δp : C.(t 1 × . . . × tn) -ℓ 1 ∪ ℓ 2 → t H|G ⊢ node f [δ 1 , . . . , δp](x 1 , . . . , xn) = e with D : [σ/f ]/ℓ 1 ∪ ℓ 2 (APP) H|G ⊢ f : t -ℓ 1 → (t ′ 1 × . . . × t ′ n )/ℓ 2 H|G ⊢ e : t/ℓ 3 H|G ⊢ (x 1 , . . . , xn) = f (e) : [t ′ 1 /x 1 , . . . , t ′ n /xn]/ℓ 1 ∪ ℓ 2 ∪ ℓ 3 (AND) H|G ⊢ D 1 : H 1 /ℓ 1 H|G ⊢ D 2 : H 2 /ℓ 2 H|G ⊢ D 1 and D 2 : H 1 , H 2 /ℓ 1 ∪ ℓ 2 (IF)
H|G ⊢ e : c at s/ℓ H|G ⊢ D 1 : We denote by v : t the fact that the distributed value v has spatial type t: lv at s : c at s v1 : t1 v2 : t2 (v1, v2) : t1 × t2

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
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 our type system, then there exists a spatialized execution such that the distributed values of this execution are equal to the centralized ones. The types are preserved by this spatial execution. The proof is omitted for lack of space. Theorem 1 (Soundness). 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 ′ .

Distribution 4.1 Principle

Once programs have been typed, every expression is annotated with a location that specifies where it has to be computed. Communica-tions are inserted when a value is 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 the node f of Section 2.2 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 on f_A (named here c_y, holding the value y computed on A and used on B), together with an additional input on f_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 5. 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) = (⊥,c4,c5) if c1 then (y,c4) = channel(⊥,gmsk,⊥,⊥,c2) else (y,c5) = channel(⊥,qpsk,⊥,⊥,c3)

Figure 5. Result of the projection on DSP

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 will use a refined version of the type system, allowing the inference of communication channels.

A channel is a location pair associated with a name, noted A1 c → A2: c is the name of the channel, A1 its source location, and A2 its destination location. The set of channel names is ordered by <, so as to keep consistency of inputs and outputs added, from the node definition to node instances. T denotes sequences of channels. The concatenation of two sequences of channels, noted T1, T2, is defined iff channel names in T1 and T2 are disjoint. We denote by ǫ the empty sequence.

We note dom(T ) the set of channel names of T . T ′ ∼ = T means that the sequences T and T ′ are equal, modulo channel renaming. This renaming allows the multiple instanciations of node comprising communications.

T ′ ∼ = T ⇔ T ′ = T [c ′
1 /c1,...,c ′ n /cn] where {c1,...,cn} = dom(T ) 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 spatial 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 c in an environment channel will be introduced as the variable c 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:

     ∅ ↑ A = ∅ ([A1 c → A2], T ) ↑ A = [A1 c → A2], (T ↑ A) if A1 = A (T ↑ A) else,      ∅ ↓ A = ∅ ([A1 c → A2], T ) ↓ A = [A1 c → A], (T ↓ A) if A2 = A (T ↓ A)
else.

The projection rules are given in Figures 6 and7. Channels are used at communication points. If an expression e is sent from A to A ′ through the channel A c → A ′ , then:

• 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 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); and 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). H|G ⊢ e 1 : The global meaning of a distributed program is then defined by the parallelization of its projected declarations.

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 ,
H|G ⊢ f : t -ℓ 1 /T 1 → (t ′ 1 × . . . × t ′ n )/ℓ 2 /T 2 A =⇒ f ′ /D 1 H|G ⊢ e : t/ℓ 3 /T 3 A =⇒ e ′ /D 2 T ′ 1 ∼ = T 1 T ′ 1 ↑ A = [A c 1 → A 1 , . . . , A cm → Am] T ′ 1 ↓ A = [A ′
We note S = {A1, . . . , An} 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 defined by: D1 and . . . and Dn where ∀i, H|G ⊢ D : H ′ /ℓ/T A i

=⇒ Di

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 v1 v ′ 2 A t 2 v2 (v ′ 1 , v ′ 2 ) A t
′ , D, D ′ , ℓ, T , Di, R, R ′ , if R ⊢ D R ′ -→ D ′ ,

Discussion

Implementation

The spatial type system presented in Section 3.4 relies on a subtyping mechanism. It corresponds to the case where communications can occur anywhere in the code. This situation raises two problems. Firstly, the implementation of type systems with subtyping mechanism is costly: usual algorithms rely on the systematic application of the subtyping rule. Secondly, this choice leads to a situation where the programmer has no control over 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 refine our type system in order to address these two problems.

We restrain communicated values to be variables introduced by equations (x = e). Thus, in the program of 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 to instantiation points. This refined type system, as well as the projection operation presented in Section 4, have been implemented in the Lucid Synchrone compiler [START_REF]Lucid synchrone[END_REF]. The independence of the method w.r.t. other analysis allowed this implementation to be quite modular, implying very few modifications within the rest of the compiler. The implementation consists to generate distribution constraints, which are resolved modularly for each node. We implemented a naive resolution algorithm, which can easily be replaced by any existing distribution algorithm, taking into account efficiency issues (for example, the AAA method of SynDex [START_REF] Sorel | SynDEx: System-level cad software for optimizing distributed real-time embedded systems[END_REF]). This implementation has been tested on the software-defined radio example, which is in its actual size composed of 150 lines of code, spread out into 25 Lucid Synchrone nodes. We have tested our automatic distribution algorithm on a benchmark suite composed of programs of few hundred of lines from the current Lucid Synchrone release. This point is a good indication of the flexibility of the extension proposed, allowing the distribution of programs not primarily designed with distribution in mind. The scalability of this method is a direct outcome of the use of a type system aiming at modular distribution; it has been also applied on an ad hoc example composed of 10 Lucid Synchrone nodes, comprising each 60 equations.

Related Work

Various solutions have emerged in order to use synchronous languages for the design of distributed systems. Some of them operate on a compiled model of the program, by "coloring" atomic instructions with localization information, inferred from input and output 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 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 soundness 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 spatial 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 [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] can be given to our language, the semantic 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. This last approach, as well as our projection operation, can be compared with slicing methods [START_REF] Ward | Slicing as a program transformation[END_REF], as they consists in extracting specific parts of a global program. 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. Our approach can be compared with automatic partitioning: the J-Orchestra system [START_REF] Liogkas | Automatic partitioning: A promising approach to prototyping ubiquitous computing applications[END_REF] allows the user to assign network sites to classes of Java programs. Then, this automatic partitioning system transform the initial program into a distributed one, taking into account distant or direct references. This last approach differs with our by the fact that we integrate the distribution constructs within our language, which allows relying distribution on semantical basis. 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. These two languages 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 spatial 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 spatially 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 a synchronous dataflow compiler [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.

Figure 1 .

 1 Figure 1. Functional model of a multichannel software radio.

3. 1

 1 The Core Language Syntax P ::= A;d;D A ::= A;A | loc A | link A to A s ::= δ | A d ::= node f [δ1, . . . , δn](p) = e with D | d;d D ::= p = e | p = x(e) | D and D | if e then D else D p ::= p, p | x e ::= i | x | (e, e) | op(e, e) | e fby e | e at s 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](p) = e with D). Definitions D define patterns of variables p, and are either single equations (p = e), definitions naming the result of an application (p = x(e)), parallel declarations (D and D), or alternative declarations (if e then D else D).

  v ::= i | (v, v) | λx.e with D R ::= [v1/x1, . . . , vn/xn] s.t. ∀i = j, xi = xj S ::= R1.R2 . . . A reaction environment R associates values to names and assumes that names are pairwise distinct. S denotes a sequence of reaction environments. Given a sequence d of node definitions node fi[ δi](xi) = ei with Di, an initial global environment R d is defined, holding λ-values of each fi. This initial environment will be given as input of the main program. R d = [λx1.e1 with D1/f1, . . . , λxn.en with Dn/fn] The synchronous centralized semantics is defined by means of two reaction predicates. R ⊢ e1 v -→ e2 states that in the reaction environment R, the expression e1 emits the value v and rewrites into the new expression e2. The predicate R ⊢ D1 R ′ -→ D2 states that in the reaction environment R, the declaration D1 defines the reaction environment R ′ and rewrites into D2. The centralized execution of a program P is denoted Si ⊢ P : So, meaning that under a sequence of input environments Si = R1.R2 . . ., the program P = A;d;D produces a sequence of output environments So

  λx.e with D lv ::= i | (lv, lv) R ::= [v1/x1, . . . , vn/xn] s.t. ∀i = j, xi = xj Ŝ ::= R1. R2. . . . G ::= S, LA distributed value v is either a local value lv, localized on the site A (lv at A), a distributed pair (v, v), or a node. A sequence of location parameters δ is associated to nodes. A local value is either an immediate value i, or a local pair (lv, lv). R denotes a distributed reaction environment, and Ŝ a sequence of distributed environments. G denotes an architectural graphs composed of a set of locations S, and a set of communcation links L ⊆ S × S.

  ℓ D Ro --→ D ′ Ŝi A;d;D ′ : Ŝo Ri. Ŝi A;d;D : Ro. Ŝo where Rd is defined from the sequence of node definitions d = node fi[ δi](xi) = ei with Di as: Rd = [Λ δ1.λx1.e1 with D1/f1, . . . , Λ δn.λxn.en with Dn/fn]

σ

  ::= ∀α1, . . . , αn.∀δ1, . . . , δn : C.t t ::= tℓ → t | t × t | tc at s tc ::= c | α | tc → tc | tc × tc ℓ ::= {s1, . . . , sn} s ::= δ | A H ::= H at A | [x1 : σ1, . . . , xn : σn] C ::= {s1 ⊲ s ′ 1 , .

Figure 4 .

 4 Figure 4. Spatial type system.

(

  IMM-P)H|G ⊢ i : c at s/{s}/ǫA =⇒ i/ǫ (INST-P) (t, C) ≤ (H(x)) L |= C H|G ⊢ x : t/ℓ/ǫ A =⇒ x A /ǫ (AT-P) H at A|G ⊢ D : H ′ /ℓ/T A =⇒ D ′ H|G ⊢ D at A : H ′ /ℓ/T A =⇒ D ′(SUPPR-P) A ∈ ℓ H|G ⊢ e : t/ℓ/T A =⇒ ⊥/ǫ (COMM-P-FROM) H| S, L ⊢ e : tc at A/ℓ/T A =⇒ e ′ /D L |= A ⊲ s ′ H| S, L ⊢ e : tc at s ′ /ℓ ∪ {s ′ }/T, [A n → s ′ ] A =⇒ ⊥/D and cn = e ′ (COMM-P-TO) H| S, L ⊢ e : tc at s/ℓ/T A ′ =⇒ e ′ /D L |= s ⊲ A ′ H| S, L ⊢ e : tc at A ′ /ℓ ∪ {A ′ }/T,

3 A 2 ( 1 AD ′ 1 H|G ⊢ D 2 : H 2 /ℓ 2 /T 2 AD ′ 2 H|G ⊢ D 1 2 AD ′ 1 and D ′ 2 Figure 6 .

 321122221226 Figure 6. Rules for the projection operation (I).

  H|G ⊢ D : H ′ /ℓ/T and ∀i, H|G ⊢ D : H ′ /ℓ/T A i =⇒ Di, then there exists Rp, R ′ p , Dp, D ′ p such that Dp = D1 and . . . and Dn, R H Rp, Rp ⊢ Dp R ′ p --→ D ′ p , and R ′ H ′ R ′ p .

c 1 → A 1 , 1 AD ′ 1 H|G ⊢ D 2 : 2 AD ′ 2 C 1 → 2 ( 1 AD ′ 1 H|G ⊢ D 2 : 2 AD ′ 2 C 2 Figure 7 .

 1111222121122227 Figure 7. Rules for the projection operation (II).

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

•

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

  ∅, ∅ ⊢A : G H 0 |G ⊢ d : H/ℓ H, H 1 |G ⊢ D : H 1 /ℓ ′ ⊢ A;d;D : H 1 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 (DEF)H|G ⊢ e : t 1 × . . . × tn/ℓ H|G ⊢ (x 1 , . . . , xn) = e : [t 1 /x 1 , . . . , tn/xn]/ℓ

	(PROG)
	(IMM) H|G ⊢ i : c at s/{s}	(INST)	(t, C) ≤ (H(x)) H| S, L ⊢ x : t/ locations(t) L |= C
	(PAIR)
	(AT)	H at s| S, L ⊢ e : t/ℓ H| S, L ⊢ e at s : t/ℓ s ∈ S
	(COMM)	H| S, L ⊢ e : tc at s/ℓ	L |= s ⊲ s

′

H| S, L ⊢ e : tc at s

  e ′ 2 /D 1 and D 2 (DEF-P) H|G ⊢ e : t 1 × . . . × tn/ℓ/T ′ /D H|G ⊢ (x 1 , . . . , xn) = e : [t 1 /x 1 , . . . , tn/xn]/ℓ/T 1A , . . . , x nA ) = e ′ and D

	(APP-P)

A =⇒ e A =⇒ (x

  1 ×t 2 (v1, v2) We can then relate two reaction environments R and Rp w.r.t. a typing environment H: R H Rp iff ∀x ∈ dom(R), ∀A ∈ S, R(x) A H(x) Rp(xA) Theorem 2 states that the projection operation is correct, i.e., the projection of a source program D into Di (for every location Ai) defines a new target program D1 and . . . and Dn, which is semantically equivalent, taking into account spatial types' values, with the source declaration D. The proof is omitted for lack of space. Theorem 2 (Soundness of the declarations projection). For all H, H

  (NODE-P)H, x i : t i , H 1 |G ⊢ D : H 1 /ℓ 1 /T 1 A =⇒ D ′ H, x i : t i , H 1 |G ⊢ e : t/ℓ 2 /T 2 A =⇒ e ′ /De {α 1 , . . . , αm} = FTV(t) -FTV(H) σ = ∀α 1 , . . . , αm.(t 1 × . . . × tn)ℓ 1 ∪ ℓ 2 /T 1 , T 2 → t T 1 , T 2 ↑ A = [A