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)

Abstract: 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
From: Jean-Pierre Talpin <>
Submitted on: Tuesday, 30 June 2009 13:46:47
Updated on: Monday, 6 July 2009 14:26:41

See detailed view

Associated documents

PDF :

PS :

Export

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>Research reports</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>