Thierry Gautier

Paul Le Guernic

Loïc Besnard

Jean-Pierre Talpin
email: jean-pierre.talpin@inria.fr

The Polychronous Model of Computation and Kahn Process Networks

Keywords: synchronous languages, semantics of programming languages, formal methods, synchrony and asynchrony, Kahn process networks

In 1974, Gilles Kahn defined a seminal semantic model for asynchronous dataflow programming that would then be called as the eponymous Kahn process networks (KPN) and instantiated in as many models of the so-called DPN hierarchy as domain-specific fields of information processing from digital signal processing to hybrid cyber-physical systems. Among these, synchronous programming models have had an important impact in the specific domain of embedded system design. In this paper, we consider an instance of what seems to be one of the many synchronous models of computation: polychrony, initiated by the dataflow language Signal and its multi-clock (i.e. polychronous) model of computation and, later on, CCSL (clock constraints specification language). We provide an in-depth study of its semantic relationships with respect to the original definition of KPNs and hint toward the idea of polychrony as a methodology to locally synchronize (abstractions of) globally asynchronous processes. In particular, we formally define the property, referred to as "polyendochrony", that allow to consider a given desynchronized network of synchronous Signal processes (a GALS architecture) as an implementation of a corresponding KPN model (an asynchronous network of Khan-deterministic functions). For this class of networks, we formalize the Signal program analysis and transformations that defines synchronous clusters of Signal processes of guaranteed deterministic behavior in an asynchronous network, that is, without synchronizing communications in the entire network. This definition yields a new strategy of multi-threaded code generation that is available in the open-source Polychrony toolset of the Signal language and blurs the limits between asynchronous and polychronous models of computation.

Introduction

Models of cooperating processes have a long history in both theory and practice of computer science. On the one hand, theory, process calculi describe interactions and communications between processes with algebraic laws that permit to express equivalence relations and to formally reason about process expressions. Well-known models are CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], ACP [START_REF] Bergstra | Process algebra for synchronous communication[END_REF], or the πcalculus [START_REF] Milner | A calculus of mobile processes (parts I and II)[END_REF], among many others. Other formal models of computation and communication (MoCCs) provide a central notion of process, with sometimes a real proximity with effective industrial practice. This is the case for instance of Dataflow Process Networks [START_REF] Lee | Dataflow process networks[END_REF], which are used in particular in signal processing software. Dataflow Process Networks are themselves a special class of Kahn Process Networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], which are one of the origins of the dataflow concept. The dataflow model handles general parallel asynchronous execution of processes.

On the other hand, practice, the design of embedded systems, and more specifically safety critical systems, has given rise to models based on the so-called "synchronous hypothesis" (which roughly consists in abstracting non-functional implementation details, essentially real-time, from a system under design) and to associated "synchronous languages" [START_REF] Benveniste | The synchronous approach to reactive and realtime systems[END_REF][START_REF] Benveniste | The synchronous languages twelve years later[END_REF]. In the class of synchronous languages, or close to it, the refinement-based Signal specification language [START_REF] Le Guernic | Programming realtime applications with Signal[END_REF][START_REF] Le Guernic | Polychrony for system design[END_REF][START_REF] Gamatié | Designing Embedded Systems with the SIGNAL Programming Language[END_REF], based on the "polychronous MoCC", is characterized by its ability to describe systems with multiple clocks and verifiably transform them to globally asynchronous, locally synchronous systems, prior to multi-threaded, multi-core, dynamic or static real-time scheduling analysis. The language adopts a dataflow style, but flows of data are synchronized through these clocks.

Traditionally, models of cooperating processes are classified along two aspects, which are cooperation (or composition) and communication. These aspects are qualified using two criterias: asynchronous and synchronous. In this way, Bergstra et al. [START_REF] Bergstra | Process algebra with asynchronous communication mechanisms[END_REF] situate CSP, CCS and ACP in the regime of asynchronous cooperation, while SCCS [START_REF] Milner | Calculi for synchrony and asynchrony[END_REF] follows synchronous cooperation; dataflow networks are considered as representative of asynchronous communication, while CSP, CCS or ACP obey to synchronous communication.

Considering the polychronous MoCC and the synchronized dataflow [START_REF] Le Guernic | Data-flow to von Neumann: the SIGNAL approach[END_REF] language Signal, this classification based on the distinction synchronous/asynchronous could be refined using a third criteria which is precisely "synchronized". Thus, regarding composition (cooperation), we distinguish:

• asynchronous: processes are driven by different non-synchronized clocks, each one progressing at its own pace;

• synchronized : some implicit or explicit synchronization rules are introduced (relations on communications);

• synchronous: processes are driven by a single global clock such that an "atomic" action is activated at each tick.

With this classification, CCS (for instance) would be considered as following synchronized composition rather than asynchronous one. Regarding communication (interaction) we also distinguish:

• asynchronous: asynchronous interaction indicates the fact that data transfer between processes may take an unbounded amount of time and may need an unbounded amount of memory to hold sent and unreceived values;

• synchronized : some implicit or explicit synchronization rules are introduced (bounded FIFOs may be used);

• synchronous: communication occurs in a fixed number of ticks of each participant (rendez-vous. . . ).

In this paper, we provide an in-depth overview of the relation between two models of processes: the one of asynchronous (or untimed) dataflow represented by Kahn Process Networks, and that of synchronized dataflow represented by the polychronous model. In particular, the fact that processes in the polychronous model (represented by Signal programs) can be asynchronously nondeterministic has to be carefully and analytically taken into account.

In general, the relationship synchrony/asynchrony is crucial since on the one hand, synchronous programs may have to be at least partly desynchronized to be implemented efficiently onto possibly asynchronous architectures, and on the other hand, asynchronous programs need to be synchronized in order to get effective, correct-by-construction, implementations.

Previous works

In this aim, a number of theoretical results have been formulated, and reference papers on the semantic model, including formal properties for compositionality and asynchronous implementation, consider this issue more or less explicitly under the term of isochrony.

Isochrony is the property of (at least) two processes to indifferently produce the same flows of values, whether synchronously or asynchronously composed. Isochrony is a much desirable property, as it implies the capability to design and schedule processes compositionally, that is, independently of their runtime scheduler or architecture. A ground motivation for seeking isochrony is desynchronization: the transformation of a monolithic synchronous design into several tasks to be executed in parallel.

The first formal address of desynchronization can be found in [START_REF] Caspi | Clocks in dataflow languages[END_REF], where precise relations between well-clocked synchronous functional programs and the subset of Kahn-networks are established, and shown to be amenable to bufferless evaluation. In [START_REF] Caspi | Execution of distributed reactive systems[END_REF], the author considers the distribution of synchronous automata on asynchronous networks using Fifo-buffered broadcast communications. In [START_REF] Berry | An implementation of constructive synchronous programs in POLIS[END_REF], a model for the distribution of synchronous programs on distributed architectures is introduced which uses low-level non-blocking one-place buffers.

In [START_REF] Benveniste | Compositionality in dataflow synchronous languages: Specification and distributed code generation[END_REF], an analysis of the links between synchrony and asynchrony is presented in the context of synchronous transition systems and the compositional property of isochrony introduced (a pair of processes is isochronous iff its synchronous and asynchronous compositions admit the same traces). It provides a first intuition for defining the property of isochrony from that of endochrony: the capacity of an individual process to determine the status (present or absent) of all events, at all times.

As this property is however too strong (endochronous processes are not isochronous, in general), a number of subsequent works refined it by weakening it to endo-isochrony [START_REF] Le Guernic | Polychrony for system design[END_REF][START_REF] Talpin | From multi-clocked synchronous processes to latency-insensitive modules[END_REF], by first repurposing the static analyser for endochrony, and then by defining the the largest class of such isochronous processes under the term of weak endochrony [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF][START_REF] Potop-Butucaru | Correct-by-construction asynchronous implementation of modular synchronous specifications[END_REF][START_REF] Potop-Butucaru | From concurrent multiclock programs to deterministic asynchronous implementations[END_REF]. In turn, weak endochrony is the capacity of a process to always make its environment aware when it locally choose an event to be absent (relevant absence). It does, in particular, correspond to the common practice of flow-control in the design of asynchronous protocols.

Isochrony also relates to the notion of latency-insensitive circuits of Carloni et al. [START_REF] Carloni | Latency insensitive protocols[END_REF], which we formally characterize and compare with in Section 2.7.

Goal

In this paper, we revisit the above line of works by an analysis of the polychronous model of computation of Signal under the perspective of its semantic relations with the original model of Kahn process networks, knowing that both models have given rise to efficient implementations in different domains of application such as time-critical systems and stream processing. We will make the choice to present and expand these formal results by considering them under a close relationship to the present implementation of the Signal language in the open-source Polychrony toolset1 , which does not integrate advanced analysis to synthesize weakly-endochornous networks.

Plan

The rest of this article is organized as follows. In Section 2, we review the formal basis of the polychronous model and introduce characteristic properties and categories of processes. In particular, we define the class of so-called polyendochronous processes [START_REF] Ouy | Génération de code asynchrone dans un environnement polychrone pour la production de systèmes GALS[END_REF]. Then we provide typical simple Signal specifications. In Section 3, we first review the definition of KPNs as flow functions. Then we define Signal operators as extended flow functions and show in which conditions Signal programs can be seen as KPNs. In this context, we consider different cases of process networks, including polyendochronous processes. Then, in Section 4, we describe code generation for the class of such polyendochronous processes. Finally, in Section 5, we propose an extension to Signal allowing to consider (bounded) KPNs as (extended) Signal programs.

Signal polychronous model

Several semantics of the Signal language have been provided along years. Our presentation of the polychronous model is mainly based on [START_REF] Le Guernic | Polychrony for system design[END_REF], with some revisions. Basics of the model are defined in Section 2.1, including synchronous composition of processes. Then, Sections 2.2 and 2.3 provide different order and equivalence relations allowing to compare processes. The asynchronous composition of processes is defined in 2.4, and the property of flow-invariance allows to relate synchronous and asynchronous compositions. A special category of "endochronous processes" is defined in Section 2.5, deterministic processes are characterized in Section 2.6, and weakly endochronous processes (with, among them, polyendochronous processes) are defined in Section 2.7. Then, the semantics of Signal basic operators is described in Section 2.8 and useful derived operators are defined in 2.9. The use of these operators is illustrated in a few typical examples in Section 2.10.

Basics of the polychronous model

In the polychronous model, a component will be abstracted by its time relations on its observable variables. Time domain. The following requirements are considered for a time domain (or tag domain since it is not necessarily directly associated with a numeric notion of time) Ω:

• Ω is a poset equipped with a partial order relation ≤.

• Ω is a meet-semilattice: any two elements in Ω have an infimum (or greatest lower bound) in Ω. This allows for time causality.

• Ω is a densely ordered set: for all x and y in Ω for which x ≤ y, there exists z in Ω such that x < z < y. This allows for context adaptation and implementation refinement.

• Any finite family of subsets of Ω has an upper bound in Ω.

A chain C of Ω is a countable and well-ordered subset of Ω. Such a chain C is well-ordered if all its non-empty subsets have a minimal element for ≤. In particular, a (countable and well-ordered) chain C has a lower-bound for ≤, written min(C) [START_REF] Le Guernic | Polychrony for system design[END_REF].

We denote by C the set of such chains C. For a nonempty chain C ∈ C \ ∅, we write min(C) for the least element of C, and for a tag t ∈ C \ min(C), we write pred C (t) for the (unique) immediate predecessor of t in C.

Domain of values. The domain of values D is a set of values containing at least

Boolean values (B = {ff , tt} ⊆ D).

Timed history.

Definition 1 (Timed history-a.k.a. signal-, event). A timed history (or a signal ) is a mapping s from a chain C ∈ C to the domain of values D (s : C → D). We write tags(s) to denote the domain of s. The pairs (t, v) in s such that s(t) = v are called events.

Let S be the set of timed histories.

Behavior. We consider a countable set V of variables.

Definition 2 (Behavior).

A behavior on V , where V is a finite set of variables of V (V ⊆ V), is a mapping b from V to the set of timed histories (b : V → S).

t 1 = t 3 x → y → z → t1<t2 x tt x ff x tt x 0 x 1 x 0 x 1 x 0 x tt x tt x tt t 3 ≶ t 4
Figure 1: Depiction of a behavior b from signal names x, y, z to partially ordered tags and values. The 1 st tag t 1 of x precedes its 2 nd (t 1 < t 2 ) and equals the 1 st tag of y (t 1 = t 3 ) while z is synchronized with neither of x or y ( 3 ≶ t 4 ).

A behavior prefix (which is a finite behavior), written b ≤Θ , is the projection of the behavior b on the set of the tags t ∈ tags(b) such that ∀θ ∈ Θ, t ≤ θ. Similar notations are considered for a behavior prefix until a tag θ and before a tag θ (respectively, b ≤θ and b <Θ ).

Concatenation of reactions.

A reaction is a behavior with (at most) one tag. As for behaviors, we write vars(r) to denote the domain of a reaction r and tags(r) to denote the tag of a non empty reaction r.

A reaction r is concatenable to a behavior b iff vars(b) = vars(r) and ∀x ∈ vars(b), either r(x) = ∅ (where ∅ is the empty set of timed histories), or, if

t is the tag of r, t ≤ u ⇒ u ∈ tags(b(x)). In that case, concatenating r to b is defined ∀x ∈ vars(b), ∀t ∈ tags(b) ∪ tags(r), by (b • r)(x)(t) = r(x)(t) if t ∈ tags(r(x)) and (b • r)(x)(t) = b(x)(t) otherwise.
In particular, reactions can be concatenated to form behaviors.

Process.

Definition 3 (Process). A process P on a finite set of variables V ⊆ V is a set of behaviors on V (V is also noted vars(P )).

There is a single process on the empty set of variables, which is {∅}. Let P be the set of processes. The restriction P |V of a process P on V , with V ⊆ V , is defined by the set of behaviors b |V such that b ∈ P .

Composition.

Definition 4 (Synchronous composition). The composition (or synchronous composition) P 1 |P 2 of two processes P 1 and P 2 , respectively on V 1 and V 2 , is the process on Synchronous composition defines an "intersection" of behaviors and implies a syntactic congruence property:

V 1 ∪ V 2 defined as the set of behaviors b such that b |V1 ∈ P 1 and b |V2 ∈ P 2 . P b =   i → x → y → x ff x ff x tt x ff x tt x 2 x 2 x 1 x 5 x 4   Q c =   x → y → j → x tt x ff x tt x 2 x 2 x 1 x 5 x 4 x tt x tt x tt  
• (P, |, {∅}) is a commutative monoid.
• The composition operator | is idempotent.

Stretching and stretch-equivalence

A "stretching" relation is defined as follows on behaviors:

Definition 5 (Stretching). Let b 1 , b 2 be two behaviors, b 2 is a stretching of b 1 , written b 1 ≤ b 2 , iff vars(b 1 ) = vars(b 2
) and there exists a bijection f :

tags(b 1 ) → tags(b 2 ) such that: ∀C ∈ C, ∀t ∈ C, t ≤ f (t), ∀t 1 , t 2 ∈ tags(b 1 ), t 1 ≤ t 2 ⇔ f (t 1 ) ≤ f (t 2 ) (f is increasing), and b 1 and b 2 are isomorphic: ∀x ∈ vars(b 1 ), f (tags(b 1 (x))) = tags(b 2 (x)), ∀x ∈ vars(b 1 ), ∀t ∈ tags(b 1 (x)), b 1 (x)(t) = b 2 (x)(f (t)).
The stretching relation is a partial order on behaviors. An equivalence relation, called "stretch-equivalence", is defined from this partial order: The equivalence class of a behavior for the stretch-equivalence forms a meetsemilattice which has a least element. We call strict behaviors the behaviors which are minimal for the stretching relation. For a given behavior b, the set of all behaviors that are stretch-equivalent to b defines its stretch-closure, written b * . The stretch-closure of a set of behaviors p is the set denoted by p * , which contains all the behaviors resulting from the stretch-closure of each behavior b ∈ p, i.e., p * = b∈p b * .

It is interesting, in particular, to consider the so-called stretch-closed processes, which are those processes p such that p = p * . A non-empty stretch-closed process p admits a set of strict behaviors, written (p) ≷ , such that (p) ≷ ⊆ p (for all b ∈ p, there exists a unique c ∈ (p) ≷ such that c ≷ b).

Relaxation and flow-equivalence

All stretch-equivalent behaviors have the same synchronization relations between their events. A weaker relation than stretching may be considered, which discards these synchronization relations and allows for comparing behaviors with respect to the sequences of values that variables hold.

Definition 7 (Relaxation

). A behavior b 2 on V is a relaxation of a behavior b 1 on V , written b 1 b 2 , iff for all x ∈ V , b 1|{x} ≤ b 2|{x} (the projection of b 2
on each variable is a stretching of the projection of b 1 on this variable).

The relaxation relation is a partial order on behaviors. An equivalence relation, called "flow-equivalence", is defined from this partial order: The equivalence class of a behavior b for the flow-equivalence forms a meet semi-lattice which has a least element; it is a strict behavior, written b ≈ .

The following properties, which are easy to establish, will be used in some proofs:

• If b ≈ c and X ⊆ vars(b) then b |X ≈ c |X ; • If b |X ≈ c |X and b |Y ≈ c |Y then b |X∪Y ≈ c |X∪Y .

Asynchronous composition and flow-invariance

The asynchronous composition (or parallel composition) of processes is more flexible than the synchronous composition. It allows behaviors that would be rejected in synchronous composition. The asynchronous composition of two processes P and Q contains all the behaviors b that are relaxations of behaviors b 1 and b 2 from P and Q along shared variables, and that are stretch-equivalent to behaviors b 1 and b 2 along independent variables of P and Q. Definition 9 (Asynchronous composition). If processes P and Q are respectively defined on sets of variables V 1 and V 2 , their asynchronous composition is:

P || Q = b ∈ B |V1∪V2 ∃b 1 ∈ P, b 1|V 1 ∩V2 b |V1∩V2 ∧ b 1|V 1 \V2 ≷ b |V1\V2 ∃b 2 ∈ Q, b 2|V 1 ∩V2 b |V1∩V2 ∧ b 2|V 2 \V1 ≷ b |V2\V1
Flow-invariance, based on flow-equivalence, allows to relate synchronous and asynchronous compositions of processes.

Definition 10 (Flow-invariance). A process

P defined on V is flow-invariant on I ⊆ V iff ∀b 1 , b 2 ∈ P, b 1|I ≈ b 2|I ⇒ b 1 ≈ b 2 or, equivalently, ∀b 1 , b 2 ∈ P, (b 1|I ) ≈ = (b 2|I ) ≈ ⇒ b 1 ≈ b 2 .
In particular, if P is the asynchronous composition of two processes, P = p || q, the flow-invariance of P on some variables I implies the flowequivalence between behaviors of p || q and behaviors of p | q (since P contains all these behaviors). Thus, flow-invariance ensures that the refinement of a synchronous specification p | q by an asynchronous implementation p || q preserves the sequences of values along all signals for any given behavior. Moreover, flow-invariance is compositional: if p and q are respectively flow-invariant on I ∩ vars(p) and I ∩ vars(q), then p || q is flow-invariant on I.

Endochronous processes

Endochronous processes are distinguished because they have a key role in "delay insensitive" implementations. Informally, a process is endochronous on a set of variables I if, given an external (asynchronous) stimulation of I, it is capable of reconstructing a unique behavior (up to stretch-equivalence). The following definition makes this more formal.

): ∀b 1 , b 2 ∈ P, Φ(b 1 ) = Φ(b 2 ) ⇒ b 1 = b 2 .
To examplify endochrony, consider an oversampling write process (that will be depicted at the end of Section 3), which is paced by a Boolean input signal c, such that c ≈ = (f f, tt, f f, tt), to read an integer input y, such that y ≈ = 1, 2, 3, 4 when c is true and output either of that value or the previously memorized one (initially 0) along an output signal x. Whichever time tags t are assigned to c, x, y, y must always synchronizes to c and x to carry a new value of y if c is true, hence x ≈ = (0, 2, 2, 4).

As a consequence of this definition, a process P defined on V is endochronous on

I ⊆ V iff ∀b 1 , b 2 ∈ P , b 1|I ≈ b 2|I ⇔ b 1 ≷ b 2 .
If the set of variables I is the set of inputs of P , P is endochronous if it is endochronous on I. In other words, a process is endochronous if any behavior of this process is entirely determined by the sequence of values carried by I independently of their relative presence and absence. Proposition 1. A process which is endochronous on I is flow-invariant on I.

Proof. Let P be an endochronous process on I, and b, c such that (b |I ) ≈ (c |I ). From endochrony we have b ≷ c, and from properties of flow-equivalence

(cf. 2.3), b ≈ c. 2
While Proposition 1 is easy to prove for a trace semantics, thanks to the algebraic properties provided by the stretching and relaxation [? ], it also has an inductive proof in a constructive operational semantics of Signal that materializes the role played by event and/or time triggers [? ] upon which the evaluation of input flows by a given endochronous starts and converges to a unique solution. Endochrony will further be illustrated in Section 3.8.3 using an implementation of the example described in Section 2.10.

(b| I ) ≈ = (c| I ) ≈ ⇒ b ≶ c
Figure 5: An endochronous process P processes two input flows (green) by building a unique stretch-equivalence class of behaviors that synchronize the inputs to the occurences of the value true on its own, private, clock (yellow).

Deterministic processes

We will say that a process is deterministic on a set of variables if any behavior of this process is entirely determined by its restriction to this set of variables. More formally, we set this definition: Definition 12 (Deterministic process). A process P defined on V is deterministic on I ⊆ V if and only if the function Ψ :

P → P |I such that Ψ(b) = b |I is injective (and thus bijective, since it is necessarily surjective): ∀b 1 , b 2 ∈ P, Ψ(b 1 ) = Ψ(b 2 ) ⇒ b 1 = b 2 .
Hence, a process P defined on V is deterministic on

I ⊆ V iff ∀b 1 , b 2 ∈ P , b 1|I ≷ b 2|I ⇔ b 1 ≷ b 2 .
A process is deterministic on a set of variables iff any two behaviors of this process are stretch-equivalent when their projections on this set of variables are stretch-equivalent. We will say that a process is deterministic if it is deterministic on I.

To examplify determinism, now consider a downsampling read process, which is paced by a Boolean input signal c, such that c ≈ = (f f, tt, f f, tt), and synchronizes to an integer input signal x, such that x ≈ = 1, 2, 3, 4. When c is true, the value of x is output along a signal y. Hence, the output y ≈ = (2, 4), at the exact same time tags than the even occurrences of c and x.

The following proposition is easily deduced from the definitions of endochronous processes and deterministic processes:

Proposition 2. If a process P defined on V is endochronous on I ⊆ V , then it is deterministic on I.
Examples of deterministic and non-deterministic Signal processes will be presented in Section 3.5.

Weakly endochronous processes

As endochrony is not preserved by composition, it may be desirable, to achieve compositionality, to define a weaker notion called weak endochrony. This requires a definition of the union of so-called independent reactions. Two reactions are independent iff they have disjoint domains (they are defined on distinct variables).

The union r s of two independent non empty reactions r and s is defined as follows if they have the same tag, tag(r) = tag(s): ∀x ∈ vars(r) ∪ vars(s), (r s)(x) = if x ∈ vars(r) then r(x) else s(x).

Definition 13 (Weakly endochronous process). A process P defined on V is weakly endochronous on I ⊆ V iff:

1. P is deterministic on I; 2. for all behaviors b and independent reactions r and s and r and t, P satisfies:

• if b • r • s ∈ P then b • s ∈ P , • if b • r ∈ P and b • s ∈ P then b • (r s) ∈ P , • if b • (r s), b • (r t) ∈ P then b • r • s, b • r • t ∈ P .
P is weakly endochronous if it is weakly endochronous on its set of inputs.

Informally, a process is weakly endochronous iff it is deterministic and can perform independent reactions in any order. Note that endochrony implies weak endochrony.

A process P is non-blocking iff for all behaviors b ∈ P , there exists some reaction r ∈ P such that b • r ∈ P .

From its definition, it appears that checking weak-endochrony requires an exhaustive state-space exploration, which could be very costly, or would require a program analysis to abstract the state space to be explored, as in [START_REF] Potop-Butucaru | From concurrent multiclock programs to deterministic asynchronous implementations[END_REF]. Determining that a process is weakly endochronous is even non decidable in general for infinite-state systems. A method has been proposed based on the static abstraction and analysis of clock and scheduling relations, allowing to model-check weak endochrony [START_REF] Talpin | Compositional design of isochronous systems[END_REF]. However, this can be still costly and it may be useful to define a property which is stronger than weak-endochrony and easy to check. This property will be called polyendochrony. Unlike endochrony, that allows to reconstruct, from a given set of signals, a unique behavior (modulo stretching) on the whole set of variables, polyendochrony allows to reconstruct a unique behavior (modulo stretching) on subsets of variables.

Subdomain of a variable in a process. Let P be a process on a set of variables V and r a (referent) variable in V . We call subdomain of r, denoted r, the set of variables for which associated signals are present only at some instants of r:

r = {x ∈ V |∀b ∈ P, tags(b(x)) ⊆ tags(b(r))}.
For a behavior b, b | r is the projection of b on the subdomain of r.

Polyendochronous processes.

Definition 14 (Polyendochronous process). A process P defined on V is polyendochronous on

I ⊆ V iff ∀b 1 , b 2 ∈ P , ∀r ∈ V , b 1|I ≈ b 2|I ⇔ b 1| r ≷ b 2| r .
A process is polyendochronous if it is polyendochronous on I. Note that endochrony is a special case of polyendochrony: an endochronous process is a polyendochronous process for which all variables belong to the same subdomain. An example of a poly-endochronous Signal process is given in Section 3.9.

Relation to latency-insensitive protocols.

In [START_REF] Carloni | Latency insensitive protocols[END_REF], a theory of latency-insensitive protocols (LIP) is presented as a foundation of a methodology to design very large digital systems by assembling blocks of existing intellectual property (Ip). In the theory of LIP, a process p may accept stall moves (a stall move consists of stretching a signal s of a given behavior b by one logical instant) and respond by the appropriate procrastination effect (the other signals s of the behavior b will respond to the delay of s by making coordinated stall moves).

The mechanism of causally related stall moves is made explicit (and generalized to polychronous signals) in the relation of stretching. A stretch corresponds to a slide of tags in a given behavior: if an event e is stalled, then all other events e , causally related to e by the partial order relation ≤) will stall further. As a result, Signal processes are patient, in the sense of [START_REF] Carloni | Latency insensitive protocols[END_REF].

Definition 15 (patience [START_REF] Carloni | Latency insensitive protocols[END_REF]). A patient process p is a process such that, for all behaviors b ∈ p, for all and for all signals

x ∈ (b) s.t. b(x) = (t j , v j ) j>0 , if a signal s = (t k , v k ) k>0
differs from s by one stall move (i.e. there exists l > 0 s.t. t j = t k for all j = k < l and t l ≤ t l ) then there exists b ∈ p such that b (x) = s .

The (multi-clocked) notion of flow-equivalence relates to the notion of latency-equivalence of Carloni et al. [START_REF] Carloni | Latency insensitive protocols[END_REF]. Two signals are latency-equivalent iff they present the same values in the same order.

Definition 16 (latency-equivalence [START_REF] Carloni | Latency insensitive protocols[END_REF]). Let (t i ) i>0 and (t i ) i>0 be two chains of s.t. for all j, k > 0, j ≤ k iff t j ≤ t k and t j ≤ t k . The signals

s = (t i , v i ) i>0 and s = (t i , v i ) i>0 are latency-equivalent iff for all i > 0, v i = v i .
Notice that, if s and s are flow-equivalent, then they are latency equivalent. Flow-equivalence extends the property of latency-equivalence to multiclocked systems: the theory of LIP considers synchronous processes equipped with totally ordered time tags (i.e. single-clocked systems). This hypothesis corresponds to the low-level behavior of circuits (where silence, i.e. τ events, corresponds to stall moves or "don't care" moves). The tagged model of polychronous signals considers a more general structure of partially ordered semi-lattice.

Signal operators

The Signal language provides a syntax to processes defined from particular relations between timed histories (signals) associated with signal variables. Elementary processes are defined by equations. An equation associates with a signal variable an expression built on operators over timed histories associated with signal variables. Syntactically, an equation is written x := f (y 1 , . . . , y n ). It is said to define the output x and use the inputs y 1 , . . . , y n (minus x). The outputs of a process P are the variables it defines and its inputs are the other it uses. For a process denoted by P , we write P to denote the set of behaviors of the process.

Two kinds of operators are distinguished: synchronous operators and polychronous operators.

Synchronous operators.

Stepwise extension of function. Let f designate some n-ary total function f : D 1 × . . . × D n → D n+1 where D i ⊆ D and n > 0 (such functions are, for instance, usual logic, arithmetic or relational operations). In Signal, these functions are extended to timed histories:

x := f (y 1 , . . . , y n ) = b ∈ B |{x,y1,...,yn} tags(b(x)) = tags(b(y 1 )) = . . . = tags(b(y n )) = C ∈ C ∀t ∈ C, b(x)(t) = f (b(y 1 )(t), . . . , b(y n )(t))
Delay. The delay operator represents a state initialized with some value v ∈ D:

x := y$ init v =    b ∈ B |{x,y} tags(b(x)) = tags(b(y)) = C ∈ C \ ∅ b(x)(min(C)) = v ∀t ∈ C \ min(C), b(x)(t) = b(y)(pred C (t))   
Polychronous operators. Polychronous operators relate timed histories defined on different sets of tags.

Sampling. The signal variable z, which takes its values in the Booleans B, true tt and false ff serves as sampling condition:

x := y when z = b ∈ B |{x,y,z} tags(b(x)) = {t ∈ tags(b(y)) ∩ tags(b(z))|b(z)(t) = tt} ∀t ∈ tags(b(x)), b(x)(t) = b(y)(t)
Merge. The merge gives priority to its first operand:

x := y default z =    b ∈ B |{x,y,z} tags(b(x)) = tags(b(y)) ∪ tags(b(z)) = C ∈ C ∀t ∈ C, b(x)(t) = b(y)(t) if t ∈ tags(b(y)) b(z)(t) if t ∈ tags(b(y))    2.

Signal syntax and derived operators

The concrete syntax for the composition of processes P and

Q is (| P | Q |).
For a process P defined on a set of variables V , the restriction of P on V \{x} (x is hidden from the outside of P ) is denoted by P / x or P where x.

Derived operators are defined from the operators of the kernel language, defined in Section 2.8, with composition and restriction. The following derived operators will be used in the examples of this article (a complete definition of the language is available online [START_REF] Besnard | SIGNAL V4-INRIA version: Reference Manual[END_REF]).

• Signal clock: x := ˆy is defined by x := y = y (y is present and tt when

x is present: y has the type event, the single value of which is the value tt-this type is used to represent clocks of signals).

• Selection: x := when y (a.k.a. x := [: y]) is defined by x := ˆy when y (x is a signal of type event, present-and tt-when the Boolean signal y is present and tt).

• Clock intersection: x := y ˆ * z is defined by x := ˆy when ˆz (x is a signal of type event, present when both signals y and z are present).

• Clock union: x := y ˆ+ z is defined by x := ˆy default ˆz (x is a signal of type event, present when either signal y or z is present).

• Clock difference: x := y ˆ-z is defined by x := when ((not ˆz) default ˆy) (x is a signal of type event, present when the signal y is present but z is not).

• Null clock: ˆ0 is defined by when (not ˆx), x being any signal (ˆ0 is a signal of type event which is never present).

• Synchronization: x ˆ= y is defined by (c := ˆx = ˆy)/ c (it is an outputfree process which constrains signals x and y to be present at the same instants-signals which are present at the same instants are synchronous: they have the same clock).

• Clock relation: x ˆ< y is defined by x ˆ= x ˆ * y (it is an output-free process which constrains the clock of the signal x to be less frequent-or equal to-that of the signal y).

• Partial definition: x ::= y is defined by x := y default x (x is defined by y when y is present, otherwise it may be present but its value is left undefined-multiple partial definitions of x may be provided).

x

:= y$ init v y → x → x ff x tt x ff x tt . . . x tt x ff x tt x ff x tt . . . x := y default z   y → z → x → x ff x ff x tt . . .

Examples of Signal programs

We use the Signal syntax with its modularity features allowing to declare a given process (a set of equations) as a process model with a name, possible static parameters (not used here) and explicit interface (input and output signals respectively preceded by "?" and "!").

Asynchronous memory cell. The following program describes an asynchronous memory cell with input x and output y:

process memoryCell = ( ? integer x ; ! integer y ; ) ( | v := x default ( v$ i n i t 0 ) | y := v when ˆy | )
where integer v ; end ;

The signal v representing the cell is hidden so that it is not possible to synchronize it from the outside: this makes the process asynchronous.

Integers generator. The following program, with no input, generates the sequence of positive integers: process i n t e g e r s G e n e r a t o r = ( ?

! integer x ; ) ( | x := ( x$ i n i t 0 ) + 1 | ) ;
Its clock is the clock of its output. It may be a node in a KPN.

Fibonacci sequence generator. In the same way, the following program describes a Fibonacci sequence generator:

process F i b o n a c c i = ( ? ! integer f i r s t ; ) ( | f i r s t := s e c o n d $ i n i t 0 | s e c o n d := tmp$ i n i t 1 | tmp := f i r s t + s e c o n d | )
where integer second , tmp ; end ; It corresponds to the KPN represented as example in [START_REF] Geilen | Kahn process networks and a reactive extension[END_REF].

Internal master clock. The following program generates a sequence of n events after each occurrence of an input signal n, and before its next occurrence (n is supposed to be a positive or null integer signal):

process N e v e n t s = ( ? integer n ; ! event i ; ) ( | c n t := n default ( p r e c n t -1 )

| p r e c n t := c n t $ i n i t 0 | n ˆ= when ( p r e c n t = 0 ) | i := when ( p r e c n t > 0 ) | ) where integer cnt , p r e c n t ; end ; This program uses the "oversampling" mechanism: the "master clock" represents a refinement of time, with respect to the clock of the input signal. Here, this master clock is that of an internal signal (the common clock of cnt and pre cnt).

Signal programs as KPNs

The formal definition of Kahn Process Networks is first recalled in Section 3.1 and some related works are mentioned in 3.2. In Section 3.3, we look at whether Signal operators can be considered as flow functions and in Section 3.4, we define an actor model for Signal operators. The question of deterministic versus non-deterministic Signal programs is considered in Section 3.5 and that of testing the absence in Section 3.6. Then, rules of syntactic equivalence allowing to rewrite Signal programs are provided in Section 3.7 and the formal clock calculus applied in compiling programs is described in Section 3.8. Resulting from these rewritings (in particular, the one of clock calculus), the first main result of this section is stated in Section 3.9, allowing to relate (composition of) endochronous processes and KPNs. In the rest of the section, special cases of such endochronous process networks are considered, including polyendochronous networks.

Fixed-point semantics of flow functions

Gilles Kahn's pioneering work in the seventies [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] has given semantical bases to the dataflow paradigm. Informally, Kahn Process Networks are process networks in which the nodes (which are concurrent sequential processes) communicate streams of data via FIFO channels with blocking read and non-blocking write operations. The denotational semantics of KPNs is defined as fixed-point semantics of flow functions. In this section, we mainly borrow to [START_REF] Geilen | Kahn process networks and a reactive extension[END_REF] the formulation of the semantics.

For a domain of values D, we write D ω for the set of finite and countably infinite sequences of values in D (strings over alphabet D). The empty sequence is denoted by . The prefix order on sequences is defined as follows: ∀x ∈ D ω , x, ∀v ∈ D, ∀x, y ∈ D ω , x y iff v • x v • y (where the symbol "•" denotes the usual concatenation of strings). Intuitively, the order relates the amount of information. (D ω , ) is a complete partial order (cpo). Each directed subset D in a cpo has a least upper bound (a subset is directed if it is non-empty and every pair of elements has an upper bound in the subset). Typically, an increasing chain of sequences D = {x 0 , x 1 , . . .}, where x 0 x 1 . . ., has a least upper bound. We write D for this supremum.

Let (D ω ) p be the set of p-tuples of sequences in D ω . Tuples of sequences are ordered as well:

(X 1 , . . . , X p ) (X 1 , . . . , X p ) if X i X i for each i, 1 ≤ i ≤ p. ((D ω ) p ,
) is a cpo for any integer p.

A KPN process (or actor) with m inputs and n outputs is a function f : (D ω ) m → (D ω ) n that maps a tuple of input sequences into a tuple of output sequences. In a KPN, this function is required to be Scott-continuous, that is to say it preserves least upper bounds: for every directed subset D of the set of m-tuples of sequences in D ω (typically, an increasing chain of m-tuples of sequences), the image by f of the supremum of D is the supremum (that must exist) of the set of the images of all the elements of D. This is denoted by f ( D) = f (D). We say that f is a flow function. Intuitively, continuity expresses that any finite amount of information about the output of the function is due to a finite amount of information about the input. Scott-continuity implies in particular monotonicity: x y =⇒ f (x) f (y) (order preservation, or causality: the more input the function is given, the more output it produces, and computations flow from past to future). A process can be computed iteratively.

A KPN is defined by a set P of KPN processes and a set C of channels, partitioned into disjoint sets of inputs I, outputs O and internal channels L. Each process p has a set of input channels I p and output channels

O p in C (with p∈P I p ∪ p∈P O p = C and p∈P O p = L ∪ O).
In the context of KPNs, a history of a channel associates with the channel (designated by a variable) the sequence of data (also referred to as stream, or sometimes pure flow ) communicated along the channel. A history h of a set V of channels is a mapping from V to D ω . The set of all histories of V is denoted as H(V ). Thus a KPN process p is described by a Scott-continuous function f p : H(I p ) → H(O p ) that maps input histories to output histories.

For a history h ∈ H(V ), we write h |V for the projection of h on a set of channels V ⊆ V . We define an order on histories as follows: for two histories

h 1 ∈ V 1 , h 2 ∈ V 2 (with V 1 , V 2 ⊆ V ), h 1 h 2 iff V 1 ⊆ V 2 and for every c ∈ V 1 , h 1 (c) h 2 (c). The set of histories (H(V ), ) is a cpo.
The behavior of a KPN is described by its network equations, expressing relations on histories h ∈ C for all its processes:

h |Op = f p (h |Ip ) for all p ∈ P .
Then, it is described as a (Scott-continuous) flow function f from input histories to histories of all channels of the network, f : H(I) → H(C), that obeys to the following recursive equations:

f (i) |I = i f (i) |Op = f p (f (i) |Ip
) for all p ∈ P From these equations, we define a functional Φ : (

H(I) → H(C)) → (H(I) → H(C)): Φ(f )(i) |I = i Φ(f )(i) |Op = f p (f (i) |Ip
) for all p ∈ P Φ is a Scott-continuous function on a cpo. Thanks to Kleene fixed-point theorem, Φ has a least-fixed point: the "smallest" function f that satisfies the network equations. It is the supremum of the ascending Kleene chain of Φ: ∅ Φ(∅) Φ(Φ(∅)) . . . (where ∅ is the everywhere undefined function). The behavior of the network can be iteratively computed using Kleene iteration.

KPNs and related work

In Kahn's model, processes are deterministic. Considering non-deterministic computations is more problematic. It has been shown in [START_REF] Brock | Scenarios: A model of non-determinate computation[END_REF] that, in this case, the input-output relation computed by a network is not compositional. A lot of references for non-deterministic operations may be found in [START_REF] Panangaden | The expressive power of indeterminate primitives in asynchronous computation[END_REF]. In [START_REF] Panangaden | The expressive power of indeterminate dataflow primitives[END_REF] the authors use trace sets, which are compositional, as abstractions of process behaviors and discuss the problem of having fair merge in dataflow networks.

On another side, synchronous dataflow languages Lustre [START_REF] Raymond | The synchronous dataflow programming language Lustre[END_REF] and Signal offer a way to abstract the time at which computations take place and allow to generate efficient implementations with bounded memory. Synchronous (or synchronized) dataflow appears as some restriction of general dataflow, which has to respect some "synchronous constraints". The rules that define these restrictions provide a static analysis which is called "clock calculus" [START_REF] Caspi | Clocks in dataflow languages[END_REF][START_REF] Amagbegnon | Implementation of the dataflow synchronous language Signal[END_REF]. Clock calculus is a verification of clock relations (timing relations between streams) in Lustre, while it is a synthesis of such relations in Signal (cf. Section 3.8).

In [START_REF] Caspi | Synchronous Kahn networks[END_REF], the authors relate synchronous constraints to "listlessness" [START_REF] Wadler | Listlessness is better than laziness: Lazy evaluation and garbage collection at compile-time[END_REF] and extend the class of static synchronous dataflow to higher order and some class of recursive networks. They call their programs "synchronous Kahn networks".

Another restricted dataflow model is that of SDF (for Synchronous Data Flow, again) [START_REF] Lee | Static scheduling of synchronous data flow programs for digital signal processing[END_REF], which is one of the basic models of computation of the Ptolemy framework [START_REF] Hylands | Overview of the Ptolemy project[END_REF][START_REF] Ptolemaeus | System Design, Modeling, and Simulation using Ptolemy II, Ptolemy.org[END_REF]. As it is the case for synchronous languages, SDF models have a "consistency checking" that makes possible static scheduling at compile time.

More generally, as discussed in [START_REF] Caspi | Actors without directors: A Kahnian view of heterogeneous systems[END_REF], in order to give a formal semantics to heterogeneous systems, the authors of Ptolemy have proposed a semantics which is a generalization of a Kahn semantics based on a tagged signal model [START_REF] Lee | A framework for comparing models of computation[END_REF]. In Kahn's theory, the tag domain is N, signals are partial functions from N to a set of values V , and signals are assumed to be prefix-closed (if they are undefined at some time n then they remain undefined for all n > n). Generalization consists in considering other tag sets T, where T is a poset, while remaining orderpreserving [START_REF] Liu | CPO semantics of timed interactive actor networks[END_REF]. In this theory, signals are partial functions from T to a set of values V . The authors of [START_REF] Caspi | Actors without directors: A Kahnian view of heterogeneous systems[END_REF] observe that in many useful cases, simplifying assumptions can be considered: 1/ the tag set is a total order, 2/ the defined values of a signal can be indexed in non decreasing order (discrete signal). Then signals can be seen as streams and the theory reduces to the ordinary Kahn theory. Heterogeneity (dealing with different tag sets) and distribution are then handled in this generalized Kahn semantics.

On a practical aspect, KPNs are a popular model to describe signal processing and multimedia applications. Unlike synchronous dataflow models, general KPNs must be scheduled dynamically: a run-time system is necessary to schedule the processes and to manage memory for the channels. Conceptually, the FIFO channels of a KPN have an unbounded capacity, however, for a given realisation, a KPN has to run with a finite amount of memory. It is undecidable in general to know which buffer capacity is needed in every channel [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF]. A model of execution has been proposed [START_REF] Parks | Bounded scheduling of process networks[END_REF], where fixed capacities of memory are allocated to FIFOs and these bounds can be changed dynamically. This model is used for many implementations of KPNs [START_REF] Stevens | Implementation of process networks in Java[END_REF][START_REF] Goel | Process networks in Ptolemy II[END_REF][START_REF] De Kock | YAPI: application modeling for signal processing systems[END_REF]. In this model, a write action on a full FIFO is blocked until there is room again in the buffer. Unfortunately, if buffers are chosen too small, artificial deadlocks may appear and the proposed global deadlock resolution strategies do not guarantee fairness. In [START_REF] Geilen | Requirements on the execution of Kahn process networks[END_REF], it is proposed for a subclass of KPNs an improved scheduling strategy that uses local deadlock detection.

In the synchronous dataflow context, [START_REF] Cohen | N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems[END_REF] proposes a model of "nsynchronous Kahn networks": two processes are n-synchronous if they can communicate in the ordinary synchronous model with a FIFO buffer of size n. Periodic clocks defined as periodic infinite binary words are considered. In this framework, minimal buffer sizes needed to communicate between synchronizable clocks may be statically computed. The approach is generalized in [START_REF] Cohen | Abstraction of clocks in synchronous data-flow systems[END_REF] to non necessarily periodic clocks using a notion of "clock envelope" that represents interval of clocks up to bounded buffering.

Signal operators and flow functions

Signal operators can be viewed as actors that map a tuple of input sequences into an output sequence. Composed processes correspond clearly to networks of actors.

In particular, synchronous operators are flow functions. Let + ω be the stepwise extension on finite and countably infinite sequences of the usual + operator defined on some type domain. In Signal, constraints on length of flows (sequences) make this operator monotonic:

• ∀s ∈ D ω , s + ω = + ω s = • ∀v 1 , v 2 ∈ D, s 1 , s 2 ∈ D ω , v 1 • s 1 + ω v 2 • s 2 = (v 1 + v 2 ) • (s 1 + ω s 2 )
Then, to prove Scott-continuity for a function f (representing here stepwise extension of usual functions or delay operator), we have to prove that for every chain C = {s 0 , s 1 , s 2 , . . .} of partially constructed inputs of the actor f , f ( s∈C s) = s∈C f (s).

• s∈C f (s) f ( s∈C s):
As s s∈C s, it follows directly from monotonicity since for each s ∈ C, f (s) f ( s∈C s).

• f ( s∈C s) s∈C f (s): Let w ∈ f (C); w is some atomic piece of information in the output. It comes from some finite approximation, say u, of the input: u s∈C s. Thus w ∈ f (u). Since u is finite and it is "included" in the supremum of the directed set, there is some v in C such that u v. By monotonicity,

f (u) f (v), thus w ∈ f (v). And since v ∈ C, f (v) s∈C f (s). 2
On the other hand, Signal polychronous operators are not flow functions. If they are seen as operators on sequences of values, they are even not (mathematical) functions.

Consider for example (refering to the definition of the merge operator provided in Section 2.8) behaviors on a set of variables {x, y, z}, x being defined as x := y default z, with different chains of tags for y:

• First, y has values 3, -2, -1, . . . respectively associated with the chain of tags (in the time domain N) {0, 1, 3, . . .}, and z has values 0, 0, 2, 1, . . . associated with the chain {1, 2, 3, 4, . . .}. Then x has values 3, -2, 0, -1, 1, . . . , associated with the chain of tags {0, 1, 2, 3, 4, . . .}.

• Second, y has the same values, 3, -2, -1, . . . , associated with the chain of tags {0, 1, 2, . . .}, and z has also the same values as above, associated with the same chain. In this case, x has values 3, -2, -1, 2, 1, . . . , associated with the chain of tags {0, 1, 2, 3, 4, . . .}.

Considering only sequences of values, y and z have the same ones in both cases, but the sequences for x are different (non-determinism).

An actor model for deterministic reaction

With respect to the polychronous model presented in Section 2.1, the symbol ⊥ is introduced to designate the absence of valuation of a signal:

⊥ ∈ D, D ⊥ = D ∪ {⊥}.
Definition 17 (Synchronized history, behavior). A synchronized history is a mapping s from a chain C ∈ C to the extended domain of values D ⊥ (s :

C → D ⊥ ).
A behavior on a finite set of variables V is a mapping b from V to the set of synchonized histories S, such that all histories have the same domain (which is the time domain of b): b : V → S, where ∀x 1 , . . . ,

x n ∈ V , tags(b(x 1 )) = . . . = tags(b(x n )) = tags(b) = C ∈ C.
The symbol ⊥ represents "meaningful" absence (Section 3.6). Then, Signal operators (or actors) are expressed as flow functions and the semantics is defined as a fixed-point semantics.

Let D ω denote the set of sequences of values (extended streams, or synchronized streams, or sometimes synchronized flows) in D ⊥ (the same notations are used for subsets of D). Signal operators are defined as functions

f : D ω 1 × . . . × D ω n → D ω n+1
where for all i, D i ⊆ D. These functions satisfy the following general rules:

• Termination: (∃i ∈ 1, . . . , n, s i = ) ⇒ f (s 1 , . . . , s n ) = • Stretching: f (⊥ • s 1 , . . . , ⊥ • s n ) = ⊥ • f (s 1 , . . . , s n ) A function f is synchronous iff it satisfies: ∀v 1 , . . . , v n ∈ D 1 , . . . , D n , x 1 , . . . , x n ∈ D ⊥ 1 , . . . , D ⊥ n , s 1 , . . . , s n ∈ D ω 1 , . . . , D ω n ,        • (∃v ∈ D n+1 , s ∈ D ⊥ n+1 )f (v 1 • s 1 , . . . , v n • s n ) = v • s and • ((∃i, j ∈ 1, . . . , n)(∃v ∈ D j )(x i = ⊥ ∧ x j = v)) ⇒ (f (x 1 • s 1 , . . . , x n • s n ) = )
Let a configuration of a set of variables be a simultaneous valuation (in D ⊥ ) of these variables. The absence configuration of a set of variables is the configuration for which all variables have the absence value.

The so-called stretching rule corresponds to a possible insertion of any finite number of the absence configuration in a given behavior (stuttering). This defines an equivalence relation ("equivalence modulo ⊥") on behaviors. Equivalence modulo ⊥ preserves the simultaneousness of valuations within a configuration and the ordering of configurations within a behavior. This equivalence modulo ⊥ corresponds to the stretch-equivalence of Section 2.2 and strict behaviors are those for which there is no absence configuration between two configurations which have valued variables (in D).

Stream operators

Synchronous functions are defined as stream operators (the absence value ⊥ serves only for stretching). They correspond to "delay insensitive" operations (the sequencing of computation is determined by the data flow).

Stepwise extension of function. Let f designate some n-ary total function: f :

D 1 × . . . × D n → D n+1 .
The corresponding actor, represented by its stepwise extension on streams, denoted by f ω , is the synchronous function

f ω : D ω 1 × . . . × D ω n → D ω n+1 that satisfies: ∀v 1 , . . . , v n ∈ D 1 , . . . , D n , s 1 , . . . , s n ∈ D ω 1 , . . . , D ω n , f ω (v 1 • s 1 , . . . , v n • s n ) = f (v 1 , . . . , v n ) • f ω (s 1 , . . . , s n ) Delay.
The actor representing the delay is the synchronous function delay :

D ω 1 × D 1 → D ω 1 that satisfies: ∀v 1 , v 2 ∈ D 1 , s ∈ D ω 1 , delay(v 1 • s, v 2 ) = v 2 • delay(s, v 1 )

Extended stream operators

Polychronous operators are defined on synchronized streams, taking into account the absence value ⊥.

Sampling. The actor representing the sampling operator is the function when

: D ω 1 × B ω → D ω 1 that satisfies: ∀x 1 ∈ D ⊥ 1 , s 1 , s 2 ∈ D ω 1 , • when(x 1 • s 1 , tt • s 2 ) = x 1 • when(s 1 , s 2 ) • when(x 1 • s 1 , ff • s 2 ) = ⊥ • when(s 1 , s 2 ) • when(x 1 • s 1 , ⊥ • s 2 ) = ⊥ • when(s 1 , s 2 )

Merge.

The actor representing the merge operator is the function

default : D ω 1 × D ω 1 → D ω 1 that satisfies: ∀v 1 ∈ D 1 , x 2 ∈ D ⊥ 1 , s 1 , s 2 ∈ D ω 1 , • default(v 1 • s 1 , x 2 • s 2 ) = v 1 • default(s 1 , s 2 ) • default(⊥ • s 1 , x 2 • s 2 ) = x 2 • default(s 1 , s 2 )
Example. For the two behaviors of the merge operator considered in Section 3.3:

• y having successive values (including the absence value) 3, -2, ⊥, -1, ⊥, . . . and z successive values ⊥, 0, 0, 2, 1, . . . , then x, defined as x := y default z, has successive values 3, -2, 0, -1, 1, . . .

• y having successive values 3, -2, -1, ⊥, ⊥, . . . and z successive values ⊥, 0, 0, 2, 1, . . . , then x has successive values 3, -2, -1, 2, 1, . . . It appears clearly that sampling and merge operators are now flow functions on the extended domain: they are synchronized flow functions. However, Signal programs may be non-deterministic. Thus they are not KPNs in general.

Deterministic and non-deterministic Signal programs

Note that the definition of determinism given in Section 2.6 takes into account the synchronizations between the considered variables (or, equivalently, the possible absence value for these variables).

As a consequence, all basic Signal equations (presented in 2.8) are deterministic. However, the determinism is not stable by composition and restriction.

Processes with feedback (typically, x := f (x)) or local variables (due to restriction) may be non-deterministic.

The input-free process (| x := x$ init 0 | y := y$ init 1 |) is a typical example of non-deterministic process. Both following output synchronized streams (represented here as sequences of pairs of values corresponding respectively to the outputs x and y) are examples of possible behaviors: (0, 1), (⊥, 1), (0, ⊥), (⊥, 1), . . . and (⊥, 1), (0, ⊥), (0, ⊥), (⊥, 1), . . . (since x holds a sequence of constant values 0 separated by any number of ⊥ and y holds a sequence of constant values 1 also separated by any number of ⊥). However, if we consider only streams (without the absence value), this process describes a flow function.

On the contrary, the process (| x := a | y := b |) (where a and b are two independent inputs) is deterministic (but it is not endochronous).

The process with trivial cycle x := a or x is non-deterministic since x can be tt or ff when a is ff .

The following process is also non-deterministic: (| x := a default ((x$ init 0) + 1) | b := x when ˆb |)/x. The internal signal x holds the value of the input a when there is an occurrence of a and then successive increments of this value (until the next occurrence of a). But since x is hidden from the outside, it is not possible to synchronize it, thus it can have any number of occurrences between successive occurrences of a, and b can output any of its values.

Other examples of non-deterministic processes are provided by partial definitions such as x ::= a (equivalent to x := a default x): it only defines x as�being equal to a when a is present; x may be present at other instants but its values at these instants are left undefined in this process. A given signal may have multiple definitions, obtained using several partial definitions (| x ::= a 1 | . . . | x ::= a n |) (note that in KPNs, no two processes send data to the same channel). Such multiple definitions are consistent if for every pair of equations x ::= a i , x ::= a j , when a i and a j are both present, they hold the same value. Technically, if one can prove that when ((a 1 when ˆa2 ) = (a 2 when ˆa1 )) ˆ= a 1 ˆ * a 2 , then the process (| x ::= a 1 | x ::= a 2 |) is equivalent to x ::= a 1 default a 2 .

Meaningful absence

Kahn Process Networks are characterized by their determinacy. In the execution model of a KPN, writes to the channels are nonblocking, but reads are blocking. When a read operation is executed on an empty input channel, the reading process should stall until the FIFO has sufficient tokens. It cannot do anything else, for example testing for absence, otherwise it would break determinacy.

Although Signal operators can be seen as flow functions on the extended domain, the additional value is an encoding for the absence, thus it may be necessary to test this absence value to get the result. This is the case, for example, for the merge operator x := y default z. If we add to this process two synchronous Boolean inputs, cy and cz, representing respectively the clocks of y and z (cy, resp. cz, is tt iff y, resp. z, is present), we get the following process (written in Signal syntax):

process merge = ( ? boolean cy , c z ; integer y , z ; ! integer x ; ) ( | x := y default z | cy ˆ= c z | y ˆ= when cy | z ˆ= when c z | ) ;
The process merge is a flow function. It can be implemented without testing the absence (test for absence is replaced by a test to the value ff of the added Boolean inputs). More generally, adding Boolean signals as inputs may be a way to transform a process into a synchronized flow function that does not need to test the absence of signals.

Syntactic equivalence

Syntactic equivalence rules apply to Signal programs. In particular, the following properties of composition and restriction are used to rewrite programs.

• Associativity: (| P | Q |) | R ≡ P | (| Q | R |). • Commutativity: P | Q ≡ Q | P .
• Idempotence: if P is a process without "side effects", then P | P ≡ P (in the full Signal language, side effects may be produced by calls to external system functions, for instance).

• Externalization of restrictions: if x is not a signal of P , then

P | Q / x ≡ (| P | Q |) / x.
As a consequence, expressions of composed processes can be normalized, modulo required substitutions of variables, as the composition of elementary processes, included in terminal restriction.

Expressions on signals can also be normalized thanks to properties of the operators.

• when is associative and right commutative:

(x when y) when z ≡ x when (y when z) ≡ x when (z when y).

• default is associative: (x default y) default z ≡ x default (y default z).

• default can be written in exclusive normal form:

x default y ≡ x default (y when (y ˆ-x)).

• default commutes in exclusive normal form: if x ˆ * y ˆ= ˆ0 (x and y are exclusive), then x default y ≡ y default x.

• when is right distributive over default: (x default y) when z ≡ (x when z) default (y when z).

Then every signal x can be rewritten as follows:

x := (e 1 when c 1 ) default . . . default (e n when c n ) default ((x$ init v) when c n+1 ), where the e i are synchronous expressions with no delay and the c i are signals of type event representing mutually exclusive clocks (c n+1 can be the null clcok). As a fundamental characteristic, the equational nature of the Signal language makes it possible to consider the compilation of a process as a composition of endomorphisms over Signal processes.

Clock calculus

The clock calculus [START_REF] Amagbegnon | Implementation of the dataflow synchronous language Signal[END_REF] is one of the formal tools allowing to rewrite Signal processes, in order to make explicit synchronization relations and to organize the "control" of processes as a clock hierarchy.

Clock relations

Synchronisation relations (or clock relations) associated with basic Signal expressions P are described in Table 1 as Signal expressions Cl(P ). The notations [: z] and [/: z] are other forms for, respectively, when z and when not z (which are signals of type event representing clocks).

Moreover, for every Boolean signal b, the following clock relations are stated:

[: b] ˆ+ [/: b] ˆ= b [: b] ˆ * [/: b] ˆ= ˆ0
(the clock of a Boolean signal b is partitioned into its exclusive subclocks [: b] and [/: b], which represent the instants at which the signal b is present and has, respectively, the values tt and ff ).

The so defined transformation Cl satifies the following property making Cl(P ) an abstraction of P :

(| Cl(P ) | P |) ≡ P .

x := f (y 1 , . . . , y n ) x ˆ= y 1 ˆ= . . . ˆ= y n x := y$ init v x ˆ= y x := y when z x ˆ= y ˆ * [: z] x := y when not z x ˆ= y ˆ * [/: z] x := y default z x ˆ= y ˆ+ z (| P | Q |) (| Cl(P ) | Cl(Q) |) P / x Cl(P ) / x
Note that the variables involved in clock relations are "clock variables" ˆx: for instance, x ˆ= y ˆ+ z can be written equivalently ˆx ˆ= ˆy ˆ+ ˆz. Clock variables can be seen as Boolean variables (as a Boolean variable, ˆx will be denoted by x) related in a system of Boolean equations. Clock operators ˆ * , ˆ+, ˆ-correspond respectively to Boolean operations of conjunction (∧), disjunction (∨) and difference (x \ y = x ∧ ¬y, where ¬ is the negation).

Clock hierarchy

From clock relations, the clock calculus has to determine how clocks can be computed. For that purpose, it builds a (well-formed) clock hierarchy and tries to define clocks with Boolean functions. The definition of a well-formed clock hierarchy is made more precise below. Initially, each clock is an isolated node of the clock hierarchy (it is a root of an elementary clock tree reduced to this node).

To reduce the number of trees by placing clocks in the clock hierarchy, the clock calculus considers a set F of Boolean signals the value of which is considered "free" (for the clock calculus The depth of the hierarchy may grow since the clock ĉ1 may be itself dominated by another clock.

Then, clocks written as Boolean formulas (using operators ∧, ∨ and \) are set in the clock hierarchy according to the following rules (( ˆ ) * designates the transitive closure of ˆ ):

• If x = f (x 1 , x2 )
, where f is a Boolean operator, and there exists c such that c ( ˆ ) * x1 and c ( ˆ ) * x2 (x 1 and x2 are placed in the same tree of the clock hierarchy), then x is written in canonical form x = g(ŷ 1 , . . . , ŷn ) (using BDDs) [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF]. The clock g(ŷ 1 , . . . , ŷn ) is either the null clock, or the clock c, or is transitively dominated by c. If such a c does not exist, x remains as a root of the clock hierarchy (with an associated clock formula-it is not a free clock).

• If x = g(ŷ 1 , . . . , ŷn ) is a canonical form with n ≥ 2 and there exists d such that d ( ˆ ) * ŷi for all ŷi in ŷ1 , . . . , ŷn , then there exists a lowest clock c that dominates those ŷi , and the following relation is added: c ˆ x. The direct parent of the clock x in the tree is the least common ancestor of clocks ŷi (the insertion of a formula into a tree can be seen as a factorization).

This again reduces the number of trees.

A clock hierarchy constructed with these rules is well-formed in the following sense: Let min ˆ denote the set of minimal elements for the relation ˆ . The roots of the clock hierarchy (clocks which have no higher clock) are the clock equivalence classes of minimal elements for the relation ˆ :

0 ˆ = {c ∼ | c ∈ min ˆ }.
A tree of root c in the clock hierarchy, denoted by c ˆ , is the tree from c in the relation ˆ :

c ˆ = {(c, d)} ∪ d ˆ such that c ˆ d.

Definition 20 (Hierarchical process).

A process is hierarchical iff its clock hierarchy has a unique root.

Canonical forms are given to clock formulas placed in a given tree. The roots which have no associated clock formula are considered free. Concerning roots with associated formula, classical Boolean reductions are applied on these formulas in order to merge trees and to iterate, if possible, the "placing" process in the clock hierarchy. The rewriting of formulas is limited using a fixed maximal depth in the syntax of formulas to avoid termination problems.

In some contexts, the clock difference operator, which may appear in clock expressions, may be problematic since it refers to clock negation. However, even if the canonical forms of clocks (in a given clock tree) use the clock difference operator, this operator could be easily eliminated and such a canonical form can be expressed as a sum of products of conditions placed in the considered tree (disjunctive form) [START_REF] Besnard | Compilation de SIGNAL : horloges, dépendances, environnement[END_REF]. On the other hand, if a clock formula is associated with a root and this clock formula is a clock difference, it is not possible to eliminate it without referring to the absence (the negation) of a clock. We say that the clock hierarchy is disjunctive if it has no root clock the expression of which is defined using clock difference.

Definition 21 (Well-clocked process). A process is well-clocked if its clock hierarchy is well-formed and disjunctive.

Note that the clock calculus does not reach completeness: it is rather a heuristic calculus aimed at efficient compilation (of a control flow graph). Thus, in some particular cases, it may fail to provide an explicit form for some clock equations.

When the clock hierarchy computed by the clock calculus is composed of a single tree (i.e., there is a unique clock k with no higher clock and such that all other clocks are lower than k), then it means that all clocks can be computed by explicit functions from the root clock. Thus the process has a fastest rated clock (which is the root clock) and the status (presence/absence) of all signals is expressed as a flow function. From their Boolean expression, clocks can be expressed as Booleans the presence of which is also expressed, recursively, by a Boolean; and the test for presence/absence is replaced by a test of value of a Boolean, which, thanks to the clock hierarchy (which represents an inclusion relation), is conditioned itself by the Boolean clock of this Boolean.

The equations defining the value of the signals are themselves conditioned by the Boolean clock of these signals. Thus, when the clock hierarchy is composed of a single tree, and provided that there is no cyclic definition, thanks to syntactic equivalence rules and clock calculus, the whole process is rewritten as a synchronized flow function and the absence value has never to be tested. Detection of cyclic definitions corresponding to possible "deadlocks" is briefly described below, Section 3.8.4 (refer to this section for the definition of an acyclic process-the intuition about that may be sufficient in the following).

As a consequence, the input streams of the process (the sequences of input values, independently of their relative presence/absence) are sufficient to completely determine the behavior, in synchronized histories, of the process.

Definition 22 (Compilable process).

A process is compilable iff it is wellclocked and acyclic.

Proposition 5. Let P be a compilable process. There exists I ⊂ vars(P ) such that P is deterministic on I.

Proof. For I = vars(P ), the process P is immediately deterministic. We can remove from I the variables linked in all behaviors, P remains deterministic (x is linked if there exist y i ..y n ∈ I such that x = f (y i ..y n )). 2

Acyclic process

Detection of cyclic definitions requires the building of a directed graph representing precedence relations between signals and clocks. Associated with the clock hierarchy, this "precedence graph" is the basic formal tool for the internal representation of programs. Precedence relations are conditioned by the clock at which the precedence holds: x precedes y at clock ĉ is represented as ĉ : x → y. It expresses that for all instants of the clock ĉ, the computation of y cannot be performed before the value of x is known. Precedence relations associated with basic Signal expressions P are described in Table 2.

Process P Precedence x := f (y 1 , . . . , y n ) x : y 1 → x, . . . , x : y n → x x := y$ init v x := y z

x : y → x x := y default z ŷ : y → x, (ẑ ˆ-ŷ) : z → x Moreover, for each signal x, there is a precedence x : x → x, and for each clock x n-1 → x 1 is called a pseudo cycle. Since precedences are conditioned by clocks, pseudo cycles are not necessarily true cycles: it may be the case that there is no common instant at which all the precedences along the cycle are effective. A process P is acyclic, or deadlock-free, iff for all pseudo cycles ĉ1 : x 1 → x 2 , ĉ2 : x 2 → x 3 , . . . , ĉn-1 : x n-1 → x 1 in its associated precedence graph, the intersection of clocks ĉ1 ˆ * ĉ2 ˆ * . . . ˆ * ĉn-1 is equal to the null clock.

Process network

Networks of processes are constructed with (synchronous) composition of polychronous processes. The compositional design of networks requires for component processes and the way they communicate to verify composition properties.

Endochronous process network. The following result relates composition of endochronous processes and KPNs.

Composition of endochronous processes as KPN. .../... Notice the subtle "rewriting" condition: a Signal specification defines implicit clock and causality relations whose structure can both be used to verify the formal properties of its components (endochrony) but, once automatically inferred, can also be used to refine the original specification into one which, in particular, syntactically materializes its KPN structure (see Section 3.8.3). Theorem 1. A Signal specification denotes a Kahn Process Network if it can be rewritten, using syntactic equivalence and clock relations, as the composition of endochronous processes, whose master clocks are free or input signals.

Proof. This is a direct consequence of the results described in Section 3.8.2, which shows that an endochronous process is obtained from a Signal specification by an analytic rewriting that consists of a well-formed clock hierarchy (that defines its control flow) and an acyclic causality graph (that defines its static schedule).

By Proposition 6, such a process is deterministic on a set of signals I which can be regarded as its input triggers. Now, plunge a set of such deterministic processes in an asynchronous network by interfacing their input triggers (the Is) with a idealized infinite FIFO buffers (which employ a blocking read method). By the definition of [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], they now form a deterministic process network over continuous flows of events.

2

We observe, however, that the converse of Theorem 1 is not true: some Khan networks may not be rewritten as the asynchronous composition of endochronous Signal processes. This is essentially due to the limitations of the clock calculus, which uses symbolic graph and Boolean reasoning. Also, Theorem 1 does not express the fact that the fixpoint semantics of Signal processes always coincides with its "intersection" semantics, although it might, but only for deadlock-free processes.

Among the corollaries of Theorem 1, we further the discussion by considering classes of such endochronous process networks with particularly interesting formal properties that can be decided using Signal's clock calculus and, similarly, obtained by rewritting.

Endo-isochrony. Endo-isochrony is a property on the composition of endochronous processes. It ensures that a system composed of endochronous processes is equivalent in its synchronous and asynchronous composition.

Definition 23 (Endo-isochronous process). Let P 1 and P 2 be two processes defined respectively on V 1 and V 2 . They are endo-isochronous iff P 1 , P 2 and (P 1|V 1∩V2 | P 2|V 1∩V2 ) are endochronous and (P 1|V 1∩V2 | P 2|V 1∩V2 ) is acyclic.

Proposition 7. If P 1 and P 2 are endo-isochronous, their asynchronous composition P 1 || P 2 is flow-invariant.

Proof. If P 1 and P 2 are endo-isochronous then they are endochronous, thus P 1 || P 1 and P 2 || P 2 are flow-invariant. Since flow-invariance is compositional,

P 1 || P 2 is flow-invariant. 2
Unfortunately, ensuring endo-isochrony may be costly on large systems of components since it requires to ensure endochrony for each component and for each pair of components. Hence the interest of considering polyendochronous processes (cf. Section 2.7). • And so on.

Polyendochronous systems.

In all cases, it is shown that the variables of a subdomain use the tag support of their referent, namely:

∀ρ ∈ vars(P | Q), b | ρ ≷ c | ρ . 2
Polyendo-isochrony. Like endo-isochrony for endochronous processes, polyendoisochrony is a property on the composition of polyendochronous processes. It ensures that a system composed of polyendochronous processes is equivalent in its synchronous and asynchronous composition.

Definition 24 (Polyendo-isochronous process). Let P 1 and P 2 be two processes defined respectively on V 1 and V 2 . They are polyendo-isochronous iff P Proof. By definition, a polyhierarchical process P is a composition of processes P i which are compilable and hierarchical, thus endochronous. Since endochrony implies polyendochrony and polyendochrony is stable by composition, the composition P of processes P i is polyendochronous.

Let P i and P j be two endochronous subprocesses from the composition P | Q, that share some variable x the clock of which is x. The processes P i and P j have (respectively) r i and r j as roots and synchronize on x with (respectively) c i and c j . Since they are hierarchical, these clocks can be computed from the roots. r i r j {c i , x, c j } Since P i | P j is compilable, the clocks c i and c j have disjunctive forms. Thus, the clock x can be calculated either, as c i , only from clocks recursively dominated by r i , or, as c j , only from clocks recursively dominated by r j . Thus, any reaction initiated in P i that leads to x can locally decide to wait for a rendez-vous with a reaction of P j containing x. Since P i and P j are well-formed, the equation x = ˆ0 is excluded, and the reaction can thus occur. And since P i | P j is acyclic, the rendez-vous of c i and c j cannot be locked by a deadlock.

For each such pair of processes P i , P j from P | Q, it is thus shown that this pair is non-blocking. The composition P | Q is non-blocking.

Finally, this corresponds to the criteria of polyendo-isochrony.

In [? ], the authors proposed an operational method to characterize weakly endochronous processes. There technique is based on the construction of "generator sets" composed of partial reactions. These generator sets contain minimal synchronization patterns that characterize all possible reactions of a process. A process is weakly endochronous when its generator set is free of forced absence constraints. However, the proposed algorithms to compute generator sets involve an exploration of combinations of generators that can be very costly, with questionable scalability for realistic programs. To our knowledge, the method has not been implemented. On the contrary, the characterization of the polyendochronous processes that we propose, pertaining to the polyhierarchical property, is based on the calculation of the clock hierarchy, which has been proved as a very efficient and scalable technique [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF]. It integrates smoothly within the Polychrony framework, which already uses the hierarchical criterion to characterize endochrony. Testing polyendochrony and generating code for polyendochronous processes (see Section 4) are now available in Polychrony.

A polyendochronous example. We consider a toy Signal example so that it can be easily demonstrated and understood. It is composed of specific simple devices: a writer and two instances of a reader. A realistic polyendochronous use case, namely the simulation model for a loosely time-triggered architecture (LTTA), could be obtained from more general versions of such devices, together with a model of bus: the LTTA [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF][START_REF] Glouche | A module language for typing SIGNAL programs by contracts[END_REF] is composed of a writer, a bus and a reader, each of them being paced by its own clock.

Here, our writer is paced by some Boolean clock cw ; it delivers its input data xw on its output yw at the instants at which its clock cw is tt (other data values are lost): The reader is paced by a Boolean clock cr . It reads data values on its input xw at the instants at which its clock cr is tt. At these instants, it delivers its scribed in [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF]: sequential code generation, clustered code generation with static scheduling, clustered code generation with dynamic scheduling, distributed code generation, as well as multithreaded, multi-core core generation [START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF][START_REF] Yang | Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study[END_REF].

All these strategies consist of different source to source transformations. All of them proceed by analytic rewriting that refine a Signal process with an explicit control flow (obtained from the inference of hierarchical clock relations) and by a static schedule (obtained by the inference of causality relations). Additional user directives allow to map such processes on abstract architecture descriptions and interconnect them, before imperative code is finally generated.

In this section, we consider the latest of these strategies: to generate multithreaded code for polyendochronous processes. We make the choice of focusing on the model transformations that come into play in its elaboration, rather than on the code generated that is generated, as the aim poly-endochrony is to exploit parallelism at its finest grain of modularity, rather than performing runtime optimization (using, e.g., WCET analysis and real-time schedule synthesis).

After the clock calculus, a program P is reorganized as a composition of processes, P = (| P 1 | P 2 | . . . | P n |), each one structured around a clock tree. We have thus a composition of trees (the hierarchy is a set of trees). Each tree is dominated by a clock, which is a local root. Testing polyendochrony then consists in verifying that no clock formula associated with a given root is recursive (in this case, the program could be non-deterministic), and that clock formulas associated with roots do not use the clock difference operator (ˆ-), i.e., there is no reference to the absence of a root clock (the absence of an input cannot be tested).

So we consider the program P as polyendochronous, with Clk 1 ˆ= Clk 2 as clock constraint, with Clk 1 being a clock in the subtree corresponding to P 1 and Clk 2 a clock in the subtree corresponding to P 2. Such a constraint induces a synchronization between two parts (P 1, P 2) of the program when Clk 1 or Clk 2 occurs. The principle of the code generation for polyendochronous processes is based on the existing distributed code generation [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF], but with the additional resynchronization of parts of the application induced by the constraints on clocks (Clk 1, Clk 2) not placed in the same clock trees.

To prepare the code generation, the graph is modified by adding nodes to express the "rendezvous" between different parts of the application. A technique quite similar to the synchronization by semaphores is used. For that purpose, three intrinsic predefined processes are considered: pK Send (), pK Receive() and pK RendezVous(). They are added as described below in the graph and explicit dependencies are also added. The pK Send will allow to express to another part (say, P 2) that the current part (P 1) is at its point of rendezvous; the pK Receive will specify that the current part is waiting for the rendezvous with another part; finally, the pK RendezVous allows to manage the coherence of the logical instants between different parts.

For Clk 1, the following definitions at clock Clk 1 are added: onClk1 : : ( | n11 : : rdv1 := pK Send ( )

• one task for the cluster of state variables (i.e., Q1$),

• one task that manages the steps (Q1iter ).

Synchronization between these tasks is obtained by semaphores (one semaphore per task). Such a task has the following scheme: WAIT; code ; SIGNAL where:

• "WAIT" ia a set of "wait" instructions on the semaphore associated with the task. The number of "wait" is equal to the number of predecessors in the graph of the clusters (in the considered partition).

• "code" is the code of the cluster or the code of the read/write for the inputs/outputs; it is empty for the task that manages the steps.

• "SIGNAL" is a set of "signal" instructions on semaphores. The number of "signal" is equal to the number of successors in the graph of the clusters. For example, consider a task T j that implements the cluster Cj, with Sj as associated semaphore. If Cj depends on the cluster Ci, implemented by the task T i, the instruction "signal(Sj)" will be generated at the end of the task T i.

The iterate task (Q1iter ) waits for the end of the other tasks (end of a logical instant) and signals the beginning of a new instant to the clusters without predecessor. In this way, the presented mechanism ensures the dynamic scheduling of tasks. Moreover, to ensure a correct resynchronization, this code generation has to be completed specifically for the partitions involved in the clock constraint. For such a partition (Q1 for example), the following actions are applied:

• a local step counter (which counts logical instants) is introduced to resynchronize the partition Q1 with the other one (Q2 );

• the code associated with the pK Send () intrinsic process, for example rdv 1 := pk Send (), consists in the assigment of the value of the local step counter to rdv 1;

• the pK receive() intrinsic process does not produce any code;

• and the pK RendezVous(rdv 1, rdv 2) produces the generation of (rdv 2rdv 1) "⊥ instants" if the rdv 1 is lower than rdv 2, where rdv 2 is sent by the other partition (Q2 ) and its value is the local step counter of this partition (indeed, in this case, the partition Q2 has taken some advance on the partition Q1 ).

This method may be easily generalized for n constraints on a same clock. For that, the pK RendezVous node has a variable number of inputs depending on the number of constraints on the same clock. Typically, a constraint on three clocks (Clk 1 ˆ= Clk 2 ˆ= Clk 3) placed in different clock trees induces the definition of the following nodes:

• n13 :: pK RendezVous(rdv 1, rdv 2, rdv 3) in the hierarchy of P 1,

• n23 :: pK RendezVous(rdv 2, rdv 1, rdv 3) in the hierarchy of P 2,

• and n33 :: pK RendezVous(rdv 3, rdv 1, rdv 2) in the hierarchy of P 3.

For example, pK RendezVous(rdv 1, rdv 2, rdv 3) in the hierarchy of P 1 produces the generation of (m -rdv 1) "⊥ instants" if the rdv 1 is lower than m = max (rdv 2, . . . , rdv n), where the values rdv 2, . . . , rdv n are sent by the other partitions.

KPN are (extended) Signal programs

In Section 3, we have considered the question "are Signal programs KPNs?" In this section, we consider the more or less inverse interrogation: "how can KPNs be viewed as Signal programs?" In particular, which extensions to Signal could be required?

As a preliminary remark, it should be noticed that an actor in a KPN can be defined recursively. This is not the case of Signal programs (though bounded recursion would not be conflicting with the principles of the language).

We first give the principle of the description of a bounded FIFO in Signal (Section 5.1). Then, in Section 5.2, we propose an extension of Signal to handle asynchronous communications and in Section 5.3, we revisit asynchronous composition. Associated with counters of events, this allows to express synchronized Signal programs from KPNs (Section 5.4).

Bounded FIFO

Recall that, in the implementation model of a KPN, actors communicate via FIFO channels. If the specification of general unbounded FIFOs is out of the scope of the Signal language (the purpose of which is mainly the description of real-time safety-critical applications), on the other hand, bounded FIFOs can be specified as Signal programs.

The following program partly describes a FIFO buffer of size fifo size: The equation counter ˆ= when (counter <= n), as an assertion, constrains the signal counter to be present only when its value is less than or equal to n. Then, a "synchronized program" can be expressed as a Signal program with unbounded FIFOs (a KPN), composed with a set of such bound constraints.

Conclusion

In this paper, we examined the polychronous model of the synchronized dataflow language Signal with respect to the well-known model of Kahn Process Networks. In particular, we tried to answer two questions:

1/ When are Signal programs Kahn Process Networks? 2/ When can Kahn Process Networks be seen as Signal programs?

To answer the first question, we have shown the somewhat unexpected role of the Signal clock calculus. To answer the second one, we have proposed a small syntactic extension of the Signal language that makes the idealized, mathematical, notion of flow-equivalence syntactically explicit.

The "takeaway" of this comparison is to invite the reader enrich implementation techniques used by one's community with analytic techniques used by the other's. From a theoretical point of view, the extension of Signal proposed in Section 5 could for instance lead one revisit the polychronous model. Relations on flows, together with event counters, could be used to express unbounded asynchronous or weakly synchronous communication (e.g. loosely time-triggered systems), and/or to redefine synchronous communication from more primitive operations. From a practical point of view, we have described program transformation techniques for the special class of networks called "polyendochronous processes" in the Polychrony toolset.

  For a variable x ∈ V , b(x) is the signal (timed history) designated by x in b. We write vars(b) to denote the domain of b and tags(b) to denote its tags (or tag support): tags(b) = x∈vars(b) tags(b(x)). The relation ≤ tags(b) on tags(b) is the partial order relation defined by the union of order relations on chains of tags of the signals of b. The behavior on the empty set of variables is denoted by ∅. For any behavior b on V , we write b |V for the projection of b on a set of variables V ⊆ V . We write B |V for the set of behaviors on variables V .

Figure 2 :

 2 Figure 2: Synchronous composition of two behaviors b, c forming P |Q: signals common to P and Q (x, y) must hold the same tags and values whereas others (i, j) need not

Definition 6 (Figure 3 :

 63 Figure 3: A depiction of stretching the time tags of behavior b as the behavior c, to allow for a scalable refinement of b as d and partial synchronization to a contextual "hyper-period" (z)

Definition 8 (

 8 Flow-equivalence). Two behaviors b 1 and b 2 are flowequivalent, written b 1 ≈ b 2 , iff there exists a behavior c such that c b 1 and c b 2 .

Figure 4 :

 4 Figure 4: Asynchrony as the relaxation of synchronization relations. Relaxation allows to individually stretch the signals a and b of flow-invariant processes P and Q. While P alternates a and b depending on the values of x, process Q instead needs to sample a or b depending on the values of y. Relaxation is implemented by the insertion of a FIFO protocol between P and Q. The FIFO itself can be defined as a flow-invariant process.

Proposition 3 . 2 Lemma 1 ( 2 Proposition 4 .

 32124 A process which is polyendochronous on I is flow-invariant on I. Proof. Let P be a polyendochronous process on I, and b, c such that (b |I ) ≈ (c |I ). Polyendochrony ensures that for each x ∈ vars(P ) we have b | x ≷ c | x . Thus (b |{x} ) ≷ (c |{x} ). And from properties of flow-equivalence (cf. 2.3), b ≈ c. Lemma of tag supports). Let P be a polyendochronous process on I, for each behavior b of P , tags(b) = tags(b |I ). Proof. Suppose there is a variable r ∈ vars(P ), a behavior b ∈ P and a tag θ ∈ tags(b | r ) such that θ ∈ tags(b |I ). The behavior prefix b ≤θ is not stretchequivalent to the behavior prefix b <Θ . However, prefixes (b |I ) ≤θ and (b |I ) <θ are stretch-equivalent since θ does not belong to tags(b |I ). Thus, for Θ = {t ≤ θ} and Θ = {t < θ}, we have (b |I ) ≤Θ ≈ (b |I ) ≤Θ and (b | r ) ≤Θ ≷ (b | r ) ≤Θ . This contradicts the hypothesis of polyendochrony, thus, ∀t ∈ tags(b), t ∈ tags(b |I ). In the other side, it is obvious that ∀t ∈ tags(b |I ), t ∈ tags(b). A process which is polyendochronous on I is deterministic on I. Proof. Consider behaviors b, c such that b |I ≷ c |I : behaviors b and c are stretch-equivalent on I. Thus their tag supports restricted on I are isomorphic, and from lemma of tag supports, tag supports of the whole behaviors are also isomorphic. Moreover, we have b |I ≈ c |I . Thus, from polyendochrony, we get ∀r ∈ vars(r), b | r ≷ c | r . In conclusion, tag supports of behaviors b and c are isomorphic and the signal values are preserved between b and c. Thus b ≷ c. 2

Figure 6 :

 6 Figure 6: A depiction of some possible behaviors of delay, sampling and merge equations.

Definition 18 (

 18 Clock hierarchy). A clock hierarchy is a relation denoted by ˆ (dominate) on the set of clocks (a given clock being associated with synchronous signals). A clock c dominates a clock d (c ˆ d) if d is computed as a function of Boolean signals the clocks of which are c and/or clocks recursively dominated by c (d is hierarchically lower than c).

  ): input Boolean signals, delayed Boolean signals, Boolean signals defined by non-Boolean predicates (for example, c := a > b). Let c ∈ F be such a free variable. The clock of c, ĉ, is partitioned into its subclocks [: c] and [/: c]. This partition is represented by a tree by adding the following elements in the dominate relation (which is an inclusion relation): ĉ ˆ [: c] and ĉ ˆ [/: c] (note that if c�is defined by a > b for instance, then ĉ = â = b). Generally, let d ∈ F be a free variable that partitions a clock ĉ1 (ĉ 1 = d), the following relations apply: ĉ1 ˆ [: d] and ĉ1 ˆ [/: d].

Definition 19 (

 19 Well-formed clock hierarchy). A clock hierarchy is illformed iff either there exists c such that [: c] ˆ ĉ or [/ : c] ˆ ĉ, or there exists b 1 = f (c 1 , c 2 ), where f is a Boolean operator, and b 2 , such that b 1 ˆ b 2 , where b 2 ˆ c 1 , b 2 ˆ c 2 and ∀b such that b ˆ c 1 and b ˆ c 2 , b ˆ b 2 . A well-formed clock hierarchy is a clock hierarchy which is not ill-formed.

  [: b] (respectively, [/: b]), there is a precedence [: b] : b → [: b] (respectively, [/: b] : b → [/: b]). Note that no precedence is associated with the delay operator. From basic precedence relations, a simple path algebra can be used to verify the absence of cycles: ĉ : x → y and d : y → z ⇒ (ĉ ˆ * d) : x → z ĉ : x → y and d : x → y ⇒ (ĉ ˆ+ d) : x → y A precedence path ĉ1 : x 1 → x 2 , ĉ2 : x 2 → x 3 , . . . , ĉn-1 :

Proposition 8 .

 8 The synchronous composition of two polyendochronous processes P and Q is polyendochronous if the clock hierarchy of P | Q is wellformed.Proof. Let P and Q be two polyendochronous processes and b, c behaviors of P | Q. There exist b P and c P ∈ P such that b |vars(P ) = b P and c |vars(P ) = c P . Similarly, there exist b Q and cQ ∈ Q such that b |vars(Q) = b Q and c |vars(Q) = c Q . Since I is a subset of vars(P )∪vars(Q), we have b P |I ⊆ b |I , b Q |I ⊆ b |I , c P |I ⊆ c |I and c Q |I ⊆ c |I . The proposition b |I ≈ c |I implies b P |I ≈ c P |I and b Q |I ≈ c Q |I . P and Q are polyendochronous, thus, ∀r ∈ vars(P ), ∀r ∈ vars(Q), (b P | r ) ≷ (c P | r ) and (b Q | r ) ≷ (c Q | r). Or: ∀r ∈ vars(P ), ∀r ∈ vars(Q), (b |vars(P ) | r ) ≷ (c |vars(P ) | r ) and (b |vars(Q) | r ) ≷ (c |vars(Q) | r ). For all r ∈ vars(Q) \ vars(P ), we have (b |vars(P ) | r ) ≷ (c |vars(P ) | r ), since the sets tags(b |vars(P ) | r ) and tags(c |vars(P ) | r ) are empty. Thus we can write: ∀ρ ∈ vars(P | Q), (b |vars(P ) | ρ ) ≷ (c |vars(P ) | ρ ) and (b |vars(Q) | ρ ) ≷ (c |vars(Q) | ρ ). Finally, if the clock hierarchy of P | Q is well-formed, we can find all couples of variables of P | Q such that x ∈ y. • If x and y are both in vars(P ), then tags(b(x)) ⊆ tags(b(y)) for all behaviors b ∈ P . • The same results are obtained for x, y in vars(Q). • If x is in vars(P ) \ vars(Q) and y in vars(Q) \ vars(P ), there exists a variable z in vars(P ) ∩ vars(Q) such that tags(b(x)) ⊆ tags(b(z)) for all b in P and tags(c(z)) ⊆ tags(c(y)) for all c in Q. So for all d in P | Q we have tags(d(x)) ⊆ tags(d(y)).

  process w r i t e r = ( ? integer xw ; boolean cw ; ! integer yw ; ) ( | xw ˆ= cw | yw := xw when cw | ) ;

5 . 4 .

 54 process FIFO = { type m e s s a g e t y p e ; integer f i f o s i z e ; ( ? m e s s a g e t y p e m e s s i n ; ! m e s s a g e t y p e m e s s o u t ; ) ( | i n d e x := ( ( p r e v i n d e x + 1 ) when ˆm e s s i n ) default ( ( p r e v i n d e x -1 ) when ˆm e s s o u t ) default p r e v i n d e x Back to synchronized flows Let us associate each signal x with a counter #x of its valued events. This counter can be defined by the signal nx in the following process: (| nx := ((znx + 1) when ˆx) default znx | znx := nx $ init 0 |)/znx A bounded FIFO between y and x, with n slots, can then be defined as: (| x :-y | (| counter := #y -#x | counter ˆ= when (counter <= n) |) |)

  Definition 11 (Endochronous process). A process P defined on V is endochronous on I ⊆ V , I = {i 1 , . . . , i n }, if and only if the function Φ : P → P |{i1} × . . . × P |{in} such that Φ(b) = (b |{i1} , . . . , b |{in} ) is injective (and thus bijective, since it is necessarily surjective

Table 1 :

 1 Clock relations associated with a process

	Process P	Clock relations Cl(P )

Table 2 :

 2 Precedence relations associated with a process

  1 , P 2 and (P 1|V 1∩V2 | P 2|V 1 ∩V2 ) are polyendochronous and (P 1|V 1∩V2 | P 2|V 1∩V2 ) is acyclic. Proposition 9. If P 1 and P 2 are polyendo-isochronous, their asynchronous composition P 1 || P 2 is flow-invariant. Proof. If P 1 and P 2 are polyendo-isochronous then they are polyendochronous, thus P 1 || P 1 and P 2 || P 2 are flow-invariant. Since flow-invariance is compositional, P 1 || P 2 is flow-invariant.

2

Polyhierarchy. Just like the hierarchical criteria of a compilable process may be used to test endochrony, we define a polyhierarchical property to test polyendochrony. Polyhierarchy is defined (recursively) as follows:

Definition 25 (Polyhierarchical process). If P is a compilable and hierarchical process, then it is polyhierarchical. If P and Q are polyhierarchical processes and

P | Q is compilable, then P | Q is polyhierarchical.

Then, we have the following properties for polyhierarchical processes: Proposition 10. If P is a polyhierarchical process, then P is polyendochronous. If P and Q are polyhierarchical processes and P | Q is compilable, then P and Q are polyendo-isochronous.

http://polychrony.inria.fr

Proposition 6. Let P be a process which is compilable and hierarchical. There exists I ⊂ vars(P ) such that P is endochronous on I.

Proof. Let r ∼ be the single root of the clock hierarchy of P . P is compilable, thus it is deterministic on some set I. If a representative of the root, r, belongs to I, the result is immediate: r is present in each reaction, thus for any behavior b in P , tags(b) = tags(b |{r} ) = tags(b |I ). If no representative of the root, r, is is I, then r is linked: there exist y i ..y n ∈ I such that r = f (y i ..y n ). Then tags(b) = tags(b |{yi..yn} ) = tags(b |I ).

2

The roots of the clock hierarchy are also called master clocks. When its clock hierarchy has several master clocks, and there is no additional "clock constraint" (several formulas associated to a given clock, but which have not been proved equivalent), a process may be further parameterized so that it becomes endochronous: an example has been given in Section 3.6. This transformation can be named "endochronization", or "lustrage" (the resulting process can be seen as a Lustre program).

A small example

To illustrate clock calculus and its results, we consider as simple example the process N events presented in Section 2.10.

First, the clock calculus establishes clock relations and applies elementary clock reductions. The process is rewritten as the following set of equations (texts between "%" are comments, IOStepN events is the union of the clocks of the interface signals):

Then clock static resolution is applied and clock hierarchy is refined. The process is rewritten as follows:

The clock hierarchy has a single root (which is here the clock of an internal signal): this clock ˆcnt dominates clocks of n, i and IOStepN events.

Finally, event clocks are transformed into Boolean clocks. The process is rewritten as follows (where, for example, the Boolean clock C IOStepN events is now written as a Boolean expression):

input data on its output xr ; at the other instants of its clock, it delivers again the previous value (which has to be memorized):

process In this composition, the instants of the three Boolean clocks, cw , cr1 and cr2 , are left completely free, however, the instants at which they are tt are constrained to be strictly synchronous.

The following clock hierarchy is obtained by applying clock calculus:

ˆcw

The clock hierarchy has three free clocks as roots, which are the clocks of the Booleans cw , cr1 and cr2 . However, clock constraints apply on subclocks of them. In some sense, the clock hierarchy appears as composed of three trees, each of them corresponding to an endochronous process, connected to the others at two rendezvous points. This observation justifies a possible code generation strategy for polyendochronous processes, which will be described in the next section.

From equations to process networks by model transformation

Different strategies may be applied to implement "endochronous process networks". These strategies, available in the Polychrony toolset, are de- Note that two additional syntactic notations, not used so far, appear here. These are first the notation x --> y, which expresses an explicit dependency between signals x and y; and the notation l :: P , which associates the label l with the process P (this label, viewed as a signal of type event, may be used in particular in synchronizations and explicit dependencies) [START_REF] Besnard | SIGNAL V4-INRIA version: Reference Manual[END_REF].

Symmetrically, for Clk 2, the following definitions at clock Clk 2 are added: Note that this writing induces that the signal rdv 1 (resp., rdv 2) becomes an output signal of Q1 (resp. Q2) and an input of Q2 (resp. Q1).

At this step, the technique used for distributed code generation in Polychrony is applied [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF], considering that each hierarchy Q1, Q2, P 3, . . . , P n will run on a specific processor. In this case, the purpose is mainly to partition the application and the processors will be virtual ones. The distribution technique requires in particular the application of a clustering on each partition. A cluster consists of all the nodes that depend on the same subset of the partition's inputs. Thus, the graph of a partition is a graph of clusters. A cluster may be executed as soon as its inputs are available, without any communication with the external world.

The Signal program is now defined by: The signal index represents the index of the first free cell in the buffer. Note that in this simple specification, it is considered that a write (signal mess in) and a read (signal mess out) actions in the buffer cannot be simultaneous. In addition, this partial specification represents only the control part of the FIFO (the full specification uses the Signal sliding window operator-derived from the delay-which is not presented in this article).

The Boolean signals OK write and OK read have the value tt when it is possible to write (respectively, to read) a new data in the FIFO. To ensure that the FIFO is safe, the following constraints are added (as assertions) to the process: mess in ˆ< (when OK write) and mess out ˆ< (when OK read ).

Equations in extended Signal

We have seen that Signal equations, written x := y, relate extended streams, which are sequences of values and meaningful absence. The equation x := y expresses synchronized flow equality. There is a synchronous communication between y and x.

Kahn Process Networks describe flow functions. The absence is not explicitly considered as a value. An extension of Signal as flow functions would mean the introduction of a new, idealized, class of equations, written x :-y to denote the equality between the considered streams as pure flows (that is, infinite sequences of values, filtering or discarding the absence of values).

By analogy with flow-equivalence defined in Section 2.3, we can say that x and y are flow-equivalent through x : -y. Since both signals hold the same sequences of values, with possibly any number of absence value between these values, the equation denotes an idealized asynchronous communication between y and x.

Back to asynchronous composition

The equation x :-y represents the behavior of an unbounded FIFO buffer. By using it, it is possible to express the asynchronous composition P || Q of processes P and Q (see Section 2.4) as their synchronous composition with unbounded FIFOs (i.e. as it becomes continuous). Let (x i ) i be the signals shared by P and Q. Then, their asynchronous composition is equal to

where the notation P [(x ip /x i ) i ] represents the substitution of variables shared by P and Q. KPNs can hence be expressed as such Signal programs "extended" with idealized unbounded FIFOs.