同步数据流语言可信编译器Vélus与L2C的比较*

康跃馨, 甘元科, 王生原

(清华大学 计算机科学与技术系,北京 100084)

应用于航空航天、高速铁路、核电能源和医疗卫生等领域的安全攸关系统[1]一旦失效,将给人类生命财产、社会生产、生活环境带来巨大的破坏.如何为安全关键系统构造一个基础的安全软件环境是需要面对的首要问题,尤其是对操作系统、编译器等基础软件而言.

作为用来产生代码的工具,编译器的实现和维护自然经过了“精雕玉琢”,因此编译器的正确性问题容易被人们忽视.但了解实际情况的人都知道,编译器的“误编译”问题是司空见惯、习以为常之事.对于许多领域来说,由于一般不会引发本质的问题,又是小概率事件,人们也往往容易忽视误编译所带来的负面影响.然而,对于安全关键系统而言,则必须考虑因编译器引入的错误,否则,花大力气在源程序级的验证工作可能在目标程序级失效.实际上,如航空领域的RTCA DO-178B/C标准,编译器属于需要鉴定的工具类软件,需要按照机载软件的要求那样对待.

要保障编译器的正确性/可靠性,传统上采用大量的测试以及严格的软件过程管理来实现,这并不能杜绝“误编译”现象.对编译器进行正确性验证,而不仅仅是测试,是解决问题的根本途径.最严格的验证手段莫过于采用形式化方法,近年来,有关编译器形式化验证的研究工作取得了长足的进步,达到了实用化水平,为未来新的工业标准的制定奠定了强有力的基础.CompCert编译器[2]是经过形式化验证的可信编译器的杰出代表.该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码(后来也支持IA、ARM以及RISC-V后端),其编译过程划分为多个阶段,每个阶段的翻译正确性都借助证明辅助工具 Coq[3]进行了证明,且这些证明可由独立的证明检查器检查,这是迄今最强的形式化验证手段,达到了人们所能期望的最高可信程度[4].Yang等人关于Csmith[5]的研究工作表明:CompCert在正确性方面的表现明显优于常用的开源或商用 C编译器.因 CompCert编译器的杰出成就,其代表性论文[6]的作者 Leroy获得了 2016年度的 10年前最有影响 POPL论文奖(Most Influential POPL Paper Award).

C语言一直以来是安全关键领域中使用最为普遍的开发语言,人们下了很大功夫,使基于 C语言的系统开发更加安全、高效.然而,毕竟C语言程序层次较低,不易使人们聚焦于问题本身,开发效率受到很大影响,并且也难于验证,于是基于模型/模型驱动的开发逐步兴起并成为业界主流,由模型自动生成的代码(C代码为主)占比越来越高.比较著名的建模语言/工具,如Simulink[7]、Scade[8]等.

有一类建模语言称为同步语言,特别适合于实时控制系统的开发.所有同步语言均遵循同步假设,即每个周期内的计算(从输入值得到输出值)都是瞬间完成的.另外,同步语言的语义被要求具有确定性.同步假设以及确定性可以极大地简化实时系统的验证.Esterel[9]、Argos[10]、Lustre[11,12]和Signal[13]是几种有代表性的同步语言.其中,Esterel是命令式语言;Argos是基于并行和分层自动机的图形化语言;Lustre和Signal是陈述式语言,具有数据流特征,常称为同步数据流语言.Lustre是函数风格的语言,而Signal是关系型的语言.这些同步语言各自的特点有利于进行一些实质性的静态检查甚至于形式化分析和验证,从而有益于产生安全的代码.在基于同步语言的开发工具中,最著名的是Scade,其代码生成器KCG将一种基于Lustre的建模语言翻译到C语言,KCG应该是获得民用航空软件生产许可(DO-178B/C)的第一个商用代码生成器.目前,Scade工具已渗透到我国航空、航天、轨道交通及核电等若干安全关键领域.

与 C语言编译器的情形类似,人们同样不会止步于像 Scade这样的安全级代码生成器.基于高级建模语言代码生成器的形式化验证近年来已受到极大关注.本文主要分析与比较两个关于同步数据流语言 Lustre的可信编译器项目,二者均采用如CompCert那样的方法对翻译过程本身进行验证.这两个项目是目前仅有的从事形式化验证的Lustre可信编译器研发的长线项目,一个是法国Pouzet教授的项目组,另一个是作者所在的L2C项目组.前者较早的工作[14]将具有Lustre语言关键特征的Lustre子集翻译至一种基于对象的中间语言,最近的工作是将这一中间语言翻译至Clight(见CompCert项目),并与CompCert衔接后称为Vélus编译器[15].L2C项目致力于基于Lustre的语言到C语言的可信代码生成器(或称L2C编译器)的研发,从一开始便以Clight作为目标语言,从而与 CompCert实现对接.有关这两个可信编译器项目的进一步发展情况会在正文中详细介绍.为方便起见,文中分别以Vélus和L2C代称这两个项目以及相应的编译器.

编译器形式化验证的另外一种重要方案是翻译确认(translation validation),由Pnueli等人于1998年首先提出[16].翻译确认不是直接验证翻译程序,而是对翻译前后代码前的语义等价关系进行确认.比起直接对翻译过程进行验证,这种方法具有较好的可重用性.然而,它必须是一个自动化的过程,因而从理论上决定了它可能出现误报(false alarm).值得指出的是,Pnueli等人首次提出翻译确认方法时,是以Signal作为示范例子,即编译器源语言是同步数据流语言Signal,目标语言是C.翻译确认的话题与本文主题关系不大,因此不再进一步展开讨论.

本文第1节首先介绍Vélus和L2C的基本情况.第2节～第6节分别就源语言特性、编译器结构、核心翻译步骤、同步数据流语义与翻译正确性验证、实现与性能等多个角度对Vélus和L2C进行较为深入的分析与比较.最后,第7节是全文总结.

1 基本情况

同步的概念[17]早在20世纪80年代初就开始被关注.到20世纪80年代后期出现了包括Lustre[12]的几个最著名的同步语言,其他,如 Esterel[9]和 Signal[13]等.Lustre语言最初是由 Caspi和 Halbwachs等人提出来的[18],然后在工业领域需求的基础上发展起来[19].先是在Merlin-Gerin公司开发了基于Lustre的Saga工具,用于核电保护系统开发.接着,Verilog公司接手了 Saga商品化的工作.同时期,Aerospatiale公司(现隶属于空客)为空客 320机载软件开发设计了Sao工具,其思想也类似于Saga.后来,在Saga和Sao的基础上,Aerospatiale、Merlin-Gerin以及Verilog联手启动了新工具(Scade)的开发计划.当时,Verimag实验室建立了Verilog公司和Lustre项目组合作的一个共同实验室,专攻Scade的设计,并由Lustre项目组的Pilaud领导Scade团队.再后来,Scade又吸收了其他公司的一些技术,并经多次转卖,目前全球闻名.

Lustre语言被应用于商用工具后得到更多的重视,Verimag的Lustre团队也一直在维护和更新版本,目前的最新版本是Lustre V6[20].

Pouzet教授课题组很早开始从事同步语言相关的研究工作,曾与Caspi等人合作在数据流语言Lucid[21]基础上加入同步特征,设计实现了同步数据流语言Lucid Synchrone[22],实际上也可以看作是Lustre的函数式语言(ML)的扩展[23].

大致在2006年前后,Pouzet与Paulin共同启动了形式化验证Lustre语言编译器的一个长线项目[24].最早的参与者有Bertails和Biernacki.在TYPES 2007会议上,Bertails[25]报告了该项目的目标以及最初始的一些工作(类型检查、时钟演算以及因果性分析等问题).Biernacki等人在 2008年发表的论文[14]中刻画了一个更加清晰的蓝图并给出一些实质性进展,为该项目奠定了基调.后来,Auger完成了其博士论文工作[26,27],该项目取得进一步的成果.从这些工作可知,该课题组这一时期实现的形式化验证编译器,源语言为包含Lustre语言关键特征的小型同步数据流语言,目标语言是一种基于对象的中间语言.最近几年,Bourke等人基于Biernacki和Auger等人的工作,实现了从上述中间语言到CompCert的前端中间语言Clight的翻译与验证,从而得到一个核心Lustre子集的可信编译器Vélus[15].

本文作者所在课题组的L2C项目,源于国内核电领域的实际需求,于2010年9月正式启动.L2C可信编译器的预研工作于2013年6月完成验收[28],源语言为一个单时钟的核心Lustre子集.L2C可信编译器的一个完整企业版于2015年4月完成验收[29],源语言为一个面向领域的类Lustre同步数据流语言.L2C项目开展后,合作企业的建模与代码生成工具从原 Scade的用户走向自主研发之路,目前已被实际应用.最近几年,L2C项目组主要在做开源L2C可信编译器的工作[30-32].

后续各节中,会涉及到有关Vélus编译器和L2C编译器的更多细节.

2 源语言特性

本节在讨论Vélus和L2C的源语言特性时,会涉及到原始论文中的Lustre语言、Lustre V6以及Scade源语言的特性.

Caspi和 Halbwachs等人在其早期论文[11,12]中给出了 Lustre语言最基本的特性.Lustre程序由若干节点(node)组成,执行时会明确一个主节点.每个节点相当于普通语言中的子程序.不同于普通语言,Lustre语言的所有数据对象(变量、常量以及表达式)的取值都是流(stream).每个流都有各自的时钟(clock);每个节点有一个基本时钟,是该节点中所有数据对象的时钟里面最快的一个.程序的执行是无限循环的过程,每次循环均在一个时钟周期(cycle)内完成,每次执行都针对不同的输入和输出.对于每个时钟周期,一个流或者有值,或者没有值,前者是当前时钟周期包含在这个流的时钟的激活(activation)周期,而后者是当前时钟周期不属于激活周期的情形.时钟相同的流之间可以进行运算,相当于这些流在该时钟的每个激活周期里的取值都进行相应的运算.节点可以被调用,可以看作特殊的运算.节点调用相比传统语言(如C语言)的函数调用,允许有多个返回值.每个节点中包含一组等式,每个等式的执行效果类似于赋值.

Lustre语言中有几个与时钟和流相关的特殊运算(或算子).when和current均为一元运算,它们产生新的流,其时钟会不同于原来的流;when会使时钟变慢,而current会使时钟变快,二者为互补的运算.pre为一元运算,所产生的流会比原来的流延迟一个激活时钟周期.二元运算 arrow(→),所产生的流第 1个激活周期的值取自第 1个流,其余激活周期的值取自第2个流;特别是,通常会与pre运算配合使用,为新流置第 1个激活周期的值.fby为二元运算,所产生的流第1个激活周期的值取自第1个流,其余激活周期的值取自第2个流进行pre运算之后的流,其效果相当于前面提到的arrow(→)与pre运算的配合使用.为叙述方便,下面将pre、arrow以及fby之类的算子称为时态(temporal)算子,而将when和current之类的算子称为时钟(clock)算子.

为方便起见,我们称上述原始论文中的 Lustre语言为经典 Lustre语言.为便于实际应用,Lustre V6以及Scade在经典Lustre语言核心特性的基础上增加了更为丰富的语言特性,在下面讨论Vélus和L2C时会涉及到其中一些.

Vélus编译器目前未开源,其源语言的信息主要依据其里程碑论文[14,15,27]以及该项目最新论文[15]的作者Bourke提供给我们的Vélus编译器部分源程序测例.

从实现角度看,无论是Lustre V6和Scade,还是本文讨论的Vélus和L2C,对于经典Lustre语言核心特性的实现基本上是遵循原始论文中所定义的语义.有一个值得注意的例外,即关于节点的调用.在Caspi和Halbwachs等人的论文中以及之后相当一段时间内的学术探讨中,Lustre语言编译器在翻译时都是将节点调用进行宏展开(有必要时会进行一系列换名),形成实际上只含一个节点的中间语言.这在实际应用中显然是不合适的,因此在Lustre V6、Scade、Vélus以及 L2C中,节点调用的实现均与传统语言类似.对此,在 Vélus中,将其称为模块化(modular)实现[14,15,27].

从传统语言特性方面看,Vélus与Lustre V6基本类似,而L2C和Scade除了这些特性外,还增加了一些面向实际应用的特性,主要包括case表达式以及更多的数组和结构体运算.

在时态算子方面,Vélus目前仅支持经典Lustre语言中的fby算子,而L2C、Lustre V6以及Scade均支持经典Lustre语言中的全部时态算子(pre、arrow和fby).在Bourke提供的Vélus测例程序中,对原始例子中出现pre和arrow之处均用fby及条件(if)表达式进行了等价替换,参见PLDI 2017论文[15].另外,L2C与Scade还增加了一个三元fby算子.二元fby算子可通俗理解为:结果流是将原来的流(第2个参数)延后一个激活周期,且第1个激活周期取第1个参数的流在该周期的值.三元fby算子是一种扩展:结果流是将原来的流(第3个参数)延后n个激活周期,且前n个激活周期均取第1个参数的流在第1个激活周期的值,这里,n为第2个参数.

在时钟算子方面,Lustre V6是最全面的,包含when、current和merge算子.merge算子是作用于互补的慢速流,将它们归并后得到一个快速的流.Vélus与Scade均不支持current算子,认为merge完全可以替代current的作用.虽然Vélus与Scade同样都是支持when和merge算子,但二者有一个本质的差异:Scade既有布尔型的时钟,又有枚举型的时钟.布尔型时钟是通过布尔量的true或者false进行二选一取样(或确定是否激活周期),而枚举型时钟则可以通过枚举量进行多选一取样.Scade和Lustre V6都同时支持布尔型时钟和枚举型时钟,Vélus与L2C目前都只支持布尔型时钟.与Vélus不同的是,L2C除支持when和merge算子外,也支持current算子.L2C规划中拟支持枚举型时钟,但目前尚未实现.

对于一般运算,各操作数的时钟要求是相同的.但对于节点调用的运算,在一些语言中各个参数的时钟可以是不同的,L2C、Lustre V6以及Scade都是这样,但Vélus目前要求所有参数的时钟是相同的.

在高阶迭代算子方面,L2C的两个主要版本有不同的支持.对于面向核电领域的企业版L2C,支持Scade的9个高阶迭代算子[29];对于开源版的L2C,则支持Lustre V6的全部5个高阶算子[31].这二者之间,有3个算子的含义是等价的.目前,Vélus未支持高阶迭代算子.

表1是有关Vélus和L2C的源语言特性对照的一个简单小结.

Table 1 Source language features (L2C vs. Vélus)表1 源语言特性(L2C vs. Vélus)

3 编译器结构

Vélus编译器的架构如图1所示,该图与Bourke等人在PLDI 2017论文[15]中的编译架构图(该文的图1)相对应,包括所有中间语言和翻译过程所用的名称.Vélus编译器继承了 Pouzet课题组的前期工作[14,27],下面的介绍并未刻意区分这些集成进来的部分,欲了解详情可参考文献[15].

图2刻画了最新的L2C编译器架构,是目前的开源版L2C[31]所采用的架构.以前的L2C版本(主要有原型版与企业版)的架构与此有所不同,不在本文讨论范围之内,这里不再赘述.

两个编译器的前期处理工作很相似.图1中Vélus将源程序(Source)翻译至中间表示SN-Lustre的过程,对应于L2C将源程序(Lustre*)翻译至中间表示LustrS的过程.

二者的 Parsing过程如同常规的编译器,实现词法和语法分析,并生成抽象语法树(AST).经过 Parsing过程,Vélus将源程序变换至AST,图1中标为Unannotated Lustre.同样,L2C经过Parsing过程也将源程序变换至AST,之后附加了一个LustreWGen过程,最后生成LustreW中间表示.LustreWGen最核心的任务是完成全局和部分局部常量表达式求值(含常量定义的依赖性检查和排序),以方便后续技术环节高效地处理需要单个常量的情形,如三元 fby运算中的延后激活周期数(正整数常量值)、高阶迭代运算的迭代次数常量、数组定义或访问区间有关的常量,等等.Vélus目前不支持这些特性,故此类需求不足.LustreWGen还有一些个别很细节的任务,比如根据调用关系自动设定主节点.主节点不一定非要自动设定,也可以在执行时手动设定,对于此类细节,在Vélus的相关论文中并未提及,因此在本文后续内容中,对于此类细节也并未作为关注重点.

随后,是类型和时钟检查及其标注过程,Vélus和L2C所完成的工作是一致的:对程序(AST)进行常规类型检查以及时钟检查.若检查不通过,则报错;检查通过后,进行类型和时钟标注,类型检查与传统语言相同,时钟检查二者遵循相同的时钟演算规则.如图1所示,Vélus称这一过程为Elaboration,标注后的中间语言称为Lustre.同样的工作在L2C中是由LustreVGen过程完成的.除了类型和时钟检查及其标注过程之外,LustreVGen还包括一些后续阶段所需要的准备工作,参见随后的介绍.

完成类型和时钟检查及其标注之后,Vélus进行Normalization变换,其最核心的工作是使每个fby表达式和节点调用实例从上层表达式分解出来,确保它们只出现在专用等式的右端,而不是嵌在其他表达式中.这与Lustre官方编译器以及 Scade工具的做法是一致的,主要是进行一些使代码规范化以及新生成某些结构信息,为后续阶段做好铺垫:对于fby等时态算子,要准备好如何对fby等时态算子在有关历史数据的访问方面得到妥当处理;以及针对节点的每一个调用实例要如何做好输入流和输出流相关的处理.首先是不同输入流和输出流的时钟有可能不同(Vélus目前不支持这种情形),其次是输出流可能有多个(比较,C函数仅有一个返回参数).

在L2C框架中,与Vélus的Normalization相对应的工作体现在LustreVGen和LustreSGen过程中,如图 2所示.LustreVGen首先进行如前所述的工作(类型和时钟检查及其标注),之后是生成fby和pre等时态运算所需要的特殊标识符和类型;以及生成类型比较函数的函数名;结果得到LustreV中间表示.使每个fby表达式和节点调用实例从上层表达式分解出来的工作在LustreSGen过程完成.除此之外,LustreSGen还实现以下功能:将含有表达式列表的平行等式分解为多个不含表达式列表的等式集合,将arrow(→)和pre算子的组合转换成二元fby算子,以及将高阶迭代算子处理成类似for循环的结构(为后续阶段的高阶算子消去,即生成for循环作准备)等.

在LustreVGen和LustreSGen过程中有许多方面对于当前的Vélus来说是不需要的.另外,在对于包含条件的表达式处理上,Vélus和L2C略有不同.经Normalization变换后,Vélus将所有if和merge表达式置为顶层,而L2C是在排序(见后文)之后才处理if、case和merge等算子.

接下来,Vélus和L2C均对上述变换之后的中间代码以等式为粒度进行排序.这些等式之间具有数据流并发关系,排序之后等式之间具有先后顺序关系,等式的语义与命令式语言的赋值语句相类似.排序的结果应不违背数据依赖关系,即满足先写(或先有值)后读的原则.Vélus和 L2C的排序过程分别称为 Scheduling和 Toposort,如图1和图2所示.

后续翻译过程中,Vélus从SN-Lustre到Obc的过程,以及L2C从LustreS到LustreC的过程,集中了多数核心同步数据流语言特征的翻译.同样,Vélus从Obc到Clight以及L2C从LustreC到Clight的变换将同步数据流语言的可信编译与可信编译器CompCert衔接起来,对二者来说都是整个编译器最后的重要环节.对于这些核心翻译步骤,我们将在下一节加以专门讨论.

在当前的开源版L2C中,已发布了从LustreS到LustreC全部翻译过程(包含了所有的核心翻译阶段)的正确性验证代码;LustreWGen、LustreVGen和LustreSGen等非核心过程的验证工作多数也已完成,将会在后续版本中陆续发布(试对比,CompCert的前端一些非核心翻译过程如语法分析、类型检查等的验证工作也是在新近的版本中才陆续发布).因Vélus至今尚未开源,其核心翻译步骤的验证工作可以从相关论文中有所了解,但非核心翻译过程验证的工作在论文中很少提到具体的实现情况.有关二者核心翻译阶段的验证工作,在第 5节有进一步的讨论.

相比Vélus,L2C之所以有更多的翻译阶段,主要有如下原因:(1) L2C立项时是面向实际的领域需求,所以支持较多和较为复杂的语言特性,而 Vélus相关的工作主要面向学术研究,二者在源语言特性方面的对照参见表1;(2) 实用语言的编译器开发需要不断维护,多阶段的翻译有利于可重用性及可扩展性,如 CompCert面向可实用的 C语言,其编译器结构中包含了许多翻译阶段;(3) 安全攸关领域一般都有可追溯的要求,多阶段的翻译有利于提高可追溯性.

4 核心翻译步骤

从 Lustre语言翻译到 C,由同步数据流范型变换为串行命令式范型,必须实现几个核心同步数据流语言特征的翻译,Vélus和L2C的翻译阶段均包含了对这些核心特征的处理,主要包括:(1) 通过以等式为粒度的排序或调度,完成数据流并发特征的消去,实现等式集合的串行化;(2) 实现同步数据流语言时钟算子特征的消去;(3) 实现同步数据流语言时态算子特征的消去;(4) 结合前述这些特征的处理,实现同步数据流范型向串行命令式范型的转换.

在上述几个核心同步数据流语言特征的翻译步骤中,以等式为粒度的排序或调度容易解释,在前面一节已经介绍过(Vélus中对应Scheduling,L2C中对应Toposort),剩余的3个方面在本节进行讨论.对于经历这几个消去同步数据流特征的翻译步骤之后所得到的中间代码,Vélus和 L2C最终将其翻译至 Clight代码,从而实现与CompCert的对接.翻译至Clight代码的步骤也是本节要讨论的重点内容之一.

L2C支持高阶迭代算子,高阶算子的消去也是L2C的核心翻译步骤之一.这项工作主要是在LustreRGen过程(如图2所示)中实现的,它将高阶运算翻译为等价的for循环语句.由于Vélus未支持高阶迭代算子,所以我们不对这一核心翻译步骤作进一步讨论.顺便,对于其他L2C支持而Vélus不支持的非核心语言特征,其处理过程也同样不作讨论,比如,将复杂类型比较运算翻译为比较函数的过程(图2中的TransTypecmp).

值得注意的是,在上述核心翻译步骤中,除了排序(调度)和生成到Clight,对于其余几个方面,Vélus均集中在从SN-Lustre到Obc两个层次的变换,而L2C则是分散在LustreS到LustreC的多个层次的变换中.

(a) 时钟算子的消去

我们仅讨论Vélus和L2C均支持的时钟算子when和merge(此外,L2C还支持current算子).

Vélus和L2C遵循相同的时钟演算规则,在仅限于布尔型时钟的情况下,嵌套时钟可由时钟变量(或其否定)的序列来表示(可参见Biernacki等人在2008年发表的论文[14]):baseonb1onb2… onbn.其中,base为当前节点的基准时钟,每个bi或者是某个时钟变量(布尔型)x或者是其否定notx.

图3给出Vélus和L2C均可以接受的一个源程序例子.我们来观察节点tracker的代码.假设该节点的基本时钟为base.根据时钟演算规则,变量c的时钟为baseonx(与counter调用中的两个参数的时钟相同),而表达式(ptwhen notx)的时钟为baseon notx;x,t,pt等变量的时钟均为base.表达式mergexc(ptwhen notx)的作用是将时钟分别为baseonx和baseon notx的两个表达式c和(ptwhen notx)归并为一个时钟为base的表达式.这里,需要注意的是,when算子会使时钟变慢,而merge算子会使时钟变快.

在得到各变量以及表达式的时钟后,when算子实际上就可以消去了.翻译的结果就是将等式(左边的变量和右边的表达式具有相同的时钟)的执行加上时钟为真的条件,生成if条件语句.这一条件的构成是将时钟表达式中所有的时钟变量(或者其否定)进行合取,而基本时钟base可认为是true.例如,若时钟为baseon notx,则条件即为notx.

对于merge算子,则会翻译为if-else条件语句或case语句.例如,图3中的mergexc(ptwhen notx),Vélus会翻译为类似于if (x) {c=…} else {pt=…}之类的语句.在L2C中也类似,不同的是,L2C的设计要支持枚举型时钟,所以目前选择了一种更为一般的情况,会将merge表达式翻译至case语句.具体细节可分别对应于附录中图4所示右半边的if语句和图5所示右半边的case语句.

顺便,Vélus在生成Obc表示后会针对这些if语句进行Fusion Optimization的优化处理(如图1所示),使条件相容(多为时钟相同)的分支语句序列进行合并,这样仅需一次条件判断即可.目前,L2C尚未开展此类优化工作.这个问题,后面还会提到.

(b) 时态算子的消去

Vélus经过Normalization变换,或者L2C经过LustreVGen和LustreSGen过程,已确保了每个fby表达式只出现在专用等式的右端,而没有嵌在其他表达式中.图3中的所有fby表达式均已满足这一要求,对应的等式为:节点counter中的f=true fby false和c=1 fbyn,节点rising中的ps=true fbys,以及节点tracker中的pt=0 fbyt.我们以tracker中的pt= 0 fbyt为例解释fby算子的消去.

每个fby对应一个时态变量,用于记录历史状态.对于图3中节点tracker的含fby等式pt=0 fbyt,这一变量为pt.无论是Vélus还是L2C,都会将pt包装为节点tracker内可访问的特殊变量.下一小节会看到,Vélus会将pt看作节点tracker所对应的类的属性变量,每个tracker实例都会维护一份pt的存储,可以保存以前周期的信息,而其他普通变量(比如t)只能看作节点tracker所对应的类的方法的内部变量.类似地,L2C会将pt看作与每个tracker的实例相关联的某个全局结构体的域变量,而其他普通变量(比如t)不在这个全局结构体的域中.

若从对应到Vélus翻译后的Clight代码角度来看,图4所示的结构体类型tracker包含了域变量pt,对应于上述节点tracker所对应的类的属性变量pt.若从对应到L2C翻译后的Clight代码角度来看,图5所示的结构体类型outC_tracker包含的域变量acg_fby4,对应于上述节点tracker所对应的类的属性变量pt.这种时态变量在L2C中是自动产生的新变量,比如对于图 3所示的程序,将会产生acg_fby1、acg_fby2、acg_fby3和acg_fby4,分别对应于该程序中的4个fby的时态变量f、c、ps和pt.

对于每个tracker实例中pt=0 fbyt的执行过程,Vélus和L2C的处理是类似的.在该实例执行的第1个激活周期开始时,会将相应于这一实例的时态变量pt的值置为0,而在之后的每个激活周期开始时会将pt的值置为前一个激活周期结束时pt的值.在每个激活周期的结束阶段,会将在该周期中已经计算好的t的值存入pt的存储空间,存入之后在该周期不会再有对pt的读取.

若从对应到翻译后的Clight代码角度来看,图4中省略了reset相关的部分,而从图5右半边上部的if语句来看,我们会发现:第1个激活周期(acg_init为1时)开始时,pt会被置为0,而在之后的每个激活周期开始时会将pt的值置为相应时态变量acg_fby4在前一个激活周期结束时的值.关于每个激活周期结束时对时态变量的修改,图 4中是由最后一句(∗self).pt=(∗out).t来完成的,而在图 5中是由倒数第 2句(*outC).acg_fby4=(*outC).t来完成的.

另外,L2C还支持三元的fby算子,其实现更加复杂一些.L2C的实现方案是将自动产生的新增时态变量(类似上述的acg_fby4)扩展为数组,其大小即为三元fby比起前面讨论的二元fby多出来的常量参数值.因Vélus目前不支持三元fby算子,所以我们不在这里讨论相应的翻译细节.

除了二元和三元fby算子,L2C还支持传统Lustre的时态算子pre.虽然Vélus目前未涵盖pre算子,但其实现与fby雷同.

(c) 同步数据流范型转换为串行命令式范型

在处理好前述几个核心同步数据流语言特征翻译的基础上,再解决好流数据对象的表示及其周期性处理的环节,基本上就实现了同步数据流范型向串行命令式范型的转换.在 Vélus中,这种范型转换体现在生成 Obc中间表示.相应地,在L2C中,这种转换导致了LustreC中间表示的产生.

Vélus的Obc是一种基于对象的中间表示,用于封装从同步数据流代码到命令式代码的翻译结果.在翻译到Obc时,每一个节点会对应到一个类.这个类中包含的属性有两类:一类是该节点中的所有时态变量(每个fby对应一个这样的变量);另一类是该节点中调用其他节点的实例(注:不允许调用到本节点的实例).这两类属性都是有状态的,即要维护其以前周期的历史信息(注:节点实例内部也可能有自己的时态变量).该类中包含的方法有两个:一个是reset,用于初始化时态变量属性以及调用实例,仅在第1个激活周期执行;另一个是step,用来执行该节点内部的所有等式,每个激活周期都会被重复调用.每个节点的输入输出参数以及局部变量均在 step方法中得以体现.

与 Vélus不同,L2C从同步数据流代码到命令式代码的翻译结果(LustreC中间表示),并未将每个节点对应的方法及reset方法与它们要处理的状态数据(时态变量和调用实例)封装在一起,而是采用了类似于C程序的组织方式.每个节点对应 C的一个函数,它的每个实例(对应于程序中实际调用该节点的位置)对应于一个结构体,其中封装了对应的时态变量和要调用的其他节点实例.为方便每个周期的循环调用,每个节点的输入输出参数变量也会被封装在一个该节点专用的结构体中,对于主节点要封装所有输入和输出变量,而对于其他节点仅封装输出.因为有可能有多个输出,所以对应到C时用一个结构体类型的变量存放多个返回值,所以,所有节点的输出变量均被分装在结构体中.主节点的输入变量要作为外部输入,为方便起见,也被封装在结构体中.同时,每个节点均有一个对应的reset函数.由此可见,虽然没有对每个节点对应的函数和reset函数以及它们要处理的数据对象进行封装,但这些内容均包含在生成的LustreC代码中,如同C语言的代码结构.

从翻译后的Clight代码可以看到一些具体的细节,如图4和图5所示.

(d) 翻译至Clight

综合前面几个核心同步数据流语言特征的翻译步骤,应该能够看明白从图 3所示的 Lustre源程序分别经Vélus和L2C翻译至图4和图5所示的Clight代码(二者虽然形式上不同,但体现的行为是相通的),从而也可以了解最后阶段的这一核心翻译步骤所起到的作用.

在这个阶段,Vélus就是将Obc中间代码的语法设法与翻译后的Clight代码的语法对应起来.L2C也类似,通过CtempGen完成从LustreC到Ctemp的翻译,又通过ClightGen将Ctemp中的memcpy语义翻译为内存拷贝函数,最终翻译至Clight代码.L2C后面这一步骤(从Ctemp到Clight)在Vélus目前的版本中没有对应的需求.这些翻译步骤的图示可分别如图1和图2所示.

5 同步数据流语义与翻译正确性验证

这部分内容的准确论述需采用形式化或半形式化方式,但受限于篇幅,本文仅就其要点进行非形式描述.

(a) 同步数据流语义

在从Lustre到C的转换过程中,经历了同步数据流语义逐步向串行命令式语义的过渡.在现阶段,Vélus的动态语义的形式化定义是从SN-Lustre中间表示开始的,在Obc,中间表示被变换至一种基于对象的串行命令式语义;相应地,L2C的动态语义形式化定义是从LustreS中间表示开始的,在LustreC,中间表示彻底变换为一种类C的串行命令式语义.这些中间层语言所处位置,如图1和图2所示.

可以看出,Vélus的同步数据流语义消去仅在一个阶段完成,而L2C则经历了多个阶段逐步消去.由于L2C的源语言特征相比Vélus要复杂很多,实践过程决定了跨多层的语义过渡是必然的选择.

Vélus在定义 SN-Lustre语义时已完成排序(scheduling),因此无需考虑同步数据流语言的数据流并发特性.L2C是在LustreS层进行排序(toposort),在LustreS层有串行语义定义(节点内部的所有等式相互之间存在全序关系),同时也定义有超粗粒度的并发语义(以等式为粒度,等式操作是不可分割的原子操作,等式之间存在由数据依赖所确定的偏序关系).

Vélus和L2C的同步数据流语义都选择了基于操作语义来定义(虽然也存在看似很不错的基于指称语义的基础工作[33]).在Lustre语言的原始论文[11]中,作者给出了Lustre语言的基本操作语义规则.Vélus和L2C的操作语义定义首先要与学界公认的这些工作相符,同时也应考虑实现的因素(交互式定理证明的方便性).比如,采用Coinductive来定义流看似是非常自然的(因为要处理的是 infinite对象),然而无论是Vélus还是L2C均放弃选择这种方法,L2C团队当初遇到的问题主要是因为采用Coq实现整体任务需求的技术难度无法预测.

在Vélus和L2C的同步数据流语义中,对于流数据对象的基本理解是一致的,均将其看作是从自然数到取值论域的函数.比如,可以将一个流s在第n个周期的值记为s(n).然而,在具体实现上,L2C采取了一些不同的措施.特别是针对同步数据流语义中最具代表性的fby算子.

在定义fby算子的语义时,Vélus使用了一个辅助算子hold,会将所处理的流数据对象在上一个激活周期的取值保持到其后续的无效周期,这样,若当前周期是激活周期,则fby运算的结果就相当于当前周期hold运算的结果.这一思想在 L2C项目开展的初期用来实现一种时钟归一化(clock unifying)算法[34],其中定义了类似于hold的算子,并用来刻画fby算子的语义.然而,在后来的工作中,L2C摈弃了这种做法.主要原因是,这种方法仅适合于定义二元fby算子,而难以推广到实际应用中很有用的三元fby算子.L2C对二元和三元fby算子的语义定义采用了一致的框架,定义一个大小为n的循环缓冲区,并设法限定仅在激活周期可访问缓冲区,这里,n即为三元fby算子的第3个参数(对于二元fby算子,n=1).

定义同步数据流语义的另一个重要方面,就是语义环境中要保留子环境的状态,这些子环境对应于当前环境下调用其他节点而形成的实例环境.保存这些子环境的原因是因为存在时态变量(见第4.2节),需要保存历史状态,这就导致了在调用的节点实例返回时不能像传统的函数调用那样释放掉变量的存储空间.因而,我们必须要定义并维护一个树状的语义环境,这对语义定义以及相应的证明来说,难度增加了许多,但这是我们必须要应对的.L2C在定义语义时对是否是时态变量进行了区分,以方便对应到Clight的语义环境中.Vélus在文献[15]中对这种树状语义环境也有许多描述,但仅从论文无法了解其进一步的实现详情.

另外,L2C因支持高阶迭代算子以及更多的数组和结构体算子,使语义定义的难度增大许多,但相关细节不属本文所要讨论的范围.L2C的多阶段翻译架构(如图 2所示)正是为了适应各种各样的语义复杂度以及与Clight语义之间的巨大差异,同样,图2所示的许多翻译步骤也不在本文所讨论的议题之内.

(b) 翻译正确性验证

在形式化定义动态语义阶段,Vélus和L2C的各阶段翻译正确性的验证目标与CompCert所建议的阶段翻译正确性目标从形式上是一致的,都是要证明一种从高层到低层单向的语义模拟等价关系.这种模拟等价关系之所以可以是单向的,是由于每一层语言均具有确定的语义(deterministic semantics).

对于同步数据流语义来说,这种单向的语义模拟等价关系可大致描述为:任意数据流程序G的每个节点f,若可以将输入流xs映射到输出流ys,则对于翻译后得到的程序G′中与f对应的节点或函数f′以及这一层次中相应于G′的初始化函数reset,如果G′在其第1个激活周期先执行reset后执行f′,而在其他后续激活周期中都重复执行f′,那么同样可以将xs映射到输出流ys.注意:这一命题中的G、f、xs和ys都是任意的.

虽然各阶段要证明的单向语义模拟等价关系形式上看都是相似的,但具体到不同阶段,其含义却都有所不同.首先,各个阶段的语法和语义互不相同;其次,每个阶段可能有或没有语法层面的reset函数,如果有的话,不同阶段的reset函数也可能有所不同;以及还有其他各种不同,这里不再赘述.

一般来说,从 Lustre源程序到 Clight程序的各阶段翻译过程中,同步数据流语言的语法及语义特征逐渐被消去,C语言语法及语义特征逐渐增加.在定义上述单向语义模拟等价关系时,所消失的语义特征描述通常会由新增加的语法特征来弥补.比如前面提到的 reset特征,在较高的语言层次,语法层面并没有对应的函数,所以是在语义定义中体现其行为,而在靠后的语言层次(比如图2所示的LustreE2层)已有语法层面的reset函数,就不会也不可能通过语义定义来体现reset行为.

因Vélus和L2C的编译框架之间差异较大(如图1和图2所示),可以想象到二者在翻译正确性验证方面存在较大的差异.这种差异体现在各个方面.这里仅列举一例.如果考虑第4.1节～第4.3节提到的核心翻译步骤,在Vélus中仅由Translation一个阶段完成(如图1所示),而在L2C中则是分散到从LustreR1到LustreD的许多阶段实现的(如图2所示).一般来说,一个翻译阶段所负责的工作越多,其正确性证明的难度也越大,重用性也越差.然而,另一方面,翻译阶段也不能太多,否则会导致语言层次增加太多,反而加重维护的负担.因此,应根据源语言的规模合理设计翻译阶段的数量.

Vélus中SN-Lustre之前的阶段未定义动态语义,这些阶段所保持的特性主要是静态方面的.多数这些阶段,甚至从 SN-Lustre到 Obc的过程(Translation),基本上是继承前人(Bertails、Biernacki和 Auger等人)的工作.Bourke等人的论文[15]对这些静态语义相关阶段的介绍很少,同时,Vélus未开源,所以具体继承情况的详情未能很好地得到了解,从Biernacki和Auger等人的论文[14,27]仅可了解到其中的一些.

Vélus的语法分析器是Bourke等人重新写的,它基于Jourdan等人提出的对LR(1)自动机进行确认并对确认程序进行验证的方法[35],因此可以认为是一个经过形式化验证的语法分析器.L2C中,最近刚完成与此平行的工作[32],并以编译选项的方式集成到了开源L2C编译器[31]中.

对于 Vélus中的类型、时钟检查(elaboration)以及接下来的规范化过程(normalization),仅了解 Bertails、Biernacki和 Auger等人在 Coq中实现了这些过程以及进行了验证,但他们的论文中未提到是如何进行验证的.L2C中与此对应的过程(LustreWGen、LustreVGen和 LustreSGen)的验证在目前的开源版本中尚未发布,相关工作仍在完善和整理之中.这些翻译过程在Vélus和L2C编译框架中所处位置,如图1和图2所示,下同.

Vélus对于排序过程(Scheduling)的验证是基于翻译确认的方法[16],具体实现在相关论文[14,15,27]中未加介绍.L2C中的排序过程(Toposort)是经过严格形式化验证的,证明了经过排序后的LustreS程序的串行语义行为,与排序前LustreS程序的等式粒度并发语义所刻画的行为是兼容的.从实现角度来看,对排序过程的形式化验证要比翻译确认的工作量大很多,所以从通常的观点来看,是否有必要这样做是值得商榷的.但 L2C的这项工作,对于在项目开展初期积累团队成员在使用Coq进行编程和验证的经验以及检查LustreS操作语义定义的合理性等方面起着重要的作用.

6 实现与性能

Vélus和L2C的开发环境与CompCert[2,36]一致,有验证需求的部分均在Coq[3,37]工具之中实现,并自动抽取得到相关的 Ocaml代码.词法分析器的 Ocaml代码由 Ocamllex自动产生.语法分析器使用了 Ocamlyacc,或者Menhir[38],前者针对未经验证的语法分析器选项,后者针对经过形式化验证的语法分析器选项.驱动程序以及其他辅助工具(如各层的语法树或代码的格式输出程序)通过手工编写Ocaml代码实现.

由于Lustre没有标准测试集,在Bourke等人的论文[15]中从前人相关工作中选取了14个有代表性的程序进行性能测试,在开源OTAWA框架[39]下,对Vélus以及其他一些Lustre编译器(Lustre V6和Heptagon与CompCert或者GCC的组合)的最坏执行时间(worst-case execution time,简称WCET)指标进行了测试评估.CompCert的版本是2.6,GCC的版本是4.8.4,目标体系结构是armv7-a(含硬件浮点单元vfpv3-d16).

我们从Bourke那里获得了文献[15]中使用的全部14个测例程序源码,并在与上述测试环境基本相同的配置下(配置选项为-march=armv7-a-mfloat-abi=softfp-mfpu=vfpv3-d16),针对L2C完成了测例程序的评估测试.我们将得到的测试结果汇总于表2.

表2中的第1列是14个测例程序的名称,第2列是L2C和CompCert 2.6组合编译器的测试结果(WCET值),第3列是从文献[15]中摘录的Vélus测试结果,第4列是L2C和GCC4.8.4(加-O1优化选项)组合编译器的测试结果,最后一列是Lustre V6和GCC4.8.4(加-O1优化选项)组合编译器的测试结果.

Table 2 WCET estimates in cycles for an armv7-a/vfpv3-d16 target表2 周期为单位的WCET评估值(目标处理器:armv7-a/vfpv3-d16)

从表2的结果粗略来看,L2C+CompCert的性能比Vélus低50%左右.L2C性能不如Vélus的原因,目前能想到的主要是因为Vélus在Obc中间表示进行了if语句的Fusion Optimization优化(如图1所示),而目前L2C未作任何优化,CompCert目前也没有支持有关的优化.

附件A.1和A.2分别给出了测例程序tracker(源码如图3所示)经Vélus和L2C编译生成的Clight代码,如图4和图5所示.从图5可以看出,L2C生成的代码中包含了大量可融合的if语句.从图4可以看出,Vélus生成的代码中时钟相同的操作已被合并到相同的条件分支下.

表2的第4列给出了L2C和GCC4.8.4(加-O1优化选项)组合编译器的测试结果.从中可以看出,测例程序tracker的WCET值比起第2列有显著降低(由1 035降至580),其他测例程序的情况也是如此,性能也优于Vélus的测试结果(见第3列).在GCC的“-O1”优化选项中,包含了针对if语句的“-fif-conversion”优化,可以缩短if-then语句所花费的时间.

Lustre V6编译器设计时也未过多考虑相关优化,主要是寄望于C编译器会负责这些优化工作(L2C也曾有类似的考虑,但更主要的是在开发L2C企业版时,用户方出于可追溯性的硬性要求,原则上不允许对代码进行编译优化,这种理念一直延续至今,但不一定适合各种场合).从文献[15]的测试结果(如该文中图12第6列所示)看,Lustre V6和CompCert组合的编译器对于各测例程序的WCET性能指标均不如L2C和CompCert组合的编译器.目前,我们对Lustre V6和CompCert组合编译器的性能测试工作也在进行之中.

7 总 结

Vélus和 L2C都是基于辅助定理证明器(Coq)构造 Lustre可信编译器的长线项目,它们都是先将源语言翻译至Clight,并与CompCert编译器实现衔接.Vélus和L2C课题组在立项目标、发展过程和方向、源语言需求以及工作基础等方面都不同,因而导致Vélus和L2C编译器在许多方面有明显的差异,形成了各自的特色.

本文从基本情况、源语言特性、编译器结构、核心翻译步骤、同步数据流语义与翻译正确性验证以及实现与性能等多个角度对Vélus和L2C进行了较为深入的分析与比较.当然,也不排除漏掉一些比较重要的方面,今后会通过其他机会加以补充.

据Bourke介绍,Vélus项目组近期在开展将有限自动机融入 Vélus的研究工作.Scade[8]工具中包含对有限自动机的支持,其目的是增加控制流特性.L2C项目组目前尚无计划开展类似的工作.

附录

A.1

例:Vélus生成的Clight代码.如图4所示.

A.2

例:L2C生成的Clight代码.如图5所示.