安全的原子分裂方法

理论计算机科学电子笔记155（2006）43-60www.elsevier.com/locate/entcs一种安全的原子分裂方法C. B. 琼斯1计算机科学泰恩河畔纽卡斯尔大学英国纽卡斯尔摘要本文的目的是作出贡献（组合）并发程序的开发方法。涉及的主题包括干扰，原子性，可观测性和粒度。该文件提出了一些要求的方法来开发系统的关键词：并发程序，原子动作，可观察性，粒度。1引言如果一个动作被“原子地”执行并发的麻烦在于必须容忍干扰。在共享状态程序中，一个动作必须达到某种要求的结果，即使它的状态可能被其他干扰进程改变。这里的目的是要论证，有一种开发并发程序的有用方法，它明确地使用“原子性的概念”作为抽象，然后允许“安全地分裂原子”的开发步骤。这种发展过程可以称为“细化原子性”。之一1. ncl.ac.uk1571-0661© 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.05144C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）43使这种方法有趣的是它被广泛使用：当实现故意重叠事务的执行时，大部分数据库实现都是关于保持原子性的这里所寻求的是一种通用的开发方法，它具有开发程序的其他形式化方法的特性。2干扰将编程语言归类为“命令式”的是其程序改变某种形式的“状态”的能力。例如，请考虑（VDM–从包含空集的初始状态开始，操作ENQ和DEQ（后者受其先决条件的约束）可以以任何顺序执行;这两个操作都显示为（ext wr）改变状态（队列）。操作ENQ接受一个参数但不提供结果，而DEQ不接受参数并提供结果。函数mins假设从它的（非空集）参数中传递最小值重要的是要认识到，像图1中这样的具体说明的意图是外部行为是所定义的。内部状态不需要用set数据类型实现。 关键点是，假设观察优先级队列行为的唯一方法是使用所述操作的（输入和）输出术语图1的后置条件定义了可接受的最终结果，对于顺序程序，原子性问题得到了解决。VDM使用短语这些规则类似于后置条件不需要在单个步骤中执行，这样的执行只能被认为是原子的，在这个意义上，没有干扰开发被期望创建一个在许多步骤中执行的程序;但是对于顺序程序，我们忽略它们执行过程中的干扰由于下面使用了优先级队列的例子，因此值得强调一下实现的范围：例如，实现者可以通过向无序的状态-DEQ需要确定最小的元素;在另一个极端，在一些实现中，ENQ需要更多的时间将新元素放入有序的数据结构中，以便DEQ快速响应。C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）4345ENQ（新：X）ext wrqueue：X-setpostqueue=q-u−e−u−e{new}DEQ（）r：Xext wrqueue：X-setprequeue/={}postr=mins（q-u−e−u−e）qqe=q-u−e−u−e−{r}Fig. 1. 优先级队列第5节展示了如何使用并发来使两个操作都快速响应。数据细化和操作分解都是换句话说，人们可以证明设计的一个步骤是正确的，并且知道-干扰使得很难找到并发系统的组合开发“Owicki/Gries方法”[ 17 ]扩展了类似Hoare的方法来处理并发性，但由此产生的方法是非组合的，在这个意义上，如果独立过程的证明最终没有达到“干扰自由”的性质，那么它们可能不得不这是努力的组合性，这导致作者寻找的方式来记录使用依赖和保证条件的干扰。本质上，依赖条件记录了实现必须容忍的对其状态的干扰，而保证条件记录了对干扰的限制组件可以生成。依赖条件和保证条件都与先决条件一样另一方面，担保条件类似于后置条件，因为它们记录了创建程序的义务。像[10，21]这样的论文包含了证明规则，表明如果组件被开发以满足其规范，则分解为并行过程将是正确的具体方法的细节各不相同，在这里并不重要;[6]包含不同成分的详细比较。46C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）43−→−→和非合成方法。3SOS中的原子性本文更感兴趣的是干涉和原子性之间的联系在这里查看描述语言语义的技术的一个原因是表明SOS [18]提供了一种直接的方法来形式化粒度等方面的许多点。在第6节中，当解决证明设计方法的问题时，可以看到探索SOS的更强有力的证明人们可以将SOS描述视为定义程序文本和状态对之间的关系;因此，−→s ：P（（语句×）×（语句×））共享变量并发的情况是，当多个控制线程可以读取和/或写入状态的同一部分时，会发生干扰。作为一个简单的例子，考虑并行执行两个赋值序列。现在忽略表达式计算中的非确定性的可能性，使用eval：表达式×值→值从左序列头部开始的赋值语句的（原子）执行表示为v=eval（e，σ）（[x←e] arestleft||右，σ）s（restleft||右，σ <${x <$→ v}）根据右序列的明显对称规则v=eval（e，σ）（左）||[x←e] a restright，σ）s（左）||restright，σ <${x <$→ v}）这说明了非确定性如何根据两个并行流中语句的执行顺序而产生因此（x ← x 2; x ← x 3）||（x ← x 4; x ← x 5）如果x的初始值为1，则将x的最终值设置为阶乘5，无论赋值语句交错的顺序如何。而当x从1（x←x + 1）||（x←x 2）可以让x为3或4。C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）4347虽然这里用赋值语句说明了基本点，但这不应掩盖这样一个事实，即相同的问题出现在不同的语言层次上。干扰可能表现为单独的程序访问共享文件或单独的附录A概述了第5节中使用的并发OOL的SOS。4粒度和细化上一节中的操作语义显示了原子执行的赋值状态。也就是说，如果left的head（比如x←e）正在执行，那么在e的求值开始和x的变化之间没有状态变化;right也不能在x变化的同时观察x对于一个有用的编程语言来说，这样的原子性假设是不现实的，因为它的实现成本非常高（就信号量设置而言）。为了避免两个线程引用共享变量所带来的问题，一种尝试是说任何赋值语句最多可以使用（在左边或右边的上下文中）一个共享变量。这有时被称为“雷诺规则”。它有自己明显的缺点，因为任何形式的声明必须重写为x←e（x）local←e（x）;x←local即使程序的逻辑表明在该上下文中，没有其他线程可以改变x。更严重的是，这个想法没有给出如何处理不能被原子访问和/或改变的变量的线索：例如考虑数组或记录赋值（但假设数字可以被不可分割的机器操作改变前面的部分解释了依赖和保证条件是如何作为关于干扰的假设的，但是引用的关于这种开发并发程序的方法的论文只暗示了“原子性”的问题在像简单（布尔）开关这样的情况下，一个依赖条件声明环境永远不会将myswitch设置为false-−−myswitch 电子开关是安全的在使用依赖/保证条件的程序开发中，经常需要条件，比如说，状态变量单调递减，并且在原子地实现变化的意义上可以更微妙，48C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）43对大多数编程语言都很难理解在许多这样的情况下，与数据重新定义有着迷人的相互作用在[17]中有一个例子，其中两个（或多个）并行进程正在搜索谓词p（A（i））保持的数组A的最小索引（i）。在[9]中给出了这个例子的推广的合成发展开发中的一个关键点是，两个过程都依赖于并保证找到这样一个值的最低索引t单调递减（t≤--t）。如果t本身是一个共享变量，即使是在v≤t的情况下，像t←v这样的赋值不会安全地减少t，执行开始，因为干扰可能将t减小到小于v.实际上在[9]中所做的是将t具体化为两个变量v1和v2，并使用retrieve函数t=min（v1，v2）(The第i个进程可以写vi;任何一个进程都可以读vj。第i个进程现在可以通过改变vi来减少t，而不用担心干扰，也不用对赋值语句等事情进行原子性假设。这一观察似乎很重要，因为它在其他例子中得到了回应-其中一些例子要复杂得多。事实上，像辛普森的“四槽”算法这样极其微妙的“异步通信机制”（ACM）可以这样理解。ACM问题的本质是有一个共享变量，进程可以在不等待任何锁的情况下对该变量进行读写如果不假设整个变量的读写是原子的，这将变得非常困难。Hugo Simpson已经表明-论文[7]使用数据修正开发了这个例子在同时出现的“埃拉托斯特尼筛”的发展中，也可以看到数据细化和干扰之间的同样联系其目的是安排一些共享集s被设置为恰好是素数的集合，直到某个值n。序贯筛选首先会去除2的所有倍数（2及以上）然后找到s中的下一个最低值，并去除其倍数，以此类推，直到n的平方根。并行版本的想法是使用一系列并行进程Rem（i）每个Rem过程的规范（i）不能定义一个精确的集合，该集合将在过程完成后存在（因为其他过程也会删除）。（ii）可以指定它的所有倍数都应该被删除;(iii)只能在没有人重新插入删除的值的依赖条件下实现这一点;（iv）必须保证自己永远不会重新插入值;（v）必须保证C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）4349只是为了去除复合材料。这个例子的完整发展可以在几篇被引用的论文中找到。在这里，兴趣在于集合s的具体化。即使有一种编程语言支持set类型的变量，s：=s− {i<$n}在存在干扰的情况下将不满足保证条件（例如，已经访问S以计算集合差异，另一个过程可以移除某个复合j，然后将通过对S的分配来重新插入该复合j）。同样，它是s的数据表示的选择，使事情工作。本质上，s由位向量表示;可以通过将相应的位设置为false来删除集合中的元素;假设此操作成为原子。5安全地分裂原子如果要为并发程序找到一种开发方法，那么值得回顾一下数据重新定义和操作分解（目前，在该标题下，使用依赖/保证条件开发并发程序）。这些方法在有用的意义上是组合的从一个简短的规范，关键的早期设计决策可以记录和公正的知识，进一步，更详细的步骤不会无效的早期决策。开发过程，无论多么正式，创建一个完整的程序，然后接受一些最终的大规模的请注意，无论事后是否检查是测试、模型检查甚至是证明。这正是Owicki最终的“干扰自由”证明的问题因此，我们希望找到开发并发程序的方法，这些程序也是组合的。这里所建议的是设计，好像事情将是原子的，然后允许过程的步骤重叠。这种方法可以称为显然，有些情况下它是微不足道的，有些情况下它是无效的。现在几乎所有的程序都运行在共享硬件资源的操作系统上;甚至物理内存本身也通过分页方案共享;但是操作系统有责任保持这些程序完全独立，不相互干扰大多数情况下，他们成功地做到了这一点。50C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）43原子性可以在没有干扰危险的地方放松另一方面，为了计算阶乘5，在第2一旦人们意识到“原子性的概念”的力量，很明显，它是理解大量核心并发思想的意图的非常有用的方法。2尽管这种抽象看起来很有用，但没有一种普遍的方法可以证明随后的原子分裂是安全的。数据库文献（参考文献见[2]）是有趣的，但其中所展示的方法是针对其特定应用而磨练的，不会超过一般的开发方法。另一个领域的工作示例值得考虑作为开发方法的存在证明。[12]中原子性细化的例子满足了开发方法所寻求的性质它可以应用于图1中给出的规范的开发。（这个例子比以前的文章中的例子简单特别是一些新的意见，对可观性的进一步工作，本文的最后一节勾勒了指针。在开发依赖/保证推理之后，它被认为是“沉重的我们需要的是一种明确的方法来表明哪里不可能发生干扰，并将干扰证明的使用限制在程序的最小部分。面向对象的语言--基于类的OOL使程序设计者能够更好地控制干扰的程度：本地“实例”变量只能通过本地方法访问;引用（即，点-对象之间共享的资源（资源到实例）控制干涉的程度。在早期的论文中，研究了一种语言（πoβλ），它要求在任何对象实例中在一个时间点上只有一个方法是活动的。加上为了识别不能被复制的私有引用（以及其他限制）[2]从某种意义上说，数据库的实现就是实现一个原子性的集合。 很容易为事务其示出了（从一组等待事务中）选择并原子地执行一个实现者的任务是实现这种语义所描述的可能（非确定性）结果之一由于事务可以运行（相对）较长的时间，因此实现实际上需要重叠它们的处理。但这必须以一种不引入任何新结果的方式进行（例如由于数据库上的争用而损失银行C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）4351“islands”对于图1中指定的优先级队列，数据重新定义的一个简单步骤是用有序的值序列表示集合。开发（通过顺序操作分解）（πoβλ）程序在图2和3中顺序地将一个值插入其正确的位置现在的想法是将并发性引入到这样的顺序程序中。图3显示了insert方法头部的return与顺序程序相比，这个版本的insert将立即从集合点释放其客户端，并且客户端可以与Priq元素的链式序列内的活动并行进行此外，只要在l元素中调用insert，活动就可以并行地沿着序列向下传播。这些转换依赖于引用的属性一个初步的定义确定了可以（不可以）使用私有引用做什么。私有引用被定义为永远不会被“复制”，也不会有通用（非共享）引用传递给它-既不输入也不输出（因为不能传递私有引用，这限制了对“不可变”对象的一个等价性是：return（e）等于return（e）;S提供• 不包含return或delegate语句，并且总是终止;• e是简单表达式，并且不被S约束;并且• S调用的每个方法都属于私有引用所到达的对象并不是所有的程序都打算终止;即使它们是，终止也不是一个语法上可检查的属性;但是在开发方法的精神(This然而，这一点确实使人们怀疑所考虑的那种等价是否另一个等价性是：雷肯湖m（x）等价于委托l。m（x），提供• L. m（x）终止;以及• l是唯一的引用。3由于变量和方法的名称在Ap- pendixB中用于语义表达式，因此有机会使用单字符名称。52C.B. Jones/Electronic Notes in Theoretical Computer Science 155（2006）43舱Qvarsv：N<$0;l：private referenceQ<$nil;i（n：N）方法开始如果l=nil，则（l<$newQ;v<$n）埃 尔 夫 湾 < ， 然 后湖。i（n）else（l.i（v）;v←n）fi;返回端r（）方法r：N...c（n：N）方法 r：B如果l=nil，则返回（false）elifv

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