没有合适的资源?快使用搜索试试~ 我知道了~
并发模块的规范步骤及验证技术
可在www.sciencedirect.com在线获取理论计算机科学电子笔记319(2015)3-18www.elsevier.com/locate/entcs并发模块的模块化规范步骤(特邀论文)Pedro da Rocha Pintob,1,3 Thomas Dinsdale-Younga,2,4Philippa Gardnerb,1,5奥胡斯大学计算机科学系丹麦奥胡斯英国伦敦帝国理工学院计算机系摘要并发程序模块的指定是一个困难的问题。 规范必须足够强大,以便能够在不引用底层模块实现的情况下推理预期的客户端。我们调查了一系列用于指定并发模块的验证技术,特别强调了四个关键概念:辅助状态,干扰抽象,资源所有权和原子性。 我们将展示这些概念如何结合起来,提供强大的方法来指定并发模块。保留字:并发性,规范,程序验证。1引言并发程序模块的指定是一个困难的问题。当并发线程处理共享数据时,产生的行为可能很复杂。因此,这种模块的规范需要有效的抽象来描述这种复杂的行为。自1970年代以来取得的进展是巨大的在本文中,我们描述了一些关键概念,1这项研究得到了EPSRC计划赠款EP/H 008373/1和EP/K 008528/1的部分支持2这项研究得到了丹麦自然科学独立研究委员会(FNU)ModuRes Sapere Aude Advanced Grant的部分支持。3电子邮件:pmd09@doc.ic.ac.uk4电子邮件:tyoung@cs.au.dk5电子邮件:pg@doc.ic.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2015.12.0021571-0661/Crown Copyright © 2015由Elsevier B. V.出版这是CC BY许可下的开放获取文章(http://creativecommons.org/licenses/by/4.0/)。4P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3在过去的几十年里出现了。我们将我们的论述限制在我们发现最重要的概念上:辅助状态,干扰抽象,资源所有权和原子性。我们使用计数器模块来强调指定并发模块的挑战。我们需要一个规范,它要有足够的表达能力来验证模块的预期客户端,比如一个ticket lock。我们还要求规范是不透明的,因为实现细节不会泄漏到规范中。以计数器为例,我们来看看一系列并发性的历史验证技术:• Owicki-Gries引入辅助状态来抽象线程的内部状态• 依赖/保证引入了冲突抽象,抽象出不同线程之间的交互;• 并发分离逻辑引入资源所有权,将干扰抽象编码为辅助状态;• 线性化引入原子性作为抽象操作的效果的一种方式我们展示了最近的发展如何使我们能够结合这些技术来提供表达方式指定并发模块,如计数器。2并发计数器在本文中,我们使用并发计数器作为运行示例。2.1执行考虑以下并发计数器的实现:6public void run(x){int [x];return r;}public void run(x){做什么?int [x];b:=CAS(x,r,r+1);}while(a);return r;public void run(x){int [x];[x]:=r+ 1;}}规范应该描述每个操作如何影响计数器的值在这里,read操作返回计数器的值,incr操作递增计数器的值并返回旧值,incr操作只是递增计数器的值一个规范应该要求计数器作为每个操作的先决条件存在,因为除非分配了保存计数器的内存,否则操作将无法工作。在本文中,我们使用抽象谓词C(x,n)来表示在存储器位置x处存在值为n的计数器。6.我们假设原始的读、写和比较交换(CAS)内存操作是原子的。P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)35函数lock(x){t:= incr(x.next);do {v:= read(x. 业主)public void run(x){wkincr(x. 所有者);}}while(v/=t);}图1.一、使用计数器模块的票证锁实现规范还应该描述并发操作上下文中允许的干扰。直观地说,读取和递增操作对于改变计数器值的并发操作来说是健壮的。相比之下,(可能更快7)wkincr要求在读取和递增值之间没有改变计数器值的并发操作2.2票证锁定客户端票锁算法[16]使用计数器模块来提供同步。锁的密码如图1所示。锁使用两个计数器,next和owner,它们的初始值都是0。线程通过调用锁操作来获取锁。此操作递增下一个计数器以获得名义票证。当所有者计数器的值与此票证一致时,线程就获得了锁。然后,它可以使用锁保护的任何资源,而不会受到其他线程的干扰。通过调用解锁操作放弃对这些资源的控制这将递增所有者计数器,将锁传递给下一个等待线程。直观地说,使用incr进行锁操作是必要的,因为它需要在并发线程获取票证方面具有健壮性。使用wkincr进行解锁操作是可能的,因为只有持有锁的线程才应该释放它。挑战在于开发一个计数器模块的并发规范,该模块足够强大,可以推理票据锁。这个例子需要精确描述每个操作如何影响计数器的值,并详细说明干扰,以直观地区分incr和wkincr。计数器及其票证锁客户端是说明关键并发模块的定义和推理困难。3顺序规范我们可以使用Hoare三元组[11]给出计数器模块的顺序规范{C(x,n)}read(x){C(x,n)}{C(x,n)}incr(x){C(x,n+1)incret=n}{C(x,n)}wkincr(x){C(x,n+ 1)}7在一个快速和肮脏的实验中,wkincr比incr快60%左右。6P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3使用标准Hoare逻辑,我们可以使用此规范来验证调用计数器操作的顺序客户端。然而,这个规范没有给出并发设置中操作行为的4辅国Owicki和Gries [19]为并发程序开发了第一个易于处理的证明技术,确定了线程之间的干扰和使用辅助状态的重要性。使用Owicki-Gries方法,每个线程都有一个顺序证明。当线程组成时,我们必须检查它们不会干扰彼此的证明。这是通过使用Owicki-Gries规则扩展标准Hoare逻辑来实现的:{P1}C1{Q1}{P2}C2{Q2}无干扰{P1<$P2}C1<$C2{Q1<$Q2}非干扰侧条件约束C1和C2的证明推导。它要求C1证明中的原子动作之间的每个中间断言必须被C2证明中的每个原子动作所保留,反之亦然。计数器的抽象规范需要在非干扰条件下具有鲁棒性。但是,通常情况下,该条件将根据并发上下文而变化。让我们假设客户端可以并发调用任何计数器操作,但不会直接与计数器的状态交互。也就是说,我们将只考虑由计数器操作本身引起的干扰为此,我们可以使用一个不变量--一个由模块中的每个原子操作保存的断言对于计数器,不变量是n。C(x,n)断言在x处的计数器被分配并且具有某个值。我们可以为计数器模块提供以下规格:{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080} C(x,n)} read(x){\displaystyle {\mathbb {n} C(x,n){\displaystyle C(x,n)}{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080} C(x,n)} incr(x){n,m. C(x,n){\displaystyle C(x,n)}{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080} C(x,n)} wkincr(x){n. C(x,n)}但是,这些规范太弱,无法将此类客户端指定为票证锁。它们丢失了关于计数器值的所有信息,并且没有给出关于操作如何改变该值的信息。事实上,读操作可以改变计数器的值,但它仍然满足规范!不幸的是,描述计数器精确值的断言不是不变的。Owicki-Gries方法能够通过使用辅助状态来提供更强的规范,辅助状态通过辅助变量记录有关执行历史的额外信息。该代码使用辅助代码进行检测,该辅助代码更新辅助变量。由于辅助代码只更新辅助变量,它对程序行为没有影响,因此可以删除-当程序运行时不需要它。P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)37{C(x,0)}y:= 0;z:= 0;{C(x,0)<$y= 0<$z = 0}{C(x,y+z)<$y= 0}做什么?int [x];n=CAS(x,r,r+1);if(b)y++;}while(a);{C(x,y+z)<$y= 1}{C(x,y+z)<$z= 0}做什么?int[x];n=CAS(x,rJ,rJ+1)如果(bJ)z++;}while(bJ= 0);{C(x,y+z)<$z= 1}{C(x,2)y= 1z = 1}{C(x,2)图二、使用辅助状态的并发增量推理作为示例,考虑两个线程都递增计数器,如图2所示。初始值为0的辅助变量y和z用于记录每个线程的贡献(即增量的数量)。对于每个线程,incr操作的代码都被插装了在CAS操作成功时更新辅助变量的代码。辅助变量必须与计数器在同一时刻更新,这样计数器总是保持两个贡献的和-我们的不变量。这用尖括号表示,它表示CAS和辅助代码应该在单个原子步骤中执行。由此产生的两增量程序的规范是强大的,具有关于计数器的初始值和最终值的精确信息。然而,这是以模块化为代价的。首先,每次使用incr操作都需要用辅助代码扩展底层实现,以增加适当的辅助变量。模块化证明不会为客户端的每次使用修改模块代码其次,递增操作需要根据客户端一个模块化的证明将给出一个捕获所有用例的模块的规范。第三,更微妙的是,Owicki-Gries方法需要全局无干扰条件。为了满足这一点,我们做了一个隐含的假设,即客户端只通过计数器操作与计数器的状态进行交互。一个模块化的证明将是明确的关于客户端行为的假设论文Owicki-Gries方法中引入的辅助状态的概念在指定并发模块时非常重要。辅助状态抽象线程的内部状态。在描述不变量时,使用辅助变量进行推理比考虑程序计数器和每个线程的局部变量更方便这8P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3抽象是向组合推理迈进的一步。正如我们将看到的,各种后续方法对辅助状态采取了比Owicki-Gries方法中提供的辅助变量更模块化的方法5干扰提取Jones [13]引入了干扰抽象,提供了依赖/保证方法作为改进Owicki-Gries方法的组合性的一种方法为了避免全局非干扰条件,规范显式地约束来自并发上下文的为此,每个规范都包含两个关系-依赖关系和保证关系-抽象线程之间的干扰。依赖关系抽象了其他线程的操作;派生中的每个断言在所有这些操作下都必须是稳定的保证关系抽象了派生中的操作;线程的每个原子更新都必须由保证来描述依赖/保证规范具有形式R,G<${P}C{Q},其中R和G分别是依赖和保证关系。当组成并发线程时,每个线程的保证必须包含在另一个线程的依赖中。因此,并行组成规则适用于:R<$G2,G1<${P1}C1{Q1}R<$G1,G2<${P2}C2{Q2}R,G1<$G2<${P1<$P2}C1<$C2{Q1<$Q2}读取和递增操作的可靠性/保证规范为:A,你好{\cH00FFFF}{\3cH000000} A. C(x,n)} read(x){\displaystyle{\mathbb {x}}} C(x,n)≤ n}A,A. C(x,n)} incr(x){n. C(x,n)≤ n}其中A ={C(x,n)~C(x,n + 1)|n∈N}。读规范有一个空的保证关系,表明读操作不会改变任何东西它具有依赖关系A,说明其他线程只能递增计数器,尽管它们可以根据自己的意愿进行多次递增。增长关系具有相同的依赖关系。它的保证关系也是A,说明增量可以增加计数器的值。必须为所有值n定义保证,因为上下文可以更改计数器值。这意味着我们不能表示incr操作只做一个增量。wkincr操作的rely/guarantee规范很微妙。回想一下,直观地说,wkincr操作是在没有其他线程并发更新计数器时使用的。作为第一次尝试,我们可以给出一个带有依赖条件的简单规范来强制执行此约束:n,G<${C(x,n)}wkincr(x){C(x,n+1)}其中G{C(x,n)~C(x,n+ 1)}.依赖关系为空,因此此规范不能用于可能发生并发更新的上下文中。这意味着P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)39保证关系可以非常精确,由单个动作组成。实际上,增量将显示为单个原子操作。虽然这个规范捕获了wkincr的一些预期行为,但它不足以解释ticket lock。使用票证锁,可以同时执行两个wkincr操作调用。任何时候只有一个线程可以调用unlock,因为只有一个线程可以拥有锁。但是,假设一个调用unlock的线程已经执行了wkincr的主体。然后,第二个线程可以正确地得出结论,它现在有锁并释放它,在第一个线程的调用返回之前。这将导致wkincr的并发调用。通过排除对具有空依赖关系的计数器的所有并发更新,上述规范不允许这种并发行为。通过改变依赖,可以允许这样的并发更新,但代价是削弱规范:R,G. C(x,n)=0.nJ≥n+1。C(x,nJ)其中R ={C(x,m)~C(x,m + 1)|m> n},G和以前一样。请注意,依赖声明只有当计数器的值大于n时才能发生并发增量。还要注意的是,在削弱依赖时,我们必须削弱后置条件以使其稳定。总而言之,这个规范又太弱了,无法解释票据锁。可以像Owicki-Gries方法那样用辅助变量来检测代码,但这会再次导致模块性的损失论文在可靠/保证方法中引入了干扰抽象的概念,这在指定并发模块时是很重要的。通过抽象不同线程之间的交互,规范可以表达其并发上下文上的约束这种抽象导致了更多的组合推理:由于干扰是规范的一部分,我们不需要为了证明并行组合而检查证明虽然它们可能会不同地指定它,但在随后的并发验证方法中通常会出现某种形式的干扰抽象6资源所有权在Owicki-Gries和rely/guarantee方法中,辅助变量提供了一种机制,用于推理哪些线程可以在何时做什么例如,可以使用辅助变量来推断各个线程对计数器的贡献,如我们在第4节中所演示的,或者一个线程可以在另一个线程之后递增并发分离逻辑是一种Hoare逻辑,其断言描述被视为资源的数据(如堆单元或计数器对象)每一次行动10P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3特定资源,前提是赋予其所代表的资源的所有权当线程在不相交的资源上操作时,它们不会相互干扰,因此它们的结果可以简单地组合在一起。这一原则体现在不相交的平行合成规则中:{P1}C1{Q1}{P2}C2{Q2}{P1<$P2}C1<$C2{Q1<$Q2}其中分离合取词P1→P2描述P1和P2的资源的不相交组合。我们可以认为所有权体现了辅助国家和干涉抽象的专门概念。所有权是辅助状态的一种形式:程序并不显式地记录哪些线程拥有哪些资源,它是我们用于推理的抽象。所有权实现了一个简单的干扰抽象:线程可以更新它们拥有的资源,所有权的不相交性强制它们不能干扰其他线程在最初的并发分离逻辑中,只能推理线程之间通过同步传输的共享资源8随后的方法[23,7,6]通过在共享资源上整合各种风格的依赖/保证推理,在此工作的基础上,并发抽象谓词(CAP)[5]方法在这些可以分割的共享资源上引入抽象,从而允许在抽象级别上进行并发操作将抽象谓词C(x,n)视为资源,我们可以将原始的顺序指定用作并发指定。然而,对于使用计数器的多个线程,它们必须使用一些同步的形式这种指定有效地强制对计数器的顺序访问这是因为客户端没有划分资源的机制:特别是,并不成立C(x,n)=<$C(x,n)<$C(x,n)继Boyland [2]之后,Bornat等人 [1]将许可会计引入分离逻辑。这允许共享资源通过将它们与区间(0, 1]中的分数相关联来划分共享资源可以通过分割该部分来细分例如,我们可以将分数与计数器资源相关联,并声明逻辑公理:C(x,n,π1+π2)<$$>C(x,n,π1)<$C(x,n,π2)其中π1+π2≤1。 我们现在可以修改计数器规格,8在[18]中,条件关键区域提供了同步机制。P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)311读访问:{C(x,n,π)}read(x){C(x,n,π)ret=n}{C(x,n,1)}incr(x){C(x,n+1, 1)incret=n}{C(x,n,1)}wkincr(x){C(x,n+ 1, 1)}请注意,我们需要完全权限(1)才能执行任何一个递增操作。这意味着只允许并发读取;并发更新必须与所有其他并发访问(增量和读取)同步如果只需要部分权限,那么对read的指定就不正确了,因为它不能再保证被读取的值与它所拥有的资源相匹配。通过改变我们解释计数谓词C(x,n,π)的方式,可以指定并发增量。现在资源C(x,n,π)不再断言计数器的值是n,除非π= 1。相反,它断言线程正在为计数器的值贡献n;其他线程也可能有贡献。我们可以通过声明逻辑公理来分割这个计数器资源C(x,n1+n2,π1+π2)<$$>C(x,n1,π1)<$C(x,n2,π2)对n1,n2∈N和π1,π2∈(0,1]. 然后,我们将计数器操作指定为:{C(x,n,π)}read(x){C(x,n,π)ret≥n}{C(x,n,1)}read(x){C(x,n,1)}{C(x,n,π)}incr(x){C(x,n+1,π)incret≥n}{C(x,n,1)}incr(x){C(x,n+1, 1)incret=n}{C(x,n,1)}wkincr(x){C(x,n+ 1, 1)}最后,我们有一个允许并发读取和增量的规范。图3显示了如何使用它来验证两个并发增量的示例而在图2中,每个线程都使用不同的辅助代码进行检测,这里的代码没有改变。不是每个线程都有一个辅助变量来记录它对计数器的贡献,而是将贡献记录在线程所拥有的辅助资源中,并封装在C(x,n,π)谓词中。这种主观辅助状态的思想是主观并发分离逻辑(SCSL)[15](以及随后的FCSL [17])的核心这种规范仍然有一些弱点。 wkincr行动必须仍然 与其他操作同步。此外,测序读取将永远不会看到计数器的递减值(因为贡献没有改变并且仅提供下限)。可以描述一个更详细的权限系统,允许在存在读取的情况下使用wkincr,并扩展谓词以记录最后一个已知值作为读取的下限。这将给我们一个更有用的,如果有点麻烦,规范。但是,它仍然不会处理票锁。虽然已经使用CAP [5]验证了票证锁,但证明取决于12P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3{C(x,0, 1)}{C(x,0,0. 5)n(x,0,0. (5)}{C(x,0,0. (5)}增量(x){C(x,1,0. (5)}{C(x,0,0. (5)}增量(x){C(x,1,0. (5)}{C(x,1,0. 5)n(x,1,0. (5)}{C(x,2, 1)}图3.第三章。基于所有权的并发增量推理底层计数器操作的原子性,以便同步对共享资源的访问。这个证明对我们的任何抽象规范都是有效的,因为它们根本不包含必要的原子性。论文由并发分离逻辑及其后继者发展起来的资源所有权的概念在指定并发模块时是重要的。所有权的习惯用法可以被看作是一种辅助状态,它批判性地体现了一种不相交和干涉抽象的概念。各种方法已经探索了所有权对并发推理的影响[5,15,17,3,14]。虽然它是一个有效的工具,可以用来提供优雅的规范,但还需要更多的东西来提供我们正在寻求的强大规范7原子性原子性是操作在单个离散时刻发生的抽象这种原子操作的并发行为相当于操作的顺序交织。原子性的一个著名的正确性条件是线性性[10],它识别并发模块的操作何时表现为原子性客户端可以像使用简单的原子操作一样使用这些操作使用线性化方法,每个操作都有一个顺序的规范。然后,操作被证明是原子相对于彼此的行为。看到这一点的一种方法是,在每个操作的调用过程中,都有一个瞬间,它似乎在这个瞬间发生了反应。 这一瞬间被称为 线性化点。在线性化的情况下,每个操作的干扰在任何时候都被任何其他操作所容忍。因此,干扰抽象被认为是模块边界。给定我们在§3中对计数器的顺序指定,我们的实现是可线性化的吗?如果我们只考虑读和递增操作,那么是的,它是。然而,wkincr操作的添加破坏了线性化。wkincr的问题是,例如,两个并发调用可能导致计数器只增加一次。这与原子行为不一致问题的本质是我们只设想在并发的P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)313没有其他增量的上下文在这种情况下,它看起来像原子一样。顺序规范本身不能表达这种约束。我们需要一个约束并发上下文的干扰抽象线性化与语境修饰的概念有关 通过上下文细化,程序代码的行为由(更抽象的)规范代码描述。[9]上下文精化断言,在任何上下文中,规范代码都可以被程序代码替换,而不会引入新的可观察行为;我们说程序代码上下文地精化规范代码。Fili po v i'cetal. [8]我已经表明,在某些假设下,对于一种编程语言,线性化意味着该语言的上下文细化。对于可线性化的模块,每个操作都在上下文中细化了原子执行的操作本身。例如,incr(x)在上下文中细化了incr(x)。CaReSL [22]是一种用于证明并发程序的上下文细化的逻辑CaReSL在证明技术中利用了辅助状态、干扰抽象和所有权等技术。然而,这些概念并没有在其规范中公开。这意味着在CaReSL中wkincr的合适规范应该是什么并不明显。论文原子性的概念是由线性化提出的,它在并发模块的定义中起着重要的作用 原子性可以被看作是一种干扰抽象:它有效地保证了来自操作的唯一可观察到的干扰将发生在其执行的单个时刻。 这是一个强大的抽象,因为客户端不需要考虑原子操作的中间状态(对于非原子操作,可能会违反不变量),而只需要考虑它执行的整体8合成现在我们将研究几种方法,它们将我们迄今为止讨论的思想结合在一起,为并发模块提供表达性规范8.1高阶方法Jacobs和Piessens [12]介绍了克服Owicki-Gries方法的非模块性的一种方法他们的关键思想是为操作提供更高阶的规范,这些规范由辅助代码参数化,当抽象原子操作出现时执行在前面我们为不同的调用站点不同地插装incr操作的代码的地方,这里它是统一插装的;辅助代码是在调用站点确定一般来说,规范代码不需要直接执行,尽管它确实有语义。14P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3将这个想法应用到incr操作中,我们得到以下代码:public voidrun(x){做什么?int [x];n=CAS(x,r,r+1);如果(b)ρ;}while(a);return r;}注意,ρ是操作的辅助代码参数。当对计数器的原子更新发生时,辅助代码被运行并且可以更新客户端的辅助变量。增量的指定由辅助码的指定参数化。作为一种证明规则,具体规定如下:I(x)是一种优惠。C(x,n)<$R(n)<$n. {R(n)<$P} ρ {R(n +1)<$Q(n)}I(x)<${S<$P}incr(x,ρ){S<$Q(ret)}在这个规则的结论中,I(x)是一个不变量;它与前置条件和后置条件不相交,并且必须通过所有线程的原子更新来保留在计数器以原子方式递增时,概念上发生以下步骤:(i) 来自前提的等价性用于将不变量I(x)和前提S的一部分的组合转换为针对某个n值的反谓词C(x,n)和R(n)。(ii) 模块执行递增,将C(x,n)更新为C(x,n+1)。(iii) 运行辅助码ρ,将R(n)<$P更新为R(n+ 1)<$Q(n)。(iv) C(x,n+1)和R(n+1)一起被转换回来以恢复不变量I(x)和S.这种规范现在允许我们以模块化的方式利用辅助变量的表达能力。图4显示了如何使用这种技术来证明两个并发增量。这个证明与图2所示的证明非常相似。新的规范允许我们抽象由incr执行的原子更新,并为两个线程使用相同的模块实现在图4中,不变量I(x)被实例化为C(x,y+z)。谓词R(n)被实例化为n=y+z。谓词S是True,而P和Q在每个调用点用incr的前置和后置条件读操作可以指定为:I(x)是一种优惠。 C(x,n)<$R(n)<$n. {R(n)<$P}ρ{R(n)<$Q(n)}I(x)<${S<$P}read(x,ρ){S<$Q(ret)}P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)315{C(x,0)}y:= 0;z:= 0;{C(x,0)<$y= 0<$z = 0}{y= 0z = 0}联系我们return(x,y);[001pdf1st-31files][001 pdf1st-31files]int n= nums(n,n);{z= 1}{y=1z= 1}{C(x,2)y= 1z = 1}{C(x,2)图四、使用参数化辅助代码进行并发增量推理最后,回想一下,wkincr操作是在环境没有更新时使用的这可以被指定为:I(x)P惠C(x,n)<$R{C(x,n+ 1)<$R}ρ{I(x)<$Q}I(x)<${P}wkincr(x,ρ){Q}与wkincr规范的一个关键区别是,n在每个子过程中都没有量化。这是因为计数器的值必须在更新之前由其他线程保留。请注意,虽然这些规范是以证明规则的形式编写的,但它们实际上是蕴涵。如果一个客户端建立了这个结论,那么它就可以使用这个结论。实现必须表明结论是从这些假设中得出的。谓词I、P、Q、R和S以及幽灵码ρ都是通用量化的:客户端可以根据需要实例化它们这种高阶规范方法已被其他高阶逻辑采用,如HOCAP [21],iCAP [20]和Iris[14]。在这些逻辑中,辅助状态不是由辅助代码操纵的,而是由视图移位操纵的[4]。这些视图转换本质上服务于相同的目的-它们可以更新辅助状态,但对具体状态没有影响-但不涉及检测代码。8.2一阶方法在程序逻辑TaDA [3]中引入了一种为并发模块提供规范的替代方法,即使用原子三元组。原子三元组不是将原子规范视为高阶构造,而是将这些规范作为一阶构造构建到TaDA原子三元组具有以下形式:x∈X。P(x)从表面上看,这可以理解为“C原子地将P(x)更新为Q(x)(对于任意的x∈X)"。它实际上的意思是更微妙一点规范的实现可以假设断言P(x0)最初成立(对于某些x0∈X)。它必须能容忍来自环境的干扰不变式:C(x,y+z)16P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3将P(x)更新为P(xJ)(对于任意x,xJ∈X)。它可以自由地更新状态,只要它保持P(x)(对于x的当前值),直到它将其更新为Q(x)。在此更新之后,Q(x)不再可用于实现(另一个线程可能正在使用它)。最后,如果在某个点没有将P(x)更新为Q(x),使用原子三元组,我们可以将计数器指定为:n. C(x,n)n. <$C(x,n)<$incr(x)<$C(x,n +1)<$ret = n<$C(x,n)直观地说,前两个规范声明计数器的值将被原子地读取和递增,即使在存在由环境改变计数器的值的并发更新的情况下也是如此-因为值n由. 但是,环境必须保留计数器,例如:最后一个指定意味着wkincr(x)将原子地将计数器从n更新为n+1,只要环境保证共享计数器不会在原子更新之前更改值-因为n的值不受约束。原子三元组指定了关于抽象的操作(例如C(x,n)),这意味着每个操作都可以独立验证。这使得可以使用新操作扩展模块,而无需再次验证相比之下,线性化是一个完整的模块属性:添加新的操作(例如wkincr)可以打破线性化。在[3]中,我们引入了一个广义的原子三元组,它可以将原子性与资源转移相结合。例如,我们可以指定一个将计数器的值读入缓冲器的操作;读操作是原子发生的,但写入缓冲器的操作不是原子发生的,因此缓冲器的所有权在客户端和实现之间转移。这对于传统的线性化是不可能的,尽管Gotsman和Yang [9]提出了支持所有权转移的线性化扩展。评价本节中显示的反规范是强的:客户端可以从中导出抽象的不相交规范。此外,它们足够强大,可以支持同步:票锁的正确性可以从计数器规范中得到证明。这些具体化方法的表达能力足以在客户端和实现上强制执行义务。相比之下,CAP规范往往会过度限制客户端(例如, 计数器规范不能用于同步),而线性化规范往往会过度限制实现(例如,计数器不能提供WKINCR操作)。原子三元组已经在Iris中编码[14],将它们解释为规范雅各布斯-皮森风格这捕获了原子三元组背后的内涵意义-也就是说,它们可以用于什么-在TaDA中通过使用原子三元组的证明规则P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3179结论我们已经考虑了一些证明方法验证并发程序:Owicki-Gries,依赖/保证,并发分离逻辑和线性。在每种方法中,我们都发现了对指定并发模块的特别有价值的贡献。最后,我们展示了如何将这些想法结合在一起,以产生既有表现力又有模块化的规范引用[1] Richard Bornat,Cristiano Calcagno,Peter O'Hearn,and Matthew Parkinson.分离逻辑中的权限核算。见POPL,第259[2] 约翰·博兰德检查与部分权限的冲突SAS,第55-72页,柏林,海德堡,2003年史普林格出版社[3] Pedro da Rocha Pinto,Thomas Dinsdale Young,and Philippa Gardner. TaDA:时间和数据抽象的逻辑。在ECOOP,第207-231页[4] Thomas Dinsdale-Young、Lars Birkedal、Philippa Gardner、Matthew Parkinson和HongseokYang。视图:并发程序的组合推理。在POPL,第287-300页[5] Thomas Dinsdale-Young、Mike Dodds、Philippa Gardner、Matthew J. Parkinson和Viktor Vafeiadis。并发抽象谓词。ECOOP,第504[6] Mike Dodds,Xinyu Feng,Matthew Parkinson,and Viktor Vafeiadis. 拒绝担保推理。在ESOP,第363-377页[7] 新御风。局部可靠保证推理。见ACM SIGPLAN通告,第44卷,第315-327页。ACM,2009年。[8] I vanaFili pov ic,PeterO'Hearn,Noam Rinetzk y,and Hongseok Yang.并发对象的抽象。见ESOP,第252-266页[9] Alexey Gotsman和Hongseok Yang。所有权转移的线性化。在CONCUR,第256[10] 作者声明:Dr.翼线性化:并发对象的正确性条件。ACM翻译计划。Lang.系统,12(3):463 -492,1990年7月。[11] C. A. R.霍尔计算机程序设计的公理基础。Commun. ACM,12(10):576 -580 ,October 1969 .[12] 巴特·雅各布斯和弗兰克·皮森斯。明确的模块化细粒度并发规范。在POPL,第271-282页[13] 克莱·琼斯。(并行)程序的规范和设计。IFIP大会,第83卷,第321-332页[14] Ralf Jung、David Swasey、Filip Sieczkowski、Kasper Sundarsen、Aaron Turon、Lars Birkedal和DerekDreyer。Iris:Monoid和不变量作为并发推理的正交基础。在POPL,第637[15] 鲁伊·雷-怀尔德和亚历山大·纳涅夫斯基。粗粒度并发的主观辅助状态在POPL,第561-574页[16] John M.作者声明:Michael L. Scott.共享内存多处理器上可扩展同步的算法。ACM Trans. Comput.系统,9(1):21[17] 亚历山大·纳涅夫斯基,鲁伊·莱·怀尔德,伊尔·阿·塞尔日,还有热尔·曼和雷·德尔比安科。细粒度并发资源的通信状态转换系统。在ESOP中,第290[18] Peter W.奥赫恩资源、并发和本地推理。Theor. Comput. Sci. ,375(1-3):271[19] Susan Owicki和David Gries并行程序的公理性质:公理方法。Commun. ACM,19(5):279 -285,May1976.[20] 卡斯帕·斯沃森和拉尔斯·伯克达尔。非谓词并发抽象谓词。在ESOP中,第149-168页18P. da Rocha Pinto et al. /Electronic Notes in Theoretical Computer Science 319(2015)3[21] 卡斯珀·森普森,拉尔斯·伯克达尔,马修·帕金森。并发数据结构分离的模块化推理。在ESOP中,第169[22] 亚伦·图伦德里克·德雷尔和拉尔斯·伯克达尔在高阶并发逻辑中统一精化和Hoare风格的推理。见ICFP,第377[23] 维克多·瓦菲亚迪斯模块化细粒度并发验证。剑桥大学计算机实验室博士论文,2008年。
下载后可阅读完整内容,剩余1页未读,立即下载
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)