信号时钟演算综述：从规范到代码的建设性分析与编译技术

理论计算机科学电子札记88（2004）39-54www.elsevier.com/locate/entcs信号时钟演算综述Mirabelle Nebut1L3I- U n i v. deLaRochelle- a v M. Creeau摘要信号编译过程基于一种称为时钟演算的形式化分析。它通过合成一个顺序控制结构来建设性地确定一个规范是否是内隐的。该分析适用于从规范推断并编码为布尔方程的时钟关系。本文首先概述了与时钟相关的必要基本概念（数据流规范中的控制，操作语义的链接，布尔编码），然后使用这种照明来呈现微积分的技术方面[1，2]。保留字：一代信号，时钟演算，时钟，数据流范例，控制流综合，代码1介绍从规范自动安全地生成代码是同步开发环境的吸引力优势之一。虽然它们有着共同的关注点，如代码效率和紧凑性，但同步语言已经开发了适当的和非常不同的编译技术，这些技术可以产生不同的代码结构（自动机，命令式单循环，函数代码，电路，布尔方程等）。早期的LUS-TRE和ESTEREL编译器生成一个自动机，而SIGNAL和SCADE编译器合成一个顺序控制结构。然而，ESTEREL编译过程正在朝着从控制流图生成顺序代码的方向发展（ESUIF，SAXO-RT[12]），而SIGNAL可能会利用自动机的LUSTRE这表明，尽管范式不同，每种语言都可以1电子邮件：nebut@lifl.fr1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.05.00540M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-其他一些优秀方法的优点。它要求明确确定其基本原则，并尽可能从技术、与实现有关和依赖语言的细节中抽象出来本文主要讨论了S信号的情况。信号编译过程，称为时钟演算，是一个基于原创思想的非常丰富的分析，涉及理论和实现相关的概念，非标准对象（时钟），技术（将方程系统转换为一组定义），数据结构（时钟树）和专业词汇。这些方面的多样性使得很难解释，并且主要是从技术实现相关的角度提出的[1，2]。虽然基于示例的演示或将系统的翻译方案转换为重要代码应该是解释性的，但本文（没有增加任何研究贡献）侧重于概述基本的必要概念，强调[1，2]中提出的技术细节。第2节回顾了基本的同步（主要是数据流）模型和操作语义.第3节重点讨论时钟，因为它们在数据流范式中被定义（作为一组时刻）和使用（用于控制目的），然后在信号上下文中给出它们的形式化，强调它们的组合性质和布尔编码。第4节介绍了时钟演算本身，通过直观，理论和技术方面。最后，第五节结束。2一般同步概念同步范式认为反应系统的执行是一个无限的反应序列（反应是输入获取，计算和输出发射的过程同步假说假设反应发生在一个合乎逻辑的瞬间。图1（a）表示这样的执行，由离散的时刻序列ti索引。在2.1节中，我们解释了在反应中可以不存在同步变量。然后，我们将重点放在数据流范例上，并在第2.2节中提出一个通用的操作模型，该模型是在信号情况下实例化的。2.1无信号和变量命令式范式致力于控制主导的应用程序。对命令性规范的控制是通过被称为信号（纯信号或有值信号）的事件的发射和接收来规范的，这些信号在任何反应中都具有不存在或存在的固有状态在ESTEREL的情况下，信号的值只能在存在的情况下被修改，但它是持久的：它可以在2[1]使用了一个简单的语义，但一个操作的语义似乎更直观。M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-411001t1t2t3t4.t1t2t3t4t5N*1*-23.y *py *-23...0− 2 ......这是什么？(a) 总体实施方式my0 −→ 0 −→ 1 −→ 0 −→ − 2...(c)添加内存py>1 N=t1t2Xt3t4...N≤0 y=N py≤0N=py=y=N=Ny=py−1N= py=y=y(b) 数据流执行Py= 1Py= 0(d)符号自动机Fig. 1.同步模型没有信号在数据流范式中，事情是不同的，致力于对数据进行密集计算：规格是指定如何计算变量3的值然而，变量也有存在/不存在4的状态。此外，一个不存在的变量没有重要的价值。我们在这里用一个特殊的值5* 来表示缺席，就像[10]中一样一个数据流的执行展示了这个特殊的价值，如图所示. 1（b）.2.2数据流操作语义和表示法让我们使用非常通用的符号标记转换系统（SLTS，参见[10]以获得更正式的细节）来精确数据流操作模型中的缺失发生在哪里。 一个SLTS是建立在域D的一组变量S和一组持久存储器M上的（通常mx∈M是与x∈S相关联的存储器）。请注意，变量具有状态，而内存本质上始终存在。赋值V：S→D{*}表示系统的反应。一个状态是对记忆E：M→D的估值。SLTS包含初始化谓词I（初始状态）、记忆谓词M和组合（无状态）谓词C。M处理系统的状态，从外部看不见。 C将系统与其环境连接起来，它描述了反应中发生的事情。 SLTS平行组合是标准的。3 LUSTRE有变量，但 SIGNAL有信号，如 ESTEREL：我们选择使用术语“variable” for the whole data-flow4 例如，当x>0时，LUSTRE方程y = x导出了如果x为负，则y5传统上，在信号背景下。py≤0y=NN=/联系我们我的我的产品编号：*5*42*反应1反应2反应3反应41342M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-y2.2.1信号情况记得信号kernelconnaparall elco mpositiono perer|、一个延迟运算符$，加上运算符when，default和函数（请参阅它们的语法图2）的情况。只有延迟运算符涉及记忆部分。等式py：= y$1initv0由SLTS表示：⎧⎪⎨mJ.=y如果y*I：（my=v0），C：（py=*惠y=*），M：不包括myelse（一个）如果py/=*，则py=my其他组合信号运算符将SLTS归纳为谓词C，如图所示二、信号平行合成对应于SLTS合成。注意，缺失只发生在组合部分的赋值模型集合中，这些赋值模型标记了底层符号自动机的转换（参见例如，图1（d））。这样的自动机是一个经典的验证模型：带* 的扩展名阻止使用标准工具。因此，专用于信号规范的布尔验证工具SIGALI[9]使用三个值s{*，true，fals e}in到{0，1，-1}的编码，通过将BDD扩展到三个值来产生Z / 3 Z中的计算。不幸的是，这种原始技术不能扩展到无限域。例2.1设y是一个用输入变量N初始化的计数器：当它为正时，它会减小，当它达到0时，它会用N重新初始化py：= y $1 init 0 |y：= N默认py-1|当py <= 0时，这些方程由包含谓词I和M的SLTS表示显示在Eq. 其中v0= 0，以及以下组合部分C：py=*惠y=*惠y/=*惠（N/=*惠py*）惠N/=*惠y=N（N=**优惠（py）*≤0）图1（c）给出了一种可能的执行方式（箭头表示变量和存储器之间的链接）。相关的符号自动机如图所示1（d）.⬦y = g（x1，...，xn）~Vy=*惠x 1 =*惠... 优惠xn=*yi=*i，xi*y=g（xi，.， xn）y：= x when c~c/=truey=*Vc=truey=xy：= x默认值z~x/=*y=xVx=*y=z图二. 信号组合算子的CM. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-433时钟我们将在3.1节中解释什么是时钟，以及它们如何用于指定数据流系统的控制。然后，我们在3.2节中介绍了它们在处理信号时传统上使用的形式化。3.1数据流时钟一个系统的时钟，一个组件在图1给出的执行模型中出现的瞬间序列在命令式范式中被称为时间尺度，在数据流范式中被称为时钟。更确切地说，一个系统的时钟是它的反应瞬间的集合（图1）。1（a））。这个概念是经典的在同步范例之外（仅考虑电路）：时钟触发周期系统的激活。因为没有理由一个系统的并发组件应该同时执行它们的计算，它们必须有不同的激活，所以系统应该包含几个时钟：它是多时钟方法的基础，而不是单片单时钟方法。变量的时钟现在让我们来看看时钟是如何传递的到组件。 的情况下用户6组件的激活是由至少一个输入变量的存在触发，比如y。 的组件的时钟精确地对应于y存在的时刻的集合：这是通过在信号上下文中扩展由y确定的y的时钟来实现的。请注意，变量的潜在缺失现在是后验的：变量具有数据流传送器和（通过其时钟）用于控制行为的偶发事件的双重身份，如命令式范式。时钟和控制信号哲学强调这最后一点：时钟基本上是程序员指定控制其规格7，指示某些计算发生的时刻 时钟在信号中的应用非常广泛：任何与 计算（例如，表达式、数据依赖性）与时钟这是一个ctivs它。一个特例是变量y的clocky^，其中触发y的计算。遵循这一原则，与系统相关的可执行代码包含对时钟的测试6 信号机制更一般，详细讨论见[10]。7.回想一下，数据流方程不像命令式范式那样具有控制结构;简单地执行方程是非常不明智的。44M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-3.2信号钟的形式化时钟代数在信号上下文中，时钟的关系是用时钟代数（这里用H表示）来描述的。钟是在Sect中定义的。3.1作为瞬间的集合;时钟代数相应地使用集合符号：H = U，O其中U是参考时刻集，O是空时钟。给定一组闭合变量Ki被解释为U的子集ets（包括例如， 其中，Hc可以表示关系式，如x^=y^z^。我们都使用的集合包括操作系统。表达性即使在它们的第一个定义中，时钟是索引执行的时间尺度的子集（见图1（a）和1（b）），时钟上的关系并不描述这样的执行（即估值序列），而只是估值/反应的集合。事实上，在这个方程中，x^=y^。如果对于任何索引时刻t，x和y都存在，则执行为真或者在发生这种情况的情况下。在上述文字中，如果在执行的任何反应/估值中，x和y都存在或不存在，则x ^ = y ^为真：对时间的引用已经消失，估值的顺序也消失了。关系在时钟上的表现力是纯组合的。 等式x^=y^表示值的集合Vs。t. V（x）=*惠V（y）=*。命题演算中的实用编码这组值可以通过将命题变量bx和by分别置于sx ^和y ^之间并考虑布尔方程bx惠by来简单地表示，其中描述了分布sδ的 选 择 ：{bx，by}→{0，1}，其中eδ（bx）=0惠δ（by）=0。 我们只需要解释δ（bx）=0（分别为 1)当present）"。更一般地，[2]提出了H和布尔函数之间的对应关系。我们更喜欢像[10]那样的命题演算PC。编码非常简单：每个变量k∈ K都与一个命题变量bk相关联;每个集合算子都与对应于其特征函数的逻辑算子相关联。非正式地考虑以下示例：HUOx^y^=z^w^x^\z^=y^PC真假bxby惠bzbwbxbzb惠by由于这种编码，可执行代码将时钟作为命题变量而不是时刻集合来处理。一个时钟有一个值真或假的反应，并测试在节中提到的时钟3.1只不过是测试[8]请注意，变量的LUSTRE时钟直接是指定的特定布尔变量，其缺点是时钟的概念是递归的。M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-45一个布尔变量：4信号时钟演算原理同步语言的编译过程并不局限于代码生成：一些分析首先应用于确定规范是否确实可执行。让我们提及LUSTRE[6]和ESTEREL[4]因果分析，LUSTRE[6]和LUCIDSYNCHRONE[5]时钟分析以及ESTEREL构造性分析[4]。信号编译过程包含一个称为时钟演算的主要分析[1，2]，代码生成和因果关系分析[1]直接遵循该分析。因此，时钟演算包含各种方面，这使得它非常丰富，但很难解释。微积分适用于4.1节中所介绍的规范的同步。它合成了一个控制结构，单循环代码直接遵循该结构（从同步推断的控制结构的示例在第4.2节中给出）。它的核心是一个建设性的决策程序，它确定一个规范是否是内隐的（第二节）。4.3）。我们描述在节。4.4节中的数据结构和算法及其实现四点五4.1信号规范的同步一个信号方程指定一个关系1。当前变量2.变量的状态。 例如，y：= x默认值z表示y存在i =x存在或z存在。这个语句描述了方程的同步，或者说是一个与时钟的关系。它可以被描述使用该关闭的标签（例如，y^=x^z^）或信号高h-水平运算符（例如y ^= x ^+ z）。但是变量的时钟是不足够的：由欠采样引起的同步，当算子涉及b〇lee和变量y：= x的值时，其中c表示y存在，x和c存在，并且c具有值true。因此，有必要引入一种新的时钟来处理布尔值。这样的条件时钟表示为[c]∈ K（当c在SI-GNAL中时），这意味着当c以值true（[<$c]）存在时的时刻集合。对应于值false）。 [c]被认为是通过欠采样（或在条件C下，信号同步显示在图三.在时钟代数中表示，它们形成一个称为时钟系统/方程的方程组。括号方程是可选的：它们通过指定nc存在时，c是真还是假（假设（[c]，[<$c]）是^ c的一部分）来关联[ c ]，[<$c]和^c。现在让我们精确地描述同步化的命题编码和用*（如Z/3Z）扩展的布尔模型之间的联系。的编码46M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-P信号P同步P在H中的同步化y：= g（x1，...，xn）y ^= x 1|......这是什么？| y^= xny^=x^1.. . y^=x^npy：= y $1init v0py ^= yp^y=y^y：=xwhency ^= x ^* 当cy^=x^[c][c][<$c]=^c[c][<$c] =Oy：= x默认值zy ^= x ^+ zy^=x^<$z^图三. 同步将变量的时钟关系转换为PC（3.2节）是非常直观的，因为变量的状态显然是布尔的。一个条件时钟[c]类似地被编码到一个命题变量b[c]中，但是分布指示了c的状态和值，例如δ（b[c]）=0意味着c要么不存在，要么存在，值为false。如在2.1节中所解释的，语义计算域是{*，true，fals e}，但是条件集合k的引入使得编码成为可能，编码成命题演算的仅有的两个值。这个技巧只不过是使用辅助变量9将三值逻辑编码为布尔代数的经典编码：bc=b[c] =b[<$c] = 0~c =*bc =1，.b[c]=0，b[<$c]= 1~c =假b[c]= 1，b[<$c] = 0~c =true换句话说，由于条件时钟，时钟代数可以描述全布尔组合部分信号规格10和类似任何布尔组合谓词C（2.2节）。这意味着，通过将这样的编码应用于C，可以使用标准的stu语言来实现SIGALI从现在开始，我们同化时钟变量（分别为时钟上的关系）及其相应的命题变量（分别为布尔方程）。4.2从同步到控制结构：主要思想如第3.1节所述，信号哲学强调时钟指示对数据流规范的控制因此，管制─9.不同的b[c]、b[<$c]和b bbc之间的关系不是由其他关系决定的：闭合微积分只使用b[c]和b[<$c]。例如，如果x、y和z是布尔变量，则等式y：= x default z可以被编码为布尔等式：[y]=x^|z^，[y]=[x]|（[z]|x^）。M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-47目标可执行代码的流是从时钟上的关系或同步合成的由于时钟只能描述反应内部发生的事情，我们只讨论与组合指令对应的控制流（完整的例子见第5我们在这里给出了一个主要思想的直觉（它们将在下面的章节中详细介绍），通过考试来说明请。第一个例子涉及方程：= xdfaultz，第二个在Ex的边界上。二、第三个方程y = x+2|z：= y+2wheny<= 0|w：= zwhenz<0. 这两个同步分别由等式（1）和（2）表示。（2）、（3）和（4）：y^=x^<$z ^（2）y^=^pyy^=N^p^yN^=[c]（3）y^=x^z^=y^[cJ]w^=z^n[cJJ]（4）其中c， CJ和cjj分 别抽象条件py≤0，y≤0和z0。相应的代码分别在图4（a）、4（b）和4（c）中给出。显然，控制流程是通过对时钟11的测试来实现的。(1) by：= b x或b z;(2) 如果是，然后//计算y(3)ifbxthen y：=xendif(4)如果（bzandnot bx），则y：= z结束如果结束如果（一）（1）如果by然后（二）b[c]：= py≤0（三）bN：=b[c];如果bN则y：=Nelse y：= py- 1endif(4)endif （b）第（1）款（1）如果by然后（二）y：=x +2（三）bz：= y = 0(4)如果bz(5)然后z：= y +2bw：=z0ifb w那么w：=z end如果结束如果结束如果（c）第（1）款见图4。 反应内部的控制结构时钟基本上是用作变量值的r/w守卫。在图1中，许多方法都可以用来计算一个可变的值。4（c）z：= y+2（行5）由y对y^（y是已知的）和z^（必须计算z），行1和4来表示。测试时钟的价值意味着必须选择一个定义：这是时钟微积分的主要目标。有些定义是非常直观的：图4（a）中y线1的定义的选择直接来自于将方程（2）转化为定向定义。 看一眼计数器就 可以看出，在一般情况下 ，[11]控制流（时钟）和数据流（变量值的计算）之间的联系是由语法决定的。例如，解析方程y：= x defaultz表示需要计算y，通过yx定义y，以及通过z定义y。因此，图4（a）的代码来自第2行。因此，一旦从同步中推断出控制流程，代码就直接跟随。48M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-[12]条件钟的定义不需要微积分来处理，因为它不需要同步化来具体说明（也见4.3节）。例如，参见图4（b）第2行b[c]的定义（实际上，SIGNAL编译器抑制了这个无用的变量）。M. Nebut / Electronic Notes in Theoretical Computer Science 88（2004）39-49对于自定义覆盖的定义是复杂的： （3）意味着y^受到递归方程y^=N^y^的约束;实际上，由于被认为是输入时钟，因此没有给出定义，图4（b）的第1行。最后，一些时钟包含和等价的知识被用来优化控制结构，避免在执行时无用的测试。公式的同步化（4）单包含sz^y^和w^z^（因为如果by不为真，则m∈bz不可能为真因此，在Fig.4（c）by上的测试，bz和bw是嵌套的。测试也是因式分解的：by只测试一次，而y是写 （ 第 2 行 ） 和 读 （ 第 5 行 ） 。 此 外 ， 时 钟 变 量 的 数 量 被 优 化 ：Sincesynchronization实现y=x，因此不需要针对某个变量b x。4.3共时性：从方程到定义如果一个组件可以在只提供输入值而不提供其状态信息的异步环境中执行，则该组件是内循环的（更多细节请参见[3该组件无法确定性地测试其输入的状态（直观上，因为这样的测试是阻塞的）：它不能确定性地测试多个输入时钟。因此，一个内插组件必须拥有一个标识的主时钟（这只是它的激活时钟），这是可执行代码的唯一输入时钟。因此，所有其他（必然较慢）的时钟必须从主时钟递归定义LUSTRE组件是由结构内：一个参考质量-给定一个时钟，任何其他时钟都是已经存在的时钟，或者一种时钟，在功能上由现有时钟的欠采样定义我-GNAL更一般：不能确保Endochrony。 此外，如第4.1节所述，时钟不仅通过欠采样连接在一起，还通过运算符、和\的任意组合连接在一起。最后，一些基本的关系同步不能转换为函数。示例4.1图4（a）的代码不能被确定性地执行，并且不表示时钟的结束：创建的时钟不是主时钟，因为计算数据是输入时钟的函数。我的天clockonFig. 4（b）和4（c）是y^。 考虑方程y^

下载后可阅读完整内容，剩余1页未读，立即下载