同步系统模型下的全局异步局部同步设计条件及挑战

理论计算机科学电子笔记245（2009）69-84www.elsevier.com/locate/entcs同步系统比乔伊河何塞1 薛斌2桑迪普K.Shukla3FERMAT实验室弗吉尼亚理工学院和州立大学布莱克斯堡，弗吉尼亚州，美国摘要安全关键的嵌入式应用程序通常是分布式的。例如，汽车控制或航空电子控制中的软件分布在大量分布式处理器上，这些处理器通过某些特定领域的总线连接。这些应用程序的正确性是至关重要的，因为它们的安全性至关重要。 同步编程模型（例如Esterel、SIGNAL、Lustre）使同步假设（零时间模块内计算和零时间模块间通信），同时对这样的应用进行建模，使得模型更容易验证。一旦得到验证，使用这些假设构建的模型需要分布在基于异步通信的平台上，这带来了全局异步和局部同步（GALS）设计的挑战。 在全局异步通信介质上保持完全同步模型的正确性意味着对同步模型施加各种限制。 在多面体编程模型领域（示例通过SIGNAL语言），在20世纪90年代初提出了称为“内等时性”的性质。 各个模块的内时性确保了从模块规范安全地顺序生成代码，而等时性确保了模块之间的安全通信。本文首先给出了一个更一般的等时性充分条件。其次，我们推广了弱内禀模的等时性定义。此外，我们引入了方向等时性的概念，它为模块之间在一个方向上而不是在另一个方向上的安全通信提供了充分的条件。 本文中的结果不仅简化了对GALS中可以实现多变量规范的条件的理解，而且还对因果关系和等时性提供了有趣的见解。当同步模块作为IP重用时，可以检查这里描述的条件，以查看这些模块是否可以以与其同步组合相同的行为异步组合关键词：同步规划模型，多时，信号，内时，等时，全局异步局部同步系统，单向等时1引言由于两个事实，全局异步和局部同步（GALS）设计在片上系统（SoC）设计领域越来越重要：首先，由于时钟速度的提高，以及当今设计中元件数量的增加1 电子邮件地址：bijoy@vt.edu2 电子邮件地址：xbin114@vt.edu3 电子邮件地址：shukla@vt.edu1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.02970B.A. Jose等人/理论计算机科学电子笔记245（2009）69在时钟周期内从芯片的一端到达另一端变得困难;第二，时钟分配网络中消耗的功率与计算中消耗的功率相比太因此，对多个时钟域的推动，以及跨时钟域的信号引起了GALS设计的兴趣。由于同步设计比异步设计容易得多这一点已被广泛接受，因此开发用于GALS设计的方法和工具是很重要的。然而，还有另一种GALS设计，它在SoC设计中的GALS应用变得至关重要之前就已经存在在20世纪80年代早期，各种同步编程语言，如Esterel，Lustre，SIG-NAL等，的开发，以简化嵌入式控制软件的设计，使用一个简化的抽象所花费的时间来计算和通信。在同步性假设下，为控制相关的计算建立模型是容易的。也更容易验证这些模型的计算正确性。然而，同步假设是相当强的，假设计算需要零时间，同步模块之间的通信需要零时间。类似于硬件设计的情况，如果后续输入（或输入的子采样）之间的到达间隔时间大于计算时间，则可以容易地验证计算零时间。然而，当模块分布在异步通信介质上时，例如CAN总线（在汽车应用中），所有信号的零时间通信和同步通信并不容易合理。这在1990年代引起了大量的研究。同步模型的各种条件下，整个系统可以有相同的计算行为，尽管异步媒体被发明。在[2，3]中，引入了一个称为“内等时性”的条件所谓GALS部署和原始同步模型之间的这种等效概念被称为在本文中，我们假设，每当我们说一个同步模型和它的GALS实现是等价的，我们的意思是在[2，3]中，这个条件有两个部分。首先，各个模块必须是“内时”的。非正式地说，这意味着模块规范本身应该有足够的信息，以便在编译成顺序软件组件时，它们能够在需要时准确地对输入进行采样，而不会遗漏任何输入更改。在内时性中，序列性是一个首要的前提条件，导致了一类满足这一条件的限制性同步模型。在后来的作品中[16]，这个条件被放宽，使得模块的严格顺序可实现性不是主要的。允许不干扰模块实现的全局确定性的局部非确定性，导致弱内时性的概念弱内点类B.A. Jose等人/理论计算机科学电子笔记245（2009）6971模严格地包含内模类弱内插模块在它们的规范中有足够的信息，以便它们的多线程或并发实现可以在需要时准确地采样所有输入，而不会错过任何输入更改。因此，弱内时是模的一个较弱的限制。另一方面，等时性的概念不是关于模块本身，而是关于模块之间的通信。在[2，3]中，这个想法是以两种方式表达的。第一种方法是从它们的异步通信轨迹中重建同步通信第二个公式是一个充分的条件，可以解释如下。如果两个模块通过多个信号进行通信，则信号必须同相。假设模块M1和M2通过信号x，y，z，w进行通信，使得M1计算信号x，y的值，并且M2消耗这些值，并且z，w值由M2产生，而M1消耗这些值。那么，为了使M1和M2之间的通信被认为是等距的，必须是这样的情况，即M1必须总是在相同的时刻产生x，y的值，而M2在产生z，w时也是如此。如果发生这种情况，那么M1将始终等待y的值到达，如果x的新值到达，反之亦然。因此，M2可以重建x，y的产生的同步行为，而不必从M1获得任何专门的握手信号，反之亦然。然而，这是限制性的，并且被设计为在零时间计算和通信中工作的模块可能不容易保证该条件。它还需要模型检查来检查这是否成立。如果这一点成立，那么M1和M2可以很容易地通过它们之间合适的以太网流控制协议跨越异步介质。本文推广了文献[2，3]中的充分条件，给出了用信号间的时钟关系刻画等时性的一个在另一个方向上，我们提供了弱内点模的充分条件，这需要修改用于内点分量的定义。在[17]中，考虑了弱内模复合和相应的构造，使全复合等距.然而，我们的目标是找到方法来检查弱内模的集合，如果它们满足修改的等时性条件，使得它们的组合在GALS设置中是安全可实现的。因此，与以前的工作相比，在本文中，我们找到了直接编码为时钟约束或间接从数据流方程推断的时钟关系的条件，这将意味着所分析的原始同步模型的GALS实现是正确的。在本文中，我们不进入这样做的算法，而是停止在时钟关系方面提供等时性的充分在我们继续之前，我们必须简要地讨论一下在这项工作中使用的编程模型如前所述，同步编程模型有多种变体。Esterel [4]是一种基于同步假设的命令式编程范式另一方面，Lustre [9]描述了数据流方程来描述嵌入式应用程序中固有的计算TheLustre se-72B.A. Jose等人/理论计算机科学电子笔记245（2009）69mantics假设这些方程是基于全局时钟节拍来评估的，因此适合于实现全局时钟同步的分布式应用，例如时间触发架构[12]。我们的工作基于SIGNAL [8]语言和Polychrony框架[7]。SIGNAL是一种数据流同步语言，在Java中更接近Lustre。然而，SIGNAL指定的不是数据流方程，而是数据流关系（因此SIGNAL更多的是在指定域而不是编程语言）。此外，SIGNAL不假设任何全局时钟来调整数据流的计算，而是SIGNAL模型中的每个信号都基于其自身的速率（时钟）进行采样或计算。这些速率与时钟关系有关，时钟关系从数据流关系（使用）推断或通过模型中写入的直接时钟约束。然后用时钟演算[1]对这些速率进行分析，内时性基本上由时钟演算决定。因此，可以通过求解对时钟关系进行编码的布尔关系来检查内时性（尽管具有高复杂性）。本文旨在为等时分析奠定基础本文的分析和贡献安排如下。第二节给出了同步语言的理论背景，特别是SIGNAL语言.讨论了SIGNAL中的运算符和基于码率关系的码生成策略。我们还定义了SIGNAL中的速率关系，并在本节中介绍了表示它们的形式。第3节包含控制允许的组合要求的断言，并根据SIGNAL模型的属性对其进行检查。定义了通信信号及其结构，这将在整个论文中用于解释其他贡献。在第4节中给出了具有正确和不正确情况的示例的分量的方向合成从基于数据流的设计到GALS实现的过渡中的一个第5节将回顾分布式实现的代码生成建议，并对相关工作进行评论。第6节将通过详细介绍本文的贡献来结束本文。2信号建模和速率关系SIGNAL等数据流同步语言通过关系捕获数据流，并通过过程构造捕获语法模块化来表达计算。因此，在SIGNAL中，可以编写包含输入、输出和内部变量的过程描述。变量被称为信号，因为SIGNAL过程中的变量在语义上表示值的无限序列，这些值在时间上是可变的。x定义了将更新或评估所有x的数据（clock）信号可以具有各种数据类型，例如整数、布尔值、实数、事件等。计算被表示为各种信号上的并发活动。有四种基本的运算符类型（人们可以基于它们定义许多派生运算符）：函数，采样器，合并和延迟。可以使用所有可能的数据流函数（计算库元素可用于这些函数B.A. Jose等人/理论计算机科学电子笔记245（2009）6973通常，函数运算符f应用于一组信号，比如x1，.，xn以在信号y上产生值，并被写为：y：=f（x1，...，xn）（ 1）这意味着y的新值由函数f通过对信号x1，x2，.，xn.建模者有责任确保每个信号的值以其速率存在。换句话说，建模器本身对信号的使用将向编译器指示x1，x2，.，xn的更新是相同的，y以相同的速率更新，因为通过同步假设，f在零时间内计算。SIGNAL编译器假设环境将在每个时钟时刻提供输入，并且如果时钟演算显示无法保证这一点，则会显示错误。Sampler操作符的使用方法如下：y ：= x当c（2）其中c是某些信号的布尔条件，y和x必须具有相同的数据类型。这句话意味着，无论何时计算或采样条件c，但是如果c被赋值为false，那么y就不会得到新的值。 因此，y的更新速率小于x的更新速率，或者c被评估为真的速率Merge运算符称为y ：=x default z（3）其中x，y和z必须具有相同的数据类型，并且每当x被采样或计算时，y就会获得x的值。如果x没有被计算或更新，但z得到了计算或更新，那么y得到了那个值。因此，这是一个确定性合并，优先级为信号x而不是z。Delay运算符由$表示，示例用法如下：y ：= $init k（4）这意味着每次x更新时，y都会得到x的前一个值。在第一个例子中，y用k初始化。从1开始的函数运算符将使结果信号和输入信号的速率相等。类似的是延迟算子的情况，它使输入和输出信号的速率相等。等式2中y的速率可以表示为x的时钟和[c]的时钟之间的交点（c存在且为真）。类似地，我们可以观察到，当使用等式3中的合并运算符时，发生x和z的时钟的并集。表1总结了SIGNAL中输入和输出信号之间的时钟关系以及运算符。因此，一个数据流关系系统代表一个数据流网络。然而，在网络中有一个因果关系的概念，它决定了每一组74B.A. Jose等人/理论计算机科学电子笔记245（2009）69SIGNAL算子信号表达式时钟关系功能y = f（x1，x2，. ..，xn）yb= xc1=. . . =xcn采样器y=x当cyb=xb[c]合并y = x默认值zyb=xb<$zb延迟y=x$init kyb=xb表1SIGNAL运算符及其时钟关系信号必须被评估。尽管SIGNAL中的语句是并行组合的，但在某些信号之间存在依赖性，这需要这种排序。这种因果关系是由采样器操作符中的布尔高斯、输入的可用性等引起的，这引起了速率关系。我们感兴趣的是这些速率关系的评估，以及它们是如何影响组件之间的通信的。SIGNAL语言有一个称为process的语法结构，它是模块化数据流规范的方式。进程被假定为并发模块。因此，如果过程边界被删除，则会得到一个大型数据流网络，其中操作员通过信号与其他操作员连接。在模块或进程的边界处的信号也按照同步假设在零时间通信。然而，当在GALS环境中分发时，通常在不同的站点部署单独的模块。因此，跨越模块边界的信号需要特别注意，因为不能再假设这些信号等时性的概念特别涉及这些信号。还值得注意的是，数据流网络不必是语法上非循环的。这可能是令人困惑的，因为如果在零时间计算中有一个循环，它似乎是不可实现的。但是，必须记住，并非所有运算符都在前面讨论的同一时间点进行计算。 所以如果 循环使得在数据流网络中的同一循环上的所有运算符不是以相同的速率计算，因此实际上可以毫无问题地实现数据流。这些被称为建设性周期。因此，操作员计算的信号的时钟必须相关，以检查这种情况。当信号跨越模块的边界时，这对于检查是特别有问题的，因为模块可能来自不同的建模者，并且可能已经被编译成代码。因此，当将模块导出为IP时，每个模块内部所有信号的时钟关系必须与编译后的模块一起导出不同模块之间的时钟关系应使用时钟演算进行在本文的其余部分中，我们假设在尝试创建模型的GALS实现之前已经检查了这样的循环。为了更好地理解这个范例，现在让我们看一个示例SIGNAL程序。B.A. Jose等人/理论计算机科学电子笔记245（2009）6975过程采样器=（？ integera; event b;！integerc;）（|c：= a当^b|）SIGNAL程序Sampler使用when原语用另一个输入b对输入信号a进行采样。采样输出由c表示。 这里，三个信号的速率可以不同，但是c的速率由a和db的速率确定。签名的签名（clock）不是通过签名来确定的。采样器输出c的示例如下：c=（5）我们现在在SIGNAL上下文中正式定义时钟关系，这将在本文稍后用于定义通信要求，等时性等。定义2. 1给定一个符号V的集合，eachsignalx∈V具有n c l ock x {\displaystyle ncl ock x{\displaystyle n c lockx}}，它是x更新的（可能无限）时刻集合。如果信号x被输入到系统中，则x在采样x时被采样。所述放大率必须足以捕获其所有更新。信号的时钟指定信号何时有效。当两个信号在SIGNAL语句中的赋值运算符两边使用时，它们的时钟被称为相关的。现在我们正式定义一个时钟关系。定义2.2给定一组信号V，两个信号（x，y）∈V被称为通过y循环关系rxy，如果两个独立的循环（xx，y）满足关系式我是一个很好的朋友。 例如，如果x和y的块是相等的，则rxy=（x^=y^）。如果我们考虑用另外两个信号来定义一个信号（如在Sampler/Merge中），那么它们通过关系谓词r xyz相关联，其中x，y，z ∈ V，x用y和z来定义。例如，在Merge语句中x：=ydefaultz，rxyz=（x^=y^z^）。在表1中，信号以直接的方式相等，而不需要求解任何外部方程。这被称为直接关系。现在，如果两个信号不存在直接关系，并且如果可以通过求解一组时钟关系来找到它们之间的关系，则可以说这两个信号是间接相关的。现在我们引入一个特殊的时钟关系这个新的关系可以用来断言，在所考虑的信号的时钟之间不存在直接或间接的关系。定义2.3信号x和 y是独立的，当且仅当时钟关系rxy=（x^#y^）。SIGNAL程序使用Polychrony编译器[7]合成为ANSI C代码Polychrony编译器仅为endoCastSIGNAL程序生成C代码。非正式地说，如果一个SIGNAL规范的操作存在一个静态的顺序调度，那么这个规范被称为是内隐的。目前，Polychrony工具从并发的SIGNAL规范中生成顺序C代码。一个不那么严格的道具-76B.A. Jose等人/理论计算机科学电子笔记245（2009）69弱内时性。即使连续计划也满足此属性是不可能的，但是局部并发调度（对于某些操作符具有不确定的执行顺序）使输出保持确定性。因此，如果多个可能的行为在没有约束输出的情况下对于一个规范是可容许的，那么这样的SIGNAL规范是弱内隐的。更详细地描述内年代，弱内年代，在[11]中可以找到适当的例子。这些属性在GALS架构的设计中至关重要，用于将操作排序和分布到不同的站点。在从各个模块生成的代码的GALS部署中，由于在从一个模块到另一个模块的通信中的各种信号的不相等延迟以及由于缺乏全局时钟，进程之间的通信肯定会失去同步。内同步涉及组件中信号速率之间的关系，并且不足以保证正确的通信。如前所述，如果各种同步模块之间的公共变量满足等时性等属性，则可以确保正确的通信[3]而不会丢失系统的正确性等时性是适用于通过公共变量通信的同步模块的集合的条件。当通信是同步的（零时间）时，更新模块更新共享变量的时刻，以及读取这些变量的更新的模块看到更新的时刻是相同的。然而，当模块是分布式的，并且它们的通信是异步的（GALS部署）时，这就不再正确了。这些共享变量的更新和采样条件必须有某种关系，以便GALS部署以与完全同步模型相同的方式工作。这[2，3]定义了内等值线系统，其组件是内等值线，它们之间的通信是等值线。在那里，等时性已被研究的基础上组成的同步过渡系统（STS）。如果一对STS（Φ1，Φ 2）的同步合成上的异步观测（迹线）与去同步STS的异步合成的异步观测可以相等，则称这对STS（Φ1，Φ2）是等距的[2]。从[2]，（Φ 1||Φ 2）a =Φ a||aΦ a4（6）1 2当具有一组公共变量的两个STS Φ1、Φ2和Φ2具有以下性质时，等时性的定义被证明是成立的：如果V是Φ1和Φ2之间共享的变量的集合，并且V1=V由Φ1更新，并且由Φ2，且V2≠V由Φ2代替，且由Φ1代替，且V=V1≠V2，V1≠V2=V，那么V1中的所有变量必须具有相同的时钟，V2中的所有变量必须具有相同的时钟。换句话说，如果在任何时刻，Vi（i=1，2）的一个变量不存在（没有值），那么该Vi的所有变量都必须不存在。然而，事实证明，这是一个充分的条件，但不是必要的。等时线的实际定义可以通过变量集V1和V2上更一般的条件来满足。 这种概括有几个优点。 首先，它简化了4此处Φ a代表去磁STS，||a表示异步合成B.A. Jose等人/理论计算机科学电子笔记245（2009）6977与[2，3]相比，对等时性的理解基本上是一致的。其次，将其推广到弱内点模。第三，方向性的等时概念自然产生。3同步系统在GALS系统中，每个组件都需要通过通信线路以异步方式进行交互通信介质的性质定义了组件之间所需的组成类型。在异步通信介质中，在模块之间需要缓冲器来平衡各个模块的速率。在实践中，缓冲器的大小不可能是无限的，这限制了模块速率的差异另一个妨碍系统正常运行的因素与该因素相关的问题有两个方面：i）发送器和接收器共用的信号的时钟必须被共享，以及ii）共用信号之间的时钟关系将必须在两个模块中保持。在这里，我们考虑的组成endo-endo-endo-process和弱endo-endo-endo-endo-process。我们假设在整个过程中的文件，提供的程序或IP的组成没有组合循环，是无错误的。此外，当程序或IP被合成时，必须检查它们是否存在作为合成的结果而创建的任何新的组合循环3.1内分泌过程对于内循环过程，存在静态计划。不同的输入信号有自己的时钟，它们与速率关系相互连接。根时钟将作为Polychrony编译器中这些速率关系的结果而形成，其相当于SIGNAL域中的全局时钟。因此，对于内隐过程，过程中的每个信号之间存在直接或间接的关系这种过程的优点在于，每个信号的时钟流（没有时钟的值的顺序）连同时钟关系足以为整个过程创建时钟同步时钟流，即，不需要外部时钟信息在信号术语中，这被称为然而，内同步不足以保证正确的通信。下面的例子将说明这个问题。处理Endo1=（？ a，b; integer out1，out2;）|输出1：= a + b| out 2：= a + 1当out 1> 0时|）end;process Endo2=（？integer out1，out2;！integerc;）（|c：=输出1+输出2|）end;在此，处理Endo1具有两个输出信号，其由Endo2通过异步介质接收根据输入到Endo2的到达顺序，c的值将改变。下面显示了两种情况下的重建c为不同的利率78B.A. Jose等人/理论计算机科学电子笔记245（2009）69ABC一102输出1-112B-两个10出213输出1-112C04出2⊥13在Endo1中，out2的值仅在out1> 0的瞬间更新。在通过异步介质传输之后，out1和out2之间的同步丢失，因此对于Endo2不能观察到out2的缺失值。Endo2只能分别观察out1和out2的数据序列，如右图所示。通过c：= out1 + out2，Endo2假设out1和out2同时更新，这与Endo1生成它们的方式相矛盾。因此，内时不足以在组成过程时确定输出。随着确定性计算，确定性通信必须保持。等时性是关于系统之间通信的属性，它指定它们是否可以正确组合。对于内消旋过程，只要满足某些条件，我们可以保证适当的成分。在进入检查合成过程中的从[3]中，我们理解了构成内隐过程的严格条件。断言A1：对于内循环过程P1和P2，如果P1在同一时刻产生所有事件，P2在计算之前等待所有输入到达，反之亦然，则可以保证等时性。文[3]中的这一论断是内生过程的一个充分条件在GALS域中，这通常是一个严格的条件，并且很难实现。合成过程中的关键因素是合成IP的时钟信息因此，我们将断言A1以更一般的形式用于同步进程： 断言A2：对于两个通信进程P1和P2，公共信号的时钟信息必须共享。在分布式环境中IP之间的时钟信息共享涉及交换关于这些内插过程的时钟关系的元信息该信息将包括信号及其速率关系，可用于检查等时性。一旦IP作为IP实现和交付，就不可能在IP中添加任何时钟信息。因此，元信息将有助于检查等时线并重新设计IP以使其等时线。现在我们形式化一个等时性的充分条件。对于两个内插过程Pi和Pj，其中的信号集合分别为Vi和Vj，我们定义一个通信结构Cij。定义3.1元组Cij=（Wij，Rij）定义了一种通信结构，它表示时钟信号从Pi到 Pj的投影，其中i) Wij=Vi<$Vj，ii) Rij={rij，根据Pi中的v^b和v^c定义v^a<$（va，vb，vc）∈Wij×Wij×Wij}B.A. Jose等人/理论计算机科学电子笔记245（2009）6979通信结构由两个进程中的共享信号和它们之间的时钟关系组成。关系r将取决于Pi中的信号之间的关系。对于内隐过程，任何两个信号之间都存在直接或间接的现在A2可以重写如下。断言A3：给定两个进程Pi和Pj，其通信结构Cij={Wij，Rij}和Cji={Wji，Rji}，如果Rij=Rji，则Pi和Pj是同构的。可以使用从这些IP中提取的元信息来检查公共信号及其速率关系的匹配。IP本身没有知识的相似性率关系，虽然他们表现在等时性。现在，让由于Endo1和Endo2经由信号out1和out2通信，因此W12=W21={out1，out 2}。接下来，让在Endo1中，R12={r12=（o_iut2=^a_i^}，在Endo 2中，R21={r21=（o_iut2=^a_i ^}，出1出 2[out1>0]）出2出 1或1）}，对于R12/=R21，并且对于A3不存在。这个例子在两个方面不能满足等时性要求首先，它没有以相同的方式在两个IP中定义out 1和out 2之间的关系。第二，输出信号不是根据第一IP中的共享信号来定义的。从定义3.1，我们可以看到，关系是在共享信号集合Wij中存在的信号之间。因此，通信结构必须由信号来完成，这些信号定义了共享信号之间的关系。为了理解断言A3如何验证两个内隐过程的等时性，我们修改了上面讨论的例子内循环过程Endo 1由一个新的内循环过程BEndo 2组成。Bendo 2的速率关系为如下：R21={r21^}。在这里，出2出1 =（out2 = [out1> 0]）通信信号在两个过程中都保持（R12=R21），因此等时性得到验证。纠正该示例的另一种方式是共享信号a以及out1和out2，并在通信IP中保持它们之间的关系。由于在组合时纠正IP块是不可行的，因此在IP的设计过程中必须注意确保通信结构和关系是完整的处理Endo1=（？a，b; integer out1，out2;）|输出1：= a + b| out 2：= 1当out 1> 0时|）end;process BEndo2=（？integer out1，out2;！integerd;）（|c：= 1当out 1>0时|d：= c + out2|）end;3.2弱内生过程如果一个过程满足[16]中定义的金刚石性质，则称它是弱内禀的。弱内时性是内时性的一种不太严格的形式，其中存在可以以多个顺序调度的不相关信号，但仍然生成确定性输出。这减轻了时钟约束，并使流程的组成更简单。下面给出两个弱内点过程的例子80B.A. Jose等人/理论计算机科学电子笔记245（2009）69IJ纪纪3434b1c1b2c143b1c1b2c134IJ4343过程Wendo 3 =（？integer a1，c1;！integer b1，b2;）|b1：= a1 + 1|b2：= c1$init0 + 1|）end;process WEndo4=（？integer b1，b2;！integerc1，c2;）（| c2：= b1 + 1| c1：= b2 + 1|）end;在这里，进程之间存在双向通信通信结构C34和C43对于公共信号是相等的。W34和W43将包含b1，b2，c1。我们已经从[16]中知道，两个过程Wendo 3和Wendo4将具有正确的成分并且是等离子体。A3可以是一种...通过计算闭合关系式R34={（b^2=c^1）}和R43={（b^2=c^1）}来确定。另一个重要的因素是弱熵过程中信号的时钟独立性。在Wendo 3中，时钟（b^1，b^2）和（b^1，c^ 1）是完全独立的。悬而未决。在R43中也是如此。为了正式表示这种情况，我们使用零时钟关系，以定义扩展时钟关系集RJ，RJ和他们的大伊济通信结构CJ，Cj，对于两个弱内禀群Pi，Pj。伊济定义3.2对于弱内禀过程Pi和 Pj，它们的扩展时钟关系集是RJ=Rij<${#}，RJ=Rji{#}和它们的扩展通信nication结构是CJ={W ij，RJ}，CJ ={W ji，RJ}。伊吉这一定义表明，与内禀过程不同，对于两个弱内禀过程，具有时钟关系r∈RJ和r∈Rj的连续过程Pl和Pm可以Lm等于必须指出，零时钟关系意味着信号之间没有关系，也不应该有任何关系，而不是关系未指定。我们将使用这个扩展的时钟关系集来评估两个弱内禀过程的等时性断言A4：给定两个弱内点过程Pi和Pj，nication结构CJ={W i j， RJ}和CJ= {Wji，RJ}分别，如果伊吉J= RJ，则Pi和Pj是同构的。我们通过分析扩展的时钟关系集Rj来分析断言A4和Wendo3和Wendo4的J。Wendo3和Wendo4之间的共享变量是b1，b2，和c2. 因此，我们有RJ34b1b2 =（b^1#b^2），r34=（b^1#c^1），r34=（b^2=c^1）}和dRJ43b1b2 =（b^1#b^2），r43=（b^1#c^1），r43=（b^2=c^1）}因此，RJJ.基于断言A4，Pi和Pj是同构的，与已知结果一致。由于任何内禀过程也是一个弱的虽然断言A4适用于两个内分泌过程，但断言A4也适用于两个内分泌过程。这证明了一个统一的方法，succiently评估正确的沟通（等时）的两个内分泌或两个弱内分泌过程。RR={r={r=RB.A. Jose等人/理论计算机科学电子笔记245（2009）69814定向等时在前几节中，我们讨论了两个内禀过程或两个弱内禀过程之间的复合。内隐过程到弱内隐过程的复合是GALS领域特别感兴趣的。向现有设计添加新模块，无需双向82B.A. Jose等人/理论计算机科学电子笔记245（2009）695656656556788765如果这种情况下的断言为真，则可以很容易地验证在进入与构图相关的定义之前，让处理Endo5=（？整数a1，b1;！integer c1，d1;）（|a1^=当b1 > 0时|c1：= a1+ 1|d1：=b1|）end;processWEndo6=（？integer c1，d1;!integer e1，f1;）（|e1：= c1+1| f1：= d1+1|）end;处理Wendo7=（？ integer a2，b2;！integer c2，d2;）|c2：= a2 + 1 |d2：= b2 + 1|）end;处理Endo8=（？整数c2，d2;！integer e2，f2;）（|c2=当d2>0时|e2：= c2+1| f2：= d2|）end;我们可以很容易地发现Endo5是一个内循环过程，类似于Endo8，而Wendo6是一个弱内循环过程，类似于Wendo7。这两种成分的区别仅在于它们的传播方向。在Endo5和Wendo6的组合中，Endo5和Wendo6的扩展通信结构CJ={W56，RJ}和CJ={W65，RJ}，其中W56=W65={c 1，d 1}，RJ=第56条^^}，RJ={r65=（c^1#d^1）}。这是为了，RJ不等于c1d 1=（c1 = [d1> 0]）65c1d156J.我们分析了Wendo 7和Endo 8之间的第二个组成，方式，我们有RJ78c2d2 =（c^2#d^2}其中ch不等于RJ87c2d2^ ^您的位置：（c2 =[d2> 0]）}。Endo 5与Wendo 6的组合是正确的，因为Wendo 6中的语句是并发的。Endo5中的时钟依赖性不相关，因为Wendo6中的状态是独立的。WEndo6可以用多个将具有相同输出的传感器重建另一方面，从Wendo 7到Endo 8的通信导致值的丢失，因为Endo 8仅在d2> 0成立时才获得c2的值。从这些例子中，我们可以得出结论：1) 断言A4不是等时性的必要条件，因为它可以拒绝Endo 5和Wendo 6的盒状组合物;2) 内隐过程与弱内隐过程的正确通信取决于其通信方向;因此，如果信息传递方向是单向的，则一个内隐过程可以合成为一个弱内隐过程。4.1两个过程PiPj−→方向上是等轴的，||P j，如果并且仅当从Pi到 Pj的通信的正确性得到保证，而相反的方向不是。所谓通信正确性，是指通信信号的正确等价性。在异步通信之后，顺序被保持，并且信号不以与发送过程中的速率关系相矛盾的方式被重构。为了测试方向等时性，零时钟关系与正常关系集一起使用R={r={r=B.A. Jose等人/理论计算机科学电子笔记245（2009）6983IJ纪IJ纪定义4.2确定的时钟关系r和空时钟关系“#”之间的偏序<<“”被定义为# r。这种偏序将导致任意两个扩展时钟之间的偏序≤关系集RJ和RJ。定义4.3对于两个合成过程Pi和 Pj， RJJ当且仅当伊杰河∈RJ和它的对应的rji∈RJ，存在一个偏序使得阿布伊杰r ij ≤ r ji。阿布吉AB AB断言A5：给定一个内隐过程Pi和一个弱内隐过程−→P，P，P当且仅当RJ≤RJ。JI ||jji对于本节开头所示的示例，RJ≤RJ并且因此−→65Endo5||温多6.从Endo 5到Wendo 6的通信正确，相反的方向不能保证。 我们可以观察到类似的行为，Wendo7和Endo8。断言A5不仅限于（内循环，弱内循环）过程，它还可以通过检查任何一对共享变量之间的时钟关系来分析任何两个弱5相关工作和代码生成机会文献[2]讨论了等时性和内等时体系的组成性。并给出了同步合成与异步合成等价的充要条件。基于此属性的相关工作试图对同步规范的异步实现进行建模[15]。它表明，异步实现是其同步规范的正确细化，因此GALS实现可以从同步模型执行。在[14]中提出了一种代码生成策略，通过单独编译多个规范并利用弱[17]中讨论了通过削弱内时性来组成等时系统的另一种策略。他们对松散的时间触发架构进行了形式化分析，以表明等时性可以在非内循环组件的组合中保持在其他同步语言中，已经提出了不同的代码生成策略，用于在Esterel中，代码已被划分为原子任务，通过引用包含依赖关系的链表[6]来并行调度。更多的重点是组合性的过程，这将有助于以后设计的编译器的分布式实现的目标在SIGNAL语言中，最早的工作之一是关于SIGNAL程序的聚类和可扩展性的讨论[13]。在同步语言的分布式执行中，一个突出的工作是将它们转换成一个公共的目标代码（OC），然后将这些代码并行化到许多计算站点[5]。在这项工作中，没有对模块或模块间通信进行表征来检查分布式部署。假设全局时钟是通过时钟同步算法分布式实现的。然而，由于全球时钟同步是昂贵的，≤R84B.A. Jose等人/理论计算机科学电子笔记245（2009）69在SIGNAL文献中或在本工作中，它没有被考虑。相反，人们寻求这样的昂贵的协议将不需要GALS执行的特征。多线程代码生成仍然是实现同步程序的分离但集中的实现的重要里程碑。在当前的Polychrony编译器中，只能实现endocomponent进程多线程代码生成编译器的测试版正在开发中。弱内隐程序的基于进程的线程化，以及用于组成进程的单独编译，已经使用现有的SIGNAL编译器[10]实现，并且在[11]中已经提出了基于同步数据流的线程化策略。同步程序的分布式实现需要设计的可扩展性，以改进或向现有系统添加新的IP通过可扩展性，我们的意思是一个新的IP到整个系统的组成和分布式实施内编译过程当前生成顺序代码，只有当整个系统被重新编译并且断言A1、A2和A3被满足时，该顺序代码才能弱内循环程序由于其并发性和空时钟关系，更适合于扩展和分布式实现。这适用于定向等熵系统中的弱内熵过程。通过给出SIGNAL同步环境下等时性检验的形式化描述，给出了GALS环境下同步IP组成的验证方法6结论使用同步编程模型的嵌入式软件编程已被发现适用于GALS架构。在同步IP之间使用异步通信所面临的挑战需要对IP的组成进行更多的研究多年来，“等时性”的概念已经发展成为一种性质，它为同步分量的正确组成提供了充分的条件。同步域的性质如内时性、弱内时性及其对等时性的影响是同步系统合成的重要内容。在本文中，我们已经正式的条件，等值线组成，并提出了一个通信结构，涉及所需的组成参数。基于通信结构提出的断言将作为对IP组合的充分测试我们已经表明，弱内同步放宽了严格的条件，组成的IP和正确性，可以保证通信对一个弱内同步进程。本文中使用的一个新的零时钟关系使我们能够定义方向等时性，这为我们提供了一组特殊的规则，以确保单向通信的正确性最后讨论了这些特性对分布式体系结构代码生成的影响IP重用和将IP添加到GALS系统中将受益于对同步IP的等熵组成的研究。B.A. Jose等人/理论计算机科学电子笔记245（2009）6985确认我们要感谢Jean-Pierre Talpin（INRIA）和Dumitru Potop-Butucaru（IN-RIA）就本文件的内容进行了有益的讨论。这项工作得到了NSF资助CCF-0702316和SRC任务1818的部分支持。引用[1] Amagbegnon，T. P.，L. Besnard和P.L. Guernic，数据流同步语言信号的实现，在：ACM程序设计语言设计与实现研讨会论文集（PLDI163-173.[2] Benveniste ， A. ， B. Caillaud 和 P.L. Guernic， 从 同 步 到 同 步 ， 在 ： Proc 。 ConcurrencyTheory ， 1664（1999），pp. 162-177。[3] Benveniste ， A. ， B. Caillaud 和 P.L. Guernic ， Compositionality in Data Flow SynchronousLanguages ： Specification and Distributed Code Generation ，