ESTEREL语言中引入的并发和Goto指令的理论计算机科学电子笔记

理论计算机科学电子笔记153（2006）55-70www.elsevier.com/locate/entcsGoto和并发在EsterelOlivier Tardieu1INRIA Sophia Antipolis，法国摘要E STEREL是一种用于实时嵌入式系统的设计语言。基于同步并发范例，它的语义将执行描述为一系列的计算时刻。在这项工作中，我们考虑在语言中引入一个新的gotopause指令，它充当与并发兼容的非瞬时跳转指令。它允许程序员在程序中的任何地方激活状态控制点，在下一个瞬间从那里继续执行。为了提供扩展语言的形式语义，我们首先定义了ESTEREL的状态语义，我们证明了它在观察上等价于原始的逻辑行为语义。在状态语义中包含gotopause就很简单了。我们勾勒出我们的新原语的两个关键应用：自动机的直接编码和消除精神分裂症行为的程序的准线性重写。保留字：同步语言，程序转换。1介绍ESTEREL[4，5，6，7，8]是一种面向高级控制的同步反应语言（第2节）。复杂的控制流程模式可以通过行为、测试、循环和抢占机制的顺序和并行组合来构建。这些都是结构性声明。没有跳转指令是可用的或容易编码在ESTEREL。这有很大的缺点，比如使自动机编码不自然地困难[1]。因此，向语言中添加类似goto的结构的可能性是一个争论的主题1电子邮件：olivier. sophia.inria.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.02556O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）551：暂停;行动1;出现A后进入顶2端，出现B后进入顶3端，进入顶1端，2：暂停;行动2;gotopause 1;3：暂停;行动3;gotopause 2Fig. 1. ESTERELsp中的自动机一方面，这样的扩展将产生一种更具表现力的语言，允许更紧凑的规范，并增强对自动机的支持。此外，大多数ESTEREL的编译器[4，9，11，16]都基于中间格式，语言或涉及跳转的表示，因此该指令的实现应该是直接的。另一方面，goto被广泛认为是一个坏主意[10]，特别是在ESTEREL这样的并发框架中，它们很容易破坏语义。此外，特定的正确性问题，如瞬时循环检测[18]可能会因为gotos而变得更糟。因此，据我们所知，没有成功的尝试，在这个方向上的扩展已被报道，提供了必要的正式背景和令人信服的实际应用。在 本 文 中 ， 我 们 详 细 介 绍 了 我 们 认 为 是 正 确 的 方 式 来 扩 展 ES-TEREL。我们在语言中添加了一条指令，我们称之为gotopause。暂停和gotopause指令现在都已标记。当控件到达某个“gotopause标签“时但是，当执行在下面的瞬间恢复时，不是从“gotopause label“位置重新启动从相应的“label：pause“位置开始这允许非即时地分支到程序的远程部分。由于非瞬时性，语义仍然足够简单，可以被定义和证明是足够的，以及理解和使用。由于分支的非局部性，这样的扩展通常需要某种延续传递风格的语义。在ESTEREL的情况下，我们首先必须以我们证明在观察上等价的状态语义的形式重新表达标准的逻辑行为语义[4，18]（第3节）。然后，我们引入并形式化了gotopause和1一行动12行动23B行动3O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5557什么都做不了pause保留控件直到下一个tick信号Sinpend声明信号SinpemitS发射S（即，S存在）presentSthenpelseqend如果S存在thendop else doqtrapTinpend声明并捕获异常Tinp出口Tp;q[p||q].如果/当p终止时，. 终止if/when q does启动p与q并行当p和q都完成循环p结束永远重复p图二. 纯E甾醇扩展语言，我们称之为ESTERELsp（第4节）。由非瞬时转换组成的自动机现在可以很容易地用条件跳转进行编码，如图1的示例所示。更重要的是，准线性再生[4，14，17]可以通过在ESTERELsp中进行简单的预处理来实现（第5节）。2纯Esterel内核语言ESTEREL[4，5，6，7，8]是一种面向反应式系统的命令式同步编程语言[12，13]。纯ESTEREL是完整ESTEREL语言的一部分，其中数据变量和数据处理原语被抽象掉了。由于我们唯一关心的是控制流原语，因此本文集中讨论纯ESTEREL。此外，在不失一般性的情况下，我们关注Berry在[4]中定义的纯ESTEREL内核语言，它保留了足够的语言语法以实现其完整的表达能力。最后，由于篇幅所限，我们认为这一声明在下文中不再适用。这并没有引起什么特别的问题。图2描述了这种语言的语法，以及其构造的直观行为。非终结符p和q表示语句（即程序）、S信号和T异常。一个ESTEREL程序运行在称为反应的步骤中，以响应全球时钟的滴答声。每个反应都需要一个瞬间。当时钟滴答作响时，就会发生反应。它可能会立即完成执行，也可能会因为暂停而延迟（部分）执行到下一个滴答指令“58O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55−−−→然后发射D并在第三时刻终止。它需要三个瞬间完成，或者换句话说，通过三个反应进行。序列、测试和（无限）循环是通常的控制流操作符。执行以确定性同步方式在并行分支中传播“发出A;[暂停;发出B;暂停;发出D||发射C;暂停;发射E];发射F“发射A和C，然后B和E，最后D和F。即时广播信号和异常提供了与环境交互的方式（通过自由标识符）以及本地通信信道（通过由信号和陷阱指令限定词法范围的标识符）。一个E星程序P具有树结构。 三个节点有更多一个孩子：测试（存在），序列和并行节点。因此，p的两个不相交的子项q和r通过这三个算子之一连接。我们注意到“q//r“，并说如果q和r不相交或并行组合，则q和r是相容的;我们注意到“q # r“，并说否则q和r是互斥的。 例如，in“p ;[q||r]“，p和q是e x c lu s i v e，p和r是互斥的，q和r是相容的。3从逻辑语义学到状态语义学我们考虑一个家庭的语义ESTEREL。项p的反应在结构操作风格[15]中通过标记的转换系统来指定EJ，kp−→pE项p和pJ将是程序或状态（参见。第3.4节）。 我们把语义的定义域称为它所应用的术语集合p。 存在信号的集合E和发射信号的集合Ej编码2反应的I/O。整数k是反应的完成码，项pJ是其残差：• 如果k= 1，则该反应不完成p的执行。它必须在下一个瞬间通过执行pJ• 如果k1，则此反应结束p的执行（pJ从未执行）：· k= 0如果执行正常完成· k=kT≥ 2，如果异常T从p逃逸，则中止执行3。一般来说，项p可以允许零个、一个或多个可能的反应，从而执行。执行是一个潜在的无限反应链，2输入和输出信号的集合I和O是这样的：E=I<$O和E′=O。程序p对输入I作出反应，输出O，完成码k和残差p′ipO，k我是 p′。根据优先级[4，18]对3个节点进行编号，因此如果p以completi oncodek和dq终止，则[p||q]temin ateswith codemax（k，l）.JO. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5559QJ除了最后一个，所有的完成码都等于1：EJ，1EJ，1EJ，k=1EJ，1EJ，1EJ，1p−−1−→p1−−2−→. −−n−−→pn或p−−1−→p1−−2−→. −−n−→.E1E2EnE1E2En3.1互模拟与观测等价为了比较各种语义，我们需要数学工具：双模拟和观察等价[3]。因为如果k不为1，反应的残差pJ是无关的（即不进一步执行），我们考虑1-互模拟的特殊定义，其中我们要求pJ<$qJ只有当k为1时。定义3.11-互模拟。设→和<$→是各自域P和Q的两个语义。→和<$→之间的1-互模拟是域P× Q的关系，使得：• 对所有p∈P，存在q∈Q使得p<$q• 对所有q∈Q，存在p∈P使得p<$qEJ，k• 如果p<$q且p−−→pE则存在qJ使得.EJ，k|−−−→qEk= 1<$pJ<$qJ.EJ，kEJ，k• 如果p≠q且q|−→qE则存在pJ使得p−→pJEk= 1<$pJ<$qJ定义3.2观察等效性。如果两个语义之间存在1-互模拟，我们说这两个语义在观察上是等价的。特别地，如果→和<$→在观测上等价，则：EJ，1EJ，1EJ，kEJ，1EJ，1EJ，k• 如果p0−−1−→p1−−2−→. −−n−→pnn n<$q0：q0|−−1−→q1|−−2−→... |−−n−→qnE1E2EnEJ，1E1E2EnEJ，1• 如果n≥0， p−−n−+−1→p，则n<$（q）：n≥0， q−−n−+−1→qnEn+1n+1个n n≥0nEn+1n+1个3.2逻辑行为语义学在图3中，我们为ESTEREL定义了一类逻辑行为语义，由辅助函数δk参数化。我们注意到→通常的逻辑行为语义[18]是通过设置δ k等于所有k的恒等式得到的。我们注意到<$→对应于δ k的另一种定义的语义：.δk（p）=如果k= 1，则无p，如果k= 1虽然在观察等价性方面与原始语义相匹配，但我们的替代版本的语义具有额外的规范化属性：JJ60O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55'E'它将已完成或已中止的执行映射为空。比如说，0，0[没什么||无]−−→E0，0[没什么||无][没什么||无] |−−→E没有什么定理3.3等价性 →和›→在观测上是等价的。证据 通过定义→和<$→之间的1-互模拟。Q定理3.4标准化。 如果pEJ，k|−−−→EpJ和k= 1，那么pJ就等于零。证据 通过归纳法证明pEJ，k|−−−→EpJ。Q这些逻辑语义不会导致直观的行为和计算反应的有效算法，因此需要构造性语义[4，19]。直观地说，它包括将语义限制在具有0，0(1) nothing −−→无ES∈E'E，kp−→pE'E，kJ（七）presentS thenp elseqend− −→pES∈/E'F，lq−→q(2)第1暂停−−→无英（8）英、法、l表示S的n个像素eqend−−→qE100，kT(3) 退出T−→无E'E，kp−→pEk= 0或k=kT'E，0（九）trapTinpend−−→无E'E，kp−→pk >0且k/=kT(4)S∈E{S}，0E（a）emitS−→无E，kkJp端的陷阱T−−→δ（p中的陷阱TE E结束）'E，kp−→pk/=0'E，kp−→p'F，lq−→qm= max（k，l）(5)EE E（b）第（1）款"" E、K、 KF，mM Jp;q−−−→δ（p;q）E[p||q]−−−−−−→δE（[p || q ])'E，0p−→p'F，lq−→q'E，kp−→pk/= 0(6) E EE（c）“的一声 F，lJ'E、K、 KJp;q−→qElooppend− →δ（p;looppend）E'E，kp−→pS∈EJE{S}（d）其他事项E'\{S}，kkJ信号Sinpend− →δ（信号SinpE结束）（五）'E，kp−→pE\{S}'E，kS∈/EJ王空军信号Sinp end− −→δ（信号SinpE结束）JJJJJJJJJJJJJO. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5561图三. 逻辑行为语义学62O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55−−−−→确定性因果（即非推测性）执行。与ESTEREL一样，这种修饰在ESTERELsp中是可能的，但不是强制性的（参见。第4.4节）。3.3标签语义我们假设暂停指令由整数标记，我们记为pausel或l：pause。我们还不要求标签是唯一的。我们称L（p）为p的标签集，例如L（pause1;emitS;pause2;pause1）={ 1， 2}。在图4中，我们通过将一组标签L添加到先前的语义（›→）作为额外的组件，为ESTEREL引入了一个标记语义<$→EJ，k，Lp<$−→pE该集合收集语句的活动暂停的标签，即在反应结束时将保留控件的暂停例如，在S存在的情况下，如果标签不是模棱两可，L携带足够的信息来表征pJ（参见 第3.4节）。如果“停顿1中的陷阱T”的反应||例如，“退出T结束”将导致空集L。因此，除了δk，我们定义将在标记语义的规则（b）中使用的函数γk如下：.γk（L）=如果k=1，L，如果k= 1EJ，k EJ，k，LTheorem3.5Equivalen ce. p，E，EJ，k，pJp|−→pJ惠L：p−→pJ.E E证据除了L的递归计算外，新的语义与前一个语义没有区别。 没有假设依赖于L值。QTheorem3.6复杂的tion。 如果p∈EJ，k， LpJ∈L∈L（p）且k/=1惠L=1惠。E如果没有设置标签，则反应完成（k =0）或中止（k = k T）执行。证据 通过归纳法证明pEJ，k，L◦−−−−→EpJ。Q推论3.7在标记语义的规则（6）中，L总是空的。因此，两个非空标签集的合并只能在规则（b）中发生。3.4国通过在语句p的一些暂停指令上添加帽子，我们得到whatwecalla teofp. 例如，JO. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5563E'S∈E'E，k，Lp<$−→p（一），0，无− −→无英（7）EE，k，L呈现Sn个像素eqend<$−→pES∈/E'F，l，Lq<$−−−→q（二）L1，{l}Epause−→无E'F，L，L存在S则pelseqend<$−→qE（八）T，T，T， T（三） 退出T−→无E'E、K、Lp<$−→pEk= 0或k=kT'E、0、L（九）trapTi npend−→无E'E、K、Lp<$−→pk >0且k/=kT(4)S∈EE（a）{S}，0，0emitS−→ nothing'E、K、L王空军transpTi npend−→δ（ transpTi npE E结束）""E、K、Lp<$−→pk/=0E、K、Lp<$−→pF，L，Lq<$−→qm= max（k，l）(5)E英、英（b）'E''m'E ，k，L kJF ，m，γ（L<$L）mJ Jp;q<$−→δ（p;q）E[p||q]◦−−−−−−−−−−−−−−→δE（[p || q ])""E、0、Lp<$−→pF，L，Lq<$−→qE、K、Lp<$−→pk/= 0(6)E E E（c）第（1）款""F，l，LLJ'E，k，LkJp;q<$−→qElooppend−−−−→δ（p;looppend）E'E、K、Lp<$−→pS∈EJE{S}（d）其他事项E'\{S}，k，LkJ信号Sinpendδ−→δ（信号SinpE结束）（五）'E、K、Lp<$−→pE\{S}'S∈/EJE，k，Lk J信号Sinpendδ−−−→δ（信号SinpE结束）见图4。 标签语义是“暂停1 ;发射S;暂停2“状态直观地说，一个状态代表程序执行过程中的某个可能的点在[4，14]中发现了类似的状态和状态扩展的引入如果一个词的暂停指令的标签是两两不同的，我们就说这个词是很好的标签。从标记良好的语句p和标签集合L的组合中，我们通过选择在L中具有标签的暂停指令来构建状态pL。例如，“（pause 1 ; emit S;pause 2）{ 2，3 }“是状态“paus e 1 ; emit S ; p ^ aus e 2“。在这种情况下，我们将尽可能方便地使用保留。从现在开始，我们只在p被很好地标记时才记为pL另一方面，如在前面的例子中，L不应该是L（p）的子集我们注意到p既是一个陈述也是（陈述p的）一个状态本身），由于没有选择暂停，所以进一步称为P的非活动状态4我们将使用状态来表示反应的起点和终点。然而，反应中的微步骤不能用状态来表示。JJJJJJJJJJJJJJ64O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55p：：=presentSthenpelseqendtrapTinpendp ||q−→（q）−→trapTin（p）end−→（p）||（q）p||Qp||q卢珀珀恩德−→є−→є−→єє（ p|| 没 什 么没什么||（qsignalSinpend−→signalSin（p）end图五. 活跃国家及其扩张我们说p L是p的有效状态，p L是p的非活动状态或某种活动状态，这是符合图5的图示的一种状态。特别地，活动状态具有至少一个选择的暂停。直观地说，无效状态是在执行过程中无法到达的状态第五章. 对于一个人来说，“p ^ aus e 1 ; p ^ aus e 2“是无效的。Astate如果在测试的两个分支或序列的两个部分中没有选择暂停指令，则暂停指令是有效的，即，如果选择的暂停指令是成对兼容的。3.5状态扩展在图5中，我们还定义了一个状态扩展函数<$：p<$→<$（p）。它从活动状态派生语句。对于非活动状态，设k（p）为空。这将扩展到有效状态。扩展将保留标签。我们观察到，即使pL是（良好标记的项p的）有效状态，标记项（pL）也不一定是良好标记的，因为可能发生循环展开。比如说，循环暂停1;暂停2结束）=无;暂停2;循环暂停1;暂停2结束3.8稳定性 如果p L是有效的，且<$（p L）EJ，k，LJ◦−−−−→EpJthenpLJ是有效的。证据如果k∈LJ，l∈Lj，则由推论3.7可知，在n（pL）中存在两个相容的停顿k和停顿l的出现.因此，pausek和pausel在p中是相容的，因为扩展没有引入并行运算符。Q定理3.9扩张。如果p被很好地标记并且pEJ，k，L◦−−−−→EpJ则n（p L）=pJ。帕奥斯河−→є没有什么p;q−→є（pp;q−→є（q）呈现S n个像素的端部−→є（pO. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55655V所有数据均不可访问！ [p^aus e1||[2]是一个既有盖又有盖的房子。66O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55−−−→证据 显然，如果k1，否则通过归纳证明pEJ，k，L◦−−−−→EpJ。Q这证明了pJ可以从L（和p）重建。反应的结果等价地由残差pJ（由逻辑行为语义定义）或我们刚刚引入的状态pL来这是在下面的部分中定义ESTEREL3.6状态行为语义学我们定义ESTEREL的状态行为语义<$→如下：对于所有pLvalid，E，EJ，k，LJ，我们记为pL <$EJ，kEpLJipJ：（pL）EJ，k，LJ◦−−−−→EpJ。处于有效状态pL中的良好标记的项p的一个反应产生valid状态pLJ（定理3.8）ii pLJ是通过项p L（pL）的标记语义（是否良好标记）计算的活动标签的集合定理3.10等价性 <$→和<$→在观测上是等价的。证据设f是关系：pL<$qi <$f（pL）=q或f（pL）=零;q。这个关系是<$→和<$→之间的1-互模拟。特别是，EJ，1EJ，1EJ，kEJ，1EJ，1EJ，kpL<$−1−→pL1<$−−2−→.<$−−n−→pLn惠函（pL）|−−1−→n（pL1）|−−2−→... |−−n−→n（pLn）E1E2EnE1E2EnQESTEREL的状态语义已经被提出[4，14]。类似地，我们的语义用“移动帽子”来描述程序的执行p^ause;[pause||pause]<$−−，→1E暂停，暂停||p^ause]<$−−，→0E暂停;[暂停||暂停]但这个新定义仍然非常接近逻辑行为语义学。“在瞬间内”执行的进展然而，我们的状态语义在连锁反应的方式上与逻辑语义不同 代替从先前反应的逻辑残差pJ恢复，执行从被完全压缩的状态p L j（的扩展）重新开始。我们的标记语义是逻辑行为语义的组合，它负责当前执行时刻，以及状态计算（标签集），为下一个执行时刻做准备虽然到目前为止，这两个计算（pJ和LJ）在标记语义中一致（定理3.9），但可以在不修改pJ 的情况下将额外的标签插入LJ的事实使得将gotopause添加到语言中成为可能。O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5567−−→−−→−−→4在Esterel中引入gotopause我们扩展了ESTEREL语法，对于任何整数标签l，使用指令gotopausel（或gotopausel）。我们注意到ESTERELsp的扩展语言。我们希望这个新构造的行为如下：p^ause1;gotopause2;emitS;pause2<$，1E暂停1;gotopause2;emitS;p^ause2• HAT首先从PAUSE1移动到GOTOPAUSE2，因为通过用具有新标签的PAUSE指令替换GOTOPAUSE而p^ause1;pause3;emitS;pause2<$，1E停顿1;停顿3;停顿S;停顿2• 然后，当在该时刻结束时，Gotopause1指令之上的HAT被移除并移动到相应的Pause1指令时，HAT从Pause3跳到Pause2这或多或少是我们在下面正式化的。但这种直观的算法在更复杂的程序上会出错。在以下示例中，初始状态p{1}有效，而派生状态p{2 ，3}无效：p^aus e1;[gotopaus e2|| paus e3];pause2<$，1E暂停e1;[gotopaus e2||p^aus e3];p^aus e2当 程 序 的 执 行 被 假 定 为 继 续 （ k=1 ） 时 ， 它 不 能 被 incen（pause1;[gotopause2||p^ause3];p^ause2)isundefined. 一个国家没有意义。因此，“暂停1 ;[gotopause2||暂停3];暂停2“不能被认为是正确的程序。这是通过对格式良好性的适当定义来处理的，这确保了gotopause的发生与ESTEREL并发兼容。4.1格式良好定义4.1格式良好。一个好标记的程序p是好格式的：⎧gotopauselk，gotopausek#pauselpausek#gotopausel如果pausek和pausel是互斥的，那么它们各自的这种纯粹的静态（语法）条件可以在构建程序的抽象语法树时轻松检查。当然，每一个标记良好的ESTEREL程序都是一个格式良好的ESTERELsp程序。68O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55−−−→4.2标签语义我们通过添加gotopause规则来构建ESTERELsp到ESTEREL的标记语义（图4）：戈托普斯湖1，{l}◦−−−−→E没有什么国 家 和 国 家 扩 张 保 持 其 定 义 在 ESTERELsp 。 因 此 ，（gotopause1;emitS;pause1;pause2）{1}=gotopause1;emitS;p^ause1;pause2 ， 并 且 对 于 example ，（gotopause1;emitS;p^ause1;pause2）=nothingg;pause2。定理4.2如果p是良型的，且n（pL）EJ，k，LJ◦−−−−→EpJthenpLJ是有效的。证据与证明3.8类似，如果k∈LJ，l∈LJ，则根据推论3.7（仍然有效），在n（pL）中存在两个相容的（goto）pausek和（goto）pausel的因此，通过定义p，在p中存在两个相容的（goto）pausek和（goto）pausel。因此，根据良构性的定义，停顿k和停顿l在p中是相容的。Q4.3状态语义我们现在定义ESTERELsp的状态语义。 对于所有p良好形成的，对于所有pLvalid，E，EJ，k，LJ，我们记为pL <$EJ，kEpLJipJ：（pL）EJ，k，LJ◦−−−−→EpJ。由 于 定 理 4.2 ， 这 种 语 义 在 良 构 程 序 上 的 有 效 状 态 当 然 ， 在 ESTERELsp中，定理3.9不再成立： 这个时候你真的用LJ。这使我们的朴素语义形式化：（i）gotopause的行为与pause一样（2）在反应过程中，由于膨胀系数的定义不确定，改变后，gotopausel和pausel都可能通过插入l变成LJ。我们注意到，对于一个给定的标号l，在p中可能有几个gotopausel出现，或者即使有一个gotopausel，也可能没有停顿l。这很好。同时跳跃到同一个目标是有意义的。虽然“goto nowhere”在实践中可能应该被禁止，但它在语义上是无害的。ESTERELsp的这种状态语义是足够的：它对程序的原E STEREL语言（即 第3.6节的状态语义）在观察上等同于rems3.3和3.10的初始语义。”一个小的，由西奥。O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5569但是，4.4建构语义学由于篇幅所限，我们只简要地概述了是的特雷尔属 ESTEREL构造性语义本质上是一种绕过逻辑行为语义的规则（d）和（e）之间的重叠问题[4，19]，这两个规则都适用于某些程序。比如说，⎧信号S在当前S中，那么...... emitS else pause end end0−−→信号S无结尾∅第1−−→信号S无结尾∅它 可 以 通 过 定 义 两 个 互 斥 谓 词 Must 和 Cannot 来 获 得 ， 用 于 disambiguation。将R u le（d）的条件“S ∈ Ej“和Rule（e）的条件“S ∈ /Ej“分别替换为“p必须发射S”和“p不能发射S”。设Must（gotopausel）和Must（pausel）被定义为Must（pause）在ESTEREL。设Cannot（gotopausel）和Cannot（pausel）为Cannot（pause）。我们的标记语义的规则（d）和（eTERELsp导致了ESTERELsp的一个充分的构造性语义。是的直觉，因为gotopause和pause指令仅通过它们的非瞬时效应而不同，因果关系（即，相对于解释语义的正确性）基本上没有改变。当然，因果ESTEREL程序是因果ESTERELsp程序.然后，由于因果程序的构造性和逻辑性行为语义相匹配，因此，这种控制的充分性是不确定的状态语义的结构语义学。ESTERELsp 是其充分性的结果，5精神分裂症和轮回ESTEREL语义的一个众所周知的复杂性由图6的无限循环说明。直觉上，由于信号S是循环的本地信号，因此每次进入循环时都会访问一个新的因此，信号O从不被发射。在形式上，逻辑语义中的循环展开会产生S的两个独立实例，因此S的发射永远不会到达测试。虽然在源程序中有一个对象S，但在本例中有两个对象S参与每个反应（从第二个开始）。这样的对象和程序被认为是精神分裂症[4，14，17]。由于超出本文范围的原因，编写精神分裂症程序是困难的。它通常直接通过复杂且容易出错的编译算法（如[4]中所述）或两步过程实现：首先重写程序以消除精神分裂症行为，然后更容易编译，如[16]。第一步叫做控制，⎪70O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55康乃馨它可以通过循环体的递归复制来获得looppend=dloo pp;pend应用到我们的例子中，这个方法产生了图7的第一个程序。每个反应都涉及一个S1和一个S2。结果程序不是精神分裂症。然而，该算法在存在嵌套循环（这里未示出）的情况下导致代码大小的潜在指数增长，这是不可接受的。已经提出了改进的方案[16，17]，但存在各种缺点，例如需要专门的中间语言来表示程序，复杂的重写规则等。相反，使用ESTERELsp的gotopause指令，可以实现简单有效的源到源转换。对于一段标号良好的ESTEREL程序p，我们通过用gotopause指令替换p的暂停指令，标号不变，循环由它们的体替换，得到ESTERELsp码p例如，我们现在考虑循环的递归重写：looppend=dloopp;pend新的重写生成图7的第二程序。通过这种预处理，最坏情况下的增长只是二次的，因为循环是从p中移除的。此外，由于无法访问的程序片段是频繁的（图7中的斜体），并且可能被擦除（死代码），因此实际上增长是准线性的，这是公认的最有效的轮回（如6为了便于阅读，我们将两个信号S重新命名为S1和S2。回路信号s存在S则发射O端;暂停;第1无信号S;发出S结束;循环信号s存在S则发射O端;发射S端−−−→∅暂停;发出S端端端见图6。精神分裂回路信号s1呈现S1然后发射O结束;暂停;发射S1端;信号s2呈现S2然后发射0结束;暂停;发射S2结束;端回路信号s1存在S1则发射O端;发射S1结束;信号s2存在S2则发射O端;1：暂停;发出S2结束见图7。 ESTEREL和ESTERELsp的再生O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）5571以及精神分裂症程序的直接编译）。6结论和展望我们设计了一个新的ESTEREL原语gotopause，并通过提供一个适当的状态行为，完全形式化了扩展语言Esterelsp虽然我们在本报告中关注的是ESTEREL，gotopause当然可以嵌入到完整的语言中。新的构造在几个小时内就被编码到我们的原型（完整）ESTEREL编译器中。使用gotopause，编译ESTEREL变得更容易。核心编译器可以专注于非精神分裂的程序，依靠第5节的预处理7来消除精神分裂的行为。 编译到ESTERELsp 也更容易。我们希望编译器的图形形式主义建立在E的STEREL，如SyncCharts [1，2]，以利用增强支持自动机在ESTERELsp。我们相信gotopause既强大又简单。它有一个非常直观的行为，因为它的行动是延迟的（即不是立即从一个常规的暂停指令不同），直觉是不会误导。特别是，它不能促成瞬时循环或因果循环。因此，它不仅便于实现目的，而且可以提供给最终用户。引用[1] 还有C 等，SyncCharts：Avissualrepresentationofreactiveehaviors，RR95-52，I3S（1995）.[2] 还有C 同步是一种并行处理，其中：计算机工程在系统应用，1996年，pp。十九比二十九[3] 阿诺德，A.和I. Castellani，An algebraic characterization of observational equivalence，Theoretical Computer Science156（1996），pp. 289-299.[4] Berry，G.，纯Esterel的构造性语义。草案第3版（1999年），http：sop.inria.fr/meije/。[5] Berry，G.，The Esterel v5 language primer（2000），www-sop.inria.fr/meije/.[6] Berry，G.，Esterel的基础，在：证明，语言和互动：纪念罗宾米尔纳（2000年）。[7] Berry，G.和G.Gonthier，The Esterel synchronous programming language：Design，semantics，implementation，Science of Computer Programming19（1992）。87比152[8] 布西诺湾和R. de Simone，The Esterel language，Another Look at Real Time Programming，Proceedings of the IEEE79（1991），pp. 公元1293-1304年。7 预处理完整的ESTEREL需要进一步扩展ESTERELsp。72O. Tardieu/Electronic Notes in Theoretical Computer Science 153（2006）55[9] C.，E.，M. Poize，J. Pulou，P. Vernier和D. Weil，Saxo-rt：Interpreting Esterel semanticon a sequential execution structure，in：Sunday[10] Dijkstra，E.W.，给编辑的信：去被认为是有害的声明，通讯。ACM11（1968），pp. 147-148.[11] 爱德华兹，S.，将Esterel编译成顺序代码，见：CODES[12] 爱德华兹，S.，[13] Halbwachs，N.，[14] Mign ar d，F. ，“Comp ila t i o n du la n gag e Es t e re l e n s y s t ` em es d '' e q u a tio n s bol ′ eennes，“Ph. D. 论文，巴黎矿业学院（1994年）。[15] Plotkin，G.，A structural approach to operational semantics，Report DAIMI FN-19，AahrusUniversity（1981）.[16] Potop-Butucaru，D.，“优化Esterel程序的更快执行”，博士论文，巴黎矿业学院（2002年）。[17] Schneider，K.和M. Wenz，一种新的编译精神分裂症同步程序的方法，在：CASES49比58[18] 塔迪厄岛和R. de Simone，纯Esterel中的瞬时终止，在：SAS91比108[19] Toma，H.， 论文，巴黎矿业学院（1997年）。