|
|
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 |
|
|
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
|
|
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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|