# Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties (ACVI 2014)

Zhibin Yang, Jean-Paul Bodeveix, M Filali

► To cite this version:

Zhibin Yang, Jean-Paul Bodeveix, M Filali. Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties (ACVI 2014). 1st International Workshop on Architecture Centric Virtual Integration (ACVI 2014), Sep 2014, Valencia, Spain. pp.1-10. hal-01150341

HAL Id: hal-01150341

https://hal.science/hal-01150341

Submitted on 11 May 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Open Archive TOULOUSE Archive Ouverte (OATAO)

OATAO is an open access repository that collects the work of Toulouse researchers and makes it freely available over the web where possible.

This is an author-deposited version published in : http://oatao.univ-toulouse.fr/
Eprints ID : 13210

**To cite this version** : Yang, Zhibin and Bodeveix, Jean-Paul and Filali, Mamoun *Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties*. (2014) In: ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Workshop on Architecture Centric Virtual Integration - MODELS 2014, 28 September 2014 - 3 October 2014 (Valencia, Spain).
# Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties

Zhibin Yang, Jean-Paul Bodeveix, and Mamoun Filali

IRIT-CNRS, Université de Toulouse, France

{Zhibin.Yang,bodeveix,filali}@irit.fr

**Abstract.** Synchronous programming models capture concurrency in computation quite naturally, especially in its dataflow multi-clock (polychronous) flavor. 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 for multi-core systems. This paper proposes a build method of time-predictable system on multi-core, based on synchronous-model development. At the modeling level, the synchronous abstraction allows deterministic time semantics. Thus synchronous programming is a good choice for time-predictable system design. At the compiler level, the verified compiler from the synchronous language SIGNAL to our intermediate representation (S-CGA, a variant of guarded actions) and to multi-threaded code, preserves the time predictability. At the platform level, we propose a time-predictable multi-core architecture model in AADL (Architecture Analysis and Design Language), and then we map the multi-threaded code to this model. Therefore, our method integrates time predictability across several design layers.

**Keywords:** Synchronous languages, SIGNAL, Guarded actions, Verified compiler, Multi-core, Time predictability, AADL

## 1 Introduction

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 [1, 21, 20] 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 in this category of systems, it further aggravates the complexity of timing analysis.

The synchronous abstraction allows deterministic time semantics. Therefore synchronous programming is a good choice for time-predictable system design. There are several synchronous languages, such as ESTEREL [5], LUSTRE [12] and QUARTZ [16] based on the *perfect synchrony* paradigm, and SIGNAL [4] based on the *polychrony* paradigm.
An integration infrastructure for different synchronous languages has gained a lot of interests in recent years [6, 19]. A classical solution is to use an intermediate representation. Guarded commands [10], also called asynchronous guarded actions by J. Brandt et al. [6], 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 [8] 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 $\langle \gamma \Rightarrow A \rangle$. The boolean condition $\gamma$ is called the guard and $A$ is called the action. To support the integration of synchronous, polychronous and asynchronous models (such as CAOS or SHIM), they propose an extended intermediate representation, that is clocked guarded actions [6] 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. [7] presents an embedding of polychronous programs into synchronous ones. The embedding gives us access to the methods and tools that already exist for synchronous specifications.

<figure><img src="image_2.png" /><figcaption>Fig. 1. A global view of the relation between our work and related work</figcaption></figure>

For a safety-critical system, it is required that the compiler must be verified to ensure that the source program semantics is preserved. Our work mainly focuses on the SIGNAL language. We would like to extract a verified SIGNAL 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. Our intermediate representation is a variant of clocked guarded actions (called S-CGA), and currently the target is multi-core code. In [23], we have already presented the compilation of sequential code and the proof of semantics preservation of the transformation from the kernel SIGNAL to S-CGA. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics) [11], denotational semantics based on tags which puts forward a partial order view of time (called tagged model semantics) [11], structural operational semantics defining inductively a set of possible transitions
[4, 11], etc. In [22], 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. The relation between our work and related work is shown in Fig. 1.

The contribution of this paper is to propose a build method of time-predictable system on multi-core, based on synchronous-model development. At the modeling level, synchronous programming is a good choice for time-predictable system design. At the compiler level, the verified compiler from the synchronous language SIGNAL to our intermediate representation (S-CGA, a variant of guarded actions) and thus to multi-threaded code, preserves the time predictability. At the platform level, we propose a time-predictable multi-core architecture model in AADL (Architecture Analysis and Design Language) [15], and then we map the multi-threaded code to this model.

The rest of this paper is structured as follows. Section 2 presents the abstract syntax and the semantics of S-CGA. Section 3 gives the multi-threaded code generation schema from S-CGA. The time-predictable multi-core architecture model and the mapping from multi-threaded code to that model are presented in Section 4. Section 5 gives some concluding remarks.

## 2 S-CGA

In papers such as [6], clocked guarded actions has been defined as a common representation for synchronous (via synchronous guarded actions), polychronous and asynchronous (via asynchronous guarded actions) models. It has a multi-clocked feature. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold [6] for supporting the asynchronous view. Since we focus on the polychronous view, we introduce S-CGA, which is a variant of clocked guarded actions. S-CGA constrains variable accesses as done by SIGNAL. 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 1 (S-CGA).** A S-CGA system is represented by a set of guarded actions of the form $\langle \gamma \Rightarrow \mathcal{A} \rangle$ defined over a set of variables $X$. The Boolean condition $\gamma$ is called the guard and $\mathcal{A}$ is called the action. Guarded actions can be of the following forms:

(1) $\gamma \Rightarrow x = \tau$ (immediate)

(2) $\gamma \Rightarrow next(x) = \tau$ (delayed)

(3) $\gamma \Rightarrow assume(\sigma)$ (assumption)

where

- the guard $\gamma$ is a Boolean condition over the variables of $X$, their respective clocks (for a variable $x \in X$, we denote its clock $\hat{x}$), and their respective initial clocks (denoted $init(\hat{x})$),
- $\tau$ is an expression over $X$,

- $\sigma$ is a Boolean expression over the variables of $X$ and their clocks.

An immediate assignment $x = \tau$ writes the value of $\tau$ immediately to the variable $x$. The form (1) implicitly imposes that if $\gamma$ is defined<fnref n="1" /> and its value is true, then $x$ is present and $\tau$ is defined. Moreover, $init(\hat{x})$ exactly holds the first instant when $x$ is present.

A delayed assignment $next(x) = \tau$ evaluates $\tau$ in the given instant but changes the value of the variable $x$ at next time clock $\hat{x}$ ticks.

The form (3) defines a constraint. It determines a Boolean condition which has to hold when $\gamma$ 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 $\parallel$.

An S-CGA example<fnref n="2" /> (Example 1) is shown as follows.

<table><tr><td>true &rarr; assume(y&#x0302;<sub>1</sub> = x&#x0302;)</td><td>z&#x0302; &and; z &rarr; s<sub>1</sub> = f(y<sub>1</sub>)</td></tr><tr><td>init(y&#x0302;<sub>1</sub>) &rarr; y<sub>1</sub> = 1</td><td>s&#x0302;<sub>2</sub> &rarr; s<sub>2</sub> = s<sub>1</sub> + 1</td></tr><tr><td>y&#x0302;<sub>1</sub> &rarr; next(y<sub>1</sub>) = x</td><td>s&#x0302;<sub>1</sub> &rarr; assume(s&#x0302;<sub>2</sub>)</td></tr><tr><td>true &rarr; assume(y&#x0302;<sub>2</sub> = x&#x0302;)</td><td>s&#x0302;<sub>3</sub> &rarr; assume(z&#x0302; &and; (not z))</td></tr><tr><td>init(y&#x0302;<sub>2</sub>) &rarr; y<sub>2</sub> = 2</td><td>z&#x0302; &and; (not z) &rarr; s<sub>3</sub> = f(y<sub>2</sub>)</td></tr><tr><td>y&#x0302;<sub>2</sub> &rarr; next(y<sub>2</sub>) = x</td><td>s&#x0302;<sub>4</sub> &rarr; s<sub>4</sub> = s<sub>3</sub> + 2</td></tr><tr><td>true &rarr; assume(x&#x0302; = z&#x0302;)</td><td>s&#x0302;<sub>3</sub> &rarr; assume(s&#x0302;<sub>4</sub>)</td></tr><tr><td>s&#x0302;<sub>1</sub> &rarr; assume(z&#x0302; &and; z)</td><td></td></tr></table>

**Definition 2 (Trace semantics of S-CGA).** The trace semantics of a S-CGA system is defined as a set of traces, that is $[SCGA] = \{S | \forall scga \in SCGA, [[scga]]_S = true\}$. We have the following semantics rules,

$$ (1) \quad [[\gamma \Rightarrow x = \tau]]_S = \\ \quad \forall i \in \mathbb{N}, [[\gamma]]_{S,i} \land [[\gamma]]_{S,i} \\ \quad \rightarrow ([\widehat{x}]_{S,i} \land [\widehat{\tau}]_{S,i} \land [x]_{S,i} = [\tau]_{S,i}) $$

$$ (2) \quad [[\gamma \Rightarrow next(x) = \tau]]_S = \\ \quad \forall i_1 < i_2 \in \mathbb{N}, \\ \quad ((\forall i' \in \mathbb{N}, i_1 < i' < i_2 \rightarrow \neg [\widehat{x}]_{S,i'} \land [\widehat{\gamma}]_{S,i_1} \land [\gamma]_{S,i_1}) \\ \quad \rightarrow ([\widehat{x}]_{S,i_1} \land [\widehat{\tau}]_{S,i_1} \land ([\widehat{x}]_{S,i_2} \rightarrow [x]_{S,i_2} = [\tau]_{S,i_1})) $$

$$ (3) \quad [[\gamma \Rightarrow assume(\sigma)]]_S = \\ \quad \forall i \in \mathbb{N}, [[\gamma]]_{S,i} \land [[\gamma]]_{S,i} \rightarrow [\widehat{\sigma}]_{S,i} \land [\sigma]_{S,i} $$

- Rule (1): when $\gamma$ is present, and the value of $\gamma$ is true, $x$ and $\tau$ are both present, and the value of $x$ is that of $\tau$.

- Rule (2): when $\gamma$ is present and the value of $\gamma$ is true at instant $i_1$, $x$ and $\tau$ are present at $i_1$, and if $i_2$ is the next instant where $x$ is present, then the value of $x$ at $i_2$ is that of $\tau$ at instant $i_1$.

<footnote n="1">¹ An expression is said to be defined if all the variables it contains are present.</footnote>

<footnote n="2">² If two guarded actions update the same variables, the guards must be exclusive.</footnote>
– Rule (3): when $\gamma$ is present, and the value of $\gamma$ is true, $\sigma$ is present and true.

The semantics of S-CGA composition is defined as $[[scga_1 || scga_2]]_S = [[scga_1]]_S \wedge [[scga_2]]_S$.

In [23], we have already presented the translation rules from the kernel SIGNAL to S-CGA, and give the proof of the semantics preservation in Coq.

## 3 From S-CGA to Multi-threaded Code

The SIGNAL compilation process contains one major analysis called *clock calculus* from which *code generation* directly follows. Moreover, the clock calculus contains several steps, such as the synchronization of each process, i.e., an equation system over clocks; the resolution of the system of clock equations; the construction of a clock hierarchy on which the automatic code generation strongly relies. Our goal here is to adapt the clock calculus to S-CGA.

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

<table><thead><tr><th>S-CGA</th><th>Clock Equations</th></tr></thead><tbody><tr><td>$\gamma \Rightarrow x = \tau$</td><td>$\hat{\gamma} \wedge \gamma \rightarrow \hat{x} \wedge \hat{\tau}$</td></tr><tr><td>$\gamma \Rightarrow next(x) = \tau$</td><td>$\hat{\gamma} \wedge \gamma \rightarrow \hat{x} \wedge \hat{\tau}$</td></tr><tr><td>$\gamma \Rightarrow assume(\sigma)$</td><td>$\hat{\gamma} \wedge \gamma \rightarrow \hat{\sigma} \wedge \sigma$<br>$init(\hat{x}) \rightarrow \hat{x} (\forall x \in X)$</td></tr></tbody></table>

As a first step, we just consider the *endochrony* property $^3$, namely we can construct a clock hierarchy based on the resolution of the system of clock equations. The clock hierarchy of Example 1 (with three clock equivalence classes C0, C1, and C2) is shown in Fig. 2. In the figure, for instance *clk_x* denotes $\hat{x}$.

<figure><img src="image_3.png" /><figcaption>**Fig. 2.** Clock hierarchy</figcaption></figure>

Moreover, we construct the data-dependency graph (DDG, as shown in Fig. 3) based on the variables reading and writing.

Finally, the multi-threaded code generation is based on both the clock hierarchy and the data dependency graph. First, we map the guarded actions to threads (i.e. partitions, as shown in Fig. 3). As presented in Fig. 4, we would like to treat the partition methods generally, this means different partition methods (such as the vertical way [2] for a concurrent execution, the horizontal way [3])

<footnote>$^3$ The weak endochrony [14] property will be considered in the future.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 3. Data dependency graph</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 4. The proof idea</figcaption></figure>

for a pipelined execution, etc) don't affect the proof (here we don't consider performance). Second, in each thread, we organize the guarded actions based on the clock hierarchy. For example, the two guards in Thread2 belong to the same clock equivalence class, so they are merged inside the same control condition in the generated code. Third, we add wait/notify synchronization among the threads. A code fragment of Thread2 is given as follows.

/* Thread 2 */
void step()
{
    wait(thread1);
    if (C1) {
        s1 = f(y1);
        s2 = s1 + 1;
    }
    notify(thread4);
}

## 4 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.
<figure><img src="image_6.png" /><figcaption>Fig. 5. A time-predictable multi-core architecture model</figcaption></figure>

processor core
features
MC: requires bus access cache_bus;
SC: requires bus access cache_bus;
SDC: requires bus access cache_bus;
CDC: requires bus access cache_bus;
end core;

processor implementation core impl
properties
Multi_Core_Propertiet::Branch_Prediction => Static;
Multi_Core_Propertiet::Execution_OOrder => In_OOrder;
end core impl;

system multicore
features
ExtMem: provides bus access shared_bus impl;
end multicore;

system implementation multicore impl
subcomponents
Core1: processor core impl { Multi_Core_Propertiet::Core_Id => 1; };
Core2: processor core impl { Multi_Core_Propertiet::Core_Id => 2; };
Cache MC1: memory method_cache impl { Multi_Core_Propertiet::MC_Id => 1; };
Cache MC2: memory method_cache impl { Multi_Core_Propertiet::MC_Id => 2; };
...
SBus: bus shared_bus impl;
C2CBus1: bus cache_bus;
C2CBus2: bus cache_bus;
connections
bus access C2CBus1 -> Core1.MC;
bus access C2CBus2 -> Core2.MC;
bus access SBus -> Cache MC1. Cache Bus;
bus access SBus -> Cache MC2. Cache Bus;
...
end multicore impl;

<caption>Fig. 6. A part of the AADL specification of the time-predictable multi-core architecture</caption>

## 4.2 The mapping method

To preserve the time predictability, we consider static mapping and scheduling. Take the example shown in the last section. 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 $\mapsto$ Core1, Thread2 $\mapsto$ Core2, Thread3 $\mapsto$ Core3, and Thread4 $\mapsto$ Core4.

- Thread1: notify(thread2), notify(thread3);
  Thread2: wait(thread1), notify(thread4);
  Thread3: wait(thread1), notify(thread4);
  Thread4: wait(thread2), wait(thread3).

Based on the simplified instruction set (considered in the architecture model),
the multi-core code can be generated. Thanks to the mechanizations such as
method cache, split data caches, TDMA and static scheduling, the execution
time of the multi-core code can be bounded.

5 Conclusion and Future Work

With the widespread advent of multi-core processors in safety-critical embedded
systems or cyber-physical systems (CPS), it further aggravates the complexity of
timing analysis. This paper proposes a build method of time-predictable system
on multi-core, based on synchronous-model development. Our method integrates
time predictability across several design layers, i.e., synchronous programming,
verified compiler, and time-predictable multi-core architecture model. Interac-
tion among cores might also arm software isolation layers, such as the one defined
in ARINC653. Thanks to the existing work such as [9] and [13] on AADL model-
ing on multi-core architectures and their association with ARINC653, we would
like to associate our work with partitioned architectures in the future.

**Acknowledgments:** This work was supported by the RTRA STAE Foun-
dation in France (http://www.fondation-stae.net/).

References

1. P. Axer, R. Ernst, H. Falk, A. Girault, D. Grund, N. Guan, B. Jonsson, P. Mar-wedel, J. Reineke, C. Rochange, M. Sebastian, R. V. Hanxleden, R. Wilhelm, and W. Yi. Building timing predictable embedded systems. *ACM Trans. Embed. Com-put. Syst.*, 13(4):82:1–82:37, Mar. 2014.

2. D. Baudisch, J. Brandt, and K. Schneider. Multithreaded code from synchronous programs: Extracting independent threads for OpenMP. DATE ’10, pages 949–952, 2010.

3. D. Baudisch, J. Brandt, and K. Schneider. Multithreaded code from synchronous programs: Generating software pipelines for OpenMP. In M. Dietrich, editor, *MBMV*, pages 11–20. Fraunhofer Verlag, 2010.

4. A. Benveniste, P. L. Guernic, and C. Jacquemot. Synchronous programming with events and relations: the signal language and its semantics. *Science of Computer Programming*, 16:103–149, 1991.

5. F. Boussinot and R. de Simone. The esterel language. *Proceedings of the IEEE*, 79(9):1293–1304, 1991.
6. J. Brandt, M. Gemünde, K. Schneider, S. K. Shukla, and J.-P. Talpin. Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. *Design Automation for Embedded Systems*, pages 1–35, 2012.

7. J. Brandt, M. Gemünde, K. Schneider, S. K. Shukla, and J.-P. Talpin. Embedding polychrony into synchrony. *IEEE Trans. Software Eng.*, 39(7):917–929, 2013.

8. J. Brandt and K. Schneider. Separate translation of synchronous programs to guarded actions. *Internal Report 382/11, Department of Computer Science, University of Kaiserslautern*, 2011.

9. J. Delange and P. Feiler. Design and analysis of multi-core architecture for cyberphysical systems. In *5th Embedded Real Time Software and Systems, ERTS'14*, February 2014.

10. E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. *Commun. ACM*, 18(8):453–457, 1975.

11. A. Gamatié. *Designing embedded systems with the SIGNAL programming language*. Springer, 2010.

12. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language lustre. *Proceedings of the IEEE*, 79(9):1305–1320, 1991.

13. J. Hugues. AADLib, a library of reusable AADL models. In *SAE Aerotech 2013 Congress & Exhibition (Montreal, Canada)*, September 2013.

14. D. Potop-Butucaru, B. Caillaud, and A. Benveniste. Concurrency in synchronous systems. *Formal Methods in System Design*, 28(2):111–130, 2006.

15. SAE. AS5506A: Architecture Analysis and Design Language (AADL) Version 2.0. 2009.

16. K. Schneider. The synchronous programming language quartz. *Internal report, Department of Computer Science, University of Kaiserslautern, Germany*, 2010.

17. M. Schoeberl. A time predictable instruction cache for a Java processor. In R. Meersman, Z. Tari, and A. Corsaro, editors, *On the Move to Meaningful Internet Systems 2004: OTM 2004 Workshops*, volume 3292 of *Lecture Notes in Computer Science*, pages 371–382. Springer, 2004.

18. M. Schoeberl, B. Huber, and W. Puffitsch. Data cache organization for accurate timing analysis. *Real-Time Systems*, 49(1):1–28, 2013.

19. J.-P. Talpin, J. Brandt, M. Gemünde, K. Schneider, and S. Shukla. Constructive polychronous systems. In *Logical Foundations of Computer Science*, volume 7734 of *Lecture Notes in Computer Science*, pages 335–349. Springer, 2013.

20. L. Thiele and R. Wilhelm. Design for timing predictability. *Real-Time Syst.*, 28(2-3):157–177, Nov. 2004.

21. R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström. The worst-case execution-time problem: Overview of methods and survey of tools. *ACM Trans. Embed. Comput. Syst.*, 7(3):36:1–36:53, May 2008.

22. Z. Yang, J.-P. Bodeveix, and M. Filali. A comparative study of two formal semantics of the SIGNAL language. *Frontiers of Computer Science*, 7(5):673–693, 2013.

23. Z. Yang, J.-P. Bodeveix, M. Filali, H. Kai, and D. Ma. A verified transformation: From polychronous programs to a variant of clocked guarded actions. In *International Workshop on Software and Compilers for Embedded Systems (SCOPES)*, SCOPES '14, pages 128–137. ACM, 2014.

24. Z. Yang, K. Hu, D. Ma, J.-P. Bodeveix, L. Pi, and J.-P. Talpin. From AADL to timed abstract state machines: A verified model transformation. *Journal of Systems and Software*, 93:42–68, 2014.