A Formally Verified Compiler for Lustre

Timothy Bourke 1 Lélio Brun 1 Pierre-Evariste Dagand 2 Xavier Leroy 3 Marc Pouzet 1 Lionel Rieg 4, 5
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
2 Whisper - Well Honed Infrastructure Software for Programming Environments and Runtimes
LIP6 - Laboratoire d'Informatique de Paris 6, Inria de Paris
3 GALLIUM - Langages de programmation, types, compilation et preuves
Inria de Paris
4 Yale University [New Haven]
5 Collège de France
Abstract : The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs. We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.
Keywords : Synchronous Languages (Lustre) Verified Compilation Interactive Theorem Proving (Coq)
Type de document :
Communication dans un congrès
PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2017, Barcelone, Spain. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, <http://pldi17.sigplan.og>
Liste complète des métadonnées

https://hal.inria.fr/hal-01512286
Contributeur : Timothy Bourke <>
Soumis le : samedi 22 avril 2017 - 06:49:47
Dernière modification le : vendredi 16 juin 2017 - 01:11:30

Fichier

velus-pldi17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01512286, version 1

Collections

UPMC | LIP6 | INRIA | PSL

Citation

Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, et al.. A Formally Verified Compiler for Lustre. PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2017, Barcelone, Spain. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, <http://pldi17.sigplan.og>. <hal-01512286>

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de
la notice

263

Téléchargements du document

305

Contact


archive-ouverte@inria.fr