股票推荐怎么做网站,云浮建设网站,晋城哪里有做网站的,北京计算机培训机构排名前十摘要
同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用#xff0c;因此与这类语言相关的开发工具本身的安全性问题受到高度关注.同步数据流语言到串行命令式语言的代码生成工具是此类工具的典型代表(如Scade)。构造代码生成工具的途径可…
摘要
同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用因此与这类语言相关的开发工具本身的安全性问题受到高度关注.同步数据流语言到串行命令式语言的代码生成工具是此类工具的典型代表(如Scade)。构造代码生成工具的途径可分为两大类一类是传统的方法例如通过大量测试和严格的过程管理等手段来实现另一类是通过形式化方法例如直接对编译器本身进行形式化证明采用翻译确认的方法等。近年来形式化方法作为构造和验证代码生成工具的关键途径而得到广泛的重视有望最大限度地解决“误编译”问题因而成为新的研究热点。文章在介绍代码生成工具的形式化构造和验证方法的基础上特别聚焦于同步数据流语言代码生成工具的相关研究工作对其现状进行综述和分析。
1引言
计算机技术日益广泛地应用于航空航天、高速铁路、核电能源和医疗卫生等领域的安全关键系统Safety-CriticalSys-tem,SCS中。SCS一旦失效将给人类的生命财产、社会生产和生活环境带来巨大的破坏。在现代计算机技术的发展中相比软件来说硬件方面的安全性保障技术更加成熟人为因素导致硬件故障的概率相对较小。虽然人们一直关注于软件安全性问题并积累了大量研究成果和实践经验但软件方面的安全保障目前仍旧是计算机系统安全性中的薄弱环节。如何为安全关键系统构造一个基础的安全软件环境是需要解决的首要问题尤其是对操作系统、编译器等基础软件。本文将针对安全可信的编译器进行介绍。 所谓安全可信的编译器就是要保证编译器做正确的事情保证它能将符合源语言规范的程序正确翻译到目标语言程序。这里“正确翻译”主要指功能方面通常情况下是指源语言到目标语言的语义保持关系通常被刻画为一种反向的行为模拟等价关系不能实现“正确翻译”的编译器则一定存在某种程度的“误编译”错误。 作为用于产生代码的工具编译器的实现和维护自然经过了“精雕玉琢”同时又“随时随地”经受着无数应用程序的“考验”因此编译器的正确性问题容易被人们忽视。但了解实际情况的人都知道编译器的“误编译”问题是司空见惯、习以为常之事。在许多领域中由于“误编译”一般不会引发本质的问题又是小概率事件因此人们往往也忽视了“误编译”所带来的影响。然而对于安全攸关系统而言则必须考虑编译器引入的错误否则在源程序级的高成本验证工作可能在目标程序级失效。实际上在航空领域的RTCADO-178B/C类标准中编译器属于需要鉴定的工具类软件,需要按照机载软件的要求同等对待。 图1摘自X。Leroy在POPL^2011的特邀报告⑵描述了安全关键的嵌入式控制领域中典型的应用程序开发流程从高级算法描述语言或建模语言所描述的安全级应用程序生成行为等价的C代码后者接着被翻译成可执行的目标代码。图1中Simulink是面向建模语言MatLab的著名工具Scade是基于同步数据流语言Lustre的建模与开发工具。如图1所示在对安全关键系统进行验证和确认VV时不能不考虑编译器可能引入的错误。另外更值得关注的是若代码生成器或编译器不可信针对高级算法描述语言或建模语言源程序模型进行的有关安全性方面的各种努力模型检查、正确性证明、静态分析及模拟仿真等则会付之东流。因此除了要保障应用程序本身的安全性之外还需要有安全可信的编译器或代码生成器。 图1编译器代码生成器带来安全隐患的流程
本文将在介绍代码生成工具的形式化构造和验证方法的基础上特别聚焦于同步数据流语言代码生成工具的相关研究工作及其发展现状。同步数据流语言如Lustre,Signal近年来在安全关键领域得到了广泛应用比如Scade工具将一种扩展的Lustre语言翻译成C语言。在实际应用中通常会将诸如同步数据流语言之类的高级算法描述语言翻译成常规的串行命令式语言通常为C语言如图1的上半部分。同步数据流语言与串行命令式语言之间有很大的语义差距正如X。Leroy所言构造这样的代码生成工具或可信代码生成器是一项很有价值且富有挑战性的工作。 本文第2节先对同步数据流语言进行简要介绍第3节分析并讨论当前实现代码生成工具的主要途径第4节侧重对同步数据流语言到串行命令式语言通常为C语言代码生成工具的典型工作和发展情况进行综述最后有针对性地进行小结。
2同步数据流语言
传统的常规语言如C语言一直以来都是安全关键领域中使用最为普遍的开发语言。人们为安全有效地使用C语言下了很大功夫积累了非常丰富的经验。尽管人们通过各种办法来使得基于C语言的系统开发更加安全高效但毕竟C语言程序层次较低不易使人们聚焦于问题本身开发效率受到很大影响并且也难于验证。因此基于模型/模型驱动的开发逐步兴起并成为业界主流由模型自动生成的代码C代码为主已占据主导地位比较著名的建模语言/工具有Simulink和Scade等。 有一类建模语言被称为同步语言特别适合于实时控制系统的开发。所有同步语言均遵循同步假设synchronyhypothesis即每个周期内的计算从输入值得到输出值都是瞬间完成的同步语言的语义被要求具有确定性。同步假设以及确定性可以极大地简化实时系统的验证。另外同步语言通常有严格且可靠的数学定义对于同步范型有友好的工程设计方法因此它在实时嵌入式应用的建模、规范描述、验证以及实现等各个层面都已成为重要的技术选项。20世纪80年代人们就开始了同步范型的理论研究工作随即又出现了许多基于同步假设的语言并且这些语言都得到了广泛的应用。Esteel,Lustre和Signal是最著名的几种有代表性的同步语言。其中Esterel是命令式语言Lustre和Signal是陈述式语言具有数据流特征常被称为同步数据流语言。Lustre是函数风格的语言而Sig-nal是关系型的语言。除Esterel,Lustre和Signal外学术界和工业界还有其他具有同步特征的语言LucidSynchrone是对早期数据流语言Lucid的同步化并采纳了Lustre的许多语言特征Quartz是一种基于Esterel的面向响应式系统的规范、验证以及实现的同步语言Argos是State-chats一种著名的响应式系统的形式化图形语言的同步化Synccharts是一种具有Statecharts风格和Esterel语义的图形语言Grafcet是一种基于有同步特征的Petri网的建模/仿真工具。 这些同步语言各自的特点有利于进行一些实质性的静态检查甚至形式化分析和验证从而有益于产生安全的代码。在基于同步语言的开发工具中最著名的是Scade,其代码生成器KCG将一种基于Lustre的建模语言翻译成C语言。KCG应该是获得民用航空软件生产许可DO-178B/C的第一个商用代码生成器。目前Scade工具已渗透到我国航空航天、轨道交通及核电等安全关键领域。 虽然同步语言的发展已经相当成熟并在安全关键的嵌入式实时系统中极具影响力但一直以来人们对安全关键系统的可信性要求日益提高期待在各个环节上都达到最高程度的安全可信。同步语言实现工具各阶段的编译器、代码生成器本身的安全性近年来已引起了学术界和工业界的极大关注和兴趣。 本文主要关注同步数据流语言的代码生成工具Lustre,Signal以及LucidSynchrone是此类语言的典型代表。上面提到的其余同步语言与本文话题关系不大仅简单提及。此外LucidSynchrone项目所积累的有关编译器验证的基础研究均由同一课题组人员转化为对Lustre编译器的验证工作。事实上关于同步数据流语言编译器的验证工作从目前学术界和工业界的进展来看仅需关注与Lustre和Signal相关的工作即可。 同步数据流语言具有时钟同步、并发、流数据对象等特征。例如,Lustre语言中所有的数据都是流stream对应于无穷多个逻辑时钟周期每个周期有一个取值。所有的运算都作用于流。每个逻辑时钟周期都执行同样的计算即相同的代码并假设在逻辑时钟周期内计算一定可以完成即满足所谓的同步假设。各个周期内的计算由多个计算节点node组成每个计算节点内部是一个等式的集合每个等式都定义流上的运算等式之间并发执行是数据驱动的计算过程。时态运算和时钟运算是Lustre语言以及其他同步数据流语言中具有特色的流运算。基本的时态运算包括pre,fby和arowf等其中pre和fby可用于访问历史信息基本的时钟运算包括when,current和merge等算子可用于改变时钟的快慢。
3代码生成工具的构造途径
如何才能保证编译器的安全和可信对于编译器来说安全和可信的具体指标就是其正确性要保证从源程序到目标程序的翻译过程正确即保证源语言的行为特征能够在目标语言中被正确地体现杜绝“误编译”。目前保证可信性的方法主要有两类1非形式化的方法或传统的方法如采用测试和过程管理;2采用形式化的方法主要包括直接对编译器本身进行验证和翻译确认以及混合使用这些方法。
3.1 通过测试和过程管理实现编译器的可信性
为了保证编译器实现的正确性普遍的做法是采用大量的测试用例对编译器进行测试。例如GCC的torture测试集包含几千个C源程序用例商用的PlumHallStandardValidationSuiteforC有几万个用例,LustreV6的开源软件包中含几百个源程序用例等等。还有一些Bug-hunting工具例如Csmith它可以产生更多或更独特的源程序用例从而扩大覆盖范围发现更多的编译器缺陷。 尽管如此采用测试的手段仍是不完善的如果测试用例的覆盖范围不够广泛则可能会遗漏编译器中的错误。即便是通过测试发现了错误并且做了修改也无法保证编译器自身的正确性。实际上仅编译器自动测试工具Csmith截至2011年2月以及EMI/SPE截至2017年10月就发现了GCC和LLVM的近1700个编译错误。 Scade工具的代码生成器KCG经过了严格的VV过程符合民航电子系统的国际标准DO-178B/C并且在空客公司的多款客机如A340和A380中成功应用。然而DO-178B/C主要是以过程质量控制为主的标准不足以说明Scade的编译器不存在“误编译”。KCG并没有通过形式化的方法加以严格验证虽然DO-178C中包含了一些非强制的形式化相关条款但经调研业界的用户仍会不时发现ScadeKCG的某些翻译漏洞。
3.2 通过对翻译过程本身进行形式化验证实现代码生成工具
为增加编译器的安全和可信程度仅通过测试和严格的过程管理都是不够的。对编译器进行正确性验证是解决问题的根本途径。最严格的验证手段莫过于采用形式化方法。工业界也早已意识到形式化软件开发的潜力在一些安全攸关领域的安全级软件开发标准中也逐步新增了与形式化方法相关的目标或者相应的补充说明。CCCommonCriteria安全评估标准6中将可信性分为7个级别EAL1到EAL7可信性级别越高其采用形式化规范和验证的程度就越高。航空无线电委员会RTCA近期也已推出民航电子系统的国际标准DO-178C,其在DO-178B的基础上增加了对形式化规范和验证的要求如DO-178C和DO-333等补充说明。 近年来有关编译器形式化验证的研究工作取得了长足的进步达到了实用化水平为未来制定新的工业标准奠定了强有力的基础。CompCert28编译器是经过形式化验证的代码生成工具的杰出代表。该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码后来也支持IA32和ARM后端目前已扩展至可支持64位处理器以及开源的RISCV体系结构其编译过程划分为多个阶段前端解析过程之后每个阶段的翻译正确性都借助辅助工具Coq进行了证明且这些证明可由独立的证明检查器检查。这是迄今最强的形式化验证手段达到了人们所能期望的最高可信程度客。由于其目标是对主体翻译过程本身进行验证如图2所示因此称此类代码生成工具为经过验证的编译器。Yang等关于Csmith的研究工作表明CompCert在正确性方面的表现明显优于常用的开源或商用C编译器。因CompCert编译器具有的杰出成就,其代表性论文的作者Leroy获得了2016年度的“十年前最有影响POPL论文奖”MostInfluentialPOPLPaperAward。 图2 经过验证的编译器(以CompCert为例)
3.3 通过翻译确认技术实现代码生成工具
尽管对编译器的翻译过程本身进行形式化验证是一种比较完美的保证可信性的办法但是其难度高工作量大并且无法扩展一旦编译器需要修改那么证明就需要重做。于是Pnueli等最早提出了翻译确认的方案1。翻译确认的方法不是直接验证翻译程序而是用统一的语义框架为翻译过程的源和目标代码建模两个模型之间定义一种特定的语义等价关系/模拟等价关系设计一种可自动证明二者等价性的确认程序返回成功与否成功时或给出证明脚本不成功时或给出反例。根据不同的语义模型确认程序可以通过自动求解或证明、符号计算、模型检查、静态分析等方式来实现模型间的等价性确认。 如图3所示的翻译确认过程中在发现前后中间表示的语义不等价时会使编译器停下来。若非主体翻译阶段比如某类中间代码的优化则可以不必让编译器停下来不做这一优化即可如图4所示。 图4翻译确认针对某个中间表示上的优化
早期,Necula和Lee提出了PCCproofcarryingcode机制并带动了关于确认式编译器certifyingcompiler的研究。可以认为Pnueli的翻译确认是比PCC更通用的机制。PCC机制主要被用来对编译结果进行安全性检查而不是对编译器进行验证。 对于翻译确认来说如果翻译前后的语义保持性的确认过程比较容易构造或者说源语言与目标语言的语义模拟等价性关系比较容易定义则证明也会相对容易那么验证该等价关系是一个不错的选择。因为该方法最大的优点就是可以不放弃现有的编译框架其可扩展性较好。一些大型编译器也有类似的工作。但是当源语言与目标语言差异较大类似于将同步数据流语言翻译成串行语言时两种语言的语义等价性关系是很难定义的其证明过程也会更加困难。 相比较而言当源语言和目标语言的语义定义达到认可的程度时对翻译过程进行验证是一种彻底的做法原理上可以保证源程序的一般性质都可以保持到目标程序上。而翻译确认的做法往往只是关注部分性质的保持性当然也可以逐步逼近一般性质因而有可能会存在“虚假预警”falsealarms。因此直接验证翻译过程与翻译确认两种方案各有利弊。目前看来针对一个完整的编译过程根据各个翻译的特点将这两种方案混合使用是一种十分有益的做法。比如一些针对优化算法的翻译确认工作可以很好地融合到CompCert编译器中。
4 同步数据流语言的代码生成工具
同步数据流语言是应用较为广泛的建模语言比如著名工具Scade所使用的建模语言是在同步数据流语言Lustre基础上定义的。如图1所示像Scade和Simulink这样的建模工具往往是先将建模语言变换到领域语言许多安全关键领域均采用传统C语言然后从C这样的领域语言编译到目标语言。 对于C语言的可信编译研究近年来已经取得了不错的进展如前面所提到的Leroy等开发的C编译器Comp-Cert其原理图参见图2。 近年来针对图1中所示的从高级建模语言到C语言之间的可信编译研究已成为人们的聚焦点⑵。比如Michael和Strichman采用了翻译确认的方法对从Simulink到C的代码生成器Real-TimeWorkshopRTW的编译过程进行了形式化验证。Simulink是MATLAB中的一种基于块状图设计环境的可视化仿真工具可实现动态系统建模、仿真和分析被广泛应用于线性系统、非线性系统、数字控制及数字信号处理的建模和仿真中。模型在Simulink中被认为是可执行的描述,借助于RTW代码生成器这些模型可以生成C代码。 这一节主要介绍以Lustre和Signal为代表的同步数据流语言的代码生成工具的研究现状。就目前的进展情况而言Lustre代码生成工具的代表性研究主要集中于对翻译过程进行验证即采用图2所示的方法;而Signal代码生成工具的代表性研究则是以翻译确认的方法为主即采用图3和图4所示的方法。4.1节介绍Lustre代码生成工具的代表性研究4.2节介绍Signal代码生成工具的代表性研究4.3节介绍一些相关的基础性研究。
4.1 对翻译过程进行形式化验证的方法
对翻译过程进行形式化验证通常需要对翻译前后语言的语法和语义以及翻译过程进行严格的形式化描述然后对翻译前后的语义保持关系进行机器证明。这其中涉及到许多相关的基础性研究本文为了更好地聚焦不对这些方面的研究工作展开讨论仅列举某些关系比较密切的内容参见4.3节。 关于同步数据流语言编译器这方面最早的工作或许是Gimenez等于1999年试图采用Coq针对ScadeV3进行翻译过程的形式化验证但这项工作似乎没有坚持下来因相关资料不详这里不多述。 关于对翻译过程进行验证的同步数据流语言代码生成工具的研究在国际上较有代表性的长线项目主要是两个团队的工作一个是法国INRIA的Pouzet团队另一个是清华大学计算机系的L2C项目组。 受CompCert项目的启发Paulin和Pouzet于2006年启动了一个有关同步数据流语言编译器验证的长线项目其源语言接近Scade的Lustre语言且具有LucidSynchro-ne的特征。据了解该项目初期的工作集中于前端完成了类型检查和时钟演算相关过程的验证后续又开展了因果性分析程序的验证工作。后来Biernacki等描述了该项目的一些相关工作细节他们将Lustre语言的一个较早版本翻译至Java和C代码采用了一种基于对象的中间语言。再后来该团队的Auger在其博士论文和技术论文中对该项目进行了较完整的表述特别是理论基础的论述方面。从中可进一步了解到Pouzet团队的工作是针对一种小的但具有全部Lustre语言关键特征的语言MiniLS并在此基础上实现了同步数据流语言代码生成工具的原型系统句。最近该团队的Bourke等又基于Biernacki和Auger等的工作实现了从上述基于对象的中间语言Obc到CompCett的前端中间语言Clight的翻译与验证从而得到一个核心Lustre子集的代码生成工具Velus。 清华大学计算机系的L2C项目组于2010年开始了一项Lustre语言核心子集到C语言的可信翻译器的研究简称L2C项目该项工作的原理与CompCert项目一致工作目标和上述Pouzet团队的项目相似。L2C项目组创立时主要是面向国内核电领域的实际需求先是实现了单一时钟情形下的一个完整翻译过程的形式化验证后来又升级到一个可以支持多个嵌套时钟的版本。L2C项目所定义的源语言Lustre综合参考了Scade工具的Lustre语言版本和LustreV6能够体现同步数据流语言的主要特征。目前该项目组正在开发和维护一个兼顾学术界和企业界的开源L2C版本。 上述两个项目和CompCert项目一样源语言、目标语言和各阶段中间语言的语法、语义、翻译过程的定义以及语义保持性证明都在交互式辅助定理证明工具Coq中实现。然而二者在许多方面存在不同。首先是源语言的差异L2C编译器立项时是出于国内某安全关键领域的实际需求因此企业版的源语言最终定格为ScadeLustre语言的一个核心子集而开源版的源语言则是将其中的高阶迭代算子9个替换为了LustreV6中的高阶迭代算子5个与L2C相比Pouzet团队的工作目前主要是面向学术研究其源语言包括最新版编译器V§lus的源语言不支持许多数组和结构体上的操作尚未支持任何高阶运算并且对时态和时钟算子的支持也略少于前者。其次L2C项目代码生成工具的目标语言C从一开始就借用了CompCert编译器中Clight的语法和语义定义或,语义定义中直接釆用了贯穿CompCert编译器几个阶段的底层存储模型而Veins是从中间语言Obc翻译到Clight语义定义中的存储模型有明显的跨度。另外一个明显的差异在于编译器结构丄2C编译器在Clight之前的核心中间层超过10层而Veins编译器在Clight之前的核心中间层仅有2层翻译过程分散为多个阶段有利于简化各翻译阶段的正确性证明且具有更好的可扩展性。对于实现工业级的代码生成工具来说可扩展性是非常重要的但同时翻译过程也不应过多否则会加重实现和维护的负担。
4.2翻译确认的方法
1998年Pnueli第一次提出了翻译确认的设计思想。Pnueii所给示范例子的源语言就是Signal特征的多时钟同步数据流语言其目标语言是C随后Pnueii在原有工作的基础上继续实现了对两种同步数据流语言到C的编译器的翻译确认这两个编译器中包含了大约100个优化规则证明了翻译确认方法也适用于优化编译器同时实现了一个翻译确认器CVTcodevalidationtool其可对编译器每一次执行所产生的代码进行检测通过模型检验判定与源代码是否等价。这一技术用到编译器可追溯的信息如状态变量是如何翻译的。 近年来Ngo和Talpin等基于翻译确认的思想也开展了同步数据流语言Signal到C的编译器验证工作。其主要工作包括对源代码和目标代码使用统一的语义框架PDSpolynomialdynamicalsystems建模给出一种源和目标之间的抽象时钟等价关系通过对等价关系进行验证来保证编译器时钟语义的一致性其证明釆用SMT求解器自动完成同时也基于一种由一阶逻辑公式定义的时钟模型开展了保持时钟语义的翻译确认工作,利用同步依赖图SDGs对依赖关系的保持性进行确认使用同步数据流求值图SDVGs,对翻译前后的求值语义保持性进行确认并基于这些技术提出了一种大规模同步数据流语言编译器验证的扩展性良好的设计方案该方案侧重于对时钟、数据依赖关系的保持性以及变量的求值等价性等方面的翻译确认。 如3.3节所述翻译确认方法不依赖于翻译的具体过程相比于对翻译过程进行验证的方法更具有可扩展性。然而,这种方法也有自身的缺陷比如一般情况下难免存在某种程度的误报mis-alarm率。总体来看上述工作要达到工业级应用的要求尚有较长的路要走。
4.3 —些相关的基础性研究
与同步数据流语言编译器验证相关的研究有很多它们都釆用了形式化的方法对同步数据流语言的语义进行定义这对翻译过程中的形式化验证是很有帮助的。 Kahn将一类异步确定并行程序现称为Kahn网络描述为基于流变换streamtransformation的递归方程系统并给出一种完全偏序集CPO语义。若将Kahn网络限制到同步程序则可以认为其是Lustre或其他同步语言的基础。以Kahn网络为出发点人们也便于对同步数据流范型进行扩展叫。 无疑对于同步数据流语言语义的形式化定义Kahn网络的CPO语义指称语义是重要的参考之一。Paulin-Mo-hring基于Coq开发的KahnNetworksinCoq库是这方面的一项重要工作同时他们也开发了通用CPO库其比Kahn为Coq开发的CPO库更加完善。 由于是一脉相承针对Lucid或LucidSynchrone语义的一些研究。包括具体的操作或指称语义定义以及这些工作在Coq环境中的实现在Lustre语言代码生成工具的研发中都可以借鉴。 借鉴上述工作可以给出同步数据流语言的指称语义甚至使用Coq的描述语言给出精确的定义。然而利用此类指称语义来指导编译器的实现以及完成翻译过程的验证有一定难度。 在Lustre语言的原始论文中作者给出了Lustre语言的基本操作语义规则涵盖了时态算子的语义规则也包含了时钟演算的规则。在Caspi和Pouzet的研究其中也釆用类似方法来定义同步数据流语言的同步操作语义。这种操作语义的语义规则非常直观且容易理解然而若是要对应到编译器的实现还需要在面向实现方面进一步细化和改进。 还有许多与同步数据流语言相关的工作也值得关注。Cohen等于2005-2008年间提出了针对同步数据流系统更加宽松的同步和时钟演算模型如。Delaval等提出了空间类型系统以支持分布式系统上同步数据流语言的设计。 Schneider等开展了类Esterel的命令式同步语言的翻译验证工作解决了Schizophrenia问题。辅助证明工具釆用HOL。Schizophrenia问题必须在因果分析causalityanal-ysis之前解决因同步数据流语言不存在此类问题故此处不赘述。 L2C课题组基于一个小的Lustre语言子集实现了一个时钟归一化过程的原型可以将多时钟流转化为单一的时钟流并形式化验证了变换过程的语义保持性然而这一方法仅适用于传统的fby算子2个参数在当前L2C项目 財中未釆用。
结束语
现阶段与常规语言一样同步数据流语言编译器或代码生成器形式化验证的方法可以大致分为两大类一类是针对编译器本身的验证整体或部分另一类是翻译确认的方法验证目标代码和源代码之间的符合性不验证编译器本身前者是一种较完美的做法但工作量大不容易扩展后者的扩展性较好但只适合于解决局部问题。目前已有一些基于辅助定理证明器针对编译器本身进行验证的工作比如本文提到的Pouzet项目组以及L2C项目组二者的源语言均基于Lustre语言。关于翻译确认Pnueli等首先提出这一方案时所釆用的示例就是基于同步数据流语言Signal;目前进展较好的工作有Ngo和Talpin等所开展的同步数据流语言Signal到C的编译器验证工作。 同步数据流语言与串行命令式语言的语义之间有很大差距因而对同步数据流语言编译器进行验证特别是针对编译器本身进行验证的难度和工作量较大但实际中存在此类需求比如花大力气开发出的安全级产品一旦经过认证而投入使用后允许再度更新的周期相当长。另外也无需对编译器的所有环节进行验证比如目前很少有人特别重视lexer和parser部分的验证工作。还有为降低难度在某些扩展和维护工作量过大的翻译阶段我们可以选择不对编译器本身进行验证而选择釆用翻译确认的方法作为补充比如Comp-Cert项目也有个别阶段釆用了翻译确认方案。用这种混合的方法能更好地平衡编译器实现过程中的可信性、难度以及工作量之间的关系。 虽然经过形式化验证的编译器离商用尚有很长的路要走但未来某些标准强制性地要求严格证明是极有可能的工业界需要有一个逐渐适应的过程。对于代码生成工具的开发形式化验证的方法无疑代表了一种未来新技术变革的趋势。 现实中可信编译还有另外一层含义即尽可能保障被编译对象的可信。本文仅关注编译过程的可信不涉及这方面内容。
致谢
清华大学L2C项目组的师生为本研究提供了许多有价值的素材在此表示感谢。 原文链接
---
转载于http://www.digiproto.com/archives/2711
