动态分离逻辑模型：Kripke模型和动态线程创建的合理性证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）121-143www.elsevier.com/locate/entcs可存储锁分离逻辑的步索引Kripke模型Alexandre Buisse 拉尔斯·伯克达尔2丹麦哥本哈根IT大学克里斯蒂安·斯托夫林3丹麦哥本哈根大学摘要我们提出了一个版本的分离逻辑模块推理的并发程序与动态分配的可存储锁和动态线程创建。 程序逻辑的断言被建模为一个递归定义的世界集上的Kripke模型和程序逻辑被证明是合理的，通过Kripke关系到标准的操作语义。这构成了一个优雅的解决方案，以解决锁资源不变量依赖于包含锁资源不变量的世界而产生关键词：语义，并发，分离逻辑，步进索引1引言我们提出了一个版本的分离程序逻辑的模块化推理共享变量并发命令式程序与动态分配的可存储锁和动态线程创建。根据早期的工作[8，9，11]，逻辑的思想是锁可以用来保护资源不变式，从概念上讲，从一个线程转移到另一个线程。资源不变量跟随锁本身的移动，通过获取和释放操作改变所有权。由于与锁相关联的资源不变量描述了堆的属性，而锁本身（动态分配和）存储在堆中，因此需要解决一种棘手的循环形式，以便开发一个模型来显示逻辑的合理性更具体地说，由于锁是动态的，第1abui@itu.dk2birkedal@itu.dk3stovring@diku.dk1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.018122A. Buisse等人理论计算机科学电子笔记276（2011）121在分配的情况下，自然使用断言的Kripke模型，使得断言的语义是程序堆集合上的世界索引谓词，并且世界集合描述分配的锁保护的谓词。总之，我们最终得到了大致如下形式的递归语义方程Pred=W→ P（H）W=Loc-finP red在早期的工作中，Gotsman等人[8]通过限制逻辑和使用锁类的静态数量来避免这种循环，因此可以通过锁类的语法名称使用间接来打破循环，并通过在程序堆中包含锁类的语法名称来检测操作语义。在[10，9]中，Hobor等人使用步骤索引和操作语义工具解决了循环性。操作语义的插装意味着在这两种情况下都需要一些额外的工作来将语义与标准操作语义相关联，就像最近Hobor等人所做的那样。[12 ]第10条。在这里，我们（1）在一类完全有界超度量空间中求解上述递归方程（的一个版本），遵循我们之前使用动态分配引用单元来建模高阶编程语言的思想[5，4]。这为谓词提供了一个真正的语义状态，例如允许通过定点运算符进行递归定义。此外，（2），我们证明了可靠的逻辑，通过给一个Kripke关系的标准（非仪器）的操作语义。这种证明可靠性的方法涉及类型系统模型可靠性的逻辑关系证明（例如，[4]），并提出了并发Vafeiadis [13，7]。在这里，我们将展示如何在一个更丰富的语言中扩展和应用该技术，包括动态线程创建和可存储锁。总之，我们相信我们的新方法的语义和可靠性是语义上简单和有用的，因为它解决了循环问题直接和可靠性证明w.r.t.标准操作语义。我们展示了我们的方法，一个简单但说明性的语言，也包括一个例子，使用由此产生的逻辑。2语言2.1定义我们将使用一个小的，低层次的命令式语言支持最小的堆管理命令，简单的锁操作和并发通过动态线程创建和同步。其语法定义如下：A. Buisse等人理论计算机科学电子笔记276（2011）121123设x=[E]inC|[E] =F|如果B那么C否则C′|而[E]做C|skip|C;C′|Makelock P（E）|获取（E）|释放（E）|C中的x=fork（f）|join（E）命令表达式包括整数常量和算术运算符，我们将在这里不详细介绍。一个程序由子过程的静态定义f0到fn组成，后跟一个主命令C：设f0= C0，f1= C1，且fn= Cn在C中在这里，主命令C可以通过调用fork来创建子过程的新实例。我们在语法上做了几个选择，试图在功能与我们感兴趣的问题正交时简化语言。特别是，我们通过连续传递样式命令（C中的letx= new和C中的letx=E分别用于分配和查找）使用不可变的堆栈变量，如下[6]。任何形式的命令letx=. 在C中使用了一个新的变量x，如果需要的话，通过alpha转换获得。此外，为了保持相对简单，该语言不支持任何资源释放，无论是常规的内存单元还是锁。后者允许我们省略在以前的作品中发现的整个分数权限系统（例如，[8]和[9]）。2.2操作语义我们将为语言使用一个简单的非确定性操作语义，接近真实机器实际执行的内容。我们的抽象锁的行为类似于自旋锁，在一个不可用的锁上的获取在我们的语义中，状态是一个三元组（h，s，tp），其中h是H=Loc→finV al中的堆，s是V ar→V al中的堆栈，tp是将每个线程标识符映射到它应该执行的代码的线程池，即。 tp：{1，.， n}→ Cmd对于某个n。需要注意的是，这种操作语义是非常低级的，不处理一些更“语义化”的特性。尤其不会 堆和栈在线程之间被分割，并且没有私有或共享空间的概念。 类似地，锁以非常简单的方式实现： 一个整数，如果锁可用，则包含0，如果它当前由标识符为k的线程拥有，则包含k。既然没有世界的概念，Var* = l，x，y，.变量E、F* =零|Var |E + F|......这是什么？表达式B* =E=F|E/=F布尔表达式CC中的x= new|设x=EinC|124A. Buisse等人理论计算机科学电子笔记276（2011）121J将锁或线程句柄与常规内存单元区分开来，并且不正确的程序可以轻易地覆盖锁值。定义2.1在我们的操作语义中，约简的一般形式是（h，s，t）−→j（hJ，sJ，tJ）。 然而，为了提高可读性，我们将写（c，h，s，t）−→j（c此外，状态（h，s，t）也可以相对于线程j被卡住，写入（h，s，t）/→j，或导致n执行故障，写入（h，s，t）-→j中止。为了节省空间，我们没有列出中止状态的所有条件：相反，我们定义了中止状态是既不卡住也不降低到另一状态的状态（令x = newinc，h，s，t）−→j（c，h[v<$→0]，s[x<$→v]，t[j<$→c]）其中v/∈dom（h）（令x =[E] in c，h，s，t）−→j（c，h，s[x <$→ v]，t[j <$→ c]），其中h（[|E|]s）= v（设x = E in c，h，s，t）−→j（c，h，s[x <$→ [|E|]s]，t[j <$→ c]）（[E] =F，h，s，t）−→j（skip，h[[|E|]s[|F|]s]，s，t[j <$→ skip]）（ifEthen c elsec'，h，s，t）−→ j（c，h，s，t [ j <$→ c ]），如果[|E|]s= True（ifEthen c elsec' ， h ， s ， t ） − → j （ c ' ， h ， s ， t [ j < $ → c ' ] ） ， i f [|E|]s=假（while [E] do c，h，s，t）−→j（skip，h，s，t [j ›→ skip]），如果h（[|E|] s）= False（while [E] do c，h，s，t）−→j（c;while [E] do c，h，s，t[j<$→c;while [E] do c]）如果h（[|E|]s）=True（skip;c，h，s，t）−→j（c，h，s，t[j <$→ c]）（c;c如果（c，h，s，t）−→j（（makelockP（E），h，s，t）−→j（skip，h[[|E|]s→›（acquire（E），h，s，t）−→j（skip，h[[|E|]s→›（acquire（E），h，s，t）/→jifh（[|E|]s）>0j]，s，t[j <$→skip]），如果h（[|E|]s）=j]，s，t[j <$→skip]），如果h（[|E|]s）= 0（release（E），h，s，t）−→j（skip，h[[|E|]s<$→ 0]，s，t [j <$→ skip]），如果h（[|E|]s）= j（令x =fork（f）inc，h，s，t）−→j（c，h[v<$→k]，s[x<$→v]，t[k<$→c]），若v/∈dom（h）， k/∈dom（t），f：c∈Γ（join（E），h，s，t）−→j（skip，h|dom（h）−[|E|]s，s，t[j <$→skip]|dom（t）−{k}），如果h（[|E|[s]）= k和t（k）= skip（join（E），h，s，t）/→j如果h（[|E|]s）=k和t（k）/=skip（h，s，t）−→j在所有其他情况下中止2.3断言语言A. Buisse等人理论计算机科学电子笔记276（2011）121125我们的断言语言是建立在分离逻辑之上的，额外的断言处理锁和动态线程创建和同步。此外该126A. Buisse等人理论计算机科学电子笔记276（2011）121可存储锁的内在循环性通过定点运算符μ来表示。PredV ar：：= p，q，r，.P：：= E1= E2|E1›→E2|PP| PP|PP|EMP|锁定（E、P）|Ex（E，P）|tid（f，E）|r（E）|（μr.λx.P）（E）（*）V al=位置Z（V al×V al）请注意，我们不包括分离蕴涵。这是我们当前模型的一个局限性;参见下面的命题4.6为了表示锁属性，我们使用两个谓词：Ex（E，P）和Locked（E，P）。第一个假设是，表达式E的解释指向堆中的一个锁，具有资源不变式P。没有关于锁是否可用的假设。Locked（E，P）与此类似，只是附加了当前线程拥有锁的声明。线程在尝试获取锁之前必须知道锁的存在，但不知道锁是否可用。类似地，锁释放的后置条件只是说锁仍然存在，但不是说它是可用的，以防止来自其他线程的干扰，这些线程现在可以成功地获取锁。侧条件（*）规定谓词变量r在P中的所有出现都是受保护的，即它们只出现在Locked或Ex谓词下。更正式地说，使用符号P[ ]是一个公式，其中有一个洞可以由谓词Q填充，写作P[Q]：定义2.2谓词变量r在P中是受保护的，如果P=1，E，Q，使得P=P1[Ex（E，Q）]或P=P1[Locked（E，Q）]且r/∈fv（P1）.此外，我们还有通常的直觉逻辑规则和一些用于断言逻辑的附加规则，例如Locked（E，P）锁紧（E，P）锁紧（，P）锁Ex（E，P）（μr.λx.P）（E）惠P[（μr.λx.P）/r，E/x]2.4精选证明规则我们现在给出一些具体化逻辑的证明规则，选择省略大部分结构规则。 我们需要以下定义：预测cateP是线程独立的，如果它不包含任何形式为Locked（E，PJ）的子谓词。直觉上，这样的谓词的含义对于给定配置中的所有线程都是相同的，而例如，Locked（E，P，J）谓词对于至多一个线程为真。谓词是移动的，如果它是线程独立的和精确的。A. Buisse等人理论计算机科学电子笔记276（2011）121127{P<$x<$→0}c{Q}x/∈fv（P）<$f v（Q） {P<$E→<$ x}c{Q}x/∈fv（Q）{P}let x =newin c{Q}{\displaystylex，P\displaystyleE} →x}let x = [E] in c{Q}{P<$x=E}c{Q}x/∈fv（Q）{P}设x = E in c{Q}{E=trueP}c{Q}{E=falseP}c{P}ifEthencelsec{[E<$→]}[E] = F{[E<$→F]}{PE<$→true}c{PE<$→}{PE <$→ }while [E] do c{PE<$→false}{P}跳过{P}{P}c{Q}{Q}c{P}c;c（*）{E›→}makelock P（E）{Locked（E，P）}（*）（*）{Ex（E，P）}获取（E）{锁定（E，P）释放（E）{Ex（E，P）}r，{R}f{S}<${P_（x）}c{Q}（*）令x =fork（f）in c{Q}Γ，{R}f{S} {tid（f，E）}join（E）{S}（*）f：{R}c► 设f：{R}c标有（*）的规则具有以下一般性限制：• 所有出现在规则中Locked（E，P）或Ex（E，P）中的谓词P都是可移动的。• 对于每个三元组{R}f{S}，假设（即，在“”的左边），R是移动的，而S是线程独立的。锁的资源不变量的精度要求需要独立于线程的谓词正是那些描述堆的部分的谓词，从概念上讲，这些部分在不同的线程之间传输。这些谓词的含义在这种转移之前和之后必须是相同的。3示例：锁紧联轴器锁耦合算法可以被认为是可存储锁的开创性示例，并且Gotsman等人以非常相似的方式进行了处理。这个想法是允许多个线程同时从一个有序的单链表中添加和删除元素不是为整个列表使用一个通用锁，这将要求所有线程等待活动线程完成其操作，而是使用每个节点一个锁。通过要求线程在搜索列表或试图修改列表时同时持有当前节点和前一个节点的锁，我们可以确保数据结构永远不会处于不一致的状态，而细粒度锁可以大大提高效率。每个节点包含三个字段：一个保护整个节点的锁，资源不变量P，一个包含整数和指向下一个节点的指针的数据字段val128A. Buisse等人理论计算机科学电子笔记276（2011）121∞−∞−∞n≤v∗∧−∞−∞ ∗−∞→ −∞ ∗›→∗∃ −∞ ∗′›→ ∗ ∧›→∗›→∗ ›→∗∗∗′∃∗或零。我们还使用了一个约定，即列表的头部总是包含值−∞，而尾部总是包含值+∞。我们在这里给出了初始化列表和在堆的正确位置添加一个值为e的新节点的代码。删除值为e的节点的过程非常类似。由于知道特定锁存在的唯一方法是通过在列表中获取其前身，因此不变量本身强制执行特定的锁定过程以迭代通过列表。下面我们给出add的注释证明的简化版本。资源不变式是一个递归定义的谓词：P（n，e）=（μr.λ（n，e）. [（n.val <$→ e e = ∞）（x，eJ，n.val→xEx（x.lock，r（x，eJ））e eJ））]）（n，e）n.nextinitialize（）{1}让尾巴=新节点在[尾巴val]=+;[tail. 下一页]=NULL;makelockP（tail，+∞）（tail. lock）;释放（Prev. lock）;letprev=curr in让Curr=Curr.下一获取（curr. lock）;}′′′释放（尾巴）lock）;lethead= new NODEin[head.return;[头。return[];makelockP（head，−∞）（head.lock）; release（head. lock）;}public void run（e）{Ex（head.lock，P（head，））letprev= headinacquire（prev. lock）;Locked（prev.lock，P（prev，））P（prev，）设curr= prev。下一个获取（curr. lock）;v′，Locked（prev.lock，P（prev，））prev.val prev.next curr Locked（curr.lock，P（curr，v′））P（curr，v′）

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