Zhibin Yang

Jean-Paul Bodeveix
email: bodeveix@irit.fr

Mamoun Filali

Kai Hu
email: hukai@buaa.edu.cn

Yongwang Zhao

Dianfu Ma

Towards a Verified Compiler Prototype for the Synchronous Language SIGNAL

Keywords: synchronous languages, SIGNAL, guarded actions, verified compiler, Coq, AADL(Architecture Analysis

SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL compiler, we propose a new intermediate representation (named S-CGA, a variant of clocked guarded actions), to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e. the translation from SIGNAL to S-CGA is presented. As well, the proof of semantics preservation is mechanized in the theorem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multi-threaded code generation with time-predictable properties. With the rising importance of multi-core processors in safety-critical embedded systems or cyber-physical systems (CPS), there is a growing need for model-driven generation of multi-threaded code and thus mapping on multi-core. We propose a timepredictable multi-core architecture model in AADL (Architecture Analysis and Design Language), and map the multithreaded code to this model.

Introduction

Safety-critical real-time systems such as avionics, space systems, and nuclear power plants, are also considered as reactive systems, because they always interact with their environment continuously. The environment can be some physical devices to be controlled, a human operator, or other reactive systems. These systems receive from the environment input events, and compute the output information, which is eventually sent to the environment. The synchronous approach is an important choice for the design of these systems, which relies on the synchronous hypothesis [START_REF] Potop-Butucaru | The synchronous hypothesis and synchronous languages[END_REF]: a synchronous program reacts to its environment in a sequence of discrete instants. At each instant, the system does input-computation/communication-output, which takes zero time. Even if the physical time is abstracted, the inherent functional properties are not changed, so we can say this method focuses on functional behaviors at a platformindependent level. In contrast to asynchronous concurrency, synchronous languages avoid the introduction of nondeterminism by interleaving. Namely, the execution of two independent, atomic parallel tasks is simultaneous. This allows deterministic semantics, thereby making synchronous programming amenable to predictable system design.

There are several synchronous languages, such as ES-TEREL [START_REF] Boussinot | The Esterel language[END_REF], LUSTRE [START_REF] Halbwachs | The synchronous data-flow programming language Lustre[END_REF] and QUARTZ [START_REF] Schneider | The synchronous programming language QUARTZ[END_REF] based on the perfect synchrony paradigm, and SIGNAL [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF] based on the poly-chrony paradigm. Synchronous languages can be considered as different implementations of the synchronous hypothesis. As a main difference from other synchronous languages, SIG-NAL naturally considers a mathematical time model, in term of a partial order relation, to describe multi-clocked systems without the necessity of a global clock. This feature permits the description of globally asynchronous locally synchronous systems (GALS) conveniently, where components based on different clock domains are integrated at the system level.

This paper reports a new compiler prototype for the SIG-NAL language, including sequential code generation and multi-threaded code generation with time-predictable properties.

(1) Intermediate representation Guarded commands [START_REF] Edsger | Guarded commands, nondeterminacy and formal derivation of programs[END_REF], also called asynchronous guarded actions by J. Brandt et al. [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF], are a well-established concept for the description of concurrent systems. In the spirit of the guarded commands, J. Brandt et al. propose synchronous guarded actions [START_REF] Brandt | Separate translation of synchronous programs to guarded actions[END_REF] as an intermediate representation for their QUARTZ compiler. As the name suggests, it follows the synchronous model. Hence, the behavior (control flow as well as data flow) is basically described by sets of guarded actions of the form γ ⇒ A . The boolean condition γ is called the guard and A is called the action. To support the integration of synchronous, polychronous and asynchronous models (such as CAOS [START_REF] Brandt | Translating concurrent action oriented specifications to synchronous guarded actions[END_REF] or SHIM [START_REF] Edwards | Shim: a deterministic model for heterogeneous embedded systems[END_REF]), they propose an extended intermediate representation, that is clocked guarded actions [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF][START_REF] Brandt | Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions[END_REF] where one can declare explicitly a set of clocks. They also show how clocked guarded actions can be used for verification by symbolic model checking (SMV) and simulation by SystemC.

Compared with the existing SIGNAL compiler-Polychrony 1) , we use clocked guarded actions as the intermediate representation, to integrate more synchronous languages such as QUARTZ, AIF 2) [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF] into our compiler prototype in the future. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold. We mention also that the DC+ [START_REF]Esprit project : Safety Critical Embedded Systems SACRES. The declarative code DC+[END_REF] intermediate format has been proposed as an intermediate format for compiling multiclock synchronous languages (ESTEREL, LUSTRE and SIGNAL). However, DC+ is introduced as a layer on top of DC which is a monoclock intermediate language. DC+ is characterized by a rich kernel with a monoclock guarded assignment (named at) and the equivalent of SIGNAL when and default constructs. Thus, we propose a variant of Clocked 1) http://www.irisa.fr/espresso/Polychrony 2) Averest Intermediate Format Guarded Actions, namely S-CGA, which constrains variable accesses as done by SIGNAL and guarded assignments are multiclocked. Compared to DC+, the SIGNAL when and default are not part of S-CGA, actually, they are compiled. More generally, to conform with the revised semantics of clocked guarded actions, we also do some adjustments on the translation rules from SIGNAL to clocked guarded actions (which are given by [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF] [START_REF] Brandt | Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions[END_REF]).

(

2) Code generation

The sequential code generation from SIGNAL programs is adapted to the S-CGA context. We also consider enhancements of the compiler and their insertion in the compilation chain. Moreover, we propose an appropriate modular architecture for our prototype.

With the advent of multi-core processors, automated synthesis of multi-threaded code from polychronous models is an attractive option for embedded system designers [START_REF] Besnard | Code generation strategies in the polychrony environment[END_REF][START_REF] Bijoy | Generating multi-threaded code from polychronous specifications[END_REF][START_REF] Bijoy | On the deterministic multi-threaded software synthesis from polychronous specifications[END_REF][START_REF] Papailiopoulou | From design-time concurrency to effective implementation parallelism: The multi-clock reactive case[END_REF][START_REF] Hu | Multi-threaded code generation from Signal program to OpenMP[END_REF]. However, we would like to consider the multi-threaded code generation with time-predictable properties. Time predictability means that the program timing can be foreseen statically, such as worst-case execution time (WCET). In order to measure WCET in a compositional way, strong architectural hypotheses must be done and this is the goal of the time-predictable architecture. In this paper, we propose a time-predictable multi-core architecture model in AADL (Architecture Analysis and Design Language) [START_REF]AS5506A: Architecture Analysis and Design Language (AADL) Version[END_REF], and then we map the multi-threaded code to this model.

(3) Verification of the compilation For a safety-critical system, it is naturally required that the compiler must be verified to ensure that the source program semantics is preserved. There are many approaches to gain assurance that the transformation or the translation of a specification or a program is semantic-preserving. This can be done by directly building a theorem-prover-verified compiler [START_REF] Leroy | Mechanized Semantics for Compiler Verification[END_REF], by using translation validation [START_REF] Pnueli | Translation validation[END_REF], etc. The existing formal verification techniques around SIGNAL are mainly based on translation validation [START_REF] Pnueli | Translation validation[END_REF] [START_REF] Van Chan Ngo | Formal verification of synchronous data-flow program transformations toward certified compilers[END_REF]. However, translation validation treats the compiler as a "black box", namely it just checks the input and output of each program transformation to validate the semantics preservation. So it yields that one needs to redo the validation when the source program is changed. We would like to extract a verified SIG-NAL compiler from a correctness proof developed within the theorem prover Coq as it has been done in the GENEAUTO project for a part of the SIMULINK compiler [START_REF] Izerrouken | Machinechecked sequencer for critical embedded code generator[END_REF].

Firstly, formal semantics is an important basis for the compiler verification. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics) [START_REF] Besnard | SIGNAL V4 Reference Manual[END_REF][START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Le | Data-Flow to von Neumann: the Signal approach[END_REF], denotational semantics based on tags which puts forward a partial order view of time (called tagged model semantics) [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Le | Polychrony for system design[END_REF], structural operational semantics defining inductively a set of possible transitions [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF][START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF], operational semantics defined by synchronous transition systems (STS) [START_REF] Pnueli | Translation validation[END_REF]. In [START_REF] Yang | A comparative study of two formal semantics of the SIGNAL language[END_REF], we have studied the equivalence between the trace semantics and the tagged model semantics, to assert a determined and precise semantics of the SIGNAL language.

Secondly, verifying a compiler is always a long-term work. The front-end of our compiler prototype has been proven. However, there already exists a mechanized semantics of a subset of C language in Coq [START_REF] Leroy | Mechanized Semantics for Compiler Verification[END_REF], and we have already worked on the mechanized semantics of different AADL subsets such as [START_REF] Yang | From AADL to timed abstract state machines: A verified model transformation[END_REF]. Thus we can envision to validate semantically the mapping from the S-CGA level to the targets such as sequential code in C and multi-threaded code in AADL.

To summarize, the relation between our work and related work is shown in Figure 1 (which extends the figure given in [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF]).

The rest of this paper is structured as follows. Section 2 introduces the basic concepts of the SIGNAL language. The abstract syntax of SIGNAL and its denotational semantics based on the trace model are also given. Section 3 presents the abstract syntax and the denotational semantics of S-CGA. Section 4 gives the front-end of the compiler, that is the translation from SIGNAL to S-CGA. The proof of the semantics preservation of the transformation is also presented in Section 4. Section 5 and Section 6 present the sequential code generation and the multi-threaded code generation respectively. Section 7 discusses the related work, and Section 8 gives some concluding remarks.

An Introduction to SIGNAL

In the SIGNAL language, the variables can be evaluated only at some instants which define their so-called clocks. Moreover, since SIGNAL is polychronous, each variable can have its own clock. In this section, we first introduce the basic concepts and the abstract syntax of the SIGNAL language, and then we present the semantics domain and the trace semantics of SIGNAL.

Basic Concepts and Abstract Syntax of SIGNAL

Signals

In the synchronous hypothesis, the behaviors of a reactive system are divided into a discrete sequence of instants.

At each instant, the system does input-computation-output, which takes zero time. Thus, the inputs and outputs are sequences of values, each value of the sequence being present at some instants. Such a sequence is called a signal. Consequently, at each instant, a signal may be present or absent (denoted by ⊥). In SIGNAL, signals must be declared before being used, with an identifer (i.e., signal variable or the name of signal) and an associated type for their values such as integer, real, complex, boolean, event, string, etc.

Example 1 Three signals named input 1 , input 2 , output are shown as follows. Here a logical time reference is denoted as

(t k ) k∈N . t t 1 t 2 t 3 t 4 • • • input 1 1 ⊥ 3 ⊥ • • • input 2 ⊥ 5 7 9 • • • output ⊥ ⊥ 10 ⊥ • • •
Abstract Clock The set of instants where a signal takes a value is the abstract clock of the signal. Two signals are synchronous if they are always present and absent at the same instants, which means they have the same abstract clock.

In the example given above, the abstract clocks of input 1 , input 2 and output, denoted respectively input 1 , input 2 and output, are defined by different sets of logical instants. For instance, the abstract clock associated with input 1 is the set {t 1 , t 3 , ...}.

Moreover, SIGNAL can specify the relations between the abstract clocks of signals in two ways: implicitly or explicitly.

Primitive Constructs SIGNAL uses several primitive constructs to express the relations between signals, including relations between values and relations between abstract clocks. Moreover, the primitive constructs can be classified into two families: monoclock operators (for which all signals involved have the same abstract clock) and multiclock operators (for which the signals involved may have different clocks).

• Monoclock operators, including instantaneous function and delay. The instantaneous function x := f (x 1 , • • • , x n ) applied on a set of inputs x 1 , • • • , x n will produce the output x, while the delay operator x := x 1 $ init c sends the previous non-absent value of the input to the output with an initial value c. • Multiclock operators, including undersampling and deterministic merging. The undersampling operator x := x 1 when x 2 is used to get the output of an input at the true occurrence of another input, while the deterministic merging operator x := x 1 de f ault x 2 is used to select between two inputs to be sent as the output, with a higher Note that, these operators specify the relations between the abstract clocks of the signals in an implicit way.

In the SIGNAL language, the relations between values and the relations between abstract clocks of the signals, are defined as equations, and a process consists of a set of equations. Two basic operators apply to processes, the first one is the composition of different processes, and the other one is the local declaration in which the scope of a signal is restricted to a process.

Extended Constructs SIGNAL also provides some operators to express control-related properties by specifying clock relations explicitly, such as clock synchronization, set operators on clocks (union, intersection, difference) and clock comparison.

• Clock synchronization, the equation

x 1 ˆ= x 2 ˆ= • • • ˆ= x n specifies that signals x 1 , x 2 , • • • , x n are synchronous.
• Set operators on clocks, such as the equation x:= x 1 ˆ+ x 2 defines the clock of x as the union of the clocks of signals x 1 and x 2 , the equation x:= x 1 ˆ* x 2 defines the clock of x as the intersection of the clocks of signals x 1 and x 2 , and the equation x:= x 1 ˆx 2 defines the clock of x as the difference of the clocks of signals x 1 and x 2 .

• Clock comparison, such as the statement x 1 ˆ< x 2 specifies a set inclusion relation between the clocks of signals x 1 and x 2 , and the statement x 1 ˆ> x 2 specifies a set containment relation between the clocks of signals x 1 and x 2 .

The semantics of each of the extended constructs is defined in term of the primitive constructs [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF], so we just consider the primitive constructs, that is kernel SIGNAL (kSIG-NAL for short). Its abstract syntax is presented as follows.

P ::= x := f (x 1 , • • • , x n ) (instantaneous function) |x := x 1 $ init c (delay) |x := x 1 when x 2 (undersampling) |x := x 1 de f ault x 2 (deterministic merging) |P|P (composition)
We can use both primitive constructs and extended constructs in the programming. However, the compiler will translate it into kSIGNAL (just use primitive constructs). Thus, in the proof of semantics preservation, we consider kSIGNAL and S-CGA.

In order to get a simplest criterion for the proof of semantics equivalence, local variables are supposed to be moved to the top level, so that the corresponding signals can be controlled from the outside. It means that non-deterministic behaviors are excluded, but our goal is to generate executable code, not specifications.

Trace Model

There exist several semantics for SIGNAL, such as trace semantics (which is used in the reference manual for SIGNAL Version 4), tagged model semantics (based on tags which puts forward a partial order view of time), structural operational semantics, etc. This paper considers the trace semantics. In the following paragraphs, we summarize the trace model [START_REF] Besnard | SIGNAL V4 Reference Manual[END_REF][START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF] which is used to define the trace semantics of SIGNAL.

Let X be a set of variables, and let V be the set of values that can be taken by the variables. For a variable x ∈ X, and a non-empty subset X of variables in X, we consider V x the domain of values that may be taken by x, and

V X = x∈X V x .
The symbol ⊥ (⊥ V) is introduced to express the ab-sence of valuation of a variable. Then we denote:

V ⊥ = V ∪ {⊥} V ⊥ X = V X ∪ {⊥}
The basic objects manipulated by the SIGNAL language are signals. The length of a signal can be either finite or infinite.

Definition 1 (Signal) A signal s is a sequence (s i ) i∈I of typed values (of V ⊥ ), where I is the set of natural numbers N or an initial segment of N, including the empty segment.

After, the definition of a trace is given. Note that, a signal is just a sequence of values corresponding to a signal variable, while a trace defines the synchronized sequences of values of a set of signal variables.

Definition 2 (Event) Considering X a non-empty subset of X, we call event on X any application

e : X → V ⊥ X • e(x) = ⊥ indicates that variable x has no value in the event. • e(x) = v indicates, for v ∈ V x , that variable x takes the value v in the event.
The absent event on X (X → {⊥}), where all the signals are absent at a logical instant, is denoted ⊥ e (X). Moreover, the set of events on X

(X → V ⊥ X ) is denoted ε X .
A trace is a sequence of events. For any subset X of X, we consider the following definition of the set Φ X of traces on X.

Definition 3 (Traces) Φ X is the set of traces on X, defined as the set of applications N → ε X where N is the set of natural numbers.

Similarly, a trace can be finite. However, we can extend the finite sequence with infinite absent events, to get an infinite trace.

The absent trace on X (N → {⊥ e (X)}), i.e., the infinite sequence formed by the infinite repetition of ⊥ e (X), is denoted ⊥ X .

Definition 4 (Process) Given a SIGNAL process, its trace semantics, denoted SProcess, includes a set of signal variables defining the domain of the process and a set of traces.

Definition 5 (Trace Equivalence) Two traces are equivalent if and only if they have the same set of signal variables and the same set of signals.

Trace Semantics of SIGNAL

Based on the trace model, the trace semantics of SIGNAL is presented as follows. It defines the set of traces associated to each primitive construct of SIGNAL.

Trace Semantics 1 The trace semantics of the instantaneous function

x := f (x 1 , • • • , x n ) is defined as follows: ∀t ∈ N x t = ⊥ i f x 1t = . . . = x nt = ⊥ f (x 1t , . . . , x nt ) i f x 1t ⊥ ∧ . . . ∧ x nt ⊥
At each instant t, the signals are either all present or all absent, i.e., they are synchronous, denoted

x ˆ= x 1 ˆ= • • • = x n .
x t gets the value of f (x 1t , . . . , x nt ) when the signals are all present. The function f includes different mathematical operations, such as arithmetic operations, boolean operations, etc.

Trace Semantics 2 The trace semantics of the delay construct x := x 1 $ init c is defined as follows:

-(∀t ∈ N) x 1t = ⊥ ⇔ x t = ⊥ -{k | x 1k ⊥} ∅ ⇒ x min{k|x 1k ⊥} = c -(∀t ∈ N) x 1t ⊥ ∧ {k > t | x 1k ⊥} ∅ ⇒ x min{k>t|x 1k ⊥} = x 1t
Here, min(X) denotes the minimum of a non-empty set of naturals. Similarly to the instantaneous function, the delay construct also requires signals x and x 1 have the same clock, denoted x ˆ= x 1 . Given a logical instant t, x takes the most recent value of x 1 except the one at t. Initially, x takes the value c.

Trace Semantics 3 The trace semantics of the undersampling construct x := x 1 when x 2 is defined as follows:

∀t ∈ N x t = x 1t i f x 2t = true ⊥ otherwise
Here, x and x 1 have the same type and x 2 is a boolean signal. The clock of x is the intersection of the clock of x 1 and the true occurrences of

x 2 , denoted x=x 1 ˆ* [x 2 ], where [x 2 ] = x 2 ∧ x 2 represents the true occurrences of x 2 .
Trace Semantics 4 The trace semantics of the deterministic merging construct x := x 1 de f ault x 2 is defined as follows:

∀t ∈ N x t = x 1t i f x 1t ⊥ x 2t otherwise
Here, signals x, x 1 and x 2 have the same type. The clock of x is the union of the clocks of x 1 and x 2 , denoted x = x 1 ˆ+ x 2 . Given a logical instant t, x t gets the merge of the values of x 1t and x 2t , and the value of x 1t has a higher priority.

Finally the semantics of parallel composition is defined as the intersection of the semantics of the components. We apply these semantics rules to a SIGNAL process, to get a com-plete semantics of the process, that is SProcess (Definition 4).

Synchronous Clocked Guarded Actions for SIGNAL

In papers such as [START_REF] Brandt | Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions[END_REF], clocked guarded actions have been defined as a common representation for synchronous (via synchronous guarded actions), polychronous and asynchronous (via asynchronous guarded actions) models. It has a multiclocked feature. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold [11] [29], in this case the read value is the most recently written value, while in SIGNAL read and writes can be simultaneous provided the causality is respected. As a consequence, we introduce S-CGA, which is a variant of clocked guarded actions. S-CGA constrains variable accesses as done by SIGNAL. We remark that the SIG-NAL compiler has introduced intermediate representations to manage guards and dependencies such as HCDG (Hierarchized Conditional Dependency Graph) [START_REF] Le | Polychrony for system design[END_REF]. The proposed intermediate language is not at the same level: S-CGA does not resolve dependencies. Actually, HCDG could be reused in the next stages of the compilation process. In this section, we first present the syntax of S-CGA, and then we give the denotational semantics of S-CGA based on the trace model. S-CGA has the same structure as clocked guarded actions, but they have different semantics.

Definition 6 (S-CGA) An S-CGA system is represented by a set of guarded actions of the form γ ⇒ A defined over a set of variables X. The Boolean condition γ is called the guard and A is called the action. Guarded actions can be of the following forms:

(1) γ ⇒ x = τ (immediate) (2) γ ⇒ next(x) = τ (delayed) (3) γ ⇒ assume(σ) (assumption)
where

• the guard γ is a Boolean condition over the variables of X, and their respective clocks. For a variable x ∈ X, we denote:

its clock x, its initial clock init( x) as the clock which ticks the first time (if any) where x ticks. • τ is an expression over X, • σ is a Boolean expression over the variables of X and their clocks.

An immediate assignment x = τ writes the value of τ immediately to the variable x. The form (1) implicitly imposes that if γ is defined 3) and its value is true, then x is present and τ is defined.

A delayed assignment next(x) = τ evaluates τ in the given instant but changes the value of the variable x at next time clock x ticks.

The form (3) defines a constraint. It determines a Boolean condition which has to hold when γ is defined and true. All the execution traces must satisfy this constraint. Otherwise, they are ignored.

Guarded actions are composed by using the parallel operator .

Definition 7 (Trace semantics of S-CGA) The trace semantics of an S-CGA system is defined as a set of traces, that is S CGA = {S | ∀scga ∈ S CGA, scga S = true}. We have the following semantics rules, [START_REF] Potop-Butucaru | The synchronous hypothesis and synchronous languages[END_REF]

γ ⇒ x = τ S = ∀t ∈ N, γ S ,t ∧ γ S ,t → ( x S ,t ∧ τ S ,t ∧ x S ,t = τ S ,t ) (2) γ ⇒ next(x) = τ S = ∀t 1 < t 2 ∈ N, ((∀t ∈ N, t 1 < t < t 2 → ¬ x S ,t ) ∧ γ S ,t 1 ∧ γ S ,t 1 ) → ( x S ,t 1 ∧ τ S ,t 1 ∧ ( x S ,t 2 → x S ,t 2 = τ S ,t 1 )) (3) γ ⇒ assume(σ) S = ∀t ∈ N, γ S ,t ∧ γ S ,t → σ S ,t ∧ σ S ,t
where e S ,t defines the domain of e: it is true if all the variables of e are present in trace S at the instant t; e S ,t is a partial function defined over the domain e S ,t whose value is the valuation of e on trace S at the instant t.

• Rule (1): when γ is present, and the value of γ is true, x and τ are both present, and the value of x is that of τ. • Rule (2): when γ is present and the value of γ is true at instant t 1 , x and τ are present at t 1 , and if t 2 is the next instant where x is present, then the value of x at t 2 is that of τ at instant t 1 . • Rule (3): when γ is present, and the value of γ is true, σ is present and true.

The semantics of S-CGA composition is defined as scga 1 scga 2 S = scga 1 S ∧ scga 2 S .

3) An expression is said to be defined if all the variables it contains are present.

4 From kSIGNAL to S-CGA and its Semantics Preservation

In this section, we present the front-end of the compiler, that is the translation from kSIGNAL to S-CGA. We envision the extraction of a complete verified-compiler prototype from the theorem proof. Thus, we would like to use the theorem prover Coq, to express and verify the translation from kSIGNAL to S-CGA.

Translation Rules

kSIGNAL can be structurally translated to S-CGA by translating each construct separately. The translation rules are close to the ones which have been given in [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF]. However, to conform with the semantics of S-CGA (i.e. the revised semantics of clocked guarded actions), we have done some adjustments.

kS IGNAL S -CGA

(1) x := f (x 1 , • • • , x n )                x ⇒ x = f (x 1 , • • • , x n ) x 1 ⇒ assume( x) ... x n ⇒ assume( x) (2) x := x 1 $ init c          init( x) ⇒ x = c x ⇒ next(x) = x 1 true ⇒ assume( x = x 1 ) (3) x := x 1 when x 2 x 1 ∧ x 2 ⇒ x = x 1 x ⇒ assume( x 1 ∧ x 2 ) (4) x := x 1 de f ault x 2          x 1 ⇒ x = x 1 x 2 ∧ ¬ x 1 ⇒ x = x 2 x ⇒ assume( x 1 ∨ x 2 )
• Translation (1): The instantaneous function is applied to the inputs and produces the output. Note that the immediate assignment the value of x 1 to x whenever it is needed. The clock assumption ensures that x only holds when both inputs (i.e., x 1 and x 2 ) are present and x 2 is true. Thanks to the assume semantics (Rule(3) of Definition 7), assume(

x ⇒ x = f (x 1 , • • • , x n ) implicitly imposes x ⇒ x 1 , ..., x ⇒ x n ,
x 1 ∧ x 2 ) implies x 1 ∧ x 2 ∧ x 2 .
• Translation (4): The deterministic merging construct merges two signals with priority for the first one. Therefore, if the first input is present, it is passed to x. If it is not present, but the second one is, the second one is passed to x. The clock assumption ensures that x only holds when at least one of the inputs is present.

Remark 1 Compared with the translation rules given in [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF], the main change is in the Translation (3). Namely, true ⇒ assume( x = x 1 ∧ x 2 ∧ x 2 ) has been changed into x ⇒ assume( x 1 ∧ x 2 ). According to the Rule (3) (Definition 7): when γ is present, and the value of γ is true, σ must be present, and the value of σ is true. true ⇒ assume( x = x 1 ∧ x 2 ∧ x 2 ) implies x 2 is always present and always true. Thus, to conform with the semantics of S-CGA, we change it into x ⇒ assume( x 1 ∧ x 2 ). It means when x is present, x 1 ∧ x 2 is present and true, i.e., x 1 is present and x 2 is present and true.

Example 2 A translation from kSIGNAL to S-CGA 4) is given as follows.

(|y 1 := x$ init 1

|y 2 := x$ init 2 |z := x > 0 |s 1 := f (y 1 ) when z |s 2 := s 1 + 1 |s 3 := f (y 2 ) when (not z) |s 4 := s 3 + 2 |) true ⇒ assume( ŷ1 = x) init( ŷ1 ) ⇒ y 1 = 1 ŷ1 ⇒ next(y 1 ) = x true ⇒ assume( ŷ2 = x) init( ŷ2 ) ⇒ y 2 = 2 ŷ2 ⇒ next(y 2 ) = x true ⇒ assume( x = ẑ) ẑ ⇒ z = (x > 0) ŝ1 ⇒ assume(ẑ ∧ z) ẑ ∧ z ⇒ s 1 = f (y 1 ) ŝ2 ⇒ s 2 = s 1 + 1 ŝ1 ⇒ assume( ŝ2 ) ŝ3 ⇒ assume(ẑ ∧ (not z)) ẑ ∧ (not z) ⇒ s 3 = f (y 2 ) ŝ4 ⇒ s 4 = s 3 + 2 ŝ3 ⇒ assume( ŝ4 )

The Proof of Semantics Preservation

As shown in Figure 2, the Coq mechanization includes 7 modules (about 1300 lines of Coq code), i.e., the abstract syntax of kSIGNAL, the trace model, the trace semantics of kSIGNAL, the abstract syntax of S-CGA, the trace semantics 4) If two guarded actions update the same variables, the guards must be exclusive.

of S-CGA, the translation rules, and the proof of the semantics preservation. Here, the semantics preservation is defined as a trace equivalence between two trace semantics models related to kSIGNAL and its translation into S-CGA respectively.

Figure 2 The global view of the semantics preservation All the definitions given as above have been mechanized in Coq. Here we just present the main idea of the proof.

Firstly, we prove each semantics rule of the trace semantics of kSIGNAL is trace equivalent with its translation into S-CGA. For each semantics rule, there are two Lemmas to be proven (in two directions).

Instantaneous function.

(1) Its trace semantics is defined as Sassignment. (2) As defined in section 4.1, its translated guarded actions are x ⇒ x = f (x 1 , • • • , x n ), x 1 ⇒ assume( x), ..., and x n ⇒ assume( x). Applying the semantics of S-CGA (scgaSimm is the semantics of immediate assignment), we can get the semantics of instantaneous function construct translated into S-CGA. Then, we prove the trace equivalence between (1) and (2).

Lemma s i g n a l 2 s c g a _ a s s 1 : ∀ f x x i t r , S a s s i g n m e n t x f x i t r → ( scgaSimm ^x x { | e x p _ f u n := f ; e x p _ a r g s := x i | } t r ∧ s t r M o d e l . s t r a c e s ( s c g a 2 S p r o c e s s ( GA_ipar ( f u n i :

F c t A r f ⇒ ^( x i i ) =⇒ assume ( ^x ) ) ) ) t r ) .
Lemma s i g n a l 2 s c g a _ a s s 2 : ∀ f x x i t r , scgaSimm ^x x { | e x p _ f u n := f ; e x p _ a r g s := x i | } t r → s t r M o d e l . s t r a c e s s c g a 2 S p r o c e s s ( GA_ipar ( f u n i : F c t A r f ⇒ ^( x i i ) =⇒ assume ( ^x ) ) ) ) t r → S a s s i g n m e n t x f x i t r .

Delay. (1) Its trace semantics is defined as Sdelay. (2)

There are three translated guarded actions, i.e., init( x) ⇒ x = c, x ⇒ next(x) = x 1 , and true ⇒ assume( x = x 1 ). Applying the semantics of S-CGA (getFirst0 is used to get the first instant when x is present, that is init( x), scgaSnext is the semantics of delayed assignment, and scgaSctr is the semantics of assumption), we can get the semantics of delay construct translated into S-CGA. Then, we prove the trace equiv-alence between (1) and ( 2). In the Lemmas, x = x 1 is denoted x ˆ= x 1 (as clock synchronization operator in SIGNAL).

Lemma s i g n a l 2 s c g a _ d e l a y 1 : ∀ x x1 v t r , S d e l a y x x1 v t r → ( ( scgaSimm i n i t ( x ) x v t r ( g e t F i r s t 0 t r ) ) ∧ ( ∃ c : Value , s c g a S n e x t g T r u e x x1 c t r ( g e t F i r s t 0 t r ) ) ) ∧ s c g a S c t r g T r u e ( ^x ^= ^x1 ) t r ( g e t F i r s t 0 t r ) .

Lemma s i g n a l 2 s c g a _ d e l a y 2 : ∀ x x1 v t r , scgaSimm i n i t ( x ) x v t r ( g e t F i r s t 0 t r ) → ( ∃ c : Value , s c g a S n e x t g T r u e x x1 c t r ( g e t F i r s t 0 t r ) ) → s c g a S c t r g T r u e ( ^x ^= ^x1 ) t r ( g e t F i r s t 0 t r ) → S d e l a y x x1 v t r .

Undersampling. (1) Its trace semantics is defined as Swhen.

(2) There are two translated guarded actions, i.e., x 1 ∧ x 2 ⇒ x = x 1 and x ⇒ assume( x 1 ∧ x 2 ). Applying the semantics of S-CGA, we can get the semantics of undersampling construct translated into S-CGA. Then, we prove the trace equivalence between (1) and ( 2). In the Lemmas, x 1 ∧ x 2 is denoted x 1 ˆ * x 2 (reusing the clock intersection operator of SIGNAL). Deterministic merging. (1) Its trace semantics is defined as Sdefault. (2) There are three translated guarded actions, i.e., x 1 ⇒ x = x 1 , x 2 ∧ ¬ x 1 ⇒ x = x 2 , and x ⇒ assume( x 1 ∨ x 2 ). Applying the semantics of S-CGA, we can get the semantics of deterministic merging construct translated into S-CGA. Then, we prove the trace equivalence between (1) and ( 2). In the Lemmas, x 2 ∧ ¬ x 1 is denoted x 2 ˆx 1 (clock difference operator of SIGNAL), and x 1 ∨ x 2 is denoted x 1 ˆ+ x 2 (clock union operator of SIGNAL).

Lemma s i g n a l 2 s c g a _ d e f a u l t 1 : ∀ x x1 x2 t r , S d e f a u l t x x1 x2 t r → ( scgaSimm ^x1 x x1 t r ∧ scgaSimm ( ^x2 ^-^x1 ) x x2 t r ) ∧ s c g a S c t r ^x ( ^x1 ^+ ^x2 ) t r .

Lemma s i g n a l 2 s c g a _ d e f a u l t 2 : ∀ x x1 x2 t r , scgaSimm ^x1 x x1 t r → scgaSimm ( ^x2 ^-^x1 ) x x2 t r → s c g a S c t r ^x ( ^x1 ^+ ^x2 ) t r → S d e f a u l t x x1 x2 t r .

Secondly, based on these Lemmas, we prove the following Theorem, that the two semantics models, i.e., (Pro-cess2Sprocess P) and (scga2Sprocess(signal2scga P)) are trace equivalent (they have the same set of signal variables and the same set of traces). This property concerns infinite objects and cannot generally be proved automatically. This is why we use the proof assistant which verifies a user-assisted proof.

Record SPeq ( p1 p2 : S p r o c e s s ) : Prop := { SPd : ∀ y , sdom p1 y ↔ sdom p2 y ; SPs : ∀ t r , s t r a c e s p1 t r ↔ s t r a c e s p2 t r } .

Theorem s i g n a l 2 s c g a _ c h e c k : ∀ p , SPeq ( P r o c e s s 2 S p r o c e s s p ) ( s c g a 2 S p r o c e s s ( s i g n a l 2 s c g a p ) ) .

Finally, we can extract the corresponding CAML code, to synthesize the first stage of the verified compiler prototype.

Sequential Code Generation

The compilation process of synchronous languages is not limited to code generation: some analyses are first applied to determine if the specification is indeed executable. The SIG-NAL compilation process contains one major analysis called clock calculus from which code generation directly follows. Moreover the clock calculus contains several steps [START_REF] Le | Polychrony for system design[END_REF], such as construction of an equation system over clocks; resolution of the system of clock equations; construction of a clock hierarchy on which the automatic code generation strongly relies.

For a safety-critical system, it is important to optimize the control structure of the generated code. In the SIGNAL compiler, the control flow expressed by abstract clocks serves to derive a control structure in automatic code generation. Thus, the quality of clock calculus has a strong impact on the correctness and efficiency of implementations. In [START_REF] Feautrier | Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction[END_REF], the authors have shown that there is a limitation of the clock calculus of the SIGNAL compiler. For example, for the undersampling construct x = x 1 when x 2 , the clock of the Boolean expression x 2 is partitioned into [x 2 ] and [¬x 2 ], which are referred to as condition-clocks. If x 2 is defined by a numerical expression such as an integer comparison, [x 2 ] and [¬x 2 ] are seen as black boxes. This has a strong impact on the analysis precision and the quality of generated code. Thus, the authors propose a new clock abstraction, that is combined numerical-Boolean abstraction, to eliminate this problem. They also use an SMT solver to reason on the new abstraction. With the same purpose, in [START_REF] Gamatié | Towards Static Analysis of SIGNAL Programs using Interval Techniques[END_REF], an interval-based data structure referred to as Interval-Decision Diagram (IDD) is considered for the analysis of numerical properties in SIGNAL programs.

As shown in Figure 3, in our compiler prototype (sequential code generation): [START_REF] Potop-Butucaru | The synchronous hypothesis and synchronous languages[END_REF] We have considered the main components of the clock calculus, such as construction of an equation system over clocks, resolution of a system of clock equations, and construction of a clock hierarchy. [START_REF] Boussinot | The Esterel language[END_REF] To integrate more synchronous languages, such as QUARTZ, AIF, etc., into our prototype in the future, we introduce S-CGA as the intermediate representation, and we adapt the clock calculus to S-CGA. [START_REF] Halbwachs | The synchronous data-flow programming language Lustre[END_REF] We propose an appropriate modular architecture for our prototype. One benefit of this approach is that we just need to redo a part of proof when some modules of the compilation process are changed. ( 4) We have considered existing enhancements such as [START_REF] Feautrier | Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction[END_REF] [31], namely we can use both BDD and SMT in the resolution of a system of clock equations.

Specifically, the compilation process is mainly structured as five modules. At each module, there are several submodules.

• Module 1: Beyond the usual lexical analysis, parsing and type checking, the compiler will transform the user program (using the subset of SIGNAL) whose statements all expressed with both primitive constructs and extended constructs to the normalized program (using kSIGNAL) whose statements are all expressed with primitive constructs. • Module 2: As a difference with the existing SIGNAL compiler, we construct S-CGA from the normalized program. S-CGA contains control flow (a system of clock equations) as well as data flow. As mentioned above, for the under-sampling construct, the SIGNAL compiler consider the condition-clocks [x 2 ] and [¬x 2 ] as black boxes if x 2 is defined by a numerical expression. When x 2 is defined by a complex boolean function, we have

[x 2 ] = x 2 ∧ x 2 and [¬x 2 ] = x 2 ∧ ¬x 2 .
Based on this abstraction, we can get more precise clock analysis. • Module 3: If the system of clock equations contains more than one equation with the same clock, the execution of the generated code will check the same control condition several times, and it is inefficient. This is why we need to resolve it. All the clock equations are considered as predicates. We can use BDD or SMT technology to check the equivalence of two predicates, and put the corresponding clock variables into the same equiva-Figure 3 The architecture of the verified compiler prototype lence class. We also check the endochrony property at this step, namely there is just one master clock. • Module 4: The code generation is based on both the clock hierarchy and the data dependencies. However, there may be clock-to-data cycles. To reduce these cycles, we first sort all the guarded actions. It will be easier to construct a clock hierarchy based on deterministic sorting, and we consider the sorting as a depth first search (DFS) order. • Module 5: The basic idea of code generation is the same as in the SIGNAL compiler. Furthermore, we do some optimizations based on clock inclusions. Given two equations such as y = x when x 1 and z = x when (x 1 and x 2 ), there is a clock-inclusion relation:

[x 1 ∧ x 2 ] → [x 1 ], i.e., the clock of [x 1 ∧ x 2 ] is a subset of the clock of [x 1 ]
. Consequently, we can do the code optimization illustrated as follows. If control condition x 1 holds, we do not need to check x 1 again in x 1 &&x 2 .

We just need to check if x 2 holds or not.

i f (x 1 ){ do actions ... i f (x 1 &&x 2 ){ do actions ...} } i f (x 1 ){ do actions ... i f (x 2 ){ do actions ...} }
Actually, the first version of the compiler prototype has been implemented in CAML directly. It is a good way to provide a basis for the Coq mechanization of the prototype. Finally, we envision the extraction of a complete prototype from the mechanization.

Multi-threaded Code Generation with Time-Predictable Properties

Safety-critical embedded systems or cyber-physical systems (CPS) distinguish themselves from general purpose computing systems by several characteristics, such as failure to meet deadlines may cause a catastrophic or at least highly undesirable system failure. Time-predictable system design [START_REF] Axer | Building timing predictable embedded systems[END_REF][START_REF] Wilhelm | The worstcase execution-time problem: Overview of methods and survey of tools[END_REF][START_REF] Thiele | Design for timing predictability[END_REF] is concerned with the challenge of building systems in such a way that timing requirements can be guaranteed from the design. This means we can predict the system timing statically. With the widespread advent of multi-core processors, it further aggravates the complexity of timing analysis. We would like to consider the multi-threaded code generation with time-predictable properties. At the modeling level, synchronous programming is a good choice for time-predictable system design. At the compiler level, we give the verified compiler from SIGNAL to our intermediate representation S-CGA and thus to multi-threaded code. At the platform level, we propose a time-predictable multi-core architecture model in AADL (Architecture Analysis and Design Language) [START_REF]AS5506A: Architecture Analysis and Design Language (AADL) Version[END_REF], and then we map the multi-threaded code to this model. Therefore, our method integrates time predictability across several design layers.

From S-CGA to Multi-threaded Code

The SIGNAL compilation process contains one major analysis called clock calculus from which code generation di-rectly follows. Moreover the clock calculus contains several steps [START_REF] Le | Polychrony for system design[END_REF], such as construction of an equation system of relations over clocks; resolution of the system of clock equations; construction of a clock hierarchy. Our goal here is to adapt the clock calculus to S-CGA. Moreover, in the multi-threaded code generation scheme, the data-dependency graph (DDG) should also be constructed to find more parallelism.

Based on the semantics of S-CGA, we can get the equation system over clocks. The general rules are given as follows.

S-CGA Clock Equations

γ ⇒ x = τ γ ∧ γ → x ∧ τ γ ⇒ next(x) = τ γ ∧ γ → x ∧ τ γ ⇒ assume(σ) γ ∧ γ → σ ∧ σ init( x) → x (∀x ∈ X)
As a first step, we just consider endochrony property 5) , namely we can construct a clock hierarchy based on the resolution of the system of clock equations. The clock hierarchy of Example 2 (with three clock equivalence classes, i.e., C 0 , C 1 , and C 2 ) is shown in Figure 4. For instance, the signals x, y 1 , y 2 , and z are synchronous, thus they are in the same clock equivalence class (C 0 ). The properties of the clock hierarchy are presented as follows [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF].

• Each node is a clock equivalence class.

• There is just one master clock equivalence class, here is C 0 in the clock hierarchy. • There is a clock implication relation (checked by BDD or SMT) between a son node and its father node, for instance, ẑ ∧ z → ẑ. Thus, all the clocks in the clock hierarchy can be defined from the master clock.

In the sequential code generation scheme, we associate guarded actions to each clock equivalence class of the clock hierarchy, then the deterministic sequential code will be generated [START_REF] Yang | A verified transformation: from polychronous programs to a variant of clocked guarded actions[END_REF]. In the multi-threaded code generation schema, the DDG should also be constructed to find more parallelism. We construct the DDG, as shown in Figure 5, based on the variables reading and writing. 5) Weak endochrony [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF] property will be considered in the future.

Definition 8 (Reading and Writing Dependencies) [START_REF] Baudisch | Dependencydriven distribution of synchronous programs[END_REF] Let FV(τ) denote the free variables occurring in the expression τ. The dependencies from guarded actions to variables are defined as follows:

RdVars(γ ⇒ x = τ) := FV(γ) ∪ FV(τ) RdVars(γ ⇒ next(x) = τ) := FV(γ) ∪ FV(τ) WrVars(γ ⇒ x = τ) := {x} WrVars(γ ⇒ next(x) = τ) := {next(x)}
Then, the dependencies from variables to guarded actions are defined as follows:

RdActs(x) := {γ ⇒ A | x ∈ RdVars(γ ⇒ A)} WrActs(x) := {γ ⇒ A | x ∈ WrVars(γ ⇒ A)}
Note that, γ ⇒ assume(σ) is used in the construction of the clock hierarchy. We expect that it is not needed to associate some actions to assume inside the DDG. This leads to proof obligations that should be checked to guarantee the correctness of the generated code.

An action can only be executed if all read variables are known. Similarly, a variable is only known if all actions writing it in the current step have been evaluated before. The multi-threaded code generation depends on the data dependency graph which has been associated with the clock hierarchy. We first need to find partitions. As presented in Figure 6, we would like to treat the partition methods in general, this means different partition methods (such as the vertical way [START_REF] Baudisch | Multithreaded code from synchronous programs: Extracting independent threads for OpenMP[END_REF] for a concurrent execution, the horizontal way [START_REF] Baudisch | Multithreaded code from synchronous programs: Generating software pipelines for openmp[END_REF] for a pipelined execution, etc.) don't affect the Figure 6 The proof idea proof. Our approach is general and it only requires a legal partition, here we reuse the definition of [START_REF] Baudisch | Dependencydriven distribution of synchronous programs[END_REF].

Definition 9 (Legal Partition) Let P be a partition, A 1 and A 2 be guarded actions of P, and be the reflexive and transitive closure of the following relation

R ⊆ A × A : (A 1 , A 2 ) ∈ R ⇔ WrVars(A 1 ) ∩ RdVars(A 2 ) {}. P is legal if only if is a partial order.
Note that, the intersection of WrVars(A 1 ) and RdVars(A 2 ) is empty if A 1 is a delayed action for a reading variable in A 2 .

Based on the Definition 9, a partition scheme of Example 2 (with 4 partitions) is given in Figure 5. The basic principle of our partition method is described as follows.

• Consider one partition (i.e. one thread) for each vertex of the data-dependency graph. • Merge two partitions for example P 1 and P 2 , if P 2 is the only son of P 1 and P 1 is the only father of P 2 . • In each partition, we organize the guarded actions based on the clock equivalence classes. For example, the two guards in Thread2 belong to the same clock equivalence class, so they will be merged inside the same control condition in the generated code.

Finally, we add wait/notify synchronization among the threads. A code fragment of Thread2 is given as follows.

/ * T hread 2 * / void step() { wait(T hread1); i f (C1){ s 1 = f (y 1 ); s 2 = s 1 + 1; } noti f y(T hread4); }

Mapping Multi-threaded Code to Multi-core

To allow for static prediction of the system timing, we need time-predictable processor architectures, thus we know all the architecture details such as the pipeline and the memory hierarchy to analyze the execution time of programs. Furthermore, the mapping from multi-threaded code to multi-core architectures should be also static and deterministic.

A time-predictable multi-core architecture model

With the advent of multi-core architectures, interference between threads on shared resources further complicates analysis. There are some recommendations from R. Wilhelm et al. [START_REF] Wilhelm | The worstcase execution-time problem: Overview of methods and survey of tools[END_REF][START_REF] Thiele | Design for timing predictability[END_REF], i.e., the better way is to reduce the time interference: (1) pipeline with static branch prediction and with inorder execution; (2) separation of caches (instruction and data caches); (3) LRU (Least Recently Used) cache replace policy; and (4) access of main memory via an TDMA (Time Division Multiple Access) scheme. In the EC funded project T-CREST 6) , M. Schoeberl et al. [START_REF] Schoeberl | Data cache organization for accurate timing analysis[END_REF][START_REF] Schoeberl | A time predictable instruction cache for a Java processor[END_REF] propose a new form of organization for the instruction cache, named method cache (MC), and split data caches (including stack cache (SC), static data cache (SDC), constants data cache (CDC), and heap allocated data cache (HC)), to increase the time predictability and to tighten the WCET. The method cache stores complete methods and cache misses occur only on method invocation and return. They split the data cache for different data areas, thus data cache analysis can be performed individually for the different areas. In our work, heap is avoided to be used because we don't use dynamic memory allocation in our multi-threaded code.

Based on existing work, we would like to model a timepredictable multi-core architecture in AADL. AADL is an SAE (Society of Automotive Engineers) architecture description language standard for embedded real-time systems, and supports several kinds of system analysis such as schedulability analysis. Moreover, we have already worked on the semantics of different AADL subsets such as [START_REF] Yang | From AADL to timed abstract state machines: A verified model transformation[END_REF]. So we envision how to validate semantically the mapping from the language level to the architecture level.

Our multi-core architecture model is illustrated in Figure 7. Inside the core, we consider static branch prediction and in-order execution in the pipeline. A simplified instruction set (get_instruction, compute, write_data, and read_data) is used. As a first step, we just consider first level cache (i.e. without L2 and L3). Each core is associated with a method cache, a stack cache, a static data cache, and a constants data cache. However, the same principle of cache splitting can be applied to L2 and L3 caches. The extension of the timing analysis for a cache hierarchy is straightforward. Moreover, TDMA-based resource arbitration allocates statically-6) Time-predictable Multi-Core Architecture for Embedded Systems computed slots to the cores. As proposed by [START_REF] Delange | Design and analysis of multi-core architecture for cyber-physical systems[END_REF], a core is associated with an AADL processor component and a multi-core processor with an AADL system component containing multiple AADL processor subcomponents, each one representing a separate core. This modeling approach provides flexibility: an AADL system can contain other components to represent cache, and shared bus, etc. For that purpose, we define specific modeling patterns with new properties such as MC_Properties. TDMA_Window denotes a Slot to an access connection. For a bus, there will be a list of allocations of slots, that is TDMA_Schedule. For instance, for N access connections, the TDMA period of the bus is T=Slot * N. Here, we consider all the access connections have the same slot duration.

property set MC_Properties is TDMA_Window : type record ( AccessPoint : list of reference (access connection); Slot : time; ); TDMA_Schedule : list of MC_Properties ::TDMA_Window applies to ( bus ); ... end

The Mapping Method

To preserve the time predictability, we consider static mapping and scheduling. Take the Example 2, it generates a configuration file (such as num_of_threads=4) in multi-threaded code generation. Moreover, we have a manual configuration file for the time-predictable multi-core architecture model, for example num_of_cores=4. Thus, we can generate a static mapping and scheduling, for instance:

• Thread1 → Core1, Thread2 → Core2, Thread3 →
Core3, and Thread4 → Core4. • Thread1: notify(Thread2), notify(Thread3); Thread2: wait(Thread1), notify(Thread4); Thread3: wait(Thread1), notify(Thread4); Thread4: wait(Thread2), wait(Thread3).

Thanks to the mechanizations such as method cache, split data caches, TDMA and static scheduling, the execution time of the multi-threaded code can be bounded.

Related Work

We discuss in this section some related work about two aspects: verification of the SIGNAL compilation (mainly focuses on sequential code generation) and multi-threaded code generation from SIGNAL.

Verification of the SIGNAL Compilation

For a safety-critical system, it is naturally required that the compiler must be verified to ensure that the source program semantics is preserved. For example, the SCADE Suite KCG automatic C code generator has been qualified as a development tool at DO-178B level A. Moreover, one of the supplements to DO-178C, the DO-330 (Software Tool Qualification Considerations) provides a guidance to qualify tools. This means a tool for example a development tool or a verification tool also needs to be qualified. There are many approaches to gain assurance that the transformation or the translation of a specification or a program is semantic-preserving. This can be done by directly building a theorem-prover-verified compiler [START_REF] Leroy | Mechanized Semantics for Compiler Verification[END_REF], by using translation validation [START_REF] Pnueli | Translation validation[END_REF], etc.

A. Pnueli et al. propose the notion of translation validation to verify the code generator of SIGNAL [START_REF] Pnueli | Translation validation[END_REF]. In that work, the authors define a language of symbolic models to represent both the source and target programs, called Synchronous Transition Systems (STS). An STS is a set of logic formulas which describe the functional and temporal constraints of the whole program and its generated C code. Then they use BDD representations to implement the symbolic STS models, and their proof method uses a SAT-solver to reason on the signal constraints.

In [START_REF] Van Chan Ngo | Formal verification of synchronous data-flow program transformations toward certified compilers[END_REF], the authors adopt translation validation to formally verify that the clock semantics and data dependence are preserved during the compilation of the SIGNAL compiler. They represent the clock semantics, the data dependence of a program and its transformed counterpart as first-order formulas which are called Clock Models and Synchronous Dependence Graphs (SDGs) respectively. Then they introduce clock refinement and dependence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock models and SDGs respectively. Finally, an SMT-solver is used for checking the existence of the correct transformation relations.

In the work of [START_REF] Van Chan Ngo | Formal verification of compiler transformations on polychronous equations[END_REF], the authors encode the source SIG-NAL programs and their transformations with Polynomial Dynamical Systems (PDSs), and prove that the transformations preserve the abstract clocks and clock relations of the source programs. By using the simulation in model checking techniques, their approach suffers from the increasing of the state-space when it deals with large programs.

These existing researches mainly use the method of translation validation. However, translation validation treats the compiler as a "black box", namely it just checks the input and output of each program transformation to validate the semantics preservation. So it yields that one needs to redo the validation when the source program is changed. We would like to extract a verified SIGNAL compiler which considers a subset of the SIGNAL language, based on the theoremprover-verified compiler method [START_REF] Leroy | Mechanized Semantics for Compiler Verification[END_REF]. Moreover, the challenge is to be modular enough to make proof compositional and to be able to update the proof when we need to do more optimization.

Multi-threaded Code Generation from SIGNAL

The report [START_REF] Besnard | Code generation strategies in the polychrony environment[END_REF] describes all code generation strategies available in the Polychrony toolset. In the multi-threaded code generation scheme, it uses micro-level threading which creates a large number of threads and equally large number of semaphores, leading to inefficiency. Thus, [START_REF] Bijoy | Generating multi-threaded code from polychronous specifications[END_REF] proposes a process-oriented and non-invasive multi-threaded code generation using the sequential code generators. It means that instead of changing the compiler, they use the existing sequential code generator and separately synthesize some programming glue to generate multi-threaded code. [START_REF] Papailiopoulou | From design-time concurrency to effective implementation parallelism: The multi-clock reactive case[END_REF] defines a full design flow starting from high level domain specific languages (Simulink, SCADE, AADL, SysML, MARTE, SystemC), transforming to polychronous specifications, and going to the generation of deterministic concurrent (multithreaded) executable code for simulation or (possibly distributed) implementation. The multi-threaded code generation in [START_REF] Bijoy | Generating multi-threaded code from polychronous specifications[END_REF] and [START_REF] Papailiopoulou | From design-time concurrency to effective implementation parallelism: The multi-clock reactive case[END_REF] are both based on the weak endochrony property.

There are also some work about multi-threaded code generation from the guarded actions. [START_REF] Baudisch | Multithreaded code from synchronous programs: Extracting independent threads for OpenMP[END_REF] presents a compilation of synchronous programs to multi-threaded OpenMP-based C programs. They start at the level of synchronous guarded actions. In addition to the explicit parallelism given in the source program, their method also exploits the implicit parallelism which is due to the underlying synchronous model of computation and the data dependencies of the guarded ac-tions. To speedup the execution of multi-threaded code, [START_REF] Baudisch | Multithreaded code from synchronous programs: Generating software pipelines for openmp[END_REF] proposes an automatic synthesis procedure that translates synchronous guarded actions to software pipelines. The synchronous guarded actions are analyzed in terms of their datadependencies to define legal partitions into pipeline stages. Given such a legal partitioning into pipeline stages, the presented synthesis procedure automatically identifies potential pipeline conflicts and implements code for forwarding (if possible) while stalling is implicitly given by the FIFO buffers. Finally, the sequential threads for the conflict-free pipeline stages are implemented in OpenMP-based C-code.

However, these works have not considered timepredictable properties. The mapping from their multithreaded code to multi-core platforms is handled by the underlying system. In addition, architectural aspects are not addressed and consequently architectural based properties, e.g., time determinism, cannot be explicitly controlled in order to have precise and safe timing properties.

Conclusion and Future Work

This paper reports a SIGNAL compiler prototype based on the intermediate representation S-CGA. Since SIGNAL is polychronous, each variable can have its own clock. Moreover, the variables can be evaluated only at some instants which define their so-called clocks. In contrast to the SIG-NAL language, clocked guarded actions can evaluate a variable even if its clock does not hold. As a consequence, we propose a variant of clocked guarded actions, namely S-CGA, which constrains variable accesses as done by SIGNAL. S-CGA has the same structure as clocked guarded actions, but they have different semantics. The front-end of the compiler, i.e. the translation from SIGNAL to S-CGA is presented. The proof of semantics preservation mechanized in the theorem prover Coq is also given. Moreover, we present the back-end of the compiler, including sequential code generation and multi-threaded code generation. Concerned with the sequential code generation, we adapt the code generation to the S-CGA context. But we also consider enhancements of the compiler and their insertion in the compilation chain. Moreover, we propose an appropriate modular architecture for our prototype. One benefit of this approach is that we just need to redo a part of proof when some modules of the compilation process are changed. With the widespread advent of multi-core processors, it further aggravates the complexity of timing analysis. This paper proposes the multi-threaded code generation by considering time-predictable properties. Our method integrates time predictability across several design layers, i.e., synchronous programming, verified compiler, and time-predictable multi-core architecture model.

Interaction among cores might also jeopardize software isolation layers, such as the one defined in ARINC653. There are some existing work such as [START_REF] Delange | Design and analysis of multi-core architecture for cyber-physical systems[END_REF], [START_REF] Hugues | AADLib, a library of reusable AADL models[END_REF], [START_REF] Gamatié | Synchronous modeling of avionics applications using the SIGNAL language[END_REF], and [START_REF] Gamatié | Polychronous design of embedded real-time applications[END_REF], about AADL modeling on multi-core architectures and their association with ARINC653.

Again, for us, the challenge will be to specify formally such a platform, with respect to space and time isolation, and to prove the satisfaction of timing properties at the application level.

Figure 1 A

 1 Figure 1 A global view of the relation between our work and related work

so in the assumption we only assert x 1 ⇒

 1 assume( x), ..., x n ⇒ assume( x). Thus all variables have the same clock as required by the semantics of SIGNAL. • Translation (2): The translation of the delay construct is split up in two cases. a) The first value that is produced by this construct is the constant c at the first instant when x is present. b) In all other instants the value of x is assigned by the value of x 1 evaluated at the last nonabsent instant of x 1 . The assumption ensures that both variables have the same clock. • Translation (3): The undersampling construct transfers

Lemma s i g n a l 2

 2 s c g a _ w h e n 1 : ∀ x x1 x2 t r , Swhen x x1 x2 t r → scgaSimm ( ^x1 ^ * x2 ) x x1 t r ∧ s c g a S c t r ^x ( ^x1 ^ * x2 ) t r . Lemma s i g n a l 2 s c g a _ w h e n 2 : ∀ x x1 x2 t r , scgaSimm ( ^x1 ^ * x2 ) x x1 t r → s c g a S c t r ^x ( ^x1 ^ * x2 ) t r → Swhen x x1 x2 t r .

Figure 4

 4 Figure 4 Clock hierarchy

Figure 5

 5 Figure 5 Data dependency graph

Figure 7 A

 7 Figure 7 A time-predictable multi-core architecture model

Acknowledgements This work was partially supported by the Natural Science Foundation of Jiangsu Province under Grant SBK2015041894, the National Key Basic Research Program of China (973 plan) under Grant 2014CB744904, Project of the State Key Laboratory of Software Development Environment of China under Grants SKLSDE-2015KF-04, SKLSDE-2014ZX-09 and SKLSDE-2013ZX-30, and the RTRA STAE Foundation in France (http://www.fondation-stae.net/).