×

Formal verification of synchronous data-flow program transformations toward certified compilers. (English) Zbl 1425.68061

Summary: 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.

MSC:

68N20 Theory of compilers and interpreters
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Berry, G., The foundations of Esterel, 425-454 (2000)
[2] Halbwachs, N., A synchronous language at work: the story of lustre, 3-11 (2005)
[3] Gamati A. Designing embedded systems with the Signal programming language: synchronous, reactive specification. Springer Publishing Company, Incorporated, 2009
[4] Inria. The coq proof assitant. http://coq.inria.fr
[5] Do-178c. http://rtca.org
[6] Pnueli, A.; Siegel, M.; Singerman, E., Translation validation (1998)
[7] Pnueli A, Shtrichman O, Siegel M. Translation validation: from Signal to C. Lecture Notes in Computer Science, 1999,1710: 231-255 · doi:10.1007/3-540-48092-7_11
[8] Inria. The compcert project. http://compcert.inria.fr
[9] Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83-94 · doi:10.1145/358438.349314
[10] Tristan, J. B.; Govereau, P.; Morrisett, G., Evaluating value-graph translation validation for LLVM, 295-305 (2011)
[11] Dutertre B, Moura de L. Yices Sat-solver. http://yices.csl.ri.com
[12] Espresso, Polychrony toolset. http://www.irisa.fr/espresso/Polychrony
[13] Benveniste A, Le Guernic P. Hybrid dynamical systems theory and the signal language. IEEE Transactions on Automatic Control, 1990, 35(5): 535-546 · Zbl 0709.68012 · doi:10.1109/9.53519
[14] Gautier T, Le Guernic P, Besnard L. Signal: a declarative language for synchronous programming of real-time systems. Lecture Notes in Computer Science, 1987, 274: 257-277 · doi:10.1007/3-540-18317-5_15
[15] Abramsky, S.; Jung, A.; Abramsky, S. (ed.); Gabbay, D. M (ed.); Maibaum, T. S E. (ed.), Domain theory, 1-168 (1994), Oxford
[16] Kahn, G., The semantics of a simple language for parallel programming, 471-475 (1974)
[17] Besnard, L.; Gautier, T.; Guernic, P.; Talpin, J. P., Compilation of polychromous data flow equations, 1-40 (2010) · doi:10.1007/978-1-4419-6400-7_1
[18] Ackermann W. Solvable Cases of the Decision Problem. Vol. 12. North-Holland Pub. Co., 1954 · Zbl 0056.24505
[19] Le Guernic P, Gautier T. Data-flow to von neumann: the signal approach. Rapports de recherche-INRIA · Zbl 0624.68012
[20] Gamatié A, Gonnord L. Static analysis of synchronous programs in signal for effcient design of multi-clocked embedded systems. ACM Sigplan Notices, 2011, 46(5): 71-80 · doi:10.1145/2016603.1967688
[21] Allen, F. E., Control flow analysis, 1-19 (1970)
[22] Biere A, Heule M, Maaren v H, Walsh T. Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, 2009 · Zbl 1183.68568
[23] Ma-eïs, O.; Guernic, P., Combining dependability with architectural adaptability by means of the signal language, 99-110 (1993)
[24] Barrett C, Ranise S, Stump A, Tinelli C. The satisfiability modulo theories library (SMT-LIB). http://www.SMT-LIB.org, 2008
[25] http://www.smtcomp.org/2009
[26] Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8): 677-691 · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819
[27] Leroy X. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. ACM SIGPLAN Notices, 2006, 41(1): 42-54 · Zbl 1369.68124 · doi:10.1145/1111320.1111042
[28] Tristan J B, Leroy X. A simple, verified validator for software pipelining. ACM SIGPLAN Notices, 2010, 45(1):83-92 · Zbl 1312.68069 · doi:10.1145/1707801.1706311
[29] Biernacki D, Colaço J L, Hamon G, Pouzet M. Clock-directed modular code generation for synchronous data-flow languages. ACM SIGPLAN Notices, 2008, 43(7): 121-130 · doi:10.1145/1379023.1375674
[30] 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 · doi:10.1007/978-3-642-30729-4_9
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.