Zhibin Yang
email: yangzhibin168@163.com

Shenghao Yuan
email: shyuan@nuaa.edu.cn

Jean-Paul Bodeveix
email: bodeveix@irit.fr

Mamoun Filali
email: filali@irit.fr

Tiexin Wang
email: tiexin.wang@nuaa.edu.cn

Yong Zhou
email: zhouyong@nuaa.edu.cn

Multi-task Ada Code Generation from Synchronous Dataflow Programs on Multi-core: Approach and Industrial Study

Keywords: Safety-critical systems, Synchronous dataflow language, Multi-task code generation, Ada, Multi core 2020 MSC: 00-01, 99-00

The growing trend to use multi-core processors to get more performance is increasingly present in safety-critical systems. Synchronous dataflow programming is naturally well-suited to parallel execution, thanks to the fact that all data dependencies are always explicit. MiniSIGNAL is a multi-task code generation tool for the synchronous dataflow language SIGNAL. The existing Min-iSIGNAL code generation strategies mainly consider coarse-grained parallelism based on Ada multi-task model. However, when we applied it to industrial case studies, this code generation scheme has revealed inefficient: architecture aspects of the target platform have to be taken into account to achieve finegrained parallelism. To generate more efficient target code from industrial cases, this paper presents a new multi-task code generation method for MiniSIGNAL.

Starting at the level of synchronous clocked guarded actions (S-CGA) which is an intermediate language for the compilation process of MiniSIGNAL, the transformation consists of two parts: at the platform-independent level, transforming the S-CGA representation to an abstract multi-task structure (called Virtual Multi-Tasks, VMT); at the platform-dependent level, adopting the thread pool pattern concurrent JobQueue to support fine-grained parallel Ada code genera-

Introduction

Safety-critical systems are those systems whose failure could result in loss of life, significant property damage, or damage to the environment. There are many well known examples in application areas such as avionics and space systems. Currently, Model-Driven Development (MDD) is generally accepted as a key enabler for the design of the safety-critical systems. For example, in the guidance of civil avionics software certification DO-178C [1], MDD (DO-331) and formal methods (DO-333) are considered as vital technology supplements. There are many MDD languages and approaches covering various modeling demands, such as UML for generic modeling, SysML for system-level modeling, AADL [START_REF] Feiler | Model-based engineering with AADL: An introduction to the SAE architecture analysis & design language[END_REF] for the architectural modeling and analysis of embedded systems, SCADE 1 and Simulink for functional modeling, and Modelica for multi-disciplines modeling.

Synchronous languages, which rely on the synchronous hypothesis, are widely adopted in the design and verification of safety-critical systems. There are several synchronous languages, such as LUSTRE [3] , ESTEREL [START_REF] Boussinot | The ESTEREL language[END_REF], SIGNAL [START_REF] Le Guernic | Programming Real-Time Applications with Signal[END_REF], QUARTZ [6], PRELUDE [START_REF] Pagetti | Multi-task implementation of multi-periodic synchronous programs[END_REF], SCADE, and so on. SCADE is the industrial version of LUSTRE, which is commercialized by ANSYS/ESTEREL TECHNOLO-GIES. SIGNAL is a kind of polychronous language, and it naturally considers a mathematical time model, in terms of a partial-order relation, to describe multi-clocked systems. Safety-critical systems have evolved to use multi-core processors to get higher computation performance to implement advanced functionalities, such as autonomous driving in the flight control. Several recent works focus on multi-task code generation and the scheduling and mapping of tasks to multi-core processors, with synchronous languages. For instance, the mapping of PRELUDE programs to many-core architectures [START_REF] Puffitsch | Mapping a multi-rate synchronous language to a many-core processor[END_REF], extension of SCADE code generator to support multi-core platform [9][10], parallel code generation of LUSTRE synchronous programs for a many-core architecture [11], compilation of ESTEREL for multi-core execution [12], generating OpenMPbased multi-threaded code from the intermediate representation of QUARTZ [13] [14]. In our case, building on our previous works, such as the mechanized semantics of a subset of SIGNAL in Coq [START_REF] Yang | A comparative study of two formal semantics of the SIGNAL language[END_REF], and the sequential code generation of SIGNAL [START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF] [START_REF] Hu | Simulation of real-time systems with clock calculus[END_REF], we mainly focus on the SIGNAL language.

Research Problems

In terms of multi-task code generation for SIGNAL, the existing SIGNAL compiler Polychrony2 uses micro-level threading which creates a large number of threads and equally large number of semaphores. Thus, Jose et al. [START_REF] Jose | Generating multithreaded code from polychronous specifications[END_REF] propose a process-oriented and non-invasive multi-task code generation using the sequential code generators in Polychrony and separately synthesise some programming glue. Moreover, in our previous works such as [START_REF] Yang | Towards a simple and safe objective caml compiling framework for the synchronous language SIGNAL[END_REF], we propose a novel multi-task code generator for SIGNAL, called MiniSIGNAL, which consists of the front-end (from SIGNAL to the intermediate language S-CGA (Synchronous Clocked Guarded Action)) and back-end (from S-CGA to target languages). For the back-end, this paper proposes a platform-independent structure called Virtual Multi-Tasks (VMT) which is defined as a common multi-task structure for different target platforms of our compiler.

For a synchronous program, several levels of parallelization are possible, such as inter-block parallelization (coarse-grained), intra-block parallelization (fine-grained), and so on. The existing MiniSIGNAL code generation strategies mainly consider coarse-grained parallelism based on Ada multi-task model.

However, this code generation scheme has revealed inefficient: architecture aspects of the target platform have to be taken into account to achieve fine-grained parallelism, for instance reusing in-cache data is always expected. Moreover, sometimes the task's execution time is very short. Hence, creating tasks and context-switching between them incur significant overhead. To generate more efficient target code from industrial cases, this paper presents a new multi-task code generation method for MiniSIGNAL.

We select Ada as the target language because Ada is an explicit-concurrency and high-safety programming language which is very popular in the safetycritical systems, especially in the aerospace industry such as Airbus, ESA, NASA and China Aerospace. The Ada language includes support for concurrency as part of the language standard, by means of Tasks, which are entities that denote concurrent actions, and inter-task communication mechanisms such as protected objects or the rendezvous mechanism. This model is targeted to support the concurrent functionalities that the software should support, providing coarsegrained parallelism. Recently, two complementary research lines are tackling the extension of Ada to support fine-grained parallelism, for instance: 1) The next revision of Ada standard (Ada 202x) [START_REF] Group | Ada 202x Language Reference Manual[END_REF] is currently considering a draft proposal of parallel model. It specifies that an Ada task (a concurrent activity) can represent multiple logical threads of control which can proceed in parallel within the context of well specified parallel regions: parallel blocks and parallel loops. However, it is still not available now. 2) Sara Royuela et al. [21] proposed the incorporation of the OpenMP parallel programming model into Ada. However, in OpenMP a structured concurrency is enforced and we do not always have such a structure. JobQueue is an alternative way to exploit finegrained parallelism. In this paper, we extend the multi-task code generation of MiniSIGNAL with concurrent JobQueue (i.e., several JobQueues with shared memory). For instance, one task is created for one core at initialisation time, a job is a set of data that is processed by a task. Thus the overhead of creat-ing/destroying tasks and context switching between them can be reduced. The jobs which belong to a task, are stored in a job queue, and workers are employed by the job scheduler to process the jobs. Efficient job scheduling improves resource utilization by automatically load-balancing jobs across workers, thereby enhancing the overall performance of the computation. Inspired by the work of [START_REF] Shams | Load balancing prioritized tasks via work-stealing[END_REF] and [START_REF] Chase | Dynamic circular work-stealing deque[END_REF], this paper presents a lock-free implementation of the work-stealing JobQueue scheduler in Ada.

In addition, the front-end of our compiler prototype has been proven in the proof assistant Coq3 [START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF]. In this paper, the formal syntax and the operational semantics of VMT are also mechanized in Coq. Invariants are put forward and allow the proof of an important structural property: when a task is started, its required data have already been computed.

Main Contributions

The main contributions of the paper can be summarised as follows:

• A new multi-task code generation approach is proposed for transforming S-CGA models to multi-task Ada code. The transformation is divided into two parts:

-Platform-independent level. A platform-independent structure, called Virtual Multi-Tasks (VMT), is defined as a common multi-task structure for different target platforms of our compiler. The transformation algorithm from S-CGA to VMT is given.

-Platform-dependent level. Concurrent JobQueue is adopted for implementing the platform-dependent parallel code to provide fine-grained parallelization. The transforming algorithm from VMT structures to multi-task Ada code is also presented.

• The formal syntax and the operational semantics of VMT are mechanized in the proof assistant Coq. A VMT contains a set of tasks that communicate through shared data and synchronise through a wait/notify mechanism. The Coq formalisation allows to establish an important property of the VMT structure: once a given number of notifications have been received, needed data have been computed and the task can run until completion.

• A real-world aerospace industrial case, the Guidance, Navigation and Control (GNC) system, is used to show the feasibility of the method presented in the paper. It mainly shows three subsystems of GNC which are suitable for modelling in SIGNAL: Attitude Determination subsystem, Orbit Calculation subsystem and Attitude Control subsystem. The subsystems are also used for the comparisons to indicate the effectiveness of various code generation strategies.

This paper is an extended version of our FTSCS 2019 conference paper [START_REF] Yuan | Automated ada code generation from synchronous dataflow programs on multicore: Approach and industrial study[END_REF].

The main extended parts can be summarised as follows:

• In Section 3.1, the details of the task partition approach has been given.

• In Section 3.2, we have enriched the formal definition of VMT (Virtual Multi Task Structure) in the proof assistant Coq. Compared with the conference version, we introduce an action language inside the tasks of VMT in order to make possible the composition of tasks as required by the partitioning methods. In addition, we define well-formedness conditions for VMTs based on conditional write-once and acyclicity properties, and the operational semantics of VMT as a synchronous transition system.

• In Section 3.3, we have improved the Ada code generation strategy by using concurrent JobQueue.

• In Section 4, the prototype tool has been presented.

• In Section 5, we have given a more detailed description of our industrial case studies. We take CASE C as the running example to illustrate the compilation phases step by step. The details of CASE B are still given (Appendix B).

Outline

The rest of this paper is organised as follows. Section 2 briefly introduces SIGNAL and the intermediate language S-CGA through an industrial case study. Section 3 presents the multi-task Ada code generation approach which includes the platform-independent level and the platform-dependent level. The prototype tool is presented in Section 4. Section 5 gives a real-world aerospace industrial case study to show the effectiveness of the proposed approach in this paper. Section 6 discusses related work and Section 7 provides concluding remarks and plans for future work.

Preliminaries

In this section, we first introduce the basic concepts of SIGNAL, and then give the definition of the intermediate language S-CGA.

SIGNAL

As declared in the synchronous hypothesis, the behaviours 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. So a variable (called signal ) in SIGNAL is an infinite sequence, at each instant, a signal may be present with a value or absent (denoted by ⊥). The set of instants where a signal x takes a value is the abstract clock (denoted by x). Two signals are synchronous if they are always present and absent at the same instants, which means they have the same abstract clock.

SIGNAL provides four primitive constructs to express the relations between signals: SIGNAL also provides several extended constructs to express control-related properties by specifying clock relations explicitly, for example set operators on clocks (union x 1 ˆ+x 2 , intersection x 1 ˆ*x 2 , difference x 1 ˆ-x 2 ). Each extended construct can be equivalently transformed into a set of primitive constructs.

• instantaneous function y := f (x 1 , x 2 , . . . , x n ) • delay y := x $ init c
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.

Each of the extended constructs can be defined in term of the primitive constructs [START_REF] Gamatié | Designing embedded systems with the Signal programming language: synchronous, reactive specification[END_REF], so we just consider the primitive constructs, that is kernel SIGNAL (kSIGNAL for short). Its abstract syntax is presented as follows:

P ::=x := f (x 1 , ..., x n ) ( instantaneous f unction) |x := x 1 $ init c (delay) |x := x 1 when x 2 (undersampling) |x := x 1 def ault x 2 (deterministic merging) |P |P (composition)
Running Example. We take one of the functions of Eliminate Initial Deviation in the Guidance, Navigation and Control (GNC) case study (See Section 5) to show the modelling in SIGNAL.

The GNC system is a core system supporting orbiting operations of spacecrafts, which undertakes the tasks of determining and controlling spacecraft attitude and orbit. (1

) γ ⇒ x = τ (immediate) (2) γ ⇒ next (x) = τ (delayed) (3) γ ⇒ assume (σ) ( assumption) (4) γ ⇒ read (x) ( input) (5) γ ⇒ write (x) ( output)
where,

• γ and σ are Boolean conditions over the variables of X, and their clocks.

For a variable x ∈ X, we denote:

its clock x, -its initial clock init( x), and the initial clock ticks only at the first instant of a signal.

• τ is an expression over X

The form (1) immediately writes the value of τ to the variable x. The form (2) evaluates τ in the given instant but changes the value of the variable x at its next instant of presence. The form (3) defines a constraint which has to hold when γ is defined and true. The form (4) shows x that gets a value provided by the environment while the form [START_REF] Le Guernic | Programming Real-Time Applications with Signal[END_REF] indicates the environment gets a value x if γ is defined and true. Guarded actions are composed by the parallel operator

||.

S-CGA models can be structurally generated from kSIGNAL programs by generating each construct separately, the details are introduced in [START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF]. Here we show the S-CGA model generated from the running example:

1 || true ⇒ Read x 2 || true ⇒ Read y 3 || true ⇒ Write jet DC 4 || true ⇒ Write count DC 5 || true ⇒ Write jet sign 6 || x ⇒ f := y + 0.05 * x 7 || x ⇒ C1 := (x < -0.5)&&(f < -0.25)&&(y < 0.15) || ...

Approach

The multi-task Ada code generation approach MTCodeGen adopts a modular architecture, which is shown in Fig. 1:

• Normalization: All extended constructs of the input SIGNAL programs are transformed into primitive constructs, and the normalisation result complies with the kSIGNAL syntax.

• kSIGNAL2SCGA: The normalized programs are transformed into the intermediate format S-CGA which is defined as a common representation for synchronous languages.

• Clock Calculus: The clock calculus contains several steps [START_REF] Le Guernic | Polychrony for system design[END_REF], for instance construction of an equation system over clocks and resolution of the system of clock equations.

• Dependency Analysis: The Data Dependency Graph (DDG) is constructed by read-write dependency relations.

• Partition Method: The Virtual Multi-Tasks (VMT) structure can be generated from the DDG and the initial/delayed information of S-CGA models by different partition methods. Such an abstract structure is expected to support some purposes, such as generating simulation code (e.g.

Simulink), verification (e.g. UPPAAL), and specific-platform code generation.

• VMT2Ada: The platform-dependent target executable code is generated from VMT by considering concurrent JobQueue.

Dependency Analysis and Task Partitioning

In the sequential code generation scheme, guarded actions are associated to each clock equivalence class of the clock tree, then the deterministic sequential code will be generated. In the multi-task code generation schema, the datadependency graph (DDG) should also be constructed and then the task partition algorithm is used to extract more parallelism.

Dependency Analysis

We construct the DDG based on reads and writes occurring in guarded actions. Notice that next(x) is considered as a new variable.

Definition 4 (Read and Write Dependencies) [START_REF] Baudisch | Dependency-driven distribution of synchronous programs[END_REF] Let F V (τ ) denote the free variables occurring in the expression τ . The dependencies from guarded actions to variables are defined as follows:

RdV ars (γ ⇒ write (x)) := F V (γ) ∪ {x} RdV ars (γ ⇒ x = τ ) := F V (γ) ∪ F V (τ ) RdV ars (γ ⇒ next (x) = τ ) := F V (γ) ∪ F V (τ ) W rV ars (γ ⇒ read (x)) := {x} W rV ars (γ ⇒ x = τ ) := {x} W rV ars (γ ⇒ next (x) = τ ) := {next (x)}
Then, the dependencies from variables to guarded actions are defined as follows:

RdActs (x) := {γ ⇒ A|x ∈ RdV ars (γ ⇒ A)} W rActs (x) := {γ ⇒ A|x ∈ W rV ars (γ ⇒ A)}
An action can only be executed if all read variables are known. Similarly, a variable is only known once all actions writing it in the current step have been evaluated. SIGNAL ensures that at most one write will be performed.

Definition 5 (Data Dependency Graph) Let GA be the set of guarded actions except assumption and V ar be the set of the variables of GA. A DDG is a directed acyclic graph GA, → D , where:

• → D ⊆ GA×V ar×GA is a data-dependency relation: ga 1 , v, ga 2 ∈→ D ⇔ v ∈ W rV ars(ga 1 ) and v ∈ RdV ars(ga 2 ).
The DDG describes the execution order of guarded actions. We ignore the initialisation information (immediate actions containing keyword init) and assumption actions when constructing the DDG, because the former only takes effect once while the latter is only used for constructing the clock tree. The DDG of the running example is shown in Fig. 2, where the labels represent variables appearing in the edges. For instance, 01, x, 06 denotes the variable x ∈ W rV ars(01) and x ∈ RdV ars(06).

Global Synchronization

The DDG specifies a partial order between variable updates. Once all variables determined to be present have been computed, the state of system, defined by the value of variables associated to next statement of the S-CGA which are present, must also be updated. Then, the next tick of the master clock will start a new cycle. Thus, a global synchronisation is introduced to wait for the completion of current step computations. We can imagine three implementations:

• for the system to be correct computations should complete before the occurrence of next input. Thus, the next input or a timer can fire the end of the current step. It is efficient but requires the study of environment and platform timing assumptions which are beyond the scope of this paper.

• a dependency between all the nodes of the dependency graph and the big step task is added. It follows that all the tasks should run, even if they are associated to absent variables. It is costly.

• the big step waits for tasks linked to present variable to complete. This set of task is dynamic but can be much smaller. This solution makes tasks associated to absent variables fully passive. We have retained this solution. Once variables associated to clocks have been computed, we know how many tasks must be waited for. This fact will be used to implement this global synchronisation between tasks attached to present variables.

In the next section, we will present the task partitioning over DDG from which we define the parallelism through elementary tasks.

Task Partitioning

There are several partition methods, such as the topological sorting way [START_REF] Hu | Simulation of real-time systems with clock calculus[END_REF], the vertical way [13] and the horizontal way [14]. This paper would like to give a general framework for task partitioning, in which we can use different partition methods [START_REF] Hu | Simulation of real-time systems with clock calculus[END_REF][13][14] and the partition combination patterns which will be presented in the following paragraphs.

Here we show the main idea in a general way: map the guarded actions to tasks one by one, and map the read/write dependencies to the synchronous communication between tasks. Moreover, combination is a key step for task partitioning to achieve more efficiency. In this paper, three combination patterns are proposed to optimise the partitioning result.

At first, several preliminary functions are defined.

• nGA = GA ∪ {n} \ {ga}, • → nD = { na, x, n | na, x, ga ∈→ D } ∪ { n, x, nb | ga, x, nb ∈→ D }
In addition, a cost function is introduced to evaluate the computation of each node in the graph, i.e., Cost(n) = {LOW, HIGH} for each node n. In this paper, the cost is given by the engineers, for example the numbers of statements in a node.

The essential idea of optimization is to merge as many nodes as possible.

Three partition combination patterns are proposed, as shown in Fig. 3.

Merge

Platform-Independent Level: VMT Generation

As mentioned above, S-CGA provides a common intermediate format to support more synchronous languages such as QUARTZ, AIF as the inputs of our compiler. However, the purpose of the introduction of VMT is to provide a common multi-tasking structure for different platform targets. The introduction of VMT increases the scalability of the MiniSIGNAL compiler. The scalability is manifested in two ways: First, it is expected to support both simulation analysis (translating to Simulink) and formal verification (e.g. UPPAAL) at the platform-independent level. Second, low-level abstract structure is easily transformed into various target executable code.

This section introduces the syntax and the operational semantics of a VMT based on Synchronous Transition System (STS) [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF]. A VMT is defined by a set of tasks synchronised by a wait-notify mechanism. Notifications could be associated to newly computed variables and sent to the reading tasks. However, to reduce the number of notifications, they specify task completion instead of single variable computations. Static properties make the link between the two viewpoints and ensure that once a task has received enough notifications, its required variables have been valued.

In the following, we first introduce tasks, their before-after semantics and then VMTs and their STS-based semantics.

Tasks

A task could be simply defined as guarded assignment as specified by a S-CGA statement. However, in order to make possible the composition of tasks as required by the partitioning methods presented in Section 3.1.3, we have introduced a small action language.

Actions. Starting with the Cond and Assign constructors allowing the specification of elementary guarded actions, we have added sequence (Seq), if-then-else (Ite) as well as a Load statement to make explicit the access to memory storage of past values. Moreover, we have introduced the Notify statement to notify target tasks about the completion of the calculus of some variables. Note that waits are not explicit: once a task is ready, its action part can execute without blocking.

The following Coq code defines the abstract syntax of the action language.

The Action type is parameterized by the type Id of variable identifiers which are supposed to have a decidable equality, the type Tid of task identifiers which are supposed to be iterable (i.e. they can all be put in a list) and the type M of identifier-data mappings 5 . The execution of an action is seen as atomic. Thus semantics of an action is defined as the condition under which a notification is sent and with which set of known variables. Thus, notifying a same target several times is forbidden.

As an example, the following Coq code defines the guard and action parts of task t24. The guard is a conjunction of two (boolean) variables c_C1to6 and

C1to6. The action is a sequence of three assignments. The guard is an expression defined as the conjunction of two Boolean variables. The action is defined by constructors introduced in this section. They allow sequences of conditional writes and notifications.

Tasks. A task is defined in the context of a VMT which is made of a set of tasks communicating through shared variables and synchronised by notifications. A task is a tuple Inputs, Counter, Body where,

• Inputs is (a super-set of) the set of variables required to be known for the task body to be computable.

• Counter is the number of notifications that the task waits for before starting its execution. It should be ensured that if the number of notifications reaches the value of the counter, all input variables are known.

• Body is an action defining the behavior of the task, which consists in computing variables and performing notifications. This Coq declaration should be completed by the proof of the three properties attached to tasks and guaranteeing its well-formedness. For example, we prove that the knowledge of the given inputs is sufficient to run the body. It has to be noted that the value given for the counter cannot be checked here:

the graph of tasks is needed for that and this static check should be done at the VMT level.

VMT Syntax

VMT defines a set of sequential behaviours called tasks. As shown in Section 3.1.2, after a global synchronisation, tasks are fired according to the wait/notify mechanism. When all tasks have completed, the state of the system is updated and an iteration is performed.

Definition 9 (Virtual Multi-Task (VMT)) A VMT structure is a tuple mem, Task, Init , where,

• mem is the set of memory locations.

• Task is the set of tasks (defined in the next paragraph).

• Init contains the initial values of memory locations.

The VMT structure is defined in Coq by a record of four fields.TaskId is the set of task identifiers. task associates a task definition to a TaskId. vmt_mem and vmt_init define the global memory and its initial state. It has to be noted that this acyclicity condition differs from the one derived from other synchronous languages such as LUSTRE where arcs of the dependency graph are unconditional. Thus, the direction of data flows may change during system execution. This hypothesis has consequences on the acceptability of the SIGNAL source code: it should be rejected if it contains some cyclic conditional dependencies. As a consequence, this property relies on a decidable sufficient condition. We have proved its decidability when arc labels are ignored.

Thus, the static test is for the moment more strict than necessary.

• For any set of tasks of sufficient cardinal, if their notification condition for target t is satisfied then the conditions of all input variables of t are also satisfied. This static property can be defined by the following formula that should be true for each set pids of tasks of cardinal greater or equal to the counter N of a given task t:

( p∈pids tk notifyCond p t) → v∈Inputs T p∈pids

tk notifyVar p t v

• There should exist at most one writer for each variable of the system. More precisely, the conjunction of writing conditions of the same variable by two distinct tasks should be unsatisfiable. It is thus possible for two guarded actions to update the same variable if their guards are exclusive. This can be the case for guarded actions derived from a default construct in SIGNAL or in the translation of synchronous automata where assignments would be state dependent.

These properties are decidable because the set of tasks is finite (declared Iterable in Coq) and clock conditions are abstracted as propositional formulas.

VMT Semantics

The semantics of a VMT is defined by a synchronous transition system (STS) which, given a set D of values is a triple S, V, .

→ where S is a set of states, V a set of variables and →⊆ S × (V D) × S is a set of transitions labelled by reactions defined as partial functions from V to D mapping simultaneously present variables to values. In order to give the semantics of a VMT, we first need to define the structure of an auxiliary state used to schedule the execution of the tasks. Its main constituents are the following:

• vmt env: the environment containing the value of currently known variables which will eventually constitute the STS reaction: once all tasks are completed, the environment contains the system reaction and the value of memorised variables.

• vmt done: the set of completed tasks.

• vmt prev: associates a task with the set of tasks from which it has received a notification.

• vmt wrt: associates a variable of the environment with the task that has produced its value.

Several invariant properties are associated to this structure. They are ensured by the initial empty environment (tasks should first read from memory), and preserved by each task execution.

• (vmt dreq) input variables of terminated tasks are known by the environment,

• (vmt dsub) running a terminated task would not create new variable-value mappings 6 ,

• (vmt prev) sources of notifications are in the set of terminated tasks,

• (vmt pdone) the notification condition of sources is satisfied by the environment,

• (vmt cnd) sources of variables are in the set of terminated tasks,

• (vmt wcnd) the writing condition of sources is satisfied by the environment.

The fields defining a VMT run-time state together with their invariant properties are formally defined in Coq as follows: A micro-step of the VMT selects a ready task and makes it update the The semantics of a VMT as a STS can now be given. The STS state is defined as the set of valued memory locations. For each macro step, a VMT runtime state is initialised. It contains an empty environment from which a maximal sequence of micro steps is run. Then, the memory contents is updated and the reaction label is built from two projections of the runtime state which contains the value of all the variables making the reaction as well as the value of memory variables. Remark: Here, we do not show the Coq representations of some concepts (such as variables, data type and data structure) which are derived from the source SIGNAL specifications.

VMT Generation

VMT can be structurally translated from S-CGA and DDG by generating The top-level structure of VMT is an infinite loop of elementary iterations:

the Main program calls the Init function, then keeps calling all tasks. Once all 575 tasks are completed, the Next function is called before the next loop.

For example, the VMT model translated from the running example is shown in Fig. 5. Where the dependency relation from DDG (e.g. "07;14 → 20;03" in Fig. 4) is transformed from the corresponding counter statements and notify statements (e.g. declared by t7 and t20 in Fig. 5). The Cond of t7 is an ifstructure while the condition of t20'Cond is omitted because its value is always true. In addition, the prefix "c "+ x, represents the clock of the x variable (in symbol x). According to the intuitive semantics of guarded actions, the clock "c "+ x is assigned to true before the variable x is computed, otherwise, the clock is set by false.

Platform-Dependent Level: Ada Code Generation

We could associate one Ada task to each DDG node and use the Ada rendezvous mechanism or protected objects to control race conditions. However, the generated code would be inefficient as it would contain too many tasks.

In addition, as mentioned before, the init data and the next update generated from the delay construct x = x1 $ init c are dealt with outside of the multi-task partition. The current data before next update, are always reused by the tasks, i.e., reusing in-cache data is expected. Moreover, sometimes the task's execution time is very short. Hence, creating tasks and context-switching between them incur significant overhead.

In this paper, we adopt concurrent JobQueue to support fine-grained parallelism for Ada. For instance, one task is created for one core at initialisation time, a job is a set of data that is processed by a task. Thus the overhead of creating/destroying tasks and context switching between them can be reduced. The jobs which belong to a task, are stored in a job queue, and workers are employed by the job scheduler to process the jobs. Efficient job scheduling improves resource utilization by automatically load-balancing jobs across workers, thereby enhancing the overall performance of the computation. In order to guarantee load balancing, we have chosen the lock-free work-stealing deque [22] [23] to implement the parallel computation of DDG (Fig. 6): Each job corresponds to one procedure in Ada, and each worker is bound to a specific core with one local deque. The deque's owner worker pushes and pops local job to and from the deque's bottom, and steals a job from other local deque if its deque becomes empty.

The type TID is used to specify the number of available cores provided by execution platforms.

Main". Secondly, all jobs corresponding to tasks in VMT with empty counter value are put into the lock-free work-stealing deque. Thirdly, the number of workers is set to the number of available CPUs in the target platform to achieve the fastest execution speed. Finally, when the counter value of c next is zero, 640 memory is updated, the deque is reinitialised and the value of three outputs is recorded.

Prototype Tool Support

As mentioned in Fig. 1, the MTCodeGen prototype tool also adopts a modu-645 lar architecture, which is implemented in the functional programming language OCaml. The statistical OCaml code of each module is shown in Table 1.

The architecture of the MTCodeGen tool consists of three layers: infrastructure, compilation and application, which is shown in Fig. 7. The infrastructure layer specifies that the tool is developed on the OCaml Eclipse plug-in OcaIDE 7 .

The compilation layer focuses on the compilation process from the source OCaml project to the MTCodeGen plug-in. Firstly, the whole project is compiled into an execution file, i.e. the MTCodeGen compiler, by using the OcaIDE environment; then the target plug-in is generated from the execution file according to the instantiation mechanism of Eclipse.

The application layer includes two particular applications of the MTCode-Gen compiler: Firstly, the compiler can consider SIGNAL models with a configuration file as the input, and generate multi-task Ada code. Secondly, the compiler has already been integrated with the AADL modelling environment OSATE 8 , to support the co-modelling with AADL and SIGNAL, and code generation.

Evaluation

We have conducted three case studies for evaluating our approach. The case studies have been selected to address and balance several considerations.

Industrial Case Studies

The Guidance, Navigation and Control (GNC) system is a core system supporting orbiting operations of spacecrafts, which undertakes the tasks of determining and controlling spacecraft attitude and orbit. GNC is composed of navigation sensors (such as navigation cameras, star sensors, gyroscopes, and accelerometers), actuators (such as reaction flywheels, nozzles, orbit-controlled engines), and control computers (AOCS) which process the guidance and control tasks of various sensors, perform orbit determination, orbit control, attitude determination and attitude control. In addition, a data process unit (DPU) is usually added between navigation sensors and AOCS to pre-process data sent by 7 http://www.algo-prog.info/ocaide/ 8 https://osate.org/ navigation sensors according to engineering guidelines. A simplified architecture of the GNC system is given in Fig. 8. The statistical data of the GNC system (AADL/SIGNAL models) is shown in Table 2.

In this paper, we select three subsystems (the bold font in the Table 2)

involved SIGNAL models as study cases.

• CASE A: Data Processing of Sun Sensor (DPSS). The subsystem mainly performs the computation about data processing according to the data received from sun sensors. • CASE B: Computation of Orbit Elements (COE). The subsystem is used to compute six Keplerian orbital elements at a particular time according to the system clock and the GPS data.

• CASE C: Eliminate Initial Deviation (EID). The subsystem eliminates the angular rate of attitude generated by the separation of satellites from launch vehicles by calling some three-axis attitude control algorithms of spacecraft.

Code Generation

The statistical data of Ada code generation (three case studies) is shown in Table 3. Here, we use CASE A to illustrate the whole compilation process of Ada code generation. For the CASE B, the Data Dependency Graph can refer to Appendix B. In addition, the details of CASE C have already been shown in the running example.

In CASE A, it involves two kinds of hardware devices: three sun sensors of the Satellite (Sa, Sb, Sc) and a sun sensor of the Solar Array (SA), each sun sensor has four batteries. The system receives the input data from the hardware devices, performs the data processing (including 4 parallel sub-processes) and sends the results to other subsystems (e.g. Data Processing of Star Sensor).

The main requirement of CASE A consists of:

• Req1.1: Converting the source data of the sensors (Sa, Sb, Sc) to the corresponding voltage value.

• Req1.2: Computing the voltage value of the four batteries of each sensor, if a sensor doesn't satisfy the related constraint, resetting the solar angle to zero, otherwise calculating the solar angle.

• Req1.3: Computing the filter of each solar angle by the filter algorithms.

• Req1.4: Using the data from two sensors (Sb and Sc) to calculate the projection of the sun vector in the satellite celestial coordinate system.

• Req2.1: Converting the source data of the sensor (SA) to the corresponding voltage value.

• Req2.2: Calculating the solar angle of the solar array.

Code Generation Strategies Comparison

Three cases are also used to experiment various code generation strategies comparisons for SIGNAL under a specific multi-core platform. The experiment contains purpose, environment, strategies, process, result, analysis and conclusion.

Experiment Purpose: We envision providing an experiment framework to the industry engineers. Three modules (Case A, Case B and Case C), i.e., Experiment Strategies: Four strategies are listed below:

• Coarse-grained: Multi-task code generation adopting the typical Ada rendezvous mechanism.

• Schneider: Multi-task code using the vertical task partition method [13].

• JobQueue: Multi-task code using a thread pool pattern [START_REF] Yuan | Automated ada code generation from synchronous dataflow programs on multicore: Approach and industrial study[END_REF].

• Concurrent JobQueue: Multi-task code using the aforementioned lock-free work stealing deque.

Where the Coarse-grained strategy, resembling the semaphore-style strategy adopted by Polychrony, is proposed in our previous work [START_REF] Yang | Towards a simple and safe objective caml compiling framework for the synchronous language SIGNAL[END_REF]. In addition, Schneider et al. mainly proposed two partition methods: the vertical strategy and the horizontal one [14]. We mainly consider the vertical one in this paper.

Experiment Process: Firstly, target programs are generated from three SIGNAL cases with adopting various strategies; Secondly, generated programs are executed on the platform with a specified number of cores (2, 4, 6 and 8). The Coarse-grained strategy like Polychrony produces a lot of micro tasks, thus it is costly. The vertical Schneider strategy is better than the first one, however it may also create many tasks when the DDG includes complex dependency relations, and lots of task switching may take much time to save registers, reload stack from memory, etc.

One benefit of JobQueue or concurrent JobQueue is that the number of tasks (or workers) is controlled by users: Users can specify the number of workers according to the specific physical platform. Workers randomly get jobs and execute them in parallel on respective cores, thus the time overhead of 'conflicts' among tasks is very low.

The Concurrent JobQueue strategy proposed in the paper has a better execution efficiency than the JobQueue strategy, the main reason is that the former adopts the combination patterns to reduce some administrative overhead, and also considers the lock-free work-stealing deque method for the purpose of better load balancing.

The experiment also validates the combination patterns and the concurrent between the cores' number and the execution efficiency. • The partition combination patterns improve the execution efficiency.

• The concurrent JobQueue strategy significantly improves the execution efficiency, comparing with other strategies.

Related Work

Several compilers for synchronous languages have been proposed, such as the commercial SCADE KCG code generator [START_REF] Colaço | SCADE 6: A formal language for embedded critical software development[END_REF], and the academic LUSTRE V6 [33], Heptagon [34], ESTEREL V5 929 , Averest10 for QUARTZ, Polychrony for SIGNAL, and so on. With the advent of multi-core processors, automated synthesis of multi-task code from synchronous languages has gradually become a hot research topic.

Here, we classify the related work based on different synchronous languages.

For a synchronous program, several levels of parallelization are possible, such

In [9], ANSYS presents a first step and an overview of the generation of parallel code from the SCADE application. Its principle is to rely on parallelism annotations on the model that does not affect the semantics but tells the compiler to generate independent tasks that communicate through channels.

The generated set of tasks form a Kahn Process Network (KPN). The actual implementation of the generated set of tasks on the final platform, as well as its timing analysis, is done afterwards and outside of the language.

The work [9] mainly focuses on the structure of generated code. Based on it, ANSYS gives a detailed extension of SCADE to generate parallel code that targets execution on Infineon's latest generation AURIX multi-core processor [10].

However, the solution of ANSYS requires the user to specify how to partition the model for parallel execution with annotations parallel subsets.

(4) SIGNAL

In terms of multi-task code generation for SIGNAL, the report [START_REF] Besnard | Code generation strategies in the Polychrony environment[END_REF] describes multi-task code generation strategies available in the Polychrony toolset, including clustered code generation with static and dynamic scheduling, distributed code generation. Jose et al. [START_REF] Jose | Generating multithreaded code from polychronous specifications[END_REF] propose a process-oriented and non-invasive multi-task code generation using the sequential code generators in Polychrony and separately synthesise some programming glue. Our previous works [16][19] present a sequential/multi-task code generator for SIGNAL.

Comparing with existing work of multi-task code generation for SIGNAL, this paper focuses on improving the efficiency of target code when applied to real-world aerospace industrial cases, by supporting of fine-grained parallelism with the concurrent JobQueue pattern.

(5) ESTEREL Li et al. [START_REF] Li | Mapping esterel onto a multi-threaded embedded processor[END_REF] present a multi-threaded processor that is the KEP3a, which allows the efficient execution of concurrent ESTEREL programs.

Yuan et al. [START_REF] Yuan | Efficient Compilation of Esterel for Multi-core Execution[END_REF] propose two distinct approaches that distribute ESTEREL threads evenly across multi-core architectures. The first approach statically distributes threads based on the computation intensity approximated by the number of instructions generated from each thread. The second approach distributes threads dynamically using a thread queue that dispatches a thread whenever a core becomes idle.

In general, compared with the data-flow synchronous languages such as LUSTRE, SCADE, PRELUDE, SIGNAL, and so on, ESTEREL offers control flow primitives to express reactive behaviors. As the threads within an ESTEREL program are tightly coupled, the distribution technique introduced in these works depends on the number of concurrent execution paths without data dependencies.

(6) QUARTZ Baudisch et al. [13] propose two synthesis procedures generating multi-threaded OpenMP-based C code from QUARTZ by vertical/horizontal partitioning respectively.

Furthermore, in [14], they show an automatic synthesis procedure that translates synchronous programs to software pipelines. Thereby, the original system does not need to be divided into threads, but they are automatically generated by cutting the original system into pipeline stages. It is based on pipelining these programs before turning them into OpenMP-based C-Code. By connecting all parts of the implementation by FIFO buffers, the execution of the stages can be desynchronised.

Compared to our approach, their work also consider fine-grained parallelism.

However, our target language is Ada and we introduce concurrent JobQueue to support fine-grained parallelism in the Ada multi-task model. In OpenMP a structured concurrency is enforced and we do not always have such a structure.

(7) Other variants of synchronous languages Li et al. [START_REF] Li | Using design space exploration for finding schedules with guaranteed reaction times of synchronous programs on multi-core architecture[END_REF] present the transformation from synchronous SystemJ code to implementation on two types of time-predictable cores, the evolutionary algorithm is used to evaluate multi-core scheduling solution for finding guaranteed reaction time of real-time synchronous programs for multi-core targets. It aims at finding the mapping and schedule of synchronous programs that guarantees, statically, reaction times when mapped onto a multi-core platform.

Yip et al. [START_REF] Yip | The forec synchronous deterministic parallel programming language for multicores[END_REF] introduce the ForeC language that enables the deterministic parallel programming of multi-cores. ForeC inherits the benefits of synchronous language ESTEREL, such as determinism and reactivity, along with the benefits and power of the C language, such as control and data structures. The ForeC compiler generates statically scheduled code for direct execution on a predictable parallel architecture. The aim is to generate code that is amenable to static timing analysis.

Conclusion and Future Work

Synchronous languages are widely adopted for the design and verification We will consider to introduce this new Ada parallel model proposed in Ada 202x. With the widespread advent of multi-core processors, it further aggravates the complexity of timing analysis. For instance, FAA has published the CAST-32A document [START_REF] Faa | Position Paper on Multi-core Processors -CAST-32A[END_REF] and some recommendations for time-predictability on multi-core, that is the timing behavior of a system must be analyzable and validable off-line. An interesting work is to estimate worst-case execution time (WCET)

of SIGNAL programs running on multiprocessors. Separate compilation of synchronous programs is also an important issue [START_REF] Benveniste | Application of interface theories to the separate compilation of synchronous programs[END_REF]. Constructive semantics [27] of SIGNAL provides a basis for the separate compilation of SIGNAL programs and we can implement it with several technologies such as interface theory. In addition, we are currently working on the whole proof of semantics preservation of MiniSIGNAL in Coq.

•

  undersampling y := x when b • deterministic merging y := x 1 def ault x 2 The instantaneous function and the delay are monoclock operators which mean all signals involved have the same abstract clock, while the undersampling and the deterministic merging are multiclock operators which represent the signals involved may have different clocks.

14 ||

 14 C1&&C1 ⇒ C1 DC := 500 || ... 20 || true ⇒ jet DC := C1 DC?C1 DC : ... : 0 24 || C1to6&&C1to6 ⇒ add DC := tmp DC + 1 25 || true ⇒ count DC := add DC?add DC : tmp DC 27 || init (true) ⇒ tmp DC := 0 || ... 29 || true ⇒ next (tmp DC) := count DC For instance, the instantaneous function f := y + 0.05 * x is transformed into the immediate action x ⇒ f := y + 0.05 * x, the delay construct tmp DC := count DC $ init 0 is translated into init(true) ⇒ tmp DC := 0 and true ⇒ next(tmp DC) := count DC, and the nested structure of deterministic merging (line 21 in the running example) is also transformed into the nested ternary operator (line 20).

Figure 1 :

 1 Figure 1: Multi-task Ada code generation approach MTCodeGen.

  DDG can be constructed by simply traversing S-CGA programs twice to calculate all data-dependency relations and optimizing them. A direct dependency relation will be removed, if it can be implied by other relations. For instance, true ⇒ Read x (line 01), x ⇒ f := y + 0.05 * x (line 06) and x ⇒ C1 := (x < -0.5)&&(f < -0.25)&&(y < 0.15) (line 07) can generate three direct relations 01, x, 06 , 01, x, 07 and 06, f, 07 , where the line numbers of the S-CGA model are used to note the corresponding guarded actions. 01, x, 07 is implied by the relations 01, x, 06 and 06, f, 07 , thus it can be omitted.

Figure 2 :

 2 Figure 2: The data-dependency graph.

  Pattern. Let a and b be two nodes in DDG. If a and b satisfy Ending(a) = {b} and Starting(b) = {a}, then a and b can be merged into one new node named a;b. As shown in Algorithm 1, the combination consists of firstly removing the edge { a, x, b } (line 4, here x represents the variable that is read by b and written by a), and then calling the Replacing function twice to replace a and b with a;b (line 5-line 6).

Figure 3 :Algorithm 1 1 :Algorithm 3

 3113 Figure 3: Partition Combination Patterns.

Figure 4 :

 4 Figure 4: The partitioning result.

5

  isM M m is true when m designates a memory location Inductive Action '{Id: EqDec} {Tid: Iterable} '{M:Mem Id}: Type := Skip (* does nothing *) | Load (v:Var Id) (m:Var Id) (ism:isM M m) (* loads v from memory location m *) | Notify (tid: Tid) (* notifies target task tid *) | Assign (v: Var Id) (e: Exp (VarDec Id)) (* assigns expression e to v *) | Seq (a1: Action) (a2: Action) (* sequential composition *) | Cond (c: Exp (VarDec Id)) (a: Action) (* conditional execution of action *) | Ite (c: Exp (VarDec Id)) (ift: Action) (iff: Action). (* if then else *)

  Definition t24_guard: Exp (VarDec VID_dec) := eAnd (eVar _ (vId c_C1to6)) (eVar _ (vId C1to6)). Definition t24_action: Action VID_dec TID_it M := Seq (Assign (vId c_add_DC) (eTrue _)) (Seq (Assign (vId add_DC) (eFun F_inc [eVar _ (vId m_DC)])) (Notify T25)).

The

  Coq definition of a task is shown below. Several auxiliary definitions are attached to tasks, derived from action observers. They provide helpers for the definition of wellformedness conditions. The last section defines the run-time task semantics with the help of the act_run function taking as parameters the memory contents (sM), the environment of currently known signal variables and the action of the task. It returns the updated environment and for each task identifier, the set of variables known when notified. Record Task '(Id: EqDec) (Tid: Iterable) (M:Mem Id): Type := { inputs: SV.set (VarDec Id); (* set of declared required variables *) counter : nat; (* number of notifications to be waited for *) body: Action Id Tid M; (* auxiliary definitions *) tk_requires := act_requires body; (* variables needed to run body *) tk_writes := act_writes body; (* variables written by body *) tk_writeCond := writesCond body; (* var -> condition to be written *) tk_notifyCond := notifiesCond body; (* tid -> condition to be notified *) (* well-formedness conditions *) twf_req: SV.subset tk_requires inputs; (* required variables are inputs *) twf_RO: SV.disjoint tk_writes inputs; (* input variables are unchanged *) twf_MRO: forall v, SV.set_In v (act_writes body) -> not (Inp v); (* no direct write in memory *) (* semantics *) tk_ensures (env: Env inputs) := act_ensures body (dom env); (* known variables after any execution *) tk_run (sM: sMem M) (env: Env inputs): act_state (tk_ensures env) Tid := act_run sM body (subEnv env twf_req) }. As an example, we define in Coq Task t24 of Figure 5. The body of the task is obtained by using the Cond action constructor to associate the action with its guard: Program Definition t24: Task TID_it M := {| inputs := SV.list2set (VarDec VID_dec) [vId m_DC; vId c_C1to6; vId C1to6];

•

  Record VMT '(Id: EqDec) := { TaskId: Type; (* set of task identifiers *) vmt_mem: Mem Id; (* internal state of the system *) vmt_init: vmt_mem; (* initial state of a task *) task: taskId -> Task Id TaskId vmt_mem }. Several important wellformedness conditions apply to a VMT and should be ensured by the translation from the data dependency graph and thus be guaranteed by the static analysis of the source (SIGNAL) model: The task graph should be acyclic. As mentioned in the definition of DDG, this property is expressed as a reachability condition in a graph labelled by Boolean expressions: any path built from dependency arcs labelled by a notification condition and such as the conjunction of conditions along the path is satisfied should be finite. This condition is a generalisation of Coq accessibility predicate Acc used to define the well-founded induction principle [31]. Here, we manage conditional arcs. Inductive vmt_acyclic '{Id: EqDec} (vmt: VMT Id) (tid: TaskId vmt) (d: Exp (VarDec Id)) : Prop := vmt_isReachable: (isSat d -> forall (pid: TaskId vmt) v, vmt_acyclic vmt pid (eAnd (tk_notifyVar (M:=vmt_mem vmt) (task pid) tid v) d)) -> vmt_acyclic vmt tid d.

  environment. Notifications and writes to variables are taken into account to update the corresponding fields. Then proof obligations associated to state invariants must have been proved. It comes to establish that when a task is launched, i.e. when its declared counter has been reached, its input variables are known by the environment. This is the main result related to VMT semantics. It is expressed in Coq as the ability to define the function vmt_step computing the next state after a micro step when the precondition VMT_enabled is fulfilled (the task has not yet run and has received enough notifications). The following Coq fragment only contains the header of the function. Several auxiliary variables are introduced before defining the next state. Then, thanks to the Program construct proof obligations are generated. They require to prove that all the stated invariants are preserved. The statement of the invariants together with the completion of these proofs constitute the main challenge of VMT definition. Program Definition vmt_step '{Id: EqDec} (vmt: VMT Id) (wf: VMT_WF vmt) (sM: vm t_smem vmt) (st: vmt_state wf sM) (en: VMT_enabled st) : vmt_state wf sM := ... The VMT runs while some ready task exists, which defines a macro-step (named vmt_steps) in the following Coq code: Inductive vmt_steps '{Id: EqDec} (vmt: VMT Id) (wf: VMT_WF vmt) {sM: vmt_smem vmt} (st: vmt_state wf sM) : vmt_state wf sM -> Prop := vmt_end: (VMT_enabled st -> False) -> vmt_steps st st | vmt_one: forall (h: VMT_enabled st) st', vmt_steps (vmt_step h) st' -> vmt_steps st st'.

Definition

  VMT_sem '{Id: EqDec} (vmt: VMT Id) (wf: VMT_WF vmt): sts _ := {| State := vmt_smem vmt; (* memory structure *) Init := vmt_init vmt; (* memory initialisation *) Next st r st' := (* transitions labelled by reactions *) exists vst', vmt_steps (vmt_init_step wf st) vst' /\ r = env2reaction (vmt_env vst') /\ (* projection to reaction *) st' = env2state (vmt_env vst') st (* projection to memory *) |}.

  each element separately, as shown in Algorithm 5. The algorithm first generates the Init field by the initial clock of S-CGA (line 03) and the Next(i.e. mem) field by the delay actions to update the memory (line 04). Each task is then produced from the vertices of the DDG (line 05 -line 18): For each vertex (i.e. a guarded action), the corresponding taskId is derived from the variable name (line 07); the Action field including most of the task body is generated from the guarded action(line 08); the Inputs field is generated from the Action (line 09); the Counter and Notify are generated according to two rules: for each edge whose ending vertex is the current vertex, their starting vertices are added 570 to the Counter (line 11 -line 12); likewise, for each edge whose starting vertex is the current vertex, their ending vertices are added to the Notify (line 13line 14). Then, the generated task is added to the Task field of VMT (line 17). Algorithm 5 VMT Generation.

Figure 5 :

 5 Figure 5: The VMT model of the running example(part).

Figure 6 :

 6 Figure 6: Lock-free work-stealing deque.

Figure 7 :

 7 Figure 7: The architecture of the MTCodeGen prototype tool.

Figure 8 :

 8 Figure 8: Guidance, Navigation and Control (GNC) system.

• Req2. 3 :

 3 Computing the filter of the solar angle. Our industrial partner specifies the requirement of CASE A as a SIGNAL model. Then the model, as the input program loaded on the prototype tool, is transformed into the multi-task Ada code. Here we start with the data dependency graph shown in Fig. 9 (a), in which the numbers of nodes stand for the locations where the corresponding guarded actions appear in the generated S-CGA model, the mapping relations between nodes and requirement specifications are also shown below the figure. Secondly, the partitioning result is shown in Fig. 9 (b) according to the combination patterns. Then, the VMT structure (Fig. 9 (c)) is generated from the S-CGA model and the DDG. Finally, The generated Ada code (e.g. task36) is shown in Fig. 9 (d).

Figure 9 :

 9 Figure 9: The compilation process of CASE A.

Finally, the average

  execution time of each generated program is recorded. Experiment Results: Fig.10 shows the experiment results of the three GNC subsystems (CASE A/B/C), where the abscissa expresses the number of cores and the ordinate indicates the average execution time. Discussion and Analysis: The average time shows the execution efficiency of generated Ada code using different strategies. Given the same number of cores, the execution efficiency ranking from high to low is: Concurrent JobQueue > JobQueue > Schneider > Coarse-grained.

Figure 10 :

 10 Figure 10: The experiment results of CASE A/B/C on multi-core

Figure 12 :

 12 Figure 12: The experiment results of CASE A with high computation

  of safety-critical systems. With the advent of multi-core processors, multi-task code generation for synchronous languages has become a trend. MiniSIGNAL is a multi-task code generation tool for SIGNAL. The existing MiniSIGNAL code generation strategies mainly consider coarse-grained parallelism based on Ada multi-task model. However the generated code is still inefficient when we apply the tool to the real-world aerospace industrial cases. Therefore, this paper presents a new multi-task code generation method for MiniSIGNAL, which supports fine-grained parallelism. Our method first generates a platformindependent multi-task structure (VMT) from the intermediate representation S-CGA, then generates target Ada code with the concurrent JobQueue pattern from VMT. Moreover, the formal syntax and the operational semantics of VMT are mechanised in the proof assistant Coq, to support the semantics preservation proof of the new multi-task code generation strategy proposed by this paper in the future. Finally, the industrial case study has shown that the approach is feasible.

  Definition 6 (Starting) Let ga be a node from a generated DDG G = GA, → D . The function Starting(ga) {ga | ga , x, ga ∈→ D }, maps ga to a set of nodes which have relationships with ga and pointing to ga.

Definition 7 (Ending) Let ga be a node from a generated DDG G = GA, → D . The function Ending(ga) {ga | ga, x, ga ∈→ D } , maps ga to a set of nodes which ga has relationships with. Definition 8 (Replacing) Let ga be a node from a generated DDG G = GA, → D , and let n be a new node which doesn't appear in G. The function Replacing(ga, n, G) nGA, → nD returns a new graph in which ga occurs in G are replaced with n, where

Table 1 :

 1 Main Modules of the MTCodeGen prototype tool.

	Module	Description	OCaml (lines)
	Normalization	input programs → kSIGNAL models	300+
	kSIGNAL2SCGA	kSIGNAL models → S-CGA models	300+
	Clock Calculus	resolution the equation system, etc	400+
	Dependency Analysis	S-CGA models → DDGs	100+
	Partition Method	S-CGA + DDG → VMT models	250+
	VMT2Uppaal	VMT models → UPPAAL models	300+
	VMT2Ada	VMT models → Ada code	300+

Table 2 :

 2 Statistical data of the GNC model.

		GNC component	Language	size(line)
		navigation cameras	AADL	100+
		star sensors	AADL	100+
	sensors	gyroscopes	AADL	100+
		. . .
		reaction flywheels	AADL	100+
		nozzles		AADL	200+
	actuators	orbit-controlled engines	AADL	100+
		. . .
			AD's Architecture	AADL	4000+
			DPSS	BA/SIGNAL 200+/200+
		AD	Shadow Region Detection	BA	300+
			. . .
			OCn's Architecture	AADL	3500+
		OCn	COE	BA/SIGNAL 300+/300+
			Argument of Periapsis	BA/SIGNAL 150+/100+
	AOCS
			. . .
			AC's Architecture	AADL	4200+
			EID	SIGNAL	200+
		AC	Capture Earth	BA	200+
			. . .
			OCl's Architecture	AADL	2000+
		OCl	. . .
	Total			AADL	20000+
				BA	2400+
				SIGNAL	2000+

Table 3 :

 3 Statistical data of generated code of three cases.

	Case	Task Number Synchronous Communication Size (line of Ada)
	CASE A	31	30	1000+
	CASE B	12	29	900+
	CASE C	11	21	600+

https://www.ansys.com/products/embedded-software/ansys-scade-suite

http://www.irisa.fr/espresso/Polychrony/

The Coq reference manual: https://coq.inria.fr/distrib/current/refman/

Averest Intermediate Format, http://www.averest.org/

It does not occur but the proof uses this property

http://www-sop.inria.fr/esterel.org/files/Html/Downloads/Downloads.htm

http://www.averest.org/

Acknowledgement. Supported by the National Natural Science Foundation of China (62072233,61502231), Aviation Science Fund of China (201919052002), and The Fundamental Research Funds for the Central Universities (NP2017205).

is called; Finally, the Merge Pattern is used to merge all possible nodes. A local deque presents three methods in its interface:

• PushBottom: pushing an object onto the bottom of the deque;

• PopBottom: poping an object from the bottom of the deque if the deque 615 is not empty, otherwise returning Empty;

• Steal : returning Empty if the deque is empty. Otherwise, returning the element successfully stolen from the top of the deque, or returning Abort if this worker loses a race with another worker to steal the topmost element. Each job has one counter with an initial value, which is the number of jobs it depends on. When one of them is completed, the value decreases by 1 (i.e. calling the procedure decr once). If the return value of decr z is zero, then the job can be executed. For instance, the Ada code generated from the running example is shown below. Firstly, initialised variables are declared in the structure "begin ... end The green one records the result of the target code using both the concurrent JobQueue and the combination patterns.

Comparing the blue line with the red one, it presents that the combination patterns reduce the execution time because these patterns reduce the number of tasks of the target code and cut down communication consumption by means of merging some tasks that are potentially suitable for sequential execution.

Comparing the red one with the green one, it shows that the concurrent JobQueue method further reduces the execution time: the concurrent JobQueue adopts the work-stealing deque method to achieve better load balancing and replaces the Ada rendezvous mechanism with the lock-free call.

Note that, all three kind of strategies suffer from a higher execution time when the number of cores is 6 or 8, one potential reason is that each node in the Fig 9 (b) has low computation (few equations/statements) and the cost of tasking administration could be greater than the cost of tasking computation along with the increase of the number of CPUs. To validate it, each node performs high computation, and Fig. 12 shows there is a positive correlation as inter-block parallelization (coarse-grained), intra-block parallelization (finegrained), etc. Moreover, task partition, synchronization, mapping and scheduling are the main topics in the multi-task code generation for synchronous languages.

(1) LUSTRE Graillat et al. [11] consider the top-level node of a LUSTRE application as a software architecture description where each sub-node corresponds to a potential parallel task. Given a mapping (tasks to cores), they automatically generate code suitable for the targeted many-core architecture. However, they focus on a minimal case where only the direct sub-nodes of the main node are implemented as parallel tasks.

Souyris et al. [START_REF] Souyris | Automatic parallelization from Lustre models in avionics[END_REF] propose a solution for automatic parallel code generation from LUSTRE/Heptagon models with non-functional specification (e.g. period). It is formed of two parts: the specification of each sequential task as a synchronous program (nodes), and the integration specification. Each task specification is compiled into sequential C code using a classical LUSTRE/Heptagon compiler. The integration specification describes how tasks communicate and synchronize. It is taken as input by the parallelization tool. So, they mainly consider node-level parallelization.

(2) PRELUDE Pagetti et al. [START_REF] Pagetti | Multi-task implementation of multi-periodic synchronous programs[END_REF] introduce a real-time software architecture description language, named PRELUDE, which is built upon the synchronous language LUSTRE and which provides a high level of abstraction for describing the functional and the real-time architecture of a multi-periodic control system. They have given a compilation from PRELUDE to multi-task execution on a monoprocessor real-time platform with an on-line priority-based scheduler such as Deadline-Monotonic or Earliest-Deadline-First. [START_REF] Puffitsch | Mapping a multi-rate synchronous language to a many-core processor[END_REF] describes a static mapping from dependent real-time task sets which are specified by PRELUDE, to a many-core platform. Furthermore, it gives a lightweight run-time environment for scheduling and execution of the resulting real-time system. Thus, their main consideration is the mapping and scheduling of multi tasks on a platform.