有关翻译正确性验证的重点疑难问题及其设计实现方案
在L2C可信编译器的设计与实现中, 对于实线所对应的翻译过程 (CompCert编译器除外) 均借助于Coq证明了正确性 (语义保持性), 然后得出LustreSGen所产生的LustreS代码到Clight代码整个翻译过程的正确性.从LustreS到Clight的任意两个中间语言***S***和***T***(设***S***在前) 之间的语义保持性可描述为
| ∀P.sound§⇒sound(τ§)∧SS§≈ST(τ§),∀P.sound§⇒sound(τ§)∧SS§≈ST(τ§), |
其中, τ是翻译函数, 可将S中间语言的程序P翻译至T中间语言的程序τ(P); SS是S中间语言的语义函数, ST是T中间语言的语义函数; sound(P) 和sound(τ(P)) 分别刻画翻译前后的程序应满足的一些Well-formedness性质 (比如第5.4节所述的左右值不相交的性质.另外, 各层中间表示的性质会有所不同), 用以将各阶段翻译过程的证明串连起来得到整个翻译过程的语义保持性, 同时保证在每一阶段可以正常得到SS(P) 和ST(τ(P)); ≈是单向模拟等价关系:SS(P)≈ST(τ(P)) 意味着:P的所有环境变量在τ(P) 都有匹配对象, 且SS(P) 对环境的改变可以由ST(τ(P)) 对相匹配环境的改变进行模拟.对于合法的LustreS程序, 求值结果总是确定的, 这意味着语义计算的确定性 (在非串行语义的情形, 不同求值过程的结果也是确定的).因此, 证明上述单向模拟关系就足够了.全数字实时仿真软件SkyEye与可信编译器L2C的核心翻译步骤的设计与实现
这一验证目标看似比较明确, 然而在具体设计和实现时, LustreS到Clight的验证过程很复杂, 会遇到许许多多的疑难问题.一方面是因为这两种语言差异非常大, LustreS自身有很多独特的特点; 另一方面是因为形式化验证的特点决定证明的过程可能会经过多次反复.限于篇幅, 本文有选择地与读者分享在实际的设计和实现过程中遇到的一些重点疑难问题以及采取的具体方案, 首先讨论若干共性的问题, 然后再针对前一节提到过的核心翻译步骤详细加以说明.
1 整体证明框架的定义
形式化验证的特点决定了工作最难点在于整体证明框架的定义.形式化证明虽然能够为验证的正确性提供可靠保证, 但验证过程的可复用性、可移植性差.如果在整体框架的定义上出现问题, 即使是微小的问题, 也可能造成整个证明过程需要推倒重来.所以, 如何定义证明框架是能否完成证明的基础, 这直接决定了整体证明的工作量.
为了解决证明框架的定义问题, 我们在总结经验后采取了逆序分层验证的方式.一是由正常的LustreS到Clight的顺序验证, 改为由Clight到LustreS的逆序验证过程.二是尽量将翻译过程拆分为小的步骤, 每步只完成1个功能, 使每一步的的验证尽量简单, 以减少出错的可能性.
2 语义值和语义环境的定义
Lustre*的操作语义定义是实现L2C编译器中主体翻译阶段正确性验证的基础, 而语义值和语义环境又是操作语义定义的基础.
在实现L2C编译器的证明过程中语义值的定义反复经过多次改动.每次改动都给证明过程带来很大的影响.最初Lustre语义值的定义与Clight相差非常大, 这一方面导致Lustre在自身的简化证明过程中难度很大, 另一方面又导致很难和Clight进行对接.最开始的定义尤其在Lustre语义值的写入和读取时, 不支持读写范围的限制, 这导致最后和Clight对接时, 无法提供相应的条件.经过多次证明的反复修改, 最终决定让Lustre语义值的定义尽量接近Clight, 这样一方面可以吸收Compcert的成功经验, 另一方面减少语义值的差异能够简化证明的过程.
3 ID管理
翻译过程中可能产生大量的中间变量, 而且翻译的层数比较多.如何定义程序中已有的id集合不重复, 如何保证翻译新生成的id集合不重复, 以及如何保证新生成的id集合与已有id集合不相交, 是贯穿整个验证过程的问题.为了解决这个问题, 我们对整个翻译过程中的id进行了分类:程序自带的id、翻译新增中间变量的id、预定义id以及特殊预定义的id.
4 左右值不相交的保持性证明
这一难点是在CtempGen的证明中处理结构体和数组类型的赋值运算时发现的.结构体和数组类型赋值运算要翻译为Ctemp中memcpy运算, 这需要有一个对地址范围的限制:要么源地址和目的地址的指针不同, 要么源地址和目的地址的偏移量不同, 要么源地址范围和目的地址范围不相交.而Lustre中不存在指针, 在这一步的证明之前也没有对Lustre赋值运算左右值的地址进行限制, 所以需要定义Lustre中赋值的左右值地址不相交.后来发现在call运算中也存在类似的问题.由于地址不相交性质贯穿Lustre的所有层, 还涉及call运算, 所以带来的工作量非常大.尤其是在部分类型节点的输入和输出参数需要被翻译成结构体的情况下, 这时结构体变量的地址相同, 要证明其偏移范围不相交, 证明过程很复杂.又因为这个定义涉及对表达式的地址求值, 这也增加了证明的工作量.
5 程序初始化及reset函数的证明
Lustre*程序的主节点和节点列表都有对应的reset函数, 主要用于初始化时态运算中所需的第1周期标识变量acg_init.Reset函数的生成和证明本身难度不大, 难点在于在哪些层生成reset函数.Reset函数的生成位置选择不对, 会使证明难度加大, 还可能因为提供的条件不够造成无法证明.经过多次试证, 才发现节点类reset函数的生成ResetfuncGen放在返回值分类ClassifyRetsVar之后最合适.因为返回值分类后, 将需要翻译为输出结构体的变量都归为一类, 这为reset函数的翻译证明提供了合适的条件.而且reset函数翻译后, 和普通节点类型统一起来, 后续不必单独证明reset函数.reset函数和程序初始化紧密相连, 都是贯穿整个证明的过程, 整体证明的工作量也较大.
6 拓扑排序Toposort的证明
经过预处理的LustreS程序是未经排序的.需要对节点列表和每个节点内的等式列表进行排序.使排序后的程序的执行按顺序语义执行, 为后续证明提供条件.其中, 节点的排序能够为后续只翻译单个节点时的证明提供条件.这一部分的证明分3个方面:(1) 排序后的程序和排序前的程序是同一个程序的排列; (2) 排序后的程序满足拓扑排序的性质; (3) 对同一程序经排序后, 任意两个满足拓扑排序性质的程序按照LustreS顺序语义执行的结果是等价的.当前版本中定义了LustreS的并发语义, 从并发语义到顺序语义的语义保持性证明本质上与这3个方面的证明是等效的.
7 高阶算子与嵌套时钟消去过程LustreRGen的证明
为了描述Lustre*复杂的高阶运算, 以及mix等各种特殊运算, LustreS的语法定义比较复杂.LustreS中的高阶运算以及各种特殊运算实际上是由多种简单运算组合而成.比如, 普通的高阶运算可以化简为for循环运算; mapw等特殊高阶运算可以化简为for循环和if运算的组合; flatten运算可以拆分为多个赋值运算的序列; aryprj运算可以拆分为if语句和赋值运算的组合.高阶算子消去的作用就是将LustreS中各种复杂运算拆分为多步简单运算.另外, 嵌套时钟的消除仅需要在等式/语句之前添加相应的条件语句.LustreRGen翻译的过程不产生中间变量, 其证明不涉及环境匹配的问题, 因为翻译前后执行环境都完全相同.但因为需要拆分的复杂运算比较多, 部分复杂运算的拆分过程比较复杂, 使得证明的过程虽然不是很难, 但证明的量比较大.
8 时态算子消去过程LustreFGen的证明
这一层的翻译主要是消去节点列表中的时态运算, 这也是整体翻译和证明的难点.但通过前面一系列的分类和简化, 使得这一部分的证明得以完成, 需要处理3个时态算子fby, fbyn和arrow, 而且以语句的形式独立呈现.全数字实时仿真软件SkyEye与可信编译器L2C的核心翻译步骤的设计与实现
Fby语句的来源分为两部分, 一是由arrow (→) 和pre算子转换过来的, 二是fbyn中n为1的语句.Fby和fbyn的翻译需要生成后置赋值等式 (参见第5.7节的示例), 负责延续历史值的生成.Fby的翻译比较简单, 通过第1周期标志变量FLAGID, 生成主体的if分类赋值语句, 再生成预定义的中间变量和后置赋值等式.Fbyn语句的翻译较为复杂, 因为其历史值是存放在对应的数组当中的.在第1周期是需要利用for循环对其进行初始化; 在后续周期循环取数组对应位置的值; 后置等式要对fbyn下标进行模加运算, 还需循环更新对应下标的值.Arrow的翻译比较简单, 通过第1周期标志变量FLAGID, 生成if分类赋值语句即可.
9 LustreC到Ctemp的证明
LustreC到Ctemp翻译过程CtempGen的证明是整个证明过程中工作量最大的, 也是最难的证明.由于证明的量过大, 不得不分成两部分, 第1部分主要是完成一些基本定义和底层证明, 第2部分完成主体的证明.这里我们抛开翻译细节, 主要分析一下证明量大的原因并描述解决方案.
首先是语义环境的差异较大.LsemC的语义环境主要包括全局常量环境gc、存储节点本地变量的环境te、存储节点输入参数变量的ta和存储输出参数的se.Ctemp的环境主要包括全局环境ge、存储节点本地变量地址的环境eC、存储输入参数的环境leC、存储输出参数的环境teC和存储数据的内存mem.其次, 输出C代码的规范要求造成证明分支多.第三, Ctemp语义环境内的隔离性定义.最后, 函数和语句的互归纳证明.所有各层的节点和语句的证明都要通过互归纳的方式来实现.
高性能嵌入式仿真软件SkyEye
随着科技的发展，系统工程的设计体量逐渐庞大起来，尤其是对于轨道交通、航空航天、核电站等安全关键领域中，如何在复杂度逐年变大的同时保证其安全性和可靠性，是近年来各大公司需要研究的课题。最近比较火热的基于模型的系统工程（MBSE）技术则给大家提供了一种全新的技术方向，分享一种全数字实时仿真的安全关键领域解决方案，提供一种新的解决思路。全数字实时仿真软件SkyEye与可信编译器L2C的核心翻译步骤的设计与实现，提供高效的运算速度，提高研发效率和安全性。
新一代全数字仿真平台SkyEye
基于模型的全数字研发解决方案MBSE工具软件SkyEye是能够满足模拟或仿真外部硬件行为进行软件运行和测试需求的工具。该工具运用国际流行的仿真、测试脚本语言来编写外部硬件逻辑行为所产生外部激励事件以构成嵌入式软件的外部信号激励或数据输入，从而满足软件在全数字仿真运行环境下无须人的干预而闭环运行的要求。全数字实时仿真软件SkyEye与可信编译器L2C的核心翻译步骤的设计与实现
作为基于嵌入式应用的特点，嵌入式软件全数字仿真测试支撑平台SkyEye要为嵌入式系统提供全数字仿真测试环境或测试平台，实现对嵌入式系统进行实时、闭环的系统测试。在该平台上完成被测软件的分析、运行和测试，最重要的是要实现嵌入式系统外部事件的全数字仿真平台，使得嵌入式软件就像在真实硬件环境下连续不中断地运行。
本文标题：高性能嵌入式仿真软件SkyEye
本文链接：http://www.digiproto.com
