Towards a verified compiler prototype for the synchronous language SIGNAL

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)

References

[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

[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

[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

[6] Dijkstra EW. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453–457

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[34] Thiele L,Wilhelm R. Design for timing predictability. Real-Time Systems, 2004, 28(2–3): 157–177

[35] Potop-Butucaru D, Caillaud B, Benveniste A. Concurrency in synchronous systems. Formal Methods in System Design, 2006, 28(2): 111–130

[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

[37] Baudisch D, Brandt J, Schneider K. Dependency-driven distribution of synchronous programs. IFIP Advances in Information and Communication Technology, 2010, 329: 169–180

[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

[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

[41] Schoeberl M. A time predictable instruction cache for a Java processor. Lecture Notes in Computer Science, 2004, 3292: 371–382

[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

[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

[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

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg