并发分离逻辑中的精度与合取

可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）171-190www.elsevier.com/locate/entcs并发分离逻辑中的精度与合取Alexey Gotsmana Josh Berdineb Byron Cookb，cIMDEA软件学院b微软研究院伦敦玛丽女王大学摘要并发分离逻辑是一种霍尔逻辑，用于对通过锁同步的并发堆操作程序进行模块化推理。它通过将程序状态划分为线程本地部分和锁保护部分，并为后者分配资源不变量来实现模块化推理。令人惊讶的是，除非资源不变量是精确的，否则逻辑是不合理的，即，明确地在堆中划出一块区域。证明不合理性的反例涉及合取规则。 然而，到目前为止，它一直是一个悬而未决的问题，是否并发分离逻辑没有合取规则是健全的，当资源不变的限制被删除：所有公布的证明有精度限制烘烤。在本文中，我们提出了一个单一的证明，显示了不精确的资源不变量的逻辑的可靠性，但是没有合取规则，以及它的经典版本，其中需要资源不变量准确地说，并包括合取规则。我们的证明产生了一个精确和直接的公式关键词：分离逻辑，并发，精度，合取规则。1引言并发分离逻辑[12]是一种霍尔逻辑，用于对通过锁（又名互斥锁）同步的并发堆操作程序进行模块化推理它通过将变量和堆划分为几个不相交的部分来实现模块化推理：线程本地部分（每个线程一个，又名进程）和受保护部分（每个空闲锁一个，即， 不被任何线程持有的锁）。线程本地部分只能由相应的线程访问，而锁保护部分只有在线程持有锁时才能访问。当存在这样一个划分时，我们称该程序满足分离性原则.为了指定分区，逻辑将程序中的每个锁与一个断言（它的资源不变式）相关联，该断言描述它所保护的状态部分例如，一个资源不变式可能声明一个锁保护一个单链表，该表的头节点由一个特定的变量指向对于任何给定的线程，1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.021172A. Gotsman等人理论计算机科学电子笔记276（2011）171资源不变量限制其他线程如何改变受保护状态，因此允许独立地推理线程重要的是要注意，上面描述的状态划分不是的程序本身，但在逻辑中的证明，使模块化推理的并发干扰的存在。 此外，划分不需要是静态的，即，该逻辑允许在不同线程和锁所拥有的区域之间转移变量和堆单元的所有权。这样一种非标准的程序状态观使得程序状态的表述和证明的合理性逻辑上的困难。事实上，这个逻辑是由O'Hearn在2001年提出的这是因为，正如雷诺兹在逻辑发明后不久所展示的那样，除非资源不变量是精确的，否则它是不可靠的。非正式地，程序状态上的谓词是精确的，当它明确地划分出堆的一个区域时（见2.1节的正式定义）。例如，表示存储0的地址x处的单元格的分隔逻辑assertionx<$→0是精确的;然而，表示单元格或空堆的assertionx<$→0空堆不是精确的。反例中使用的证明不可靠性的关键规则是合取规则：{P1}C{Q1}► {P1<$P2}C{Q1<$Q2}该规则对于合并两个证明的结果很有用;例如，它被抽象解释中的约简积构造所使用[6]。O’Hearn has conjectured that the logic might be sound in the case when boththe restriction of precision and the conjunction rule are dropped [这个猜想的有效性问题例如，考虑以下两个列表段谓词的定义[15]，我们可以在资源不变式中使用：ls1（E，F）惠（E=Femp）惠（E = F emp）E<$→X<$ls1（X，F）<$E/=F）;l s2（E，F）惠（E=Femp）惠（FX. E<$→X<$ls2（X，F）），其中X被选择为新鲜的。后一种定义产生了不精确的断言：例如，由yX→Y和yZ描述的堆。X<$→YY<$→ZZ<$→Y满足ls2（X，Y）;只有前一个断言蕴含ls1（X，Y）。但是，ls2谓词验证了ls1没有验证的断言之间的某些蕴涵。 由于这个原因，基于分离逻辑的现代程序分析工具使用的是ls2[16]）。由于基于并发分离逻辑的自动工具通常建立在相应的顺序分析之上，因此这些工具经常推断不精确的资源不变量[3，9]。到目前为止，O'Hearn猜想是否正确仍然是一个悬而未决的问题产生不精确不变量A. Gotsman等人理论计算机科学电子笔记276（2011）171173已经被证明是直接相对于程序语义的声音[9]，或者依赖于猜想是真的[3]。在本文中，我们提出了一个单一的证明，显示了不精确的资源不变量的逻辑的可靠性，但没有合取规则，以及它的经典版本，其中资源不变量需要是精确的，并包括合取规则（定理4.1）。除了显示并发分离逻辑的可靠性之外，我们的证明还提供了一种语义分析，这种语义分析比以前提出的基于动作轨迹[2，4]或Petri网[11]的语义分析要基本得多我们使用语义证明的概念来实现这一点，语义证明用线程的本地状态描述来注释线程代码中的程序点（第4.1节）。与Hoare三元组的标准解释不同，语义证明方面的解释是相当有意的。三元组有效的定义并没有抽象出命令或证明的所有内部句法结构，而标准的解释仅仅是根据命令的外延意义和前置条件断言和后置条件断言给出的。这种有意定义的使用是承认，具有不精确资源不变量的合取规则的不合理性的直观原因关键在于证明，而不是命令的特别是，不精确的资源不变量允许合取规则的两个分支对如何划分状态做出有冲突的选择正是这些在证明的不同分支中对状态划分的不同选择导致了问题，但是所讨论的划分与命令的操作行为无关。以前的合理性证明的一个观点是，代替使用三元组的有意解释，它们用划分的操纵来仪表化命令的语义，以便即使用扩展解释也能暴露足够的有意细节。使用语义证明而不是工具化语义的一个关键结果是，分离属性可以直接公式化（引理4.2）为并发执行的不变量：对于程序中的给定点，线程的局部状态可以从它们的语义证明中确定。因此，不需要沿着执行轨迹跟踪变化的插装，并且可以避免先前将并发执行分解为组成顺序执行的交错的关键和困难步骤（Brookes从技术上讲，为了证明并发分离逻辑的可靠性，我们定义了程序中每个线程的线程本地解释作为语义证明。分离属性的形式化（引理4.2）将线程本地解释与标准的交织操作语义联系起来（第3节）。然后，我们定义了霍尔三元组对于关于这种解释的命令的有效性的概念，并证明了所有证明规则的可靠性（4.2节）。尽管没有跟踪状态的划分，线程本地解释足够强大，可以建立并发分离逻辑中程序的可证明性意味着程序是无数据竞争的（第5节）。174A. Gotsman等人理论计算机科学电子笔记276（2011）171n2并发分离逻辑本文考虑Calcagno等人[4]提出的并发分离逻辑。这个版本的逻辑是抽象的，因为它可以可以在具有给定结构的大量语义模型上进行解释，这允许在多个上下文中重用有关逻辑的结果。与任何霍尔逻辑一样，并发分离逻辑包括两个形式系统--一个用于断言，一个用于规范。我们首先讨论前者。2.1断言在抽象分离逻辑中，断言相对于表示程序状态的分离代数来解释。定义2.1（分离代数）分离代数是一个部分交换幺半群（ε，ε，ε），其单位元素ε ∈ε。 部分交换幺半群由单独组合的部分二元运算给出，其中单位、交换性和结合性定律对于相等成立，这意味着两边是有定义的且相等的，或者两边都是未定义的。在[4]中给出的分离代数的原始定义要求将运算是可消的：对于每个σ∈φ，部分函数σφ·：φ~φ必须是单射的。这个要求与验证合取规则的条件有关霍尔的逻辑我们在这里省略了它，因为我们也考虑了使规则无效的并发分离逻辑模型。本文用整环D来理解格（D，±，H，H，T，H）. 对于一个集合，设P（T）T是具有一个特殊元素T的T的子集的域。订单±在域P（π）T中是子集包含，其中T是最大元素，π是最小元素。当T表示程序状态时，我们通常使用T来表示错误状态，例如，这是由于解引用无效指针而导致的。注意，阶数±定义了域P（n）T上相应的连接H和满足H运算。如果p是一个分离代数，我们可以逐点地将p的运算提升到P（p）T：对所有p，q∈P（p）pq ={σ η |σ ∈ p，η ∈ q，定义σ <$η};T <$p=p<$T= T。因此，P（ε）T具有单位为e = { ε }的全交换幺半群结构。 对于分离代数n，我们称P（n）T为从代数n构造的分离域。我们用②表示P（π）T上的π的迭代形式：②k=1p k= e p1. 不规则的;Forσ∈T{T}w e表示为{|σ|}单例集{σ}，i fσ∈Σ，且T，i fσ=T。 Thus，{|σ|}∈P（n）T.分离代数Σ上的谓词p∈ P（Σ）是精确的，如果对于任何状态σ，至多存在一个子状态σ1满足p：σ=σ1<$σ2，对于某些σ2。如果这样的子状态存在，并且该运算是可消的，则子状态σ2是唯一的。A. Gotsman等人理论计算机科学电子笔记276（2011）171175（Ⅲ）分离代数和整环的元素通常使用部分函数来定义。我们使用以下符号：f（x）↑表示函数f在x上未定义，[]表示无定义函数。 我们用f [x：y]表示函数，该函数在任何地方都与f具有相同的值，除了x，它的值为y（即使f（x）↑）。下面是一个分离代数RAM的例子，通常用于关于堆操作程序的推理：值= Z变量={x，y，.. . }堆= Locs~finn值Locs=N堆= Vars~finn值RAM=堆×堆状态由堆栈和堆组成，这两个函数都是将变量或位置映射到其值的有限部分函数。为了简化演示，代数不包括权限[1，14]。我们还省略了逻辑变量;参见2.4节。这个运算形成了栈和堆的不相交的并集：（s1，h1）（s2，h2）=（s1s2，h1h2）。单元元素是一个空栈和空堆的状态：（[]，[]）。对于余项，我们固定一个分离代数（ε，ε）和相应的域P（ε）T。我们进一步假设一种断言语言，用于表示在ε上的谓词，包括具有预期解释的ε，ε，ε和ε连接词，断言emp仅表示空状态ε。重言式断言是那些意义是重复的断言。我们用P∈ P（n）表示断言P的意义。一个断言是精确的，如果它表示一个精确谓词。2.2原始命令和局部函数我们在本文中考虑的编程语言是由一组原始顺序命令PComm参数化。对于每一个C∈PComm，我们假设它的表示为fC：C→ P（C）T，它将每个预状态映射到通过执行C获得的状态。正如Calcagno等人[4]所示，为了使分离逻辑合理，编程语言的原语命令的转换器fC必须以相对于C中存在的结构的本地方式运行。下面的定义形式化了这个条件。定义2.2（局部函数）对于分离代数（ε，ε，ε），函数f：ε→P（ε）T是局部的，如果对于任何状态σ1，σ2∈ε，使得σ1<$σ2被定义，我们有f（σ1<$σ2）± f（σ1）<${σ2}.定义2.2是一种简洁的方式来表述分离逻辑的可靠性所依赖的两个条件：如果f：f→ P（f）T是命令C的含义，则（安全单调性）如果从状态σ1<$σ2执行C导致错误f（σ1<$σ2）=T，则从更小的状态σ1执行C也会产生错误：T±f（σ1）<${σ2}意味着f（σ1）=T;176A. Gotsman等人理论计算机科学电子笔记276（2011）171...（框架性质）如果从状态σ1执行C不会产生错误，则从更大的状态σ1<$σ2执行C具有相同的结果，并且使σ2不变：在这种情况下，我们通常有f（σ1<$σ2）=f（σ1）<${σ2}。局部性的要求排除了可以检查单元是否在堆中分配的命令，而例如，设f=RAM（见2.1节），考虑下面的函数f：RAM →P（RAM）T：f（s，h）={（s，hJ）}， 如果h（10）被定义;{（s，h）}，否则，其中hJ与h相同，除了它被定义为10。函数f定义了一个“命令”的含义，如果地址10处的单元被分配，则该命令将其处理，如果没有分配，则该命令将其作为空操作。 函数f不是局部的：取σ1=（[ ]，[ ]），σ2=（[ ]，[10：0]），则f（σ1<$σ2）=f（（[]，[]）<$（[]，[10：0]））=f（[]，[10：0]）={（[]，[]）}和f（σ1）<${σ2}=f（[]，[]）<${（[]，[10：0]）}={（[]，[]）}{（[]，[10：0]）}={（[]，[10：0]）}，因此，不等式f（σ1<$σ2）±f（σ1）<${σ2}不成立。函数f的点态提升： P→ P（P）T 至P（）T 是一个函数f：P（n）T→P（n）T定义如下：对所有p∈P（n）Tf（p）={f（σ）|σ∈ p}， 如果p= T;T，如果p=T。给定命令C∈PComm的表示fC：n→ P（n）T，我们可以将其提升为前向谓词TransformerfC：P（n）T→ P（n）T。我们注意到，所得到的Transformer分布在域P（N）T中的H和H操作上：p，q ∈ P（n）T. f C（p H q）= f C（p）H f C（q）;（1）p，q ∈ P（n）T. f C（p H q）= f C（p）H f C（q）.（二）此外，如果表示是局部的，则对于对应的Transformer，我们有：p，q ∈ P（n）T. f C（p <$q）± f C（p）<$q.当谓词Transformer满足这个属性时，我们说它是局部的典型的堆操作命令可以在代数上解释为：A. Gotsman等人理论计算机科学电子笔记276（2011）171177RAM来自第2.1节。我们在第5节中提到它们，在那里我们公式化并证明178A. Gotsman等人理论计算机科学电子笔记276（2011）171（）（）（）（2）（Ⅲ）（Ⅲ）（Ⅲ）skip，（s，h）~（s，h）x=E，（s[x：u]，h）~（s[x：E s[x：u]]，h）x=[E]，（s[x：u]，h[E s[x：u]：b]）~（s[x：b]，h[E s[x：u]：b]），[E]=F，（s，h[E s：u]）~ （s，h[E s：F s]）x=new，（s[x：u]，h）~（s[x：b]，h[b：w]），如果h（b）↑删除E，（s，h[<$E）s：u]）~ （s，h），ifh（<$E）s）↑假设（B），（s，h）~（s，h），如果<$B）s=真假设（B），（s，h）~if<$B）s=falseC，（s，h）~T， 否则图1.一、 原始命令RAMComm的转换关系。 T表示命令出错。 ~/用于表示命令不会出错，但会卡住。我们用E s∈值表示，B s∈ {true，false}堆栈s中表达式的值。并发分离逻辑的数据竞争自由定理。设E、F在整数表达式上的范围和B在布尔表达式上的范围：x ∈VarsE、F：：= NULL|X|E + F|......这是什么？B：：=E = F|B|......这是什么？我们考虑以下原始顺序命令的集合RAMCommRAMComm：：=跳过|X = E |x =[E]|[E]= F |x =新|删除E|假设（B）通常，方括号表示指针解引用。assume（B）命令充当程序状态空间的过滤器-在执行assume（B）之后，B被假定为真。我们使用图1所示的转换关系~：RAMComm×RAM×（RAM{T}）定义C∈RAMComm的表示fC：RAM→ P（RAM）T：对于所有σ∈RAMfC（σ）=.. {|σJ|个文件夹|C，σ~σJΣ.不难证明fC对每个C∈RAMComm是局部的[4]。在本文的其余部分中，我们假设命令C∈PComm的局部表示fC：f→P（f）T及其到谓词变换器的提升。2.3逻辑我们考虑并发分离逻辑[12]的一种变体，用于并发程序设计语言，其中程序由多个线程的并行组合组成A. Gotsman等人理论计算机科学电子笔记276（2011）171179使用锁（互斥锁）l1，...，我是同步的。程序S的语法如下：C：：= PComm|C; C|C + C|C|获取（l k）; C;释放（l k）S：：= C... CQC线程的代码可以包括来自PComm的原始顺序命令、顺序组合C;C、选择C+C、迭代C++和可用锁上的（语法范围的）关键区域。当PComm包含assume语句时，条件、循环和条件关键区域（CCR）的标准命令可以在我们的编程语言中定义如下：ifBthenC1elseC2=（assume（B）;C1）+（assume（<$B）;C2）whileBdoC=（assume（B）;C）;assume（<$B）当B做C时用l=获取（l）;假设（B）;C;释放（l）原始的并发分离逻辑还考虑了嵌套的并行组合和显式的锁声明。这里选择的程序的限制形式简化了形式的发展，并使基本思想更加明确。我们的结果已经扩展到动态分配的锁和动态创建的线程（参见[8]），它们是比锁声明和并行组合更通用的构造。并发分离逻辑的判断具有Ik{P}C{Q}的形式，其中C是线程代码中的命令，P和Q是描述线程的本地状态的断言，并且I是程序中所有锁的资源不变量Ik的向量直觉上，判断意味着，如果线程从满足P的初始局部状态开始执行C，那么它只访问状态的局部部分，遵守资源不变量I，并且只在满足Q的局部状态中终止。并发分离逻辑的证明规则总结在图2中。大多数规则都是来自霍尔逻辑的标准规则。我们有一个单一的公理，用于解释命令（PRIM），它允许任何前置和后置条件与该命令的谓词Transformer一致。对于C∈PComm的一组特定的状态和表示fC，这个公理可以专门化为几个语法版本，从而获得这里提出的抽象逻辑的具体实例[1，14，15]。合取规则（CONJ）用于合并两个证明的结果，而析取规则（DISJ）用于通过案例进行证明。框架规则（FRAME）规定，在更大的本地状态下执行命令不会改变其行为。锁在逻辑中的处理方式如下。当线程获取锁时，它接收满足锁的资源不变量（ACQUUIRE）的部分状态的所有权。在释放锁之前，线程必须重新建立相应的资源不变式。在锁被释放后，线程将放弃180A. Gotsman等人理论计算机科学电子笔记276（2011）171（2）fC（P）±QI<${P}C{Q}P轮辋I{P}C1{Q}I{Q}C2{R}SE qI{P}C1;C2{R}I{P}C1{Q}I{P}C2{Q}CHOI cEI={P}C1+C2{Q}I{P}C{P}I{P}C{P} 哦I{P1}C{Q1}I{P2}C{Q2}D是JI{P1 $>P2}C{Q1$>Q2}I{P1}C{Q1}I{P2}C{Q2}CONJI{P1 $>P2}C{Q1$>Q2}P1P2II{P1}C{Q1}IPCF框架I{PR}C{QR}CONSE q获取I{emp}acquire（lk）{Ik}释放I{Ik}释放（lk）{emp}I{P1} C1{Q1}.. .I{P n}C n{Q n}P AR我... P n} C1 C n{Q1 Q n}图二.并发分离逻辑资源不变量（resource invariant，RELEASE）。注意，我们可以通过在框架规则下关闭它们来获得公理ACQUUIRE和RELEASEI{P}获取（lk）{PIk}I{PIk}释放（lk）{P}最后，PAR规则将关于几个线程的判断组合成对整个程序的形式I{P}S{Q}的判断。2.4逻辑变量在程序证明中，我们经常需要使用所谓的逻辑（也称为幽灵）变量，它们出现在断言中，但不在程序中。我们现在展示如何用证明规则来扩展逻辑，以操作这些变量。让我们固定一组整数逻辑变量LVars ={X，Y，. . . }并让Ints =A. Gotsman等人理论计算机科学电子笔记276（2011）171181→LVarsZ是他们的解释的集合。我们说一个分离代数是一个有逻辑变量的代数，如果对于某个分离代数<$J，我们有<$i =<$J× Ints，并且<$i上的<$i运算定义如下：（σ1，i1）<$（σ2，i2）=（σ1<$σ2，i1），如果i1=i2，则为unfined，否则。例如，对于在2.1节中定义的分离代数RAM，令RAMJ=RAM×Ints，其中RAM上的取整操作如上所述提升到RAMJ则RAMJ是一个带逻辑变量的分离代数。给定一个函数f：J→ P（J）T在没有逻辑变量的基础代数上，我们可以将它提升为一个函数f：j→ P（j）T在有逻辑变量的代数上，如下所示：f（σ，i）=.f（σ）×{i}，若f（σ）T;T，如果f（σ）= T.设A是一个带有逻辑变量的代数，并假设一个断言语言带有逻辑变量上的量化器：P：：=.. | ∃X. P|第十章P满足关系定义如下：（σ，i）|= 10X。 我会的 （σ，i [X：u]）|= P（σ，i）|= 10X。我会的（σ，i [X：u]）|= P当定义原始顺序命令语义的函数fC从底层代数上的函数中提取出来而没有逻辑变量时，我们可以用以下两个证明规则来扩展并发分离逻辑，用于操作逻辑变量：I{P}C{Q}E存在我...P} C {\displaystyle{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000} P} C{\displaystyle{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000} P} C{\4cH000000} Q}I{P}C{Q}FORALL我... P}C {\displaystyle{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000} P} C {\displaystyle{\cHFFFFFF}{\3cH2F2F2F}{\4cH000000} P} C {\4cH000000} Q}3编程语言和语义我们现在定义简单的操作语义，我们证明了可靠性。从现在开始，我们固定一个程序S = C1…在我们的并发编程语言中，Cn由n个线程C1，...，C n使用m个锁l1，...，我是同步的。从程序设计语言的特定语法中抽象出来，用控制流图（CFG）表示程序中182A. Gotsman等人理论计算机科学电子笔记276（2011）171的每个线程，在技术上是方便的。CFG被定义为元组（N，T，start，end），其中N是程序点的集合，TN×Comm×N是控制流关系，并且开始和结束A. Gotsman等人理论计算机科学电子笔记276（2011）171183N=k=1是区分的初始和最终程序点。CFG中的边缘用来自集合Comm的命令标记，该集合Comm由原始顺序命令PComm、锁定获取获取（lk）和释放释放（lk）组成我们假设，不失一般性，控制流关系没有导致开始或结束的边。我们注意到，我们语言中的线程代码可以以标准的方式转换为CFG。即，假设原始顺序命令的集合PComm包括跳过语句。然后，命令C的CFG通过其语法的归纳构造如下：(i) 原始命令C∈PComm具有CFG（{start，end}，{（start，C，end）}，start，end）.(ii) 假设C1和C2有CFG（N1，T1，start1，end1）和（N2，T2，start2，end2），（3）。那么C1，C2有CFG（N1<$N2，T1<$T2<${（end1，skip，start2）}，start1，end2）.(iii) 假设C1和C2具有CFG（3）。 则C1+C2具有CFG（N1<$N2<${start，end}，T1<$T2<${（start，skip，start1），（start，skip，start2），（end1，skip，end），（end2，skip，end）}，start，end）.(iv) 假设C有一个CFG（N，T，start，end）。 然后C有CFG（N {startJ，endJ}，T {（startJ，skip，start），（end，skip，start），（end，skip，endJ）}，startJ，endJ）.因此，让我们用它的CFG（Nk，Tk，startk，endk）来表示S中的每个线程Ck让nk=1 Nk和T=nTk是程序点的集合，程序S的关系。程序S的交错操作语义由转换关系→S定义，该转换关系转换程序计数器对（由从线程标识符到程序点的映射表示）和程序状态：-S：（（{1，.，n}→N）× N）×（（{1，.，n}→N）×（n{T}））。请注意，由于在我们的编程语言中，由获取和释放命令形成的关键区域在语法上是有作用域的，因此我们可以确定集合Free（pc）{1，...， m}的索引的自由锁在每个程序计数器pc ∈{1，.， n} → N，即，不被任何线程持有的一组锁 再-184A. Gotsman等人理论计算机科学电子笔记276（2011）171lation→S由图3中的规则定义。语义执行命令A. Gotsman等人理论计算机科学电子笔记276（2011）171185.∈∗.∈∗（v，C，vJ）∈T C∈PCommfC（σ）/=TσJ∈fC（σ）pc[k：v]，σ→Spc[k：vJ]，σJ（v，release（lj），vJ）∈Tpc[k：v]，σ→Spc[k：vJ]，σ（v，C，vJ）∈T C∈PComm fC（σ）=Tpc[k：v]，σ→Spc[k：vJ]，T（v，acquire（lj），vJ）∈Tj∈Free（pc[k：v]）pc[k：v]，σ→Spc[k：vJ]，σ图三. 操作语义从PComm原子地。还要注意，根据我们的语义，一个线程如果两次试图获取同一个锁，就会被卡住。让我们用pc0表示初始程序计数器[1：start1]. [n：startn]和pcf的最后一个[1：end1]... [n：endn].我们说程序S从n个初始状态σ0∈φ运行时是安全的，如果对于某个程序计数器pc，pc0，σ0→φSpc，T不是这样.4可靠性证明本节的目的是证明下面的定理，说明2.3节中提出的逻辑的可靠性。定理4.1（可靠性）假设I<${P}S{Q}，其中• I中的资源不变量是精确的，并且所述递归操作是可取消的;或者• C ONJ不用于三元组的推导。则对于任何σ0∈ε，使得σ0P②mk=1（4）第（1）款所指的是：当从σ0，ndifpc0，σ0→φSpcf，σ运行时，programS是安全，我们有σQ②mk=1I k）（五）4.1线程局部解释与分离性语义证明被定义为三元组（C，G，I），其中• C是具有CFG（ N，T，start，end）的命令;• G： N→ P（N）将 C语言的程序点映射到语义标注;• I ∈（P（n））m是资源不变表示Ik∈ P（n）的向量，k=1. m使得对所有边（v，CJ，vJ）∈T186A. Gotsman等人理论计算机科学电子笔记276（2011）171免费k=10k=1KKk∈{1，...，m}K• 如果CJ∈PComm，则• 如果CJ 被获取（lk），则• 如果CJ被释放（lk），则fC′（G（v））±G（vJ）;（6）G（v）<$Ik<$G（vJ）;（7）G（v）<$G（vJ）<$Ik.（八）请注意，在该定义中，由语义注释映射G分配给程序点的P（n）的元素类似于非结构化控制流证明系统中的标签不变量[7]。 不等式（6）、（7）和（8）分别是公理PRIM和ACQUUIRE和RELEASE的全局版本的语义对应。 命令的线程本地解释由其语义证明给出。在第4.2节我们展示了如何从并发分离逻辑中的语法证明中提取程序中线程的语义证明。正如我们在第1节中所解释的，我们的可靠性证明的核心包括建立分离属性[12]：在任何时候，程序的状态都可以划分为每个线程和每个空闲锁所拥有的状态。下面的引理形式化了线程的局部状态由它们的语义证明定义的情况下的属性。这在我们的线程本地解释和第3节的操作语义之间建立了对应。引理4.2（分离性质）假设语义证明（C k，G k，I），k= 1. n.如果σ0∈Σ，{σ} ±.②nG（st art）为零。②I型，（9）那么，每当pc0，σ0→<$S pc，σ，我们有{|σ|}±。②nG（pc（k））≠0。②Kk∈（pc）我知道。（十）证明我们证明了该定理的陈述通过归纳σ在程序S的操作语义中的导子的长度。在基本情况下，（10）等于（9）。现在假设pc0，σ0→Spc[j：v]， σ→Spc[j：vJ]，σJ.则对于某个原子命令C∈Comm，（v，C，vJ）∈T。 我们必须证明如果然后{σ} ±.②n{|σJ|}±。②nk=1A. Gotsman等人理论计算机科学电子笔记276（2011）171187免费（pcGk（（pc[j：v]）（k））{\displaystyle{\frac{j：v}k∈②[j：v]）Ik，（11）G k（（pc [j：vJ]）（k））②Ik.（十二）k=1k∈Free（pc[j：v′]）有三种情况对应于命令C的类型。188A. Gotsman等人理论计算机科学电子笔记276（2011）171（Ⅲ）（2）案例1. C∈ PComm. 在这种情况下，Free（pc[j：v]）=Free（pc[j：vJ]）。让r=.1②n，Gk（pc（k））≠0。k②Ik，（13）≤k ≤ ∈Wk/=j其中W=Free（pc[j：v]）=Free（pc[j：vJ]）。然后{|σJ|}±fC（{σ}）→S的定义±fC（Gj（v）r）（11）±fC（Gj（v））<$r fC是局部的±Gj（vJ）r（6）案例2.C是acquire（l i）。 在这种情况下，i ∈ Free（pc [j：v]）和i/∈ Free（pc [j：vJ]）。设r由（13）定义，其中W=Free（pc[j：v]）\{i}=Free（pc[j：vJ]）。然后{|σJ|}={σ}→S的定义±Gj（v）Iir（11）±Gj（vJ）r（7）案例3. C是释放（I i）。 在这种情况下，i/∈ Free（pc [j：v]）和i ∈ Free（pc [j：vJ]）。设r由（13）定义，其中W=Free（pc[j：v]）=Free（pc[j：vJ]）\{i}。然后{|σJ|}={σ}→S的定义±Gj（v）r（11）±Gj（vJ）Iir（8）在所有情况下，我们得到等价于（12）的不等式，从而完成归纳。Q4.2关于螺纹局部解释为了证明定理4.1，我们首先定义了霍尔三元组关于4.1节的线程局部解释的有效性概念，并证明了在这种解释中证明规则的可靠性。逻辑关于具体语义的可靠性则是引理4.2的直接结果。定义4.3如果存在一个语义证明（C，G，I）使得G（start）=P和G（end）<$Q，我们写I <${ P } C { Q }，其中start和end是C的CFG的起始和最终程序点。我们说，如果一个推理规则保持了判断的有效性（如上述关系式所定义A. Gotsman等人理论计算机科学电子笔记276（2011）171189的），那么它对于190A. Gotsman等人理论计算机科学电子笔记276（2011）171（2）（2）（Ⅲ）（Ⅲ）∈（2）（）（）引理4.4PRIM、ACQUUIRE、RELEASE、SE q、CHOI cE、LOOP和CONSE qare声音相对于线程本地解释。为了说明，我们考虑这个简单引理的情况PRIM和SE q，并省略其他情况。好的。 考虑公理PRIM的应用I{P}C{Q}，哪里 C∈PComm.然后 fC（P）±Q.根据 到 该encod-从第3节开始将命令转换为CFG，命令C具有CFG（{start，end}，{（start，C，end）}，start，end）。设G（start）=P，G（end）=Q，则fC（G（start））±G（end）.因此，（G，C，I）是一个语义证明，而I是一个语义证明。{P}C{Q}（根据需要）。S E q。 假设I <${P} C1{Q}和I <${Q} C2{R}。 设C1和C2的CFG分别为（N1，T1，start1，end1）和（N2，T2，start2，end2）。 则C1; C2具有CFG（N1{（end1，skip，start2）}，start1，end2）。存在语义证明（C1，G1，I）和（C2，G2，I），使得G1（开始1）= P、G1（末1）Q，G2（开始2）= Q，G2（end2）设G（v）= G1（v），其中v∈N1; G（v）= G2（v），其中v∈N2.我们有fskip（G1（end2））±G2（st art1）.（G，（C1; C2），I）是的语义推广，且I ∈ {P} C1; C2{R}.Q现在我们继续证明规则FRAME、DISJ和CONJ的可靠性。 为此，我们表明，我们可以构造语义证明这些规则的结论，从语义证明他们的推理。这本质上是证明这些规则在包括全局获取和释放公理的逻辑中是可接受的语义对应物，即，使用这些规则的派生可以转换为不使用它们的派生通过在我们的证明系统中使用语义证明而不是推导，我们避免了在我们的编程语言中处理逻辑和控制流构造中的证明规则的语法形式。引理4.5（i）对于任意r∈P（n），如果（C，G，I）是语义证明，则（C，GJ，I），其中，Gj（v）= G（v）<$r.(ii) 如果（C，G1，I）和（C，G2，I）是语义证明，则（C，GJ，I）也是，其中别客气。 Gj（v）= G1（v）<$G2（v）.(iii) 如果（C，G1，I）和（C，G2，I）是语义证明，则（C，GJ，I）也是，其中别客气。Gj（v）= G1（v）<$G2（v），假设I中的资源不变表示是精确的，并且该迭代操作是可取消的。证明考虑命令C的CFG中的边（v，CJ，vJ）。 当CJPComm时，新语义注释Gj的不等式（6）由谓词Transformer f C′是局部的并且分布在H和H上的事实得出。 后者通过构造由逐点提升定义的变换器而成立，见（1）和（2）。我们省略了当CJ是acquire（lk）时的简单情况。现在假设CJ是release（l k）。我们依次考虑引理的每一种情况。