ǁ理论计算机科学电子笔记265（2010）177-195www.elsevier.com/locate/entcs公平、资源和分离斯蒂芬·布鲁克斯美国匹兹堡卡内基梅隆大学计算机科学系摘要Fair交织 算法 是共享内存并行 程序指称语义模型中的一个基本规则，它从Park的迹语义出发，基于一个fairmerge关系，使得（α，β，γ）∈ fairmerge当且仅当γ可以通过交织α和β得到.帕克的公式化的fairmerge使用嵌套的最大和最小固定点的单调函数的痕迹，但他指出，不动点归纳原则似乎不适合证明自然的代数性质，如结合性。这样的性质是验证程序等价性的直观法则和支持层次分析所必需的的程序。 最近的模型和逻辑共享内存程序与可变状态和指针的基础上，并扩展公园的基础上，强调资源和逻辑规则，体现分离原则。例如，并发分离逻辑是基于fairmerge的一个竞争检测、资源敏感的变体。对于这些模型中使用的交织类型，以及其他更复杂的fairmerge变体，代数困难加剧了。而不是搜索特设技术，我们在这里开发一个通用的框架来定义k元fairmerge运算符，首先通过选择资源模型进行参数化，然后通过选择冲突或干扰关系进行细化。 我们的公式避免了嵌套的固定点，并支持基于迹的有限前缀长度的归纳推理。我们证明了广义结合性的性质，并获得结合性证明先验模型作为一个副产品。关键词：并发，共享内存，指称语义，不动点归纳，公平性，资源，分离逻辑1引言公平执行是对并发程序的活性属性进行推理的一个关键假设[18]。事实上，公平性已经在共享内存并行程序的指称语义模型的定义中奠定了基础，从Keller [14]和Park在Park 更正式地说，帕克在迹上引入了一个（三元）公平合并关系，其特征是迹集的完备格的卡耐基积上单调函数的最大和最小不动点的嵌套组合，按分量集包含排序。这个关系被设计成使得（α，β，γ）∈fairmerge当且仅当γ是1电子邮件：brookes@cs.cmu.edu1571-0661 © 2010 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.08.011178S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177ǁ ǁ ǁǁ所有的α与所有的β交错。 正如帕克所指出的，固定点归纳原则 在试图建立自然的代数性质时，例如Fairmerge的结合性，似乎不合适。这样的属性需要验证程序等价的自然法则，例如c1（c2c3）=（c1c2）c3，以及关于并行组合和局部声明范围之间的相互作用的法则。这些规律有助于支持过程网络的层次分析。Park基于迭代连接推导出了一个等价的Fairmerge关系式，但他指出需要额外的（或替代的）见解来证明结合性和其他属性[22]。Park最近的共享内存语言的模型和逻辑涉及多表状态和指针也建立在Park 这导致了依赖于资源敏感和种族检测形式的公平交织的语义模型的发展[8，9]。 这些模型在建立一致性的合理性方面至关重要， 租金分离逻辑[8，17]。这些模型，如最初所提出的，也支持代数问题，加剧了额外的技术复杂性，需要处理资源会计和竞争检测。此外，Park的fairmerge的结合性证明 理想情况下，我们需要一个连贯的、易于处理的数学公平帐户 这有利于代数推理，更好地支持程序等价性定律的验证。我们在这里解决这些问题，通过开发一个抽象的和一般的公平性框架，参数化的资源模型的选择和行动的干扰或冲突关系，假设有一些直观的自然属性。在我们的方法中的一个关键因素是从公园的2元fairmerge的一个统一的家庭k元fairmerge关系密切相关的属性的概括我们避免处理固定点运算符，而是处理迹的有限前缀，并支持基于迹长2的归纳的推理风格。我们证明了一个广义结合定理适用于这个框架的所有实例早期的语义模型可以作为我们的公平框架的实例进行重铸，因此我们作为副产品获得了这些模型的关联性证明该框架足够健壮，可以包含基于信号量和其他同步机制的资源模型，以及涉及权限的模型。2背景我们在一个抽象的环境中开发了我们框架的主要成分，通过使用任意的（非空的）我们将使用λ作为一个元变量，其范围为λ。设m是有限序列的集合，2我们对前缀的强调并不与fairmerge在以下方面是非单调的这一事实相矛盾：[20 ]第20话：在路上我们的研究结果与长期以来的结论相反，从非单调性来看，公平性超出了指称的范围。在我们的方法中，缺乏单调性是不相关的。S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177179∪→[≤⊆×≥对于来自于的元素，+是非空有限序列的集合，而ω是（可数的）无限序列的集合。设表示空序列。跟踪是一个有限或无限的动作序列。 设∞ = ω是所有迹的集合。我 们 使用α，β，γ作为元变量，其范围超过∞。当α是非空的有限迹时，令last（α）是由α的最终元素组成的单例迹，令last（α）=α。对于α，β∈∞，我们让αβ表示α和β的级联;当α无限时，αβ=α。连接是结合的，空序列是一个单位：（αβ）γ=α（βγ）和α γ=α=α。当α∈∞且h：∞时，设映射hα是将h应用于α中的元素出现所得到的序列.函数映射具有通常的性质：映射h=，映射h（λα）=（h λ）（映射h α），映射h（αβ）=（映射h α）（映射h β）。对于迹α和α的子集A，我们将α的子序列记为α A由A的动作组成。定义2.1对于迹α，设pre（α）是α的有限个前缀的集合，按前缀关系排序：α1<α2i ∈α1是α 2的真前缀。我们也写α1α2，当α1= α2或α1<α2时，我们说α 1是α 2的前缀。显然，（pre（α），<）是一个线性序，元素最少;α属于pre（α）当且仅当α是有限的。我们可以从它的前缀中恢复α，通过按前缀顺序列出pre（α）的成员并连接它们的最后一个元素：α=map last（pre（α））。注意，如果pre（α）=pre（β），则α=β。定义2.2函数f：pre（α）→pre（β）严格单调当且仅当f（α 1）=f（α 2）且对所有α1<α2∈pre（α），f（α1）f（α2）.<对于任何函数h：n → n，很容易看出pre（map h α）= {map h αJ|αJ∈pre（α）}，当α1<α2 时，也有映射h α1映射h α2.<因此映射h：pre（α）→pre（maph α）是严格单调的。定义2.3当f：pre（α）→pre（β）严格单调时，我们定义f−1（βJ）= max {αJ∈ pre（α）|f（αJ）≤ βJ}。如果f是严格单调的，则f−1是单调的（但不一定是严格单调的）：只要β1≤β2∈pre（β），f−1（β1）≤f−1（β2）。还应注意，对于所有αJ∈pre（α），f−1（f（αJ））=αJ;对所有βJ∈pre（β），f（f−1（βJ））≤ βJ。使用这些成分，我们现在可以定义一个家庭的家庭，|k≥ 1阶k元公平归并关系，直观地读作（（α1，...，αk），β）∈FM ki <$β是序列α1，.，αk。定义2.4k元公平合并关系FM k（k∞）k∞，对于k 1，由下式给出：（（α1，...，αk），β）∈FM k有严格单调函数f1：pre（α1）→ pre（β），...，fk：pre（αk）→ pre（β）180S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177⟨|⟩具有以下特性：(a) 对于所有i j，rge（fi）∈rge（fj）={f}。(b) pre（β）=rge（f1）· · ·rge（fk）.(c) 对于所有i和所有αJ∈pre（αi），last（fi（αJ））=last（αJ）。我们将引用严格单调函数（f1，...，fk）与所指示的类型和属性一起作为用于合并α1，.，αk转化为β。调度函数指定α1，…，αk产生β，通过为β中的每个元素出现描述α1.αk。单调性和（a）、（b）和（c）所施加的约束确保β中的每个元素出现都来自α1，.，αk，来自每个α i的每个元素出现在α中，并且来自每个α i的元素出现的相对顺序被保持。例2.5设={0， 1}。(i) （（0ω，1ω），β）∈FM2当且仅当β是包含无限多个0和无限多个1的0和1的无限序列。这很容易从FM 2的定义中得出，因为0 ω的每个非空有限前缀0n必须生成一个以0结尾的β的不同前缀，而1 ω的每个非空前缀1m必须生成一个以1结尾的β的不同前缀。在这个简单的例子中，对于每个这样的轨迹β，存在唯一的调度。(ii) （（0ω，0ω），β）∈FM2当且仅当β=0ω. 在这种情况下，有无限多个可能的时间表，因为β中每一个出现的0都可以从第一个输入序列或第二个输入序列中选择;每一个时间表的选择都会产生相同的结果迹。(iii) ((0ω，1），0ω）不属于FM2，因为0ω没有以1结尾的前缀，所以没有办法定义从pre（1）到pre（0ω）的调度函数接下来，我们确定了关系族FMkk >0的一些明显的性质。非正式地，我们可以总结说，fairmerge在“输入”迹的置换下是不变的此外，空迹在公平合并中没有贡献。我们还隔离了一对属性，表示公平合并和串联操作之间的自然连接的痕迹。引理2.6关系FM k满足以下性质：（i）如果（（α1，...，αk），β）∈FM k且π：{1，.，k} → {1，...，k}是a置换，则（（απ1，...，απk），β）∈FM k.（ii）如果h：α → α且（（α1，...，αk），β）∈FM k，则（（map h α1，.，映射h αk），映射h β）∈FM k.证据（一）显而易见。对于（ii），如果（f1，...，fk）是（（α1，...，αk），β）我们可以定义一个时间表（g1，.， gk）对于（（map h α1，.， 映射hαk），映射h β），设gi（映射h αJ）=映射h（fi（αJ）），其中1 ≤i≤k且αJ∈ pre（αi）.QS. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177181≥≤引理2.7空序列在合并中起着微不足道的作用。(i) （（，α1，.，αk），β）∈FM k+1i <$（（α1，.，αk），β）∈FM k.（ii）（（α1，.，αk），α k）∈FM k当且仅当每个αi都是α i。证据 这些结果是由pre（ε）={ε}这一事实简单地得出的。Q定理2.8k元fairmerge关系FMk，对于k1，满足以下“prefix/suprix”和“concatenation”性质：(i) 如果（（α1，...，αk），β）∈ FMk，βJ∈ pre（β）和β= βJβJJ，则有pefixesα1J∈p re（α1）， . ，αkJ∈p re（αk），其中子集α1J J， . ，αkJJ，使得α1 为 α1Jα1J J， . ，αk= αkJαkJJ，其中，（（α1J， . ，αkJ），βJ）∈FMk和（（α1J J， . ，αkJ J），βJ J）∈FMk.(ii) 如果（（α1，… ，αkJ），βJ）∈FMk，（（α1J J， . ，αkJJ），βJJ）∈FMk，且βJ是有限的，则（（α1Jα1J J， .. . ，αkαkJ），βJβJ）∈FMk.证据 为 (i)、假设 （f1，.，（fk） 是 一 附表 为 （（α1，...，αk），β）并让β = βJβJJ，其中βJ有限。如果βJ= β（所以βJJ= β），我们可以取αiJ= αi，αiJJ i=1，.，k，结果由引理2.7平凡地保持。其他-明智地，设i是βJ∈rge（fi）的（唯一）索引such，并且设αjJ=fj−1（βJ）对于j=1， . ，k. 则fi（αIJ） =βJ，并且对于ji =i，e有fi （αIJ）<βJ。F1的限制， … ，fk到pre （α1，J）， . ，pre（αk， J）形成对于（（α1， J， .. . ，αkJ），βJ），所以（（α1J， . ，αkJ），βJ）∈FMk. 令α1J J， . ，αkJJ和βJJ是对应于α1J， . ，αkJ和βJ，使得α1=α1Jα1J J， . ，αk=αkJαkJ J，以及β=βJβJ J。的功能g1：p re（α1J J）→p re（βJ J）， . ，gk：pre（αKJJ）→pre（βJJ），使得gj（αJJ）=fj（αJJαJJ），对each j和eachαJJ∈pre（αJJ），是严格单调的，充分条件s（a），（b）和（c）. 所以（g1， . ，gk）是对于（（α1，J， . ，αkJ J），βJ J），表明（（α1J J， . ，αkJ J），βJ J）∈FMk，根据需要。F或（ii），假设βJ是有限的，（f1， … ，fk）是（（α1，J， . ，αkJ），βJ），和（g1， . ，gk）是对于（（α1，J， . ，αkJ J），βJ J）.则eachαiJ是有限的，并且we可以定义函数hi：pre（αiJαiJ J）→pre（βJβJ J）by： hi（αJ）=fi（αJ）当αJ当αjj∈pre（αijj）时，hi （αIJJ） =gi （αJJ）. 这些函数定义明确，严格单调，并满足（a），（b）和（c）。所以（h1，.，h，k）是针对（（α1Jα1J， . ，αkJαkJ J），βJβJ J）。Q接下来的两个结果表明，对于k= 1和k= 2，我们的定义在相应的arity上产生了预期的 fairmerge关系：一元fairmergeFM1是迹上的恒等关系，二元fairmergeFM2与Park定理2.9 FM 1={（（α），α）|α ∈ <$∞}。证据图3：显然pre（α）上的恒等函数是（（α），α）的时间表。所以{((α），α）|α ∈ <$∞} FM 1. 相反，注意如果（（α），β）∈FM1，182S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177f：pre（α）→pre（β）是严格单调的，rge（f）=pre（β），并且对所有的αJ∈pre（α），[3]也许是学究式的，我们在符号上区分了1元组（α）和迹α。S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177183⊆××T T{，，}T T T→→···last（f（αJ））=last（αJ），很容易通过对αJ的长度的归纳证明，f（αJ）=αJ. 因此，β=α。Q定理2.10FM2与Park的fairmerge关系相吻合证据 帕克关系式Σ ∞ [22 ]可以用下面的公式来表示。 首先将迹上的级联运算αβ扩展到迹的三元组，按分量：（α1，α2，α3）（β1，β2，β3）=（α1β1，α2β2，α3β3）;然后按点扩展到三元组的集合。对于一组三元组，设0 =（），n+1 = n，其中n≥0，且T=∞n=0Tn. 然后T满足以下方程：T={（α1.αnβ1βn，γ1...γn）|n ≥ 0。我是阿吉1 ≤ i ≤ n <$（αi，βi，γi）∈ T}.如果T中的每个三元组都有非空分支，即无论何时（α，β，γ）∈T，我们有α/，β/=α/，γ/=α/，我们可以定义Tω={（α1. αn...， β1... βn...， γ1... γn.. . ）的方式|Eli ≥ 0。 （αi，βi，γi）∈ T}.(TheT上的非空约束意味着我们避免了退化项ω。设A、B、C为：A ={（α，α，α）|α∈<$∞}<${（<$，β，β）|β∈ ∞}B = {（λ，λ，λ）|C = {（λ，λ，λ）|λ ∈ λ}。如Park所示，fairmerge=（B <$C）<$A <$（B<$CC<$B）ω。（注意，每个三元组（α，β，γ）∈B<$CC<$B都有非空分量，所以这里使用的无限次迭代是定义良好的。我们证明了（（α，β），γ）∈FM2i ∈（α，β，γ）∈fairmerge，如下.设（（α，β），γ）∈FM2.设f：pre（α）pre（γ），g：pre（β）pre（γ）构成（（α，β），γ）的一个时间表. 很容易证明，如果rge（f）和rge（g）中 至 少有 一 个 是 有限的，则（α，β，γ）∈（B <$C）<$A，如果rge（f）和rge（g）都是无限的，则（α，β，γ）∈（B<$CC<$B）ω。因此，（α，β，γ）∈fairmerge，如所要求的。相反，如果（α，β，γ）∈fairmerge，我们可以为（（α，β），γ）构造一个调度（f，g），表明（（α，β），γ）∈FM2。 细节很简单。Q现在我们来讨论结合性的关键结果，它以一种适当的广义方式来处理k元合并。我们使用诸如α之类的符号来表示轨迹的k元组，依赖于上下文来指定K. 当α1，...，αn是长度为k1，.的元组，kn，我们写α1.αn表示元组长度为k1++kn，通过连接和收缩得到，例如（α，β）（γ，δ）=（α，β，γ，δ）。定理2.11关系FMk具有下列(i) 如果（α1，β1）∈FMk1，.，（αn，βn）∈FMkn和（（β1，...，βn），γ）∈FMn，则（α1.. . αn，γ）∈FMk1+···+kn.(ii) 如果（α1.. . αn，γ）∈FMk1+···+kn 且对每个i，len（αi）=ki，则存在reβ1，...，βn等的（α1，β1）∈FMk1，.， （αn，βn）∈FMkn，184S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177→◦≤ ≤ ≤≤j=1[≤ ≤ [[（（β1，.，βn），γ）∈FM n.证据 对于（i），设（α1，β1）∈FM k1，.，（αn，βn）∈FM kn 和（（β1，...，βn），γ）∈FM n.设f1=（f11，...，f1k1）是（α1，β1）的调度，且令f2，.，fn是（α2，β），.，（αn，βn），对于分量函数具有类似的符号fij。设（g1，.，gn）是（（β1，...，βn），γ）。则定义Fij=gifij，其中1 我n和1 Jki，且令Fi=（Fi1，...，Fiki）。函数Fij：pre（αij）pre（γ）是严格单调的，并且满足预期的性质（a）、（b）和（c），因为fij和gi具有类似的性质。 因此，F1.. . Fn是（α1. . αn，γ），和（α1. . αn，γ）∈FMk1+···+kn.F或（ii），suppose（α1. . αn，γ）∈FMk1+···+kn，对eachi，len（αi）=ki. 让F1... Fn是（α1.αn，γ），其中对于1≤i≤n，每个Fi有形式（Fi1，.，Fiki），且对1 ≤ j ≤ ki，每个Fij都是严格单调函数从pre（αij）到pre（γ）。设rge（Fi）为Kirge（Fij）. 为1i n letβi=map last（pre（γ）rge（Fi）），其中pre（γ）rge（Fi）表示集合属于其中一个调度函数的范围的γ的有限个前缀Fi1，. Fiki，按前缀顺序枚举。然后对于每个i，我们有（αi，βi）∈FM ki，使用Fi作为调度。此外，我们可以获得（（β1，...， βn），γ）通过定义函数gi：pre（βi）→ pre（γ）使得当βJ∈ pre（βi）时，gi（βJ）= Fij（αJ），其中j是唯一索引，αJ∈pre（αij）是唯一前缀使得βJ=map last（pre（Fij（αJ））rge（Fi））。相关的存在性、唯一性、严格单调性以及性质（a）、（b）和（c）由F ij的假设性质和迹βi的定义得出。Q推论2.12Park证据如果（（α1，α2），β）∈FM2且（（β，α3），γ）∈FM2，则根据前面的结果，（（α1，α2，α3），γ）∈FM3.因此有一个δ使得（（α2，α3），δ）∈FM2和（（α1，δ），γ）∈FM2.相反的论点是类似的。由于FM2与Park的fairmerge重合Q使用Park最初的fairmerge固定点公式，甚至从基于迭代级联的fairmerge导出公式中找到结合性的直接证明似乎更困难此外，试图推广Park相反，我们的方法显示了显式处理调度函数的好处，它给出了一个更内涵的前缀由前缀帐户的方式交织是建立在组件跟踪。我们还证明了一些一般的结果，如引理2.6，引理2.7，定理2.8，从公园的fairmerge类似的结果虽然引理2.6和引理2.7的类似物很容易在Park的设置中直接证明S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177185×⟨|⟩⊕⊕Park的工作为许多并发程序的指称模型奠定了基础，每一个模型都采用了某种形式的“公平合并”。“字母表”的选择和交织的种类可能会有所不同，但基本思想与上面概述的一般设置有很多共同之处。例如，在Park的迹中，步骤是表示单个原子动作的结果的（全局）状态对，因此S = S S，其中S是状态的集合;在转换迹模型中，每个步骤表示有限序列的原子动作的结果，并且迹集合在口吃和口吃下是封闭的。在动作跟踪语义模型中，例如[7]动作包括读取i = v和写入i：= v到程序变量，并且动作对底层状态的影响被单独处理。3资源与分离涉及可变状态和指针的共享存储器语言的最新模型和逻辑强调资源和分离原则[17]，并依赖于公平交织的资源敏感形式[8]。定义一个合适的公平合并关系和建立结合性和其他自然属性的任务由于需要考虑资源而加剧。接下来，我们介绍一个简单的资源模型，用抽象的术语和[11]建议的直观公理来表达。（资源模型对应于[11]中的分离代数。我们扩展了我们的框架来包含资源，定义了一个资源敏感的公平合并关系族RFMkk >0，它体现了资源分离：在所有阶段，并行进程“拥有”的资源是“兼容的”。我们可以将先前的资源敏感模型重新构建为该框架的实例。我们将假设资源属于一个集合M，它配备了一个部分二元运算，我们说M中的m1，m2是兼容的，即m1m2被定义。我们还假设M包含一个当e1，e2是包含部分运算的元语言表达式时，我们写e1e2表示e1和e2要么都是未定义的，要么都是有定义的且相等的。定义3.1资源模型是一个部分可交换可消幺半群（M，n， 0），其中n：M×M~ M且0∈M，满足：• m1m2m2m1• m1（m2m3）（m1m2）m3• mm1=mm2m1=m2• m0 = 0 m = m.示例3.2以下是资源模型的示例。(i) 平凡模型：集合{0}，其中0 0 = 0。(ii) 资源集模型：M=Pfinn（R），其中R是一组资源名称，是不相交的并集，0 ={}。186S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177联系我们⊕×αλ►−→(iii) 局部状态模型：设M=Ide~finV是一组状态，其中Ide是标识符的集合，V是可表示值的集合。定义：M M~M通过：s1s2=s1S2第1条dom（s2）= ，设0为空状态读者可以参考[11]以获得资源模型的进一步示例及其在形式化分离的直观概念一个进程执行动作的能力取决于该进程所拥有的资源，也取决于“环境”所拥有的资源，即被假设为并发运行的其他进程所拥有的资源;当一个动作发生时，它可能会影响该进程所拥有的资源。为了描述资源和动作抽象之间的相互作用，我们引入了一个资源赋能的概念，一个形式mm1−→λmJ1的关系，解释为一个有资源的过程m1，在具有资源m的环境中，可以做λ，然后具有资源mJ1。假设使能关系满足一些直观自然的公理，分离和帧特性：进程和环境资源保持分离，保留额外的进程资源，并且不禁用动作的额外环境资源对进程资源没有影响。定义3.3给定一个资源模型（M，N， 0）和一组动作N，使能关系是一个子集NNM×（M× N ×M），具有以下属性：用fix表示法表示：当（m，（m 1，λ，m j 1））∈ → w e写m <$m 1 − → λ m j 1。(i) 如果m<$m1−→λmJ1，则定义m<$m1和m<$mJ1。(ii) 如果m<$m1−→λmJ1且m<$m 1<$m2−→λmJ，则mJ=mJ1<$m2。(iii) 若m<$m1−→λmJ1且m<$m 2<$m1−→λmJ，则mJ=mJ1。(iv) 如果m<$m2<$m1−→λmJ1，则m<$m1−→λmJ1。定义3.4我们将使能归纳地扩展到限定动作序列。当m≠m1被定义，且λ∈λ，α∈λ，• mm1−→• m<$m1−λ−→αM1.mJ2ifm<$m1−→λmJ1和m<$mJ1−→αmj2，对某个mj1∈M.在资源为0的环境中启用是一种特殊情况，直观地对应于不竞争资源的执行 我们说，迹α可从m执行当且仅当存在mJ满足0<$m−→mJ。这些概念以明显的方式延伸到无限的痕迹。最后，我们说一个跟踪α是简单可执行的，如果它是从0可执行的例3.5设M = {0}为平凡资源模型。对于任何集合λ，我们可以定义一个平凡的使能关系，使得0 0 0对所有λ∈λ成立。对于这种数据组合，每个跟踪都是可执行的。例3.6令Δ R = Δ R {acq（r），rel（r）|r∈R}和M= P fin（R）是资源集模型。将关系式定义如下：当A，B满足R，S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177187λ►×[详细]⊆×AB={}，B<$A−−a−cq−（−r→）A<${r}如果r相对量A组B组B<$A−→A−{r}如果r∈AB<$A−→A如果λ∈Δ。这实际上是一种使能关系，并且规则强制执行互斥：每个资源名r最多只能被一个进程获取，在此之后，其他试图获取r的进程必须等待它的释放。其中命名资源的获取和释放交替的跟踪，受互斥约束，在同步构造的语义子句中是常见的，例如条件关键区域[7，8]。有了这个使能关系，跟踪α是可执行的，当且仅当对于每个r∈R，序列αacq（r），rel（r）是（acq（r）rel（r））ω的前缀，所以在跟踪执行的每个阶段，每个资源r最多被一个进程“拥有”。给定一个资源模型M和基于M和M的使能关系，我们将定义一个“资源敏感”的公平合并函数族RFMk：Mk→ P（（∞）k×∞）如下这个想法是，当（（α1，...，αk），β）∈RFMk（m1，.，mk）存在用于合并α1，...，αk并产生β，假设对于每个i，执行轨迹α i的进程最初拥有资源mi;在每个阶段，采取下一步骤的进程由其当前资源启用，而不是由其余进程的资源禁用;并且进程所拥有的资源保持兼容。当这些条件成立时，我们说β是迹 （α1，...，αk）从初始资源分配（m1，...， mk）。我们将RFM k表示为从Mk到（M ∞）k的子集的函数不好意思的设置RFM k（m1，...，mk）将为空，如果m1，...，m、k不兼容，或者在某个 点上没有办法保持资源兼容性。我们可以参考 设置RFM k（m1，...，mk）（m ∞）k m ∞作为具有初始资源（m1，...，mk）。定义3.7对于每个k≥ 1，RFMk：Mk→ P（（∞）k×∞）由下式给出：（（α1，...，αk），β）∈ RFMk（m1，...，（mk）有严格单调函数f1：pre（α1）→ pre（β），...，fk：pre（αk）→pre（β）和函数res：pre（β）→Mk，满足以下性质：(a) 对于所有i=j，rge（fi）∈rge（fj）={j}。188S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177λλλǁǁP(b) pre（β）=rge（f1）· · ·rge（fk）.(c) 对于所有i和所有αJ∈pre（αi），last（fi（αJ））=last（αJ）。(d) res（m）=（m1， . ，mk），且对所有βJ∈pre（β），若res（βJ）=（MJ1， . ，mJk），则mJ1···mJk被定义。(e) F或所有i和所有βJ和λ，i ffi（αJλ）=βJλ，res（βJ）=（mJ1， . ，m，J，k），以及res（βJλ）=（mJ1J， . ，mJkJ），则m<$mJi-→mJiJ，其中对于所有lji=i，mJjJ=mJj，且m= n {mj|1 ≤ j ≤ k &ji}。在（e）中，我们也可以使用缩写m;当k=1时，m的mula退化为0。 条件（d）确保所需的性质，RFM k（m1，...，当m1，...，K是不相容的。直观地说，当β是（α1，...，αk）从（m1，.，mk），β是（α1，.，（k）和以前一样，在每个阶段， 在那里的合并是对进程的资源的兼容分配，使得在给定其他进程的资源的情况下，进行下一步骤的进程具有足够的资源来启用该步骤。调度函数f1，...，fk，连同初始约束res（k）=（m1，...，mk）和使能关系，通过迹长的归纳，确定了对所有βJ∈ pre（β）的res（β j）.定理3.8对所有m∈M，RFM1（m）= {（（α），α）|a可执行文件从m}。证据 直接从定义出发。Q定理3.9对于平凡资源模型（示例3.5），RFM k（0，...，0）用FM k.证据在这种情况下，令res（βJ）=（0，...，0）对所有βJ∈pre（β）. 这是真的。在这里定义资源映射的唯一方法（d）和（e）是空的。RFMk的条件（a）、（b）和（c）与FMk中的条件完全相同。Q定理3.10对于资源集模型（例3.6），当A≠B ={}且如[ 8 ]中所定义的，γ∈ α ∞，（（α，β），γ）∈RFM2（A，B）i <$γ∈αA<$Bβ。4证据[8 ]中 的·AB·的 定 义 使用了 一种 灵活的“ 使 能” 形 式关系A−−B→AJ，其中h与B<$A−→AJ完全重合，如这里所模拟的。如果（（α，β），γ）∈RFM2（A，B）使用调度和资源分配证明γ ∈ αABβ. 如果γ ∈αABβ，则使用选择公理导出（（α，β），γ）的调度和资源分配。Q定理3.10示出了对于资源集模型fin（R），相关联的资源敏感公平合并操作RFM2为每个命名资源保持预期的互斥属性。例 如 ，α = acq（r）λ1λ2rel（r）和β = acq（r）λ rel（r）的唯一公平合并是αβ和βα。2.8的类似数字需要谨慎措辞，以考虑到资源。S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）1771894这里的条件γ∈∞限制于[8]中的跟踪模型的无异常中止子集，反映了RFM处理资源但尚未处理竞争检测的事实。这种不匹配将在下一节的定理4.6190S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177定理3.11函数RFMk具有以下对资源敏感的(i) 令（（α1，...，αk），β）∈RFMk（m1，.，mk），并且令res：pre（β）→Mk为相关联的资源映射。 若βJ∈ pre（β）且β = βJβJJ，则有are pefixesα1J∈p re（α1）， . ，αkJ∈pre（αk），和子集α1JJ，. ，αkJJ，这样α1=α1Jα1J J， . ，αk=αkJαkJ J，（（α1J， . ，αKJ），βJ）∈RFMk（m1， . ，m，k）和（（α1J J， . ，αkJ J），βJ J）∈RFMk（mJ1， . ，m，J，k），其中，e（m，j， . ，mJk）=res（βJ）.(ii) Sup pose（（α1J， . ，αKJ），βJ） ∈RFMk （m1， . ，mk ），其中剩余映射res：pre（βJ ）→Mk，且补βJ是有限的.Letre s （βJ）=（mJ1， . ，mJk）。如果（（α1， J， . ，αkJ J），βJ J）∈RFMk（mJ1， . ，mJk），则（（α1Jα1J， .. . ，αkαkJ J），βJβJ J）∈RFMk（m1，.，mk）。证据 修改定理2.8的证明以纳入资源核算。为(i) 这些假设和定义3.7中的属性允许我们使用res为前缀合并和后缀合并构造资源映射。为(ii) 这些假设确保可以组合来自前缀合并和后缀合并的资源映射，以获得用于（（α1Jα1J，. ） ，αkJαkJ J），βJβJ J）。Q我们 也有定理 2.11 的适 当类似物 ，适用 于处理资 源。我们 使用诸如m=（m1，...，mk），并且对于组合m1· · ·mk，定理3.12函数RFMn满足以下资源敏感的(i) 若（α1，β1）∈RFMk1（m1），.，（αn，βn）∈RFMkn（mn），且（（β1，.，βn），γ）∈RFMn（n=1，.，n），则（α1.. . αn，γ）∈RFMk1+···+kn（m1.. . mn）。(ii) 如果（α1.. . αn，γ）∈RFMk1+···+kn（m1.. . mn）和len（αi）=len（mi）=ki，1≤i ≤ n，则有迹β1，...，βn使得（α1，β1）∈RFM k1（m1），.，（αn，βn）∈RFMkn（mn）和（（β1，.，βn），γ）∈ RFM n（RFM1，.， m n）。证据修改定理2.11的证明以包括资源分配。在（i）和（ii）中的假设，以及M的性质和使能关系，对于确保子公司合并的资源会计能够正确地合并在一起是至关重要的。特别是，在（i）的组件的m1. mn是相容的，因为m1，. mn是假设相容的。Q4种族检测到目前为止，我们一直避免在语义上显式地处理竞态条件，例如一个进程试图写入并发使用的状态片段另一个过程。这种回避是共享内存程序的早期语义解释的典型特征，它假设赋值和表达式求值是S. Brookes/Electronic Notes in Theoretical Computer Science 265（2010）177191λi⊇►⊆×⊕联系我们原子地执行（如Park [21]），或者对共享变量的读写是原子的（如[7]）。然而，竞争条件可能导致不可预测的程序行为和对超出控制的硬件实现细节的依赖 或程序员的知识最近的模型结合了竞争检测，并将潜在的竞争视为灾难[8，9]。我们现在以类似的方式扩展我们的框架。这种扩展与上面给出的资源敏感的公平合并关系的公式中的微妙差距很好地吻合。RFMk的定义并没有规定当我们到达两个过程的阶段时该怎么做，其中两个过程具有资源mi和 mj，具有下一个动作λi和λj，使得每个进程用我们的使能关系来表述，当定义了mi<$mj，但没有m ji和mJjsuch，使得mj<$mi−−→mJi，mi<$mj−−λ→j mJ。当这种情况发生时，合并定义中的条件（e）将是eJ不可能填满。 即使这种情况不成立，操作，例如对同一个变量或堆单元的两次写入，我们希望 当作一场灾难。我们可以很容易地适应以前的框架来处理这样的问题，通过引入一个动作中止来表示运行时错误，和一个对动作的冲突（或干扰）关系，并扩展合并构造，使一个潜在的冲突产生一个以中止结束的跟踪。我们假设一些直观的公理，链接的consumption和使能关系。我们用一个特殊的动作来表示错误。设={abort}。我们将abort视为右侧连接的零：abortβ=abort。令∞=∞a b或t。定义4.1给定一组动作，一个资源模型（M，，0）和一个使能关系，ac在n上是子集dαΣˆ函数，写成一个整型运算符，这样：(i) 如果λ1dα λ2，则λ2dα λ1。(ii)
我的内容管理
展开
