并发库抽象局部推理与细化：SSL和CAP在www.sciencedirect.com在线获取

可在www.sciencedirect.com在线获取理论计算机科学电子笔记308（2014）147-166www.elsevier.com/locate/entcs并发库的抽象局部推理：注意差距Philippa Gardner1，Azalea Raad1，Mark Wheelhouse1和Adam Wright1英国伦敦帝国理工学院计算机系摘要我们研究并发库的抽象局部推理。有两种主要的方法：通过对实现的具体推理进行抽象来提供库的规范;或者提供直接抽象库规范，通过细化到一个实现来实现。这两种方法在推理上都有很大的差距，这是由于抽象的抽象连接性和抽象的抽象连接性数据结构和具体堆表示的具体连接性。 我们证明这一点使用结构分离逻辑（SSL）指定并发树库和并发抽象的间隙谓词（CAP）用于推理具体的树实现。抽象和具体连接之间的差距表现为SSL树谓词和CAP堆谓词之间的不匹配。这个间隙由接口函数I闭合，该接口函数I将抽象的连通性和具体的连通性联系起来。在随附的技术报告中，我们将我们的SSL推理和结果推广到任意并发数据库。关键词：并发，抽象，细化，分离，翻译，推理1引言局部推理首先在分离逻辑中引入，以推理RAM内存模型。从那时起，有相当多的工作结合本地推理与抽象。主要有两种方法。一种方法是从具体的代码推理开始，这些代码操作标准堆，然后建立抽象层：这种方法被并发抽象谓词 （ CAP ） 及 其 变 体 [1 ， 16 ， 17] 所 使 用 ， 并 且 非 常 适 合 推 理 并 发 库java.util.concurrent，其中库函数是使用实现建立的。另一种方法提供了操作抽象模型的抽象代码的直接抽象规范，然后通过将其细化为正确的具体实现来调整规范：这种方法由上下文使用。1电子邮件：{pg，azalea，mjw 03，adw 07}@ doc.ic.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2014.10.0091571-0661/© 2014作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/3.0/）。148P. Gardner等理论计算机科学电子笔记308（2014）147（）（）（）（）（）（）（）（）（）（[]）（）（）逻辑[7，9]，并且非常适合于推理库，如POSIX和顺序DOM，其中库规范不基于实现。这些当前的抽象和细化方法在其推理中存在重大差距。通过抽象，实现细节泄漏到抽象中。例如，考虑用于描述树片段的CAP谓词树t i，jl，u，r。谓词由抽象树t参数化，具体指针i、j、l、u、r描述用于连接具体树片段的具体接口。在这种情况下，具体接口由树片段的第一个（i）和最后一个（j）节点，以及父节点（u）、左节点（l）和右节点（r）组成。一个不同的实现，比如说使用列表的实现，将需要一个不同的具体接口。因此，这个树谓词不够抽象，不能抽象地推理更新树片段2。缺少的部分是一种分割和组合树片段的抽象方式，以及一种将其链接到由i，jl，u，r给出的具体接口的方式在精化方法中，我们有一些具体化是真正抽象的例子（例如，[12，19]），但它们通常由操作语义的可靠性结果而不是实现来证明。例如，树模块（如DOM）的真正抽象推理基于使用上下文和占位符连接树片段来使用谓词。相反，关于实现的具体推理使用指针。我们需要在抽象数据结构的抽象连接性和具体堆表示的具体连接性之间架起一座桥梁我们引入了结构分离逻辑（SSL）来推理并发抽象数据库[2，19]。SSL由一种特定的通用方法来支持，用于抽象结构化数据的连接。在本文中，我们使用一个简单的并发树库来说明我们的想法。我们使用CAP [1]提供了关于库的树实现的具体推理。抽象和具体连接之间的差距表现为SSL树谓词和CAP树谓词之间的不匹配这个间隙由接口函数I闭合，该接口函数I将抽象的连通性和具体的连通性联系起来。在随附的技术报告[18]和Raad即将发表的论文中，我们将SSL和我们的结果推广到任意结构化数据库。 这里介绍的工作确实依赖于特定的SSL方法to abstract抽象connectivity连接.然而，我们的想法应该适用于抽象和具体连接之间不匹配的任何时候。SSL支持对存储在抽象堆中的细粒度抽象数据片段进行推理。抽象堆包含由抽象地址（例如地址x）标识的单元这些数据片段包含上下文漏洞，也由抽象地址给出，这些地址是在适当的抽象单元中找到的数据片段的占位符。例如，SSL谓词ATreetx描述了一个树单元，其抽象地址x包含树上下文t。我们可以拆分（抽象分配）这个谓词以获得2同样的问题也出现在著名的谓词listseg1， 2， 3i r中，它描述了具有具体地址i、抽象内容1， 2， 3和具体右指针r的列表片段。这个谓词适用于使用单链表的实现，但不适用于那些需要额外的具体左指针的双链表。谓词不够抽象，因为具体接口泄漏到谓词中。缺少的位是列表片段的抽象连通性P. Gardner等理论计算机科学电子笔记308（2014）147149（）（） /]∗用指针接口（i，j）（l，u，r）修饰x。 我们证明了我们的实现∗CAP谓词CTreeI（t）（x），其中接口函数I将抽象ad- ∗（）（）∗trast，我们的保留翻译确保了兼容的稳定资源位于∗语义等价断言y。A树t1xA树t2y，其中t t1t2y。断言表示相同的底层树片段，只是分成两个不相交的部分。关于语义等价断言的推理仅可能是由于视图框架[6]给出的并发推理的最新进展。我们提供了我们的树库的自然实现，并通过将库函数的抽象SSL规范与具体函数实现的CAP类规范相关联，表明它对于我们的抽象SSL规范是正确的。要做到这一点，我们必须用接口函数I扩展CAP谓词，接口函数I将抽象地址与具体指针联系起来。例如，考虑抽象树谓词ATreetx和对应的具体对于我们的抽象规范来说是正确的，使用由I参数化的保局部翻译（类似于[9]中的保局部翻译）。在本文中，我们专注于精炼。调整我们的工作是微不足道的到虚构分离逻辑（FSL）[13]的方法，其中翻译被整合在霍尔推导中。然而，我们对翻译的选择从根本上与外语二语有着很大的不同。FSL被设计成使用- 破坏翻译（类似于[9]中的局部破坏翻译）：FSL的证明假设所有可能的框架在程序执行期间都被保留。虽然在推理顺序程序时这是一个合理的假设，但在并发程序中建立它的可靠性并非易事。证明其正确性的一个可能的方法是提供线性证明，以表明所有的框架确实被保留，并且程序的行为是原子的。与此同时-抽象层（pq）一旦翻译就产生兼容的稳定资源（pq）3.并发程序的正确性直接遵循并发分离逻辑的不相交并发规则[20]。在使用CAP进行抽象时，我们首先具体地推理堆，然后以保留的方式建立抽象级别。如图所示，当前CAP推理将实现细节泄漏到抽象中。我们相信这可以通过扩展抽象规则来隐藏接口函数以及谓词解释来纠正。我们相信，接口功能我几乎没有研究过的文献。它们确实出现在[9]中，用于使用上下文逻辑推理顺序库上下文逻辑的粒度不够细，无法扩展到并发，因为它使用了一个非交换的分离应用程序，不适合与不相交的并发规则一起使用。SSL推理使这种扩展成为可能。SSL在[19]中用于指定顺序POSIX，目的是将来扩展到并发POSIX。然而，合理性是通过与抽象操作语义的比较来证明的在[15，16，13]中，强调了与抽象概念相关的解释。[3]请注意，p q不一定表示物理上不相交的资源;而是两个可以组合在一起的兼容资源，提供了一个不相交的集合。150P. Gardner等理论计算机科学电子笔记308（2014）147αXX一个抽象堆，描述一个值为n的可变单元n，和一个树单元R，[客户以及在R的不完整树，其中上下文洞x指示{（）×（[]）（）}{（）×（）（）}图中的抽象堆1b，子树n[t]在一个新的抽象单元格x上Rn*Rn*R*Xn un unLn不（RLXR不（b）第（1）款图1.一、S S L 中 的 抽象（解）分配（左）; SSL中deleteTree（n）的 推 理 （右）具体的国家。然而，没有提到抽象和具体接口之间的映射I，因为所研究的示例中的连通性很简单。2结构分离逻辑：树库结构分离逻辑（Structural Separation Logic，SSL）是一种通用的程序逻辑，用于指定结构化数据库并在本地对调用这些库的客户端程序进行推理。在这里，我们给出了使用抽象树库的SSL的直观和技术细节。我们在随附的技术报告中给出了SSL的一般理论[18]。更多的细节，包括大量的例子，可以在[2]中找到2.1直觉我们给出了一个简单的deleteTree（n）命令的公理化SSL规范。直观地说，这个命令删除了整个子树，其顶部节点标识符对应于变量n的值，而树的其余部分不变。我们使用描述抽象堆的断言来正式化这个英语描述。抽象堆存储抽象数据片段。例如图1a示出完整的抽象树作为其值。这棵树由一个子树n t和父树u，以及左、右兄弟树l和r组成，没有子树。它抽象了树在机器中的具体表示方式直观地说，deleteTree（n）命令只会删除由n标识的子树。抽象堆允许结构化数据被拆分，以通过使用抽象地址施加附加的插装来提供对该子树的直接访问。考虑从图1a到图1b的过渡。图1a包含了一个抽象堆，它有一个完整的树。我们使用抽象分配来分割这棵完整的树，子树将返回。现在可以直接访问n处的子树。一旦完成了更新，就可以使用抽象释放将堆重新连接在一起，如图1b到图1a的转换。deleteTree（n）的公理化规范（图1c）形式化为：varn，nATree n isCompletexdeleteTree（n）varn，nATreex前提条件描述变量存储，其中变量n具有值n，⎧⎪⎪⎨nn*X⎫⎪⎧⎪nn*n deleteTree（n）删除X⎫⎪⎪⎬⎪⎪⎩⎪不⎪⎪⎭⎪⎪⎪⎩⎪⎪⎪⎭⎪（c）第（1）款P. Gardner等理论计算机科学电子笔记308（2014）147151RRR∣∣和n，以及表示com的抽象树谓词ATree（u[l<$n[t]<$r]）（R）R===∣ ∣∣∈∗抽象单元X具有以顶部节点N作为其值4的完全子树。由于x处的子树是完整的，我们拥有更新其内容的专有权类似地，后置条件声明更新的结果是抽象单元格x处的空树，而变量n保持不变。请注意，抽象单元格x必须保留，以便使用抽象释放将该树片段与它从中分裂的树连接起来。这个命令的占用空间很小，因为它直观地捕获了安全执行deleteTree（n）所需的最小资源。有了这个公理化，我们可以验证简单的客户端程序deleteTree（l）deleteTree（n）同时删除两个不相交的子树。考虑图中的证明推导 2，程序变量l和n，它们的值l全树AT包含具有顶部节点n的子树、具有顶部节点l和r的左兄弟树和右兄弟树以及父树u。初始前提条件描述了完整的树。为了得到这两个子树，我们使用抽象分配将树拆分两次，分别将节点l和n上的子树放置在新分配的单元地址y和x上。 我们应用标准的分离逻辑规则的存在消除和框架暂时搁置部分树，因为它不是由程序更新。然后，可以使用不相交并发规则将结果状态拆分为两个不相交的部分这两个部分现在都以正确的形式匹配deleteTree公理的前提条件。这两个更新可能发生，导致在y和x处具有空树的后置条件，它们通过不相交并发规则连接在一起。我们重新引入了通过逐步消除和框架规则保留的状态，并在使用两次抽象释放来移除y和x时得到了完整的树。2.2技术细节我们使用第2.1节中讨论的树库T给出SSL的技术细节。定义2.1T的抽象原子树命令集定义为：A TOMm：= getFirst（n）m：= getRight（n）m：= getUp（n）m：= newNodeAfter（n）deleteTree（n）appendChild（m，n）对于所有程序变量n，m PV ARS。我们的命令被选择来演示广泛的结构操作。命令getFirst（n）返回节点n的第一个子节点的标识符，如果n没有子节点，则返回null。getRight（n）和getUp（n）命令的行为分别与节点n的右兄弟节点和父节点类似命令newNodeAfter（n）创建一个新节点，并使用新标识符，使其成为节点n的正确兄弟节点，并返回新标识符。deleteTree （ n ） 命 令 从 树 中 删 除 由 n 标 识 的 整 个 子 树 最 后 ， 命 令appendChild（m，n）将n处的子树移动到节点m的最后一个子节点。如果给定的任何节点4注意，前提条件是由变量断言和子树（堆）断言组成的一对。我们使用变量作为资源模型[14]。然而，与将变量作为资源的断言相反，当堆和变量断言使用组合时，我们将这两个组件分开。正如我们在第4节中所展示的，这是因为当翻译一个库时，只有堆被转换，而程序变量被简单地 保留下来。152P. Gardner等理论计算机科学电子笔记308（2014）147R{R}{（（）（））×（（）（ [ ]））}{（（））×（（[]）（R））}（）（） [2014 - 05 - 23][]]）（R））}{（（）（））×（（[]）（R）（[ ]）（））}{（（））×（（））}{（（））×（（ [ ]））}⋯{{（（））×（（））}{（（））×（（））}{（（）（））×（（[]）（R）（））}（）（））×（（）（））}：：==[]李明博1 2电子邮件[email protected]表示用t2来替换t中的x。1与单位的关联性。 为简洁起见，我们将n+写成n。 有一个标识符和抽象地址存在于抽象树中应用t○t1x2//不确定性消除和框架规则varl，lvarn，nATreeulntr//抽象分配（两次）v arl，lv arn，nx，y. ATreeuyxrATreelyATreentx//不确定性消除和框架规则varl，lvarn，nATreelyATreentx//不相交并发规则varl，lATreelyvarn，nATreentxdeleteTree（l）deleteTree（n）varl，lATreeyvarn，nATreexvarl，lvarn，nATreeyATreexv arl，lv arn，nx，y. ATreeuyxrATreeyATreex//抽象释放（两次）varl，lvarn，nATreeur图二、 并发程序deleteTree（l）的证明推导||deleteTree（n）.因为树中不存在参数。此外，appendChild（m，n）命令在m是n的后代时出错。这些命令适用于任何编程语言。在本文中，我们使用视图框架[6]的编程语言，用ATOMT实例化作为原子命令集我们写PROGT来表示用这种语言编写的程序集我们使用抽象堆指定树命令，其中单元的地址是抽象地址或树根地址，其值是抽象树。定义2.2给定一个可数无限的抽象地址集AA DD，其范围为x，y，z，抽象树堆的地址集为A DDTAADD。我们现在定义抽象树，它可以是完整的树，也可以是具有上下文洞抽象地址的树片段。定义2.3给定抽象地址集AADD，抽象树集数据T，由t，t1，t n，归纳地定义为：其中n∈ N+t n t t tx，x∈AADD，集合AADD与N+不相交，且没有树包含重复节点标识符或抽象地址。 抽象树等于关联标识符函数ids：数据T→ N和关联地址函数addrs∶DataT→T（AADD）分别返回节点集是标准的：当x∈/addrs（t1）时，它被定义，否则被定义为st1[t2/x]，[5]严格地说，这个文法描述森林或抽象树的有序列表。 当我们希望用第一个和最后一个元素来强调列表时，我们使用术语森林P. Gardner等理论计算机科学电子笔记308（2014）147153∈=n/x∈AADD. xD+x∈D+x∈dom（h）<$AADD. RDxhh定义2.4抽象树堆的集合H∶ADD≠DATA，范围为T T T所有h∈H，以下限制成立：T{→ [] → []}≜∩()≜∩(⋃())∈()A（●）其中，H是给定的。2.4、●是与TT的标准离散函数联合[14]和抽象树堆的代数（Def. 2.5）。（T，0σ×0T）， 是变量抽象树堆是从地址到抽象树的映射芬由h，h1，n，hn，是从地址到抽象树的函数的集合，使得对于a，a aA DD. a a addrs h a addrs h aa1，a2∈A DDT. a1=a2拟阵（h（a1））拟阵（h（a2））=拟阵其中堆h的下降关系D定义为：+a Dhy∈addrs（h（a））Dh表示它的传递闭包。前两个限制规定，用作上下文洞的抽象地址和节点标识符在抽象堆中是唯一的。最后一个条件指出，抽象地址连接起来产生合理的抽象树。 比如说，Xmy，ynx不是抽象树堆，因为周期一个抽象树堆可能是：完整的，没有使用抽象地址;完整的，但是树被分成几个堆单元;或者不完整的，缺少一些需要连接一些抽象地址的堆单元。使用框架规则进行局部推理需要不完整的抽象堆。在这种情况下，对于缺失的单元格将有一些选择，以使树完整。给定抽象树堆h，hin和hout分别表示抽象单元地址和上下文洞hinAA DDdomhhoutAA DDtco-domhaddrs t.从设计上讲，抽象树堆与标准堆类似。因此，在它们上构造分离代数是简单的。定义2.5抽象树堆的分离代数是THT，T，0T，条件是得到的抽象堆是符合定义2.4的良构的;并且0T是由具有空域和共域的部分函数组成的单例集由于我们使用变量作为资源[14]，因此我们将变量存储与抽象树堆配对，用于声明变量D●定义2.6抽象行为的分离代数表示SAT（Σ×HT，●σ×为了推理我们的树程序，我们使用了[6]中描述的视图框架的程序逻辑。我们用抽象树状态的分离代数（定义2.6）作为视图幺半群，用树库命令（定义2.1）作为原子命令来实例化框架。剩下的就是描述与树库命令相关的公理（定义2.7）。154P. Gardner等理论计算机科学电子笔记308（2014）147{（（）（））×（（[ [] ]））}{（（）（））×（（[ [] ]））}{（（）（））×（（[]））}{（（）（））×（（[]））}（））×（（）（={each（ ）=}σ，h）<$v∈V <$σ∈p<$h∈q}假设任何载波集V.最后，我们定义了{h（1●Th2<$h1∈p<$h2∈q}. 对于抽象树的状态，我们记为V∈V. （p×q），（1）（2）（ ×）w，x，y，z ∈ ADD，t ∈ C OMP DATA. C{对于一个b-t-t-t- e-p的集合，我们对{x→d}和p-q-e-e-（d）（x）进行了计算，varn，n变量集，我们写var（x，v）为{x→v}和p<$q为{σ●σ<$σ ∈p<$σ∈q}。1σ2 12A树n tcXvarn，nvarm，oA树n my z xint n（n）varn，nvarm，mA树n my z x{（var（n，n）<$var（m，o））×（ATree（n[y]<$m[z]）（x））}M：= getRight（n）{（var（n，n）<$var（m，m））×（ATree（n[y]<$m[z]）（x））}{（var（n，n）<$var（m，o））×（ATree（m[y<$n[z]<$w]）（x））}m：= getUp（n）{（var（n，n）<$var（m，m））×（ATree（m[y<$n[z]<$w]）（x））}varn，nvarm，oA树nxint n（n）varn，nvarm，null A树nx{（var（n，n）<$var（m，o））×（ATree（u[y<$n[z]]）（x））}M：= getRight（n）{（var（n，n）<$var（m，null））×（ATree（u[y<$n[z]]）（x））}{（var（n，n）<$var（m，o））×（ATree（x<$n[y]<$z）（R））}m：= getUp（n）{（var（n，n）<$var（m，null））×（ATree（x<$n[y]<$z）（R））}{（var（n，n）<$var（m，o））×（ATree（n[y]）（x））}M：= newNodeAfter（n）{（（））×（（[ ]））}公司简介（var（n，n） var（m，m））×deleteTree（n）））}⎨⎪⎩∃m∈N. （ATree（n[y]m[]）（x））varn，nATreex{（var（m，m）<$var（n，n））×（ATree（m[z]）（y）<$ATree（n[tc]）（x））}appendChild（m，n）{（var（m，m）<$var（n，n））×（ATree（m[z<$n[tc]]）（y）<$ATree（x））}图三. 树库命令的公理化：假设任意m，n∈PV ARS，l，m，n，o∈ N+n {null}，我们的观点是一组抽象的树状态，在<$（<$×HT）。为了增加可读性，一组完整的抽象树作为一组没有上下文洞的抽象树：COMP DATATDDATAT地址d.定义2.7原子树命令的公理化：AXIOMT ATOMT HT HT在图3中定义。为了保证可靠性，每个公理必须保留所描述数据中存在的抽象地址集。如果不这样做，将给出不稳定的命令，因为由抽象地址描述的抽象连接性将被破坏。这在deleteTree公理中很明显，它要求被删除的子树是完整的，因为它不包含上下文漏洞。如果子树确实包含上下文漏洞，它将被销毁，并且将有一些匹配的抽象堆单元，这些单元无法连接到任何地方。视图框架的技术细节使用了一个标记的转换系统来描述状态之间的转换。转换由原子命令或标识符标记，标识符标记状态未改变的计算步骤我们通过声明抽象分配/释放的关系AXIOMID来扩展视图的id转换的行为抽象（解）分配不会改变底层的程序状态，因此可以看作是id转换。定义2.8恒等式公理化：AXIOMID∶（×HT）× {id}×（×HT）（P. Gardner等理论计算机科学电子笔记308（2014）147155{（○）（）}{（○）（）}（C∈PROG（Def. 2.1），abstract三元组是Ω<$ {p}C{q}。Ω ∈PEnv是一个过程 TT Tf是一个过程名，p， q∈H（H ×H）是f的前/后条件. 11吨‹由抽象的分配和释放公理给出：A树d1xd2aidy。A树d1xyaA树d2y{\1cHFF8000}{\1cHFF8000} A树（d1 ○ xy）（a）A树（d2）（y）} id {A树（d1○ xd2）（a）}抽象地址y的存在性量化类似于分离逻辑中用于堆分配的定义2.9给定抽象树堆的集合HT（Def. 2.4）、原子命令集ATOMT（定义2.1）及其公理化AXIOMT（定义2.7），则抽象树库T被定义为：THT，ATOMT，AXIOMTAXIOMID定义2.10给定抽象树的状态p，q∈H（H ×HT）（定义2.6），指定环境是一组过程指定f∶p1<$q1，其中3并发抽象谓词：树实现我们使用并发抽象谓词（CAP）来推理我们的实现。我们在§ 3.1中描述了抽象树的具体表示和树命令的具体实现。我们在§3.2中对我们的实现进行推理。我们给出了一个非正式的说明，说明如何根据§3.3中的抽象规范来确定它的正确性，并在§4中给出正式的证明。3.1具体树实现树表示我们给出了§ 2中介绍的抽象树堆的具体表示。考虑图1中描述的抽象树堆。1a.对应的具体树堆如图4所示。每个树节点由节点单元表示，该节点单元具有指向其左兄弟、parent、firstchild、lastchild和右兄弟的指针，其中表示空指针。对于抽象树堆，删除根为n的子树是一个自包含的操作;它不依赖于子树周围的上下文。然而，执行情况并非如此由于每个节点单元保持指向其兄弟的指针，删除n处的子树需要改变其兄弟（有时是父）的输出指针。 在该示例中为必须将节点单元L的右指针重定向到R，反之亦然;只有这样，才能丢弃n处的子树。此外，在实现并发图4：具体的树表示。客户程序deleteTree（l）||deleteTree（n），两个执行线程需要同时访问l和n之间的指针，这需要合适的同步技术。在我们的实现中，我们通过锁定同步对这些指针的访问每个左，第一，最后和右指针都受到保护nR*nuLn r不156P. Gardner等理论计算机科学电子笔记308（2014）147（）个{=============/（）个{：=[]（）：=[]（）（）个{（）个{→第九章d：=[n.first];calldisposeForest（d）;dealloc（n，9）;联系我们procdeleteTreenlocall，u，d，r in//获取所需的指针锁。1.u：= [n.up];lock（n. left）;l：= [n.left];2.if lnullthen lock（l.rightL）elseifunullthen lock（u.firstL）;3.intn = [n];4.如果rnullthen lock（r.leftL）; elseifunullthen lock（u.lastL）;//指针摆动。5.if lnullthen [l.right]：= r elseifunullthen [u.first]：= r6.if r nullthen [r.left]：= l else if unullthen[u.last]：=l//对获取的指针锁进行解锁。7.if lnullthen unlock（l.rightL）elseifunullthen unlock（u.firstL）8.如果rnullthen unlock（r.leftL）else if unullthen unlock（u.lastL）//处理节点n的子树}proc disposeForestn local r，d in如果nnull然后r n. right;call disposeForest r;dn.first;calldisposeForestd;dealloc（n，9）}进程锁定A同时（！CAS（a，0，1））skip;}procunlocka[a]：= 0;}图五. 实现deleteTree（n）和一些辅助程序。由竞争线程预先获取的相应锁（lL，dL，eL，rL）来确定。我们将这些锁称为指针锁。我们将每个树节点表示为一个节点单元，该节点单元由九个连续堆单元组成，n l，u，d，e，r，lL，dL，eL，rL，其中第一个单元包含指向兄弟，父和子的指针，最后四个单元包含指针锁。 选择这种特定表示的主要原因是它类似于WebKit项目6的文档对象模型（DOM）实现中的树节点表示。为了增加可读性，我们分别对n，n1，，n 8写n.l，n.u，，n.rL树实现我们提供了每个抽象树命令的具体实现。 图5显示了deleteTree命令和一些辅助过程的实现。 该实现需要满足关于节点n的兄弟节点的各种情况，例如当n没有左兄弟节点或右兄弟节点时。其余命令的实现在技术报告中给出[18]。注意，这种实现容易出现死锁;这可能发生在我们的示例程序deleteTree（l）中||deleteTree（n）当l和n是相邻的兄弟时。我们在这里关注这个简单的实现，因为它足以描述我们的想法。我们在[18]中讨论了无死锁实现6然而，WebKit只 支持顺序DOM操作，不使用锁。P. Gardner等理论计算机科学电子笔记308（2014）147157πUnlocked（ R，x）解锁锁定（R，x）1（）[U]（）线程取（x）LU1锁定，将能力[U]R移动到线程关联的动作A（●）11)并且锁定螺纹要求解锁能力。该动作的非零能力（例如能力[L]R对于π>0）。的11CH<$×MH，●σ×●CH，0σ×0CH），其中×表示标准笛卡尔投影。π3.2具体树实现的推理回想一下，两个兄弟节点（有时是父节点和子节点）之间的指针是两个节点都可以访问的共享资源。我们使用并发抽象谓词（CAP）[1]来管理这种共享。并发抽象谓词在CAP中，状态被建模为一对由线程本地状态和共享状态组成的状态。共享状态分为一个集合每个区域都包含国家的一些共享部分。每个区域由区域标识符R标识，并由描述如何操纵区域资源的协议管理。例如，位置x处的锁资源可以通过以下方式指定：lock（x）{\displaystyle\lock（x）} [L]RRT（R，x）其中未锁定R，x x0R和锁定R，x x1。这个锁的定义指出，存在一个共享区域R，其中包含位置x处的锁，[L]R来获取它。该区域处于两种状态之一：π（x=0）并且该区域拥有解锁它的全部能力[U]R;或者该锁是共享区域的协议是通过一组动作来指定的，例如锁的动作和。线程可以执行一个动作，如果它有在锁区域上允许的动作在T（R，x）中声明：T（R，x）<${L∶（x<$0<$[U]R）<$x<$1U∶ x<$1<$（x<$0<$[U]R）与L关联的操作将共享区域的状态从未锁定更改为withU的行为是双重的，将[U ]R从本地状态返回到共享区域。1CAP分离代数的定义在[1，6]中给出。它提供了一组仪表状态MH，包括本地状态，共享状态和动作关系，捕捉共享状态可以被操纵的方式。该定义由用于描述局部状态的底层分离代数参数化。在本文中，我们使用CAP分离代数实例化标准的分数堆分离代数。定义3.1CAP分离代数，用分数堆sep-aSrAationna（lgebra，是CHMH，CH，0CH .CAP态的分离代数为回想一下，我们的推理基于视图框架[6]，该框架提供了关于由一组原子命令及其公理化参数化的通用编程语言的一般推理。定义3.2让ATOMH是原子堆命令的集合，包括：赋值、值查找、内存分配/释放以及比较和设置158P. Gardner等理论计算机科学电子笔记308（2014）147Xn不我是Lxuxn不Rx（A）∶→一M）是f的前/后条件。HPROG（Def. 3.2），一个共轭三元组是Ω<$ {p}C{q}。Ω∈PEnv是HCH H的集合R堆R lijr，其中ch可以被e分割为h●其中h< $ R <$l<$x<$r121T≜ ↦⊗构建CAS。我们为用集合A到H实例化的视图编程语言生成的程序集编写PROGH让AXIOMH成为标准这些命令的分离逻辑公理化集合基于分数堆分离代数。视图框架为PROGH提供了相关的推理。定义3.3给定CAP分离代数CH（定义3.1），原子堆命令A TOMH和它们的公理化A XIOMH，用于分数堆的CAP库CH定 义 为：CHCH，A TOMH，A XIOMH。定义3.4给定CAP状态p，q∈ N（N×MH）（定义3.1）和程序C∈过程规范f∶p1<$q1，其中f是过程名，p1，q1∈ n（n × n在§ 4中，我们定义了库细化τTC H用于抽象树库T（定义2.9）和混凝土CAP库C H（定义3.3）。作为定义τ的第一步，我们识别对应于抽象树片段的具体CAP状态。这些具体的CAP状态依赖于将抽象地址与具体指针链接起来的接口函数I τ。接口功能。 图图4示出了根地址处的完整抽象树的具体堆表示 然而，许多抽象树命令（例如deleteTree）是使用树片段而不是完整的树来指定的。我们需要理解树碎片的具体表示当使用抽象分配拆分抽象树堆时，组成堆对彼此的形状是不可知的。 例如，考虑抽象树和h2X我J.抽象树堆h1没有体现出对树放在x内;对h2作必要的修改。在具体层面上，位置是不同的。h2的具体表示依赖于来自h1的具体表示的附加知识，因为节点i的表示包括指向其左兄弟节点（l）和父节点（u）的指针。 因此，当使用抽象地址来描述抽象堆时，我们需要来自具体堆的补充信息。我们追踪这个额外的与每个抽象地址x∈ 通过一个骗局-混凝土界面考虑图6，它描绘了一个抽象树在抽象单元x（左）和它的具体表示（右），假设一个界面函数I τ。在具体的表示中，实线表示-重新发送本地保存的资源，例如节点n、其向上指针和子树t，而虚线表示共享资源，例如节点n和其兄弟节点之间的指针一个具体的入接口记录了第一个（i）和最后一个（j）节点森林的具体表现，图6：树木碎片。在我们的例子中，in-interface是in（n，n）。一个具体的外接口P. Gardner等理论计算机科学电子笔记308（2014）147159·ICTreeIτ（t）（q，j）（p，u，r）2（）（R）（）（）（）（）（）（）·（）=（）（）=（）（）（）（=）（=）（）=（）（）=（）≜()()τ我出去了（AAddinoutOUT）。接口函数的集合是II×I。τ τR（）⊗∅⊗在根地址R处的树片段t。谓词CTreeIτ（t）（x）提供了一个（）（）（）（R）指针等式断言ir简单地声明第一个节点的地址<$左（n，l，u）<$前（n，d）<$后（n，e）<$右（n，r，u）<$∅τττCTreeIτ ti，j. ICTreeIτ t i，j null，null，nullCTreeIτ t xICTreeIτ t ix，jx lx，ux，rxIτinxstecix，jx Iτoutxsteclx，ux，rxICTreeIτi，j l，u，r istecr jsteclICTreeIτ xi，j l，u，r Iτinxsteci，j Iτoutx stecl，u，rICTreeIτ（t1<$t2）（i，j）（l，u，r）<$p，q. ICTreeIτ（t1）（i，p）（l，u，q）IC TreeIτ（n[t]）（i，j）（l，u，r）i=stecj=stecnn.u→ud，e.⎞TreeIτ（t）（d，e）（null，n，null）图第七章抽象树堆的CAP表示：我们为a=b的树堆写一个树堆b。记录父节点（u）和紧挨着抽象地址x的左边（l）和右边（r）放置的节点的地址;在我们的示例中，输出接口是out lx，ux，rx。界面函数Iτ将x映射到in，out。定义3.5混凝土输入和输出界面的集合定义如下：Inτ（N+ {null}）2OUTτ（N+ {null}）3输入和输出接口函数的集合由Iinπ（AADD<$Inτ）定义，图7定义了并发抽象谓词，用于描述抽象树堆的具体表示，由界面函数I τ参数化。 关于CTreeIτ 不谓词提供了具体的表示抽象地址x处的树片段的具体表示。这两个谓词都是使用ICTree谓词定义的，ICTree谓词由Iτ确定的输入和输出接口索引。对于，out-interface为null，null，null。 此时内界面是未知的，因此是存在性量化的。它的值稍后使用ICTree谓词找到。x的界面由界面函数Iτ决定。我们现在按照归纳定义的情况，用显式的输入和输出接口参数i，j和l，u，r来描述ICTree谓词。ICTreeIτ（）在具体的堆表示中没有资源，只是一些森林中的单元格等于树右侧的节点单元格的地址;对于j和l也是如此。这是为了确保树的正确具体表示，如t1t2.ICTreeIτ（x）在具体的堆表示中没有资源，160P. Gardner等理论计算机科学电子笔记308（2014）147→≐≐⋐[客户线程的本地状态持有见证能力[W]的完全权限。⊗∗与该区域相关的锁定能力[L]n，l，u 这个谓词描述了节点n和它的（=/）↦∗↦由isRLock（l，n，u，0. 5）谓词。另一方面，如果n不==/Ru（isDL ock（u，n，0. （5））。最后，如果n是第一个在rotadress下面的child，并且完全解锁能力（[U]Rnl）和可解锁资源在该区域中。，因此它的左兄弟和父都对应于null（l=u=null），1抽象地址x和Iτ给出的接口之间的适当连接。ICTreeIτ（t1t2）这是简单的组成抽象子树的具体表示的组合，给出了适当的接口选择。ICTreeIτ（n t）前两行提供节点n的具体表示，最后一行表示子树t。对于子树，具体的表示是直接的。 对于节点，i因为只有一棵树在森林里具体表示拥有父指针的全部所有权n.u u，因为没有来自其他节点的对该资源的竞争。左、右、第一和最后谓词表示与左兄弟、右兄弟、第一个孩子和最后一个孩子相关联的指针和锁，它们与附近节点的表示竞争，因此必须共享。我们在这里给出了