Lustre V6相关资料

Lustre V6编译器的相关资料，慢慢学习。

参考网站：

https://www-verimag.imag.fr/Lustre-V6.html?lang=en

源文件包：

https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/lustre-v6

工具手册：

https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox/#orgcd4ce3a

Lustre V6的语法规则和参考手册的文档已下载至本地：

C:\Users\huiyu\Desktop\每周任务\2021-8-1-从Lustre语言到C语言\Lustre V6。

https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/doc/lustre-v6-tutorial.pdf

Lustre

安全攸关的嵌入式领域广泛使用基于Lustre语言描述的图形化逻辑。工程师通过图形化逻辑建模工具编写控制逻辑，再通过代码生成器把控制逻辑转换成可执行代码下装到嵌入式设备中运行。

安全攸关的嵌入式控制领域（如核仪控、轨道交通等领域）常使用基于 Lustre 语言描述的图形化逻辑建模工具（如 SCADE 等）来开发控制逻辑，然后使用代码生成器将控制逻辑翻译为 C 代码。

Lustre 作为一种同步数据流语言，多用于嵌入式控制系统和信号处理系统。它在工控领域主要用于描述实时控制逻辑，核仪控、航天航空、轨道交通等安全攸关领域广泛使用的 SCADE Suite 就是基于 Lustre 语言描述实现的。

Lustre 语言具有数据流特征和确定性语义，适用于反应式控制系统编程、模块化的代码生成以及程序的形式化验证。Lustre 程序是由一系列的 node 或 function 声明、常量声明和数据类型声明组成，node 或 function 是用于处理输入流并输出的函数，node 体是由一系列等式组成。与串行命令式语言（如 C 语言）相比，具有许多独有的特征。

代码生成器

基于前人对 Lustre 语法语义及性质的研究基础上，法国 INRIA 的 Poute 团队和清华大学计算机系的 L2C 团队利用对代码生成器本身进行证明的方式，各开发了一款用于学术研究的 Lustre 到 Clight 的代码生成器，分别为 Velus 和L2C。Vélus 编译器目前未开源。

Velus架构:

Velus、L2C和SCADE的特性比较：

小结：

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

参考文献：

[1]兰林,马权,侯荣彬,蒋维,杨斐.Lustre语言可信代码生成器研究进展[J].仪器仪表用户,2020,27(05):68-72.

Lustre V6

Aerospatiale、Merlin-Gerin以及 Verilog 联手启动了新工具(Scade)的开发计划。当时，Verimag 实验室建立了 Verilog 公司和 Lustre 项目组合作的一个共同实验室，专攻 Scade 的设计，并由 Lustre 项目组的 Pilaud 领导 Scade 团队。再后来，Scade 又吸收了其他公司的一些技术，并经多次转卖，目前全球闻名。

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

Lustre V6是学术Lustre编译器的最后一个版本，具有类似ada的包机制、结构化数据类型（枚举、结构）、数组迭代器和静态递归。

对比

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

[2] Bourke T, Brun L, Dagand PÉ, Leroy X, Pouzet M, Rieg L. A formally verified compiler for Lustre. In: Proc. of the Programming Language Design and Implementation. 2017. 586-601.

参考文献：

[3]康跃馨,甘元科,王生原.同步数据流语言可信编译器Vélus与L2C的比较[J].软件学报,2019,30(07):2003-2017.

Lustre V6 Tools

程序举例 : https://github.com/jahierwan/lustre-examples

编译Lustre V6程序

Lustre V6编译器名为lv6。lv6从.lus文件默认生成lic代码。lic表示“Lustre内部代码”，总的来说，lic是去除了所有泛型和语法性的Lustre V6。

例如edge.lus文件如下：
1
2
3
4
5
6
7
8
node edge (X: bool) returns (Y: bool);
let
Y = r_edge(X) or r_edge(not(X));
tel
node r_edge (X: bool) returns (Y: bool);
let
Y = false -> X and not pre(X);
tel
这是一个Lustre程序，用于检测布尔流的边缘（上升或下降）。如果要从Lustre程序生成lic，只需调用：
1
lv6 edge.lus -lic -n edge
*注意，设置顶级节点的**-node选项**（简称-n）是必需的。
1
2
lv6 edge.lus -node edge
lv6 edge.lus -n r_edge
生成lic代码不是很有用；可以使用**-2c生成C代码**：
1
lv6 edge.lus -n edge -2c
运行Lustre V6程序

对lv6 edge.lus-node edge-2c的调用不仅生成C文件：它还生成一个edge.sh脚本，可用于生成edge.exec二进制文件。edge.exec文件可以通过-cc（–compile-generated-c）选项直接生成。
1
2
lv6 edge.lus -node edge -2c -cc
./edge.exec
也可以通过-exec选项使用嵌入在lv6中的解释器。
1
2
rm -f edge.rif
lv6 edge.lus -node edge -exec -o edge.rif
在这两种情况下，都需要通过键盘输入数据，也可以通过luciole rif使用基于tcl/tk的GUI：
1
2
luciole-rif lv6 edge.lus -node edge -exec
lv6 edge.lus -node edge -2c -cc; luciole-rif ./edge.exec
*注意：luciole-rif
- 需要安装V4工具集。
- 可以与遵循RIF约定的所有工具一起使用（有关更多信息，请参阅luciole RIF-h）。
使用V4工具集

通常可以使用V4工具集执行和编译V6程序，使用*-lv4或-ec*：
1
2
lv6 edge.lus -node edge -lv4 -o edge_v4.lus
lv6 edge.lus -node edge -ec -o edge.ec
接下来应该能够使用V4工具集：lus2ec、ecexe、ec2c、ecverif等。

V4工具集参考手册： https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/lv4-html/index.html