信号量实现并发全抽象：游戏语义研究

理论计算机科学电子笔记265（2010）423-436www.elsevier.com/locate/entcs不带同步原语的完全抽象安杰伊·S Murawski1牛津大学计算实验室Wolfson Building，ParksRoad，Oxford OX1 3QD，UK摘要使用博弈语义，我们证明了一个完整的抽象结果（关于可能测试前序）的理想化的Algol扩充与并行组合（IA||）.虽然大家都知道信号量可以使用共享内存实现，我们发现，信号量不扩展IA||保守地说我们解释了不匹配的原因关键词：共享变量并发，互斥，全抽象，游戏语义1引言互斥问题要求一个人找到一段代码，允许两个线程共享一个一次性资源而不发生冲突。事实证明，共享内存（具有原子读取和写入）可以用来解决它，而无需任何额外的同步原语。一个典型的解决方案包括两段代码（分别称为进入和退出协议），两个进程中的每一个都可以使用这两段代码分别进入和退出指定的关键部分相当多的试验解决方案已被证明是不正确的，在某些时候，人们已经开始怀疑这个问题是否可以解决。因此，Dijkstra [3]写了关于解决这个问题的早期尝试。他认为德克尔是第一个正确的解决方案，后来被其他几位作者简化了1由EPSRC高级研究金（EP/C539753/1）支助。1571-0661© 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.08.025424A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423彼得森/* 输入代码1 */[1]：= 1;return1;而（Q[2]和（turn=1））确实跳过;/* 退出代码1 */[1]：= 0;/* 输入代码2 */Q[2]：= 1;return2;而（Q[1]和（turn=2））确实跳过;/* 退出代码2 */[2]：= 0;两个过程的解决方案随后被推广到n个过程（Lamport虽然结果表明，从理论的角度来看，共享内存是足够的，以执行互斥，他们被认为是不满意的概念和面向实现的观点。由代码生成的交互的复杂性被认为模糊了它应该服务的目的， 这种“繁忙等待”的做法看起来很浪费。这激发了信号量的引入[3]，一种比内存读写更高级别的同步结构。在这篇文章中，我们将重点关注信号量的表达能力在设置共享变量高阶并发和上下文测试。 我们考虑Reynolds理想化代数[ 11 ]的一个变体IA，它被平行合成扩充，称为IA||并证明了所导出的上下文可能测试概念的一个不等式完全抽象结果。结果是使用游戏语义通过发现一个前序的战略，建立在一个概念，让人想起赛车计算。与各种互斥算法可能建议的相反，我们发现有对应于具有信号量的程序的策略，这些策略不对应于任何IA||- 条款更重要的是，我们可以确定一个博弈语义封闭属性所享有的所有战略对应的IA||- 术语，在信号量存在的情况下可能失败。这使得我们的模型可以应用到语义检测的“信号量的需要”。对于语境中的may-近似和may-等价，我们证明了IA||扩展信号量并不构成IA的保守扩张||.我们的结论是有关的明显的不匹配的非均匀性互斥算法的基础上共享内存。从游戏语义的角度来看，我们的研究结果表明，没有信号量的语言是相当困难的处理比一个纳入他们。因此，在语言中添加通信原语可以导致更清晰的数学结构。2理想化的藻类我们将关注Reynolds的理想Algol [ 11 ]的平行扩展A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423425类型β：：= com|exp|varθ：：= β|θ → θ特尔姆斯电子邮件：info@hotmail.中文（简体）i∈Nr，x：θx：θΓM1：comΓM2：βr =M1;M2：βΓM1：expΓM2：exprM1M2：exprM：exprN0：θrN1：θrifMthenN1elseN0：θΓM：var你好！M：expΓM：varΓN：expΓ ►M: =N:comΓ，x：varM：βM：β中的τ_nnewvarxΓM：exp→comΓN：expΓmkvar（M，N）：varΓM：θ→θJΓJ <$N：θ联系我们Γλxθ.M：θ→θJΓ，x：θ<$M：θJr，x：θ<$M：θΓμxθ.M：θFig. 1. IA的最后期限编程.理想化大陵五的特殊变体，如图1所示，此后称为IA，在文献中称为具有主动表达式的理想化大陵五[1]。本文主要研究用并行复合算子扩展的免疫算 法 ||. 它通过以下类型规则输入语法Γ M1：comΓ M2：comΓ M1||M2：com我们应该写IA||来表示扩展语言。 我们的主要目标将是达到一个完全抽象的模型，上下文近似和等价诱导IA||.特别是，我们想了解如何将信号量添加到IA中，||a选两者。为此，我们考虑另一种原型语言，称为PA，它是IA||扩展了信号量。我们在图2中给出了PA的语法。 我们假设信号量和变量被初始化为“可用” 分别为0注2.1 PA在[ 4 ]中引入。它 与Brookes的Paral- lel Algol [ 2 ]密切相关，与PA相反，它代表了强制原子性的粗粒度方法。并行Algol包含awaitMthenN构造，它将警卫M作为原子动作执行，如果警卫为真，则N在之后立即运行，也作为不可分割的操作。PA和Parallel Algol的表现力相当。显然，信号量可以使用await-then-和普通变量来实现。另一个方向的翻译也是可能的，为了考试-426A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423±►⇓±类型β：：= com|exp|var|semθ：：= β|θ → θ特尔姆斯定义IA的所有规则||加上以下几个（M）：favorite（M联系我们电子邮件：info@gmail.com联系我们M：β中的Γnewsemxr，x：semM：β联系人：李先生联系人：李先生（M，N）：sem图二. 关于PAPle，以并行Algol编码到π-演算中的风格[12]。 我们使用PA是因为我们所依赖的游戏语义更适合于细粒度并发建模，而await必须通过翻译间接解释对于一个封闭的IA-，IA||- ，PA-term M：com我们将写M i，如果存在M的终止游程（归约规则是例行的，例如可以在[ 4 ]中找到）。请注意，我们的终止概念是天使般的。因此，这里考虑的上下文近似和等价的概念将与may测试一致，并且不会考虑死锁/分歧的可能性。定义2.2设Γ ≠ M1，M2：θ为IA||- 条款我们称Γ M1：θ在上下文上近似于ΓM2：θ（记作ΓM1± IA||M2：θ），当且仅当，对任意IA||- 上下文C [−]使得<$C[Mi]：com（i=1，2），C [M1]<$蕴含C [M2]<$。此外，Γ M1：θ和Γ M2：θ在上下文上是等价的（writ.十个Γ<$M1<$=IA||M2）如果一个ch可以在文本上近似另一个。类似地，人们可以定义上下文近似（分别为）。等同）使用IA或PA的术语和上下文。 我们可以写为±IA（分别为±A=IA）或±PA（分别为± A = IA）。当提到它们时，P = P A）。例如，可以容易地看出，IA||不IA的保守扩展。例2.3两个IA-项λfexp→com→com。newvarxinf（！x）（x：=！x+ 2）λfexp→com→com。newvarxinf（！x）（x：=！x+1;x：=！x+1）是IA-等效的，但不是PA-等效的。本文的主要结果是一个明确的特点IA||（定理4.5）关于策略的前序。 这将使我们能够证明PA不是IA的保守扩张||.例2.4根据下面给出的结果，最简单的例子说明PA相对于IA的非保守性。||（根据上下文近似）A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423427||||为±±→ {} × {}∈►一一一项x和x||x，其中x是com类型的自由标识符。我们将得到x ± IA||X||x和x/± PAx||X.非正式地，x近似IA中的x x||因为C [ x ]的任何成功运行都可以紧接着C [x x]的运行，其中第二个x的每个原子动作都发生在第一个x的相应动作之后（一个继续比赛另一个）。 与此相反，在PA中，x可能会用代码实例化， 获 取 一个信号量，在这种情况下，||x不会终止（例如，C [] newsem S in（（λxcom. []）grab（S）。类似的术语表明，语境对等也没有得到保留。我们有（x或（x||x））λ=IA||（x个||x））/x = P A（x||x))/∼=PA(x||x),whereMorNstandsnewvarXin（（X：=0 ||X：= 1）; if！Xthen M else N）.3游戏语义IA和PA已经分别在[1]和[4]中使用博弈语义学进行了研究。其中提出的完整抽象结果是特别优雅的，因为它们通过（完全）播放包含来表征IA和PA 接下来，我们将回顾PA的博弈模型（最初在[ 4 ]中提出），作为我们对IA的完整抽象结果||将根据该模型中的策略进行措辞。更准确地说，我们将展示一个不同于包含的前序，它将在IA中捕获上下文近似||.导出等价关系，刻画A= IA||也不同于平面均衡。游戏语义学使用竞技场来解释类型。定义3.1AnarenaA是一个三重函数，其中• MA是一套招式;• λA：MAO，P，Q，A是确定m是否并购是 一个对手或一个支持者的移动，一个问题或一个答案;我们分别将λ A与第一个和第二个投影的合成写成λOP，λQA;A A•A是MA上的二元关系，称为使能，使得m<$An意味着λQA（m）=Q和λOP（m） λOP（n）。此外，如果n∈MA使得m/<$An对任意m ∈ MA，则λA（n）=（O，Q）.如果m我们说m使n成为可能。 我们将写IA为所有移动的集合，没有使能者的移动;这种移动称为初始移动。请注意，初始移动必须是对手问题。在用于解释基本类型的竞技场中，所有问题都是初始的，所有P-移动是通过初始移动实现的答案，如下表所示，其中m∈N。428A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423►············是我。N一1∈ 12∈ 2一一一一竞技场O型问题P答案竞技场O型问题P答案网（Ⅲ）运行做exp（Ⅲ）QMvar（Ⅲ）读写（m）M好sem（Ⅲ）抢释放okg奥克河上下文和函数类型在竞技场上的附加构造的帮助下建模：MA×B=MA+MBλA×B= [λA，λB]MAB=MA+MBλA<$B=[<$λPO，λQA<$，λB]A×B= |b ∈ IB和a ∈ IA}函数λPO：MA→ {O，P}定义为λPO（m）=O i <$λOP（m）=P。竞技场提供了所有必要的细节来指定允许的移动交换。形式上，它们将是满足一些额外性质的证明序列竞技场A中的一个正当序列是A的一个配有指针的有限移动序列。第一步棋是初始的，没有指针，但随后的每一步棋n都必须有一个指向前一步棋m的唯一指针，使得mAn。我们说n（显式地）被m证明，或者当n是一个答案时，n回答M.如果一个问题在一个合理的序列中没有答案，我们说它在那个序列中是未决的（或开放的）。 下面我们用字母q和a分别表示问题和答案移动，o和p表示O和P移动，m表示任意移动。并非所有合理的序列都将被视为有效。为了构成一个合法的游戏，一个合理的序列必须满足一个良构条件，这反映了PA中并发的用游戏术语来说：如果一个问题被回答了，那么所有被它证明的问题都必须在之前被回答过（确切地说是一次）。这在下面的定义中是精确的定义3.2A上的博弈集PA由A上的正义序列s组成，A满足以下两个条件。FORKInanyprfixsJ=q，om在m被演奏之前。对于s，问题q必须待定WAITInanyprfixsJ=q，oa回答对于s，所有由q证明的问题必须是请注意，正则化序列的交织不是正则化序列;相反，我们将称它们为正则化序列。对于两个被移位的序列s1和s2，s1s2表示s1和s2的所有交织的集合。 对于两组移位序列S1和S2，S1NS2=sS，sSs1NS2. 给定一个树序列集合X，我们定义X0= X，Xi+1=XiNX。则 定义X③，称为X的迭代shu_e，i∈NX我们说PA的子集σ是O-完全的，如果s∈σ，且so∈PA蕴涵so∈σ。定义3.3 A上的策略σ（记作σ：A）是PA的一个预闭O-完备子集。A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423429≤⇒⇒∈≤≤≤×· ··×<$θ）（Ⅲ）（）（）竞技发电机;||：=！抓取释放newvarnewsem（Ⅲ）var× <$exp）com）（Ⅲ）com× <$β）012Q 运行 做 Q a a2 0 0112com× <$com）<$com）（Ⅲ）012 2 01012运行 运行 运行 做 完成完成012运行 q m write（m） 好了2 1 10 0 2（Ⅲ）（Ⅲ）（Ⅲ）semcom）var（exp）01q读取 M m1 0 0 101运行 grab0 okgdone101semcom）01运行 释放 ok0完成R101q q（读 0）（2 10 0q2q1（grab0okg release0okr）（grab0okg+）a1a2Σi∈N（写（i） 好 （阅读 （一）（二））（三）（四）（五）0 00 01 2000策略σ：A B和τ：B C是以标准的方式组成的，通过考虑从τ开始的所有可能的策略与在共享竞技场B中的σ③的shu-eded序列的相互作用，然后隐藏B移动。对于并发程序的建模，我们考虑一类特殊的所谓饱和策略，它包含了相关（并行）交互的所有可能（顺序）观测。因此，环境的动作（O-moves）总是可以更早地观察到（一旦它们被启用），程序的动作总是可以稍后观察到（但不晚于它们证明的动作）。为了形式化这一点，对于任何区域A，我们定义PA上的预序为满足s0s1os2sos1s2和sps1s2s0s1ps2对于所有s0，s1，s2。 在上面提到的对局中，在左手边移动 在右边的是相同的正义。这两个饱和条件，在各种公式中，在并发语义学中有很长的历史[13，5，6]。定义3.4策略σ是饱和的i ∈ s ∈ σ且s ≤ SJ意味着SJ∈ σ。Arenas和饱和策略构成了一个笛卡尔闭范畴Gsat，其中Gsat（A，B）由A <$B上的饱和策略组成. 身份战略是定义为“饱和”交替策略s P A 1 <$A 2，其中P“复制”O-移动到另一个A -分量（形式上，对于s的任何偶数长度前缀t，我们有t T A 1 = t TA 2）。我们用A1和A2来区分竞技场中A的两个副本A/CN.4/2004/L.11/Rev.1）。PA-项x1：θ1，···，xn：θn<$M：θ可以在Gsat中解释为竞技场θ1。同一性策略被用来解释自由识别器。语法的其他元素通过具有设计策略的组合来解释。下面我们给出一些策略来定义它们（作为包含这些策略的最不饱和策略）。我们用下标来表示一步棋来自哪个子竞技场。变量绑定和信号量绑定的策略分别用于（var0<$β1）<$β2和（sem0<$β1）<$β2的竞技场。如[4]所示，上面概述的PA的解释产生了一个完全抽象的模型，如定理3.5所详述。如果一个剧本不包含430A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423（2）仅当，comp（r M））= comp（rM））。12∈···联系我们···≤≤（三）2¢com.）1¢）1没有答案的问题我们写comp（σ）来表示非空完备集策略σ的对策定理3.5[4]对任意PA-项Γ <$M1：θ和Γ <$M2：θ，Γ <$M1± PAM2当且仅当comp（Γ<$M1）<$comp（Γ<$M2）. 因此，如果，和，我们将证明IA的一个类似结果||，尽管所涉及的预购将要复杂得多4克隆一个蜀地戏序列是一个交叉的发挥将被称为蜀地戏。一个戏曲化的剧本，如果是完整剧本的交错，就称为完整剧本。为了在IA中捕获上下文近似，||，事实证明，一种对完整的舒剧进行的辅助操作。该操作将克隆序列的一部分，即一个选定的问题以及它所证明的所有移动。形式上，让s是一个完全的shu-化的游戏，让q是s中一个问题的发生。设m1，，mk是s中所有被q遗传证明的移动，特别地，mk是被q证明的答案。为了方便起见，我们写m0对于q，所以s = s0m0s1m1skmksk+1，其中每个si（0ik+1）是可能为空的移动序列。现在让我们定义另一个序列sq为s，其中每个mi（0≤i≤k）后面都跟着它的新副本mJi，即。sq=s0m0mJ0s1m1mJ1···skmkmJksk+1，m0和mJ0由相同的移动（从s0开始，如果有的话）调整，mJi调整mJj（i< j）当且仅当mi满足mj。我们称MJ0和MJk为锚点。直觉上，sq可以被认为是s，其中部分游戏被 注意，如果s是完全博弈，被选作初始问题，那么整个S就被克隆，SQ就成为一个完整的舒剧。定义4.1给定两个完整的剧本s，tPA，如果s包含一个问题q的出现，使得t =sq，我们就写s t。 如果我们想强调q是一个X-问题（XO，P），我们写为sXt. 接下来，我们将经常考虑上述关系的传递闭包，它们分别用y_n，y_n_O和y_p表示。例4.2（i）考虑以下两种情况网）×exp ）0.s1=r0r2r3q101d3d2d0O PO POPO Ps2=r0r2r3r3q101d3d3d2d0OPOOPOPPO P为了清楚起见，我们省略了一些要点：在两种策略中，r2，q1，d0;r2为d2;r0为d0，q1为01。 然后是s1Os2。(ii) 考虑以下两个剧本在com（）0起 在 （（com（Ⅲ）3A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423431（2）（Ⅲ）（2）（Ⅲ）s1=r0r1d1d0s2=r0r1r1d1d0注意，s1Ps2。定义4.3设σ1，σ2：A. 我们定义σ1≤σ2成立，当对任何s1∈comp（σ1）存在s2∈comp（σ2），使得s1<$Ps2.例4.4x：comx：com≤x：comx||x：com≤支持我们的完整抽象结果。本文的其余部分将致力于它的证明。定理4.5（全抽象）设Γ ∈ M1，M2：θ为IA||- 条款然后呢，M1± IA||m2当且仅当 Γ<$M1≤Γ <$M2。5可定义性首先我们建立定理4.5的从左到右的蕴涵，为此我们需要证明一个可定义性结果。 ”[4]这句话的意思是：s，可以构造PA-项，使得对应的策略是包含s的最不饱和策略。此属性不再适用于IA||- 项（这将从下一节中得出，在下一节中，我们确定了对应于IA的策略的闭包属性||- 术语）。 相反，我们将证明IA的一个弱化结果||（引理5.2）。例5.1让我们写[cond] for ifcondthen skip else Ω com.考虑从（com 2 → com 1）→ com 0的策略s=r0r1r2d2d1d0，λfcom→com。newvarXin newsemSinf（grab（S）;X：= 1）; [！X=1]，这实际上是由包含s的最小饱和策略解释的。当信号量不再可用时，为了确保assignmentX：= 1被执行一次是为了用guard [！X=0]，而不是抓（S）。但是，如果f并行运行其参数的多个副本（以便每个副本都能通过测试），这将不会阻止发生多个！在X被设置为1之前，X = 0因此，对应于λfcom→com。newvarXinf（[！X=0];X：= 1）;[！X=1]，将包含完整的游戏r0r1r2r2d2d2d1d0。事实上，战略包含所有完整的计划，是的。 这一观察结果可作如下概括。引理5.2假设Θ是IA||- 型和s∈ comp（PΘ）。 那里有一个IA||-term ms：Θ，使得OOOC++（ Ms））= {u|t ∈ P <$Θ）。（s）t且t≤u）}。让我们来描述一下Ms结构背后的一些思想。首先是值得注意的是，由于涉及饱和策略，s决定了P-移动对前面O-移动的依赖性。为了执行这个命令我们安排了O型动作432A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423∈（Ⅲ）► M）s2¢¢生成全局侧效应（Gi：= 1），使得P移动仅在对应于先前O移动的侧效应发生时才发生。上面的例子表明，单独使用共享内存，我们无法控制完整游戏中O移动的确切数量。 但是，我们可以 确保无论何时播放来自原始游戏的O移动副本，它们都是全局同步的。 为此，在将相应的标记变量Gi设置为1之前，我们安排测试[！Gi=0]。这就创造了一个“机会之窗”，比赛的O型移动，如果要达到完整的比赛，他们必须适应（迟到将无法通过测试并导致分歧）。在O型动作上同步比赛后，我们还需要确保全球层面的影响并不足以达到这个目的，因为它们只是在其中一个种族中发出必要的行动已经完成的信号为了确保与克隆子播放中的s的一致性（即，为了确保来自s的所有相关移动都被克隆），我们引入局部标记Li，除了存在是否确实已经设置Li的局部测试之外，每个局部标记Li与Gi同时被设置这一机制只适用于O型问题，因为O型答案的存在是因为最终要达到一个完整的游戏例5.3考虑θ（com4→ com3）→ com2）→ com1）→ com0和下面的策略s Pθ，其中我们抑制了从问题到答案的指针。r0r1r2r3r4d4d3d2d1d0O PO P O P O P下面的Ms项满足引理5.2。注意L4的存在如何确保在任何包含两次r出现完整博弈中，我们还必须至少有一次r4的出现是由r2遗传的。单靠G4是无法实现这一目标的.λf. newvarG0，G2，G4，G6，G8，L0in[！G0=0];G0：= 1;L0：= 1;[！n=1];newvarL2inf（λg. [啊！G2= 0]; G2：= 1; L2：= 1;[j∈{0，2}（！[inti= 1）];newvarL4ing（[！G4=0];G4：= 1;L4：= 1; [j∈{0，2，4}（！[1]）;[！L4= 1];[！G6=0];G6：= 1; [j∈{0，2，4，6}（！[1]）;[！L2= 1];[！G8=0];G8：= 1;[j∈{0，2，4，6，8}（！Gj=1）]有了可定义性结果，我们得到以下推论。推论5.4对于任何IA||- 条款M1，M2：θ，如果 ADM1± IA||M2：θ，然后是θM1：θ）≤ M2：θ）。A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423433（Ⅲ）P0∈6健全性在本节中，我们确定了一个技术属性，该属性可以通过与IA相对应的策略来满足||-条款除了帮助我们完成完整抽象结果的证明之外，它还为我们提供了一个工具，用于检查给定策略是否可能源自IA||- 任期。引理6.1设ΓM是IA||- 项，σ=Γ<$M且s∈ comp（σ）.然后，对于任何游戏t，使得s<$Ot，re存在u∈comp（σ），使得t<$Pu。直觉上，引理断言，对于环境和系统之间的每一次成功的交互，环境总是可以触发其他人，这些人紧紧跟随（竞争）原始蓝图。它的逻辑结构类似于游戏语义学文献[8，9]中用于表征无mkvar在讨论证明之前，让我们考虑一些例子。例如6.2（i）引理6.1对于用于解释信号量绑定的策略σ失败，该策略由形式q2q1（grab0ok grelease0ok r）（grab0ok g+）a1a2.000观察s=q2q1grab0okga1a2∈σ，并考虑t=g g0q2q1抓0抓0好0好0a1a2。很明显是这样。然而，请注意，tPu，其中u∈comp（σ），必须意味着t=u（唯一可能的P移动）。用于支持测试+u是q1，但σ中的策略只能包含一次发生-Q1）。t=u∈comp（σ）是不可能的，因为从σ开始的任何包含两个okg的实例必须至少包含一个释放0因此，(ii) 上述推理不适用于负责内存管理的策略τ。例如，对于s=q2q1write（3）oka1a2，t=q2q1write （3）write（3）ok ok a1a2，我们确实有t comp（τ），因为其中一个定义策略是q2q1write（3）ok write（3）ok a1a2。(iii) 很容易看出恒等式策略满足引理6.1。(iv) 与IA语法相对应的所有其他策略||满足引理，因为s∈comp（σ）且s∈0t，其中t是平面，蕴涵s=t。为了证明引理，它表面上表明，所涉及的性质是由复合保持。 自然的方法是尝试应用该属性 这两种策略交替使用，希望能为复合材料得出它。然而，鉴于目前的提法，这种交替似乎没有任何意义。结束！ 为了恢复，我们将使财产更加精确，通过将见证t_P_u的操作与完成s_p_t的相同任务的操作相关联。因此，我们要表达这样一个事实，即每个底层克隆都被嵌入到一个底层克隆中。为了使直觉更精确，让我们为在每个步骤中显示的两个颜色点分配一个新的颜色Ot（颜色将与移动保持一致，因为正在添加其他移动）。 那么我们可以说434A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423（Ⅲ）→ →<$）{}►对于在从t到u的过程中生成的每对锚点，t_P_u_c_s在s_t_t_i_s内（根据t这两个是两个相同颜色的运动。新要求的直接结果是，在搜索中涉及的锚点之间的最大距离（以将要介绍的方式计算）将严格大于锚点之间的最大距离生成的。这不一定是明显的概念的情况下，距离（移动次数），因为-steps添加移动到播放。定义6.3给定一个移动序列s，我们将s的交替长度定义为从左到右扫描序列时移动所有权改变的次数假设空序列具有交替长度0。例如，o1o2o3的（交替）长度为0，o1o2p2p3的长度为1，o1p1o2p3的长度为3。从现在开始，锚点之间的距离将被定义为它们之间的线段的交替长度（不包括点）。Givens1我们应该知道关联的weig ht是从s1到s2的转变中涉及的锚点之间的距离中的最大距离。注意，如果st，则s和t具有相同的交替长度。因此，如果t_P_u发生在s_t内，t_P_u的宽度必须严格小于s_t的宽度。“发生在内部”的另一个结果此外，由σ和τ引起的降低可以有意义地组合。因此，我们可以展示引理6.1的加强版。引理6.4设ΓM是IA||- 项，σ=Γ<$M且s∈ comp（σ）.然后，对于任何游戏t使得s<$Ot，存在u∈comp（σ）使得t<$Pu，并且t<$Pu在s <$Ot内curs。例6.5引理6.4中的闭包性质表明，例5.1中的问题是不可避免的：不可能有IA||-term1、（1）M =0，m = 0，m M）= r0r1r2d2d1d0 . 相反，PA-术语λfcom→com。newvarXin newsemSinf（grab（S）;X：= 1）;[！X=1]满足等式。因此，在PA中，信号量（事实上，即使是一次抓取）也不能被共享内存所取代，直到观测等价。例6.6test-and-set指令（test-set（X））将给定变量的值设置为1，并将旧值作为单个原子（不可中断）操作返回。 注意，如果我们将测试集（X）添 加 到IA中，||，我们可以替换λfcom→com。newvarX in newsem S in f（grab（S）; X：= 1）;[！X=1][2]在这里，我们稍微滥用了一下符号，把s_t看作是一个具体的序列的简写，它说明了s_t。A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423435推论6.7对于任何IA||- 条款M1：θ和如果<$M1：θ）≤<$M 2：θ，）与λfcom→com。newvarXinf（[test-set（X）=0]）;[！X= 1]。由于PA[4]的可定义性论证仅依赖于这种“抓取”，因此它可以延续到IA||+测试集。因此，||+测试集具有与PA相同的鉴别能力。使用引理6.4，我们最终可以通过以下方式完成定理4.5的证明：M2：θ然后 ADM1± IA||M2：θ。7结论我们构造了一个不等式完全抽象的IA模型||在一个现有的PA模型，并给出了一个明确的表征PA的上下文近似在一个完整的播放前序。我们还确定了一个闭包属性，所有IA||- 项满足而一些PA-项不满足。 因此，我们可以得出结论，信号量不能在IA中编程||如果翻译是为了保持观察等效（PA术语）。那么，为什么互斥问题的解决方案不适用呢？原因是信号量对互斥问题没有统一的解决方案。当不同的进程打算使用临界区时，它们可以运行相同的进入和退出协议（分别为grab和release相比之下，基于共享内存的现有解决方案并不统一，尽管它们通常是“对称的”，因为每个进程运行的代码仅依赖于它的识别器。例如，在彼得森算法中，两个过程的代码在交换1和2的排列之前是相同的。 这样的解决方案将不会帮助我们模拟grab（S）在例如f（grab（S））中的效应，因为f也可以使其自变量与自身并行运行，这种情况不会出现在协作顺序过程的框架中。此外，我们的结果表明PA不是IA的保守扩展||关于观测等价性（因此也是观测近似性）。下面是这种失败的最简单的例子，由于定理3.5和4.5，现在很容易验证。(i)x：com±IA|| （x个||x）：comx：comx/± PA（x||x）：com(ii)x：com（x或（x||x））λ=IA|| （x个||x）：comx：com（x或（x||（x））PA（x）||x):com436A.S. Murawski/Electronic Notes in Theoretical Computer Science 265（2010）423确认我感谢Samson Abramsky就本文的主题进行讨论引用[1] Abramsky，S.和G. McCusker，线性，共享和状态：一个完全抽象的游戏语义与积极的表达理想化的Algol，在：P。O'Hearn和R. D. Tennent，editors，Algol-likelanguages，Birkhauiser，1997pp. 297-329[2] 布鲁克斯，S。D、The essence of Parallel Algol，Information and Computation179（2002）.118-149。[3] Dijkstra ， E. W. ， 合 作 的 顺 序 过 程 ， 在 ： F 。 《 编 程 语 言 ： 北 约 高 级 研 究 所 》 （ ProgrammingLanguages：NATO Advanced Study Institute），学术出版社，1968年。43-112[4] Ghica，D. R.和A. S. Murawski，Angelic Semantics of Fine-Grained Concurrency，Annals of Pure andApplied Logic151（2-3）（2008），pp.89比114[5] Jifeng，H.，M. B. Josephs和C.A. R. Hoare，A theory of synchrony and synchrony，in：Programming Concepts and Methods，Elsevier，1990，pp.459-473.[6] Laird，J.，A game semantics of Idealized CSP，in：Proceedings of MFPS1-26，ENTCS，Vol. 45岁。[7] 兰波特湖，Dijkstra的并发编程问题的新解决方案453-455[8] McCusker ， G. ， 关 于 没 有 坏 变 量 构 造 函 数 的 理 想 化 代 数 的 语 义 。 参 见 ： Proceedings of MFPS ，Electronic Notes in Theoretical Computer Science83（2003）。[9] Murawski，A.美国，Bad variables under control，in：Proceedings of CSL，Lecture Notes in ComputerScience4646，Springer，2007 pp.558-572.[10] Peterson，G. L.，Myths about the mutual exclusion problem，Information Processing Letters12（1981），pp. 115-116[11] 雷诺兹，J.C.，大陵五的本质，在：J.W. de Bakker and J. van Vliet，editors，Muslimic Languages，North Holland，1981 pp.345-372.[12] R？ockl，C. 和D. Sangiorgi，并发标识符和语法的算术概率语义，在：Proceedings of FoSSaCS，Lecture Notes in Computer Science1578（1999），pp.306-321[13] 乌丁，J.T.，定义和分类延迟不敏感电路和系统的正式模型，分布式计算1（4）（1986），pp. 197-204.