延迟动作的Esterel类程序转换为转移关系和方程组的局部声明处理方法

理论计算机科学电子笔记153（2006）71-97www.elsevier.com/locate/entcs一个带局部声明的Klaus Schneider、Jens Brandt和Tobias Schuele德国凯泽斯滕大学计算机科学系反应系统组P.O. Box 3049，67653 Kaiserlestern，Germanyhttp://rsg.informatik.uni-kl.de摘要我们描述了具有延迟动作的Esterel类程序到等价的转移关系和方程组的转换.由局部声明引起的潜在的精神分裂症问题通过以下方式解决：（1）生成语句表面的副本，以及（2）重命名这些副本中的局部变量，以允许它们在同一时间点具有不同的值。翻译在多项式时间内运行，并已通过HOL定理证明器正式验证。关键词：同步语言，验证编译器1介绍同步语言[1]，如Esterel[2，4]及其变体[13，17]，为反应式实时系统的开发提供了足够的编程范式。在航空电子、汽车工业、交通运输等安全关键应用中，已经报道了几个成功的案例[9]。这些语言的形式语义允许我们应用形式化方法不仅验证特定的程序，而且在元级别上推理语言的语义。特别是，这允许我们验证程序转换和整个编译[22，18]，以便获得形式验证的代码生成器。这些语言的共同范例是完美同步[1]，这意味着大多数语句都是以零为单位的微步骤执行的。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.02872K. Schneider等人理论计算机科学电子笔记153（2006）71时间时间的消耗是通过将有限的微观步骤组合成宏观步骤来明确规划的因此，程序的所有线程都以锁步方式运行：它们在零时间内执行当前宏步骤的微步骤，并在宏步骤结束时自动同步。由于宏步骤的所有微步骤都在同一时间点执行，因此它们在宏步骤内的顺序是无关紧要的。因此，变量的值是相对于宏观步骤而不是微观步骤来确定的。对宏步骤的抽象是同步语言语义的基本范式。它为多线程程序和硬件电路提供了一个清晰的编程模型.然而，这种抽象不是免费的：循环依赖（因果循环）和精神分裂症问题是编译器必须解决的两个主要问题。当执行一个动作的条件立即被这个动作的结果所破坏时，因果循环就出现了。检查这种循环依赖性是否具有唯一解的因果分析算法与硬件电路的组合反馈回路的分析有关[14，12，6，25，5，3，19，21]。通常，因果关系分析作为编译成中间数据结构之后的第二步执行。精神分裂症问题[15，3，22]必须在因果关系分析之前解决一般来说，如果一个语句的一些微步骤在一个宏步骤中执行了不止一次，那么这个语句就是精神分裂的。只有当语句属于同时离开和（重新）进入的循环体时（在同一宏步骤中），才可能发生这种情况。如果一个局部声明的作用域因此离开并（重新）进入，那么编译器必须仔细区分同时存在但在不同作用域中的局部变量的不同化身。为了避免混淆，编译器必须生成本地声明变量的副本（化身）。通常，可能需要多个副本，因为深度嵌套的abort和loop语句可以在单个宏步骤中强制执行多个局部声明。引用局部变量的正确化身给编译器带来了一个困难的问题，因为所有变量在每个时间点都必须有一个唯一确定的值（至少对于硬件合成来说）。本文提出了一种将同步程序转换成简单中间格式的新算法：控制流用方程组[10，3，16]给出，数据流用一组保护命令[7，17]给出。为了解决精神分裂症问题，我们必须分别为程序的表面和深度计算控制和数据流表示[15，3，17，22，27]。直观地说，表面由程序启动时执行的微步骤组成，即，当控件进入程序时。深度包含在执行K. Schneider等人理论计算机科学电子笔记153（2006）7173程序在宏步骤之后恢复执行，即，当控件已经在程序内部并继续执行时。局部声明的表面和深度部分的重叠执行可能导致精神分裂症问题，因为这些微步骤属于局部变量的不同范围。出于这个原因，我们必须分别为语句的表面和深度计算控制和数据流，以便我们能够重命名表面部分中的局部变量。此外，值得一提的是，在编译循环（而不是局部声明）期间处理这个问题是足够的，因为循环是造成精神分裂症问题的原因。我们已经在HOL定理证明器 [11]中嵌入了[17]我们的Esterel变体Quartz。这种嵌入使我们不仅可以推理特定的Quartz程序，还可以推理Quartz的语义。在以前的工作中，我们已经证明了方程组综合的正确性[16]和与SOS规则的等价性[18]。后者使我们能够推理微观步骤，这是必要的，以证明本文所提出的翻译的正确性。本文的组织如下：在下一节中，我们简要描述了Esterel和Quartz之间的差异[16，17，18，22]。特别是，我们在第2.2节中考虑了Quartz程序中发生的精神分裂症问题。在第3节中，我们考虑以前解决精神分裂症陈述的解决方案，并最终在第4节中提出我们的翻译。2石英中的精神分裂症问题2.1Quartz的语义与语义Quartz[16，17，18]是Esterel[2，4，9]的变体，它通过延迟赋值，延迟发射，异步并发，非确定性选择和内联断言扩展了经典的Esterel（同时，Esterelv7中也提供了延迟操作，并且Oracle输入也允许实现其他语句）。Quartz的基本声明如下：定义2.1【Quartz的基本语句】Quartz的基本语句集合是满足以下规则的最小集合，前提是S、S1和S2也是Quartz的基本语句，l是位置变量，x是事件变量，y是状态变量，σ是布尔表达式，α是类型：• 空语句（empty statement）• emitx和emit next（x）（立即/延迟发射）• y：=τ和next（y）：=τ（立即/延迟分配）• l：暂停（消耗时间）• ifσthenS1elseS2end（条件）74K. Schneider等人理论计算机科学电子笔记153（2006）71•S1;S2（顺序组成）•S1和S2（同步并发）•S1S2（异步并发）• chooseS1→S2end（非确定性选择）• doSwhile σ（iteration）• 当σ（悬浮）时，悬浮S• 当σ（弱悬浮）时，弱悬浮S• abortSwhenσ（abort）• 弱流产S当σ（弱流产）• localxinSend（本地事件变量）• S端的局部y：α（局部状态变量）• 现在σ（瞬时断言）• 在S保持σ期间（不变断言）Quartz 中 有 两 种 变 量 ， 即 事 件 变 量 和 状 态 变 量 ， 它 们 分 别 由 emit 和assignment语句操纵。状态变量是它们存储当前值，直到执行一个延迟的赋值next（y）：=τ意味着以在当前宏步骤（环境）中评估τ，并在随后的宏步骤中将所获得的值分配给y即时派任更新当前宏步骤中的变量，因此是等式而不是赋值。事件变量具有布尔值，即，它们可以是真的也可以是假的当且仅当在当前宏步骤中执行立即发射emitx或者在先前宏步骤中执行延迟发射emitnext（x）时，事件变量x在某个时间点为真因此，事件变量不存储它们的值（除非显式编程）。在下文中，分配和排放被称为可以延迟或立即的动作。延迟动作对于描述硬件电路特别有用。Quartz中不使用Esterel用于访问先前值的附加pre运算符（也不用于Esterelv7中的注册变量）。不确定性选择和异步并发都引入了不确定性，这在react的开发中通常是不希望的。1Quartz的事件变量在Esterel中被称为纯信号，Quartz的状态变量类似于没有状态的有值Esterel信号。在Esterelv7 [9]中，状态变量显示为仅值信号，必须使用reg关键字声明（作为所谓的注册变量）以允许使用延迟操作。在Quartz中，不存在在Este r e l的局部变量的意义上的变量，该局部变量可以通过在mic r o步骤期间的时间和时间来实现（这些变量可以通过具有延迟分配的局部（Quartz）变量来容易地消除）。K. Schneider等人理论计算机科学电子笔记153（2006）7175⎢⎥五个系统非确定性语句由不可观察（oracle）输入实现[17]，这些输入可以由显式调度程序确定性地控制。因此，它们可能会让编译器有一些自由来添加合适的调度程序（例如，最后，用“”代替。现在形式为σ的直接断言要求σ当前成立，在S保持期间，σ要求只要控制当前在S内，σ就保持[17]。其他语句的语义基本上与Esterel中的相同。由于篇幅有限，我们没有详细描述它们的语义，而是参考[17，16，18]，特别是Esterelprimer [4]，这是对同步编程的一个很好的介绍通常，语句S可以在某个时间点t1并且可以在时间t2≥t1时终止，但是它也可以永远不终止。如果S在启动时立即终止（t2=t1），则称为瞬时，否则控制流进入S，并将在下一个时间点从S内部的某个地方恢复执行一个语句是否是瞬时的或不可以取决于输入变量。只有一个基本语句，即暂停语句2，控件可以在其中停留以进行下一宏步骤。出于这个原因，我们赋予pause语句唯一的布尔值位置变量l，如果控件当前位于位置l：pause，则该变量为真。使用这些位置变量，语句S的控制流由（S）、inst（S）、enter（S）、term（S）和move（S）中的控制流条件定义，S的数据流由一组保护命令guardcmd（S，S）定义[17]：in（S）是出现在S中的停顿标记的析取。因此，在（S）中，在某个时间点i，控制流当前处于S内的某个位置。inst（S）保持i =当S现在将被启动时，控制流不能停留在S中。这意味着S的执行在这个时间点是瞬时的。enter（S）描述了当S现在将被启动时，控制流在下一个时间点将在哪里。显然，inst（S）→<$enter（S）是成立的。2.准确地说，直接形式的暂停也具有这种能力。因此，它们可以取代暂停如下：⎡abort⎤⎢pause：暂停悬置无当 立即为真时，如果为true76K. Schneider等人理论计算机科学电子笔记153（2006）71一term（S）描述了控制流当前在S内部某处（因此，term（S）→in（S）成立）并且想要离开S的所有条件。然而，注意，控制流在下一个时间点可能仍然在S中，因为S可以同时被（重新）输入，例如，通过一个环绕的环声明move（S）描述所有内部移动，即，从S内的某个位置到S内的另一个位置而不暂时离开S的所有可能的转换。guardcmd（γ，S）是一个形式为（γ，C）的对的集合，其中C是一个动作或一个现在形式为σ的立即断言。（γ，C）的含义是只要它的保护γ成立，C就立即被执行。上述控制流条件以及保护命令可以通过语句上的原始递归[17，18]来定义。这些条件的定义只需要布尔运算符和时间下一个运算符。给定一个语句S和一个起始位置st（通常称为引导寄存器），则定义控制流Rcf（st，S） 如下3：0 1（<$in（S）term（S））stinst（S）<$next（in（S））RcfB（<$in（S）term（S））最先进入（S）@（<$in（S））下一个（in（S））下一移动（S）下一页（st）转换关系的四个析取描述了即时执行、进入语句、终止执行和在语句内移动控件的行为初始条件Icf（st，S）简单地为我的意思是，我的意思是。除了控制流之外，还必须计算保护命令以构造数据流的初始条件和转移关系。计算的细节在[17，22]中给出，特别是在本文的附录中。2.2石英中的精神分裂症问题在同步编程语言社区中众所周知，当局部声明嵌套在循环语句中时可能会出现微妙的问题。因此，问题是在同一个宏步骤中可以留下和（重新）输入局部声明。这样一个宏步骤的微步骤必须引用局部变量的正确具体化，这取决于它们是属于局部声明的旧作用域还是新作用域[3]在[16，17]中已经证明了Rcf（st，S）等价于一个方程组，该方程组由每个程序位置的一个方程组成。在附录中，我们展示了如何计算这个方程系统，这是转换为硬件电路的基础（st，S）：K. Schneider等人理论计算机科学电子笔记153（2006）7177{st}{l}假假{}精神分裂症模块：输入i，j，k;输出x：整数;弱中止做locala：integer inreturn 0;弱异常终止命令localb：integer inb：= a;弱中止执行localc：integer inc：= b;next（c）：=f（a，b，c）;l：pause;intx = a;（a）：=g（a，b，c）;next（b）：=h（a，b，c）end localwhiletruewhenkendlocalwhiletruewhenjendlocalwhiletruewheni端模块真我？j？真k？假真a：= 0b：= ac：= bnext（c）：=f（a，b，c）x：= anext（a）：=g（a，b，c）next（b）：=h（a，b，c）c3：= bnext（c）：=f（a，b，c3）b2：= ac2：= b2next（c）：=f（a，b2，c2）a1：= 0b1：= a1c1：= b1next（c）：=f（a1，b1，c1）图1. 带有延迟操作的本地声明。在同一时间点产生不同局部变量化身的局部声明被称为分裂（[3]，第12章）。作为一个例子，考虑图1左侧给出的程序1. 图1的右侧显示了相应的控制-数据-流程图。此图的圆形节点是控制流程状态，这些状态用当前活动的位置变量（包括开始位置78K. Schneider等人理论计算机科学电子笔记153（2006）71地点街）。除了这些控制流状态，还有两种其他类型的节点：带有阴影框架的框包含当遍历指向该节点的弧时执行的动作。其余的方框表示影响以下计算的分支。外弧这种节点的外弧对应于条件的“then”和“else”分支。例如，如果程序是从状态{l}执行的，并且我们有i，那么我们执行控制状态{ l }下的两个动作框以及条件节点j下的一个动作框。.可以看出，条件kji执行所有可能的动作节点，同时从控制节点{l}遍历到其自身。第一个动作节点是所有局部声明的深度，第二个动作节点（重新）进入c的局部声明，但仍留在b和a的局部声明中。一个新的化身c3就这样被创造出来了。条件节点k下面的节点？（重新）进入b和c的本地声明，但仍保留在a的本地声明中。因此，它分别创造了b和c的新化身b2和c2最后，剩下的节点（重新）进入所有局部声明，因此生成三个化身a1，b1和c1。注意，这四个动作框可以在同一时间点执行，因此，转世a1、b1、c1、b2、c2和c3可以全部存在于一个宏步骤中。对于软件生成，可以简单地通过跟踪旧作用域的化身来实现化身。然而，这对于硬件电路生成来说是不可能的，因为在同步硬件电路中，每条线在每个时钟周期都恰好具有一个值。因此，我们必须根据可能的“（重新）进入”（也称为曲面）的数量生成局部声明变量的多个副本延迟的动作给本地声明的变量的再生增加了更多的困难：如果一个改变本地声明变量值的延迟动作在本地声明终止时执行，那么我们必须禁用它的执行（至少当本地声明同时（重新）输入时）。 即使终止的原因是弱流产，因为作用域被留下，因此，这个化身的下一个值丢失。如果我们在同一时间点（重新）输入本地声明，我们不能将延迟值转移到新作用域。我们还必须在局部声明的那些表面中禁用局部变量上的延迟操作，这些表面不直接进行到它们的深度。请注意，局部声明的表面可以执行多次（参见图1），但这些表面实例中最多有一个可以继续执行到深度而不离开作用域。只有这种情况下的延迟动作表面被执行。例如，在图1中，ac-下一个（c）：=f（a，b，c），下一个（c）：=f（a，b，c3），下一个（c）：=f（a，b2，c2），和K. Schneider等人理论计算机科学电子笔记153（2006）7179Xnext（c）：=f（a1，b1，c1）必须执行。在附录中给出的代码中，我们只对深度的操作应用禁用函数但是请注意子语句的表面可能属于周围语句的深度，因此，在需要时，也将在表面中处理禁用。最后，请注意，我们必须重命名所有局部变量，而不仅仅是最外面的变量：中止语句可以从每个位置终止语句，并且进入语句的适当条件可能导致轮回。因此，嵌套局部声明的表面可能重叠。3以前的解决方案治愈精神分裂症对于精神分裂症陈述的解决方案，已经提出了几种解决方案[15，3，22，27]。一般来说，这些解决方案可以分为在源代码级别工作的解决方案[22，27]和在方程系统上工作的解决方案[15，3]。3.1Poigné和HolenderskiPoigné和Holenderski定义了一种纯Esterel程序（所有动作都是立即发射的程序）到布尔方程系统的翻译[15]。他们的翻译也解决了精神分裂症问题的地方宣言没有拖延行动。给定一个位置为l1，.的语句Sll，输入x1，.，xm，并且输出y1，.， yn，它们计算方程next（li）=li，并且yi=i，其中i和i是关于变量xi、yi和li的命题公式。 对于其余部分，需要以下定义，其中我们使用再次ST作为一个特殊的开始位置。 此外，[τ]e意味着替换所有x在τ中的出现次数：定义3.1给定一项τ，其中包含布尔变量st，l1，. ln，我们将α部分αL（τ）定义为αL（τ）：[τ] false. 假，其中L：={l，. ，l}。此外，我们定义了τ的η-部分η（τ），l1. Ln北一街假如ηst（τ）：η [τ] st。因此，直觉是，在假设控制流当前不在S内的情况下，αL（τ）等于τ。特别地，当控制流第一次进入τ时，αL（τ）等于τ。类似地，在st=假的假设下，ηst（τ）等于τ，即，当语句当前未启动时。特别地，当控制流在S内部移动时，ηst（τ）等于τ，因为我们有一个不变式，即如果它们目前处于活动状态，不会终止。80K. Schneider等人理论计算机科学电子笔记153（2006）71请注意，一个项的α和η部分并不不相交，这是精神分裂症问题的根源。一般来说，跃迁的α和η部分控制流Rcf（st，S）的关系如下：⎛ ⎞stinst（S）<$next（in（S））• αL（Rcf（st，S））：最大最小中心（S）下一个（in（S））<$in（S）<$ <$next（in（S））<$下一个（st）⎞• ηst（Rcf（st，S））：下一项（在（S）中）下一项（st）移动（S）虽然st在ηst（τ）中被设置为假，但我们不能从ηst（τ）得出st为假的结论，因为st不再出现在ηst（τ）中。此外，很容易看出，αL（Rcf（st，S））和ηst（Rcf（st，S））所作的情况区分是完全的，即，Rcf（st，S）惠<$in（S）<$αL（Rcf（st，S））惠<$st <$ηst（Rcf（st，S））成立。简单地注意到，st<$in（S）在开始时成立，之后，我们有<$st。项τ的α和η部分对应于τ的不同观点，在表面和深度的一个声明。普瓦涅和霍兰德斯基使用它来重命名表面部分中的本地声明变量，即， 在方程组的右手边的α 所以他们J J计算新方程next（l）= [α（n）]x ∨η （二）y = [α（λ）]xλi L ixstIi L ixηst（ηi），当局部声明的方程组必须被计算。如上所述，必须对所有出现在S中的局部变量进行重命名，以便深度嵌套的局部变量产生多个副本。这种方法的优点是非常简单明了。然而，对非布尔数据类型和延迟操作的推广还不清楚。此外，如果局部声明没有嵌套在循环中，甚至会重命名变量，因此过程会生成比必要的更多的副本。3.2Berry当然，公共领域的Esterel编译器[4]和商业工具，如Esterel Studio [9]能够解决精神分裂症问题。由于基本陈述的不同集合（陷阱而不是中止），Berry还考虑了双膈平行陈述（这也在[15]中完成）。[3]（第12章和第13章）给出的解为每个语句定义了它的“化身层”，直观上就是它的曲面的必要副本的数量。这种代码段的重复对于区分不同的内部康乃馨是必要的，并且不能被规避。另一方面，程序K. Schneider等人理论计算机科学电子笔记153（2006）7181X在[3]中描述的是在电路门级给出的，因此，它相当复杂。此外，很难用优化来扩展它，并检查它的正确性，例如，一个定理证明器。最后，类似于Poigné和Holenderski3.3语句的表面-深度拆分在[22]中，提出了一种解决精神分裂症问题的新方法。它的主要思想是为每个语句S定义相应的语句surface（S）和depth（S），使得surface（S）是当S被输入时执行的S的一部分，而depth（S）是S的剩余部分。这两个语句都是在[22]中通过语句上的简单原始递归定义的，并且可以在时间O（|S|2）的情况。二次爆破的原因是序列和循环生成表面语句的副本[22]。我们在这里不考虑表面（S）和深度（S）的定义，但列出[22]的以下结果定理3.2（表面和深度）对于每个陈述S，我们有：• 表面（S）对于所有输入都是瞬时的• S和深度（S）具有相同的控制流程• S和表面（S）;深度（S）具有相同的控制流程• S和表面（S）;深度（S）具有相同的数据流• 当输入深度（S）时，不执行深度（S）的操作在[22]中提出的想法大致如下：我们用下面的语句替换S端的局部declarationlocalx，其中x（1）是x的相同类型的副本在[surface（S）]x（1）中localx，x（1）;depth（S）end将S分裂为表面和深度会产生新的动作，这些动作明确地属于表面或深度，而在S中，可能存在既属于表面又属于深度的动作（取决于变量的当前值）。因此，这种分割允许在表面中重命名局部变量。然而，上面的转换是不够的：分割成表面和深度提取在表面中执行的所有动作但是，如果depth（S）包含一个条件语句，其条件在开始时间，那么这个评价也应该参考表面值。怎么--简单地重命名条件语句的条件显然是错误的。更有甚者，还有带有精神分裂症条件语句的语句82K. Schneider等人理论计算机科学电子笔记153（2006）71X也就是说，其中，同一个条件在同一时间点被评估两次，第一次是表面值，第二次是深度值。为此，在[ 22 ]中已经提出，使用当输入S时保持e xth的n e xpressi o nn k来替换这样的条件，例如，用k expression k[1] x（1）来表示。 然而，一个条件可能有几个化身，因此，我们必须根据可能化身的数量来进行这种转换。在[22]中，还错误地指出局部变量的一个副本就足够了。一般来说，这是真的，因为只有一个表面处理的深度，而其他表面的值是隐藏的，因此可以消除编译器。然而，[22]中列出的程序是不正确的，这已经由Edwards指出[8]。对这个过程的修正是可能的，但是由于不同的副本，如上所述的if条件的替换变得非常困难。作为替代，可以定义一个新的语句gotoL，其中L是一份控制流程位置列表。语义是控件直接移动到列出的位置L以等待下一个宏步骤。 使用这种一个语句，人们可以在表面生成条件句的副本，这样他们的精神分裂症也被治愈了。最近在[26]中提出了这样一个带有goto语句的Esterel扩展。将[22]和[26]结合起来，在源代码级别上给出了精神分裂症的另一种解决方案（参见[27]）。4我们的验证编译方案我们的新解决方案基于我们在以前的工作中开发的各种先决条件[16，17，22，18]。类似于[22]，主要思想是在给定语句S的一次遍历中计算所需的信息，如控制流条件inst（S），in（S），enter（S），move（S），term（S）和保护的命令[17]。 为此，翻译要有向前启动的条件在递归下降期间，goα和goη：goα使能表面的动作，并且goη另外强制控制进入所考虑的状态4。 除了goα和goη之外，平移还保持以下条件： KL和SP用于跟踪周围的流产和悬浮条件5. 此外，还维护一般来说，goη意味着goα，但反之亦然：考虑弱中止S1;S2当kl时，并假设控制当前处于S1中S1终止的位置，并进一步假设kl保持，因此发生中止。由于流产是弱的，我们必须执行S2表面的动作，但控制不能进入S2。因此，S2的起始条件goα成立，但goη为假。5 kl因此具有更高的优先级，因此我们实际上将abort suspendSwhensp翻译为kl。K. Schneider等人理论计算机科学电子笔记153（2006）7183其长度取决于嵌套循环的最大数量。我们将在下面更详细地解释后者。解决精神分裂症问题的关键是考虑语句的表面 很容易看出，inst（S）和enter（S）完全指的是表面，而术语（S）和移动（S）完全提到深度。 因此，不需要区分表面和这些条件的深度。相反，保护命令和转移方程必须分别被分成表面部分Gα、Rα和深度部分Gη、Rη。表面和深度部分由函数CableSurface和CableDepth计算，如附录中详细所示。这些函数最初由函数StartCompile调用，该函数还预先计算需要对局部变量进行重命名。 函数调用的结果是元组（I，Gα，Rα）和（C，L，G η，A，T，Gη，Rη），其含义如下（参见定理4.2）：C是一组新的（oracle）输入变量，用于模拟选择和异步并发的不确定性（这些变量可以由额外的调度程序控制）。条件I、A和T分别是控制流谓词inst（S）、in（S）和term（S）。Gα和Gη分别是S此外，Rα和Rη是方程组6，其包含对于每个位置变量li的形式为next（li）=lli的唯一方程。Rα和Rη是跃迁方程的α-部分和η有趣的是，Rα的合取等价于enter（S）。最后，L是在S中局部声明的变量的集合（我们假设不存在阴影问题），并且xj是一个列表，其中包含S中循环的每个再生表面的一组元组（goη，x，xJ），使得xJ是在曲面中使用的局部变量x∈L的重命名，开始条件goη。 在附录B中，解释了为什么这些信息这是从中间结果最终生成转换关系或可执行代码所需的。由函数StartCompile确定的最终结果简单地计算GαGη和（RαRη）作为数据和控制流的表示，其中（RαRη）定义如下：[6]原则上，这样的方程系统只不过是硬件电路。因此，我们使用[16]中提出的类似模板进行计算。84K. Schneider等人理论计算机科学电子笔记153（2006）71定义4.1给定相同状态变量的两个转移系统Rα和Rη，我们定义组合转移系统（RαRη）如下：（Rα&Rη）：τ {[下一个（1）= τατη]|[next（l）= τα] ∈ Rα<$[next（l）= τη]∈ Rη}为了获得在二次时间内运行的翻译，在翻译期间生成的子项必须由新变量缩写。在本文的会议录中，我们使用了两个方程组Eα和Eη，它们分别是表面积和深度的缩写，re-tap。这是必要的，因为精神分裂症问题的解决方案需要重命名循环表面中的局部声明变量（请参见下面）。因此，我们不得不分裂缩写的方程组，以便仅重命名表面部分Eα成为可能。然而，这会改变散列值，而且允许一个项在不同的表面Eα中出现多次而不被重命名。为了避免以后的重命名，从而避免使用多个哈希表的必要性，附录中给出的解决方案有不同的工作原理：图A.1中给出的函数Renamings在实际编译之前计算所有可能的作用域：函数调用Renamings（S）返回一对（L，N），其中L是S中局部声明的变量的集合，并且是一个替换列表。例如，对于图1中给出的程序，我们得到L= {a，b，c}和ρ =[ρ1，ρ2，ρ3，{}]，其中ρ1={（a，a1），（b，b1），（c，c1）}，ρ2={（b，b2），（c，c2）}，ρ3= {（c，c3）}。在S中的替换数是S中循环的最大嵌套加一（我们对循环的每个表面都有一个替换，另一个是深度）。在预先计算了重命名之后，我们可以在将术语存储到哈希表中之前对其进 行 。 为 此 ， 所 有 需 要 的 重 命 名 都 将 由 CableDepth 转 发 给 函 数CableSurface，以正确计算循环体的重命名曲面（请参阅转换循环的代码在附录的函数中，我们假设所有局部变量都有不同的名字，因此，没有阴影。此外，局部变量的名称与输入和输出变量的名称不同。函数NewVar生成一个新变量，NewDef（τ）返回该变量与表达式τ相关联（如果τ已经出现在哈希表中），或者在哈希表中生成一个新条目，其中包含一个新变量，τ。最后，我们使用函数来操作列表，比如Cons添加最左边的元素，Head复制最左边的元素，Tail剪切它。下面的定理总结了我们构造的不变量[7]替换是一组对（x，τ），意味着变量x必须被项τ替换。K. Schneider等人理论计算机科学电子笔记153（2006）7185定理4.2（翻译Quartz语句）给定一个Quartz状态S，起始条件goα和goη，S的局部变量的重命名ρ，函数调用VeeSurface（ρ，goα，goη，S）计算一个三元组（I，Gα，Rα），其含义如下（图A.5）：• I=inst（S）• Gα=guardcmd（goα，表面（S））• αL（Rcf（goη，S））惠τ，其中L是S的位置τ∈Rα给定一个挂起条件sp，一个中止条件kl，以及嵌套循环的所有曲面的重命名，调用XaveDepth（S，sp，kl，S）会产生一个元组（C，L，R，A，T，Gη，Rη），使得以下成立（图A.2-A.4）：• C是添加的控制变量8的集合，用于消除不确定性状态（不确定性选择和异步并发）• L是在S中局部声明的变量的集合• S是一个列表，它包含S中所有循环曲面的一组元组（goη，x，xJ），使得xJ是在起始条件为goη的曲面中使用的局部变量x∈L• A=in（S）• T=term（S）• Gη=guardcmd（goα，深度（S））• ηgoη（Rcf（goη，S））惠ττ∈Rη最后，使用新的起始位置l0，StartCompile（l0，S）（图A.2）计算一个元组（C，L，R，G，R），其中包含控制变量C、具有起始条件的重命名、保护命令G和控制流方程R. G和R分别表示S的数据流和控制流。如 果 你 的 系 统 是 一 个 复 杂 的 系 统 ， 那 么 StartCompile （ l0 ， S ） 和OpenDepth（l，sp，kl，S）的运行时间都是O（|S|2）的情况。二次爆炸的原因是序列和循环生成其子语句的表面副本，如图2（线条分隔整个语句的表面和深度（1）A，B，C，D，|S|）的。现在考虑局部声明的翻译：回想一下，精神分裂症局部声明的原因是它的深度与至少一个表面一起执行。只有当局部声明包含在循环中因此，在循环的转换中，我们将所有局部8 这些被添加为新的Oracle输入，以模仿非确定性。86K. Schneider等人理论计算机科学电子笔记153（2006）710表面（S1）;1B如果inst（S1）则曲面（S2）结束; C•S1; S2：CIB深度（ S1）;C@ifin（S）then surface（S）end;A1 2深度（S2）0表面（S）1BdoC• doSwhile σ：深度（S）;C@如果σ，则曲面（ S）结束A当σ图2. 序列和循环生成曲面曲面中的变量，该变量是由具有第一次重新命名的XueDepth计算的。嵌套较深的曲面将使用剩余的替换进行重命名。因此，在循环的转换中，CableDepth仅转发重命名并将它们转移到CableSurface备注：然而，序列的表面拷贝没有被重命名，因为它们与精神分裂症无关。再次注意，这些重命名是通过编译转发的，因此没有显式的重命名步骤（与本文的后续版本相反）。重命名最终通过以下方式在函数VeeSurface中发生：（1）重命名条件语句的所有条件σ，(2)通过在编译操作时调用函数RenameAction。 注意因此，仅当前值被替换，从而延迟的动作可以正确地将其计算值传送到深度。然而，仅仅重命名是不够的：此外，我们必须禁用局部变量上的延迟操作，否则这些操作将在循环体终止时发生。如果不禁用这些操作，它们将错误地将值传输到新作用域的下一个宏步骤。这种“禁用”是在用函数转换循环时完成的-定义为DisableDelayedLocals（L，δ，G）的DisableDelayedLocals：={DisableDL（L，δ，（γ，C））|（γ，C）∈ G}，其中：J• DisableDL（L，δ，（γ，emitnext（x））：=• DisableDL（L，δ，（γ，next（x）：=τ））：=（γ，emit next（x））：x/∈L（γ<$δ，emit next（x））：x∈LJ（γ，next（x）：=τ）：x/∈L（γ<$δ，next（x）：=τ）：x∈L• DisableDL（L，δ，（γ，C））：=（γ，C）对于所有立即动作C这就完成了翻译。 请注意，局部变量可能重命名的数量取决于周围循环的数量。我们只在遇到循环时重命名，与[15，22]相反，重命名是在本地声明的转换中进行的。尽管如此，附录中的算法并不是最优的，因为当循环通过时，它们会生成所有包含的局部变量的副本一个精炼的版本应该检查是否转世-K. Schneider等人理论计算机科学电子笔记153（2006）7187可以通过检查局部声明的开始和终止条件的满足性来进行验证。5总结我们已经展示了如何将Esterel家族的同步程序编译成中间数据结构，这些中间数据结构可用于程序分析（如验证），也可用于代码生成。特别是，我们已经考虑了编译本地声明的变量，这是困难的同步语言由于精神分裂症的现象的问题。这意味着必须安全地区分可能存在于同一时间点的局部声明的不同作用域。为此，我们的编译技术使用了复杂的重命名步骤，并禁用了对局部变量的延迟操作，以避免不同作用域之间的干扰。引用[1] Benveniste，A.，P. Caspi，S. Edwards，N. Halbwachs，P. Le Guernic和R. de Simone，Thesynchronous languages twelve years later，Proceedings of the IEEE91（2003），pp.六十四比八十三[2] Berry，G.，Esterel的基础，在：G.普洛特金角Stirling和M. Tofte，editors，Proof，Languageand Interaction：Essays in Honour of Robin Milner，MIT，1998 pp. 425-454[3] Berry，G.， 纯粹的埃斯泰尔的构造性语义学，http://www-sop.inria.fr/esterel.org（1999年）。[4] Berry，G.，The Esterel v5_91 language primer（2000）.[5] Boussinot，F.，SugarCubes因果关系的实施，研究报告3487，国家信息和自动化研究所，Sophia Antipolis Cedex（法国）（1998年）。[6] Brzozowski，J.和C.- J. Seger，[7] Dijkstra，E.，保护命令，程序的不确定性和形式推导，ACM通信18（1975），pp。453-457[8] 爱德华兹，S.，个人通信（2002年）。[9] Esterel 技术， 网址：http://www.esterel-technologies.com。[10] Girault，A.和G.Berry，电路生成和Esterel程序的验证，在：信号，电路和系统研讨会（SCS），雅西，罗马尼亚，1999年，pp.85比89[11] 戈登，M。和T. Melham，[12] Halbwachs，N.和F.Maraninchi，电路和同步程序中组合回路的符号分析，在：欧洲微电子会议，科莫，意大利，1995年。[13] 拉瓦尼奥湖和E.Sentovich，ECL：系统级设计的规范环境，在：国际设计自动化会议（DAC）（1999年），pp。511-516[14] Malik，S.，循环组合电路的分析，IEEE计算机辅助设计学报13（1994），pp. 950-95688