Verified Compilation of Synchronous Dataflow with State Machines

Timothy Bourke; Basile Pesin; Marc Pouzet

doi:10.1145/3608102

Verified Compilation of Synchronous Dataflow with State Machines

Timothy Bourke, Basile Pesin, Marc Pouzet

École Polytechnique

PSL research University & IPSL

Research output: Contribution to journal › Article › peer-review

Abstract

Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.

Original language	English
Article number	137
Journal	ACM Transactions on Embedded Computing Systems
Volume	22
Issue number	5 s
DOIs	https://doi.org/10.1145/3608102
Publication status	Published - 9 Sept 2023

Keywords

Stream languages
interactive theorem proving
verified compilation

Access to Document

10.1145/3608102

Cite this

@article{dd43ff4247344f988f52417ca84a9da7,

title = "Verified Compilation of Synchronous Dataflow with State Machines",

abstract = "Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the V{\'e}lus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.",

keywords = "Stream languages, interactive theorem proving, verified compilation",

author = "Timothy Bourke and Basile Pesin and Marc Pouzet",

note = "Publisher Copyright: {\textcopyright} 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM.",

year = "2023",

month = sep,

day = "9",

doi = "10.1145/3608102",

language = "English",

volume = "22",

journal = "ACM Transactions on Embedded Computing Systems",

issn = "1539-9087",

number = "5 s",

}

TY - JOUR

T1 - Verified Compilation of Synchronous Dataflow with State Machines

AU - Bourke, Timothy

AU - Pesin, Basile

AU - Pouzet, Marc

PY - 2023/9/9

Y1 - 2023/9/9

N2 - Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.

AB - Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.

KW - Stream languages

KW - interactive theorem proving

KW - verified compilation

U2 - 10.1145/3608102

DO - 10.1145/3608102

M3 - Article

AN - SCOPUS:85171746172

SN - 1539-9087

VL - 22

JO - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

IS - 5 s

M1 - 137

ER -

Verified Compilation of Synchronous Dataflow with State Machines

Abstract

Keywords

Access to Document

Fingerprint

Cite this