分布式程序的输入/输出等价性

理论计算机科学电子笔记137（2005）25-46www.elsevier.com/locate/entcs分布式程序等价性推理8月2日星期三Informatica La Salle，巴塞罗那Ramon Llull大学摘要本文提出了一种新的分布式命令式程序的输入/输出等价性概念。它保留了输入/输出关系，包括初始/最终状态和通信信道值。对于它的数学正义，Manna和Pnueli的语义框架，基于有限转移系统和约化行为，扩展了输入/输出行为的概念。 一组法律的等价性进行了概述。在新的语义中定义了一个用于替换输入/输出等价过程引用的演绎规则。该规则适用于分解分布式程序简化证明，介绍了在以前的工作，其中使用的法律建立之间的等价性一个顺序和一个并行通信程序。他们将消除通信作为他们的步骤之一个这样的证明，一个流水线处理器模型的大纲，包括在内。关键词：分布式程序，并行程序，输入/输出等价，等价保持变换，验证，程序简化，同步通信，分布式程序的法律。1介绍具有显式并行性和通信语句的命令式语言提供了一个直观，明确和完整的框架来表达分布式和并发程序和系统模型，并具有验证所需的清晰度。 OCCAM [11，12，13]，Manna和Pnueli的简单编程语言SPL [15，16]，SPIN模型检查器的PROMELA [10]，以及1电子邮件：miqbe@salleURL.edu2电子邮件：fbabot@salleURL.edu3电子邮件：augc@salleURL.edu1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.03826M. Bertran等人/理论计算机科学电子笔记137（2005）25[7]中共享变量语言SVL++代表了这两种操作符号。等价推理大量用于数字、矩阵和其他领域。然而，对于命令式程序，尽管它有可能成为一种非常直观的验证活动，但它还没有在并发和分发中进行过探索。通过消除[2]是一个等价性证明，因为它减少了状态向量的大小，可以补充其他证明方法，如模型检查[10，17，5]和交互式验证[3，14]。它是基于一组适用于此目的的定律的应用，作为对一个程序的约简。法律依赖于等价的概念和公平的假设[15]。在[18]中给出了OCCAM的一组定律这里的重点不是通过消除通信来简化，而是获得范式并定义符号的语义 在[15]中给出了SPL的一些定律，其中SPL语义基于公平转换系统（FTS），但那里没有给出通信消除定律。在SVL++的框架工作中，在[7]中给出，但它们不支持通信消除。[2]中给出了第一组适合于通信消除的关系，并给出了分布式快速傅里叶变换的通信消除证明。在这部早期的著作中，等价的概念被同化为一致性，一种非常强的等价。这有一个缺点，即限制了大多数通信消除定律的制定，使其只能单向细化。显然，需要用较弱的等价来工作，在那里所有的定律都可以用它来表述，避免精炼关系的不对称，这是突出的。本文引入等价的概念，输入/输出等价，弱于同余，但强到足以保持程序的输入/输出关系，并导出通信消除律。它在语义学上是合理的，它扩展了Manna-Pnueli框架作为本文的主要贡献，其中每个语句表示一组输入/输出行为。他们扩展了[ 15 ]中给出的简化行为的概念。为了捕获完整的输入/输出关系，除了通常的数据状态变量之外，前者还向后者添加了穿越同步通道的值的记录。这反映了这样一个事实，即值可以通过通道输入或输出，以及通过适当的变量。在这种情况下，[4]中引入的流的基础工作是相关的，但在我们具体的命令式程序上下文中，我们需要一个新的模型，其中考虑到通道和变量值关于组分相容性的工作[6]也是相关的。M. Bertran等人/理论计算机科学电子笔记137（2005）2527等价推理的一个重要组成部分是两个等价过程的过程引用语句的替换.它会让证据分解。这种替代的有效性的条件也给出了其justification概述。这为分布式程序的形式化输入输出等价推理奠定了必要的理论基础。本文的结构如下。在一节的符号，包括模块化的过程，和一些概念需要在后面的文件中，输入/输出行为的概念介绍。详细介绍了顺序、并行和选择合成的IO行为合成规则，为证明替换规则的合理性做准备。接下来将介绍过程的输入/输出等价性，以及替换规则及其公正性。 这些部分包含了本文的主要贡献。 概要的法律和分布式程序简化证明如下，连同他们的应用程序的流水线处理器模型。这是一个没有证据的概述，仅用于说明目的。 本文件结尾有一个关于结论和进一步工作的简短章节。2编程符号2.1基本记程序将以SPL的简化版本编写，它足够通用，可以表达任何实际程序。现在介绍它的语法。 基本语句是Skip、Nil、Stop、赋值u：= e、sendαe和receiveαu。我们将我们的工作限制在同步通道α上，这将被称为通道。在那里，发送者和接收者都在等待。在交换一个值并继续执行之前彼此交换。通信声明将被简称为通信。skip语句涉及底层公平转换系统中的转换，但对数据变量没有任何影响。nil语句使其前后控制位置相等，不涉及转换。停止语句既没有转换也没有标签等价关系。通道和变量在使用前都是全局声明的符号的其余部分是递归定义的。连接是n元的：[S1;···; Sn]。其中，[whilecdoS]是一个布尔表达式，[loop forever doS]定义为[whiletruedoS]。该操作系统的结构都是单一的：[S1|| S n ]。||Sn]. 它的子语句Sj是合作状态的顶级并行语句这是它们的最小共同祖先。在本文中，假设Sj28M. Bertran等人/理论计算机科学电子笔记137（2005）25676737只有渠道常规选择和通信选择状态是不确定的，并且分别具有以下形式：[b1，S1or···orbn，Sn]和[b1，c1，S1or···orbn，cn，Sn]，其中bi将通信声明称为通信保护。2.2模块化程序这个概念是在[2]中结合SPL模块 [15，8]和过程的概念引入的。作为模块，模块化过程可以并行组成，但可以通过过程引用语句调用，这些语句显式显示所有接口通道和变量的名称。禁止使用通用变量。符号r：：=P（p）将用于过程引用，其中r和p代表接口的结果和参数列表，P是过程名称。模块化程序将更简单地称为程序。程序示例如下。它的过程引用位于左侧，过程主体位于右侧。2 3outr：integer6 76outcr：整数7的通道6 76external inp：integer76 76在cp中的外部：整数 7的通道6 76局部a1，a2：整数7（r，cr）：：=Pc（p，cp）：：6 76localc：channel of integer7666cp-1;663 27中国共产党第二次全国代表大会7 6 7766a1：=a 1 +p;76cr;77667 ||67 766c a1;76a2：=r+a2;7 744skip5 4 55第2章注意r和p是变量，而cr和cp是通道。r和cr是结果，p和cp是过程的参数。模式out和external in的确切含义在这里并不重要，因为进程是不相交的，通信是点对点和半双工的。在这个工作中，程序体头部的声明经常会被省略。不允许使用公共变量或通道。引用语句的语义它不随引用被过程体替换而改变，在必要时对变量和通道进行重命名它必须与在过程中封装程序的一部分的反向操作一致。一个过程的观测变量的集合O包含接口中的所有正确变量，以及接口中每个通道的辅助通道变量集合O也称为接口集合。2M. Bertran等人/理论计算机科学电子笔记137（2005）2529一个通道变量记录，作为一个三元组，在一个通信事件，一个计数反映通道事件的顺序，和一个输入/输出标记（i，o）传递的值。当事件是内部事件时，一个点代替输入/输出标记.对于上面的过程，这个集合是O：{r，p，cr，cp}，其中cr和cp是与通道相关联的辅助变量。2.3语义学的基本概念我们使用的特定SPL变体的语义遵循Manna和Pnueli的风格，基于公平转换系统（FTS）[15，16]。下文概述了其中的一些内容。[2]一个完整的账户计算是从初始状态开始的一系列状态，并将任何状态转换为其后继状态。相对于观察变量的集合O，减少的行为是一种计算，其中它的观察集合之外的变量的分量和口吃步骤（即空闲转换）删除。集合O只包含适当的变量。转换对应于与语句关联的原子程序上下文P[]是一个程序P，它的一个语句对应于一个要用任意语句S填充的洞。在某些符号滥用的情况下，P[S]将表示程序上下文，其中S表示放置在孔中的任意语句。 有些定律是陈述之间的同余关系。 报表S1对于任意一个程序C=tP[·]，我们导出了任意一个函数S2，记为S1±OSP[S1]的行为也是P[S2]的约化行为。S1与S2全等，记作S1<$OS2，当S1±OS2和S2±OS1时。这些关系是关于一组O观测变量定义的。接下来介绍了本文所需的一些扩展概念。输入/输出计算（io-计算）记录执行过程中过程体的变量和通道的值历史。每个值更改对应一行，每个变量或通道对应一列。io计算为每个通道向计算添加一列。而计算只是一个状态序列，IO计算是一个状态序列，其中跨通道的值也被记录。计算组将被表示为模式，模式具有值变量。计算只有值（整数、布尔值等）。一个三元组（值、计数、i/o指示）与通道变量的每个新值相关联下面是上述过程的io计算模式30M. Bertran等人/理论计算机科学电子笔记137（2005）25RpCRCPA1A2C0初始Xp1XTXTXXXT1中国共产党第一次全国代表大会Xp1XTcp1，1，iCP1XXT2尼泊尔共产党Xp1XTcp2，2，iCP1CP2XT3a1：= a1+ pXp1XTcp2，2，icp1 + p1CP2XT4ca 1|| c rcp1 + p1p1XTcp2，2，icp1 + p1CP2cp1 +p1，1，·5a2：=r+ a2cp1 + p1p1XTcp2，2，icp1 + p1cp1 + p1 +cp2cp1 +p1，1，·6第2章cp1 + p1p1cp1 + p1 + cp2，1，ocp2，2，icp1 + p1cp1 + p1 +cp2cp1 +p1，1，·x表示任何值，并且xT表示任何三元组。p1，cp1，cp2，等等.是值变量，而a1，a2，r和p是程序变量。cp、cr和c是辅助信道变量。给p1、cp1和cp2给定整数值，将获得特定的io计算。除了初始行，每一行都对应于第二列。行4的转换是信道c上的同步通信的联合转换。所有的计算都是无限长的。因此，最后一行对应于终端状态，通过空闲转换触发隐式地重复自身。一个计算模式可以通过删除cr，cp，c和两个左列，然后删除，如在[15]中，任何一行等于它的前任，但不是所有的继任者。3输入/输出行为3.1基本概念输入/输出行为是从外部看到的过程执行轨迹。定义3.1（过程的输入/输出行为）过程的输入/输出行为，也称为io行为，是从io计算中删除所有不属于O，然后删除任何等于其前一行但不等于其所有后继行的行。最后一次删除的条件是必要的，因为最后一行的无限隐式重复不应该被删除。由于事件计数器的原因，连续事件在其值相等时不会被删除。这应该是这样的，因为它们可以对应于过程函数的两个输入因此，所有通道事件在io行为中由至少一行表示一个io行为对于结果变量v∈ O的每个值变化都有一行。一个参数变量永远不会改变它的值，除非它也是一个结果。输入和输出通道变量显示值变化。以下为-行为模式由上述IO计算模式产生。M. Bertran等人/理论计算机科学电子笔记137（2005）2531RpCRCP0Xp1XTXT1Xp1XTcp1，1，i2Xp1XTcp2，2，i4cp1 + p1p1XTcp2，2，i6cp1 + p1p1cp1 + p1 + cp2，1，ocp2，2，i删除了第3条和第5条，因为它们分别与前两条和第4条相同。假设现在cp1 =cp 2，那么由于cp列的计数器字段的新值2定义3.2（io行为的组件）io行为组件是值列表，一个列，对应于一个变量O。但列表中任何等于其前任但不是其所有继任者的值都将被删除。有固有分量和信道变量分量。定义3.3（io-行为的等价性）当两个io-行为共享相同的接口集，并且两者的同一变量的两个分量相等时，它们是等价的。不同组件之间的值变化顺序在行为中丢失，但同一组件内的变化顺序不会丢失。等同性仅要求同源组分列表相等。3.2IO行为的合成本小节介绍了IO行为之间的操作，稍后需要对替换规则进行调整。3.2.1顺序组合顺序组合的io行为是通过将其第二语句的io行为后耦合到第一语句的以二进制组成[r1：=P1（p1）] ; [r2：=P2（p2）]，一般为O1O2，O1O2可以是空的，也可以不是空的。给定P1的模式b1，P2的模式b2依赖于最后一行的值。对应于b1和b2的P1;P2的模式b 1; 2具有与O1<$O2中的变量一样多的分量。它是通过在b1之后耦合b2而形成的。非正式地说，b2的分量在b1的分量之后，但是b2的第一行的某些值必须等于它们在b1的最后一行的同调值。更具体地，后耦合如下进行：(i) 适当的变量组件。案例：(a) v∈ O1<$O2：b2必须使得这样的v的分量的第一个位置（初始行）的值等于它们的b1的同源分量的最后一个这样的b2总是可以找到的，因为32M. Bertran等人/理论计算机科学电子笔记137（2005）25CR1RCP1p0初始XTXXTX21cp1-11XTXx3，1，iX22cr1-21x4，1，oXx3，1，iX2c护2pCP2R0初始XTXXTy21p：= v12XTy3XTy22cp2-22XTy3y4，1，iy23cr2-32y5，1，oy3y4，1，iy2当v是P2的参数时，对应的值共享相同的类型，并且当v是P2的结果时，未定义的值（x）可以改变为任何值。(b) v∈ O1<$O2和v∈ O1：b1的v个分量在（a）中选择的b2上传播到未来(c) v/∈ O1<$O2和v∈ O2：上面b2的这样的v分量的第一个值在b1上传播到过去。(ii) 通道可变组件。案例：(a) c∈ O1<$O2：b2的此类c分量的任何未定义的初始三元组被设置为等于它们的b1的同源分量的最后三元组。其余三胞胎的计数相应增加。(b) c∈ O1<$O2和c∈ O1：b1被重复到b2部分，换句话说，到未来。(c) c∈ O1<$O2和c∈ O2：这样的c分量的b1部分填充有未定义的三元组。例3.4在合成[cr1，r：=P1（cp1，p）] ; [cr2，p：=P2（cp2，r）]中，第一个结果变量r是第二个结果变量的参数，第一个p是第二个的结果相应的接口集是O1：{cr1，r，cp 1，p}和O2：{cr2，p，cp 2，r}。 没有频道共享。 此外，本发明还提供了一种方法，O1<$O2={r，p}，我们假设O：O1<$O2：{cr1，r，cp 1，p，cr 2，cp 2}。下面的模式，其中vijP1的io行为b1，P2的io行为b2，以及它们耦合后的io行为b1，b2.b1b2b1;b2CR1RCP1pc护2CP20初始XTXXTX2XTXT1cp1-11XTXx3，1，iX2XTXT2cr1-21x4，1，oXx3，1，iX2XTXT3r：= v31;初始x4，1，o（y2：=）x5x3，1，i（x：=）x2XTXT4p：= v12x4，1，oX5x3，1，iy3XTXT5cp2-22x4，1，oX5x3，1，iy3XTy4，1，i6cr2-32x4，1，oX5x3，1，iy3y5，1，oy4，1，i在b1;b2中，b2的y2变为x5，b2的x被强制为x2。M. Bertran等人/理论计算机科学电子笔记137（2005）25333.2.2并联组成并行组合的io行为是通过其组件语句的io对象的侧耦合而形成的。 在下面的平行组合中[r 1：= P1（p 1）]||[r 2：= P2（p 2）]，一般来说，O1O2和O1O2可能或可能不要空着。给定P1的模式b1和P2的模式b2，||2个P1||P2对应于ob1，b2在P：（O 1 <$O 2）− O I中有一个简单的变量，其中OI<$（O1<$O2）是组合中声明为内部不可观察的真变量和通道变量的集合。OI中的通道引起内部通信事件。 我们假设不相交性以及它们的并行组合的无死锁性。在这工作时，P的无死锁意味着内部无死锁，不考虑与P可能嵌入的任何环境的交互。生物行为B1||2，由侧耦合产生，构造如下：(i) 选择匹配的行为。由于P1和P2是不相交的，所以P1和P2的io行为b1和b2的选择是由内部通道决定的。它们的选择是为了使价值组成部分在两个三元组中，每个IO行为中的一个三元组引起每个内部通信事件是相等的。这将总是可能的，因为我们假设无死锁，这在我们的上下文中意味着P1中的任何内部通信在P2中具有匹配的通信，反之亦然。此外，在此假设下，对应也可以使三元组相等，并且其中一个具有I标记，另一个具有O标记，但不一定总是在同一侧（IO行为）。我们说这样的对应三元组是匹配的。(ii) 中间体形式b1的转换||二、(a) 它的组成部分的数量等于O1<$O2中变量的数量。(b) 它的行被其内部通信事件行分隔成子列表，首先构造如下：它们的变量分量填充有两个IO行为的匹配行的对应变量的值一个点将被放置在它的第三个组成部分，取代i和o。这假定没有死锁。(c)b1和b2的子列表的行，由通信分隔evenentrowws，areeinterleavedinb1||二、 一个陌生的人是有可能的。(iii) B1||2是通过删除f'b1的组件来构造的||2不是在P中，nd是结果的ny行，它等于它的前一个结果，但不是它的所有后继结果。例3.5考虑合成[r 1，cr 1：= S（p 1，cp 1）]||[r 2，cp 1：=A（p2，cr 1）]的两个不相交的过程，其内部通道集合OI：{cr1，cp 1}。34M. Bertran等人/理论计算机科学电子笔记137（2005）25R1p1CR1CP10初始XX2XTXT1cr1-21XX2x3，1，oXT2cp1-11XX2x3，1，ox4，1，i3r1：= v31X5X2x3，1，ox4，1，iCR1CP1R2p20初始XTXTXy21r2：= v12XTXTy3y22cr1-22y4，1，iXTy3y23cp1-32y4，1，iy5，1，oy3y2S和A的接口集是Os：{r1，cr 1，p 1，cp 1}和O：{r2，cp 1，p 2，cr 1}。假设复合的接口集是P：（OS<$O）− OI：{r1，p 1，r 2，p 2}。 以下架构对应于io-beh aviorsbsofS，baofA，anddoftheiside-coouplinggin ntermediat e f o rmébs||a.bsbab′s||aR1p1CR1CP1R2p20初始XX2XTXTXy21r2：= v12XX2XTXTy3y22cr 1 - 21|| cr 1- 22XX2（y4：=）x3，1，·XTy3y23cp 1 - 11|| cp 1- 32XX2x3，1，·（y5：=）x4，1，·y3y24r1：= v31X5X2x3，1，·x4，1，·y3y2通过通道cr1和cp1的匹配内部通信行以及内部通信事件行已被隔离。3.3选择组成对于选择复合[b1，c1;[r1：=P1（p1）]or···orbn，cn;[rn：=Pn（pn）]]，io-行为的集合是它的每个备选项Ak所贡献的io-行为的并集。每个人都贡献了[ck;[rk：=Pk（pk）]]的io行为的子集，其第一行满足布尔条件bk。设Ok是过程Pk的接口集.则备选方案Ak的接口集OAk由Ok<$var（ck）<$chan（ck）<$var（bk）给出;其中var（e）是表达式E，chan（c）的变量集合是包含信道变量fc的单例集合。上述选择的接口集合可以是任何集合P，则Pnk=1 OAk. 所有这些都与非决定论相一致。4输入/输出等效性4.1概念定义4.1（IO等价过程）两个过程P1和P2相对于它们的接口集合O是IO等价的，记为P1=OP2，当它们中任何一个的任何IO行为等价于另一个的IO行为时。IO等价比同余弱。全等过程总是等价的，但反之则不然.在io等价中，忽略了不同分量的值变化的相对顺序。因此，替换M. Bertran等人/理论计算机科学电子笔记137（2005）2535通过引用另一个过程来引用一个过程，IO-等效于第一个过程，可能会引入死锁。考虑两个程序hi（r1，r2）：：=P1（cp1，cp2）：：cp1<$r 1;cp 2<$r 2hi（r1，r2）：：=P2（cp1，cp2）：：cp2<$r 2;cp 1<$r 1具有相同的接口集合O。现在P1/P 2，因为如果P1与一个进程并行，该进程总是在通过程序中的通道cp 1操作另一个输出之前通过通道cp 2操作另一个输出，并且我们在该程序中将P1替换为P2，则引入死锁。但是，P1=OP2。4.2置换规则引用语句替换为IO等价过程是等价推理的重要步骤。三个第一引理，关于concatena-tion，合作和选择，在准备的一般规则。仅处理后连接情况，其他情况将类似地执行。引理4.2（级联中的替换）设Si [r：=A（p）]是无死锁的。然后，如果[r：=A（p）]= O[r：=B（p）]，则等价S;[r：=A（p）]= PS; [r：=B（p）]成立，其中P <$O <$OS，并且O=OA=OB根据定义，S;A和S;B的io-行为具有相同的接口集P，并且由于A和B具有相同的接口集O。关于组件列表的相等性，级联的io行为是通过将A或B的io行为后耦合到S的io行为来形成的。我们表明组件列表的相等性，回顾3.2小节中给出的后耦合构造规则。(i) 适当的变量组件。案例：(a) v∈ OS<$O：bA的这组分量的初始值（或bB）等于它们对应的bS的最后值。由于A=OB，abB（或abA）io-等价于bA（或bB），具有相同的初始值，值总是可以找到的。因此，两侧的后耦合将为这些v分量中的每一个给出相同的值列表(b) v/∈ OS <$O和v∈ OS：对于这些分量，传播到未来只取决于bS，S的io行为，它两边相等。(c) v/∈ OS<$O和v∈ O：传播到过去取决于bA或bB上，其已被选择为与（a）中的bA(ii) 通道可变组件。案例：36M. Bertran等人/理论计算机科学电子笔记137（2005）25(a) c∈ OS<$O：由于S在两边都相同，因此bS的这些分量的最后三元组在两边都相同。由于bB已经被选择为与（i-a）中的bA的初始unfined三元组，将被更改为最后的值，bS的c分量。因此，双方的io行为将是等效的。(b) c∈ OS<$O和c∈ OS：bS的最后一个三元组，必须是bA或bB区域，在两侧是相同的，因为S在两侧。因此，它们将相等地传播到bA或bB。(c) c∈ OSO和c∈ O：对于这些分量，两边的列表是通过将一个未定义值与列表连接起来而形成的。bA和bB是相等的，因为它们是IO等价的。Q我们现在研究在一个合作、平行、陈述中的替换中的等价性的保持。设S|| [r：= A（p）]具有内部通道集合I。如果O是[r：=A（p）]的接口集，OI是内部通道变量的集合，对应于I，则OI<$O。O−O I中的通道变量对应于S的外部通道||[r：= A（p）]。同样，OIOS其中OS是S的接口集。此外，OS− OI中的通道变量对应于S的外部通道||[r ： = A （ p ） ] 。 实 际 上 ， 并 行 组 合 的 接 口 集 P 是 这 样 的 ： P<$（OS<$O）− OI，因为可能存在未声明为外部的适当变量引理4.3（并行性中的替换）设S|| [r：=A（p）]是无死锁的，并且r：=A（p）与S不相交。又令[r：=A（p）]= O[r：=B（p）]，且S|| [r：=B（p）]没 有 死 锁 。然 后 ， ||[r ： =A （ p ） ]]= P[S|| [r ： =B （ p ） ]] ， 其 中 P<$（OS<$O）− OI。我们将证明，在S的io-行为的构造中，||一和S||B，可以遵循3.2小节中给出的侧耦合步骤，以便从两个语句中产生等效的io行为。无死锁这是必要的，因为它已经在建设中假设。(i) 选择匹配的行为。由于bS对于两个语句是相同的，并且A=OB，所以任何匹配bS的io行为bA都可以被等价的bB替换，它也将匹配bS。(ii) 作为一个序列，S的终止||A和B||B将相对于集合OS O是相等的。(iii) 因此，3.2.2（iii）的运算，其中P定义如上，开始于f romeither<$bS||一或从'bS||B将给出IO等效的结果。因此，S的任何IO行为||A可以被解释为S的等价的io行为||B和Vice verM. Bertran等人/理论计算机科学电子笔记137（2005）2537Q引理4.4（选择中的替换）设[g，[r：=A（p）]或R]是无死锁的，其中R代表选择语句的其余部分，g是布尔值保护，用于选择，或者布尔值和通信警卫，用于通信选择。 设[r：= A（p）]= O[r：= B（p）]，OR是R的接口集. 然后，用P（ORO）[g，[r：= A（p）]或R]= P[g，[r：= B（p）]或R]。令IR、IAg和IBg分别表示R、A和B的替代物的io-行为的集合，并且IA和IB分别是A和B的io-行为的集合如果语句是一个正则选择，则IAg和IBg分别由IA和IB的io行为形成，其第一行满足g的布尔保护。然而，如果语句是通信选择，则通过将最后一个情况的IAg的io行为后耦合到防护g中的发送或接收语句的io行为来获得IAg的每个io行为。对于I Bg也是如此。选择语句的IO行为集是它的每个备选项的IO行为集的并集。因此，IRIAg和IRIBg是l.h.s.的io行为的集合。和r.h. s，分别。因此，对于l.h.s.在R.H. S中存在等效的IO行为BR反之亦然。在io行为属于IR的情况下是这样的，因为该集合被包括在两侧中，并且相等的io行为也是io等价的在剩下的情况下，其中io行为在IAg或IBg中，真理从[r：=A（p）]=O[r：=B（p）]的事实得出，并且保护g在两侧是相同的Q下面的结果对于围绕分布式程序的过程组织证明是必要的，使得证明分解成为可能。引理4.5设P []是一个无循环的程序上下文，P [r：= A（p）]是无死锁的，r：= A（p）与P [r：= A（p）]中的所有并行子语句不相交。然后，如果[r：= A（p）]=O[r：= B（p）]，并且P [r：= B（p）]是无死锁的，则等价P[r：=B（p）]=PP[r：=A（p）] 对于任何P。这个结果由引理4.2，4.3和4.4得出。A在P[r：=A（p）]或P[r：=B（p）]中的最小祖先是一个连接、合作或选择。然后，这些祖先语句之间的等价性由三个引理之一，以及合作和连接组合的结合律得出，如下一节所述。同样的推理现在可以递归地应用于这些前向子的祖先，直到达到P[r：=A（p）]和P[r：=B（p）]Q38M. Bertran等人/理论计算机科学电子笔记137（2005）25HK我HKHK不不KKK5输入/输出等价5.1介绍本节概述了一些分布式程序的通信消除等价性证明所需的一组定律。这是必要的，以便提出一个例子io等价推理。通信消除和例子都将在后面的文章中进行概述既有适当的消除法，也有辅助法。后者虽然不能直接消除任何通信，但需要将程序转换为可以应用适当通信消除律的形式在[2]中有一些直观的辅助定律，其中许多在强公平性假设下不成立。其中一些是无; S=S，S;跳过S，S||斯基普·马里斯。 此外，连续和平行组合是关联的。 后者也是可交换的。5.2消除通信的法律注意力将仅限于其通信不在选择或迭代范围内的声明。我们将这些语句称为有界通信（BC）语句。由它们的执行产生的通信事件的数量是有限的和恒定的。以下法律允许从不列颠哥伦比亚报表中删除通信下一节还将介绍一些扩展形式的通信消除，以及无限迭代。对于每个BC状态S，我们定义一组I内部通道，其通信必须被消除。S中涉及的其余通道都是外部的，因为通过这些通道的通信语句永远不会与S中的其他通信相匹配。以下是两个直观的沟通消除定律。[α]e||αu][u：= e][Hl; α-e; T l]||[Hr; α u; T r][Hl||Hr]; u：= e;[T l||T r]其中Hl和Hr不包含I中通道上的通信子语句。如[2]所示，在一次约简中，从BC语句中消除一对匹配的通信，没有有限数量的通信消除定律。下面的等效模式2 32Hl;6 766 766 766 763Hr;77772hi3L||Hr;6K76 76 76hi76Gl|| Pl;7||6 Gr|| Pr;7=O6G|| PlK|| Pr;76kk76k k76 7 676 7 674 5 456 76 76 76 74hi5l rlk kk||Tr我不M. Bertran等人/理论计算机科学电子笔记137（2005）253900其中k= 0， 1，···，定义了一组无界的定律，当我们将其等同于lk+1rk+1] =OGk+1从那时起，语句Gl，Gr和Gk被递归地定义为k=K K1， 2，···初始条件语句Gl和Gr是αe和αu，分别 G0代表u：=e。 对于任何有限整数k都有一个定律。前两个定律是k=0，1使得某些子状态等于Nil的特殊情况。这些定律只适用于IO等价一个定律被应用为从左到右的归约，以便在单个归约中消除任何匹配的通信语句对。也要注意，在最后的定律中，有些子陈述在一边是平行的，但在另一边却不是。这种混乱可能会导致死锁。因此，必须为每项法律检查一套适当的适用条件。6申请核查6.1分布式程序简化这是一个证明程序，除其他外，适用上述法律。第一步由通信消除简化算法执行当算法成功终止时，可以保证原始语句没有死锁。由此产生的io等价形式在不相交的子语句之间具有并行性，但没有内部通信语句。以下是在消除内部通道c之后，由第2.2小节的Pc产生的过程。它具有相同的接口集。2 3[见附件1 ||[cp[2];（r，cr）：：=Pnc（p，cp）：：4 5r：=a1+p;a2：=r+a2;cr=a2Pc的每个io行为都是Pnc的io行为，反之亦然，所以Pc=OP nc。DPS的下一个步骤，并行连接转换，是carried-ried通过应用置换律转换的不相交进程的并行compo- sitions的io-等价的序列形式。得到了一个与初始程序IO-等价的顺序程序。 DPS的第三步也是最后一步是冗余变量消除。状态向量归约伴随着这最后一步。6.2非BC报表的DPS有不止一种方法可以将简化证明扩展到非BC语句，其中通信出现在无限循环中。我们将在下面的结构中详细说明：S=[S1|| S m ]，||Sm],|| G[G40M. Bertran等人/理论计算机科学电子笔记137（2005）25K其中SkBk由于它们具有通信语句并且出现在无限迭代中，因此整个语句是非BC的。假设我们将每个顶部子语句 Sk的循环展开 nk次，从而得到状态Su=[Bn1;S1|| B n m ; S m ]，当B nk||Bnm;Sm],wheretheBnk’s1百万克朗代表Bk的nk个拷贝的级联：Bk;···;Bk。我们可以将DPS部分地应用于SU，只考虑其在Bnk语句中的内部假设我们成功得到B;E，其中B没有内部通信，但结束语句E是非BC，它可能既有并行性又有内部通信。还假设B;E也被DPS减少，部分如前所述，为B;B;E。然后，作为一个结论-有限归纳的顺序， 对于任意有限整数n，S=O[Bn;E]，其中Bn是内部并行和通信自由。在第一次消除产生B;S的常见情况下，即E=S，则S=O循环永远执行B，并且右侧语句没有内部通信。在许多实际系统中，当nk= 1 ;k= 1··m时，这已经发生。6.3一个等价证明的整体结构下面的图表中显示了对类DLX [9]处理器模型的验证的简要说明，将说明报告结果的实用性IF IDEX WB证明建立了一个程序之间的IO等价性，流水线2，具有两个层次的并行性和内部通信，建模cwdWIF/IDID/EXEX/WB1cdxWdxW控制WcxwWW添加cdxA一DXAfdRS1阅读阅读注册1数据1RS1fdRS2读cdxBDXBBPC读地址寄存器2读数据2MUXcaluAwxRESa指令存储器CFDRS2写寄存器写入数据cdxRS1RS1dxRS1cxwRES寄存器Alu路RS2dxRS2wxRESbcaluBMUXrescdxRS2fdFLOW/cdxFLOWfuncfuncdxFselMuxBselMuxAcxwRDfdRD /cdxRD路路 }转发wxRD单元路CWXresWXcwdRDcwdRESRegWriteM. Bertran等人/理论计算机科学电子笔记137（2005）254126357流水线处理器，以及下面的顺序程序，2 3对于k：=1.. n是否6 7reg：：=VNCycle（reg，Vcycle）：：64ir：=0（pc）;74pc：=pc+1;5reg（ir.rd）：=alures（ir.f unc，reg（ir.rs1），reg（ir.rs2））其捕获流水线处理器软件模型的基本行为。由于这个程序是显式的，处理器解释ALU寄存器的程序只寄存指令。 指令寄存器是ir.目的寄存器和源寄存器索引分别为ir.rd、ir.rs1和ir. rs2。过程alures给出了由ir.func选择的ALU操作的结果。n是程序的长度，单位为m。并行程序有四个进程连接在管道中，模拟上述四个阶段：IF，ID，EX和WB。进程ID和EX用以下过程建模，这些过程封装了第二级并行性。（cxwW，cxwRES，cxwRD）：：=EXpar（cdxW，cdxA，cdxB，cdxRS1，cdxRS 2，cdxFS，cdxRD，cwx）：：42M. Bertran等人/理论计算机科学电子笔记137（2005）252666666666776666 473676 676 677777762677736267777667767 67722 3 3循环永久执行（ID/EX（dx）寄存器）66 2 37 766dxAdx.a;dxBdx.b;dxRS1dx.rs1;dxRS2dx.rs2;dxF dx.f unc;77666xxw.w：=dx.w;xxw.rd：=dx.rd;644cdxW dx.w;cdxAdx. a;cdxB dx.b;cdxRS1dx.rs1;cdxRS2 dx. rs2;6cdxFundamentaldx.f unc;cdxRDdx.rd;cxwWxxw.w;cxwRDxxw.rd6677777755777776||76 3 76 76循环永远做（wx寄存器）766“66cwx-10wx;#77775 76666||62wxRESa=wx.res;wxRESb=wx.res;wxRD=wx.rd777776loop forever do（转发控制）766 2 37 76 6dxRS1位1;dxRS2位2;7 7666wxRD第 二;7776466666||624selA：=（rs1 =rd）;selB：=（rs2 =rd）;557selMuxA和selA;selMuxB和selB777776循环永远做（ALU输入A）763776 766dxApaca;wxRESapacresA;selMuxApacselA;77666666||624ifselAthenaluA：=resAelsealuA：=a;557caluAaluA777776循环永远做（ALU输入B）763776 766dxBb;wxRESbresB;selMuxAselB;7766466666||624如果selBthenaluB：=resBels