并发分离逻辑的修正史

可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）5-28www.elsevier.com/locate/entcs并发分离逻辑的修正史斯蒂芬·布鲁克斯美国匹兹堡卡内基梅隆大学计算机科学系摘要并发分离逻辑（Concurrent Separation Logic）是一种资源敏感的逻辑，它将分离逻辑与Owicki-Gries推理规则相结合，以Peter O 'Hearn提出的方式实现共享可变状态的并发程序的无故障部分正确性。Owicki-Gries规则和O 'Hearn的原始逻辑缺乏组合性，仅限于具有严格并行结构的程序，因为“没有其他过程修改”某些变量的关键约束，作为条件临界推理规则的附带条件而强加。卡尔地区。在以前的工作中，我们提出了一个更一般的制定使用资源上下文的并发分离逻辑，我们oerarched一个合理性证明的基础上的跟踪语义。最近，Ian WehrmanJosh Berdine发现了一个例子，表明这种可靠性证明依赖于一个隐藏的假设，相当于“没有并发修改”，因此所提出的逻辑也只适用于刚性程序。在这里，我们表明，通过自然和简单的调整，我们可以避免这个问题。其关键思想是用一个“依赖集”的变量来增加每个断言，假设这些变量不被其他过程修改，并调整推理规则来验证和利用这些假设。这个修改的并发分离逻辑是组合的，允许刚性和非刚性程序，并且依赖集需求所施加的额外约束确保了可靠性。同时，我们放松了Owicki-Gries约束，关键变量的使用，允许变量受到多个资源的保护，并在逻辑中构建一个更简单，但更通用的保护规则。在修改后的逻辑中，想要写入共享变量的进程必须获得保护它的所有资源，而想要读取共享变量的进程只需要获得一个这样的资源。 这种概括使并发分离逻辑在精神上更加接近到基于许可的逻辑，其中进程可以被允许执行并发读取。保留字：并发，共享内存，指称语义，资源，分离逻辑1引言并发分离逻辑（CSL）是一种资源敏感逻辑，用于推理共享内存并发程序的无故障部分正确性。CSL将分离逻辑（最初由John Reynolds在[10]中引入，用于对顺序指针程序进行推理）与用于无指针共享内存程序的Owicki-Gries规则[7]结合起来，其方式由Peter O 'Hearn [ 6 ]提出Owicki-Gries和1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.0136S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5在之前的工作中，我们使用资源上下文制定了一个更通用的并发分离逻辑[3]，试图避免这些限制，并且我们使用基于跟踪的指称语义给出了可靠性证明这一发展的一个主要特征最近，Ian Wehrman和Josh Berdine发现了一个反例[12]，表明这种可靠性证明做出了一个隐藏的假设，相当于我们在这里表明，通过对先前公式的系统性自然调整，我们可以开发一个完全组合的并发分离逻辑，以避免这个问题。关键思想是用一个“依赖集”来增加CSL的断言通过使这个集合成为断言的一个组成部分，我们避免了对非组合副条件的需要;我们能够正确地解释假设并保证进程以纯粹的语法导向方式对共享变量进行修改。与此同时，我们放松了Owicki-Gries对使用关键变量的限制，允许变量受到多个资源的保护，并在逻辑中构建一个更简单，更通用的保护规则。这使得并发分离逻辑在精神上更接近基于权限的逻辑，其中可以允许进程执行并发读取[1，2]。再次使用动作跟踪语义，我们勾勒出修改后的逻辑的合理性证明，这一次没有隐藏的假设，不需要严格的程序结构。我们给出了一系列的例子，解决Wehrman我们打算用这里提出的修正和扩充的逻辑来代替原来的逻辑我们假设熟悉分离逻辑，如雷诺兹[10]所定义的。2语法我们的编程语言的语法（如[3]）由以下抽象语法给出，其中c在命令集Com上的范围c：：=跳过|i：= e|i：=[e]|[e]：= eJ|i：= consE|处置|c1; c2|如果b那么c1否则c2|而b做c|当b做c时，|c1-c2令e、b分别在整数表达式和布尔表达式上取值，并且E在形式为[e1，...，en]。表达式是纯粹的，即与堆无关。我们在语法上区分表示整数变量的标识符（i∈IdeS. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）57表和资源名（r∈Res），它们的行为类似于二进制信号量，在语义上表示为整数变量，其值被限制为0或1。设free（c）Ide是在c中有自由出现的标识符的集合，mod（c）是有自由写出现的标识符的集合，res（c）Res是在c中有自由出现的资源名称的集合。这些都像往常一样，由结构归纳法来定义比如说，free（i：=e）=free（e）{i}free（c1;c2）=free（c1c2）=free（c1）free（c2）free（当b做c时有r）=free（b）free（c）free（c中的资源r）=free（c）res（i：=e）={}res（c1;c2）=res（c1<$c2）=res（c1）<$res（c2）res（当b做c时有r）=res（c）<${r}res（c中的资源r）=res（c）−{r}mod（i：=e）=mod（i：=consE）=mod（i：=[e]）={i}mod（[e]：=eJ）=mod（disposee）={}mod（c1;c2）=mod（c1<$c2）=mod（c1）<$mod（c2）mod（withrwhenbdoc）=mod（c）mod（resourcerinc）=mod（c）3断言与Owicki-Gries [7]中一样，我们将每个资源名称r与“受保护变量”和“资源不变量”R[ 5 ]的集合X_ID在与[3]中一样，我们没有假设资源不变量和保护集的固定选择，而是扩展了部分正确性断言的语法以包括资源上下文Γ。我们放宽了Owicki-Gries，O'Hearn和原始并发分离逻辑[ 3 ]的权限规则在[3]中，我们要求资源不变量是精确的[10]。一个分离逻辑公式R是精确的，对于所有的存储器s和堆h，最多有一个子堆hJ<$h，使得（s，hJ）|= R.定义3.1格式良好的资源上下文Γ具有以下形式r1（X1）：R1，.，rn（Xn）：Rn8S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5其中r1，.， rn是不同的资源名称，X1，...， Xn是标识符的集合，每个Ri是精确的，并且对于每个i，自由（Ri）<$Xi。当r（X）：R在Γ中且x∈X时，我们说r在Γ中保护x。让拥有（r）=ni=1 Xi，ndinv（r）=R1·· ·<$Rn. Letdo m（r）be{r1， . ，rn}。Welet（r，r（X）：R）是通过用r（X）：R扩充Γ而形成的上下文，只要这是良构的。定义3.2断言有形式ΓA{p}c{q}其中A是一组标识符，我们称之为依赖集。前置和后置条件p和q以及Γ中的资源不变量没有提到资源名称。这样的断言是格式良好的i r是格式良好的上下文，free（p，q）A，free（c）owned（r）A。在一个格式良好的断言中，前置条件和后置条件可能会提到资源拥有的标识符，但前提是它们也属于依赖集A;命令c可能使用资源拥有的变量或属于依赖集的变量。推理规则（稍后将介绍）将约束如何以及在何处C被允许读取和写入这些变量：具体地，C只能写入在命名为R的临界区域内的受R保护的变量;并且受保护的变量的读取必须在临界区内，除非该变量属于依赖集。规则（在依赖集中）跟踪证明中使用的变量（在临界区域之外）：这些变量不能被任何其他过程修改，并且该约束作为并行规则的附带条件强制执行。我们修改后的逻辑实际上强制执行以下保护机制：在c中对受保护变量的每一次写入都必须在（嵌套的）命名保护它的所有资源的临界区域内;在c中对受保护变量的每一次读取都必须在命名保护它的某些资源的临界区域内。在保护集成对不相交的特殊情况下，这与通常的Owicki-Gries原则相一致：对受保护变量的读取或写入必须在命名（唯一的）保护资源的临界区域内。4有效性甚至在我们介绍编程语言的语义模型之前，我们就可以提供一个直观的特征，说明断言想要表达的关于程序行为的内容。断言表达了在适当约束的环境中对程序行为的当与其行为被假定为如所指定的那样表现的其他过程同时执行定义4.1断言ΓA{p}c{q}在c的每一个有限交互计算中有效，从满足pinv（Γ）的状态（具有Γ，A中所有变量的值）开始，在遵守Γ且不修改A中的变量的环境中，是无故障的，遵守Γ，并且在满足qinv（Γ）的状态中结束。S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）59Γ，A一尊重Γ意味着遵守由Γ隐含的保护机制，并（分别）保存每个资源不变式无故障意味着没有运行时错误（如悬空指针），也没有涉及并发写入共享变量或堆的竞争条件。这种有效性的概念将在后面通过动作轨迹语义和“局部使能”关系− − λ →进行形式化，在前面[ 3 ]中定义为e x c ep t t h a t w e只允许不修改依赖集合A中变量的“环境”移动。ΓA{p}c{q}的有效性意味着当c与a隔离执行时，状态满足pinv（Γ），则执行是无故障的，如果它终止最终状态满足qinv（Γ）。这是因为空虚的环境空虚地尊重它不修改任何变量。因此，通常的口号是可证明的程序是安全的。5推理规则我们的修改逻辑的推理规则是从原来的CSL [3]通过增加依赖集，并放松对使用保护变量的限制。我们只允许规则的良构实例，所以每个可证明的公式都是良构的，如上所述。• S基普• 一个任务Γα{p}跳过{p}如果空闲（p）A如果i∈Γ{[e/i]p}i：=e{p}• SE QUEN CE拥有的（Γ），自由的（e）• CONION• 哦<$A1{p1}c1{p2}<$A2{p2}c2{p3}ΓA1<$A2{p1}c1;c2{p3}b}c2{q}Γ <$A1<$A2{p}ifbthenc1elsec2{q}ΓA{p<$b}c{p}当b做c{pb}时，• 帕雷什<$A1{p1}c1{q1}<$A2{p2}c2{q2}如果mod（c）=A=mod（c）A关于我们Γ►A1∪A2 {p1<$p2}c1<$c2{q1<$q2}1 2 2 1• CRITI cALREGIONΓ<$A<$X{（p<$b）<$R}c{q<$R}r，r（X）：R<$A{p}，其中r当b做c{q}时10S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5一• LO cALRESOUR cE• 重新命名Γ，r（X）：R<$A{p}c{q}r∈A∈X{p∈R}资源r在c{q∈R}中• 洛库普在[rJ/r]c{q}中的r{p}资源r如果rJres（c）Γ<${[eJ/i]p<$e<$→eJ}i：=[e]{p<$e<$→eJ}如果i∈• 更新free（e，eJ），i拥有（r）• ALLOcATIONΓA{e <$→−}[e]：=eJ{e<$→eJ}如果我ΓA{emp}i：=cons（E）{i<$→E}• DISOLATEfree（E），i∈拥有（r）• 框架Γ<$A{e→ −}disposee{emp}ΓA{p}c{q}Γ<$A无约束（R）{p<$R}c{q<$R}• CONSEQUEN cE如果mod（c）无约束（R）={}• 一个辅助的ΓA{p}c{q}ΓA′{pJ}c{qJ}如果A<$AJ，pJ<$p，q<$qJΓ<$A<$X{p}c{q}ΓA{p}c\X{q}如果X对c是辅助的，则X是自由的（p，q）={}，X是拥有的（Γ）={}• CONJUN cTION评注<$A1{p1}c1{q1}<$A2{p2}c2{q2}ΓA1<$A2{p1<$p2}c{q1<$q2}我们对边条件和由well-formedness要求产生的（大部分是隐式的）随机方案提供了一S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）511些直觉和解释。• Skip：free（p）A确保良构的附带条件。12S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5• 赋值：允许读取属于依赖集A的标识符;仅允许如果i∈owned（Γ），则写入i良构性意味着i∈A。• 序列：依赖集A1→A2包含中间条件的自由变量p2，不只是前置条件和后置条件。• 条件循环：良构性意味着free（b）{\displaystyle free（b）}{\displaystyle free（b）}{\displaystyle free（b）}A。• 并行：c1依赖于它的环境来修改A 1中的变量，因此副条件mod（c2）<$A1={};类似地，c2和mod（c1）<$A2={}。假设Γ A1{p1}c1{q1}和Γ A2 {p2}c2{q2}是良构的，并且边条件成立。 然后free（p1，q1）A1和free（p2，q2）A2，所以mod（c1）free（p2，q2）={}和mod（c2）free（p1，q1）={}，如Owicki-Gries。我们也有free（c1）non-owned（Γ）即mod（c1）free（c2）owned（Γ）和mod（c2）free（c1）owned（Γ），如Owicki-Gries。依赖集A1包括在证明c1时使用的变量（在临界区域之外），同样对于A2和c2也是如此，所以我们在这里对相关变量强制执行在这里这样做是很自然的，因为这毕竟是并发进程的推理规则。• 临界区域：前提依赖于AX，因为r的互斥意味着没有并发进程可以触及X中的变量。在结论中，不需要在依赖集中包含受保护的变量，尽管这是允许的。如果前提是良构的，结论也是良构的• 局部资源：结论依赖于AX，它确保了良构性，因为free（R）X通过前提的良构性来保证• 更新、重命名、分配、处置：和以前一样的公理，带有附加条件以确保良构性。• Frame：和以前一样，c不能写任何在R中自由出现的变量。没有必要坚持free（R）_denowned（r）={}（如在原始CSL公式中），因为允许前置和后置条件提及受保护的变量;相反，我们将在R中自由出现的变量添加到依赖集，反映了没有并发过程修改这些变量的假设。• 结果：和往常一样，除了我们还允许加强依赖集。如果ΓA{p}c{q}是有效的，并且AAJ，则ΓA′{p}c{q}也是有效的，因为它表示c的不太一般的语义属性，在更受约束的可能环境集合上量化。• Auxiliary：一个变量集合X对于c是辅助的，如果来自X的变量在c中的每个自由出现都在一个赋值中，其目标标识符也属于X。辅助变量在前置或后置条件中不能自由出现的要求是标准的;它们不出现在保护列表中也是至关重要的。• 合取：正如John Reynolds所指出的，资源不变量的精确性对于显示这条规则的合理性至关重要。当R是精确的时，对于所有的p1和p2，我们有（p1<$p2）<$R惠（p1<$R）<$（p2<$R）。S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5136示例我们现在讨论一些示例程序和断言，以说明推理规则的工作方式，并将新CSL与原始CSL进行对比示例(i) 及（ii）解决Wehrman及Berdine提出的问题。我们采用这样的约定，当free（R）=X时，我们可以从r（X）：R中省略X，而只写r：R，因为这会导致更简洁的断言。(i) 的断言(a)r：x=aemp{a，t}{emp}，其中rdot：=x{t=aemp}(b)r：x=aemp{a，t}{t=aemp}，其中rdox：=t{emp}都是有效且格式良好的。每一个都可以从区域中证明，首先证明了►{a，t，x}{x=aemp}t：=x{t=aemp}，►{a，t，x}{t=ax=aemp}x：=t{x=aemp}由ASIGN和CONSEQUEN cE. 然而，断言（aJ）r：x=aemp{t}{emp}，其中rdot：=x{t=aemp}（bJ） r：x=aemp{t}{t=aemp}，其中rdox：=t{emp}是无效的（而且不是格式良好的），也不能证明。设c1为，其中r为t：=x;其中r为x：=t。 的断言(c)r：x=aemp{a，t}{emp}c1{emp}是有效的，格式良好的，并可从（a）和（b）使用SE qUEN cE证明。但是，（cJ）r：x=aemp{t}{emp}c1{emp}是一个不好的，不好的。(ii) 设c1如上所述，c2满足rdo（x：=x+ 1;a：=a+ 1）. 没有一个标识符集合A，r：x=aempA{emp}c1c2{emp}是有效的。事实上，即使对于最严格的依赖集A={x，a，t}，断言也是无效的：在没有干扰的情况下执行c1c2并不一定保持x和a的相等。此外，也不存在可证明此断言的集合A，因为A需要表示为A1A2，r：x=aempA1{emp}c1{emp}14S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5和r：x=aempA2{emp}c2{emp}是可以证明的 其中第一个需要一个中间条件，其中提到（t和）x或a，所以A1必须包含x或a。但是c2修改了这两个变量，所以平行规则的附加条件将失败。这个例子，没有依赖集，是由Wehrman和Berdine发现的，他们表明，r：x=aemp{emp}c1c2{emp}在原始并发分离逻辑中是可证明的，但不是有效的（关于CSL中使用的有效性概念）。上述分析表明， 使用依赖集避免了这个问题。(iii) 的断言r：x=a+bemp{a}{a=0emp}其中rdo（x：=x+1;a：=a+1）{a= 1emp}是有效的，并且可以从区域和条件中证明，因为►{x，a，b}{x=a+b<$a= 0<$emp}x：=x+ 1;a：=a+1{x=a+ba= 1emp}可从SE qUEN cE、ASASSIGNMENT和CONSE qUEN cE证明。同样我们可以证明r：x=a+bemp{b}{b=0emp}其中rdo（x：=x+1;b：=b+1）{b = 1 emp}。然后，使用伪随机数和逆量子数，我们可以导出r：x=a+bemp{a，b}{a=0b=0emp}其中rdo（x：=x+1;a：=a+1）其中rdo（x：=x+1;b：=b+1）{a = 1 b = 1 emp}。S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）515这种说法也是有道理的。使用RESOURcE规则和CONSEQUENcE，然后我们得到►{a，b，x}{a= 0<$b = 0<$x =a+b<$emp}资源rin其中rdo（x：=x+1;a：=a+1）{\displaystylerdo（x：=x+1;b：=b+1）}{a = 1 b = 1 x = a + b emp}。通过SE qUEN cE、ASIGNMENT和CONSE qUEN cE，我们就有►{a，b，x}{x=0emp}a：=0;b：=0;资源rin其中rdo（x：=x+1;a：=a+1）{\displaystylerdo（x：=x+1;b：=b+1）}{x = 2 emp}。最后，由于{a，b}是这个程序的辅助变量集，并且a，b不出现在前置或后置条件中，我们可以使用辅助规则来获得►{x}{x= 0emp}资源rinwithrdox：=x+ 1withrdox：=x+1{x = 2 emp}。(iv) 我们重新审视除了插入依赖集之外，该示例设R为（full= 1），−）（full=0emp）. 设PUT和GET为命令放：： whenfull= 0do（z：=x;full：=1）得到：： 当full = 1 do（y：= z; full：=0）时使用buf。的断言buf（z，ful ll）：R<${x}{x→−}PUT{emp}buf（z，ful ll）：R{y}{emp}GET{y <$→−}是有效的和可证明的。同样地，16S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5buf（z，ful ll）：返回{y}{emp}（GET;disposey）{emp}S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）517∗ ∧ ›→ ∨ ∧›→是可以证明的，buf（z，fu l ll）：R<${x，y}{x→<$−}PUT<$（GET;disposey）{emp}.现在设RJ为（full= 1<$z <$→ −）<$（full= 0<$emp）。 的断言buf（z，ful ll）：RJ<${x}{x→−}PUT{x→−}buf（z，ful ll）：RJ{y}{emp}GET{emp}是有效的和可证明的。类似地buf（z，ful ll）：RJ<${x}{x<$→−}（PUT;disposex）{emp}是可以证明的，buf（z，fu ll）：RJ<${x，y}{x<$→−}（PUT;disposex）<$GET{emp}.(v) 的断言如果rdo（x：=x+1; y：= y+1）{ emp }，则r：x = yemp {} {emp}有效。 显然，{y}是这里命令的辅助。的断言r：x=yemp{}{emp}，其中rdo（x：=x+1）{emp}显然是无效的。这表明，如前所述，要求辅助变量不得出现在资源不变量中的附带条件是至关重要的(vi) 设c1和c2为：c1：：withr1do（（withr2doa：=1）;[42]：=1）c2：：withr2do（（withr1doa：=2）;[42]：=2）.设R1和R2为断言R1：：（a= 1<$42<$→ 1）<$（a= 2<$emp）R2：：（a = 1 <$emp）<$（a = 2 <$42 <$→ 2）.注意，R1R2等价于（a= 1 42 1）（a= 2 42 2）。以下断言是可证明的：（a）<${a}{R1<$R2}a：=1 {（42 <$→ a = 1）（b）r2（a）：R2<${a}{R1}，其中r2doa：=1 {42 <$→{1}（c）r2（a）：18S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5R2<${a}{42 ›→ a = 1}[42]：=1 {R1}（d）r2（a）：R2<${a}{R1}（其中r2doa：=1）;[42]：=1{R1}（e）r1（a）：R1，r2（a）：R2{}{emp}c1{emp}ASIGNMENT，一个signment，一个SIGNMENT区域，（a）更新，如有必要，（b）（b）、（c）区域，CONSEQUEN cE，（d）S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）519同样，我们可以推导出（f） r1（a）：R1，r2（a）：R2<${emp}c2{emp}然后，通过从（e），（f）的PARRAYING，我们得到r1（a）：R1，r2（a）：R2<${}{emp}c1<$c2{emp}”[10]又云：“复有二乘。►{a}{R1<$R2}（c1<$c2）{R1<$R2}中资源r 2中的资源r 1。请注意，这个程序在原来的CSL中不能被证明是正确的，因为它违反了对关键变量使用的更严格的Owicki-Gries约束实际上，我们在证明资源上下文时使用了r1（a）：R1.r2（a）：R2其中保护列表不分离。同样的例子已经被JohnReynolds [ 11 ]讨论为我们包括这个例子来表明对变量使用采用较弱限制的优点7状态、动作和痕迹如[10]中，状态σ是由存储s和堆h组成的对（s，h）。存储将标识符（有限集合）映射到（整数）值;堆映射（有限集合的）位置转换为值;位置也是整数。在给定的状态中，dom（s）是当前作用域中标识符的集合，dom（h）是活动位置的集合。我们将资源名称视为标识符，其值限制为0（使用中）或1（可用）。设St是所有状态的集合如在[3]中，动作的集合Λ（由λ，μ组成）指定如下，其中v，vJ，v0. vnrange表示整数值，i range表示标识符，r range表示资源名称：λ：：= δ|I = v|i：= v|[v]= vJ|[v]：= vJ|alloc（v，[v0，.，vn]）|disp（v）|相对量|try（r）|try (r)| 中止我们让mod（λ）是其值被λ修改的标识符的集合：mod（i：=v）={i}和mod（λ）={}，否则。我们让writes（λ）mod（λ）是由λ修改的标识符或堆单元的集合：writes（i：=v）={i}，writes（[v]：=vJ）={v}，writes（alloc（v，[v0，...，vn]））={v，v +1，.，v + n}，写入（disp（v））={v}，否则写入（λ）={}。 类似地，我们让reads（λ）是标识符或堆单元的集合，其值由λ读取：reads（i = v）={i}，reads（[v]= vJ）={v}，reads（λ）={}20S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5I=vi：=v⇒|⇒相对论（s，h）=δ（s，h）（s，（h）=<$（s，h）if（i，v）∈sI=v（s，h）=abortifi∈dom（s）（s，h）=（[s|i：v]，h）ifi∈do m（s）i：=v（s，h）=abortifi∈dom（s）[v]=v′（s，h）=[v]=v′（s，h）如果（v，vJ）∈h（s，h）=====abortifv∈dom（h）[v]：=v′（s，h）=[v]：=v′ （s，（[h|v：vJ]）如果v∈ dom（h）（s，h）=====abortifv∈dom（h）disp（v）（s，h）=<$（s，h\v）ifv∈dom（h）disp（v）（s，h）=abortifv∈dom（h）alloc（v，[v0，.，vn]） J（s，h）=v+n} =m（h）={}，其中hJ= [h|v：v0，.，v + n：vn]获得R（s，h）=（[s r：0]，h）if（r，1）∈s尝试r（s，h）=（s，h）if（r，0）∈s（s，h）=（[s|r：1]，h）if（r，0）∈s（s，h）=a=b=o=rt中止Fig. 1. 扶持关系否则，请执行以下操作。 我们让free（λ）是λ中使用的标识符或堆单元的集合：free（λ）=reads（λ）<$writes（λ）。我们让res（λ）是使用的资源名称集S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）521单位为λ。行动对国家有影响，这是由使能关系=λ所体现的。St×（St{abort}）。 这些关系如图1所示。请注意，读和写操作（i = v和i：= v）仅依赖于存储，并且仅是一个例外;查找、更新、分配和处置操作仅依赖于堆，并且仅是堆的一部分;资源操作仅依赖于资源名称的值，并且仅是堆的一部分（同样，在存储中）。同样明显的是，存储操作的启用及其效果仅取决于附加到该操作的标识符或资源名称的值8语义我们使用与之前相同的指称语义模型[3]。我们总结了关键概念和技术细节。表达式表示求值轨迹的集合：求值轨迹具有形式（ρ，v），其中ρ是读取动作（或δ）的有限序列，v是值。表达式求值总是终止，所以ρ的范围是有限迹。因为表达式是纯的，所以它们的跟踪只涉及读操作。我们假设给定表达式的语义：对于整数表达式e，[[e]] Λ× Vint;对于布尔表达式 b， [[b]]Λ×{tru e ， fals e};对于列表表达式E ，[[E]]Λ×Vint。F或b 的表达式welet [b]]true={ρ|（ρ， tru e ） ∈[[b]]}，annd[b]]false={ρ|（ρ，fals e）∈[[b]]}. WeriteVint用于i ntegers的集合，Vbool用于真值values的集合，Vit用于i ntegers的有限序列的集合。命令表示动作轨迹的集合，可以是有限的或无限的，其结构反映了互斥假设，即资源的行为类似于二进制信号量。命令语义由结构归纳定义如下。[[skip]]={δ}[[i：=e]]={ρi：=v|（ρ，v）∈[[e]]}[[c1;c2]] =[[c1]][[c2]][[ifbthenc1elsec2]]=[[b]]true[[c1]][[b]]false[[c2]][[whilebdoc]] =（[b]]true[[c]]）<$[[b]]false<$（[[b]]true[[c]]）ω[[l 〇cali=einc]]={ρ（α|i）|（ρ，v）∈[[e]] &α∈[[c]][i：v]}[[i：=[e] ={ρ [v]= vJi：= vJ|（ρ，v）∈ [[e]]&vJ∈Vint}[e]：= eJ]]={ρρJ[v]：= vJ|（ρ，v）∈[[e]]&（ρJ，vJ）∈[[eJ]]}[[i：= cons（E）]]={ρalloc（v，L）|（ρ，L）∈ [[E]]&v∈Vint}[[dispose（e）]]={ρdisp（v）|（ρ，v）∈[[e]]}22S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5O2O2O2O2O2O1O2211O21O1 O2氧气O2==121O2O11[[withrwhenbdoc]]=等待输入等待ω其中wait ={try（r）}<${acq（r）ρ rel（r）|ρ ∈ [[b]] false}且enter={a cq（r）ρ αrel（r）|ρ∈[[b]]true&α∈[[c]]}[[resourcerinc]]={α\r|α∈[[c]][r：1]}[[c1<$c2]]= {α1{}<${}α2|α1∈[[c1]]&α2∈[[c2]]}用于本地资源的语义子句使用使能关系来表征在资源名称是“本地”的假设下可顺序执行的跟踪即，假设没有其他过程改变其值。我们说α对于ri是可执行的，并且αTr是从store[r：1]中启用的（即假设r最初是可用的）。我们写[c]][r：1]来表示可从[r：1]执行的c的跟踪集。用于局部变量的子句使用类似的结构。并行组合的语义子句使用公平交织[8]，并带有竞争检测和对资源的关注，将潜在的竞争视为灾难。如果α1和α2是轨迹，O1和O2是不相交的资源名称集合，我们将α1O1<$O2α2定义为通过将α1与α2交错可获得的轨迹集合，注意资源，假设执行α1的进程从资源O1开始，执行α2的进程从资源O2开始。当O1<$O2={}时，我们定义关系O1==λ<$OJ，当具有资源O1的进程可以在具有资源O2的环境中执行λ，之后进程将具有资源O1J。这些关系是由以下因素决定的：acq（r）O1=<$O1<${r}ifr∈相对量O1O2O1=<$O1−{r}ifr∈O1try（r）O1=<$O1ifr∈O1<$O2λO1==<$O1ifλ∈{a cq（r），rel（r），try（r）|r∈Res}我们推广到上述方法中的有限迹，使得O1=α=<$OJ以资源O1开始，可以在具有资源O2的环境中执行序列α，然后拥有资源O1J。然后对于有限迹，我们像往常一样归纳地定义公平合并算子O1<$O2αO-αO ={α|J.J.O1==α<$OJ}ϵǁβ={β|拉吉{\fnarialblack\fs12\bord1\shad0\4aH00\fscx90\fscy110}（λα）O （μ β）={λγ|O1==λ<$OJ&γ∈α奥贝奥（μ s）}μO&γ∈（λα）'β}氧气==21{中止|λ da μ}O1O2222S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）523ω我们定义一个约束关系λ da μ，使i = writes（λ）free（μ）/={}或writes（μ）free（λ）/={}。请注意，并发性因此对应于对标识符或正在并发使用的堆单元这个定义以标准的方式扩展到无限迹，但是因为我们在这里只需要处理有限迹，所以我们将省略细节。下面的结果表明命令尊重资源。引理8.1如果α ∈ [[c]]，则对于每个资源名r，α T {acq r，rel r}是（（acqr）（relr））的前缀。以下有限（非中止）跟踪的属性也很有用。引理8.2如果α∈[[c]]且（s，h）=π（sJ，hJ）则dom（sJ）=dom（s），sJ（r）=s（r）对于所有的r，且SJ（i）=s（i）对于所有的i∈写（c）。9本地状态从进程与其环境交互的角度来看，全局状态（s，h）可以表示为（s，（h1，O1），（h2，O2），H），其中（h1，O1）表示进程所拥有的堆部分和资源集，（h2，O2）由环境所拥有，H是堆的其余部分，包含其中资源不变量单独保持当前可用资源的部分。全局堆是这些部分的不相交并集，即h=h1·h2·H。与[10]中一样，堆h1和h2是分开的，记为h1<$h2，idom（h1）<$dom（h2）={}，当这成立时，我们将h1和h2的（不相交）并集记为h1·h2。对于一个资源名集合O，令Γ TO={r（X）：R∈ Γ |r∈ O}和r\O ={r（X）：R∈ Γ|rO}。当O是一个单例时，我们将ΓTr写成一个T{r}的缩写，类似地r\r为 r\{r}。回想一下，inv（Γ）是Γ中不变量的独立合取;当Γ为空时，这是emp。定义9.1Γ的局域态是满足以下分离性质的组合（s，（h1，O1），（h2，O2），H）：• h1，h2，H是独立的• O1<$O2={}，s（r）= 0，对于所有r∈O1<$O2，s（r）= 1，否则• （s，H）|= inv（r\（O1<$O2））≠ true。换句话说，进程、它的环境和可用资源拥有单独的堆部分;进程和它的环境拥有不相交的资源;在堆的其余部分，可用资源的不变量分别保持不变。设τr是τ的局部状态的集合局部状态（s，（h1，O1），（h2，O2），H）对应于全局状态，即（s，h1·h2·H），其通过组合堆部分并忽略资源所有权分区而获得。一般来说，全局状态可以以这种方式表示通过许多不同的局部状态，或者没有这样的局部状态，例如，如果没有全局堆的子堆满足资源不变量。α24S. Brookes/Electronic Notes in Theoretical Computer Science 276（2011）5Γ，AΓ，AΓ，AΓ，AΓ，Adisp（v）Γ，AΓ，A尝试rΓ，A（s，（h1，O1），（h2，O2）， H）−−δ→（s，（h1，O1），（h2，O2），H）（s，（h1，O1），（h2，O2）， H）−i=−→v（s，（h1，O1），（h2，O2），H）若（i，v）∈s且i∈owned（ΓTO1）<$A（s，（h1，O1），（h2