2019同步数据流语言可信编译器V&#233-康跃馨 , 甘元科 , 王生原.pdf

上善若水

481

15页

1次

2022-05-23

免费下载

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software,2019,30(7):20032017 [doi: 10.13328/j.cnki.jos.005755] http://www.jos.org.cn

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



康跃馨

甘元科

王生原

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

通讯作者: 康跃馨, E-mail: kyx16@mails.tsinghua.edu.cn

摘要: 同步数据流语言(如 Lustre、Signal)在航空、高铁、核电等安全关键领域得到广泛应用.例如,适合这些

领域实时控制系统建模和开发的 Scade 工具就是基于一种类 Lustre 语言.这类语言相关开发工具,特别是编译器的

安全性问题也自然受到高度关注.近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点

之一,也取得了瞩目的成果,如 CompCert 项目实现了产品级的可信 C 编译器.同样,人们也采用这种方法开展了同步

数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目,二者均研发面向基于 Lustre 的同步数

据流语言编译器,分别以 Vélus 和 L2C 代称.对 Vélus 和 L2C 从多个重要的角度进行较为深入的分析与比较.

关键词: 同步数据流语言;形式化验证的编译器;Lustre 语言

中图法分类号: TP314

中文引用格式: 康跃馨,甘元科,王生原.同步数据流语言可信编译器 Vélus 与 L2C 的比较.软件学报,2019,30(7):20032017.

http://www.jos.org.cn/1000-9825/5755.htm

英文引用格式: Kang YX, Gan YK, Wang SY. Comparison of two trustworthy compilers Vélus and L2C for synchronous

languages. Ruan Jian Xue Bao/Journal of Software, 2019,30(7):20032018 (in Chinese). http://www.jos.org.cn/1000-9825/5755.

htm

Comparison of Two Trustworthy Compilers Vélus and L2C for Synchronous Language s

KANG Yue-Xin, GAN Yuan-Ke, WANG Sheng-Yuan

(Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China)

Abstra ct : Synchronous data-flow languages, su ch as Lustre and Sign al, have been widely used in s afety-critical industrial areas, such as

airplane, high-speed railways, nuclear power plants, and so on, for example, Scade, a tool suitable for modeling and developing a

real-time control systems in those areas, is based on a Lustre-like language. Naturally, the safety of development tools, especially

compilers, for such languages, has been paid highl y attentions. In recent years, the construction of a trustworthy co mpiler based on f or mal

verification has become one of the research focuses in the field of programming language, and remarkable achievements have also been

achieved, for example, a product level trustworthy C compiler has been developed in the CompCert project. Similarly, this method has

been used to develop the trustworthy compilers of a synchronous data flow language. Two long term projects for such research work,

called Vélus and L2C respectively in this study, are focused here. Either of them has been developing a compiler for a Lustre-like

synchronous data-flow language. The analysis and co mparison are d eeply carried out in t erms of various poin ts between Vélus and L2C.

Key words: synchronous data-flow language; formally certified compiler; Lustre language

应用于航空航天、高速铁路、核电能源和医疗卫生等领域的安全攸关系统

[1]

一旦失效,将给人类生命财产、

社会生产、生活环境带来巨大的破坏.如何为安全关键系统构造一个基础的安全软件环境是需要面对的首要问

 基金项目: 国家科技重大专项(MJ-2015-D-066)

Foundation it em: National Science and Technoloy Major Project of China ( MJ-2015-D-066)

本文由“软件形式化验证”专题特约编辑贺飞副教授、张立军研究员推荐.

收稿时间: 2018-07-15; 修改时间: 2018-09-28; 采用时间: 2018-12-13; jos 在线出版时间: 2019-03-28

CNKI 网络优先出版: 2019-03-29 09:14:24, http://kns.cnki.net/kcms/d etail/11.2560.TP.20190329.0914.007.html

2004

Journal of Software 软件学报 Vol.30, No.7, July 2019

题,尤其是对操作系统、编译器等基础软件而言.

作为用来产生代码的工具,编译器的实现和维护自然经过了“精雕玉琢”, 因此编译器的正确性问题容易被

人们忽视.但了解实际情况的人都知道,编译器的“误编译”问题是司空见惯、习以为常之事.对于许多领域来说,

由于一般不会引发本质的问题,又是小概率事件,人们也往往容易忽视误编译所带来的负面影响.然而,对于安

全关键系统而言,则必须考虑因编译器引入的错误,否则,花大力气在源程序级的验证工作可能在目标程序级失

效.实际上,如航空领域的 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 是函数风格的语言,而 Signa l 是关系型的语言.这些同步语言各自的

特点有利于进行一些实质性的静态检查甚至于形式化分析和验证,从而有益于产生安全的代码.在基于同步语

言的开发工具中,最著名的是 Scade,其代码生成器 KCG 将一种基于 Lustre 的建模语言翻译到 C 语言,KCG 应

该是获得民用航空软件生产许可(DO-178B/C)的第一个商用代码生成器.目前,Scade 工具已渗透到我国航空、

航天、轨道交通及核电等若干安全关键领域.

与 C 语言编译器的情形类似,人们同样不会止步于像 Scade 这样的安全级代码生成器.基于高级建模语言

代码生成器的形式化验证近年来已受到极大关注.本文主要分析与比较两个关于同步数据流语言 Lustre 的可

信编译器项目,二者均采用如 CompCert 那样的方法对翻译过程本身进行验证.这两个项目是目前仅有的从事形

式化验证的 Lustre 可信编译器研发的长线项目,一个是法国 Pouzet 教授的项目组,另一个是作者所在的 L2C 项

目组.前者较早的工作

[14]

将具有 Lustre 语言关键特征的 Lustre 子集翻译至一种基于对象的中间语言,最近的工

作是将这一中间语言翻译至 Clight(见 CompCert 项目),并与 CompCert 衔接后称为 Vél us 编译器

[15]

.L2C 项目致

力于基于 Lustre 的语言到 C 语言的可信代码生成器(或称 L2C 编译器)的研发,从一开始便以 Cli ght 作为目标语

言,从而与 CompCert 实现对接.有关这两个可信编译器项目的进一步发展情况会在正文中详细介绍.为方便起

见,文中分别以 Vélus 和 L2C 代称这两个项目以及相应的编译器.

编译器形式化验证的另外一种重要方案是翻译确认(translation validati on),由 Pnueli 等人于 1998 年首先提

出

[16]

.翻译确认不是直接验证翻译程序,而是对翻译前后代码前的语义等价关系进行确认.比起直接对翻译过程

进行验证,这种方法具有较好的可重用性.然而,它必须是一个自动化的过程,因而从理论上决定了它可能出现

of 15

免费下载

软件学报计算机技术

关注

评论