Skip to Main content Skip to Navigation
New interface
Journal articles

Verified Lustre Normalization with Node Subsampling

Timothy Bourke 1, 2, 3 Paul Jeanmaire 3, 2, 1 Basile Pesin 3, 2, 1 Marc Pouzet 3, 2, 1 
3 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique - ENS Paris, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : Dataflow languages allow the specification of reactive systems by mutually recursive stream equations, functions, and boolean activation conditions called clocks. Lustre and Scade are dataflow languages for programming embedded systems. Dataflow programs are compiled by a succession of passes. This article focuses on the normalization pass which rewrites programs into the simpler form required for code generation. Vélus is a compiler from a normalized form of Lustre to CompCert’s Clight language. Its specification in the Coq interactive theorem prover includes an end-to-end correctness proof that the values prescribed by the dataflow semantics of source programs are produced by executions of generated assembly code. We describe how to extend Vélus with a normalization pass and to allow subsampled node inputs and outputs. We propose semantic definitions for the unrestricted language, divide normalization into three steps to facilitate proofs, adapt the clock type system to handle richer node definitions, and extend the end-to-end correctness theorem to incorporate the new features. The proofs require reasoning about the relation between static clock annotations and the presence and absence of values in the dynamic semantics. The generalization of node inputs requires adding a compiler pass to ensure the initialization of variables passed in function calls.
Complete list of metadata

https://hal.inria.fr/hal-03370264
Contributor : Timothy Bourke Connect in order to contact the contributor
Submitted on : Thursday, October 7, 2021 - 9:17:44 PM
Last modification on : Tuesday, August 2, 2022 - 4:24:38 AM
Long-term archiving on: : Saturday, January 8, 2022 - 7:45:55 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Citation

Timothy Bourke, Paul Jeanmaire, Basile Pesin, Marc Pouzet. Verified Lustre Normalization with Node Subsampling. ACM Transactions on Embedded Computing Systems (TECS), 2021, 20 (5s), pp.1-25. ⟨10.1145/3477041⟩. ⟨hal-03370264⟩

Share

Metrics

Record views

26

Files downloads

73