Jonathan Dupuy
email: jdupuy@liris.cnrs.fr

Eric Bruneton
email: ebruneton@free.fr

Real-time Animation and Rendering of Ocean Whitecaps

Keywords: I.3.3 [Computer Graphics]: Picture/Image Generation-Antialiasing I.3.7 [Computer Graphics]: Color, shading, shadowing, and texture-; whitecaps, ocean, BRDF, real-time

: Some real-time results obtained with our method showing large ocean scenes with whitecaps under different wave and illumination conditions. The whitecap contribution is correctly averaged as the viewing distance increases.

Introduction

Oceans are highly dynamic structures: their surface is constantly perturbed through time by waves of different directions, wavelengths and amplitudes. When conditions prevail [START_REF] Cokelet | Breaking waves[END_REF]], some of these waves break, causing very perceptible reflectance changes -called whitecaps-and geometrical alterations on the ocean surface. In digital environments, these phenomenons can be reproduced through complex mathematical models, which often require a lot of processing power.

Whenever applications can not afford high simulation times, such as video games, only the models meeting the computational constraints can be employed. In general, these models either completely ignore whitecaps or use very crude empirical approximations [Premoze and Ashikhmin 2001;[START_REF] Darles | Accelerating and Enhancing Rendering of Realistic Ocean Scenes[END_REF]]. Recent methods can offer more plausible results through the use of particle systems [Chentanez and Müller 2011]; however, such solutions do not scale well enough to handle vast environments. Hence a huge gap exists between the quality of ocean scenes produced by realtime renderers and offline simulators.

In this work, we present a procedural whitecap generation algorithm which narrows down this gap. Our method runs entirely on the GPU and allows us to render high quality ocean scenes in a few milliseconds. In the two following sections, we show how to produce a scalable ocean surface and derive a whitecap model with linear parameters, which in turn can be evaluated for any viewing resolution by the hardware. We then give some implementation details and conclude our paper in the fifth section.

Ocean Model Wave Model

The core of our wave model is based on the Choppy Wave Model [START_REF] Tessendorf | Simulating Ocean Water[END_REF]]: At a given time, the vertical and horizontal perturbations produced by the ocean waves can be approximated by sampling an empirical spectrum in frequency space. Because the sampling process can be done through a Fast Fourier Transform, the resulting deformations can be bounded to a small area and tiled seamlessly on the ocean surface.

Tiling a single perturbation pattern however leads to repetitive artifacts or lack of detail depending on the observation scale. Previous work solves this by generating additional noise on the surface [START_REF] Rydahl | A VFX ocean toolkit with real time preview[END_REF][START_REF] Nvidia | Ocean Surface Simulation[END_REF]. Instead, we chose to compute a number n ∈ N * + of patterns, each sampling a different part of the wave spectrum. This approach does not remove the periodicity of the final wave field, but rather increases it to the least common multiple of the n pattern periods (in practice, n = 4 is enough to avoid artifacts). It also provides an analytical expression for the whole ocean surface: Given a point p(px, py, pz) located on the ocean plane at rest, its position q(qx, qy, qz) at time t is given by

q(p, t) = p + n-1 i=0   λiui(p, t) λivi(p, t) wi(p, t)   , λi ∈ R + (1)
where wi(p, t) (resp. Di(p, t) = [ui(p, t), vi(p, t)] T ) is the choppy wave model's vertical (resp. horizontal) deformation function for a fixed pattern size [START_REF] Tessendorf | Simulating Ocean Water[END_REF]], and λi is an artistic parameter which controls the choppiness of the waves.

Surface Mesh

In order to represent the ocean surface efficiently, a multi-resolution meshing scheme has to be employed. We chose to use the projected grid [START_REF] Hinsinger | Interactive Animation of Ocean Waves[END_REF]]: a mesh is generated in screen space and reprojected on the ocean plane in the world coordinate system. Each vertex is then displaced by evaluating (1) and reprojected to the screen. This approach naturally provides adaptive level of detail with constant memory consumption, which is very convenient for GPU-based renderers.

Surface Radiance

According to Zhang et al. [START_REF] Zhang | Effects of Winds on Ocean Color[END_REF]], the ocean surface radiance R contributing to a pixel can be modeled by

R ≃ W RF + RC + RW (2)
where W ∈ [0, 1] is the whitecap fractional coverage and RF , RC , and RW respectively denote the whitecap foam, clear (foam free), and water-leaving radiance. Because our ocean wave model is analytical, we can use the work of Bruneton et al. [START_REF] Bruneton | Realtime Realistic Ocean Lighting using Seamless Transitions from Geometry to BRDF[END_REF] to compute RC and RW . Similarly, we follow Premoze et al. [Premoze and Ashikhmin 2001] and set RF to a smooth Lambertian surface with a reflectance of 0.4, a reasonnable approximation in the visible spectrum range [START_REF] Koepke | Effective reflectance of oceanic whitecaps[END_REF]].

With these assumptions, the only parameter left to evaluate is W , which is addressed in the next section.

Whitecap Model

Discrete Generation

Most of the whitecaps appearing on the ocean surface are due to wave breaking [START_REF] Anguelova | Whitecap coverage from satellite measurements: A first step toward modeling the variability of oceanic whitecaps[END_REF]. We detect such events by evaluating the choppiness of the surface at each point p as suggested by Tessendorf [START_REF] Tessendorf | Simulating Ocean Water[END_REF]], which is inversely proportional to the Jacobian determinant of the horizontal transformations, denoted by j(p, t). We chose to compute the following function

b(p, t) = Υ (ǫ -j(p, t)) , ǫ ∈ R (3)
and generate whitecaps whenever b(p, t) = 1, where Υ is the Heaviside function and

j(p, t) = 1 + i λi ∂u i (p,t) ∂x i λi ∂u i (p,t) ∂y i λi ∂u i (p,t) ∂y 1 + i λi ∂v i (p,t) ∂y (4)
The variable ǫ controls the amount of breaking. Note that this scheme does not reproduce the geometric deformations produced by wave breaking, but may be used to model the changes of reflectance it causes on the surface.

Per Pixel Filtering

If we neglect the shadowing and masking produced by the waves, the whitecap fractional coverage W using our wave breaking model inside a pixel is given by

W = 1 A A b(p, t) dp (5)
where A bounds the footprint of the pixel on the ocean plane. This integral is clearly not suitable for real-time renderers as it is not linear, nor can it be solved analytically. Therefore, approximations have to be made in order to reduce its complexity.

For large footprints, it has been observed that wave slopes tend to be normally distributed on ocean surfaces [START_REF] Ross | Detailed analytical approach to the Gaussian surface bidirectional reflectance distribution function specular component applied to the sea surface[END_REF]]. Since our formulation of j directly builds on these features, we assume that it also follows a normal distribution. This allows to us to replace (5) by an integration over a probability distribution function, thus obtaining (dropping dependencies on p and t)

W ≈ +∞ -∞ Υ(ǫ -j) 1 2πσ 2 A exp - (j -µA) 2 2σ 2 A dj = 1 2 + 1 2 erf √ 2 2σA (ǫ -µA) (6)
where erf, µA and σ 2 A respectively denote the error function, the mean, and the variance of j in A. Now, W is an analytic expression whose parameters µA and σ 2

A can be evaluated using fast linear prefiltering methods [START_REF] Bruneton | A Survey of Non-linear Pre-filtering Methods for Efficient and Accurate Surface Shading[END_REF] such as the hardware accelerated mipmap generator available on modern GPUs.

Storage

Linear pre-filtering methods require the (linear) data to be stored in textures or arrays. Since the spatial period of q(p, t) can be very large, pre-filtering µA and σ 2

A in (6) may require a prohibitive amount of memory. We show however that these variables can be evaluated using much less memory by reformulating them as sums of contributions from each wave pattern.

Developping expression (4) for any number n ∈ N * + of patterns yields

j = n-1 i=0 { 1 n + ai + bi + aibi -c 2 i } + i =j {aibj -cicj} where ai = λi ∂u i ∂x , bi = λi ∂v i ∂y , ci = λi ∂u i ∂y .
Each term in the first sum only depends on one pattern and can easily be stored in a small linearly pre-filterable texture. The terms in the second sum involve products of uncorrelated functions, and thus their average is zero. Therefore we get

µA = 1 A i A ki dp , ki = 1 n + ai + bi + aibi -c 2 i (7)
Similarly, developping the square of (4) gives i k 2 i plus terms which involve products of uncorrelated functions, whose average is also zero, and thus we have

σ 2 A = -µ 2 A + 1 A i A k 2 i dp (8)
We implemented our method in C++ using OpenGL and GLSL, which runs in two main passes. The first pass evaluates the terms of equations (1) (4) as well as the ki and k 2 i factors from ( 7) and ( 8) and stores the results in 2D textures with mipmaps. Then, we render the projected grid as described in Section 1 in a vertex shader and evaluate equation (2) in a fragment shader. Since the terms of W are stored in textures, the GPU can automatically select the correct mip and anisotropy levels for any viewpoint. Results and performances are respectively shown in Figures 1 and2. Using four different patterns requires a total of eight distinct 2D RGBA textures for storage, which consumes up to 5.33 MB (accounting for the whole mip pyramid) of memory at half floating point precision. The complete source code is available on github at http://github.com/jdupuy/whitecaps

Conclusion and Future Work

We have presented a new model to explore ocean scenes from ground to space with whitecaps in real time. Our implementation runs entirely on the GPU and takes full advantage of available hardware features to integrate the optical effects occuring at the ocean surface.

A lot of directions can be taken for future work:

• First, our model only produces whitecaps whenever a wave breaks, but does not handle their decay which can last up to several seconds, also causing reflectance fluctuations [START_REF] Koepke | Effective reflectance of oceanic whitecaps[END_REF]].

• Second, equation ( 5) does not take masking effects into account, which is important at grazing angles. This could be solved by using the masking function of Ross et al. [START_REF] Ross | Detailed analytical approach to the Gaussian surface bidirectional reflectance distribution function specular component applied to the sea surface[END_REF], already used in our framework to evaluate the sun's reflected radiance in RC in equation (2).

• Lastly, the lambertian properties of the foam surface could be replaced by a richer shading model.

Figure 2 :

 2 Figure 2: Rendering times depending on the footprint of the camera. A footprint of 100km 2 corresponds to an altitude of 4.6km if the camera is pointing straight down. Frames are generated in less than 10ms at 1280 × 720 resolution on an NVIDIA GeForce 560Ti.

Acknowledgements

The authors thank Fabrice Neyret for his advice in the early stage of the project and Jean-Claude Iehl and Pierre Poulin for proofreading the article. This work was cunducted while both authors were at INRIA Grenoble Rhône-Alpes and was funded by the ANR 2010 JCJC 0207 01 "SimOne" project.


Luis Gonzalez-Mestres
email: luis.gonzalez-mestres@megatrend.edu.rsat

CMB B-modes, spinorial space-time and Pre-Big Bang (I)

The BICEP2 collaboration reports a B-mode polarization of the cosmic microwave background (CMB) radiation inconsistent with the null hypothesis at a significance of > 5 σ. This recent and potentially important result is being often interpreted as a signature of primordial gravitational waves from cosmic inflation. However, the arguments supporting such an interpretation are strictly based on standard cosmology and do not take into account possible new phenomena suggested by Planck data such as the existence of a privileged space direction. In particular, inflation is not needed in pre-Big Bang patterns, and the spinorial space-time (SST) introduced in our 1996-97 papers automatically generates a privileged space direction for each comoving observer. In the presence of this privileged space direction, the existence of CMB B-modes is a natural phenomenon and the signal claimed by BICEP2 would not correspond to any kind of inflationary scenario.

Introduction

BICEP2 data [START_REF] Gonzalez-Mestres | BICEP2 I: Detection Of B-mode Polarization at Degree Angular Scales[END_REF][START_REF]BICEP2 Collaboration, BICEP2 II: Experiment and Three-Year Data Set[END_REF] have given rise to speculations interpreting them as a strong direct evidence for cosmic inflation and primordial gravitational waves. The basic claim being that the detected B-modes of CMB cannot be generated primordially by density perturbations and that only gravitational waves originating from the inflationary expansion of the Universe can produce such a phenomenon.

However, this reasoning can apply only to cosmologies based on the standard Big Bang approach where inflation is required to get a potentially consistent description of the Universe. Pre-Big Bang models [START_REF] Gonzalez-Mestres | Pre-Big Bang, fundamental Physics and noncyclic cosmologies[END_REF][START_REF] Gonzalez-Mestres | Planck data, spinorial space-time and asymptotic Universe, mparc 13-33[END_REF] can easily escape these constraints and do not require any inflationary scenario. Furthermore, the spinorial space-time suggested in 1996-97 [START_REF] Gonzalez-Mestres | Physical and Cosmological Implications of a Possible Class of Particles Able to Travel Faster than Light[END_REF][START_REF] Gonzalez-Mestres | Space, Time and Superluminal Particles[END_REF] naturally generates [START_REF] Gonzalez-Mestres | Spinorial space-time and privileged space direction (I), mparc[END_REF][START_REF] Gonzalez-Mestres | Spinorial space-time and Friedmann-like equations (I), mparc[END_REF] a privileged space direction for each comoving observer. Then, the existence of CMB Bmodes appears as a natural consequence of this local anisotropy.

The existence of a privileged space direction for each comoving observer may have been confirmed by recent Planck [START_REF][END_REF] results [START_REF]Planck 2013 results. XXIII. Isotropy and statistics of the CMB[END_REF] after previous indications by WMAP [START_REF]Wilkinson Microwave Anisotropy Probe[END_REF]. Similarly, pre-Big Bang models can naturally solve the horizon problem [START_REF] Gonzalez-Mestres | Cosmological Implications of a Possible Class of Particles Able to Travel Faster than Light[END_REF] and provide reasonable alternatives to the inflationary explanation of the formation of conventional matter structure in our Universe.

In this short note, we remind and briefly discuss some basic elements of the obvious alternatives to the inflationary interpretation of BICEP2 results.

Pre-Big Bang

The pre-Big Bang scenarios considered here are not based on mere extrapolations from standard dynamics to higher energies and lower energy scales. We assume that really new physics is at work at distance and time scales smaller than the Planck scale, and that the standard principles of Physics (relativity, quantum mechanics...) cease to be valid at these scales [START_REF] Gonzalez-Mestres | Pre-Big Bang, vacuum and noncyclic cosmologies[END_REF][START_REF] Gonzalez-Mestres | Planck, cosmic rays and unconventional cosmologies, contribution to the Planck 2011 Conference[END_REF]. Then, new ultimate constituents of matter and a new space-time geometry can dominate this primordial phase of the history of the Universe.

If the new ultimate constituents of matter can travel at a speed much faster than light [START_REF] Gonzalez-Mestres | Cosmological Implications of a Possible Class of Particles Able to Travel Faster than Light[END_REF][START_REF] Gonzalez-Mestres | Vacuum Structure, Lorentz Symmetry and Superluminal Particles[END_REF], the very early Universe can naturally undergo a very fast expansion. Then, the horizon problem disappears and there is no longer any need for inflation. As standard matter will nucleate inside a pre-existing and quickly expanding universe with a pre-existing matter or pre-matter, fluctuations allowing for galaxy formation will be a natural phenomenon.

Contrary to the standard inflationary pattern, pre-Big Bang cosmologies do not need the Universe to be isotropic as seen by a comoving observer [START_REF] Gonzalez-Mestres | Spinorial space-time and privileged space direction (I), mparc[END_REF][START_REF] Gonzalez-Mestres | Spinorial space-time and Friedmann-like equations (I), mparc[END_REF]. The spinorial space-time provides an explicit example of a different scenario [START_REF] Gonzalez-Mestres | Pre-Big Bang, fundamental Physics and noncyclic cosmologies[END_REF][START_REF] Gonzalez-Mestres | Cosmic rays and tests of fundamental principles, CRIS 2010 Proceedings[END_REF]. Using a spinorial space-time appears as a natural choice, as the fermion wave functions do not correspond to representations of the real space rotation group SO(3) but of its covering group SU [START_REF]BICEP2 Collaboration, BICEP2 II: Experiment and Three-Year Data Set[END_REF]. Furthermore, Planck results suggest [START_REF]Planck 2013 results. XXIII. Isotropy and statistics of the CMB[END_REF] that cosmic space anisotropy can indeed be a real feature of our Universe.

The spinorial space-time

The properties of the spinorial space-time have been reminded and further studied in [START_REF] Gonzalez-Mestres | Pre-Big Bang, fundamental Physics and noncyclic cosmologies[END_REF][START_REF] Gonzalez-Mestres | Cosmic rays and tests of fundamental principles, CRIS 2010 Proceedings[END_REF] and in [START_REF] Gonzalez-Mestres | Spinorial space-time and privileged space direction (I), mparc[END_REF][START_REF] Gonzalez-Mestres | Spinorial space-time and Friedmann-like equations (I), mparc[END_REF]. For a SU(2) spinor ξ describing spacetime coordinates, a positive SU(2) scalar is | ξ | 2 = ξ † ξ (the dagger stands for hermitic conjugate). Then, a definition of the cosmic time (age of the Universe) can be t = | ξ | with an associated space given by the S 3 hypersphere

| ξ | = t. Other definitions of t in terms of | ξ | (f.i. t = | ξ | 2 )
lead to similar cosmological results as long as a single-valued function is used.

With the definition t = | ξ |, if ξ 0 is the observer position on the | ξ | = t 0 hypersphere, space translations inside this hypersphere correspond to SU(2) transformations acting on the spinor space, i.e. ξ = U ξ 0 where:

U = exp (i/2 t -1 0 σ. x) ≡ U ( x) (1)
σ being the vector formed by the usual Pauli matrices. The vector x is the spatial position of ξ with respect to ξ 0 at constant time t 0 . The cosmic time origin (beginning of the Universe) is naturally associated to the point ξ = 0. This leads to an expanding Universe where cosmological comoving frames correspond to straight lines crossing the origin ξ = 0.

The privileged space direction associated to the space-time point ξ is then defined by the linear combination of sigma matrices (with real coefficients) that leaves ξ invariant. The space-time points on the trajectory generated by this sigmalike matrix satisfy the relation ξ ′ = exp (iφ) ξ where φ is real and exp (iφ) is a complex phase factor. Such a definition of a space trajectory is stable under SU(2) transformations and comoving time evolution.

Then, contrary to the standard isotropic situation where only E-modes associated to gradients can be present in the CMB except for the B-modes due to inflationary gravitational waves, the spinorial space-time easily leads to B-modes naturally generated by rotations around the privileged space direction and vector products by this direction. This is just a conservative example of the potentialities of new space-time geometries in pre-Big Bang cosmologies.

Thus, inflation is no longer necessary to explain the CMB B-modes that BICEP2 has possibly observed. On the contrary, such a result may have provided a signature of SST geometry or of some other unconventional structure beyond the standard space-time.

More details on the spinorial space-time can be found in [START_REF] Gonzalez-Mestres | Pre-Big Bang, fundamental Physics and noncyclic cosmologies[END_REF][START_REF] Gonzalez-Mestres | Planck data, spinorial space-time and asymptotic Universe, mparc 13-33[END_REF] and in [START_REF] Gonzalez-Mestres | Pre-Big Bang, fundamental Physics and noncyclic cosmologies[END_REF][START_REF] Gonzalez-Mestres | Cosmic rays and tests of fundamental principles, CRIS 2010 Proceedings[END_REF].

Conclusion

There is no serious reason to consider the possible existence of CMB B-modes suggested by BI-CEP2 data as an evidence for cosmic inflation rather than as a natural signature of a pre-Big Bang era or, simply, of a space-time geometry (the spinorial space-time) best adapted than the conventional real space-time to the existence of fermions among the elementary particles of standard Physics.

Planck results suggest that nonstandard cosmological phenomena may be at work. If confirmed, the BICEP2 result can be the beginning of a new evidence for physics beyond the standard model and cosmology beyond the present standard pattern based on ΛCDM and inflation.

The possibility that in pre-Big Bang and SSTlike patterns the just nucleated standard mat-ter reacts (including gravitationally) to the preexisting fast expansion of the Universe has been explicitly considered in previous papers. See, for instance, the conclusion of [START_REF] Gonzalez-Mestres | Planck data, spinorial space-time and asymptotic Universe, mparc 13-33[END_REF].

Together with Planck, recent precise measurements may be providing evidence for new cosmology and a new fundamental space-time structure. A more detailed discussion of these important issues will be presented elsewhere.


Van Chan Ngo

Jean-Pierre Talpin

Thierry Gautier

Paul Le Guernic

Evaluating SDVG translation validation: from Signal to C

Keywords: Formal Verification, Translation Validation, Certified Compiler, Value-Graphs, Synchronous Programs

In this work, we describe how the preservation of value-equivalence of variables can be proved based on translation validation of synchronous data-flow value-graphs. It focuses on proving that every output variables in the original program and their counterparts in the transformed program, the generated C code, have the same values. The computation of each output variable and its counterpart is represented by a formal representation, a shared value-graph. This graph deterministically represents the computation of the output in the original program and its counterpart in the transformed program, and the nodes for the common variables have been shared in the graph. Given a SDVG, support that we want to show that the two output variables have the same value. We simply need to check that they are represented by graphs which are rooted at the same graph node. We manage to make the check by normalizing SDVGs by some rewrite rules.

Translation Validation d'évaluation de SDVG: de Signal vers C

Résumé : Dans ce travail, nous décrivons comment la préservation de la valeur d'équivalence de variables peut être prouvée sur la base de la translation validation de valeur-graphe synchrone.

Il se concentre sur ce qui prouve que toutes les variables de sortie dans le programme d'origine et leurs correspondants dans le programme transformé, le code C généré, ont les mêmes valeurs. Le calcul de chaque variable de sortie et son correspondant est représentée par une représentation formelle, un valeur-graphe partagé.

Ce graphique représente la facon déterministe le calcul de la sortie dans le programme d'origine et son équivalent dans le programme transformé, et les noeuds pour les variables communes ont été partagées dans le graphique. Étant donné un SDVG, soutenons que nous voulons montrer que les deux variables de sortie ont la même valeur. Nous avons simplement besoin de vérifier qu'ils sont représentés par des graphiques qui sont enracinées dans le même noeud du graphe. Nous parvenons à faire le chèque en normalisant SDVGs par des règles de réécriture.

Mots-clés : Formal Verification, Translation Validation, Certified Compiler, Value-Graphs, Synchronous Programs

Introduction

At a high level, our tool works as follows. For a transformation, it takes the input program and its transformed counterpart, constructs the corresponding SDVG for each output variable. Then it checks that for every output variable in input program and its counterpart in transformed program, they have the same value. If the result says that there exists any non-equivalence then the compiler emits compilation error. Otherwise, the compiler continues its work. The integration of this verification process into the compilation process can be depicted as in Figure 1. We believe that our validator must have the following features to be effective. First, we do not modify or instrument the compiler, and we treat the compiler as a "black box", hence our validator is not affected from the future update or modification of the compiler. Our approach is to apply the verification to the compiler transformations themselves in order to automatically generate formal evidence that the clock semantics of the source program is preserved during program transformations, as per applicable qualification standard. Second, it is important that the validator can be scaled to large programs, in which we represent the desired program semantics with our scalable abstraction and use efficient graph libraries to achieve the expected goals: traceability and formal evidence.

*
The remainder of this chapter is organized as follows. Section 3 describes how code can be generated, as the final step of the compilation process, following different schemes. Section 4 illustrates the concept of SDVG and the verification procedure. In Section 5, we consider the formal definition of SDVG and the representation of Signal program and generated C code as SDVGs. Section 6 addresses the mechanism of the verification process based on the rewrite rules and the normalization of a SDVG methods, the application of the verification process to the Signal compiler, and its integration in the Polychrony toolset [START_REF]Polychrony toolset[END_REF]. Section 7 presents some related works, concludes our work and outlines future directions.

The Signal language

Language features

Signal [START_REF] Benveniste | Hybrid dynamical systems theory and the signal language[END_REF][START_REF] Gautier | Signal, a declarative language for synchronous programming of real-time systems[END_REF] is a polychronous data-flow language that allows the specification of multi-clocked systems. Signal handles unbounded sequences of typed values (x(t)) t∈N , called signals, denoted as x. Each signal is implicitly indexed by a logical clock indicating the set of instants at which the signal is present, noted C x . At a given instant, a signal may be present where it holds a value, or absent where it holds no value (denoted by #). Given two signals, they are synchronous if and only if they have the same clock. In Signal, a process (written P or Q) consists of the synchronous composition (noted |) of equations over signals x, y, z, written x := y op z or x := op(y, z), where op is an operator. A program is a process.

Data domains

Data types consist of usual scalar types (Boolean, integer, float, complex, and character), enumerated types, array types, tuple types, and the special type event, subtype of the Boolean type which has only one value, true.

Operators

The core language consists of two kinds of "statements" defined by the following primitive operators: first four operators on signals and last two operators on processes. The operators on signals define basic processes (with implicit clock relations) while the operators on processes are used to construct complex processes with the parallel composition operator:

• Stepwise functions: y := f (x 1 , ..., x n ), where f is a n-ary function on values, defines the extended stream function over synchronous signals as a basic process whose output y is synchronous with x 1 , ..., x n and ∀t ∈ C y , y(t) = f (x 1 (t), ..., x n (t)). The implicit clock relation is C y = C x1 = ... = C xn .

• Delay: y := x$1 init a defines a basic process such that y and x are synchronous, y(0) = a, and ∀t ∈ C y ∧ t > 0, y(t) = x(t -1). The implicit clock is C y = C x .

• Merge: y := x default z defines a basic process which specifies that y is present if and only if x or z is present, and that y(t) = x(t) if t ∈ C x and y(t • Composition: If P 1 and P 2 are processes, then P 1 | P 2 , also denoted (|P 1 | P 2 |), is the process resulting of their parallel composition. This process consists of the composition of the systems of equations. The composition operator is commutative, associative, and idempotent.

) = z(t) if t ∈ C z \ C x .
• Restriction: P where x, where P is a process and x is a signal, specifies a process by considering x as local variable to P (i.e., x is not accessible from outside P ).

Clock relations

In addition, the language allows clock constraints to be defined explicitly by some derived operators that can be replaced by primitive operators above. For instance, to define the clock of a signal (represented as an event type signal), y := ˆx specifies that y is the clock of x; it is equivalent to y := (x = x) in the core language. The synchronization xˆ= y means that x and y have the same clock, it can be replaced byˆx =ˆy. The clock extraction from a Boolean signal is denoted by a unary when: when b, that is a shortcut for b when b. The clock union xˆ+ y defines Inria a clock as the union C x ∪ C y , which can be rewritten asˆx defaultˆy. In the same way, the clock intersection xˆ * y and the clock difference xˆ-y define clocks C x ∩ C y and C x \ C y , which can be rewritten as ˆx whenˆy and when (not(ˆy) default ˆx), respectively.

Example

The following Signal program emits a sequence of values F B, F B -1, ..., 2, 1, from each value of a positive integer signal F B coming from its environment: • Line (4): F B is accepted (or it is present) only when ZN becomes less than or equal to 1.

1 process DEC = 2
• Line [START_REF] Maffeï | Distributed implementation of signal: Scheduling and graph clustering[END_REF]: N is set to F B when its previous value is less than or equal to 1, otherwise it is decremented by 1.

• Line (6): defines ZN as always carrying the previous value of N (the initial value of ZN is 1).

• Line [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF]: indicates that ZN is a local signal whose initial value is 1.

Note that the clock of the output signal is more frequent than that of the input. This is illustrated in the following possible trace:

1 t . . . . . . . . . . 2 FB 6 # # # # # 3 # # 2 3 ZN 1 6 5 4 3 2 1 3 2 1 4 N 6 5 4 3 2 1 3 2 1 2
5 CFB t0 t6 t9 6 CZN t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 7 CN t0 t1 t2 t3 t4 t5 t6 t7 t8 t9

Program structure

The language is modular. In particular, a process can be used as a basic pattern, by means of an interface that describes its parameters and its input and output signals. Moreover, a process can use other subprocesses, or even external parameter processes that are only known by their interfaces. For example, to emit three sequences of values (F B i ) -1, ..., 2, 1 for all three positive integer inputs F B i , with i = 1, 2, 3, one can define the following process (in which, without additional synchronizations, the three subprocesses have unrelated clocks):

Code generation in Signal compiler

Code generation is the final step in the compilation process of Signal compiler as depicted in Figure 2. When a program P consists of no deadlocks, free of clock constraints one could generate code for P following the Kahn semantics with the code generation functionalities of Polychrony toolset. The code is generated for different general purpose languages (C, C++, Java) on different architectures. The generated code in this case is called reactive code. However, one can generate the defensive code when the program consists of some clock constraints, in this mode, all alarms are emitted when a contraint is violated during the simulation.

The principle

The principle of code generation [START_REF] Besnard | Compilation of polychronous data-flow equations[END_REF] is based on the use of the clock hierarchy resulting from the clock calculation and the graph of conditional dependencies not only to schedule the instructions in sequences, but also the schedule component activation in a hierarchical target code. The code generation follows the general scheme that is depicted in Figure 2. The generated code contains a main program which controls the step block. The step block consists of a step scheduler that drives the execution of its step component and updates the state variables corresponding to delay operators and local variables. The execution of the step block is scheduled by the step scheduler. The step component can be hierarchical which consists of a set of sub-components called clusters and has its own local step scheduler. The step block communicates with its environment through the IO container.

I/O Container

State Variables

Step Component (Hierarchical)

Step Scheduler In general, the generated program will have many files. We consider the target language code is C. For a process P , a main program is defined in the file P _main.c, the program which contains the step block called body program is defined in the file P _body.c, and an input-output program which contains the IO container is defined in the file P _io.c. Each component of the generated code can be seen as a Signal process. Then they can be reused in an embedding Signal process.

Inria

The main program

The pseudo-code in Listing 1 shows the structure of the main program. The main program opens the IO communication channels with the program environment, and calls the initialization function. If everything goes fine then it calls the step function repeatedly in the infinite loop to interact with the environment. The infinite loop can be stopped if the step function returns a error code 0, meanings that the input stream is empty, and the main program will close the communication channels. All the called functions are defined in the body program.

Listing 1 : Structure of P_main.c

The step block

Once the IO communication channels and the initialization are completed, the step function P _step() is responsible for the calculation of the effect of one synchronous step of the system to interact with the environment, is the essential part of the concrete code. It reads data from the input streams, computes the outputs and writes the results to the output streams. In Polychrony toolset, the implementation of the step function can be done in many schemes based on the clock hierarchy and the graph of conditional dependencies which are produced in the previous compilation phases by the compiler front-end. These code generation schemes consist of:

• Global code generation: sequential code, clustered code with static scheduling, clustered code with dynamic scheduling.

• Modular code generation.

• Distributed code generation.

The next section will describe the sequential, inlining code generation of the step block. For other code generation schemes, interested readers can refer to [START_REF] Maffeï | Distributed implementation of signal: Scheduling and graph clustering[END_REF][START_REF] Gautier | Code generation in the sacres project[END_REF][START_REF] Aubry | Synchronous distribution of signal programs[END_REF].

The IO container

The IO container implements the communication of the generated program with the environment in case the being compiled process contains input and output signals. In the simulation mode, each input or output signal communicates with the environment via a file as the input stream or output stream. The IO container in Listing 2 consists of global functions for opening, closing all files, and for reading and writing data for each input and output signal.

Sequential code generation

In the context of this work, we will consider the sequential, inlining code generation scheme for the step function that directly interprets the Signal process obtained after the clock calculation, boolean abstraction, and scheduling phases of the compiler front-end. We describe the code structure of the step function for a simple process in Listing 3. The step function obtained by compiling it is given in Listing 4. The C code introduces an explicit variable for each signal to represent the clock. Variable C_N is the clock of N and C_F B1, C_F B2 are the clocks of F B1 and F B2, respectively. As soon as the clock is evaluated and is true, the signal is read if it is an input signal or updated, otherwise. The state variables (corresponding to the delays) are updated at the end of the step block in the step finalization. The precedence of the statements must be consistent with the graph of conditional dependencies, and one can observe that the tree structure of conditional if-then-else statements which expresse directly the clock hierarchy.

The step function works as follows. It reads the clock values of F B1 and F B2. If C_F B2, the clock of F B2, has the value true, a new value for F B2 is read and used to compute the clock of N . In the similar way, if C_F B1 has the value true, a new value for F B1 is read. If C_N , the clock of N , has the value true, N gets the value 4 * F B1. The updated value of N is also output.

A computation of this program is given below. At the initialization, the variables can have arbitrary values which are denoted by * .

Taking into account that N in C code is the value of the corresponding signal in Signal program, we have an observation that the value of N is remained when C_N , the clock of N , has the value false. Intuitively, based on this observation, we can say that if a variable in the generated C program whose value is never updated then it will be assigned no value, denoted as #. In the next sections, we will show how this assumption can be formalized to represent the computation of step function as a shared value-graph. In this example, we use the concept of gated φ-function such as x = φ(c, x 1 , x 2 ) which is mentioned more details in the next sections. It is used to represent the branching in program, which means x takes the value of x 1 if the condition c is satisfied, and the value of x 2 , otherwise. Since the generated C programs use persistent variables (i.e. variables that always have some values), while Signal programs which use volatile variables, we will assume that if a variable (including the input and output variables) in the generated C program whose value is never updated then it will be assigned the absent value, denoted as #. And if a statement involves a variable x before its value update then the value of this variable is the previous value, denoted as m.x.

Considering the equation N := 4 * F B1 when (F B2 >= 3), at a considered instant t, signal N is present if signal F B1, F B2 are present and F B2 is greater than or equal to 3. When N is present, its value is defined by the value of F B1 multiplied by 4. The value of N is # when it is absent. The computation of this equation can be replaced by the following gated φ-function:

N = φ( N , N , #)
where N ⇔ ( F B1 ∧ F B2 ∧ (F B2 >= 3)), N = 4 * F B1. Here, N , F B1, F B2 are boolean variables that represent the states (false: absent, true: present) of signals N, F B1 and F B2 at instant t, respectively. And N , F B1, F B2 are values of signals N, F B1 and F B2 with the same types. Then, this gated φ-function indicates that at any instant t such that signals F B1 and F B2 are present and the value of F B2 is greater than or equal to 3, then the value of N is equal to the value of F B1 multiplied by 4, otherwise the value of N is #.

In the same way, we use a gated φ-function to represent the branching in C code. For instance, if C_N is true then the value of variable N is defined by the value of F B1 multiplied by 4. Otherwise, the value of N is never updated. This computation can be replaced by the following gated φ-function:

N = φ(C_N, 4 * F B1, #)
We replace the variables C_CLK_36 and C_N by their definition, we obtain the synchronous data-flow value-graph for the output N that is presented in Figure 3. Notice that the compiler prefers to write C_CLK_36 = (C_F B2?(F B2 >= 3) : F ALSE) instead of C_CLK_36 = C_F B2&&(F B2 >= 3), which can be represented by the following gated φ-function:

C_CLK_36 = φ(C_F B2, F B2 >= 3, f alse)
The dashed arrows are not parts of the graph, they only mean that for each node, there is a set of labels that indicates which nodes of the graph correspond to which signals, clocks or variables in the programs. The Signal program and its generated C program have been represented in the same graph, in which the nodes are labelled by the same structures (clocks, signals, variables and function symbols) have been reused. And the unique occurrence of a reused node is said to be shared. For example, the nodes labelled >= and # are shared in the graph.

Here, the values of input signals and their corresponding variables in the generated C code are represented by the same nodes in the shared graph. In general, it is safe to assume that the values of input signals and the corresponding variables in the generated C code are equal. Thus, in the shared graph, the input signal values F B1, F B2 and the variables F B1, F B2 in the C code are represented by the same nodes.

Suppose that we want to verify that the signal N in the WHENOP and WHENOP_step (denoted by N c ) will have the same computation. This can be done by showing that they are represented by the subgraphs which are rooted at the same node. In Figure 3, we cannot conclude that they are equivalent, however we can transform the value-graph by applying normalization rules. First, by exploiting the generated program, C_F B1, C_F B2 are clocks of F B1 and F B2, respectively. Because the values of inputs F B1, F B2 are updated only when C_F B1, C_F B2 are valid. The first rule, we will apply is that:

"If x is

an input and the clock of x is read as input parameter (it is not defined in the program)

then its clocks in Signal program and C code are represented by the same node".

Thus, they are represented by the same nodes C_F B1 and C_F B2 in Figure 4. Until now, the subgraphs represent the variable N in the two programs which are not rooted at the same node. We will apply the following second rewrite rule to the resulting graph, we will replace φ(C_F B2, F B2 >= 3, false) with C_F B2 ∧ F B2 φ(c, x, f alse) is replaced by (c ∧ x) for any boolean expression x. We will go into details about the rules in the next section. After this replacement, and maximizing the variable sharing, the variable N in two programs points to the same node in the resulting graph in Figure 5. Therefore, we can conclude that the outputs are equivalent.

Inria {N } {N c } F B2 3 C_F B2 >= f alse C_F B1 φ 4 F B1 ∧ * # φ φ ∧ ∧ F B1 F B2
N N c F B2 3 C_F B2 >= f alse C_F B1 φ 4 F B1 ∧ * # φ φ ∧ ∧

Synchronous data-flow value-graph

In this section, we describe the computation of signal in a Signal program and the corresponding variable in the generated C code in terms of SDVGs. Let us recall the computation of the output signal y in the equation y := x when b in the previous section. At any instant, the signal y holds the value of x if the following conditions are satisfied: Otherwise, it holds no value. Thus, at a given instant, to represent the underlying control conditions and the computation of this equation, we can use the following gated φ-function:

N N c F B2 3 C_F B2 >= C_F B1 ∧ 4 F B1 ∧ * # φ φ
y = φ(x ∧ b ∧ b, x, #)
The condition (x ∧ b ∧ b) represents the state in which x holds a value (x = true), and b holds the value true ( b = true ∧ b = true). This section explores a method to construct that shared value-graph for both Signal and generated C code programs, which is the computational model of our translation validation approach.

Definition of SDVG

Graphs can be used to describe many structures in computer science: program control flows, communication processes, computer networks, pointer structure on the heap and many others. In fact, for most activities in the software development, many types of visual notations have been introduced, including UML, state diagrams, control flows graphs, block diagrams. These notations construct a models that can be seen as graphs. This section intends to focus on graphs which represent expressions for computing the variable values in programs. We presents basic definitions, including the notion of gated φ-function, and introduces a linear syntax presentation for terms represented as graphs. Finally, we provide the definition of our considered type of graph, synchronous data-flow value-graph. The interested readers can refer to [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF] for more detailed discussion on term graphs and linear syntax presentation for graphs.

Gated φ-function

In Static Single Assignment (SSA), a φ-node is placed at the confluence of a program control flow to represent the different choices of a variable. However, it does not contain the condition to determine which a incoming branch reaches a confluence node is chosen. By contrast, gating functions are defined with some extra parameters to represent the conditions for choosing. To construct a SDVG, we will employ the notation of gating function to capture the branching Inria statements in computation of signals in synchronous data-flow programs and variables in the generated C code.

Gating functions were first introduced by Ballance et al. in [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demand driven interpretation of imperative languages[END_REF] to represent the conditions that guard the paths to a φ-node. There are several types of gating functions as follows:

• The gated φ-function, which is an if -then -else representation. It captures the condition for choosing which branch of the confluence node. For instance, x 3 = φ(c, x 1 , x 2 ) returns the value x 1 or x 2 depending on the value of c. If c is true,

x 3 = x 1 and x 3 = x 2 if c is false.
• The µ function is used to capture the initial and loop-carried values at the header of a loop. For instance, x 2 = µ(i = 1, n, x 0 , x 1 ) represent that x 2 's initial value is x 0 when i is the first iteration and its subsequent value is x 2 from the previous iteration.

• The η function is placed at the loop exit. It selects the last value at the end of the loop. For instance, x 2 = η(i > n, x 1 ) means that x 2 takes the last value of x computed by the loop.

Terms as trees and graphs

Let X and F be an infinite set of variables and a (finite or infinite) set of function symbols such that X ∩ F = ∅. Each f ∈ F has a number of arguments (or arity) greater or equal to 0, denoted by f (x 1 , x 2 , ..., x n ), where n is the arity of f . Function symbols of arity 0 are called constants.

Then the set of terms T is inductively defined by the following rules:

• Any variable is a term.

• Any expression f (t 1 , t 2 , ..., t n ), where f ∈ F and t 1 , ..., t n ∈ T , is a term.

Given a term t, the substerms of t is t and, if t = f (t 1 , ..., t n ), all subterms of t 1 , ..., t n . For example, let X = {x, y} and F = {f, g}, then T = {x, y, f (x), g(y), f (x, y)...}. Note that we do not assume that function symbols have fixed arities.

Definition A directed graph over X and F is a tuple N, succ involving a (finite or infinite) set N of nodes which can be labelled by an element in X ∪ F and a function succ : N -→ N * .

In which the set of nodes n 1 , ..., n k = succ(n) is the successors of n.

We write succ(n) i to denote the i th element of succ(n). The pair of nodes e = (n, succ(n) i ) is called an edge, the set of all edges is denoted by E. When we draw the visual representation of graphs, a directed edge e will go from n to succ(n) i , the ordering of the edges from n to succ(n) is left-to-right corresponding to the ordering of the elements of succ(n).

For example, let X = {a, b, c}, F = {+, * } be the set of variables and the set of function symbols, respectively. The set of nodes and the function succ is defined as follows:

N = {+, * , a, b, c} succ(+) = (a, * ), succ( * ) = (b, c), succ(a) = (), succ(b) = (), succ(c) = ()
This defines a directed graph which is depicted on the left of Figure 6. Other directed graphs over F and X are depicted on the right side of the figure. Note that the in the third graph, the nodes with repeated label b are represented by a same node, and the label is shared in the graph.

Given a directed graph G = N, succ , a path in G is a list of nodes (n 0 , n 1 , ..., n k ) where k ≥ 0 and n i+1 is a successor of n i . This path is said to be from n 0 to n k and k is the length of the path. A path of length greater than 0 from a node to itself is called a cycle, and the repeated node is called cyclic node. A graph which contains a cycle is cyclic graph, otherwise it is acyclic. In a term graph, a path from the root is said to be rooted. The term graph is root-cyclic if there is a cycle containing the root. Given a directed graph G = N, succ , let n is a node in G. The subgraph of G rooted at n is the term graph N ′ , succ ′ , n where N ′ = {n ′ ∈ N | there is a path from n to n ′ } and succ ′ is the restriction of succ to N ′ . We write G \ n to denote the fact that G \ n is the subgraph rooted at n of G.

Consider, for example, the following directed graph which is depicted on the left of Figure 7. The subgraph rooted at the node labelled + is depicted as the seconde graphs in the figure. The third graph is a root-cyclic graph. We will use the similar notations as in the definition of term to introduce a linear notation for graphs. The notation is defined by the following context-free grammar:

graph := node | node + graph node := x | f (node, ..., node) | nid | nid : x | nid : f (node, ..., node)
f and x are a symbol function in F and a variable in X. nid ranges over a set, disjoint from X and F , of node identifiers. Any node identifier nid in a graph which identifies a node must occur exactly once in the context nid : x or nid : f (node, ..., node. The constants are simply represented by symbol functions with arities equal 0. This syntax is similar to the syntax for graphs in [START_REF] Barendregt | Towards an intermediate language based on graph rewriting[END_REF]. For instance, the three graphs of the examples in Figure 6 can be expressed in this syntax as follows:

+(a, * (b, c)), +(a, b) + * (b, c) and + (a, nid 1 : b) + * (nid 1 , c)
Note that multiple uses of the same node identifier mean that the multiple references to the same node.

Definition A tree is a term graph at the node r such that there is exactly one path from r to each node in the graph.

Based on the above definition, in Figure 7 the first and second graphs are trees and the third one is not. Thus it is obvious that a tree is always acyclic.

Homomorphisms of graphs and trees

Let G 1 = N 1 , succ 1 , r 1 and G 2 = N 2 , succ 2 , r 2 be two graphs, the definition of homomorphism is given as follows:

Definition A homomorphism from G 1 to G 2 is a map f : N 1 -→ N 2 such that for all n ∈ N 1 ,
• f (n) and n have the same label

• succ 2 (f (n)) = f (succ 1 (n))
where f (n 1 , ..., n k ) = (f (n 1 ), ..., f (n k )). This definition states that homomorphisms preserve node labels, successors and their order. We write G 1 -→ G 2 to denote the fact that there is a homomorphism from G 1 to G 2 . Figure 8 shows an example of a homomorphism. • A homomorphism f from G 1 to G 2 is rooted if f (r 1 ) and r 2 have same label.

• An isomorphism is a homomorphism which is inverse. We denote an isomorphism from

G 1 to G 2 by G 1 ∼ G 2 .
• When there is a rooted isomorphism from G 1 to G 2 , we say that they are equivalent, denoted by G 1 ≈ G 2 .

Proposition 5.1 For any graphs G 1 and G 2 , we have

G 1 ≈ G 2 implies G 1 ∼ G 2 .
Every rooted homomorphism from one tree to another is an isomorphism.

Synchronous data-flow value-graph

Let X be the set of all variables which are used to denote the signals, clocks and variables in a Signal program and its generated C program. In our consideration, the functions which apply on signal values in the primitive stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=) and numerical operators (+, -, *, /). A constant is defined as a function symbol of arity 0. Thus in this chapter, we consider the set of function symbols which consists of the above functions and the gated φ-function, denoted by F . As it is illustrated in Section 4, the computation of signals in a Signal program and variables in the corresponding generated C code can be represented as a directed graph, in which a node can have multiple parents, and identical subgraphs are reused. That makes the maximal sharing among graph nodes. We will consider the definition and examine some basic properties of SDVG. Formally, a SDVG is defined as follows:

Definition A SDVG associated with a Signal program and its generated C code is a directed graph G = N, E, I, O, m N , where:

• N is a finite set of nodes. Each node is labelled by an element in X ∪ F . A node represents a clock, a signal, a variable, an operator or a gated φ-node function. And the subgraph rooted at a node is used to describe the computation of a value of the corresponding element labelled at the node. In the rest of this chapter, we denote the fact that there exists edge between two nodes x and y by x -→ y. A path from x to y is any set of nodes s = {x 0 , x 1 , ..., x k } such that ∀i = 0, .., k -1, x i -→ x i+1 . An edge is a special case when k = 1.

• E ⊆ N × N

SDVG of Signal programs

Let P be a Signal program, we write X = {x 1 , ..., x n } to denote the set of all signals in program P which consists of input, output, state (corresponding to delay operator) and local signals, denoted by I, O, S and L, respectively. For each x i ∈ X, we use D xi to denote its domain of values, and D # xi = D xi ∪{#} to denote its domain of values with the absent value, where # ∈ D xi . Then, the domain of values of X with absent value is defined as follows:

D # X = n i=1 D xi ∪ {#}
With each signal x i (boolean or non-boolean type), we attach a boolean variable x i to encode its clock at a given instant (true: x i is present, false: x i is absent), and x i with the same type as x i to encode its value. Formally, the abstract values to represent the abstract clock and value of a signal can be represented by a gated φ-function, x i = φ( x i , x i , #), where x i and x i are computed using the following functions:

ˆ: X -→ B associates a signal with a boolean value, ¯: X -→ D X associates a signal with a value of same type as the signal.

Assume that we have the computation of signals in processes P 1 , P 2 is represented as shared value-graphs G 1 and G 2 , respectively. Then the value-graph G of the synchronous combination Inria P 1 |P 2 can be defined as G = V, E, I, O, m N in which for any node x, we replace it by the subgraph that represents the definition of x, in G 1 , G 2 . And in G 1 and G 2 , every identical subgraph is reused, in other word, we maximize sharing among graph nodes in G 1 and G 2 . Thus, the shared value-graph of a Signal program P can be constructed as a combination of the sub-value-graphs of its equations as above.

To demonstrate the above combination rule, we consider a simple Signal program P as follows: Suppose that we have the subgraphs that represent the equations y := x * x1 and x1 := x + 1 as depicted in Figure 9 (here, we omit to represent the abstract clocks of x and x1 at the node ŷ, x1 at the node +). We replace the node x1 by the subgraph which defines it while reusing the identical node x. As a result, the shared synchronous data-flow value-graph of P is depicted in Figure 10. The Signal program is built through the set of primitive operators. Therefore, it is obvious that to construct SDVGs of Signal programs, we will construct a subgraph for each primitive operator. In the following, we present the value-graph corresponding to each Signal primitive operator.

Stepwise functions

In our consideration, the functions which apply on signal values in the primitive stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=) and numerical operators (+, -, *, /).

Consider the operator y := f (x 1 , ..., x n ), it indicates that if all signal from x 1 to x n are defined, then the output signal y is defined by the result of the function f on the values of x 1 , ..., x n . Otherwise, it is assigned no value. Thus, the computation of y can be represented by the following gated φ-function:

y = φ(ŷ, f (x 1 , x 2 , ..., x n ), #) where ŷ ⇔ x 1 ⇔ x 2 ⇔ ... ⇔ x n
The synchronous data-flow value-graph of the stepwise functions is depicted in Figure 11. Note that in the graph, { x 1 , ..., x n } ŷ means that the clocks x 1 , ..., x n and ŷ are equivalent meaning that they point to the same node in the graph. It can be represented by the gated φ-function, y = φ(ŷ, x 1 ∧ c, #), where we replace (x >= 1) by the fresh signal x 1 . Thus the graphic representation is depicted in Figure 12.

Delay

Consider the basic process which corresponds to the delay operator y := x$1 init a. The output signal y is defined by the last value of the signal x when the signal x is present. Otherwise, it is assigned no value. Thus, the computation of y can be represented by the following nodes: Thus the graphic representation is depicted in Figure 14.

Merge

Consider the basic process which corresponds to the merge operator y := x default z. If the signal x is defined then the signal y is defined and holds the value of x. The signal y is assigned the value of z when the signal x is not defined and the signal z is defined. When both x and z are not defined, y holds no value. The computation of y can be represented by the following node: y = φ(ŷ, φ(x, x, z), #)

where ŷ ⇔ (x ∨ ẑ)
The representation uses a nested φ-function which indicates that when ŷ is true, y is defined by the gated φ-function φ(x, x, z). Otherwise, it holds no value. The synchronous data-flow For instance, consider the following Signal equation:

y := x default (z + 1)
It can be represented by the nested φ-function, y = φ(ŷ, φ(x, x, z 1 ), #), where we replace (z + 1) by the fresh signal z 1 . Thus the graphic representation is depicted in Figure 16. It can be represented by the gated φ-function, y = φ(ŷ, x, #), where ŷ ⇔ (x ∧ z 1 ∧ z 1 ) and we replace (z >= 1) by the fresh signal z 1 . Thus the graphic representation is depicted in Figure 18.

Sampling

Restriction

The shared synchronous data-flow value-graph of restriction process P 1 where x is the same as the graph of P 1 .

Clock relations

Given the above graph representations of the primitive operators, we can obtain the shared value-graphs for derived operators on clocks as depicted in Figure 19 and The clock relations between signals are given as follows:

z :=ˆx : ẑ ⇔ x xˆ= y : x ⇔ ŷ z := xˆ+ y : ẑ ⇔ (x ∨ ŷ) z := xˆ * y : ẑ ⇔ (x ∧ ŷ) z := xˆ-y : ẑ ⇔ (x ∧ ¬ŷ) z := when b : ẑ ⇔ ( b ∧ b) {ẑ} x {z} true # φ {x} ŷ {ẑ} ∨ {z} true # φ x ŷ (1) (2)
(3) The scheduling and the computations is done inside the step function of the generated C program. Therefore, it is natural to construct the sub value-graph of this function in order to prove that the values of its variables and their corresponding signals are the same. To construct the value-graph of the step function, we need to consider the following considerations. An original signal named x has a boolean variable named C_x in the step function. Then the computation of x is implemented by conditional if -then -else statements as follows:

1 if ( C_x ) 2 { 3 computation ( x ) ; 4 }
If x is an input signal then its computation is the reading operation which gets the value of x from the environment. In case x is a output signal, after computing its value, it will be written to the IO communication channel with the environment. Note that the C programs use persistent variables (e.g. variables which are always have some values) to implement the input Signal programs which use volatile variables. As a result, there is a difference in the types of a signal in Signal program and the corresponding variable in C program. When a signal has absent value, #, at a given instant, the corresponding C variable is remained and can never have absent value. For instance, in the step function WHENOP_step(), we have an observation that the value of variable N is remained when the boolean variable C_N has the value false as the following code segment:

1 if ( C_N ) 2 { 3 N = 4 * FB1 ; 4 w_WHENOP_N ( N ) ; 5 }
This consideration implies that we have to detect whenever a variable in the C program whose value is never updated. It will be assigned the absent value, #. Thus, the computation of such variables x c , recall that we use the superscript for the C program variables, to distinguish them from the signals in the Signal program, in the step function can fully be represented by a gated φ-function as follows:

x c = φ(C_x c , x c , #)
where x c denotes the newly updated value of the variable. For example, we consider the generated code of basic process corresponding to the primitive operator merge in the following listing.

Listing 6 : SDVGMerge in Signal The computation of N and C_z can be represented by the sub value-graphs in Figure 22, where m.N c denotes the previous value of the variable N . Consider the following code segment. The observation is that the variable x is involved in the computation of the variable y before the updating of x.

Inria C_cx c cx c C_cy c cy c φ φ {cx_50 c } ∧ {cy_56 c } ∧ x c y c {C_z c } ∨ {x c } φ {z c } φ {y c } φ # {z c } φ
C_F B c F B c - m.N c 1 {N c , N c } φ cx_50 c cy_56 c {C_z c , C_z c } ∨
1 if ( C_y ) 2 { 3 y = x + 1; 4 } 5 ... 6 if ( C_x ) 7 { 8
x = ... 9 } 10 ...

Inria

In this situation, we refer to the value of x as the previous value, denoted by m.x c . It can be happened when the delay operator is applied on the signal x in the Signal program. The computation of y is represented by the following gated φ-function:

y c = φ(C_y c , m.x c + 1, #)

SDVG translation validation

In order to apply the translation validation to the code generation phase of the Signal compiler, we represent the computations of signals in the intermediate representation form written in Signal language and the computations of corresponding variables in the sequential generated code, written in C language by means of synchronous data-flow value-graphs.

Then we introduce the set of rewrite rules to transform the shared value-graph resulted in the previous step. This procedure is called normalizing. At the end of the normalizing procedure, we check that for any signal x and its corresponding variable x c in the generated C code, if it is an output signal then x and x c point to the same node in the shared value-graph. That means they are represented by the same subgraph. In other words, they have the same value. We also provide a method to implement the representation of synchronous data-flow value-graph and adapt the normalizing procedure with any feature optimization of the compiler.

We introduce the graph rewriting techniques in Section 6.1. Section 6.2 provides the set of rewrite rules which is used to perform the normalizing procedure on the shared value-graph. In Section 6.3, we consider a method to implement the data structure of synchronous data-flow value-graph and the normalizing procedure.

An introduction to graph rewriting

Graphs provide a simple and powerful approach to a variety of problems of software engineering, and system modeling in particular. These graphs are mostly static descriptions of system states. Adding dynamics requires some ways to express state changes and thus graph transformations are involved, either explicitly or behind the scenes. In fact, the theory of graph transformation has found many applications in the implementing functional languages based on term rewriting [START_REF] Turner | A new implementation technique for applicative languages[END_REF], in modeling of concurrent systems [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF] and in other areas such as software engineering, hardware designs and visual languages.

First we recall the basic concepts of term rewriting, and we explain informally how the term rewriting work in a simple example. We then define our notion of graph rewriting. For a comprehensive introduction of term rewriting and graph rewriting, the interested reader may consult the textbook [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF]. Consider, for example, the following rewrite rules for defining for natural number multiplication:

x * 0 -→ 0 x * (y + 1) -→ (x * y) + x
We will apply the second rewrite rule to the expression t * (u+1), where t and u are subexpressions, which is represented by the graph on the left of Figure 23. When applying the above rewrite rule, the subexpression t is evaluated two times if it has not been yet evaluated as depicted on the right of the figure. To solve this problem, an easy solution is, instead of copying the subexpression t, to create two references to the existing subexpression t, meaning that the repeated subterms are shared. Then the result of applying the above rewrite rule looks as the graphs in Figure 24. Let X and F be the set of variables and function symbols such that X ∩ F = ∅. We denote the set of all terms over X and F by T X,F . A mapping σ :

T X,F -→ T X,F is called a substitution if σ(c) = c and σ(f (t 1 , ..., t n ) = t(σ(t 1 ), ..., σ(t n )) for every constant c and term f (t 1 , ..., t n ).
Definition A term rewrite rule over T X,F is a pair of terms (t l , t r ), written as t l → t r , such that:

• t l is not a variable, and

• ∀x ∈ X.(x ∈ t r ⇒ x ∈ t l ).
We call t l and t r are, respectively, the left and right-hand sides of the rewrite rule. A rewrite rule is left-linear (resp. right-linear ) if no variable occurs more than once in its left-hand side (resp. right-hand side).

A term rewriting system is a tuple F, R , in which F is a set of function symbols and R is the set of term rewrite rules over T X,F . A term rewriting system is said to be left-linear (resp. right-linear) if all its rules are.

Given two term t 1 and t 2 , we say that there exists a rewrite relation on T X,F for (t 1 , t 2 ) induced by F, R , denoted by t 1 t 2 , if it satisfies:

• There exists a rule (l, r) ∈ R and a substitution σ such that σ(l) is a subterm of t 1 .

• The term t 2 is obtained from t 1 by replacing the occurrence of σ(l) by σ(r).

We now define the application of term rewriting rules to graph, in other words, we make the graph representation of term rewriting rules. Let G be a graph and n and n ′ be nodes of G, the triple (G, n, n ′ ) is called a graph rewrite rule and n, n ′ are the left root and the right root of the rule.

A pair ∆ = (r, f ) is a redex in a graph G 0 if r is a graph rewrite rule (G, n, n ′ ) and f is a homonorphism from G| n to G 0 . The homonorphism is called an occurrence of the rule r. We first begin with some example to illustrate the definition of graph rewriting technique by showing how the translation of term rewrite rules to graph rewrite rule work.

Let t l → t r be a term rewrite rule, we will construct the corresponding graph rewrite rule (G, n, n ′ ). The construction works as follows. First we take the graph representing of both Inria left and right hand sides of the term rewrite rule to form the union of these graphs, sharing those nodes which represent the same structures in t l and t r . This resulting shared graph is G. Then we take the roots of t l and t r to be n and n ′ , respectively. For example, we illustrate the construction of the graph rewrite rule for the following term rewrite rule:

φ(c, x, f alse) → c ∧ x
We first make the graph representing of φ(c, x, f alse) and c ∧ x on the left of the Figure 25. Then the union graph sharing the same nodes (c and x) is depicted on the right. Finally, the left root n and right root n ′ are the nodes labelled φ and ∧. Thus the graph rule is represented as follows: The build phase The resulting graph G 1 = N 1 , succ 1 , r 1 in this phase, denoted by G 1 = G 0 + f (G, n, n ′ ), is constructed as follows.

(n : φ(n c : c, n x : x, f alse) + n ′ : ∧(n c , n x ), n, n ′ ) Let ((G, n, n ′ ), f : G| n → G 0 ) be a redex
•

N 1 = N G0 ⊎ (N G| n ′ \ N G|n )
, where ⊎ denotes the disjoint union of two sets. For any node m ∈ N G1 , it has the same label as in G 0 if m ∈ N G0 . Otherwise, it has the same label as in G.

• r 1 = r G0 .

• for every node m i = succ G1 (m) i ,

m i =      succ G0 (m) i , if m ∈ N G0 succ G (m) i , if m, succ G (m) i ∈ N G| n ′ \ N G|n f (succ G (m) i ), if m ∈ N G| n ′ \ N G|n , succ G (m) i ∈ N G|n
The redirection phase In this step all references to the node f (n) are replaced by the references to the node n ′ , the resulting graph is denoted by

G 2 = N 2 , succ 2 , r 2 = G 1 [f (n) := n ′ ].
This replacement is defined by a substitution operation in the term graph G 1 with two nodes f (n) and n ′ as follows.

• for every node c ∈ N 1 and c ∈ N 2 , they have the same label.

• for every node

c ∈ N 1 , succ 2 (c) i = n ′ if succ 1 (c) i = f (n), otherwise succ 2 (c) i = succ 1 (c) i . • r 2 = n ′ if r 1 = f (n), otherwise r 2 = r 1 .

RR n°8508

The garbage collection phase In this last step, we define G 3 = G 2 | r2 which is a part of the graph G 2 accessible from its root. We denote the graph G 3 by GC(G 2 ). Given a redex ∆ = (r, f ) and a graph G 0 , the construction of the graph resulting from the reducing the redex ∆ in the graph G 0 , denoted by RED(∆, G 0 ), is defined as:

RED(((G, n, n ′ )f ), G 0 ) = GC((G 0 + f (G, n, n ′ ))[f (n) := n ′ ])
To illustrate the above construction of graph rewriting, we consider the following example: (G, n, n ′ ) = (n : φ(n c : c, n x : x, f alse) + n ′ : ∧(n c , n x ), n, n ′ ) is the graph rule above, G 0 = ∨(φ(c, x, f alse), y) and a homomorphism f from G| n to G 0 as depicted in Figure 26. We first copy the part of G| ′ n which is not contained in G| n to G 0 , with node labels, successors, and root defined in the build phase. We obtain the resulting graph G 1 . Then all edges of G 1 pointing to f (n) are replaced by edges pointing to the copy of n ′ , giving the graph G 2 as depicted in Figure 27. The root of G 2 is the root of G 1 if that node not equal to f (n). Otherwise, the root of G 2 is the copy of n ′ as described in the redirection phase. From the graph G 2 , we remove The normalizing algorithm indicates that we apply the rewrite rules to each graph node individually. When there is no more rules can be applied to the resulting graph, we maximize the shared nodes. When there exists no more sharing or rules can be applied, the process terminates.

We classify our set of rewrite rules into three basic types: general simplification rules, optimization-specific rules and synchronous rules. In the following, we will present the rewrite rules of these types, and we assume that all nodes in our shared value-graph are typed. Note that we only write the rewrite rules in forms of term rewrite rules, t l → t r .

General simplification rules

The general simplification rules contain the rules which are related to the general rules of inferences of operators, denoted by the corresponding function symbols in F . In our consideration, the operators used in the primitive stepwise functions and in the generated C code are are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=), and numerical operators (+, -, *, /). When applying these rules, we will replace a subgraph rooted at a node by a smaller subgraph. In consequence of this replacement, they will reduce the number of nodes by eliminating some unnecessary structures.

= (t, t) → true

(1)

= (t, t) → f alse (2) = (t, true) → t (3) = (t, true) → ¬t (4)
= (t, f alse) → ¬t (5)

= (t, f alse) → t (6)
The first set of general simplification rules simplifies applied numerical and boolean comparison expressions. In these rules, the term t represents a structure of value computing (e.g., the computation of expression b = x = true). The rules 3, 4, 5, and 6 only apply on the boolean type. These rules are self explanatory, for instance, with any structure represented by a term t, the expression t = t can always be replaced with the value true.

The second set of general simplification rules eliminates unnecessary nodes in the graph that represent the φ-functions, where c, c 1 and c 2 are boolean expressions. For better representation, we divide this set of rules into several subset as follows.

φ(true, x 1 , x 2 ) → x 1 (7)
φ(f alse, x 1 , x 2 ) → x 2 (8)
The rules in this set replace a φ-function with its left branch if the condition always holds the value true. Otherwise, if the condition holds the value false, it is replaced with its right branch.

φ(c, true, x) → c ∨ x (12) φ(c, x, f alse) → c ∧ x (13) φ(c, x, true) → ¬c ∨ x (14)
The rules operate on boolean expressions represented by the branches. When one of the branches is boolean constant, the φ-function can be replaced with a boolean expression of the condition c and the non-constant branch. For instance, when the left branch is a constant and holds the value true, then the φ-function is replaced with the boolean expression c ∨ x.

φ(c, x, x) → x (15)
The rule 15 removes the φ-function if all of its branches contain the same value. A φ-function with only one branch is a special case of this rule. It indicates that there is only one path to the Inria φ-function as happens with branch elimination.

φ(c, φ(c, x 1 , x 2 ), x 3 ) → φ(c, x 1 , x 3 ) (16) φ(c, x 1 , φ(c, x 2 , x 3 )) → φ(c, x 1 , x 3 ) (17) φ(c, φ(¬c, x 1 , x 2 ), x 3 ) → φ(c, x 2 , x 3 ) (18) φ(c, x 1 , φ(¬c, x 2 , x 3 )) → φ(c, x 1 , x 2 ) (19) φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 , x 1 , x 3 ) if c 1 ⇒ c 2 (20) φ(c 1 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 , x 2 , x 3 ) if c 1 ⇒ ¬c 2 (21) φ(c 1 ∧ c 2 , φ(c 1 , x 1 , x 2 ), x 3 ) → φ(c 1 ∧ c 2 , x 1 , x 3 ) (22) φ(c 1 ∧ c 2 , φ(c 2 , x 1 , x 2 ), x 3 ) → φ(c 1 ∧ c 2 , x 1 , x 3 ) (23) φ(c 1 , x 1 , φ(c 2 , x 2 , x 3 )) → φ(c 1 , x 1 , x 2 ) if ¬c 1 ⇒ c 2 (24) φ(c 1 , x 1 , φ(c 2 , x 2 , x 3 )) → φ(c 1 , x 1 , x 3 ) if ¬c 1 ⇒ ¬c 2 (25) φ(c 1 ∨ c 2 , x 1 , φ(c 1 , x 2 , x 3 )) → φ(c 1 ∨ c 2 , x 1 , x 3 ) (26) φ(c 1 ∨ c 2 , x 1 , φ(c 2 , x 2 , x 3 )) → φ(c 1 ∨ c 2 , x 1 , x 3 ) (27)
Consider a φ-function such that one of its branches is another φ-function. The rules 16 to 27 removes the φ-function in the branch if one of the following conditions are satisfied:

• The conditions of the φ-functions are the same (as in the rules 16 and 17).

• The condition of the first φ-function is equivalent to the negation of the condition of the second φ-function (as in the rules 18 and 19).

• The condition of the first φ-function either implies the condition of the second φ-function or the negation (as in the rules 20 to 23).

• The negation of the condition of the first φ-function either implies the condition of the second φ-function or the negation (as in the rules 24 to 27).

The following code segment in C shows the use of the rewrite rules above:

1 if ( c ) 2 { 3 a = 0; b = 0; d = a ; 4 } 5 else 6 { 7 a = 1; b = 1; d = 0; 8 } 9 if ( a == b ) x = d ; else x = 1; return x ;
If we analyze this code segment the return value is 0. In fact, a and b have the same value in both branches of the first "if" statement. Thus in the second "if" statement the condition is always true, then x always holds the value of d which is 0. We will apply the general simplification rules to show that the value-graph of this code segment can be transformed to the value-graph of the value 0. We represent the value-graph in form of linear notation. The value-graph of the computation of x is φ(= (a, b), d, 0). Replace the definition of a, b and d, and normalize this graph, we get:

x →φ(= (φ(c, 0, 1), φ(c, 0, 1)), φ(c, φ(c, 0, 1), 0), 0) φ(true, φ(c, φ(c, 0, 1), 0), 0) by ( 1)

φ(c, φ(c, 0, 1), 0) by ( 7)

φ(c, 0, 0) by ( 16) 0 by (15)

Optimization-specific rules

Based on the semantics of Signal compiler, we have a number of optimization-specific rules rewrite graphs in a way that reflexes the effects of specific optimizations of the compiler. The affection of these rules does not always reduce the graph or make it simpler. One has to know specific optimizations of the compiler when she want to add them to the set of rewrite rules. In our case, the set of rules for simplifying constants expressions of the Signal compiler are given as follows.

Specific rules for constant expressions with numerical operators:

+(cst 1 , cst 2 ) → cst, where cst = cst 1 + cst 2 (28) * (cst 1 , cst 2 ) → cst, where cst = cst 1 * cst 2 (29) -(cst 1 , cst 2 ) → cst, where cst = cst 1 -cst 2 (30)
/(cst 1 , cst 2 ) → cst, where cst = cst 1 /cst 2 (31)
Specific rules for constant expressions with usual logic operators:

¬f alse → true (32)
¬true → f alse (33)

∧(cst 1 , cst 2 ) → cst, where cst = cst 1 ∧ cst 2 (34) ∨(cst 1 , cst 2 ) → cst, where cst = cst 1 ∨ cst 2 (35)
Specific rules for constant expressions with numerical comparison functions:

(cst 1 , cst 2 ) → cst (36)
where = <, >, =, <=, >=, /=, and the boolean value cst is the evaluation of the constant expression (cst 1 , cst 2 ) which can hold either the value false or true.

We also may add a number of rewrite rules that are derived from the list of rules of inferences for propositional logic. For example, we have a group of laws for rewriting formulas with and operator, such as:

∧(x, f alse) → f alse ∧(x, true) → x ∧(x, ⇒ (x, y)) → x ∧ y
Consider the following Signal program and its generated C code, in which the input signal x is present when the other boolean input signal cx is true.

{ẑ, pz} ∨ {x} ∧ <= {pz} m.z 1 {z} φ {z} φ x 0 # {pz} φ {x} φ m.z c {C_x c } <= {z c , z c } φ x c {x c } φ
x c → φ(true, x c , #) → x → φ(true, x, #) (38)
We write x → φ(true, x, #) to denote that x points to the subgraph rooted at the node labelled by φ-function. The rule 38 indicates that if a variable in the generated C code is always updated, then we required that the corresponding signal in the source program is always present meaning that the signal never holds the absent value. In consequence of this rewrite rule, the signal x and its value when it is present x (resp. the variable x c and its updated value x c in the generated C code) point to the same node in the shared value-graph. Every references to x and x (resp. x c and x c ) point to the same node. For example, consider the value-graph in Figure 29, we rewrite the subgraph representing the clock ẑ and pz into a single node labelled by the value true. Then, we apply the rule 7 on the resulting graph, we obtain the reduced graph in Figure 30.

We also have the second synchronous rule that mirrors the semantics of the delay operator of the Signal language. For instance, we consider the equation pz := z$1 init 0 in Listing 9. In the representation of the Signal program, we use the variable m.z to capture the last value of the signal z. And in the generated C code the last value of the variable z c is denoted by m.z c . We require that the last values of a signal and the corresponding variable in the generated C code are the same. That means m.z

= m.z c . m.x c → G 1 + m.x → G 2 → m.x c , m.x → G 1 (39)
The rule 39 indicates that for any signal x and its corresponding variable in the generated C code which involves in a delay operator, then we required that the last values of Finally, we add rules that mirrors the assumption on input signals and their corresponding variables in the generated C code. For any input signal x and the corresponding variable x c in the generated C code, if x is present, then the value of x which is read from the environment then the value of the variable x c after the reading statement in the C code must be equivalent. That means x c and x are represented by the same subgraph in the shared value-graph. We require that the clock of the input signal x is equivalent to the condition in which the variable x c is updated if the clock of x is also read from the environment as a parameter. Meaning that we represent x and C_x c by the same subgraph in the shared value-graph.

x c → G 1 + x → G 2 → x c , x → G 1 (40) C_x c → G 1 + x → G 2 → C_x c , x → G 1 (41)
In consequence of these rewrite rule, every references to x and C_x c (resp. x and x c ) point to the same node. By rule 40 we obtain the final normalized value-graph of the program in Listing 10 and its generated C code as in Figure 32. We can observe that the value of the signal z and the corresponding variable z c are presented by the same subgraph. Therefore, we can safely conclude that the value of output signal z and the corresponding variable z c in the generated C code are equivalent.

Implementation

We describe the main steps of our approach, and the main techniques which are used to implement them. This implementation can be integrated into the existing Polychrony toolset to prove the the preservation of value-equivalence of variables. Given a Signal program A, with an unverified compiler, we consider the following process:

1. The compiler takes program A and compiles it.

2. If there is any error (e.g., syntax error), it outputs an Error.

3. Otherwise, it outputs the generated C code C = Gr(A).

These steps can be represented in the following pseudo-code, where Gr(A) is the code generation phase from the source program A to either C program C or compilation errors:

1 if ( Gr ( A ) is Error ) 2 output Error ; 3 else output C ; Now, it is followed by our validator which checks that for any output signal x in the source program A and the corresponding variable x c in the C program, they have the same value, x = x c . In other words, x and x c point to the same node in the shared value-graph representing the computations of signals and variables in A and C. We denote this fact by C ⊑ value A.

Inria

This verification process will provide a formal guarantee as strong as that provided by a formal compiler verification approach with the assumption that our validator is formally correct.

The main components of the verification framework is depicted in Figure 33. The validator works as follows. First, it computes the Signal program and the corresponding C program into value-graphs that represent the output computations of the programs. The value-graph can be considered as a generalization of the result of symbolic evaluation. Then, the resulting valuegraphs is used to construct a single graph by allowing sharing between the two distinct graphs. The shared value-graph is transformed by applying some graph rewrite rules, this process is called normalization. The set of rewrite rules reflexes the general rules of inferences of operators, or the optimizations of the compiler. For instance, consider the 3-node subgraph representing the expression 1 > 0, the normalization will transform that graph into a single node subgraph representing the value true, as it reflexes the constant folding.

Finally, it compares the values of the output signals and the corresponding variables in the C program. For every pair of signal and variable, if their values are equivalent meaning that they point to the same node in the shared graph, the validator return correct. Therefore, in the best case, when semantics has been preserved, the value comparison of the output signals and their corresponding variables has constant time complexity O(1). In fact, it is always expected that most transformations and optimizations are semantics-preserving, thus the best-case complexity is important. In the final step, we check that the value of the output signal and its corresponding variable in the generated code merge into a single node. In this example, we can safely conclude that the output signal N and its corresponding variable N c is equivalent since they point to the same node in the final normalized value-graph.

Discussion

There is a wide range of works for value-graph representations of expression evaluations in a program. For example, in [START_REF] Weise | Value dependence graphs: Representation without taxation[END_REF], Weise et al. present a nice summary of the various type of value-graph.

Another related work which adopts the translation validation approach in verification of optimizations. Tristan et al. [START_REF] Tristan | Evaluating value-graph translation validation for llvm[END_REF] recently proposed a framework for translation validation of LLVM optimizer. For a function and its optimized counterpart, they compute a shared valuegraph. The graph is normalized (roundly speaking, the graph is reduced). After the normalizing, if the outputs of two functions are represented by the same sub-graph, they can safely conclude that two functions are equivalent.

On the other hand, Tate et al. [START_REF] Tate | Equility saturation: A new approach to optimization[END_REF] proposed a framework for translation validation. Given a function in the input program and the corresponding optimized version of the function in the output program, they compute two value-graphs to represent the computations of the variables. They then transform the graph by adding equivalent terms through a process called equality saturation. After the saturation, if two value-graph are the same, they can conclude that the return value of two given functions are the same. However, for the translation validation purpose, our normalization process is more efficient and scalable since we can add some rewrite rules into the validator that reflexes what a typical compiler intends to do (e.g., a compiler will do the constant folding optimization, then we can add the rewrite rule for constant expressions such as 1 + 2 is replaced by a single node 3).

The present chapter provides a proof of correctness of a multi-clocked synchronous programming language compiler for the preservation of value-equivalence of variables and applies this approach to the synchronous data-flow compiler Signal. We believe that the translation validation of synchronous data-flow value-graph of the industrial compiler Signal without instrumentation is feasible and efficient.

Inria

Figure 1 :

 1 Figure 1: A bird's-eye view of the verification process

  The implicit clock relation is C y = C x ∪ C z . • Sampling: y := x when b where b is a Boolean signal, defines a basic process such that ∀t ∈ C x ∩ C b ∧ b(t) = true, y(t) = x(t), and otherwise, y is absent. The implicit clock relation is C y = C x ∩ [b], where the sub-clock [b] is defined as {t ∈ C b |b(t) = true}.

  Let us comment this program:• Lines (2) and (3): F B, N are respectively input and output signals of type integer.

Figure 2 :

 2 Figure 2: Code generation: General scheme

Inria

4 And

 4 Illustrative exampleWe begin by showing how our verification process works for an illustrative example. Consider the following synchronous program WHENOP written in Signal language which is given in Listing 3WHENOP_step is step function of the generated C code. This function which is called repeatedly in an infinite loop, simulates one synchronous step of the Signal program which is shown in Listing 4.Listing 4 : Synchronous Step of WHENOP

Figure 3 :

 3 Figure 3: The shared value-graph of WHENOP and its generated C code

Figure 4 :

 4 Figure 4: The resulting transformed value-graph

Figure 5 :

 5 Figure 5: The resulting transformed value-graph

Figure 6 :

 6 Figure 6: The directed graphs of a + b * c and a + b, b * c

Figure 7 :

 7 Figure 7: The subgraph rooted at node labelled + and a root-cyclic graph

Figure 8 :

 8 Figure 8: An example of homomorphism

  is the set of edges. It describes the computation relation such that a operand and operator relation between the nodes. • I ⊆ N is the set of input nodes. They are the input signals and their corresponding variables in the generated C code. • O ⊆ N is the set of output nodes. They are the output signals and their corresponding variables in the generated C code. • m N : N -→ P(V ) is a mapping labeling each node with a finite set of clocks, signals, and variables. It defines the set of clocks, signals or variables in the Signal program and the generated C code such that they are equivalent to the computation value which is pointed by the node.

Listing 5 :

 5 Simple Program in Signal

Figure 9 :Figure 10 :

 910 Figure 9: The subgraphs of y := x * x1 and x1 := x + 1

Figure 11 :

 11 Figure 11: The graph of y := f (x 1 , ..., x n ) For instance, consider the following Signal equation: y := (x >= 1) and c

yFigure 12 :Figure 13 :

 1213 Figure 12: The graph of y := (x >= 1) and c

1 Figure 14 :Figure 15 :

 11415 Figure 14: The graph of y := (x$1 init 1) + z

1 Figure 16 :Figure 17 :

 11617 Figure 16: The graph of y := x default (z + 1)

Figure 20 .Figure 18 :

 2018 Figure 18: The graph of y := x when (z >= 1)

Figure 19 :Figure 20 :

 1920 Figure 19: The graphs of (1) z :=ˆx, (2) xˆ= y and (3) z := xˆ+ y

Figure 21 :

 21 Figure 21: The graph of SDVGMerge step function

Figure 22 :

 22 Figure 22: The graphs of N and C_z's computations

Figure 23 :Figure 24 :

 2324 Figure 23: The transformation of the graph of t * (u + 1)

Figure 25 :

 25 Figure 25: The graph rule of the term rule φ(c, x, f alse) → c ∧ x of the general construction of the graph rewriting from a graph rewrite rule (G, n, n ′ ). The construction consists of three phases: build, redirection and garbage collection, which are defined as follows.

Figure 26 :

 26 Figure 26: An example of graph rewriting

Figure 27 :

 27 Figure 27: Graph rewriting: Build and redirection phases all nodes which are not accessible from the the root, giving the result of the rewrite, the graph G 3 as depicted in Figure 28.

6. 2 NormalizingFigure 28 :Listing 8 :

 2288 Figure 28: Graph rewriting: Garbage collection phases

φ

  (c, f alse, true) → ¬c[START_REF] Ballance | The program dependence web: A representation supporting control, data, and demand driven interpretation of imperative languages[END_REF] φ(c, true, f alse) → c[START_REF] Barendregt | Towards an intermediate language based on graph rewriting[END_REF] The rules operate on boolean expressions represented by the branches. When the branches are boolean constants and holds different values, the φ-function can be replaced with the value of the condition c. φ(c, f alse, x) → ¬c ∧ x[START_REF] Turner | A new implementation technique for applicative languages[END_REF]

Figure 29 :

 29 Figure 29: The shared value-graph of MasterClk and its generated C code

1 {z 1 {zFigure 31 :

 1131 Figure 30: The resulting graph of MasterClk and its generated C code 38

  Figure 32: The final normalized graph of MasterClk and its generated C code

{ 1 {NFigure 36 :

 136 Figure 35: The resulting value-graph of DEC and its generated C code

RR n°8508

Inria

/* Signal equation */

/* Generated C code */

if ( C_cx )Inria

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

The generated C code of the step function are given in Listing 7. The computations of variable z in this function can be represented by the following gated φ-function:

The shared value-graph of SDVGMerge_step() is depicted in Figure 21. In this graph, we replace the node φ(C_cx c , φ(cx c , x c , #), #) by φ(C_cx c ∧ cx c , x c , #). We do the same for the node φ(C_cy c , φ(cy c , y c , #), #).

Listing 7 : Generated C code of SDVGMerge In the generated C program, the computation of the variable whose clock is the master clock, which ticks every time the step function is called, is implemented without the conditional if -then -else statement and it is always updated when the step function is invoked. The computation of such variables can be represented by a node in the shared value-graph as follows:

This representation is used for any variable in the generated C code such that this variable is always updated when the step function is called. For instance, consider the following code segment which computes the values of the output signal N in program DEC and the variable C_z in the SDVGMerge_step() function in the following listing:

When we construct the value-graph of the signal x, it is represented by x = φ(x, x, #) where x ⇔ cx ∧ cx. In the generated C code, the value of x is read only when the condition C_cx ∧ cx is true that is represented by x = φ(C_cx, φ(cx, x, #), #). This observation makes us add the following rewrite rule into the systems to mirror the above rewriting of the Signal compiler.

(37)

Synchronous rules

In addition to the general and optimization-specific rules, we also have a number of rewrite rules that are derived from the semantics of the code generation mechanism of the Signal compiler.

To illustrate why the synchronous rules need to be added in our validator, we consider the Signal program in Listing 9 and the corresponding generated C code in Listing 10. The shared value-graph of the Signal program and its generated C code is given in Figure 29. In this example, the fastest clock ẑ, called the master clock. All other clocks are expressed as calculus expression of the master clock (i.e., the clock x is an under-sampling of ẑ according to the values of boolean expression pz <= 1). Such programs, also referred to as endochronous, can be executed in a deterministic way.

Consider the generated C code, we observe that the value of the variable z is always updated. It holds the value of x if C x is true, otherwise it is 0. Therefore, we have the following rule that [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF]. In lines (3) and [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF], the references to the variable N c are the references to the last value of N c which is denoted by m.N c . The variable F B c which corresponds to the input signal F B is updated only when the variable C_F B c is true.

In the second step, we will normalize the above initial shared value-graph. Below is a potential normalization scenario. Figure 35 depicts the intermediate resulting value-graph of this normalization scenario. And Figure 36 is the final normalized value-graph from the initial graph when we cannot perform any more normalization.

• The clock of the output signal N is a master clock which is indicated in the generated C that the variable N c is always updated. By rule 38, the nodes { N , ZN } ∨ is rewritten into true.

• By rule ∧(true, x) → x, the nodes { F B} ∧ is rewritten into { F B} <=.

• The node φ-function represents the computation of N is removed and N points to the node {N } φ by rule 7.

• The node φ-function represents the computation of N N is removed and N N points to the node {ZN } m.N by rule 7.

•