Towards a verified compiler prototype for the synchronous language SIGNAL

详细信息    查看全文

• 作者：Zhibin Yang ; Jean-Paul Bodeveix ; Mamoun Filali ; Kai Hu…
• 关键词：synchronous languages ; SIGNAL ; guarded actions ; verified compiler ; Coq ; architecture analysis and design language (AADL)
• 刊名：Frontiers of Computer Science in China
• 出版年：2016
• 出版时间：February 2016
• 年：2016
• 卷：10
• 期：1
• 页码：37-53
• 全文大小：817 KB
• 参考文献：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–1304CrossRef
  3.Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 1991, 79(9): 1305–1320CrossRef
  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–149MATH MathSciNet CrossRef
  6.Dijkstra EW. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453–457MATH MathSciNet CrossRef
  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–56CrossRef
  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–867CrossRef
  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–69CrossRef
  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–626MathSciNet CrossRef
  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–6CrossRef
  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–166CrossRef
  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–616MathSciNet CrossRef
  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–303CrossRef
  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–693MathSciNet CrossRef
  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–68CrossRef
  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): 82CrossRef
  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): 36CrossRef
  34.Thiele L, Wilhelm R. Design for timing predictability. Real-Time Systems, 2004, 28(2–3): 157–177CrossRef
  35.Potop-Butucaru D, Caillaud B, Benveniste A. Concurrency in synchronous systems. Formal Methods in System Design, 2006, 28(2): 111–130MATH CrossRef
  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–180CrossRef
  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–28MATH CrossRef
  41.Schoeberl M. A time predictable instruction cache for a Java processor. Lecture Notes in Computer Science, 2004, 3292: 371–382CrossRef
  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–127CrossRef
  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): 9CrossRef
  
• 作者单位：Zhibin Yang (1) (2) (3)
  Jean-Paul Bodeveix (2)
  Mamoun Filali (2)
  Kai Hu (3)
  Yongwang Zhao (3)
  Dianfu Ma (3)
  
  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
  
• 刊物类别：Computer Science
• 刊物主题：Computer Science, general
  Chinese Library of Science
  
• 出版者：Higher Education Press, co-published with Springer-Verlag GmbH
• ISSN：1673-7466

文摘

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 safety-critical 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)