并发程序的动态交互状态转换语义的简单证明方法及其在并行系统中的应用

22理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html19页并发程序斯蒂芬·布鲁克斯1美国匹兹堡卡内基梅隆大学计算机科学系摘要在以前的工作中，我们已经开发了一个过渡跟踪语义框架，适用于共享内存并行程序和异步通信过程，并抽象到足以支持组合推理的安全性和活性属性。我们现在使用这个框架来形式化和推广文献中使用的一些我们确定了一个顺序到并行传输定理，在适用的情况下，允许我们用另一个代码片段，这是顺序等价的，与保证整个程序的安全性和活性属性是unaerected的一块并行程序。如果两个代码片段满足相同的部分正确性和完全正确性属性，则它们被称为顺序等价的。我们还指定了粗粒度和细粒度版本的跟踪语义，假设不同程度的原子性，我们提供了一个粗到细粒度的转移定理，在适用的情况下，允许用另一个粗略等价的片段替换代码片段，即使我们假设细粒度原子性，也保证整个程序的安全性和活性属性不受影响。这两个结果允许使用一个更简单，更抽象的语义，连同语义等价的概念，这是更容易建立，以促进推理的行为，通常需要使用一个更复杂的语义模型的并行系统。1介绍众所周知，并行程序行为属性的语法导向推理往往会因组合爆炸而变得复杂1本研究部分由美国国家科学基金会（NSF）资助，资助号为CCR-9988551。本文件中包含的观点和结论是作者的观点和结论，不应被解释为代表NSF或美国的官方政策，无论是明示的还是暗示的政府的2电子邮件：brookes@cs.cmu.edu2000年1月，出版社dbyElsevierScienceB。 V. 在CC BY-NC-ND许可下开放访问。B罗克斯23这是跟踪代码片段之间的动态交互所基于状态转换语义的简单证明方法，如霍尔式逻辑，不容易适应并行设置，因为它们从交互中抽象出来，只保留计算中观察到的初始和最终状态的信息需要一个更复杂的语义模型，在其中可以给出一个准确的帐户的互动。迹语义学提供了一个数学框架，可以在其中执行这种推理[2，3，4，5]。程序的跟踪集描述了程序与其“环境”之间所有可能的交互模式我们可以定义粗粒度的跟踪语义，其中赋值和布尔表达式求值被假设为原子执行，以及细粒度的跟踪语义，其中读取和写入（共享变量）被假设为原子。跟踪语义可以在外延上定义，并且相对于程序行为的概念是完全抽象的，其中包括部分正确性，完全正确性，安全属性和活性属性[2]。在某种程度上，程序证明可以通过一些程序等价的法律来促进，通过跟踪语义来验证，这允许我们通过分析具有更简单结构的语义等价程序来推断程序的对跟踪集使用简洁紧凑的符号（基于扩展的正则表达式）也可以帮助简化程序分析。然而，问题仍然是，在一般情况下，一个程序的跟踪集可以是难以操纵的，很难使用来建立正确的属性。跟踪集往往是相当复杂的数学对象，因为跟踪集描述了程序和任何潜在环境之间所有可能的交互出于同样的原因，粗粒度和细粒度的踪迹语义都引出了一个相当有区别的语义等价概念，并且很少有从顺序设置中熟悉的等价定律因此，仅仅通过直接操纵语义定义，或者通过以语法指导的方式使用程序等价的迹论定律来建立程序的迹等价是困难的在实践中，应该仔细设计并行系统，以确保组件进程之间的交互是高度规范和约束的。此外，当分析在严格控制的上下文中运行的代码的属性时，我们应该能够在一个更简单的语义模型中工作（或者至少在跟踪语义的简化子集中），其简单性反映了这一原则。相应地，每当我们知道一个程序片段将在一个有限形式的上下文中使用时，我们希望能够采用利用这些限制的推理形式例如，我们可能知道一段代码将在并行程序中“顺序地”使用一般来说，B罗克斯24这样做，因为在顺序设置中保持的程序等效性的定律在并行语言中不再有效，因为并发执行的代码之间可能存在干扰。 然而，局部变量只能被发生在语法规定的范围内的进程访问，并且不能被并发运行的任何其他进程更改，因此我们应该能够利用这种不干涉属性来简化对仅包含局部变量的代码的推理。特别是，当局部变量只顺序使用时，在语法结构保证不超过一个进程获得并发访问的上下文中，我们应该能够使用从顺序设置中熟悉的霍尔风格的推理。我们想知道这个想法可以精确到什么程度，以及这种技术何时适用。类似地，当试图推理程序行为时，假设细粒度原子性通常被认为是现实的，但更方便的是做出不太现实但简化的粗粒度假设，因为这种假设可能有助于减少组合爆炸。我们希望能够确定这样做是安全的条件在文献中已经沿着这些路线提出了许多特别的技术它们的共同目标是通过允许用另一段代码替换代码片段来促进并发程序分析，所述另一段代码具有在本文中，我们使用跟踪理论框架来形式化和一般化这些技术。通过仔细关注潜在的语义框架，我们能够以更精确的方式重铸这些技术，并且我们可以更明确地了解其有效性所依赖的（句法和语义）由于这些技术使我们能够推断程序等价属性的基础上，一个语义模型的推理进行的不同的语义模型的顶部，我们把我们的结果作为转移原则。 我们提供了专门设计用于解决上述动机的两个示例场景的传输原则：允许使用Hoare风格推理的顺序到并行传输原则，以及管理在细粒度正确性证明中使用粗语义的粗到细传输原则。我们的工作可以被看作是对并行程序的上下文敏感开发理论的进一步进展，建立在CliJone[8]的早期工作的基础上，并受到最近Ph. D. JürgenDingel[7]的这些观点。我们首先将注意力集中在Greg Andrews关于并发编程的书中提出的一些方法论思想上稍后，我们打算更充分地探索我们的框架作为进一步推广的基础的潜力，并扩展我们的结果，以涵盖Dingel引入的一些上下文细化思想。在这篇论文的初步版本中，我们省略了底层跟踪语义的显式细节，读者可以在[2]中找到，我们省略了B罗克斯25−大多数证明，这需要详细使用语义定义。2语法2.1编程语言我们的并行编程语言由以下命令c的抽象语法描述，其中b的范围是布尔值表达式，e是整数值表达式，x是标识符，a是原子命令（赋值的有限序列），d是声明。表达式的语法是常规的，并假定包括算术和布尔运算的常用原语c：：=跳过|x：= e |c1; c2|如果b那么c1否则c2|而b做c|本地d in c|等待B然后A|c1c2d：：= x=e|d1; d2a：：=跳过|x：= e|a1; a2形式为awaitbthena的命令是一个条件原子动作，当在满足测试表达式b的状态下执行时，会导致a的执行不中断;当在b为false的状态下执行时，命令空闲。一个顺序程序就是一个不包含await和parait-constitution的命令.假定给定了free（e）和free（b）的标准定义，则表达式中的标识符集合是free的。 我们将使用free（c）和free（d）的标准定义来表示在命令或声明中自由出现的标识符集合，以及dec（d），由d声明的标识符集合。2.2并行、原子和顺序上下文上下文是可以包含适合于插入另一命令的语法“洞”（表示为[ ]）的命令。形式上，由C覆盖的（并行）上下文集由以下抽象语法描述，其中c1，c2再次覆盖命令：C：：= [−]|skip|x：= e|C; c2|c1; C|如果b那么C否则C2|如果b那么c1否则C|而B做C|本地d in C|等待B然后A|C c 2|c1℃B罗克斯26ǁǁ−请注意，我们的上下文抽象语法只允许在任何特定上下文中出现最多一个洞采用一个更一般的多孔上下文概念是很简单的，但是技术细节会变得更加复杂，而且在任何情况下都不会失去一般性。我们还介绍了原子上下文的概念，即。一种并行上下文，其漏洞出现在await命令的主体中。我们将使用A在原子上下文上进行范围。顺序上下文是一种有限形式的上下文，其中漏洞永远不会并行出现。我们可以如下描述由S排列的顺序上下文的集合S：：= [−]|skip|x：= e|S; c2|c1; S|如果b那么S否则c2|ifbthenc1elseS|while B do S|在S中的局部d|等待B然后A|c1-c2这个定义中的重要一点是，即使S是顺序的，c1S也不是顺序关键的特性是S的顺序性确保了当我们用命令填充漏洞时，我们可以保证该命令不会与S中的任何其他代码并发执行。我们把C[c]写为通过将c插入C的孔中获得的命令。我们使用类似的符号A[a]表示将原子命令a插入到原子上下文A中的结果，并且使用S[c]表示将（并行）命令c插入到顺序上下文S中的结果。定义在上下文C中自由出现的标识符的自由集（C）是很容易的，通常通过结构归纳法。 类似地，我们让free（S）和free（A）是在顺序上下文S和原子上下文A中自由出现的标识符的集合。上下文也可能具有绑定效应，因为上下文中的洞可能出现在一个或多个（嵌套）声明的范围内，并且代码片段中标识符的自由发生器可能在插入洞后变得绑定例如，上下文在（[−]y：=z+ 1）中局部y= 0绑定y，但不绑定z。另一方面，（localy= 0inc1）<$（[−];c2）不绑定任何标识符，因为hole不会出现在局部形式的子命令中。为了准确地说明这种可能性，我们作如下定义。我们还利用类似的概念，顺序上下文和原子B罗克斯27⟨⟩⟨ ⟩ → ⟨⟩⟨ ⟩ →上下文，可以用明显的类似方式来定义 虽然我们在这里不会证明这一点，但从定义可以得出（除了没有洞的退化上下文的情况）对于所有上下文C和命令c，free（C [c]）=free（C）<$（free（c）−bound（C））。定义2.1对于上下文C，设bound（C）是标识符的集合，其中有一个绑定声明包含C中的洞，定义如下：bound（[−]）=bounded（x：=e）=bound（C;c2）=bound（c1;C）=bound（C）bound（ifbthenCelsec2）=bound（ifbthenc1elseC）=bound（C）bound（whilebdoC）=bound（C）bounded（awaitbthena）=boundedbound（C<$c2）=bound（c1<$C）=bound（C）bound（localdinC）=bound（C）dec（d）3语义3.1操作语义我们假设表达式和命令有传统的粗粒度和细粒度操作语义[2]。 在这两种情况下，命令配置的形式都 是 c，s，其中c是命令，s是状态。状态s确定从标识符到变量的（有限，部分）函数，以及将变量映射到其“当前”整数值的我们让S是状态的集合。形式的转变c，s表示c执行在状态s中启用的原子步骤的结果，导致状态改变为sJ，而cJ仍待执行。一个终端配置，其中所有并行组件命令都已终止，由（最终）状态s表示。在细粒度语义中，对变量的读写不是。在粗粒度语义中，赋值和布尔表达式是原子的。命令c的计算是一个以终端配置结束的有限转换序列，或者是一个对c的所有并行组件命令公平的有限转换序列。（当我们需要精确地确定哪个粒度假设是相关的时，我们也可以指细粒度计算我们写c，s<$cJ，sJ表示一个有限的，可能是空的转换序列;以及c，sω到一个人，从一开始，就有一个（弱）公平的无限计算B罗克斯28给定配置。交互式计算是一个有限或无限的转换序列，其中状态可以在步骤之间改变，表示并行执行的其他命令的结果。交互式计算也有类似的公平性概念。计算只是一个无干扰的交互式计算，即没有外部变化发生的交互式计算。3.2状态转换语义和顺序等价定义3.1程序的标准状态转换语义，记为M，在操作上的特征在于：M（c）={（s，sJ）|c，s ∪ {（s，s）}| εc，sε →ω}。定义3.2两个程序c1和c2是顺序等价的，c1<$Mc2，当且仅当M（c1）=M（c2）。众所周知，顺序等价是相对于我们的编程语言的顺序子集的一致性事实上，对于所有并行程序c1和c2，以及所有顺序上下文S，c1Mc2惠S[c1]MS[c2]。然而，类似的性质不适用于并行上下文，因为，例如，我们有：但x：=x+2Mx：=x+ 1;x：=x+1x：=x+2y：=x/M（x：=x+1;x：=x+1）y：=x.3.3踪迹语义一个程序c的转换轨迹是一个有限的或无限序列的步骤，每个步骤是一对状态，代表程序执行的有限序列的原子动作的 特定跟踪（s0，sJ0）（s1，sJ1）. . . （sn，snJ）. . . C表示C的一个可能的非交互式计算，其中假设步骤间状态改变（从S_0到S_1，等等）是由与C并发执行的进程引起的。 迹线“complete”, representing an entire interactive computation, rather than “par-如果状态在沿着轨迹的连续步骤之间从不改变，则轨迹是无干扰的，即，在上面使用的符号中，当W具有SIi=Sii+1对于所有i时。无干扰跟踪表示在无干扰公平计算期间所获取的状态的快照序列我们再次得到了粗粒度的迹概念，基于对原子性的粗解释和粗粒度的操作语义，以及细粒度的迹概念，基于对原子性的细解释和细粒度的操作语义。粗粒度和细粒度痕迹B罗克斯29不不不××语义将条件原子动作awaitbthena解释为原子动作。粗粒度的跟踪语义（我们将其表示为coarse）也假设赋值和布尔表达式计算是原子的。细粒度语义（表示为fine）仅假设对简单变量的读取和写入在本文的其余部分，当陈述一个对细粒度和粗粒度语义都成立的结果时，我们可以使用来代表任一版本的跟踪语义函数。迹的语义可以在组成上定义，我们特别注意到，c1的迹和c2的迹是通过形成c1的迹和c2的迹的公平合并而获得的，而c1;c2的迹是通过连接c1的迹和c2的迹而获得的，根据需要在口吃和口吃下关闭c中局部x=e的迹线不会改变x的值（全局版本），并且通过从c的迹线投影获得，其中x的值（局部版本）一个并行程序表示一个在两个自然条件下封闭的迹集，这两个自然条件被称为stuttering和stupper，它们对应于我们使用一个步骤来表示有限的动作序列：形式为（s，s）的空闲或stuttering步骤可以插入迹中，并且每当两个相邻的步骤（s，sJ）（sJ，sJJ）共享相同的中间状态时，它们可以被组合以产生一个包含步骤（s，sJJ）的模糊闭包属性确保跟踪语义对于行为的概念是完全抽象的，假设我们可以在执行过程中观察状态。因此，踪迹语义支持关于安全性和活性性质的组合推理。安全属性通常断言，当进程从满足某些先决条件的初始状态无干扰地执行时，不会活性属性通常断言某些“好”状态最终会出现。当两个进程具有相同的迹集时，在所有并行上下文中，它们满足相同的安全性和活性属性集3.4细粒度和粗粒度语义等价当使用粗粒度语义时，可以安全地使用算术的代数定律来简化关于程序行为的推理。例如，在粗粒度跟踪语义中，赋值x：=x+x和x：=2x是等价的。这一特性在程序分析中有很大的优势。然而，粗粒度通常是一个不切实际的假设，因为并行编程语言的实现通常不能保证赋值确实是不可分割地执行的。细粒度的跟踪语义在实践中更接近传统的实现，但在程序分析中不太方便。当使用细粒度语义时，不能假设表达式等价的代数定律仍然有效。例如，赋值x：=x+x和x：=2x在细粒度跟踪语义中是不等价的;这反映了以下事实：B罗克斯30不MT≡≡前者读取x两次，因此如果x在执行期间改变（例如从0到1），则赋值可能是0、 1或2，而后者赋值（在相同的情况下）将赋值0或2。从上面的讨论中可以清楚地看到，即使没有看到所有的语义定义，尽管我们使用“细”与“粗”所暗示的含义让我们写c1粗c 2 惠T粗（c1）=T粗（c 2）c1精细c2 优惠T罚款（c1）=T罚款（c2）例如，我们已经看到了一对程序，它们在粗粒度语义上是等价的，但在细粒度语义上不是：x：=x+x× ×粗x：=2×x，x：=x+x/×细x：=2×x，所以c1→coarsec2并不总是意味着c1→finec2。逆蕴涵也失败了，如程序x：=x+x和在（y：= x;z：=x;x：=y+z）中局部y=0;z= 0这些在细粒度语义上是等价的，但在粗粒度语义上不是。尽管细粒度等价和粗粒度等价是不可比的，但对于任何特定的程序c，粗粒度迹集将是其细粒度迹的子集：T粗（c）T细（c），因此将粗粒度语义称为“更简单”是合理的我们还注意到，状态转换语义的并行亲，gram由它的迹语义决定，实际上是由它的无干扰迹决定，因为（s，sJ）∈ M（c）当且仅当（s，sJ）∈ Tfine（c），并且（s，sj）∈ M（c）当且仅当fine（c）中从状态s开始存在无限无干扰迹。(Here我们采用通常的双关语，将（s，SJ）同时看作属于（c）的一对和属于（c）的长度为1的迹这样的迹线是平凡无干扰的。）每个迹等价是整个并行语言的一个同余，因此对于所有上下文C和并行命令c1和c2，我们有：c1粗的c 2惠C[c 1]粗的C[c 2]c1细的ec2惠C[c1]细的eC[c2]此外，C1精细c2暗示c1Mc2，但其逆蕴涵不是一般有效。4读取和写入命令为了给我们的转移原理打好基础，我们首先需要为每个并行程序c定义标识符出现的多集读（c），B罗克斯31−∩在C的非原子子表达式中显示为自由。这里至关重要的是，正如术语所暗示的那样，跟踪程序对每个标识符进行了多少引用我们只需要关注非原子子短语，因为只有这些子短语的执行可能会受到并发活动的影响我们还需要参考表达式和声明的类似概念;由于我们没有提供表达式的完整语法，我们将只给出几个关键情况的细节，这些情况有助于理解下面所有的例子，这些例子传达了一般的思想。为了精确的数学目的，我们可以把多重集看作是一组具有非负多重数的标识符在空多重集中，每个标识符的重数为0。当M1和M2是多重集时，将M1+M2设为增加了倍数的倍数单位，M1maxM2是多集联合，其中多重性使用max组合。 也就是说，在M1中出现n1次和在M2中出现n2次的标识符x将在M1中计算n1+n2次s，并且在M1中计算maxx（n1，n2）次s。我们写{|X|}的单例多重集，X. 我们还写了||}为空的多重集。多重集M的基数被表示|M|.union的每个版本都是对称和关联的：M1+M2=M2+M1M1+（M2+M3）=（M1+M2）+M3M1最大值M 2=M 2最大值M 1M1最大值（M 2最大值M 3）=（M 1最大值M 2）最大值M 3此外，Rmax是幂等的：M最大值M=MObviouslyprone+is not idempointnt.空多重集是两种并集形式的单位，因为M+{||}=Mmax{||}=M.给定一个多重集M和一个标识符集X，我们定义MX为从M中删除所有标识符在X中出现的多重集，我们让MX为由M中也在X中的那些成员组成的多重集，这些成员具有与它们在M中相同的多重性。我们现在准备好定义表达式的读多集这里我们只列举了几个有代表性的案例。请注意，我们将对形式为e1+e2的表达式使用多集并的加法形式（一般来说，也适用B罗克斯32∈定义4.1表达式e中的自由标识符出现的多集读数（e）归纳为：reads（n）={||}reads（x）={|X|}reads（e1+e2）=reads（e1）+reads（e2）对于布尔表达式可以给出类似的定义定义4.2在一个decd中，自由标识符出现的多集读数（d）归纳地由下式给出：reads（x=e）=reads（e）reads（d1;d2）=reads（d1）max（reads（d2）−dec（d1））在这里，我们结合使用最大值，因为d可能需要单独评估几个子表达式。现在我们可以定义命令了：定义4.3由命令c读取的自由标识符出现的多集读取（c）由下式归纳给出reads（skip）={||}reads（x：=e）=reads（e）reads（c1;c2）=reads（c1c2）=reads（c1）maxreads（c2）reads（ifbthenc1elsec2）=reads（b）reads（b）reads（whilebdoc）=reads（b）reads（c）reads（creads（await b then a）={||}reads（localdinc）=reads（d）max（reads（c）−dec（d））我们再次使用最大形成联合操作来组合来自所有子表达式计算的计数。请注意，我们认为await命令没有读操作，因为它将以原子方式执行，因此其结果将不受并发干扰。接下来，我们定义在c中自由出现的标识符出现的集合writes（c）作为赋值的目标。事实证明，我们并不需要精确计算一个标识符被分配了多少次，只需要知道每个标识符是否被分配：即使一次也足够糟糕。我们的定义确保x写（c），当且仅当在形式为x：=e的子命令中，x在c中至少有一次自由出现。定义4.4（c）作为目标自由出现的标识符B罗克斯33C中的赋值由下式给出writes（skip）=0writes（x：=e）={x}writes（c1;c2）=writes（c1c2）=writes（c1）writes（c2）writes（ifbthenc1elsec2）=writes（c1）writes（c2）writes（whilebdoc）=writes（c）writes（awaitbthena）=writes（a）writes（localdinc）=writes（c）-dec（d）5上下文的并发读写接下来，我们为每个并行上下文C定义crw（C）=（R，W）对，其中R是在与C的洞并发的求值上下文中自由出现的标识符的集合，W是在与洞并发的分配上下文中自由出现的标识符的集合通常，这个定义是归纳的。这里使用集合而不是多集合，因为对我们目前的目的来说，重要的定义5.1上下文C的并发读写由下式给出crw（[−]）=crw（skip）=crw（x：=e）=（，）crw（C;c2）=crw（c1;C）=crw（C）crw（ifbthenc1elseC）=crw（ifbthenCelsec2）=crw（C）crw （ whilebdoC ） =crw（C）crw（awaitbthena）=（a，b）crw（localdinC）=crw（C）crw（cC）=crw（Cc）=（Rreads（c），Wwrites（c）），其中（R，W）=crw（C）注意，C语言中的local d子句可能会在并发读写中包含一些由d声明的标识符;当代码插入到上下文中时，这些标识符的出现变得绑定，但我们仍然需要知道代码是否以及如何并发使用这些标识符。B罗克斯34≡∪⊆6转让原则我们现在陈述一些基本的跟踪语义性质，这些性质形式化了并行程序的行为仅取决于其自由标识符的值的意义。我们说两个状态s和SJ在集合X上一致如果每个人都有自己的身份证，那就说明他们都有自己的身份。相同的整数值。这些属性在并行设置中类似于从顺序设置中熟悉的 他们的证明是基于迹语义定义的直接结构归纳。定理6.1设α是c的迹，（s，SJ）是α的步. 则s与sJ在所有不在writes（c）中的标识符上一致。✷定理6.2设（s0，SJ0）（s1，SJ1）. （s n，sJn）. 是C的一种痕迹。 那么对于每个状态序列t0，t1，.，tn，. 使得对于所有i ≥ 0，t i与X {\displaystylex}上的s i一致，有迹（t0，TJ0）（t1，TJ1）. （t n，tJn）.使得对所有i ≥ 0，tJi与X上的t i一致，则（c）为。✷在建立了相关的背景定义和这个关键一致引理之后，我们现在可以提出我们一直在引导的转移原则。6.1一种原子上下文的转移原理第一个几乎太明显了，以至于不能包括在内：它表面上对语法原子上下文中使用的任何代码这适用在粗粒度和细粒度语义中，因此我们将使用T来代表任何形式的迹等价。Theorem6. 3如果A是一个原子整数，并且a1≠Ma2，则A[a1]≠TA[a2]。证据awaitb然后a的迹仅取决于a的在表示不间断的完全执行的迹上;并且（s，sJ）是ai ∈（s，sJ）∈ M（a）的原子迹。✷6.2顺序传输原理下一个转移原则确定了代码片段的顺序等价可以安全地依赖于建立并行程序的跟踪等价的条件。定理6.4如果free（c1）free（c2）bound（C），并且（R，W）= crw（C），并且然后|+的|writes（c i）R |=0，i = 1，2|= 0, i = 1, 2c1<$Mc2<$C[c1]<$TC[c2]。✷B罗克斯35联系我们T T T值得注意的是，这个定理中的附带条件是必不可少的。如果我们省略上下文周围的局部声明，结果将无效，因为c1和c2顺序等价的假设不足以暗示c1和c2是跟踪等价的。 如果我们试图在一个上下文中使用这些代码片段，它与之进行非平凡的交互，结果又失败了：当c1和c2顺序等价时，它不遵循这一点局部d在（c∈c1）中和局部d在（c∈c2）中对于所有c都是迹等价的，即使d声明了c1和c2的所有自由标识符。一个具体的反例是通过考虑命令c1：x：=x+1;x：=x− 1c2：x：=x我们有reads（c i）={|X|}，写出（c i）={x}。 设C为上下文localx = 0 in（（[−]x：=2）; y：= x）.则bound（C）=x和crw（C）=（，x）。使用定理的符号，我们有|=1，|writes（c i）R|=零|= 0这样就违背了假设。 很容易看出c1≠Mc2，C[c1]Ty：=0ory：=1ory：=2C[c2]Ty：=0ory：=2S = C[c1]/S=C[c2]。3另一个例子表明，另一半的假设不能放松。考虑设C为上下文c1：x：=1;whiletruedo skipc2：x：=2;while true do skiplocalx = 0 in（[−]y：= x）.则绑定（C）={x}，空闲（c i）=写入（c i）={x}，读取（c i）={||}。此外，c1<$Mc2，因为M（c i）={（s，n）}|s ∈ S}（i = 1，2）. 我们有|=0，|writes（c i）R |=1，因此假设再次被违反。|= 1 so that the assumption is violated again.同时我们也有C[c1]T（y：=0orry：=1）;whiletrueoskipC[c2]T（y：=0orry：=2）;whiletrueeoskip3虽然我们的编程语言没有包含非确定性选择操作符c1或 c2，但在这里使用它是很方便的，可以指定一个行为像c1或c2 的命令;就跟踪集而言，我们有（c1或 c2）=（c1）（c2），一个类似的方程， 在粗粒度和细粒度版本中。B罗克斯36∪⊆≡≡S = C[c1]/S=C[c2]。上述定理在上下文是顺序的特殊情况下总是适用的因此，我们声明如下：推论6.5如果S是序列上下文，且free（c1）free（c2）bound（S），则c1<$Mc2<$S[c1]<$TS[c2]。证据 当S是序贯的时，我们可以通过对S，则crw（S）=（n，n）。✷为了说明这些结果的好处，请注意，许多简单的顺序等价定律是众所周知的，并且在推理顺序程序时往往被认为是理所当然的。特别要注意以下的de Bakkerx：=xMskipx：=e1;x：=e2<$Mx：=[e1/x]e2x1：=e1;x2：=e2<$Mx2：=e2;x1：=e1，如果x1/∈free（e2）x2/∈free（e1）x1/=x2这些法律在平行的环境中不成立，被精细或粗糙取代。我们的研究结果表明，这些法律在多大程度上在对并行程序的安全性和活性性质进行推理时，可以安全地使用该方法，指出了对关键代码片段的顺序分析足以确保并行程序正确性的6.3一种由粗到细的转换原理最后，我们现在考虑必须满足什么要求，才能安全地使用粗粒度的基于迹的推理来建立细粒度的等价。这可能是有益的，如前所述，因为对于给定的代码片段，粗粒度跟踪集形成细粒度跟踪集的（通常是真的）子集这对于可以并发执行的代码尤其重要，因为它可以帮助最小化组合分析。事实上，Andrews [1]提供了一系列协议的例子，其中并行编程问题（例如互斥）的“细粒度”解决方案是通过语法转换从“粗粒度”解决方案中导出的所有这些例子的共同点是，当试图在细粒度设置中建立正确性时，都希望诉诸粗粒度推理我们从一个所谓的“最多一次”属性开始B罗克斯37∪⊆≡排除协议设计。安德鲁斯的相关定义，适用于我们的环境，如下所示：• 一个表达式b（或e）具有at-most-once属性，如果它引用了最多一个标识符，而这个标识符在表达式被求值时可能被另一个进程改变，并且它引用这个标识符最多一次。• 一个赋值x：=e具有at-most-once属性，如果e具有at-most-once属性并且x不被另一个进程读取，或者如果e不引用任何可能被另一个进程改变的标识符。• 一个命令c具有at-most-once属性，如果在c中非原子地发生的每个赋值和布尔测试都具有at-most-once属性。如果一个事件在awaitbthena形式的子命令中，则它是原子的。安德鲁斯most-once属性，则在推理其行为时，它可能会假设粗粒度执行，因为与细粒度执行没有明显的区别然而，上面对最多一次属性的描述只是非正式的，并且稍微不精确，特别是在依赖于对代码将被执行的上下文的隐式分析时。我们将基于对该属性的精确重新表述，以稍微更具体但更一般的术语来表达我们的传递原理以上定理6.6 如果free（c1）free（c2） bound（C），并且（R，W）=crw（C），并且然后要么|改为（c i）|=零或|改为（c i）|= 1&个|写（c i）（RW）|= 0，i = 1，2c1coarsec2C[c1] fineC[c2].✷因此，我们的最多一次属性的正式版本可以被理解为要求该命令最多读取上下文并发写入的标识符的一个实例，如果它读取一个标识符，那么它的写入都不影响上下文并发读取或写入的任何标识符我们坚持上述定理，即被分析的代码（c1和c2）只考虑局部变量，即标识符，当代码被插入到上下文中时，标识符被绑定，在安德鲁斯的设置中通过假设所有进程都有本地寄存器来反映我们再次表明，内置的provisos强加的局部性和至少一次属性不能被丢弃。首先，对于上下文[-]，每个程序都有最多一次属性。但是，假设c1大于粗c2不足以确保c1小于细c2。因此，如果我们忽略上下文周围的本地化，结果将变得无效。B罗克斯38×为了说明最多一次假设的必要性，让程序c1和c2分别为y：=x+x和y：=2x。这些程序显然是粗略等价的。设C为上下文localx = 0; y = 0 in（（[−]x：=1）; z：= y）.当然，c1两次引用x，它同时被上下文赋值c1不满足C的至多一次性质。此外，我们可以看到，在（（y：=x+x<$x：=1）;z：=y）中局部x= 0;y=0精细z：=0或z：=1或z：=2局部x=0;y= 0in（（y：=2×x<$x：=1）;z：=y）局部z：=0orz：=2S = C[c1]/S=C[c2]。还要注意的是，假设失败的另一种方式是当c1（比如说）对并发访问的标识符进行读写时例如，设c1为x：=x，c2为await true，则x：=x。设C为上下文localx= 0in（（[−]x：=1）;y：=x）然后我们有|改为（c i）|= 1和|写（c i）（RW）|> 0。 和c1-coarsec2. ButC[c1]定义y：=0或y：=1，且C[c2]定义y：=1。同样值得注意的是，上述原理不能通过用c1和c2顺序等价的较弱假设来代替c1和c2粗略等价的假设来加强。例如，设c1和c2为和y：=1;whiletruedo skipy：=2; while true do skip.设C是（[−]z：=y）中的上下文局部y= 0然后我们有reads（ci）={y}，writes（ci）={ y }，crw（C）=（{y}，{z}），bound（C）={y}。此外，c1<$Mc2成立，因为M（c i）={（s，n）}|s∈S}，i = 1，2. 然而，在这方面，C[c1]双烯酮e（z：=0或z：=1）和C[c2]双烯（z：=0或z：=2），S = C[c1]/S=C[c2]。上面给出的粗粒度到细粒度的转移定理推广了安德鲁斯书中基于出现计数的一些更特别的为了使与安德鲁斯的例子更精确的连接，请注意我们定理的以下特殊情况，这些情况出现在安德鲁斯的释义中：• 如果b最多引用一次并发写入的标识符（通过上下文），则awaitbthenskip可以替换为while<$bdo skip（贯穿始终B罗克斯39的方案）。此规则可用于证明用（非原子）忙等待循环替换条件原子操作的合理性。• 如果x：=e具有at-most-once属性（对于上下文），则赋值x：=e可以被其原子版本await true thenx：=e替换（贯穿整个程序）。这条规则可以用来简化关于过程之间相互作用的可能性的推理。7结论和今后的工作我们已经确定了一些条件，在这些条件下，对代码片段采用“顺序”推理是安全的，同时试图建立“并行”正确性属性，我们还确定了在证明细粒度属性时安全使用粗粒度推理的条件。这些传输原则可以被看作是安德鲁斯协议分析背后的一些想法提供了语义我们计划扩展我们的想法和结果，以涵盖更广泛的例子，包括丁格尔讨论的一些协议探索我们的方法和丁格尔的上下文敏感近似概念之间的关系也很有趣这些结果允许使用一个更简单，更抽象的语义，连同语义等价的概念，这是更容易建立，以促进推理的行为的并行系统。研究转移原理在提高有限状态并发系统的模型检验效率方面的可能效用将是有趣的8确认匿名推荐人提出了一些有益的建议。作者比他以前的博士更喜欢他。研究生，JürgenDingel，他的论文研究为这里报道的工作提供了动力。引用[1] 安 德 鲁 斯 ， G. ， “Concurrent Programming: Principles and Practice,”Benjamin/Cummings[2] Brookes，S.，共享变量并行语言的完全抽象信息和计算，127（2），145[3] Brookes，S.，平行大陵五的精髓Proc.11th IEEE Symposium on Logic inComputer Science，IEEE Computer Society Press，164出现在信息与计算中。B罗克斯40[4] Brookes，S.，理想化CSP：将过程与通信过程相结合。《程序设计语义学的数学基础》，第13届会议，1997年3月，《理论计算机科学电子笔记》6，爱思唯尔科学（1997）.网址：http://www.elsevier.nl/locate/entcs/volume6.html。[5] Brookes，S.，并行进程通信。在：计算机科学，牛津-微软研讨会在荣誉教授安东尼·霍尔爵士，由吉姆·戴维斯，比尔·罗斯科和吉姆·伍德科克编辑，帕尔格雷夫出版社（2000年）。[6] de Bakker，J.，简单赋值语句的公理系统。在由E.恩格尔Springer-VerlagLNCS 181，1[7] Dingel，J.，“系统并行程序设计”博士学位。论文，卡内基梅隆大学，计算机科学系（2000年5月）。[8] 琼 斯 角 ， 澳 - 地 B 、 对 干 扰 程 序 的 开 发 方 法 的 尝 试 性 步 骤 ， ACMTransactions on Programming Languages and Systems 5（4）：576[9] Park，D.，关于公平并行的语义。在D. Bjørner，Springer-Verlag LNCS86，504-526（1979）.[10] Park，D.，“Concurrency and Automata on Infinite Sequences,” Springer104（1981）。