并发分离逻辑的博弈论帐户和并发分离逻辑的博弈语义规范逻辑

关于我们可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）241-256www.elsevier.com/locate/entcs并发分离逻辑保罗-安德烈·梅利埃a Léo StefanescobaIRIF、CNRS、巴黎狄德罗大学里昂高等师范学校摘要在本文中，我们开发了一个博弈论帐户的并发分离逻辑。 对于代码面对环境的每一个执行痕迹，我们将一个特定的游戏关联起来，夏娃为代码而游戏，亚当为环境而游戏。Eve和Adam的目的是将执行跟踪的每个中间机器状态分解为三部分：一部分用于代码，一部分用于环境，一片用于可用的共享资源。我们通过将逻辑的每一个派生树解释为这个特定游戏的获胜策略关键词：并发分离逻辑，博弈语义规范逻辑1介绍并发分离逻辑（CSL）是O'Hearn [ 10 ]对Alfred的分离逻辑[ 12 ]的扩展由于分离逻辑的框架规则，这种规范逻辑使人们能够以优雅和模块化的方式建立这些程序的良好行为并发分离逻辑r1：P1，. r n：P n{P} C {Q}由Hoare三元组P C Q连同上下文Γ =r1：P1，.，r n：P n，它声明了许多资源变量r k（或互斥体）以及它们满足的CSL公式P k作为不变式。程序逻辑的有效性依赖于可靠性定理，该定理指出，并发分离逻辑.r1：P1，. r n：P n{P} C {Q}确保（1）并发程序C在执行时不会产生任何竞争条件，以及（2）程序C将转换每个初始状态https://doi.org/10.1016/j.entcs.2018.03.0261571-0661/© 2018由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。242P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241∗{} → {}当它终止时，满足P的状态变为满足Q的状态，只要在内存中分配的每个资源rk满足CSL不变量Pk。逻辑的可靠性是由Brookes在他关于并发分离逻辑的迹语义的开创性论文中建立的[5，6]。他的可靠性证明是社区中非常关注的对象，并且以许多不同的方式重新审视，无论是语义[13]，句法[2]还是公理[7]，并在证明助手中形式化在所有这些可靠性证明中，一个主要的技术挑战是建立并发规则的有效性Γ{P1}C1{Q1}Γ{P2}C2{Q2}并发规则Γ{P1<$P2}C1<$C2{Q1<$Q2}框架规则：Γπ{P}C{Q}标架规则Γ{P<$R}C{Q<$R}在本文中，我们基于一种受游戏语义启发的新方法建立了这两个规则（以及CSL）的有效性，该方法依赖于观察CSL的派生树π定义了特定游戏中的获胜策略[π]正如我们将看到的，指定游戏本身是从代码C的执行及其与环境（称为框架）的交互中派生出来的，使用共享内存上的锁。指定游戏将通常的信赖和保证条件表达为夏娃（代表代码）和亚当（代表框架）之间进行的交互式游戏中的获胜条件在可靠性的语义证明中，除了描述变量和堆的状态的基本概念存储器状态之外，通常考虑“状态”的两个概念(2) 逻辑状态，包括权限和其他在执行级别不可见的信息，但在逻辑中指定状态所必需的。特别是，分离逻辑的张量积需要关于权限的信息，因此它是在逻辑状态上定义的，而不是在机器状态上。 出发点的文件是观察到，存在着第三个概念的状态，我们称之为分离状态，隐含在工作中的所有语义证明的可靠性。分离状态描述了机器的全局（逻辑）状态的哪一部分由在执行过程中交互的每个组件处理。它被定义为一个三元组（σC，σ，σF），由以下组成：• 代码的逻辑状态σC∈LState，• 帧的逻辑状态σF∈LState• 函数σ：r1，...，r nLState+C，F，它告诉每个资源变量r是否被代码锁定并拥有，σ（r）=C，被框架锁定并拥有，σ（r）= F，或可用逻辑状态σ（r）∈ LState。这就引出了一个机器状态雷菲讷分离态雷菲讷逻辑状态（一）P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241243、②/∗► 关于我们∈其中，机器状态和逻辑状态这两个概念由分离状态的概念“细化”，分离状态传达关于锁（作为机器状态）和关于权限（作为逻辑状态）的也就是说，每一个分离的国家（σC，σ，σF）∈SState精化由分离张量积定义的逻辑状态②（σC，σ，σF②（σC，σ，σF）d=efσCr∈dom（σ）σ（r），σF（2）其中dom（σ）表示σ中可用的资源集合，在这个意义上，σ（r）=C，F。类似地，每一个分离状态（σ C，σ，σ F）都定义了一个机器状态（μ，L），定义为逻辑状态（2）下的内存状态μ，加上锁定资源集合L = dom C（σ） dom F（σ），详见§ 8。同样，逻辑状态的概念对于定义张量积是必要的。分离逻辑，从而指定状态，从机器状态到分离状态的转换是必要的，以指定代码，以及它与环境和资源交互的方式。本文的观点是：Hoare三元组Γ中的分离逻辑公式P和QP C Q不指定逻辑状态σ=②（σC，σ，σF）L机器本身的状态，但这个状态的片段σC代码C在执行开始和结束时的逻辑状态σ因此，分离状态的概念是分离逻辑中霍尔三元组概念的核心。我们沿着报纸上的以下线索走在讨论了相关的工作之后，我们在§ 3中阐述了机器状态和机器指令的两个概念。这使我们能够在§ 4中定义机器状态上的执行轨迹的概念以及它们上的一些代数运算。并发程序的跟踪语义，以及它们作为转换系统的解释，然后在§ 5和§ 6中公式化。一旦机器状态的概念被用来描述语言的跟踪语义，我们就转移到跨度的逻辑方面，并在§ 7中制定逻辑状态的概念和§ 8中的分离状态的概念。 在§ 10中，我们解释了如何将每个执行轨迹与在§ 9中定义的分离状态图的路径上进行的特定游戏相关联。这些博弈的移动表达了由分离逻辑强制执行的所有权规则，特别是与并发分离逻辑中的锁相关联的规则最后，我们在§11中证明CSL是合理的，证明了逻辑的每个派生树都定义了一个策略，该策略将执行跟踪的代码的每个步骤提升到分离状态图中。2相关工作并发分离逻辑的可靠性的几个证明已经给出。正确性的第一个证明是由Brookes在[5，6]中使用语义思想设计的。在他的证明中，每个程序C都被解释为一组244P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241► 关于我们从x读取71，从y读取36，获取锁r，....该模型的一个有趣的特性是，这些动作跟踪不提及（至少显式地）代码在执行时产生的机器状态。通过存在非顺序一致的迹线，例如，在x中写入89，从x中在模型中。这个想法是，环境可能在代码的两个动作之间改变了变量x的值。逻辑上的分离使人们能够将动作跟踪分解为本地计算，以反映程序Vafeiadis给出了另一个基于更直接的操作直觉的正确性证明[13]在他的证明中，代码被解释为一个转移系统，其顶点是由代码C和存储器的状态σ组成的对（C，σ） 可靠性证明的核心是，执行的每一步都将堆分解为三个部分，分别对应于代码、资源和框架。证明是在并发分离逻辑中建立三元组ΓPCQ的导出树π上用归纳法完成的。因此，使用分离态的想法来自Vafeiadis的证明，这是最接近我们的证明。然而，除了我们发展的博弈论观点之外，一个不同之处在于，我们对分离状态有一个更有内涵的描述，由跟踪每个可用锁的状态的函数σ与上面提到的语义证明相反，Balabonski，Pottier和Protzenko [2]为Mezzo开发了一个纯语法的正确性证明，Mezzo是一种功能性语言，配备了基于并发分离逻辑的类型和能力系统逻辑的合理性遵循他们的方法，从一个进步和维护定理的类型系统的Mezzo。我们在这项工作中的重点是开发一个博弈论的方法，并发分离逻辑。出于这个原因，我们倾向于保持逻辑和并发语言相当简单和具体。特别是，我们不考虑更近的，复杂的和公理化的逻辑版本，如Iris [8，9]。3机器状态和机器指令本节的目的是介绍机器状态和机器指令的概念，这些概念将在整个论文中使用。我们假设给定变量名的可数集Var，值的Val，内存位置的Loc_Val和资源的LockName实际上，Loc=N，Val=Z。定义3.1（内存状态）内存状态μ是一对（s，h）具有有限域s：Var~ finVal和h：Loc~ finVal的部分函数，称为内存状态μ的堆栈s和堆h。 存储器状态的集合被表示为State。部 分 函数s和h的域分别记为vdom（μ）和hdom（μ），我们将它们的不相交并记为dom（μ）。P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241245⊆∈∈⊆{}envM1envenvMp定义3.2（机器状态）机器状态s =（μ，L）是由内存状态μ和资源子集LLockName组成的一对，称为锁定状态，它描述了s中锁定资源的子集。机器状态的集合被表示为MState。机器步骤被定义为机器状态之间的标记转换，可以有两种不同的类型：smsJsmsJ这取决于指令m∈Instr是否已成功执行（左侧）或是否产生了运行时错误（右侧）。 当我们不想指定指令是否产生了运行时错误时，我们写m：s sJ标记机器步骤的机器指令定义如下：m：：= x：= E |x：=[E]|[E]：= EJ|NOP |x：= alloc（E）|处置（E）|P（r）|V（r）其中xVar是一个变量，rLockName是一个资源变量，E，EJ是带有变量的算术表达式通常，指令x：=E将在存储器状态μ中的表达式E的值E（μ）分配给变量x，指令P（r）在资源变量r可用时锁定资源变量r，而指令V（r）在资源变量r被锁定时释放资源变量r，如下所述：E（μ）=vr∈/Lr∈/L（μ，L）x：=E（μ[x<$→v]，L）（μ，L）P（r）（μ，L±{r}）（μ，L±{r}）V（r）（μ，L）由于包含Loc Val，表达式E也可以表示位置。在这种情况下，[E]指的是内存中位置E的值。指令nop（表示无操作）不会改变逻辑状态，而x：=alloc（E）分配（以非确定性的方式）堆上的一些内存空间，用表达式E的值来重新分配，并将位置的地址返回给变量x，而dispose（E）将地址E的位置重新分配。接下来，对于由指令m执行的锁的集合，写入l ock+（m）将是一种方便的做法，也就是说，如果m = P（r），则l o c k +（m）= r，否则l ock+（m）=r;lock-（m）是由指令m释放的锁的集合，也就是说，如果m = V（r），则lock-（m）={r}，否则lock-（m）={r}。4执行轨迹既然已经引入了机器状态的概念，那么解释程序的下一步就是定义执行轨迹的概念，其中有两种转换：由代码“播放”的定义4.1（轨迹）轨迹t是机器状态s−−→s−−→s−−→. . . −e−n→vss−−→s1 2 3它的平稳过渡MKS2p−−→2p+12p+22k−→s2k+11 ≤k ≤p246P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241∈K×≤≤·∈∈联系我们关于我们∈∈由指令mk∈Instr使得s2kMKs2k+1的芯片是由最后一个过渡是由环境发挥作用迹线的集合由迹线表示。对于迹的初始和最终状态，我们记为t=s1和t=s2p+2t分别为迹线 长度len（t）= p被定义为跟踪中代码转换的数量，并且t[k]= s2kM−−−→ s2k+1表示迹t的第k个偶跃迁，对于1klen（t）。 注意跟踪t总是由环境转换开始和停止，并且其转换次数等于2len（t）+ 1。我们指出以下事实，我们将经常使用我们的证明和建设：命题4.2迹t ∈迹的特征在于它的初始状态t [0]t和它的最终状态t [1]t，以及代码转换序列t[k]，其中1 ≤ k ≤ len（t）。我们现在介绍一些重要的代数结构上的执行痕迹，其目的是在痕迹的水平上反映程序的顺序和并行组合。定义4.3（顺序合成）给定两条迹t1，t2迹，使得t1（t1）=t0（t2），将t1t2迹定义为长度为len（t1）+len（t2）的迹，初始状态为t0（t1），最终状态为t1（t2），偶跃迁定义为（t·t）[k]=.t1[k]如果1≤k≤p，t2 [k-p]如果p +1 ≤ k ≤ p + q。定义4.4（限制）设迹p表示长度为p的迹的集合。每个递增函数f：{1，...，p}→ {1，.，q}诱导一个约束函数f：迹线q−→迹线p它将长度为q的迹t转换为长度为p的共始共尾迹ff（t）0f由指令f（t）[k]= t [f（k）]定义，其中1 ≤ k ≤ p。定义4.5（Shu n e）两个自然数pN和qN的shu n e是单调双射ω：1、......、p1、......、Q1、......、p+q。蜀汉画集设p和q为Shu_s（p，q）。每一个Shu_eω∈Shu_e（p，q）诱导一对增函数ω1：{1，…，p}→ {1，.，p+ q}和ω2：{1，...，q}→ {1，.，p+ q}定义为将ω限制为1，…，p和1，…，Q，分别。从这一点可以立即得出，命题4.6每一个shu eω∈Shu es（p，q）诱导一个函数ω：T种族p+q−→T种族p×T种族q它将一个长度为p+q的点t映射到p空气（ω1<$（t），ω2<$（t））∈T族p×痕迹q。12P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241247ǁǁ→.›−→. . . .. . ⊆ ⊆. .... ..定义4.7平行合成t1 <$t2是迹t∈迹的集合，使得对于某些shu_eω∈ Shu_e（len（t1），len（t2）），ω_e（t）=（t1，t2）。注意，t1 t2中的每条迹t都满足len（t）=len（t1）+len（t2），更重要的是，只要两条迹t1和t2不是共始和共尾的，两条迹t1和t2的平行合成t1 t2就是空的。我们最后一个构造hide[r]的目的是定义4.8函数hide[r]：Traces Traces通过应用函数（μ，L）−→（μ，L\{r}）：MState−→MState到原始跟踪的每个机器状态，并且函数mnop，如果m=P（r）或V（r）我则不然跟踪的指示： Instr−→Instr5变迁系统在这一阶段，我们准备引入转换系统的概念，我们将使用它来描述由我们的并发语言的程序生成的跟踪。在这些执行轨迹中，人们希望区分（1）终止并返回的轨迹和（2）尚未完成或终止并中止的其他轨迹。这导致我们对过渡系统的以下定义：定义5.1（变迁系统）变迁系统T=（T，T）是一组在prefix下闭合的迹T，以及一个子集 不T，谁的 据说痕迹会回来。我们将在下面解释如何将上一节§ 4中定义在迹上的代数运算提升到过渡系统。定义5.2两个变迁系统T和TJ的顺序组合被定义为变迁系统T;TJ如下：T; T J= T {t·tJ|t ∈ T，TJ∈ TJ且T ={t·TJ}T; TJ={t·TJ|t∈ T，tJ∈|TJ|且<$1t=<$0tJ}定义5.3两个跃迁系统T和TJ的平行合成定义为跃迁系统T<$TJ如下：T1<$T2=t1<$t2。T1和T2。 =.t1t2ti∈Tit i∈. Ti.定义5.4与变迁系统T相关联的变迁系统hide[r]（T）对于一个锁，r∈LockName的定义如下：hide [r]（T）={hide [r]（t）|t ∈ T} 。hide [r]（T）. ={hide [r]（t）|t∈。T. }中。248P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241∈<$）（2）∈−→... .直觉是，. .联系我们执行指令m之后，Menv请注意，每个指令mInstr都包含一个转换系统m，其定义如下：envm环境m（m）={s1−−→s2−→s3−−→s4|s2s3}m环境m. 分）。 ={s1−−→s2−→s3−−→s4|s2s3}en表示nt已完成转换s1−e−n→v（s）2，并在机器步骤S2和S3是成功的，并且不中止。下面的代数运算转换系统反映了程序在使用锁r时的计算情况。在执行之前，并且在程序返回的情况下释放锁R定义5.5[r]（T）中与转换系统T和锁r∈LockName相关联的转换系统定义如下：inside[r]（T）=P（r）;T;V（r）.下面对转换系统的操作将使我们能够解释并发程序上的条件分支。定义5.6当入口[P]（T）与转移系统T=（T，T）和谓词P：MState true，false，aborton memory states相关联时，转移系统定义如下：当中心[P]（T）={t∈T|P（t）=true}当中心[P]（T）={t∈T|P（t）=true}其中，t = s2表示代码在轨迹t中的第一个状态。当[P]（T）为假时，转换系统的定义也是类似的，在定义中用假替换真。在语言中解释条件分支的一个微妙但重要的方面是，布尔表达式B的求值可能不会成功，通常是因为它的一个变量xVar没有分配。 在这种情况下，计算会产生一个异常，然后由操作系统处理。在我们的跟踪语义中，通过定义一个名为whenabort[P，C]的专用转换系统来处理这种中止情况，其构造在附录[1]中有详细说明。6并发语言既然我们已经定义了转换系统上的基本操作，我们就可以定义并发语言的操作和交互语义了。该语言由布尔表达式B、算术表达式E和P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241249ǁ（Ⅲ）（Ⅲ）（）（）def如果B，则C，否则C）=.第二， ）<$）def资源rdoC）d=efhide[r]。（C）β，.第二， ）<$）<$）命令C，使用下面的语法：B：：=正确|虚假|B ∧ BJ|B ν BJ|E=EJE：：= 0 |1|......这是什么？ |X |E +EJ|E E JC：：= x：= E |x：=[E]|[E]：= EJ|C; CJ|C1-C2|skip| 而B做C|资源r do C|当B做C时，| 如果B那么C1否则C2|x：= alloc（E）|处置（E）并行组合操作符C1C2使两个程序C1和C2能够通过称为资源的互斥体并发地交互。资源r使用资源r声明，并在B执行C时使用withr获取，它等待布尔表达式B为真以继续。当然，一个互斥锁在任何时候最多只能由一个执行线程持有在我们遵循的语义方法中，每个命令C都被翻译成一个转换系统C，它描述了C的可能的交互式执行，以及无论他们是否回来。码C翻译转换系统C解释C是由结构归纳法定义的。司令部C对于每个叶节点C，将指令m∈Instrx：= E|x：= [E]|[E]：= [EJ] |NOP |x：= alloc（E）|处置（E）它定义了过渡系统Cd=efM . 非叶命令然后使用§5中介绍的过渡系统上的代数运算来定义JdefJJdefJCC=CC，C; C=C;C，当B做C时，带r）=whentrue[B].在[r]里面。（C）当abort[B，CJ]时，其中CJ=当B在定义的最后一部分做C时，def1 2while循环whentrue[B]nop; C1当false[B] nop ; C2whenabort[B，ifBthenC1elseC2]，当B做C时）=n≥0F n（n）定义为连续函数F：Trans→Trans的最小定点：F（T）=whentrue[B]NOP; C; Twhenfalse[B]nopwhenabort [B，whileBdo C].7逻辑状态正如我们在引言中所解释的，在分离逻辑中对并发程序的推理需要引入一个适当的逻辑状态概念，包括250P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241（2）⎧∈ T·T不⎪⎩p∗σv∈Val，σ（x）=（v，p）σE1=E2E1=E2fv（E1=E2）vdom（h）σ<$P<$Q<$$>（σ<$P）<$（σ<$Q）σ<$P<$Q<$$>σ<$Petσ<$Qσ<$P<$Q<$$><$1σ2，σ=σ1<$σ2etσ1 <$Petσ2<$Q图1.并发分离逻辑谓词的语义关于权限的信息我们考虑的并发分离逻辑的版本几乎与O'Hearn和Brookes[10，5]的原始公式相同一个不同之处是，我们受益于[3，4，11]中的工作，并使用权限和Ownp（x）谓词来处理堆以及堆栈中的变量。因此，我们假设给定一个任意的部分可消交换幺半群Perm，我们称之为许可幺半群，如下[3]。我们要求许可幺半群包含一个可区分的元素它不允许任何倍数，即。xPerm，x没有定义。这个想法是，程序在内存中的某个地方写入时上面的属性确保了一段状态不能被两个并发程序同时写入和访问（读或写），因此，在语义中逻辑状态的集合LState的定义方式与内存状态的集合State类似，但增加了权限：LState=（Var~finnVal×Perm）×（Loc~finnVal×Perm）许可的一个主要好处是，它们使我们能够定义两个逻辑状态σ和σJ之间的分离张量积σσJ。当它被定义时，逻辑状态σ∈σJ被定义为具有域dom（σ<$σ）= dom（σ）dom（σJ）对于a∈VarNLoc：如果a∈dom（σ）\dom（σJ），则a∈ dom（σ j）σσJ（a）=σJ（a）如果a∈dom（σJ）\dom（σ）（v，p·PJ）若σ（a）=（v，p）且σJ（a）=（v，PJ）两个逻辑状态σ和σJ的张量积σ σJ没有另外的定义。换句话说，如果张量积被很好地定义，那么潜在的记忆状态σ和σJ在共享变量和堆位置的值上是一致的。并发分离逻辑公式的语法和语义与分离逻辑相同。公式的语法如下：P、Q、R、J：：=电磁脉冲|真正|虚假|P ν Q |P ∧ Q|欧元/英镑|X .P |X .P|Ownp（x）|第一季第二集|E1E2公式的语义表示为图1中定义的满足谓词σP。并发分离逻辑的基础证明系统是一个关于序列的微积分，定义为以下形式的Hoare三元组：ΓP}C{Q}，P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241251∈其中C Code，P，Q是谓词，而Γ是上下文，定义为具有从资源变量的集合LockName到谓词的有限域的部分函数。直观地，上下文r =r1：J1，.，r k：J k描述了资源变量ri满足的不变量J i。 这些资源的目的是提供片段在执行过程中，不同线程之间共享的内存。图2给出了推理规则。与资源rdoC相关联的推理规则Res将代码所拥有的一段内存移动到共享上下文Γ中，这意味着它可以在C中被并发访问。然而，对这段记忆的访问是由with结构介导的，它在一个人必须归还它的条件下授予临时访问（规则W ITH）。 经预告而规则C O nj，上下文r =r1：J1，.，r k：J k必须是精确的，在这个意义上，每个谓词J i都是精确的。定义7.1（精确谓词）一个谓词P是精确的，当对任何σ∈LState，则至多存在一个σJ∈ LState使得<$σJJ，σ=σJ <$σJJ且σJ<$P。Γ<${OwnT（x）<$X=E}x：=E{OwnT（x）<$x=X}AFFΓ{E→−}[E]：=E′{E<$→E′}斯托雷x∈/fv（E）LoadΓ<${E<$→pv<$OwnT（x）}x：= [E]{E<$→pv <$OwnT（x）<$x=v}Γ{P}C{Q}Γ{Q}C′{R}Γ{P}C;C′{R}SE QPdef（B）{P{PB}C2{Q}如果如果B那么C1否则C2{Q}r精确Γ {P1}C{Q1}Γπ{P2}C{Q2}共轭Γ{P1<$P2}C{Q1<$Q2}r，r：J∈{P}C{Q}RES资源r做C{Q<$J}P<$def（B）Γ<${（P<$J）<$B}C{Q<$J}当B做C{Q}时，r，r：J∈{P}，其中rWItHΓ{P1}C1{Q1}Γ{P2}C2{Q2}PaRΓ{P1<$P2}C1<$C2{Q1<$Q2}Γπ{P}C{Q}F范围Γ{P<$R}C{Q<$R}图2.并发分离逻辑的推理规则8分离状态我们现在介绍第三个状态概念，它显示（逻辑）内存的哪个区域属于代码，哪个区域属于框架，以及哪个区域属于代码。是共享的。我们假设给定资源变量的有限集合LockName定义8.1分离态是三元组（σC，σ，σF）∈LState×（LockName→LState+{C，F}）×LState252P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241、②∈、② →∈env∈CM这样，下面的状态被定义为：σCr∈dom（σ）σ（r），σF其中dom（σ）={r ∈ LockName |σ（r）∈LState}，dom C（σ）={r∈LockName|σ（r）= C}，dom F（σ）={r∈LockName|σ（r）= F}。当L=domC（σ）domF（σ）和记忆状态μState都等于σCr∈dom（σ）σ（r），<$σF∈LState（3）在函数U：LState State下，忘记了权限。请注意，根据定义，每个分离状态（σ C，σ，σ F）组合成一个唯一的机器状态，我们将其简洁地写成（μ，L）= ②（σ C，σ，σ F）。9机器和分离状态在这一节中，我们引入了机器状态和分离状态的两个标号图G（MState）和G（SState），并构造了一个图同态②：G （ SState ） −→G （ MState ）（4），它将每个分离的状态（σC，σ，σF）映射到它的组合机器状态（σ，L），以介绍中描述的方式。定义9.1机器状态图G（MState）是这样一个图，它的顶点是机器状态的MState，它的边是以下类型的代码或环境转换：• 对于每个机器步骤smsJ，• 对于每对s，sJ∈M机器状态，有一个环境变迁s−−→sJ状态，其中env只是一个标记，表明转换已被Environment触发。请注意，迹tTraces（参见定义4.1）与图G（MState）中以环境边开始和结束的交替路径是一样的。定义9.2分离状态图G（STATE）是这样一个图，它的顶点是分离状态，它的边是夏娃移动或亚当移动的下列类型：• 夏娃的动作（σC，σ，σF）−−m→（σJ，σJ，σF）由指令m∈Instr标记，使得②（σC，σ，σF）②（σCJ，σJ，σF）P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241253F∈∈∈en∈- 不超过在机器状态之间，并且使得锁定资源上的以下条件进一步得到满足：其中σ（r）=σJ（r），<$r∈lock+（m）， r∈dom（σ）<$r∈domC（σJ），<$r∈lock−（m），r ∈domC（σ）< $r∈dom（σJ）;• 亚当移动的形式（σC，σ，σF）−−en−v→（σC，σJ，σJ）其中env只是一个标记，而且dom C（σJ）= dom C（σ）。分离状态图G（STATE）的顶点和边的定义旨在确保存在一个图同态（4），该图同态将每个夏娃移动映射到代码转换，并将每个亚当移动映射到环境转换。图同态（4）使我们能够研究如何将被定义为G（MState）中的路径的执行轨迹tTracest=②p. 在这种情况下，我们使用以下术语：定义9.3我们说，标记图G（STATE）中的一条路p结合了当t=②p时，将图G（MState）的迹t分解为迹t∈Traces.请注意，路径p组合成轨迹t轨迹在夏娃和亚当移动之间交替，并且它以亚当移动开始和停止10分离游戏在本节中，我们将解释如何将每个跟踪tTraces与Eve和Adam交互的分离博弈SGame（t）相关联，并尝试通过将代码或环境提升到组合到t中的分离执行跟踪p来“证明”执行跟踪t中定义10.1（博弈）博弈A是一个三元组A =（棋盘A，PolA，局数A），它由一个图BoardA=（V，E，P0，P1）组成，图Board A =（V，E，P0，P1）具有源函数P0，P1：E → V，其边称为步数;由一个函数PolA：E → {−1，+1}组成，它将极性+1赋给Eve（博弈者）的每一步，将极性-1赋给Adam（对手）的每一步;由一个有限路径组成的预闭集局数A，称为博弈A的局数。此外，我们还要求游戏x1−e→1 x2−e→2···−→xn−→xn+1在PolA（e i）=（1）ifor1i n的意义上是交替的，并且它以亚当移动开始和停止。当存在对策s时，对策A中的顶点称为初始顶点播放A与x=100（s）作为源。博弈A的初始顶点集记为InitA。下面我们给出一个最一般、最自由的战略定义。特别是，这种意义上的策略不需要是确定性的。254P. - A. 梅利耶斯湖Stefanesco/Electronic Notes in Theoretical Computer Science 336（2018）241∈−∈∈→∈（Ⅲ）► 关于我们∈<$）.（Ⅲ）。定义10.2（策略）博弈的策略是一组预先封闭的策略。每一个执行轨迹tTraces都会引发一个博弈，这个博弈定义如下，称为与t相关的分离博弈，记为SGame（t）。定义10.3（分离博弈）博弈SGame（t）=（Board，Pol，Plays）被定义为图Board=G（SState），其中剧本中的剧本被定义为路径p： （σC，σ，σF）−→σ（σCJ，σJ，σFJ）在G（S状态）中组合成G（M状态）中②p： ②（σC，σ，σF）−→σ ②（σCJ，σJ，σFJ）跟 踪 的 前 缀 tTraces 。 移 动 的 极 性 Pol 是 从 分 离 状 态 的 图 形 Board = G（SState）的边缘的极性Eve（+1）和Adam（1）导出的。因此，分离博弈SGame（t） 在每一转变处m：（σ，L）（σJ，LJ）由执行轨迹t中的代码执行从机器状态（σ，L）=②（σ C，σ，σ F）开始，Eve必须走一步m：（σC，σ，σF）→（σCJ，σJ，σFJ），通过将机器状态（σ j，L j）in分解为单独的d状态（σ Cj，σ j，σ Fj）来“调整”转移。对称地，亚当与环境11可靠性定理在这个阶段，我们建立了并发分离逻辑的可靠性定理，通过将每个派生树解释为特定分离博弈中的获胜策略。我们假设给定一个Hoare三元组ΓPCQ.我们首先描述分离博弈SGame（t）的获胜条件，该分离博弈SGame（t）与C的操作语义中的执行轨迹t∈C相关联。定义11.1一个分离谓词是一个三元组P=（P，Γ，Q），它由两个谓词P和Q以及一个上下文Γ = r1：J1，. r k：可变资源的J k。第11.2章我写（σC，σ，σF）<$（P，Γ，Q）并说分离态（σ C，σ，σ F）满足分离谓词P=（P，Γ，Q），当σC<$P和σF<$Q且<$r∈dom（σ），σ（r）<$Δ（r）时。从现在开始，我们假设执行轨迹tC的长度为p，并引入序列P1，...，P2p+2的独立谓词，定义为：P1=（P，r，true） P1=（true，r，true）P2p+2=（Q，r，true）对于1

下载后可阅读完整内容，剩余1页未读，立即下载