形式序列化：分布式程序的等价性证明与优化

理论计算机科学电子笔记188（2007）53-75www.elsevier.com/locate/entcs通过程序重写实现分布式系统的形式序列化1米克尔·贝尔特兰2Francesc Babot 8月3日Climent4在巴塞罗那Ramon Llull大学摘要形式序列化是一种重写过程，用于减少分布式命令式程序的并行性和内部通信语句。它以隐式的方式构造等价性证明，通过应用等价律作为重写规则，从而生成一系列等价程序。用一个例子说明了可达到的各种可能的序列化程度。该方法是静态的，从而避免了状态爆炸问题，在许多情况下具有令人印象深刻的状态向量约简，并且可以作为模型简化步骤与模型检查和交互式定理证明相结合。以前接地的结果需要在正式的顺序化进行了概述，更具体地说，算法的范围内的顺序和并行组合物，消除法律的算法适用于自动消除通信，和一个合适的等价性标准的顺序化过程。 这项工作的主要贡献是扩展这些结果，包括正式消除嵌入在一个子类的选择语句，和非不相交的同步通信对同步通信。这些情况都没有在文献中处理过，他们的解决方案大大拓宽了形式序列化的应用领域。关键词：形式通信消除，形式序列化，分布式程序，并行程序，形式验证，分布式程序的法律，重写。1介绍形式化方法越来越多地被用于工业中，以建立正确性，并在系统模型中找到规律;硬件，协议，分布式算法等。特别是，模型检查[11，19，7，21，20]自动地为有限状态系统做了这件事。然而，由于状态爆炸问题，模型检查在范围上受到限制;因为它工作在定义分布式程序语义的转换系统上。这种过渡制度往往是无限的，1由CICYT在项目TIN 2006 -14738-C 02 -02下部分支持的工作，以及由General Systems Development提供的工作，www.gsystemsd.com2电 子 邮件地址：miqbe@salle.url.edu3电子邮件：fbabot@salle.url.edu4电子邮件：augc@salle.url.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.03854M. Bertran等人理论计算机科学电子笔记188（2007）53许多状态，并且与程序的大小相比总是很大，程序总是有限的。因此，大多数实际的系统描述，特别是软件的描述，并不直接适用于有限状态验证方法，因为它们具有非常大的或有限的状态空间。对于这样的系统，交互式定理证明迄今为止是唯一可行的选择。然而，它的使用需要人工计算和数学复杂性。需要新的范例和方法，将模型检查的易用性与定理证明的能力和灵活性这种混合技术已经开始出现[18，23]。具有显式并行性和通信语句的命令式语言提供了一个直观，明确和完整的框架，以表达系统模型和分布式程序。这在核查中很重要。OCCAM [12，13，14]，Manna和Pnueli [16，17]的简单编程语言SPL， SPIN模型检查器[11]的PROMELA以及[8]中的共享变量语言++，SVL++是这些命令式符号的代表上述考虑表明，静态验证方法，避免了转换系统，直接在命令式程序上工作，原则上计算复杂度较低。基于这一动机，一些静态分析方法被提出用于状态约简;例如，作为一个优先步骤，模型检验[6，15，25]。它们间接地降低了它的 复杂 性。 形式 序列 化（ Formal sequentialization ） 或分布 式程 序序 列化（Distributed program sequentialization，DPS）是一种属于这一类的形式化方法，因为它试图获得一个简化的程序等价物，在某种意义上稍后将被澄清，到原始的分布式程序，内部通信自由，变量较少。DPS在交互式等价证明器中进行，并且可以与模型检查或简化程序的交互式验证相结合作为后续步骤，从而降低整体证明复杂性。在某些情况下，只需要验证一个等价的纯顺序程序。请注意，部分降阶方法[1]适用于过渡系统，其复杂性是程序大小的指数，而DPS适用于程序，其复杂性仅是线性的内部同步通信的消除是DPS的重要步骤，因为它是一个必要的优先任务。它将法则作为还原来应用。在[22]中给出了OCCAM的一组定律在[9]中引入了通信闭分层系统，在[8]中在SVL++的框架下给出了通信闭分层系统的一些规律。其目的是通过顺序并行、迭代展开和其他转换进行形式化设计。在[16]中给出了SPL的一些定律，也涵盖了基于公平转换系统（FTS）的SPL语义。在[4]中提出了通信消除律，表明了避免强公平性的必要性。在[5]中提出并研究了适用于DPS的等效性。在这个等价中的定律的数学证明，其适用条件，以及通信消除算法的第一个版本已经在[2]中报道。流水线处理器模型的DPS等价性证明也在[5]中讨论过。在[2]中报道了用这个DPS证明得到的模型的状态向量大小的上限令人印象深刻地减少了2- 607在[3，4]中给出了其他DPS证明。M. Bertran等人理论计算机科学电子笔记188（2007）5355当要消除的同步通信在选择语句的范围内时，这些先前的结果既不适用，这种通信引入了一种新的算法，自动正式通信消除处理这些情况下，连同必要的法律，涉及选择，这是自动应用的算法。其组织如下。两个部分包括背景材料和接地结果。第一个涉及符号，相关概念，辅助定律，接口等价和有界通信语句（BCS），这是DPS首先分析的一类语句。第二章回顾了通信消除定律，并对无选择BCS通信消除算法进行了评述。接下来的一节介绍了正式的DPS证明，以及它们对一个非常典型的非BCS的扩展。与内部通信消除兼容的序列化程度的例子也包括在内。然后，接地结果的通信消除从一个子类的BCSs的选择，以及新的算法，遵循这些结果。在此基础上，本文进一步扩展到自动消除非不相交通信对和综合这两种情况的一般情况。最后一节是结论和进一步工作。2符号和基本概念2.1辅助律程序是用SPL的简化版本编写的，它足够通用，可以表达任何实际程序。基本语句是skip、nil、stop、赋值u：= e、sendαe和receiveαu。工作仅限于同步通道α，其将被称为通道。 在他们两个的发送者和接收方在交换值和继续执行之前等待对方不涉及中间消息缓冲同步通信语句将更简单地称为通信。操作状态如下：[S1|| S n ]。||Sn]. 它也可以用于并行性语句。它的子语句Sj是协作语句的顶层并行语句，协作语句是它们的最小共同祖先（LCA）。它将在整个过程中，假设Sj连接语句也是n元的：[S1;···;Sn].其中，[whilecdoS]是一个布尔表达式，[loop forever doS]定义为[whiletruedoS]。LCA声明的概念适用于concate-国家组成如合作声明中所述。 如果两个语句的LCA是一个连接语句，则它们按连接顺序排序。这与执行命令相对应。定期和通信选择声明是非-56M. Bertran等人理论计算机科学电子笔记188（2007）53636777667727673666577确定性 和 具有，分别为形式[b1，S1or···orbn，Sn]和[b1，c1;S1or···orbn，cn;Sn]，其中bi是布尔表达式，称为布尔保护，并且CI Si 语句标签，例如l：S中的l，有时既用来引用语句，也用作控制位置。为了说明符号的使用，以下过程对停止和等待通信协议2 3局部δ，η：通道消息6布尔7的局部γ 通道6 76局部ε：零的通道76 76 7666埃克塞特：：66||6hi7η_m;γ_ack77776本地d：消息76（α，ack）：：=步长（m）*6名6数据通道：：62true，δd;nil3775766666||6ηd;24或57true，ε;nil77776本地r：消息766 6接收器：664hi7真，δr; αr; γT 7777或774hi5真，ε;γF希腊字母表示通道。有三个并行连接的语句：ESCENT、DataChannel和Receiver。要发送的消息被输入到EXP中全局内存的变量m中的Step，EXP通过η并且在信道γ上等待确认。消息通过通道δ传递到接收器。通过经由类型为nil的信道发送器与接收器通信来非确定性地模拟传输错误。只有隐式同步才有效，不需要值传递这两个选项是DataChannel中的通信选择的替代选项，与Receiver中的通信选择相匹配。在通过通道α输出来自步骤的消息之后，接收器通过通道γ传递真值来向ESTO确认。在错误接收的情况下，发送假值。这个布尔值作为Step的结果存储在全局内存的变量ack中。为了封闭符号的表达，给出了一些直观的辅助定律。在[4]中，它们被证明是合理的，其中表明，当假设强公平时，它们中的许多不成立。需要这些法律来将声明转换为可以适用适当的通信消除法的形式。其中一些是同余nil; SS，S||零S，S;跳过S，S||skip你好。此外，顺序和并行组合都是关联的。后者也是可交换的。2.2界面等价适当的沟通消除定律并不适用于一致性。然而，它们在[5]中引入的一个较弱等价中保持等价4M. Bertran等人理论计算机科学电子笔记188（2007）5357在这里，它被称为接口等效。现作总结接口等价基于Manna和Pnueli的公平转换系统（FTS）语义[16，17]。在这种语义中，语句S表示具有状态和转换的FTS。计算是转换系统的状态序列，从初始状态开始，FTS的转换将该序列的任何状态带到其后继状态。计算具有与变量相关联的组件组件是由其关联变量所取的值的列表，在计算过程中，其他人的独立性。相对于一组观察变量O的简化行为是一个计算，其变量的分量在该组之外，并且其口吃步骤已经被删除。这种语义在[5]中得到了扩展，为每个外部通道向集合O添加了一个辅助变量，通道变量，以记录遍历它的值的历史。内部渠道。这些是在S中传递并行子语句的通道，被认为是对外部隐藏的。任何渠道都是外部或内部的。 扩展集合O被称为接口集合。 当S是在过程体中，内部通道不在其接口中声明，外部渠道是。内部沟通和外部沟通分别意味着S通过内部和外部渠道的沟通子陈述。扩展计算是计算概念的扩展，也考虑到所有通道变量。通常，在本书的其余部分，它将被更简单地称为计算类似地，接口行为是对应于扩展计算的简化行为的概念的扩展，扩展集O.它记录与接口的变量和通道相关联的不同变量值变化的顺序界面行为中保留了通道。然而，所需的较弱等价可以忽略这种相对顺序，仍然保留一些输入/输出关系。然后，不是比较整个行为，而是只比较行为的组成部分下面将正式说明这一点。当两个接口行为共享相同的接口集时，它们是等效的，并且对于其所有变量，两个行为的两个组件对应于相同的值列表，除了最后一个之外，其重复的值被删除因此，不同组成部分之间价值变化的相对顺序在这种等价中消失了，但同一组成部分内部的变化顺序却没有消失。这种等价性只要求同源成分表相等最后，我们定义了在整个工作中使用的等效性。定义2.1（接口等价）两个语句S1和S2对于一个接口集合O是接口等价的，记为S1=OS2，当它们中任何一个的接口行为等价于另一个的接口行为从现在在本工作中，这种等价将被更简单地称为等价。在文献中，在过程代数[24]中，在多时框架[10]等中有许多其他等价性。如果能研究一下58M. Bertran等人理论计算机科学电子笔记188（2007）53从他们的角度来看尽管如此，接口等效被引入，因为它是在Manna-Pnueli框架内保持这项工作所需的最小扩展。继续通信协议的示例，Step的接口集合将是O：{α，ack，m}。它的元素是输入和输出变量m和ack，以及输出通道变量α。DPS证明产生的等效程序如下2hi36（α，ack）：：=SimpleStep（m）：：6或true，[αm;ack：=T]774hi5true，[ack：=F]因此，步骤={α，ack，m}简单步骤。它捕捉了基本行为，从界面上看。2.3有界通信语句一个语句S被称为有界通信，如果：（a）它的所有并行子语句是不相交的，（b）任何内部通信都在迭代体之外。因此，BC语句的执行会生成有限数量的内部通信事件。S的通信前端，写作ComFront（I，S），是通信语句集合的最小元素的子集，在其级联顺序中。两个内部通信S，l和m，被称为形成匹配通信对p，如果它们是并行的，则一个是输出，另一个是相同信道上的输入。S的竞争对的集合，写为CompPairs（I，S），根据定义，是可以用ComFront（I，S）中的通信形成的匹配对p：（l，m如果两个匹配对不共享通信语句，则它们是不相交的3从无选择BCS中无选择BCS是其所有内部通信都在选择和通信选择的范围之外的BCS。对于S的任何竞争对（l，m），Gl和Gm是它们在LCA并行语句中对应的嵌入top语句.定义了top语句的标准形式递归地，对于k = 1，. 当Gx=Hx;[Gx||Px];Tx，其中Gx要么是k k−1k−1k−1k−10通信αe和αu之一，属于通信S的前面。X表示L或m。对于某个整数，通过应用辅助律，可以通过插入nil语句将Gl和Gmk=n-l或k=n-l。 Txhx的k k k k没有内部通讯。 最简单的消元法对应于[α]e||αu][u：= e]。 它被识别为[G l||G r]G0，作为基本情况。0 0对于更复杂的形式，对于任意k≥0，消元律定义为：M. Bertran等人理论计算机科学电子笔记188（2007）5359KK不不Kk+1H472 3232hlri3hHl;ihHr;i6hHk||Hki;76Gl|| Pl;7||6 G r|| Pr;7=O6G|| P l|| P r;74kk54k k56kkki5l rlk kk||Tr当这种等价物被识别为 [Glrk+1[] =OGk+1，递归定义G l，G r， 并求出了Gk。 k=k0的定律是K K递归地，将相同的等价应用于内部Gk，其代表[G l||G r]，其中k=k0，k0− 1，···，1，0。 最后的内部平行性[G l||G r]将是k k0 0替换为G0，即前面给出的基本同余式的右侧有对于每个整数k= 0， 1，···，其可以作为从左到右的简化来应用[2]给出了这一定律模式的详细证明和适用条件注释3.1（隐式并行性减少）并行性减少是应用上述定律的一个副作用。语句对（Tl，Pr），（Tl，Gr），k k k k它们的对称结构，在左边是平行的，但在右边是连接的的方面想文[2]在假定所有可能的对都是不相交的情况下，提出并研究了一种通信消除算法。它迭代地应用程序PElim，该程序应用上述递归法则来执行对的消除。当适用性条件不成立时，将返回一个带有false值的布尔结果，算法将失败终止。当PElim调用的循环没有失败地终止时，ComFront（I，S）中仍有一些通信剩余，这意味着原始程序有死锁的可能性。该证明构造算法模拟执行，其中证明中的一对匹配通信语句的消除该算法的推广分别在第5节和第6节结尾处给出的过程DisjPairsElim和CompleteComsElim内。4分布式程序序列化证明DPS是一个具有三种类型步骤的证明：（a）消除内部通信对，（b）并行连接形式变换，以及（c）冗余变量消除。通常，后两个步骤是交错的。DPS证明的第一步可以通过第3节中提到的通信消除简化算法来进行。当算法成功终止时，得到的等价形式在不相交的子语句之间具有并行性，但没有内部通信语句。4.1级联变换DPS证明继续进行进一步的步骤，并行连接变换。这是进行应用置换法转换并行不|| G60M. Bertran等人理论计算机科学电子笔记188（2007）53将不相交的过程组合成等价的序列形式。例如，由于S1和S2不相交，||S2= OS1;S2.另一类定律是针对通信闭层系统而提出的。这些系统，连同它们的定律，在[8]中进行了处理，其语义与这里使用的语义不同。但是这些定律在现在的语义学中也成立。以下是一个例子。引理4.1（通信闭层）设语句对（A1，B2）和（A2，B1）是非通信的，且[B1;A1]与[B2; A2]不相交。然后[[B1; A1]]||[B2; A2]]= O[[B1||B2]; [A1||[2]，要么双方都没有死锁，要么双方都没有死锁。唯一改变其连接顺序关系的语句是不通信的对。因此，死锁不能被引入，因为进程只能等待内部通信的发生。此外，由于假设的结果，相同的对是不相交的。这保证了行为的可变成分不会改变。因此，如2.2节所述，两侧的界面行为保持相等。QDPS证明的第三步也是最后一步是冗余变量消除。最后一步是减少状态向量.冗余变量和状态都被消除。前者通常来自于原有分布式系统的通信总线，这些总线在消除了内部通信后就不再需要了下一小节提供了一些关于变量消除的细节。4.2变量消去法和其他顺序程序法则在DPS证明的后期阶段，程序已经进行了转换到顺序形式，并且可以应用任何顺序程序证明技术。然而，为了使用相同的风格的基础上减少，连续的程序转换法律适用。例如，简单的同余，如iftruethenS1elseS2≠S1.冗余变量的消除是通过以下引理的定律来完成的，该引理可以推广到多个变量。引理4.2（变量和赋值消去）设e是一个表达式对v没有任何影响，因此v∈/O。只有S1（v）才能被接受对v的引用，S2没有对v的读引用，并且是最后一个语句在v的范围内，或者就在v的新赋值之前，相对于程序的连接顺序。然后[v：= e; S1（v）; S2]= O [第1条（e）项;第2条]在左边给v赋值对任何约化行为都没有影响，因为v不在观测集合O中，并且由于施加在S2上的条件，观测集合中的任何变量都不能在任何约化行为中改变其值。QM. Bertran等人理论计算机科学电子笔记188（2007）5361K4.3非BC报表存在许多类型的非BC语句，其中通信出现在无限循环中。我们将只在以下非常 常 见 的 结 构 中 居 中 ： S =[S1||S m ] ， 其 中 S k = 10 op forever d o B k 。||Sm] ,w her eSk=loopforeverdoBk. Bk是一种传统的状态。省略了通道声明假设我们将S的每个顶部子语句Sk的循环展开nk次，从而得到状态Su=[Bn1; S1|| B n m ; S m]||Bnm; Sm] ，当他站起来的1百万克朗对于Bk的nk个拷贝的级联：Bk;···;Bk.DPS可以部分应用于Su，仅考虑其内部通信，在B N K中的情况 报表 假设我们成功了，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。4.4序列化程度一般来说，消除内部通信语句会减少外部通信语句之间的并行性。这是从第3节的注释3.1得出的;但除此之外，也是从并行性到串联归约。这在嵌入式程序环境中引入了死锁的可能性。这将通过以下三个寄存器队列进行说明，其中设置了接口O：{cout，cin}。（cout）：：=队列（cin）：：2 23循环永远做23循环永远做2 33循环永远做6个6“#76“#76“第七十七名4R0：：4p0：c0 =m0;p1：coutm05||R1：：4q0：c1m1;q1：c0m15||R2：：4r0：cinm2;55r1：c1m2这里，三个ci通道是内部的，并且允许经由通道cin的最多三个输入，而不发生经由通道cout的任何输出。在此状态下，最多允许三个cout输出，而无需任何其他输入。允许其他程度的外部输入/输出交错这个系统的序列化等价性证明可达到的最大并行性对应于以下程序2 3p0：cin=m0;6循环永远做74h hii5q 0：coutm 0 ||r 0：cinm 1 ; p1：m0：=m 1这个系统的接口相当于原来的队列。显然，现在只允许两个连续的输入或两个连续的输出，因此减少了可能的交织的数量，从而减少了并行化的程度。最后，这里是一个可能的等价纯顺序形式，只允许一个顺序62M. Bertran等人理论计算机科学电子笔记188（2007）533524输入/输出事件。它对应于最小的并行度2 3l0：cinm0;6循环永远做76 76 76l1：cinnum1;766 7764l2：coutm0;57l3：m0：=m 15具有选择和不相交对的BCS的推广在某种意义上，选择项下的消去已经可以用迄今为止概述的工具来处理了，但这是一个非常简单的情况，如下所述注释5.1（选择下的不正确消除当匹配对的两个通信位于选择的同一备选方案内时，第3节中概述的消除算法，对于无选择BCS，可以适当地应用于备选方案以消除它。在这一点上需要一些新的概念。程序上下文P [·]是一个程序P，它的一个语句对应于一个要用任意语句填充的洞。类似地，双程序上下文P [·|·]表示一个程序，其中两个语句对应于每个要用任意语句填充的漏洞;它们都不是另一个的子语句两个语句S1和S2是全等的，记为S1<$S2，如果对任何程序条件P[·]，P[S1]和P[S2]都有一个等价的表达式.在本节中，在消元证明的任何一点上，CompPairs（I，S）被假定为不相交的，因此不共享通信。5.1单一选择嵌入BCS下面的定义指定了本工作中处理的无选择BC语句的子类。在它们中，术语基本语句包括过程引用。初始和终止基本语句的概念与它们的直观含义一起使用。定义5.2（语句的连接链）语句的连接链是它的一些基本子语句的列表，以连续的升序连接顺序，具有并行性和选择符号，其第一个元素是初始子语句或选择或并行符号;其最后一个元素是终止或退出子语句。 这两个符号中的每一个都表示其直接后继者的LCA选择或并行性声明。定义5.3（单选嵌入BC语句）当所有的级联链在任何一对内部通信之间或在起始点和第一个内部通信之间包含最多一个选择符号时，BC语句是单选嵌入BCM. Bertran等人理论计算机科学电子笔记188（2007）5363在本工作的其余部分中，仅考虑单个选择级别的BC语句然后，在选择内存在Comp对（I，S）中的对p的通信c的三个可能位置：（a）作为保护，（b）在其通信保护是外部通信ext的通信选择的备选A[c]内，以及（c）在常规选择的备选A[c通讯-c的形式为αv或αv。 第一种情况的例子是Σ Σ···α1α v1;···||· ··[b1，α1<$v2; A1or b2，α2<$v3; A2];···||· ··α2α v4···其中经由信道α1和α2的通信作为通信选择的保护。它们属于不同的对：（α1v1，α1v2）和（α2v3，α2v4）。一般来说，这种情况可以表示为S[b，c;A或R]，其中R代表选择语句的其余部分。以下是一个示例第二种情况。Σ Σ···α1α v1;···||· ··[b1，cext =2;···α1=3···或R];···||· ··在这里，该对在通道α1上。 这种情况一般可以表示为：S[b，cext;A[c]或R]。 对于第三种情况，人们有这样的陈述：Σ Σ···α1α v1;···||···[b1，···α1，v2···或R];···||···例如，具有一般形式S[b，A[c]或R]。5.2淘汰原则在消除一个通信对的连续应用的法律模式，作为证明建设算法，概述在第3节，一个可能的执行模拟。对的消除对应于执行的通信事件。 在消除证明的任何点，CompPairs（I，S）包含一个对，并且消除选择一个对，但是剩余的预编程对象S_N将剩余的对保留到该对中，以便在之后或在其他替代方案中被消除。这取决于是否或者该对中的某个通信不在选择范围内。这个完整的执行模拟原理总结在下面的引理中。引理5.4（平行对的在选择范围之外的对p∈CompPairs（I，S）的消除必须在使用语句S的剩余部分的CompPairs（I，S）中平行于P。正义化消除必须模拟执行。在这种情况下，被消除的对与其他对平行。在当前上下文中，这些对之间的任何执行顺序都将给出等效的行为，但其他对将执行后来在目前的行为，并因此，必须保存后，消除，与它在S。Q引理5.5（失能对守恒） 的 消除 的 一对64M. Bertran等人理论计算机科学电子笔记188（2007）53p∈ CompPairs（I，S），其中一个通信是一个保护，则该保护的其他组的对应在CompPairs（I，S）中定义使用语句S_p的一个选择替换R，其中p被删除.这里，在相应的执行中，其他对，其中一个通信是选择中的保护，被禁用，并且在执行或当前行为中稍后不会执行。但是，它们将以替代方案的行为为了保持这种交替执行，在其他的情况下，因此，必须在一个安全的环境中使用它，由p的消除而产生的子语句。Q5.3单一选择对应于5.1小节中提到的c的三个位置，下面引理的同余式准备了消去律，它将使引理5.5更加具体。给我5分。6（单选择一致性）LetS[·]是一个预处理变量，并且c是对p的通信，其另一通信选择与他在S[·]中合作。ThenS[b，c;A或R]→[bp（b，H），S[c;A] ]或[true，S[R]]S[b，A[c]或R] n[bp（b，H），S[A[c]或[true，S[R]]csoutsideanotherS[b，ext;A[c]或R][bp（b，H），S[ext;A[c]或[true，S[R]]当bp（b，H）未确定在S[·]中存在布尔表达式的块时，H将确定在S[b，· ··]中存在的所有相关数据的块。注释5.7（界面扩展后向传播）后向传播bp（b，H）是一个条件，不仅取决于H的界面行为的规则变量分量的第一个值，而且也取决于其外部输入通道变量分量的所有值。回想一下，H没有内在的交流因为c∈ComFront（I，S）。如[4]所述，一种方法是证明由同余符号两侧的陈述所关联或表示的转换是相同的。下面是一个不同的方法。将同余符号左侧语句的接口计算集划分为三类：包含左备择项的类、包含其余备择项R的类和不包含任何备择项的类通过构造右侧的语句，同余符号的左侧和右侧的第一个备选项的接口计算集是相同的，因为通过定义bp（b，H），在左侧位置满足b的接口计算与在右侧变量分量的第一个位置和外部输入通道的输入位置满足bp（b，H）的接口计算相同。此外，对应于R、其他备选方案以及不涉及备选方案的那些方案的接口计算的集合对于两侧也是相同的，M. Bertran等人理论计算机科学电子笔记188（2007）5365右边的语句的构造不涉及任何备选方案的计算类但是这种明显的双重性被联合操作所抑制，因为选择的行为集是它的替代行为的联合第一个关系可能看起来不是一个同余，因为右边可能在c上死锁，而左边不会，因为它的选择有其他的选择R。但这绝不是事实，因为c属于S前面的一个匹配对p。Q对p的两个通信现在在该最高优先级的选择的第一备选方案内。 然而，其他的通信可能仍然在S [ c ; A ]内的另一个选择的范围内。如果不是这种情况，则可以使用第3节的定律来完成消除，因为这样一来，可以在LCA中进行选择，并且不会生成替代执行。下面的定义和引理将其公式化。定义5.8（单一选择下的消元原理）设Elim{p，A}为从A中消去p所得到的陈述，当适用时，可将其保留。 LetS[·]是一个预存的数组元素，并且是一个数组元素的元素，其中该元素的元素是唯一的，而不是与S[·]中的元素的选择。然后，从引理5.6，直观地，defElim{p，S[b，c;AorR]}Elim{p，S[b，A[c]orR]}=Elim{p，[bp（b，H），S[c;A] ]或[true，S[R]]}def=Elim{p，[bp（b，H），S[A[c]或[true，S[R]]}defElim{p，S[b，ext，A[c]orR]}=Elim{p，[bp（b，H），S[ext;A[c]or[true，S[R]}引理5.9（单一选择下的消元法）相同的Elim {p，A}，并假设p中只有c在S [ c ;A ]内的选择范围内。然后Elim{p，S[b，c;AorR]}[bp（b，H），Elim{p，S[c;A]}]or[true，S[R]Elim{p，S[b，A[c]orR]}[bp（b，H），Elim{p，S[A[c]]}]or[true，S[R]Elim{p，S[b，ext，A[c]orR]}[bp（b，H），Elim{p，S[ext，A[c]]}]or[true，S[R]根据引理5.6，定义5.8，从选择中消除是从其每个备选项中消除的选择合成，并且p不在S[R]中。此外，引理5.5的守恒原理（适用于第一个关系）也得到了满足，因为其中一些通信必须在R中的禁用对保留在右侧的RQ设Ac是从集合中取值的变量{c; A|A [c] |ext; A [c]}，其中垂直杆|用作值分隔符。 那么引理5.6的三个定律和引理5.9的三个定律可以分别用这两个定律来表示S[b，Ac或R]=[bp（b，H），S[Ac] ]或[真，S[R] ]，以及66M. Bertran等人理论计算机科学电子笔记188（2007）53Elim{p，S[b，AcorR]}=[bp（b，H），Elim{p，S[Ac]}]或[true，S[R]。备注5.10（空选项）仅为了简化和统一所有流程中的所有流程，简化的系统结构将加速对流程中的R进行单独评估。B、A[c]或B[c ]或B [c]i是一个有效选择，Bynvention，不存在，S[b，balt]不存在，并且d[b，balt]不存在拉瓜湖当恢复时，这两个组成部分的内容和大小都是为了这些评论被简化为他们的第一个选择。5.4裁撤2名通信甄选警卫当p的另一个通信也在另一个选择的范围内时，消除通信保护的情况必须与其他情况分开处理;因为匹配的通信保护被选择为并行执行，并且它们中没有一个可以匹配另一个选择的备选方案的任何保护，因为当前CompPairs（I，S）中的所有对必须是不相交的。引理5.11（两个选择的匹配守卫的同余）设S[·|·]是一个可压缩的整数且d（c1，c2）∈Comp Pairs（I，S）. 然后S[b1，c1;A1或R1|b2，c2; A2或R2]n [bp（b1，H1）n [bp（b2，H2），S [c1; A1|c2; A2] ]或[真，S [R1|R2]]正义化正义化将沿着与引理相同的路线进行5.6 定义5.5中的守恒原理也得到了满足，因为禁用对被保留在右侧选择的另一个选择中。 不相交对的假设在这里是至关重要的，因为它排除了四个组合可能性中的两个。Q定义5.12（两种选择的警卫的淘汰原则）根据引理5.11，以下是直观的Elim{p，S [b1，c1; A1或R1|b2，c2; A2或R2]}def=Elim{p，[bp（b1，H1）]>bp（b2，H2），S [c1; A1|c2; A2] ]或[真，S [R1|R2] ]}引理5.13（两个选择的保护的消除）|·]是一个可执行的程序上下文，（c1，c2）∈CompPairs（I，S）. 然后Elim{p，S [b1，c1; A1或R1|b2，c2; A2;或R2]}n [bp（b1，H1）] n [bp（b2，H2）]，Elim{p，S [b1，c1; A1|b2，c2; A2]}]或[真，S [R1|R2]]正义化正义化将沿着与引理相同的路线进行五点九引理5.5的守恒原理也得到了满足。Q5.5从两个选择当两个通信对被淘汰是在两个选择的适当的选择，这些通信不排除的选择选择标准这仅由布尔值守卫的评估决定。在这种情况下，在Ac的茶d中，则Ac：{A[c]|ext; A[c]}将被使用。 它只有两个元素。排除内部通信保护情况M. Bertran等人理论计算机科学电子笔记188（2007）5367引理5.14（两个真选择的同余）设S[·|·]可以在不使用pbeaguard的情况下进行预处理。 TenS[b1，A<$c，1orR1|b2，A<$c，2orR2][bp（b1，H1）<$bp（b2，H2），S[A<$c，1|Ac，2]]or[bp（b1，H1），S[A<$c，1|R2]或r[bp（b2，H2），S[R1|A<$c，2]或r[t ru e，S[R1|R2]]这个证明与引理5.6的证明是一样的。然而，引理5.5不适用，因为没有禁用的通信保护。方案的选择仅取决于布尔条件，并且必须保留所有组合上可能的方案。定义5.15（从两个真选择中消去）由引理5.14，在相同的条件下，下面是直观的Elim{p，S [b1，A<$c，1orR1|b2，A<$c，2orR2]}def=Elim{p，[bp（b1，H1）]= bp（b2，H2），S [A c，1|A c，2] ]or[bp（b1，H1），S[A<$c，1|R2]]或r[bp（b2，H2），S[R1|A<$c，2]]或[t ru e，S[R1|R2]]}引理5.16（从两个真选择中消去）设S[·|·]beadoub lepramcontextandnocommun icanofpbaguard，enElim{p，S[b1，Ac，1orR1|b2，A<$c，2orR2]}<$[bp（b1，H1）<$bp（b2，H2），Elim{p，S[A<$c，1|Ac，2]}]or[bp（b1，H1），S[A<$c，1|R2]或r[bp（b2，H2），S[R1|A<$c，2]或r[t ru e，S[R1|R2]]可以像引理5.9那样进行调整，但是守恒引理5.5在这里不适用，因为没有禁用通信保护。5.6删除一个警卫和一个替代通信最后，必须考虑混合情况，此时要消除的通信对p中只有一个p的另一个通信是在一个适当的替代。在这方面，注 释 5.17 （ A 内 的 并 行 性 ） 引 理 5.9 的 A[c] 除 了 c 之 外 还 可 以 具 有 当 前ComFront（I，S）的其他通信，因为A内允许并行性。在这种情况下，在Ac，1和Ac，2的状态下，A 1和A c，2或A c，1和Ac2; A2。由于Ac，i中可能存在来自主机的其他通信选择，因此这些备选方案必须与以下通信选择的其余部分被淘汰的守卫引理5.18（对于hybrid情况的一致性）LetS[·|·] e是一个动态的分组上下文，并且p的通信中只有一个是保护。 然后S[b1，c1; A1或R1|b2，A<$c，2orR2]n [b p（b 1，H 1）] n [b p（b 2，H 2），S [c 1; A 1A <$c，2]]或r [b p（b 2，H2），S [R 1 A <$c，2]或r [tr u e，S [R1R 2]]|||这个证明与引理5.6的证明是一样的。这里，组合上可能的替代方案[bp（b1，H1），S [c1; A1|R2]]不出现在68M. Bertran等人理论计算机科学电子笔记188（2007）53因为CompPairs（I，S）中的对是不相交的。c1只和hc2和hinAc，2通信。定义5.19（混合情形的消元原理）从引理5.18，下面是直观的Elim{p，S[b1，c1; A1或R1|b2，A<$c，2orR2]}<$Elim{p，[bp（b1，H1）<$bp（b2，H2），S[c1; A1|A<$c，2]]或r[bp（b2，H2），S[R1|Ac，2]或[true，S [R1|R2]]}引理5.20（从混合情况中消除）LetS[·|·] e是一个动态的分组上下文，并且p的通信中只有一个是保护。 然后Elim{p，S[b1，c1; A1或R1|b2，A<$c，2orR2]}[bp（b1，H1）<$bp（b2，H2），Elim{p，S[c1; A1|A<$c，2]]}or[bp（b2，H2），S[R1|Ac，2]或[true，S [R1|R2]]证明可以像引理5.9那样进行。引理5.5的守恒原理适用于在R1中具有通信保护的禁用对。右边语句的第二个替换项保留这些替换对。 此外，该语句具有通常的S [R1|R2]替代。注5.21（空同余式）继