TY - GEN
T1 - A formally verified compiler for lustre
AU - Bourke, Timothy
AU - Brun, Lélio
AU - Dagand, Pierre Évariste
AU - Leroy, Xavier
AU - Pouzet, Marc
AU - Rieg, Lionel
PY - 2017/6/14
Y1 - 2017/6/14
N2 - 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. Copyright is held by the owner/author(s).
AB - 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. Copyright is held by the owner/author(s).
KW - Formally verified compilation
KW - Interactive theorem proving (Coq)
KW - Synchronous languages (Lustre)
U2 - 10.1145/3062341.3062358
DO - 10.1145/3062341.3062358
M3 - Conference contribution
AN - SCOPUS:85025163024
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 586
EP - 601
BT - PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Cohen, Albert
A2 - Vechev, Martin
PB - Association for Computing Machinery
T2 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
Y2 - 18 June 2017 through 23 June 2017
ER -