计算机科学 ›› 2019, Vol. 46 ›› Issue (5): 21-28.doi: 10.11896/j.issn.1002-137X.2019.05.003

• 综述 • 上一篇    下一篇

同步数据流语言可信编译器的研究进展

杨萍1, 王生原2   

  1. (北京语言大学信息科学学院 北京100083)1
    (清华大学计算机科学与技术系 北京100084)2
  • 收稿日期:2018-05-11 修回日期:2018-09-02 发布日期:2019-05-15
  • 作者简介:杨 萍 女,硕士,副教授,主要研究方向为程序语言与编译器、智能语言与技术,E-mail:yangp@blcu.edu.cn;王生原 男,副教授,CCF高级会员,主要研究方向为程序语言与编译技术、程序验证,E-mail:wwssyy@tsinghua.edu.cn(通信作者)。
  • 基金资助:
    国家民用飞机重大专项项目基金(MJ-2015-D-066),核高基重大专项(2017ZX01030-301-003)资助。

Survey on Trustworthy Compilers for Synchronous Data-flow Languages

YANG Ping1, WANG Sheng-yuan2   

  1. (School of Information Science,Beijing Language and Culture University,Beijing 100083,China)1
    (Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China)2
  • Received:2018-05-11 Revised:2018-09-02 Published:2019-05-15

摘要: 同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决“误编译”问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。

关键词: Lustre, Signal, 翻译确认, 经过验证的编译器, 同步数据流语言

Abstract: Synchronous data-flow languages,such as Lustre and Signal,have been widely used in safety-critical industrialareas,such as airplane,high-speed railways,nuclear power plants and so on.Hence,the safety of development tools themselves for such languages has been paid highly attention on.The trustworthy compiler from a synchronous data-flow language to a sequential imperative language is typically one of such kinds of tools,such as Scade.There are two ways to implement a trustworthy compiler:the traditional method,for instance,plenty of testing and strict process ma-nagement;the formal method,for example,formal verification for the compiler itself,and translation validation,etc.The formal method has been paid much attention in recent years,because it has been widely studied as the critical approach in the construction and verification of a trustworthy compiler,and it is expected to have the opportunity in solving the “miscompilation” problem to the utmost extent.After the introduction of formal methods to construct and verify a trustworthy compiler,the survey and analysis of the research work and the current status for the trustworthy compilers of synchronous data-flow language were specially focused on in this paper.

Key words: Certified compilers, Lustre, Signal, Synchronous data-flow languages, Translation validation

中图分类号: 

  • TP314
[1]KNIGHT J C.Safety critical systems:challenges and directions[C]∥Proceedings of the 24th International Conference on Software Engineering(ICSE 2002).2002:547-550.
[2]LEROY X.Verified squared:does critical software deserve verified tools?[J].ACM SIGPLAN Notices,2011,46(1):1-2.
[3]Scade-suite home[EB/OL].http://www.esterel-technologies.
com/products/scade-suite.
[4]CASPI P,PILAUD D,HALBWACHS N,et al.Lustre:a decla-rative language for programming synchronous systems[C]∥14th ACM Symposium on Principles of Programming Languages(POPL’87).Munchen,1987.
[5]HALBWACHS N,CASPI P,RAYMOND P,et al.The synchronous dataflow programming language LUSTRE[J].Proceedings of the IEEE,1991,79(9):1305-1320.
[6]HALBWACHS N.Synchronous programming of reactive sys-tems,a tutorial and commented bibliography[M]∥Tenth International Conference on Computer-Aided Verification,CAV’98.Berlin:Springer Verlag,1998.
[7]HALBWACHS N.A Synchronous Language at Work:the Story of Lustre[C]∥Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and models for Co-Design,MEMOCODE’05.IEEE Computer Society,Washington,DC,USA,2005.
[8]BENVENISTE A,CASPI P,EDWARDS S A,et al.The Syn-chronous Languages Twelve Years Later[J].Proceedings of the IEEE,2003,91(1):64-83.
[9]MILNER R.Calculi for synchrony and asynchrony[J].Theoretical Computer Science,1983,25(3):267-310.
[10]BERRY G,GONTHIER G.The Esterel synchronous programming language:Design,semantics,implementation[J].Science of Computer Programming,1992,19(2):87-152.
[11]BERRY G,The foundations of ESTEREL[M]∥proof,language and interaction:essays in honour of Robin Milner.Cambridge:MIT Press,2000:425-454.
[12]GUERNIC P L,GAUTIER T,BORGNE M L,et al.Programming real time applications with SIGNAL[J].Proceedings of the IEEE,1991,79(9):1321-1336.
[13]LE GUERNIC P,TALPIN J P,LE LANN J C.Polychrony for system design[J].Journal for Circuits,Systems and Computers,2002,12(3):261-304.
[14]LUCID SYNCHRONE home[EB/OL].http://www.di.ens.
fr/~pouzet/lucid-synchrone.
[15]WADGE W W,ASHCROFT E A.LUCID,the dataflow pro-gramming language[M].Academic Press Professional,San Diego,CA,USA,1985.
[16]ASHCROFT E A,WADGE W W.Lucid,a non procedural language with iteration[J].Communications of the ACM,1977,20(7):519-526.
[17]SCHNEIDER K.The synchronous programming languageQuartz:Internal Report 375[R].Department of Computer Scien-ce,University of Kaiserslautern,Kaiserslautern,Germany,2009.
[18]MARANINCHI F.the ARGOS language:graphical representation of automata and description of reactive systems[C]∥IEEE Workshop on Visual Languages.Kobe,Japan,1991.
[19]HAREL D,STATECHARTS A.A visual formalism for complex systems[J].Science of Computer Programming,1987,8(3):231-274.
[20]ANDRÉC.Computing SyncCharts reactions[M]∥Synchronous Languages,Applications,and Programming (SLAP’03),Electronic Notes in Theoretical Computer Science.Porto,Portugal,2003:3-19.
[21]DAVID R.Grafcet:A Powerful Tool[J].IEEE Transactions on Control Systems Technology,1995,3(3):253-268.
[22]GCC.the GNU Compiler Collection[EB/OL].http://gcc.gnu.org.
[23]The Plum Hall Validation Suite for CTM [EB/OL].http://www.plumhall.com/stec.html.
[24]Lustre V6[EB/OL].http://www-verimag.imag.fr/Lustre-V6.html.
[25]YANG X J,CHEN Y,EIDE E,et al.Finding and understanding bugs in C compilers[C]∥Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011).2011:283-294.
[26]http://www.commoncriteriaportal.org/cc.
[27]Summary of Difference Between DO-178B and DO-178C[EB/OL].http://faaconsultants.com/html/do-178c.html.
[28]LEROY X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115.
[29]MORRISETT G.Technical Perspective:A Compiler’s Story[J].Communications of the ACM,2009,52(7):106-106.
[30]LEROY X.Formal certification of a compiler back-end or:programming a compiler with a proof assistant[J].Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages,2006,41(1):42-54.
[31]PNUELI A,SIEGEL M,SINGERMAN E.Translation Validation[C]∥Proceedings of TACAS’98.1998:151-166.
[32]NECULA G C,LEE P.The design and implementation of a certifying compiler[C]∥Proc.Conf.Programming Language Design and Implementation.1998:333-344.
[33]TRISTAN J B,PAUL G,GREG M.Forthcoming.Evaluatingvalue-graph translation validation for LLVM[C]∥Proceedings of the 32nd ACM SIGPLAN Conference on Programming and Language Design Implementation.2011:295-305.
[34]KANADE A,SANYAL A,KHEDKER U.A PVS based framework for validating compiler optimizations[C]∥4th Software Engineering and Formal Methods.IEEE Computer Society,2006:108-117.
[35]NECULA G C.Translation validation for an optimizing compiler[M]∥Programming Language Design and Implementation 2000.ACM Press,2000:83-95.
[36]TRISTAN J B,LEROY X.Verified validation of lazy code motion[C]∥PLDI.2009:316-326.
[37]TRISTAN J B,LEROY X.A simple,verified validator for software pipelining[C]∥POPL.2010:83-92.
[38]TRISTAN J B,LEROY X.Formal verification of translationvalidators:A case study on instruction scheduling optimizations[C]∥35th symposium Principles of Programming Languages.ACM Press,2008:17-27.
[39]RYABTSEV M,STRICHMAN O.Translation validation:From simulink to c∥Proceedings of the 21st International Conference on Computer Aided Verification(CAV 2009).Berlin:Springer,2009:696-701.
[40]GIMENEZ E,LEDINOT E.Certication de SCADE V3,Rapport final du project GENIE II,Verilog SA (Janvier 2000).
[41]PAULIN C,POUZET M.Certified compilation of scade/lustre[EB/OL].http://www.lri.fr/paulin/lustreincoq.pdf,2006.
[42]BERTAILS A,BIERNACKI D,PAULIN C,et al.A certified compiler for the synchronous language Lustre[EB/OL].http://users.dimi.uniud.it/types07/slides/Bertails.pdf.
[43]BIERNACKI D,COLACO J L,HAMON G,et al.Clock-directed Modular Code Generation of Synchronous Data-flow Languages[C]∥ACM International Conference on Languages,Compilers,and Tools for Embedded Systems(LCTES).Tucson,Arizona,2008.
[44]BIERNACKI D,COLACO J L,POUZET M.Clock-directedModular Code Generation from Synchronous Block Diagrams[C]∥Workshop on Automatic Program Generation for Embedded Systems(APGES 2007).Salzburg,Austria,2007.
[45]AUGER C.Compilation Certifiée de SCADE/LUSTRE[D].
Université Paris Sud,2013.
[46]AUGER C,COLAÇOB J L,HAMON G,et al.A Formalization and Proof of a Modular Lustre Compiler[EB/OL].http://www.di.ens.fr/~pouzet/cours/mpri/cours4/scp12.pdf.
[47]BOURKE T,BRUN L,DAGAND P é,et al.A Formally Verified Compiler for Lustre[C]∥Proceedings of the Programming Language Design and Implementation.2017:586-601.
[48]SHI G,WANG S Y,DONG Y,et al.Construction for the Trustworthy Compiler of a Synchronous Data-Flow Language[J].Journal of Software,2014,25(2):341-356.(in Chinese)石刚,王生原,董渊.同步数据流语言可信编译器的构造[J].软件学报,2014,25(2):341-356.
[49]SHANG S,GAN Y K,SHI G,et al.Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation[J].Journal of Software,2017,28(5):1233-1246.(in Chinese)尚书,甘元科,石刚,等.可信编译器L2C的核心翻译步骤及其设计与实现[J].软件学报,2017,28(5):1233-1246.
[50]Lustre V6 reference manual[EB/OL].http://www-verimag.
imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/doc/lv6-ref-man.pdf.
[51]Open L2C home[EB/OL].http://soft.cs.tsinghua.edu.cn:8000/.
[52]The Coq Development Team.The Coq Proof Assistant Refe-rence Manual Version V8.3[EB/OL].http://coq.inria.fr/.
[53]BERTOT Y,CASTÉRAN P.Interactive Theorem Proving and Program Development-Coq’Art:The Calculus of Inductive Constructions[M]∥Texts in Theoretical Computer Science.Sprin-ger Verlag,2004.
[54]BLAZY S,LEROY X.Mechanized semantics for the Clight subset of the C language[J].Journal of Automated Reasoning,2009,43(3):263-288.
[55]PNUELI A,SHTRICHMAN O,SIEGEL M.Translation validation for synchronous languages[C]∥Proceedings of ICALP’1998.Berlin:Springer,1998:235-246.
[56]PNUELI A,SIEGEL M,SHTRICHMAN O.The code validation tool(CVT)- automatic verification of a compilation process[J].Journal of Software Tools for Technology Transfer(STTT),1999,2(2):192-201.
[57]NGO V C,TALPI J P,GAUTIER T.Formal Translation validation for clock transformations in a synchronous compiler[C]∥International Conference on Fundamental Approaches to Software Engineering(ETAPS/FASE’15).Springer,2015.
[58]NGO V C,TALPIN J P,GAUTIER T,et al.Formal verification of synchronous data-flow program transformations toward certified compilers[J].Frontiers of Computer Science,2013,7(5):598-616.
[59]NGO V C,TALPI J P,GAUTIER T,et al.Formal Verification of Compiler Transformations on Polychronous Equations[M]∥IFM 2012.Berlin:Springer,2012:113-127.
[60]NGO V C,TALPI J P,GAUTIER T,et al.Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract)[C]∥International Workshop on Software and Compilers for Embedded Systems (SCOPES’15).ACM,2015:109-112.
[61]NGO V C,TALPI J P,GAUTIER T.Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler[C]∥International Conference on Formal Techniques for Distributed Objects,Components and Systems (FORTE’15).IFIP,2015:66-80.
[62]DUTERTRE B,DE MOURA L.Yices sat-solver[EB/OL].http://yices.csl.ri.com,2009.
[63] KAHN G.The semantics of a simple language for parallel programming[M]∥Information Processing 74 Congress.North-Holland Publishing Compmany,Amsterdam,1974.
[64]CASPI P,POUZET M.Synchronous Kahn networks[C]∥Proceedings of the first ACM SIGPLAN International Conference on Functional Programming (ICFP’96).Philadelphia,Pennsylvania,1996:226-238.
[65]COHEN A,DURANTON M,EISENBEIS M,et al.N-Sychronous Kahn Networks[C]∥33th ACM Symp.on Principles of Programming Languages (PoPL’06).Charleston,South Carolina,2006:180-193.
[66]PAULIN-MOHRING C.Kahn Networks in Coq[EB/OL].http://www.lri.fr/~paulin/KahnNetworks/library.pdf.
[67]PAULIN-MOHRING C.A constructive denotational semantics for Kahn networks in Coq[M]∥From Semantics to Computer Science.Essays in Honour of Gilles Kahn,2009:383-414.
[68]KAHN G.Elements of domain theory[EB/OL].http://coq.inria.fr/pylons/contribs/view/DomainTheory/trunk.
[69]CASPI P,POUZET M.A co-iterative characterization of syn-chronous stream functions.[J].Electronic Notes in Theoretical Computer Science,1998,11(4):1-21.
[70]BOULMÉ S,HAMON C.Certifying Synchrony for Free[C]∥International Conference on Logic for Programming,Artificial Intelligence and Reasoning (LPAR).La Havana,Cuba,Springer Verlag,2001.
[71]Lucid-Synchrone in Coq[EB/OL].http://www.di.ens.fr/~pouzet/lucid-synchrone/lucid_in_coq.
[72]COHEN A,DURANTON M,EISENBEIS C,et al.Synchronization of Periodic Clocks[C]∥ACM Conf.on Embedded Software (EMSOFT'05).Jersey City,New York,2005:339-342.
[73]COHEN A,MANDEL L,PLATEAU F,et al.Abstraction of Clocks in Synchronous Data-flow Systems[C]∥The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS).2008.
[74]DELAVAL G,GIRAULT A,POUZET M.A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs[C]∥ACM International Conference on Languages,Compilers,and Tools for Embedded Systems (LCTES).Tucson,Arizona,2008.
[75]SCHNEIDER K,BRANDT J,SCHUELE T.A Verified Compi-ler for Synchronous Programs with Local Declarations[J].Electronic Notes in Theoretical Computer Science,2006,153(4):71-97.
[76]HOL[EB/OL].http://www.cl.cam.ac.uk/research/hvg/HOL.
[77]ZHANG Y.Source code to unify nested clocks in a lustre-like language[EB/OL].https://github.com/yczhang89/unify-clock.
[78]SHI G,ZHANG Y C,SHANG S,et al.A Formally Verified Transformation to Unify Multiple Nested Clocks for a Lustre-like Language[J].Science China Information Sciences,2019,62(1):012801:1-012801:3.
[79]GAN Y K,ZHANG L B,SHI G,et al.A Verified Sequentializer for Synchronous Data-Flow Programs[J].Computer Applications and Software,2014,31(5):1-5.(in Chinese)甘元科,张玲波,石刚,等.同步数据流程序的可信排序[J].计算机应用与软件,2014,31(5):1-5.
[80]ZHANG L B,GAN Y K,SHI G,et al.A certified translation for eliminating temporal feature of a synchronize dataflow program[J].Computer Engineering and Design,2014,35(1):137-143.(in Chinese)张玲波,甘元科,石刚,等.同步数据流语言时态消去的可信翻译[J].计算机工程与设计,2014,35(1):137-143.
[81]LIU Y,YANG F,SHI G,et al.Brief Overview of Translation Validation Method in Trusted Compiler Construction[J].Computer Science,2014,41(S1):334-338.(in Chinese)刘洋,杨斐,石刚,等.可信编译器构造的翻译确认方法简述[J].计算机科学,2014,41(S1):334-338.
[82]SHI G,GAN Y K,SHANG S,et al.A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs[C]∥Proceedings-2017 IEEE/ACM 39th International Conference on Software Engineering Companion(ICSE-C).2017:109-111.
[83]LIU Y,GAN Y K,WANG S Y,et al.Trustworthy Translation for Eliminating High-Order Operation of a Synchronous Dataflow Language[J].Journal of Software,2015,26(2):332-347.(in Chinese)刘洋,甘元科,王生原,等.同步数据流语言高阶运算消去的可信翻译[J].软件学报,2015,26(2):332-347.
[1] 李凌, 李璜华, 王生原.
在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程
Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design
计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173
[2] 钱迎进,李永刚,汪毅,周琳琦.
Lustre文件系统元数据服务恢复机制的改进
Improvement of Recovery Mechanism for Lustre Metadata Service
计算机科学, 2015, 42(9): 177-182. https://doi.org/10.11896/j.issn.1002-137X.2015.09.034
[3] 程耀东,汪璐,黄秋兰,陈刚.
高能物理计算环境中存储系统的设计与优化
Design and Optimization of Storage System in HEP Computing Environment
计算机科学, 2015, 42(1): 54-58. https://doi.org/10.11896/j.issn.1002-137X.2015.01.012
[4] 刘洋,杨斐,石刚,闫鑫,王生原,董渊.
可信编译器构造的翻译确认方法简述
Brief Overview of Translation Validation Method in Trusted Compiler Construction
计算机科学, 2014, 41(Z6): 334-338.
[5] 王蕾,石刚,董渊,白晓颖,王生原.
一个C语言安全子集的可信编译器
Trusted Compiler for Safe Subset of C Language
计算机科学, 2013, 40(9): 30-34.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!