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

doi:10.1109/ICSE-C.2017.83

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

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 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 language	English (US)
Title of host publication	Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	109-111
Number of pages	3
ISBN (Electronic)	9781538615898
DOIs	https://doi.org/10.1109/ICSE-C.2017.83
State	Published - Jun 30 2017
Event	39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017 - Buenos Aires, Argentina Duration: May 20 2017 → May 28 2017

Publication series

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

Other

Other	39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017
Country/Territory	Argentina
City	Buenos Aires
Period	5/20/17 → 5/28/17

Bibliographical note

Funding Information:
The work was supported in part by NSFC (Grant No.61462086), MIIT (Grant No.MJ-2015-D-066) and LIAMA (grants for the project FCST).

Publisher Copyright:
© 2017 IEEE.

Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.

Keywords

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

Access

10.1109/ICSE-C.2017.83

OpenUrl availability

Full text

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). Article 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

A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs. / Shi, Gang; Gan, Yuanke; Shang, Shu et al.
Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017. Institute of Electrical and Electronics Engineers Inc., 2017. p. 109-111 7965271 (Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Shi, G, Gan, Y, Shang, S, Wang, S, Dong, Y & Yew, PC 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., 7965271, Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017, Institute of Electrical and Electronics Engineers Inc., pp. 109-111, 39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017, Buenos Aires, Argentina, 5/20/17. https://doi.org/10.1109/ICSE-C.2017.83

Shi G, Gan Y, Shang S, Wang S, Dong Y, Yew PC. 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. Institute of Electrical and Electronics Engineers Inc. 2017. p. 109-111. 7965271. (Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017). doi: 10.1109/ICSE-C.2017.83

Shi, Gang ; Gan, Yuanke ; Shang, Shu et al. / A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs. Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017. Institute of Electrical and Electronics Engineers Inc., 2017. pp. 109-111 (Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017).

@inproceedings{8009119107dd46eb808535fe1d955f42,

title = "A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs",

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.",

keywords = "Concurrency, Determinism, Semantics, Sequentialization, Synchronous Data-flow Languages, Verification, Verified Compiler",

author = "Gang Shi and Yuanke Gan and Shu Shang and Shengyuan Wang and Yuan Dong and Yew, {Pen Chung}",

note = "Funding Information: The work was supported in part by NSFC (Grant No.61462086), MIIT (Grant No.MJ-2015-D-066) and LIAMA (grants for the project FCST). Publisher Copyright: {\textcopyright} 2017 IEEE. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.; 39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017 ; Conference date: 20-05-2017 Through 28-05-2017",

year = "2017",

month = jun,

day = "30",

doi = "10.1109/ICSE-C.2017.83",

language = "English (US)",

series = "Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "109--111",

booktitle = "Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017",

}

TY - GEN

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

AU - Shi, Gang

AU - Gan, Yuanke

AU - Shang, Shu

AU - Wang, Shengyuan

AU - Dong, Yuan

AU - Yew, Pen Chung

N1 - Funding Information: The work was supported in part by NSFC (Grant No.61462086), MIIT (Grant No.MJ-2015-D-066) and LIAMA (grants for the project FCST). Publisher Copyright: © 2017 IEEE. Copyright: Copyright 2017 Elsevier B.V., All rights reserved.

PY - 2017/6/30

Y1 - 2017/6/30

N2 - 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.

AB - 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.

KW - Concurrency

KW - Determinism

KW - Semantics

KW - Sequentialization

KW - Synchronous Data-flow Languages

KW - Verification

KW - Verified Compiler

UR - http://www.scopus.com/inward/record.url?scp=85026739254&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85026739254&partnerID=8YFLogxK

U2 - 10.1109/ICSE-C.2017.83

DO - 10.1109/ICSE-C.2017.83

M3 - Conference contribution

AN - SCOPUS:85026739254

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

SP - 109

EP - 111

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

PB - Institute of Electrical and Electronics Engineers Inc.

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

Y2 - 20 May 2017 through 28 May 2017

ER -

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

Abstract

Publication series

Other

Bibliographical note

Keywords

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this