Towards a verified compiler prototype for the synchronous language SIGNAL

doi:10.1007/s11704-015-4364-y

Front. Comput. Sci.

2016, Vol. 10

Issue (1) : 37-53 https://doi.org/10.1007/s11704-015-4364-y

RESEARCH ARTICLE

Towards a verified compiler prototype for the synchronous language SIGNAL

Zhibin YANG^1,^2,³,Jean-Paul BODEVEIX²,Mamoun FILALI²,Kai HU^3,^*(

),Yongwang ZHAO³,Dianfu MA³

1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics,Nanjing 210016, China
2. IRIT-CNRS, Université de Toulouse, Toulouse 31062, France
3. State Key Laboratory of Software Development Environment, Beihang University, Beijing 100191, China

Download: PDF(644 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL compiler, we propose a new intermediate representation (named S-CGA, a variant of clocked guarded actions), to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e., the translation from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theorem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multithreaded code generation with time-predictable properties. With the rising importance of multi-core processors in safetycritical embedded systems or cyber-physical systems (CPS), there is a growing need for model-driven generation of multithreaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in architecture analysis and design language (AADL), and map the multi-threaded code to this model.

Keywords synchronous languages SIGNAL guarded actions verified compiler Coq architecture analysis and design language (AADL)

Corresponding Author(s): Kai HU

Just Accepted Date: 31 August 2015 Issue Date: 06 January 2016

Cite this article:

Yongwang ZHAO,Dianfu MA,Zhibin YANG, et al. Towards a verified compiler prototype for the synchronous language SIGNAL[J]. Front. Comput. Sci., 2016, 10(1): 37-53.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-015-4364-y
https://academic.hep.com.cn/fcs/EN/Y2016/V10/I1/37

1	Potop-Butucaru D, de Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005: 1–21
2	Boussinot F, de Simone R. The ESTEREL language. Proceedings of the IEEE, 1991, 79(9): 1293–1304 https://doi.org/10.1109/5.97299
3	Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 1991, 79(9): 1305–1320 https://doi.org/10.1109/5.97300
4	Schneider K. The synchronous programming language QUARTZ. Internal Report 375. Kaiserslautern: University of Kaiserslautern, 2010
5	Benveniste A, Le Guernic P, Jacquemot C. Synchronous programming with events and relations: the SIGNAL language and its semantics. Science of Computer Programming, 1991, 16(2): 103–149 https://doi.org/10.1016/0167-6423(91)90001-E
6	Dijkstra EW. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453–457 https://doi.org/10.1145/360933.360975
7	Brandt J, Gemünde M, Schneider K, Shukla S K, Talpin J P. Integrating system descriptions by clocked guarded actions. In: Proceedings of 2011 IEEE Forum on Specification and Design Languages. 2011, 1–8
8	Brandt J, Schneider K. Separate translation of synchronous programs to guarded actions. Technische Universität Kaiserslautern. Fachbereich Informatik, 2011
9	Brandt J, Schneider K, Shukla S K. Translating concurrent action oriented specifications to synchronous guarded actions. ACM SIGPLAN Notices, 2010, 45(4): 47–56 https://doi.org/10.1145/1755951.1755896
10	Edwards S, Tardieu O. SHIM: a deterministic model for heterogeneous embedded systems. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 2006, 14(8): 854–867
11	Brandt J, Gemünde M, Schneider K, Shukla S K, Talpin J P. Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Design Automation for Embedded Systems, 2012, 18(1–2): 63–97
12	SACRES consortium. The declarative code DC+, version 1.4. Esprit Project EP 20897: Sacres. 1997
13	Besnard L, Gautier T, Talpin J P. Code generation strategies in the Polychrony environment. Research Report RR-6894. 2009
14	Jose B A, Patel H D, Shukla S K, Talpin J P. Generating multi-threaded code from polychronous specifications. Electronic Notes in Theoretical Computer Science, 2009, 238(1): 57–69 https://doi.org/10.1016/j.entcs.2008.01.006
15	Jose B, Shukla S K, Patel H D, Talpin J P. On the deterministic multithreaded software synthesis from polychronous specifications. In: Proceedings of the 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design. 2008, 129–138
16	Papailiopoulou V, Potop-Butucaru D, Sorel Y, De Simone R, Besnard L, Talpin J P. From design-time concurrency to effective implementation parallelism: the multi-clock reactive case. In: Proceedings of Electronic System Level Synthesis Conference. 2011, 1–6 https://doi.org/10.1109/eslsyn.2011.5952287
17	Hu K, Zhang T, Yang Z B. Multi-threaded code generation from Signal program to OpenMP. Frontiers of Computer Science, 2013,7(5): 617–626 https://doi.org/10.1007/s11704-013-3906-4
18	SAE. AS5506A: Architecture Analysis and Design Language (AADL) Version 2.0. 2009
19	Leroy X. Mechanized semantics for compiler verification. Lecture Notes in Computer Science, 2012, 7679: 4–6 https://doi.org/10.1007/978-3-642-35308-6_2
20	Pnueli A, Siegel M, Singerman E. Translation validation. In: Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 1998, 151–166 https://doi.org/10.1007/BFb0054170
21	Ngo V C, Talpin J P, Gautier T, Le Guernic P. Besnard L. Formal verification of synchronous data-flow program transformations toward certified compilers. Frontiers of Computer Science, 2013, 7(5): 598–616 https://doi.org/10.1007/s11704-013-3910-8
22	Izerrouken N, Pantel M, Thirioux X. Machine-checked sequencer for critical embedded code generator. In: Proceedings of the 11th International Conference on Formal Methods and Software Engineering. 2009, 521–540 https://doi.org/10.1007/978-3-642-10373-5_27
23	Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual. http: //www.irisa.fr/espresso/Polychrony/document/V4 def.pdf. 2010
24	Gamatié A. Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification. Springer Science & Business Media. 2009
25	Le Guernic P, Gautier T. Data-flow to von Neumann: the Signal approach. Advanced Topics in Data-Flow Computing, 1991, 413–438,
26	Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits, Systems, and Computers, 2003, 12(03): 261–303 https://doi.org/10.1142/S0218126603000763
27	Yang Z B, Bodeveix J P, Filali M. A comparative study of two formal semantics of the SIGNAL language. Frontiers of Computer Science, 2013, 7(5): 673–693 https://doi.org/10.1007/s11704-013-3908-2
28	Yang Z B, Hu K,Ma D F, Bodeveix J P, Pi L, Talpin J P. From AADL to timed abstract state machines: a verified model transformation. Journal of Systems and Software, 2014, 93: 42–68 https://doi.org/10.1016/j.jss.2014.02.058
29	Yang Z B, Bodeveix J P, Filali M, Hu K, Ma D F. A verified transformation: from polychronous programs to a variant of clocked guarded actions. In: Proceedings of the 17th ACM International Workshop on Software and Compilers for Embedded Systems. 2014, 128–137 https://doi.org/10.1145/2609248.2609259
30	Feautrier P, Gamatié A, Gonnord L. Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction. CSI Journal of Computing, 2012, 1(4): 86–99
31	Gamatié A, Gautier T, Le Guernic P. Toward static analysis of SIGNAL programs using interval techniques. In: Proceedings of Synchronous Languages, Applications, and Programming. 2006.
32	Axer P, Ernst R, Falk H, Girault A, Grund D, Guan N, Jonsson B, Marwedel P, Reineke J, Rochange C, Sebastian M, Von Hanxleden R, Wilhelm R, Yi W. Building timing predictable embedded systems. ACM Transactions on Embedded Computing Systems, 2014, 13(4): 82 https://doi.org/10.1145/2560033
33	Wilhelm R, Engblom J, Ermedahl A, Holsti N, Thesing S, Whalley D, Bernat G, Ferdinand C, Heckmann R, Mitra T, Mueller F, Puaut I, Puschner P, Staschulat J, Stenström P. The worst-case execution-time problem-overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems, 2008, 7(3): 36 https://doi.org/10.1145/1347375.1347389
34	Thiele L,Wilhelm R. Design for timing predictability. Real-Time Systems, 2004, 28(2–3): 157–177 https://doi.org/10.1023/B:TIME.0000045316.66276.6e
35	Potop-Butucaru D, Caillaud B, Benveniste A. Concurrency in synchronous systems. Formal Methods in System Design, 2006, 28(2): 111–130 https://doi.org/10.1007/s10703-006-7844-8
36	Besnard L, Gautier T, Le Guernic P, Talpin J P. Compilation of polychronous data flow equations. In: Shukla S K, Talpin J P, eds. Synthesis of Embedded Software. Springer US, 2010 https://doi.org/10.1007/978-1-4419-6400-7_1
37	Baudisch D, Brandt J, Schneider K. Dependency-driven distribution of synchronous programs. IFIP Advances in Information and Communication Technology, 2010, 329: 169–180 https://doi.org/10.1007/978-3-642-15234-4_17
38	Baudisch D, Brandt J, Schneider K. Multithreaded code from synchronous programs: extracting independent threads for OpenMP. In: Proceedings of the Conference on Design, Automation and Test in Europe. 2010, 949–952 https://doi.org/10.1109/date.2010.5456915
39	Baudisch D, Brandt J, Schneider K. Multithreaded code from synchronous programs: generating software pipelines for OpenMP. In: Proceedings of Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV). 2010, 11–20
40	Schoeberl M, Huber B, Puffitsch W. Data cache organization for accurate timing analysis. Real-Time Systems, 2013, 49(1): 1–28 https://doi.org/10.1007/s11241-012-9159-8
41	Schoeberl M. A time predictable instruction cache for a Java processor. Lecture Notes in Computer Science, 2004, 3292: 371–382 https://doi.org/10.1007/978-3-540-30470-8_52
42	Delange J, Feiler P. Design and analysis of multi-core architecture for cyber-physical systems. In: Proceedings of the 7th European Congress Embedded Real Time Software and Systems (ERTSS). 2014.
43	Ngo V C, Talpin J P, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychronous equations. Lecture Notes in Computer Science, 2012, 7321: 113–127 https://doi.org/10.1007/978-3-642-30729-4_9
44	Hugues J. AADLib, a library of reusable AADL models. SAE Technical Paper, 2013
45	Gamatié A, Gautier T. Synchronous modeling of avionics applications using the SIGNAL language. In: Proceedings of the 9th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS). 2003, 144–151 https://doi.org/10.1109/rttas.2003.1203046
46	Gamatié A, Gautier T, Guernic P L, Talpin J P. Polychronous design of embedded real-time applications. Transactions on Software Engineering and Methodology, 2007, 16(2): 9 https://doi.org/10.1145/1217295.1217298

[1]

Supplementary Material-Highlights in 3-page ppt

Download

[1]	Hao LIN, Guannan LIU, Fengzhi LI, Yuan ZUO. Where to go? Predicting next location in IoT environment[J]. Front. Comput. Sci., 2021, 15(1): 151306-.
[2]	Zhibin YANG, Jean-Paul BODEVEIX, Mamoun FILALI. Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL[J]. Front. Comput. Sci., 2019, 13(4): 715-734.
[3]	Maoguo GONG, Xiangming JIANG, Hao LI. Optimization methods for regularization-based ill-posed problems: a survey and a multi-objective framework[J]. Front. Comput. Sci., 2017, 11(3): 362-391.
[4]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[5]	Zhibin YANG, Jean-Paul BODEVEIX, Mamoun FILALI. A comparative study of two formal semantics of the SIGNAL language[J]. Front Comput Sci, 2013, 7(5): 673-693.
[6]	Huafeng YU, Yue MA, Thierry GAUTIER, Lo?c BESNARD, Jean-Pierre TALPIN, Paul Le GUERNIC, Yves SOREL. Exploring system architectures in AADL via Polychrony and SynDEx[J]. Front Comput Sci, 2013, 7(5): 627-649.
[7]	Kai HU, Teng ZHANG, Zhibin YANG. Multi-threaded code generation from Signal program to OpenMP[J]. Front Comput Sci, 2013, 7(5): 617-626.
[8]	Yongjian ZHAO, Hong HE, Jianxun Mi. Noisy component extraction with reference[J]. Front Comput Sci, 2013, 7(1): 135-144.
[9]	Tim SCHLüTER, Stefan CONRAD. An approach for automatic sleep stage scoring and apnea-hypopnea detection[J]. Front Comput Sci, 2012, 6(2): 230-241.
[10]	Yongjian ZHAO, Boqiang LIU, Sen WANG. A robust extraction algorithm for biomedical signals from noisy mixtures[J]. Front Comput Sci Chin, 2011, 5(4): 387-394.

Viewed

Full text

Abstract

Cited

Shared

Discussed