A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs

Gang Shi, Yuanke Gan, Shu Shang, Shengyuan Wang, Yuan Dong, Pen Chung Yew

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Synchronous data-flow languages (SDFL), such as Lustre [1], is a concurrent language that has been widely used in safety-critical systems. Verified compilers for such languages are crucial in generating trustworthy object code. A good approach is to first translate a concurrent SDFL program to a sequential intermediate representation, such as a Clight [2] code, and then use an existing verified compiler such as CompCert [3] to produce executable object code for the target machine. A verified Sequentializer is crucial in such a verified compiler. It produces a sequential topological order among the program statements that preserve the program dependencies and the dynamic semantics of the original program. In this paper, we show such an approach for a SDFL language such as Lustre. The approach is general enough to be applicable to other SDFLs as well. It first gives a formal specification of the operational semantics, and proves its determinism property for a Lustre-like program. It then formally proves the equivalence of the original concurrent semantics and its target sequential semantics using the well-established proof assistant Coq ([4], [5]), and extracts the certified code for such a sequentializer by Coq.

Original languageEnglish (US)
Title of host publicationProceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages109-111
Number of pages3
ISBN (Electronic)9781538615898
DOIs
StatePublished - Jun 30 2017
Event39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017 - Buenos Aires, Argentina
Duration: May 20 2017May 28 2017

Publication series

NameProceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017

Other

Other39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017
CountryArgentina
CityBuenos Aires
Period5/20/175/28/17

Keywords

  • Concurrency
  • Determinism
  • Semantics
  • Sequentialization
  • Synchronous Data-flow Languages
  • Verification
  • Verified Compiler

Fingerprint Dive into the research topics of 'A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs'. Together they form a unique fingerprint.

  • Cite this

    Shi, G., Gan, Y., Shang, S., Wang, S., Dong, Y., & Yew, P. C. (2017). A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs. In Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017 (pp. 109-111). [7965271] (Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICSE-C.2017.83