微信服务号

微信订阅号

2025-5-16- 14
Home > Archive>Volume 28, Issue 5, 2017 >1233-1246. DOI:10.13328/j.cnki.jos.005213
PDF HTML XML Export Cite reminder
Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (90818019, 61462086); National Science and Technology Major Project (MJ-2015-D-066); Sino-European Laboratory of Informatics, Automation and Applied Mathematics Grants

  • Article
    • | |
  • Metrics
    • |
  • Reference [35]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Synchronous data-flow languages, such as Lustre, have been widely used in safety-critical industrial areas, such as airplanes, high-speed railways, and nuclear power plants. The safety of development tools themselves for these types of applications is highly required. In better solving the "miscompilation" problem, very successful progress has been made recently to implement the construction and verification of a conventional imperative language compiler, such as the CompCert C compiler, by using reliable-by-construction proof assistants. L2C is a trustworthy compiler developed based on such an approach, with an extended Lustre language as its source, and Clight, a C subset used in ComperCert, as its target. L2C is an industry-level synchronous data-flow language compiler developed by using the same technique. The paper focuses on the key translations of L2C and the main issues and experience in its design and implementation.

    Reference
    [1] Caspi P, Pilaud D, Halbwachs N, Plaice J. Lustre: A declarative language for programming synchronous systems. In: Proc. of the 14th ACM Symp. on Principles of Programming Languages (POPL'87). Munchen, 1987. 178-188.
    [2] Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous dataflow programming language LUSTRE. Proc. of the IEEE, 1991,79(9):1305-1320. [doi: 10.1109/5.97300]
    [3] Guernic M, Gautier T, Maire C. Programming real time applications with signal. Proc. of the IEEE, 1991,79(9):1321-1336. [doi: 10.1109/5.97301]
    [4] http://www.esterel-technologies.com/products/scade-suite/
    [5] McCarthy J, Painter J. Correctness of a compiler for arithmetical expressions. In: Proc. of the Symp. in Applied Mathematics Aspects of Computer Science, Vol. 19. AMS, 1967. 33-41.
    [6] Milner R, Weyhrauch R. Proving compiler correctness in a mechanized logic. In: Proc. of the 7th Annual Machine Intelligence Workshop, Vol.7. Edinburgh University Press, 1972. 51-72.
    [7] Dave MA. Compiler verification: A bibliography. ACM SIGSOFT Software Engineering Notes, 2003,28(6):2. [doi: 10.1145/96622 1.966235]
    [8] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009,52(7):107-115. [doi: 10.1145/1538788.15 38814]
    [9] Coq Development Team. The Coq Reference Manual. 2016. http://coq.inria.fr/
    [10] Bertot Y, Castéran P. Interactive theorem proving and program development—Coq'Art: The calculus of inductive constructions. In: Proc. of the EATCS on Texts in Theoretical Computer Science. Springer-Verlag, 2004. [doi: 10.1007/978-3-662-07964-5]
    [11] Morrisett G. Technical perspective: A compiler's story. Communications of the ACM, 2009,52(7):106. [doi: 10.1145/1538788.1538 813]
    [12] Yang XJ, Chen Y, Eide E, Regehr J. Finding and understanding bugs in C compilers. In: Proc. of the 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2011). 2011. 283-294. [doi: 10.1145/1993498.1993532]
    [13] 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. [doi: 10.1145/1111320.1111042]
    [14] Pnueli A, Siegel M, Singerman E. Translation validation. In: Proc. of the TACAS'98. LNCS 1384, 1998. 151-166. [doi: 10.1007/ BFb0054170]
    [15] Pnueli A, Shtrichman O, Siegel M. Translation validation for synchronous languages. In: Proc. of the ICALP'98. LNCS 1443, 1998. 235-246. [doi: 10.1007/BFb0055057]
    [16] Tristan J-B, Leroy X. Verified validation of lazy code motion. In: Proc. of the PLDI. 2009. 316-326. [doi: 10.1145/1542476.15425 12]
    [17] Tristan J-B, Leroy X. A simple, verified validator for software pipelining. In: Proc. of the POPL. 2010. 83-92. [doi: 10.1145/17062 99.1706311]
    [18] Shi G, Wang SY, Dong Y, Ji ZY, Gan YK, Zhang LB, Zhang YC, Wang L, Yang F. Construction for the trustworthy compiler of a synchronous data-flow language. Ruan Jian Xue Bao/Journal of Software, 2014,25(2):341-356 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4542.htm [doi: 10.13328/j.cnki.jos.004542]
    [19] http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6
    [20] Chlipala A. A certified type-preserving compiler from lambda calculus to assembly language. In: Proc. of the 2007 ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2007. 54-65. [doi: 10.1145/1273442.1250742]
    [21] Klein G, Nipkow T. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. on Programming Languages and Systems, 2006,28(4):619-695. [doi: 10.1145/1146809.1146811]
    [22] Van Ngo C, Talpin JP, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychronous equations. In: Latella D, Treharne H, eds. Proc. of the IFM 2012. LNCS 7321, 2012. 113-127. [doi: 10.1007/978-3-642-30729-4_9]
    [23] Van Ngo C, Talpin JP, Gautier T, Le Guernic P. Translation validation for clock transformations in a synchronous compiler. In: Proc. of the 18th Int'l Conf. on Fundamental Approaches to Software Engineering (FASE-ETAPS 2015). LNCS 9039, 2015. 171-185. [doi: 10.1007/978-3-662-46675-9_12]
    [24] Biernacki D, Colaco JL, Hamon G, Pouzet M. Clock-Directed modular code generation of synchronous data-flow languages. In: Proc. of the ACM Int'l Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES). Tucson, 2008. [doi: 10.1145/ 1375657.1375674]
    [25] Auger C, Pouzet M. A formalization and proof of a modular lustre compiler. Technical Report, LRI, 2012. http://www.di.ens.fr/ ~pouzet/cours/mpri/cours4/scp12
    [26] Auger C. Compilation certifiee de SCADE/LUSTRE [Ph.D. Thesis]. Universite de ParisSud, 2013.
    [27] Gu RH, Koenig J, Ramanamandro T, Shao Z, Wu XN, Weng SC, Zhang HZ, Guo Y. Deep specifications and certified abstraction layers. In: Proc. of the POPL 2015. Mumbai: ACM Press, 2015. 593-608. [doi: 10.1145/2676726.2676975]
    [28] Jourdan J-H, Laporte V, Blazy S, Leroy X, Pichardie D. A formally-verified c static analyzer. In: Proc. of the POPL2015. Mumbai: ACM Press, 2015. 247-259. [doi: 10.1145/2676726.2676966]
    [29] Blazy S, Leroy X. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009,43(3): 263-288. [doi: 10.1007/s10817-009-9148-3]
    [30] Leroy X, Blazy S. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of. Automated Reasoning, 2008,41(1):1-31. [doi: 10.1007/s10817-008-9099-0]
    [31] Zhu XY, Yan RJ, Gu YL, Zhang J, Zhang WH, Zhang GQ. Static optimal scheduling for synchronous data flow graphs with model checking. In: Proc. of the 20th Int'l Symp. on Formal Methods (FM 2015). LNCS 9109, At Oslo, 2015. 551-569. [doi: 10.1007/ 978-3-319-19249-9_34]
    [32] Yang ZB, Zhao YW, Huang ZQ, Hu K, Ma DF, Bodeveix JP, Filali M. Time-Predicatable multi-threaded code generation with synchronous languages. Ruan Jian Xue Bao/Journal of Software, 2016,27(3):611-632 (in Chinese with English abstract). http:// www.jos.org.cn/1000-9825/4984.htm [doi: 10.13328/j.cnki.jos.004984]
    附中文参考文献:
    [18] 石刚,王生原,董渊,嵇智源,甘元科,张玲波,张煜承,王蕾,杨斐.同步数据流语言可信编译器的构造,软件学报,2014,25(2):341-356. http://www.jos.org.cn/1000-9825/4542.htm [doi: 10.13328/j.cnki.jos.004542]
    [32] 杨志斌,赵永望,黄志球,胡凯,马殿富,Bodeveix JP,Filali M.基于同步语言的时间可预测多线程代码生成方法,软件学报,2016, 27(3):611-632. http://www.jos.org.cn/1000-9825/4984.htm [doi: 10.13328/j.cnki.jos.004984]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

尚书,甘元科,石刚,王生原,董渊.可信编译器L2C的核心翻译步骤及其设计与实现.软件学报,2017,28(5):1233-1246

Copy
Share
Article Metrics
  • Abstract:4368
  • PDF: 6992
  • HTML: 3235
  • Cited by: 0
History
  • Received:July 15,2016
  • Revised:September 25,2016
  • Online: January 22,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044947Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063