Skip to Main content Skip to Navigation
Journal articles

Mechanized semantics and verified compilation for a dataflow synchronous language with reset

Timothy Bourke 1, 2, 3 Lélio Brun 3, 2, 1 Marc Pouzet 2, 1, 4, 3
3 Parkas - Parallélisme de Kahn Synchrone
Inria de Paris, DI-ENS - Département d'informatique de l'École normale supérieure, CNRS - Centre National de la Recherche Scientifique
Abstract : Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre. Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.
Complete list of metadata

Cited literature [57 references]  Display  Hide  Download

https://hal.inria.fr/hal-02426573
Contributor : Timothy Bourke <>
Submitted on : Tuesday, January 7, 2020 - 9:06:47 AM
Last modification on : Tuesday, May 4, 2021 - 2:06:02 PM

File

bourke-brun-pouzet-popl2020.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Timothy Bourke, Lélio Brun, Marc Pouzet. Mechanized semantics and verified compilation for a dataflow synchronous language with reset. Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-29. ⟨10.1145/3371112⟩. ⟨hal-02426573⟩

Share

Metrics

Record views

170

Files downloads

459