HAL - INRIA :: [inria-00400272, version 1] Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form

inria-00400272, version 1

Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form

Loïc Besnard ()^a^, 1, Thierry Gautier ()^b^, 1, Matthieu Moy ², Jean-Pierre Talpin ()^b^, 1, Kenneth Johnson^b^, 1, Florence Maraninchi () ²

N° RR-6976 (2009)

Résumé : We present an approach for the translation of imperative code (like C, C++) into the synchronous formalism \signal, in order to use a model-checker to verify properties on the source code. The translation uses ßa\ as an intermediate formalism, and the GCC compiler as a front-end. The contributions of this paper with respect to previous work are a more efficient translation scheme, and the management of parallel code. It is applied successfully on simple \systemc\ examples.

a – CNRS
b – INRIA
1 : ESPRESSO (INRIA - IRISA)
CNRS : UMR6074 – INRIA – INSA Rennes – Université de Rennes 1
2 : VERIMAG (VERIMAG - IMAG)
CNRS : UMR5104 – Université Joseph Fourier - Grenoble I – Institut National Polytechnique de Grenoble (INPG)

inria-00400272, version 1
http://hal.inria.fr/inria-00400272
oai:hal.inria.fr:inria-00400272
Contributeur : Jean-Pierre Talpin <>
Soumis le : Mardi 30 Juin 2009, 13:46:47
Dernière modification le : Lundi 6 Juillet 2009, 14:26:41

Voir la fiche détaillée

Documents associés

PDF :

PS :

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="report"><head>Rapports</head>
<biblStruct type="report" xml:id="inria-00400272"><monogr>
<author><persName><forename>Loïc</forename><surname>Besnard</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">ESPRESSO</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Thierry</forename><surname>Gautier</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">ESPRESSO</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Matthieu</forename><surname>Moy</surname></persName>
<affiliation>
<orgName type="laboratory">VERIMAG - IMAG</orgName>
<orgName type="team">VERIMAG</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR5104</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Institut National Polytechnique de Grenoble (INPG)</orgName>
</affiliation>
</author>
<author><persName><forename>Jean-Pierre</forename><surname>Talpin</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">ESPRESSO</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Kenneth</forename><surname>Johnson</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">ESPRESSO</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Florence</forename><surname>Maraninchi</surname></persName>
<affiliation>
<orgName type="laboratory">VERIMAG - IMAG</orgName>
<orgName type="team">VERIMAG</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR5104</orgName>
<orgName type="institution">Université Joseph Fourier - Grenoble I</orgName>
<orgName type="institution">Institut National Polytechnique de Grenoble (INPG)</orgName>
</affiliation>
</author>
<title type="main" level="m">Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form</title><title type="main" level="m">Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form</title><imprint><biblScope type="publicationDate">2009-00-00</biblScope><biblScope type="pp">16</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00400272</idno><idno type="HALFile">http://hal.inria.fr/inria-00400272/PDF/RR-6976.pdf</idno></biblStruct>
</listBibl>
</listBibl>