Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2013, Vol. 7 Issue (5) : 598-616    https://doi.org/10.1007/s11704-013-3910-8
REVIEW ARTICLE
Formal verification of synchronous data-flow program transformations toward certified compilers
Van Chan NGO1(), Jean-Pierre TALPIN1, Thierry GAUTIER1, Paul Le GUERNIC1, Loïc BESNARD2
1. INRIA Rennes-Bretagne Atlantique, Rennes 35042, France
2. IRISA/CNRS, Rennes 35042, France
 Download: PDF(0 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract

Translation validation was invented in the 90’s by Pnueli et al. as a technique to formally verify the correctness of code generators. Rather than certifying the code generator or exhaustively qualifying it, translation validators attempt to verify that program transformations preserve semantics. In this work, we adopt this approach to formally verify that the clock semantics and data dependence are preserved during the compilation of the Signal compiler. Translation validation is implemented for every compilation phase from the initial phase until the latest phase where the executable code is generated, by proving the transformation in each phase of the compiler preserves the semantics. We represent the clock semantics, the data dependence of a program and its transformed counterpart as first-order formulas which are called clock models and synchronous dependence graphs (SDGs), respectively. We then introduce clock refinement and dependence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock models and SDGs, respectively. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.

Keywords formal verification      translation validation      certified compiler      multi-clocked synchronous programs      embedded systems     
Corresponding Author(s): Van Chan NGO   
Issue Date: 01 October 2013
 Cite this article:   
Van Chan NGO,Jean-Pierre TALPIN,Thierry GAUTIER, et al. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front. Comput. Sci., 2013, 7(5): 598-616.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-3910-8
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I5/598
1 G Berry .The foundations of Esterel. In: Proof, Language, and Interaction. 2000, 425−454
2 N Halbwachs . A synchronous language at work: the story of lustre. In: Proceedings of the 3rd ACM and IEEE International Conference on Formal Methods and Models for Co-Design. 2005, 3−11
3 A Gamati . Designing embedded systems with the Signal programming language: synchronous, reactive specification. Springer Publishing Company, Incorporated, 2009
4 Inria. The coq proof assitant.
5 Do-178c.
6 A Pnueli , M Siegel , E Singerman . Translation validation. Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1998_151−166
https://doi.org/10.1007/BFb0054170
7 A Pnueli , O Shtrichman , M Siegel . Translation validation: from Signal to C. Lecture Notes in Computer Science, 1999,1710: 231−255
8 Inria. The compcert project.
9 G C Necula . Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83−94
https://doi.org/10.1145/358438.349314
10 J B Tristan , P Govereau , G Morrisett . Evaluating value-graph translation validation for LLVM. ACM Sigplan Notices, 2011, 295−305
https://doi.org/10.1145/1993316.1993533
11 B Dutertre , L Moura de . Yices Sat-solver.
12 Espresso, Polychrony toolset.
13 A Benveniste , P Le Guernic . Hybrid dynamical systems theory and the signal language. IEEE Transactions on Automatic Control, 1990, 35(5): 535−546
https://doi.org/10.1109/9.53519
14 T Gautier , P Le Guernic , L Besnard . Signal: a declarative language for synchronous programming of real-time systems. Lecture Notes in Computer Science, 1987, 274: 257−277
https://doi.org/10.1007/3-540-18317-5_15
15 S Abramsky , A Jung S Domain theory. Abramsky , D M Gabbay , T S E Maibaum , ed(s). Handbook of Logic in Computer Science: Volume 3: Semantic Structures. Oxford:Clarendon Press, 1994, 1−168
16 G Kahn . The semantics of a simple language for parallel programming. IFIP Congress, 1974, 471−475
17 L Besnard , T Gautier , P Le Guernic , J P Talpin . Compilation of polychromous data flow equations. Synthesis of Embedded Software, Springer, 2010, 1−40
https://doi.org/10.1007/978-1-4419-6400-7_1
18 W Ackermann . Solvable Cases of the Decision Problem. Vol. 12. North-Holland Pub. Co., 1954
19 P Le Guernic , T Gautier . Data-flow to von neumann: the signal approach. Rapports de recherche- INRIA
20 A Gamatié , L Gonnord . Static analysis of synchronous programs in signal for effcient design of multi-clocked embedded systems. ACM Sigplan Notices, 2011, 46(5): 71−80
https://doi.org/10.1145/2016603.1967688
21 F E Allen . Control flow analysis. ACM SIGPLAN Notices, 1970, 1−19
https://doi.org/10.1145/390013.808479
22 A Biere , M Heule , H Maarenv , T Walsh . Handbook of Satisfiability Frontiers in Artificial Intelligence and Applications, vol. 185, 2009
23 O Ma_eïs , P Le Guernic . Combining dependability with architectural adaptability by means of the signal language. Lecture Notes in Computer Science, 1993(724): 99−110
24 C Barrett , S Ranise , A Stump , C Tinelli . The satisfiability modulo theories library (SMT-LIB). , 2008
25
26 R E Bryant . Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8): 677−691
https://doi.org/10.1109/TC.1986.1676819
27 X Leroy . Formal certification of a compiler back-end or: programming a compiler with a proof assistant. ACM SIGPLAN Notices, 2006, 41(1): 42−54
https://doi.org/10.1145/1111320.1111042
28 J B Tristan , X Leroy . A simple, verified validator for software pipelining. ACM SIGPLAN Notices, 2010, 45(1): 83−92
https://doi.org/10.1145/1707801.1706311
29 D Biernacki , J L Colaço , G Hamon , M Pouzet . Clock-directed modular code generation for synchronous data-flow languages. ACM SIGPLAN Notices, 2008, 43(7): 121−130
https://doi.org/10.1145/1379023.1375674
30 V C Ngo , J P Talpin , T Gautier , P Le Guernic , L Besnard . 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
[1] Shahbaz ALI, Hailong SUN, Yongwang ZHAO. Model learning: a survey of foundations, tools and applications[J]. Front. Comput. Sci., 2021, 15(5): 155210-.
[2] Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[3] Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.
[4] Lu YANG, Chaochen ZHOU, Naijun ZHAN, Bican XIA, . Recent advances in program verification through computer algebra[J]. Front. Comput. Sci., 2010, 4(1): 1-16.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed