[法兰西公学院] Esterel A到Z (Gérard Berry 2018)

2018年，Esterel技术创始人Gérard Berry在法兰西公学院讲授了《Esterel from A to Z》的系列课程，全面教授了他领导发明的Esterel技术。这里将叙述逐节课程的主要主题。详细内容，可参考完整视频Esterel A到Z

第一课：反应式编程的原理、思想与风格

本课程首先阐述了同步并行语言的诞生及后续发展动因 —— 这类语言专为所谓 “反应式” 系统编程设计，其核心功能是与外部环境保持持续且时间精准的交互。

随后，课程探讨了该类语言的演进历程，重点分析了其编程风格的发展脉络：从 20 世纪 80 年代中期诞生的初代 Esterel 与 Lustre 风格，逐步发展至 Esterel 技术体系下的工业级语言 SCADE 6。21 世纪初，SCADE 6 成为航空电子及其他计算机安全关键领域中 “经认证嵌入式系统” 的主流选择。该领域的技术进步，或源于新的科学发现，或由解决复杂工业问题的实际需求所驱动。

课程还强调了众多外部因素对同步语言的丰富作用 —— 尤其是图形化编程或文本 - 图形混合编程的引入，同时始终保持其与传统异步并行语言的显著差异。此外，课程对比了两种核心技术路径：同步方法通过数学理论与工程实践实现了并行性与行为确定性的统一；而其他路径试图将反应式编程与传统顺序编程或非确定性异步并行编程相结合，但这些方法的固有缺陷很快成为阻碍其大规模实际应用的严重障碍。

最后，课程展示了如何通过异步通信对同步组件进行高层级组装，进而构建全局异步 - 局部同步（GALS）系统。此类系统适用于机器人技术、片上电子系统及 Web 编程等多个领域。

第二课：同步语言的语义、因果关系与构造性

第二讲主要探讨同步语言的数学基础，尤其聚焦于 Esterel 语言，核心围绕程序中信息传递的因果关系概念展开。在同步框架下对因果关系的细粒度研究，催生出一系列粒度不断细化的形式语义；这一系列语义最终以构造性语义收尾，其不仅源于同名逻辑的思想，还得到了电路中电前沿传播相关物理考量的支撑 —— 这一物理考量已在 2013-2014 学年的课程中提及。

这些语义结构始终是 Esterel 语言各版本实际开发的基础，其理论支撑确保了各版本间的兼容性，并且在所有重要决策中起到了 “公正裁决” 的作用。不过，其他学者也开发了限制性更强的语义，以让 Esterel 的风格与经典语言更兼容。其中，弗雷德里克・布西诺（Frédéric Boussinot）设计的反应式 C 语言（Reactive C）是代表性起点，它以简洁优雅的方式将 Esterel 的部分概念融入 C 语言，并启发了包括 ReactiveML 在内的多种其他语言 ——ReactiveML 已在当天的一场研讨会上进行过介绍。

第三课：Esterel语言到电路的转换

第三讲介绍了如何将Esterel程序转换为经过优化的布尔电路。相较于以往基于自动机理论的方法，这是一次真正的概念革新。该方法诞生于与数字设备公司（Digital Equipment）让·维勒明（Jean Vuillemin）团队的合作过程中，当时该团队正致力于更好地对软件可重构电子电路（即现场可编程门阵列，FPGA）的控制部分进行规范。

这种转换方法立即发挥了重要作用，彻底解决了早期基于有限自动机生成的实现方案中存在的代码规模指数级增长问题——该问题曾严重限制了这些方案的应用。因此，Esterel目前已被工业界用于电子电路和嵌入式软件领域的商业应用，并催生了Esterel相关技术产业的诞生。

本讲内容限于无循环结构的程序，介绍了转换的通用原理、每条指令的转换方式，以及与构造性语义的关联。循环结构这一更复杂的情况将在后续课程中探讨。讲座最后回顾了2013-2014学年课程中介绍的布尔优化方法，这些方法能将电路优化到常规人工方法通常难以企及的性能水平。

第四课：Esterel语言中的循环与再生

本次课程致力于从Esterel程序生成高效的电路与软件代码。课程首先探讨了电路转换中的循环问题，该问题引出了指令再生这一极具挑战性的难题——即在同一次“反应”期间，同一条指令可能被连续且同时执行多次。这对解释器而言并无难度，但对于高效编译来说，部分此类指令必须被复制足够多的次数。

我们展示了如何逐步从一种简单却呈指数级复杂度的方法，过渡到工业编译器中所采用的二次复杂度方法，进而发展到准线性复杂度方法。同时回顾了为何即便电路中包含组合逻辑环路，构造性语义仍能确保电路的正确性。

随后，课程简要介绍了一种由哥伦比亚大学的斯蒂芬·爱德华兹（Stephen Edwards）提出的、针对软件目标的全新且效率更高的编译方法。在解决了指令再生问题后，该方法借助精妙的状态编码，以及“软件测试仅评估一个分支，而布尔传播在电路中始终遍历两个分支”这一特性，最终实现了比电路转换方法更优的性能，其性能甚至可能随程序规模增长呈亚线性提升。Esterel技术公司的Esterel v7工业编译器已实现该方法的一个变体，而我主导了该编译器的开发工作。

第五课：时钟门控、多时钟机制、实现与优化

本讲首先探讨了如何将 Esterel 程序（或广义上的同步程序）嵌入任意执行环境，详细阐述了执行机器在连接 Esterel 的本地同步世界与异步外部世界时，接收和发送事件的多种方式。此外，还详细介绍了用于调用和管理异步操作的 “exec” 原语 —— 该原语最初为机器人控制场景设计，且在第一讲中已简要提及。

随后，本讲基于 2014-2016 学年课程中介绍的程序验证技术，探讨了自动证明 Esterel 程序属性的多种方法，包括基于显式自动机的直接计算、利用 SAT/SMT 求解器的隐式验证方法等。工业界实例印证了仿真与自动证明开发的互补性，并凸显了后者的技术优势。