1、核心翻译步骤示例
本节我们以第2节提到的Lustre语言的主要特性为线索来解释L2C在翻译过程中的关键节点是如何处理的, 并以图 1的实例来解释Lustre程序是如何被一步步地翻译到Clight语言的.
1.1 数据流并发性
Lustre程序具有数据流并发性, 而Clight程序却是串行执行的.因此, 翻译过程中的一大难题就是要将Lustre语句串行化.现在一般采用的因果分析和排序大多采用测试或翻译确认的方法, 未进行形式化验证.对于L2C构建经过形式化证明的可信编译器的目标, 对排序做严格证明是必要的.我们首先定义Lustre*中的因果关系.支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤
(1) 如果一个等式A的左值出现在等式B的右值中, 则说等式B依赖于等式A.
(2) 如果一个节点A的左值出现在等式B的时钟中, 则说等式B依赖于等式B.
然后, 我们定义拓扑排序的性质, 并且定义拓扑排序等价性定理, 即任意两个满足拓扑排序性质的程序在串行执行语义中是等价的, 以此来保证串行化方案的正确性.最后利用Coq实现拓扑排序算法, 将并行的LustreS串行化, 并以此算法完成之前定义的拓扑排序性质和语义等价性证明.
实际翻译效果以图 1中的第7行~第8行为例, 按照第1条因果关系的定义, 图 1中第8行的左值出现在了第7行的右值中, 所以第7行语句依赖于第8行.图 4显示了拓扑排序后LustreS程序中与图 1第7行~第8行对应的代码片段, 在排序后, 图 1的第7行被翻译为图 4中的第4行, 图 1中的第8行被对应到图 4中的第2行, 可见排序后的语句满足因果关系的定义.
1.2 高阶算子
Lustre提供了10多个高阶算子 (涵盖了LustreV6支持的所有高阶算子), 包括map, red等.图 1第10行使用了map算子, 本节以map为例来介绍高阶算子消去.Lustre中map算子的形式为map《op; size》(a1, a2, …, an), 其中, a1~an是n个输入数组, size为数组的大小; 而op为一个操作, 可以是运算符或一个节点, 拥有n个输入参数.map算子运算的结果为一个数组, 记为res, 其中, res[i]=op (a1[i], a2[i], …, an[i]).图 1中的p值展示了图 1第10行map算子运算的结果, 可见高阶算子简化了对数组的循环操作.
由于目标语言Clight不支持高阶运算, 所以在翻译过程中, 需要消去Lustre*中的高阶算子.基于高阶算子对数组处理的特点, 我们最终在LustreS到LustreR1阶段将所支持的各个高阶算子按其语义特性展开为Clight支持的语法结构, 主体为for循环结构.
图 5展示了图 1中第10行的map运算在LustreS这一层的中间表示, 可见, 在LustreS这一层L2C不会对map高阶算子做翻译.
经过LustreRGen过程, L2C会将map高阶表达式转换成for循环, 如图 6所示.
通过设计翻译算法将LustreS中的高阶复杂运算分解成LustreR1中多个基础运算的循环, 我们消除了Lustre*程序中的所有高阶算子.
1.3 时态和时钟算子
Lustre支持如LustreV6的一些可以操作流数据的时态算子, 如fby, 以及操作变量时钟的时钟算子, 如when算子.在Lustre程序中, 每个变量均有自己的时钟, 默认情况下为一个全局基本时钟, 该时钟在每个时钟周期都为True.如图 2中拥有全局基本时钟的x3, 在每个时钟周期都有值.而Lustre提供的when算子则可以用来改变某个变量的时钟, 如图 2中的y1, b为True的周期有值且与x3当前周期值相同, 但b为False的周期的值则是未定义.再如Lustre提供的fby算子, 可以用来访问流数据的历史值, 它不改变时钟, 返回值相当于向右shift流数据的值, 如图 2中的s, 它的值在y1上整体向右shift了一位, 并且在shift产生的空缺值中补上了fby函数指定的默认值5.支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤
L2C在LustreS到LustreR1阶段会处理所有时钟算子, 在LustreR3到LustreF1阶段会处理所有的时态算子.以fby算子为例, 在LustreF1中, 图 1中Stay节点内的第27行和第28行, fby算子会被最终翻译成如图 7所示的LustreF1代码, 其中a为Stay节点的输入参数.
L2C引入acg_init变量来标识当前周期是否为第1个周期, 如果是第1个周期, 那么将对变量m和n赋初值, 赋初值时会根据fby指定的周期数来初始化存储m和n的数组大小, 并在数组中对每个值赋予fby指定的默认值, 然后在之后的周期依次循环遍历数组的值, 并在每次读取值之后在数组当前位置记录变量在fby之前当前周期的值.以图 2的输入值为例, 我们将图 7中n对应的fby相关参数acg_fby2前4个周期的变化过程展示出来, 如图 8所示, 便于更好地理解图 7的翻译结果.
1.4 翻译至Clight
经过前面几个核心步骤后, 已经消除了Lustre中最显著的同步数据流特征, 程序已经十分接近常规的串行命令式语言.又经过后续若干个关键步骤 (包含初始化函数生成ResetfunGen) 到LustreC, 已经十分接近Clight, 经由最后两个步骤实现与CompCert完全对接 (如图 3所示).从LustreC到Clight的翻译过程中, 在语法上几乎没有太大的变化, 但在语义环境上差异较大, 证明工作繁重.图 9展示了L2C翻译图 1所示Lustre程序中Main节点的最终结果, 具体翻译验证的难点我们将在下一节详细描述.
1.5 流数据对象
如图 1所示, 主节点Main的输入和输出都是无穷长的流数据, 简单来说, 每个时钟周期, Lustre*程序以输入流数据当前时钟周期的值传入Main节点作为输入, 执行得到输出流中当前时钟周期的值.
由于程序获取输入和处理输出的方式不尽相同, 所以L2C只会翻译Lustre*程序中的节点, 并不会给最终的Clight程序中加入C语言的入口函数Main函数.在实际使用中, 如图 10所示, 我们会编写C语言的main函数循环调用调用生成Main函数, 以此来处理流数据.
高性能嵌入式仿真软件SkyEye
随着科技的发展，系统工程的设计体量逐渐庞大起来，尤其是对于轨道交通、航空航天、核电站等安全关键领域中，如何在复杂度逐年变大的同时保证其安全性和可靠性，是近年来各大公司需要研究的课题。最近比较火热的基于模型的系统工程（MBSE）技术则给大家提供了一种全新的技术方向，分享一种全数字实时仿真的安全关键领域解决方案，提供一种新的解决思路。支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤，提供高效的运算速度，提高研发效率和安全性。
新一代全数字仿真平台SkyEye
基于模型的全数字研发解决方案MBSE工具软件SkyEye是能够满足模拟或仿真外部硬件行为进行软件运行和测试需求的工具。该工具运用国际流行的仿真、测试脚本语言来编写外部硬件逻辑行为所产生外部激励事件以构成嵌入式软件的外部信号激励或数据输入，从而满足软件在全数字仿真运行环境下无须人的干预而闭环运行的要求。支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤
作为基于嵌入式应用的特点，嵌入式软件全数字仿真测试支撑平台SkyEye要为嵌入式系统提供全数字仿真测试环境或测试平台，实现对嵌入式系统进行实时、闭环的系统测试。在该平台上完成被测软件的分析、运行和测试，最重要的是要实现嵌入式系统外部事件的全数字仿真平台，使得嵌入式软件就像在真实硬件环境下连续不中断地运行。
本文标题：支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤
本文链接：http://www.digiproto.com
