Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL

Abstract

This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.

Keywords

synchronous languages / SIGNAL / Synchronous Clocked Guarded Actions (S-CGA) / Objective Caml / functional programming

References

[1] Harel D, Pnueli A. On the development of reactive systems. Logics and Models of Concurrent Systems,1989, F(13): 477–498

[2] Potop-Butucaru D, De Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005, 1–21

[3] Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293–1304

[4] Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 1991, 79(9): 1305–1320

[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] Schneider K. The synchronous programming language QUARTZ. Internal Report. Kaiserslautern: University of Kaiserslautern, 2010

[7] Teehan P, Greenstreet M, Lemieux G. A survey and taxonomy of GALS design styles. IEEE Design and Test of Computers, 2007, 24(5): 418–428

[8] Benveniste A, Caillaud B, Le Guernic P. From synchrony to asynchrony. In: Proceedings of International Conference on Concurrency Theory. 1999, 162–177

[9] Feautrier P, Gamatié A, Gonnord L. Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction, Technical Report. 2013

[10] Gamatié A, Gautier T, Le Guernic P. Towards static analysis of SIGNAL programs using interval techniques. In: Proceedings of Synchronous Languages, Applications, and Programming. 2006

[11] Gamatié A, Gautier T, Besnard L. An interval-based solution for static analysis in the SIGNAL language. In: Proceedings of the 15th Annual IEEE International Conference andWorkshop on Engineering of Computer Based Systems. 2008, 182–190

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

[13] Brandt J, Gemunde M, Shukla S K, Talpin J P. Integrating system descriptions by clocked guarded actions. In: Proceedings of Forum on Specification and Design Languages. 2011, 1–8

[14] Brandt J, Schneider K. Separate translation of synchronous programs to guarded actions. Internal Report 382/11, Kaiserslautern: University of Kaiserslautern, 2011

[15] Brandt J, Schneider K, Shukla S K. Translating concurrent action oriented specifications to synchronous guarded actions. In: Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. 2010, 47–56

[16] Edwards S A, Tardieu O. SHIM: a deterministic model for heterogeneous embedded systems. IEEE Transactions on Very Large Scale Integration Systems, 2006, 14(8): 854–867

[17] Brandt J, Gemunde M, Schneider K, Shukla A K, Talpin J P. Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Design Automation for Embedded Systems, 2014, 18: 63–97

[18] ESPRIT project: safety critical embedded systems SACRES. The declarative code DC+, version 1.4. Technical Report, 1997

[19] 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

[20] Yang Z B, Bodeveix J P, Filali M, Hu K, Zhao Y W, Ma D F. Towards a verified compiler prototype for the synchronous language SIGNAL. Frontiers of Computer Science, 2016, 10(1): 37–53

[21] RTCA/DO-178B. Software considerations in airborne systems and equipment certification. RTCA Inc., 1992

[22] RTCA/DO-178C. Software considerations in airborne systems and equipment certification. RTCA Inc., 2011

[23] Pouzet M. Lucid Synchrone, version 3: tutorial and reference manual. Université Paris-Sud, LRI, 2016

[24] Forget J. A synchronous language for critical embedded systems with multiple real-time constraints. Dissertation for the Doctoral Degree. Toulouse: Université de Toulouse, 2009

[25] Castéran P, Bertot Y. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. New York: Springer, 2004

[26] Pagano B, Andrieu O, Moniot T, Canou B, Chailloux E, Wang P, Manoury P, Colaço J L. Using objective Caml to develop safety-critical embedded tools in a certification framework. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. 2009, 215–220

[27] Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. The ASTRÉE analyzer. In: Proceedings of the 14th European Symposium on Programming. 2005, 21–30

[28] Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual, 2010

[29] Gamatié A. Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification. Springer Science and Business Media, 2009

[30] Le Guernic P, Gautier T. Data-Flow to von Neumann: the SIGNAL approach. Advanced Topics in Data-Flow Computing, 1991, 413–438

[31] Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits, Systems, and Computers, 2003, 12(3): 261–303

[32] Pnueli A, Siegel M, Singerman E. Translation validation. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 1998, 151–166

[33] Talpin J P, Brandt J, Gemunde M, Schneider K, Shukla S K. Constructive polychronous systems. In: Proceedings of International Symposium on Logical Foundations of Computer Science. 2013, 335–349

[34] Brandt J, Gemunde M, Schneider K, Shukla S K, Talpin J P. Embedding polychrony into synchrony. IEEE Transactions on Software Engineering, 2013, 39(7): 917–929

[35] 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

[36] Amagbegnon T, Besnard L, Le Guernic P. Arborescent canonical form of boolean expressions. Dissertation for the Doctoral Degree. 1994

[37] Jose B A, Gamatié A, Ouy J, Shukla S K. SMT based false causal loop detection during code synthesis from polychronous specifications. In: Proceedings of the 9th IEEE/ACMInternational Conference on Formal Methods and Models for Codesign (MEMOCODE). 2011, 109–118

[38] Leroy X. Mechanized semantics for compiler verification. In: Proceedings of International Conference on Certified Programs and Proofs. 2012, 4–6

[39] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115

[40] Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83–94

[41] Necula G C. Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1997, 106–119

[42] Chen K, Sztipanovits J, Abdelwalhed S, Jackson E. Semantic anchoring with model transformations. In: Proceedings of European Conference on Model Driven Architecture-Foundations and Applications. 2005, 115–129

[43] Narayanan A, Karsai G. Using semantic anchoring to verify behavior preservation in graph transformations. Electronic Communications of the EASST, 2006, 4

[44] 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

[45] Talpin J P, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychronous equations. In: Proceedings of International Conference on Integrated Formal Methods. 2012, 113–127

RIGHTS & PERMISSIONS

2018 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature