共享可变数据的足迹跟踪语义模型

理论计算机科学电子笔记155（2006）277-307www.elsevier.com/locate/entcs共享可变数据斯蒂芬·布鲁克斯美国匹兹堡卡内基梅隆大学计算机科学系摘要我们提供了一个新的指称语义模型，基于“足迹”，共享可变状态的并行程序。 该模型的结构体现了Dijkstra提出的一个经典原则：过程应该被独立对待，干扰只发生在同步点。因此，该模型使程序之间的区别比传统的跟踪模型，这可能有助于减轻由inter-leaving触发的组合爆炸。对于顺序或无同步程序的足迹跟踪语义相当于一个非确定性的状态转换，所以新的模型支持“顺序”推理的无同步代码片段。我们表明，足迹跟踪语义是严格的抽象比动作跟踪语义，适合组成推理种族自由和部分正确性。新模型可用于建立并发分离逻辑的可靠性。我们包括一些示例程序，以便于与早期模型进行比较，我们简要讨论了与约翰·雷诺兹（John Reynolds）最近提出的一个模型的关系，在这个模型中，动作具有可辨别的开始和结束。关键词：并发，共享内存，粒度，部分正确性，竞争条件，指称语义，逻辑1大纲众所周知，并行程序的推理非常困难，因为并发线程之间可能存在冲突或竞争条件在传统的语义模型中，进程或线程表示一组跟踪，跟踪是一系列原子操作，并行组合被解释为公平交织。众所周知，这可能导致组合爆炸1电子邮件：brookes@cs.cmu.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.060278S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277当试图证明并行程序的正确性时，由于要考虑的可能交织的数量。如果并发线程写入同一个变量，而没有任何原子性或排他性的保证，结果可能是不可预测的或依赖于程序员无法控制的实现细节。传统的语义模型通常在硬件级别对某些原语的原子性进行粒度假设对整数值变量的读取和写入是原子的假设导致了具有更大原子步骤和更少交织的跟踪语义，但这种假设在实践中并不现实，因为整数值可能不适合单个机器字。另一方面，更现实的假设是字级读写是原子的，这将产生更多的交织，从而加剧组合问题，并且结果可能取决于字的大小。与其依赖于对硬件实现的可能毫无根据的期望，我们更希望能够安全地从粒度和字长中抽象出来，同时减少或避免交织问题。在某种程度上，这种方法对于简单的共享存储器程序（即没有指针的共享存储器程序）是可能的，这些程序是以严格规范的方式设计的。对于这样的程序，在Hoare [13]、Brinch Hansen [2，5]和其他人提出的基于资源的方法中，程序员必须在命名资源之间划分关键变量，并且仅允许在相关资源的关键区域由于资源被假设为信号量，这些设计规则确保互斥访问关键变量，并禁止程序与“活泼”的行为Owicki和Gries引入了一种霍尔风格的逻辑，它反映了这一学科，具有并行组合，区域和资源的规则。这提供了一种不依赖于粒度的关于部分正确性的安全推理的方法。不幸的是，这种方法不适合使用指针的并行程序，因为别名的可能性使得纯粹静态检测竞争条件是不可能的，并且Owicki-Gries证明系统在别名存在的情况下是不可靠的最近，作者开发了一个语义模型（使用动作跟踪），并使用它来证明这种并发分离逻辑的可靠性[7]。动作跟踪语义模型将并行组合解释为资源-S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277279公平交错的敏感形式，并将潜在的竞争条件视为灾难，如John Reynolds所建议的那样可靠性证明表明可证程序是无竞争的。上面的逻辑[16，14]和语义[7]是根据Dijkstra [11]提出的并发程序设计的经典原则设计的... 过程应该是松散连接的;除了（罕见的）明确的相互交流的时刻，.过程被认为是彼此完全独立的。动作轨迹模型支持体现这一原则的“本地启用”关系的定义然而，这个模型是不必要的细粒度的，并且包含对应于行为不太好的环境中的进程执行的跟踪，允许任意干扰。结果，该模型区分了满足完全相同的并发分离逻辑公式的某些命令对事实上，动作跟踪模型除了部分和全部正确性之外还支持安全性和活性属性的组成分析，因为它保留了关于在计算中发生的原子状态改变的序列的信息这种详细程度与部分正确性和完全正确性无关在本文中，我们开发了一个更抽象的语义，专门用于推理无种族的部分和全部正确性。我们使用的不是从资源操作和原子状态操作（如读取和写入单个变量）构建的操作跟踪，而是从资源操作和状态操作（压缩序列）构建的足迹跟踪，表示在没有干扰的情况下执行的状态更改序列的累积效应。我们限制了迹线的结构，以反映干涉只能发生在临界区域内的假设。因此，典型的跟踪将由状态动作和资源动作的交替序列组成，其中使新的语义模型真正体现了Dijkstra这种新的语义可以用来代替[7]建立并发分离逻辑的可靠性，基于更简洁的语义提供更精简的可靠性证明此外，一个命令的足迹跟踪集是独立于任何假设的原子动作的粒度。对于一个设计良好的并发程序，其同步点少而远，我们的模型需要较少的交织，有助于减轻组合爆炸。为了便于与动作跟踪语义[7]进行比较，并尽可能多地保留与该模型的共同点，我们对足迹跟踪语义的技术开发将呼应主要概念，280S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277从动作轨迹设置中定义，根据脚步的需要重新制定它们。（我们还重新检查了[ 7 ]中的一些程序示例，以突出新语义的优点。我们的足迹跟踪语义受到John Reynolds的思想的他最近开发了一个具有类似目标的模型[19]。Reynolds在Reynolds Reynolds然后在迹集上引入了一个抽象函数，它忽略了不必要的细节，比如独立的迹的相对顺序。在此基础上，我们的方法不需要重复使用，而是尽量避免相邻的足迹，避免基于顺序的区分，从而通过构造获得更抽象的对于没有空闲资源名称的命令，例如顺序程序，或者没有关键变量的并发程序，因此只有因此，我们的语义实现了Reynolds [19]提到的理想属性之一2语法我们的编程语言结合了共享内存并行与指针操作。定义2.1命令的语法（由c表示）由以下抽象语法给出，其中r表示资源名称，i表示标识符，e表示整数表达式，b表示布尔表达式，E表示列表表达式：c：：=跳过|i：= e|i：=[e]|[e]：= eJ|i：= cons（E）|处置|c1; c2|c1-c2|如果b那么c1否则c2|而b做c|局部i = einc|资源rinc|当b做c时，我们省略了表达式的语法，包括通常的算术运算和布尔连接词。我们假设表达式是“纯”的即表达式的值不依赖于堆。列表表达式E是一个列表e0，.，en的整数表达式。分配i：=cons（E）分配一系列新的堆单元;查找i：=[e]读取堆单元并将其内容分配给i;更新[e]：=eJ更改堆单元的内容;处置dispose（e）取消分配堆单元。S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277281我在c中，一个形式为locali=e的命令引入了一个名为i的局部变量，初始化为e的值，作用域为c。c中的资源块资源r引入了一个本地资源名r，作用域为c。当bdoc是资源r的条件临界区域时，r形式的命令。一个试图进入某个区域的进程必须等待，直到资源可用，获取资源并评估b：如果b为真，则进程执行c，然后释放资源;如果b为假，则进程释放资源并等待重试。一个资源一次只能由一个进程持有当b为真时，我们用rdoc的缩写。设free（c）是在c中自由出现的标识符的集合，表达式也有类似的符号。设reads（c）是在c中有一个自由读事件的标识符的集合，writes（c）是在c中有一个自由写事件的标识符的集合。这些集合可以像往常一样用结构归纳法来定义定义2.2令res（c）是在c中自由出现的资源名称的集合，由明显的结构归纳定义。特别是，res（c1<$c2）=res（c1）<$res（c2）res（withrwhenbdoc）=res（c）<${r}res（resourcerinc）= res（c）− {r}。如果res（c）={}，则命令c是无资源的。3个州一个状态是一个偏函数σ：Var~Vint，其中Var是Ide和Vint的不相交并。我们使用Vint表示位置（或堆单元）的集合，并且我们不区分位置和整数。这是一个集合的标识符。设St为状态集。我们使用σ作为在St上变化的元变量。如果dom（σ）是有限集合，则状态σ是有限的。请注意，dom（σ）是Var的子集，可能包括标识符和值。2我们使用传统的方法来处理数据，例如[v1：vJ， .] . ，vk：vJ]，其中1K每个vi∈Var和每个vJ∈Vint。特别地，[ ]表示空状态。我们写[σ |v：vJ]对于与σ一致的状态，除了在v处，它映射到vJ。对于X，令σ|X ={（v，vJ）∈σ|v∈X}和σ\X ={（v，vJ）∈σ|v/∈X}。我们记为σ ×σJ，当|dom（σJ）= σJ|dom（σ），即当联合σ<$σJ是有效状态时。当dom（σ）≠dom（σJ）={}时，设σ <$σ j。显然，如果σ<$σJ，则σ ×σJ也是如此。2同样合理的是将状态表示为对（s，h），其中s：Ide~Vint是“store”和h：V in t ~ V in t是“h e a p“。282S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）2774行动动作是我们语义模型的构建块。一个动作可以是一个我们包括我们使用术语足迹可能涉及变量的读写，以及堆单元的分配和处置定义4.1让λ在动作上的范围，如下面的ab-mathrammar所描述的，其中σ，σJ在状态上的范围，X在P（Var）上的范围，r在资源名称上的范围：λ：：=（σ，σJ）X|（σ，σ）X|（σ，中止）|try（r）|acq（r）|相对量处理资源的动作被解释为在早期的语义模型中：try（r）表示不成功的获取r的尝试，acq（r）表示成功的获取，rel（r）释放资源。（正常）足迹具有形式（σ，σJ）X，其中σ和σJ是有限状态，X是{v ∈ dom（σ）} dom（σJ）的子集。|σ（v）= σJ（v）}。X上的这个边条件可以等价地改写为σJ[X=σ[X]。集合X包含在该步骤中被认为是“只读”的变量（注意X是Var，所以X可以包括堆单元和标识符。这样的步骤表示“读取”σ和“写入”σ j\ X的命令的足迹状态部分σ[X]是只读的，并且在步骤中保持不变。形式为（σ，abort）的足迹，其中σ是（finite）状态，表示运行时错误，如竞争条件，或试图释放未使用的位置。这样的步骤将被视为灾难性的，因此不需要在这里记录只读集最后一个形式为（σ，）X的足迹，其中σ是一个状态，表示一个非终止计算，其中X中的变量是只读的，而dom（σ）中的变量是读/写或写的。我们包括一个只读为了能够准确地预测比赛条件而设置定义4.2对于足迹λ=（σ，σJ）X，令dom（λ）=dom（σ）dom（σJ），mod（λ）=dom（λ）−X;这是由λ修改的变量集。我们还定义了分配（λ）=dom（σJ）−dom（σ）和分配（λ）=dom（σ）−dom（σJ）。对于非终止足迹λ=（σ，λ）X，我们令mod（λ）=dom（σ）−X。S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277283同样，这表示分配给该步骤或由该步骤更新的堆单元的标识符集我们需要这个集合来保持对竞争条件的正确描述然而，当λ是中止步骤时，不需要定义mod（λ）。例4.3设v∈Var且vJ，vJJ∈Vint.• 足迹（[v：vJ]，[v：vJJ]）{v}只有在vJ=vJJ时才是良构的，在这种情况下，它表示对v的• 足迹（[v：vJ]，[v：vJJ]）{}总是格式良好的，并且表示v的• f（[vJ：vJJ]，[]）{}的前一步表示vJ的分布。• 形式为（[]，[vJ：vJJ]）{}的足迹表示vJ的分配。例4.4footstep（[x：0，y：1，z：2， 1：42]，[x：1，y：1，z：99， 99：0]）{y}表示一个状态变化，它更新x的值，分配由y表示的堆单元，并将z设置为初始化为包含0的新堆单元请注意，变量y本身不会更新，如只读set注释所示5个迹线我们通过连接有限个或无限个动作序列来构建跟踪。我们将使用α，β来在迹上进行范围，并让Tr是迹的集合在确定哪些操作序列是有意义的时，我们需要小心，记住我们对命令与其环境之间的交互的假设每个资源在任何时候都最多由一个进程持有，因此跟踪中每个资源名称的获取和释放操作将交替进行（如动作跟踪模型[7]）。假设存储管理是全局处理的：对存储分配器的每个调用都会产生一个没有被任何进程使用的堆单元最后，根据Dijkstra原则，我们将构建轨迹，其中相邻的足迹总是合并为一个步骤。这是一个从行动痕迹模型的根本出发，我们这样做的设计选择，使我们忽略中间状态无关的种族自由和部分正确性的推理。3可引发的行动我们刻画了一步一步执行的条件：如果λ1所需的状态与结果一致，则λ1可以跟随λ03这种相邻步骤的合并让人想起了[6]，但是我们专门使用最大的多个可扩展的方法来处理一个序列的所有可扩展的多个可扩展的序列，因为这会产生一个更简洁的284S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）2770并且λ1不分配由λ 0分配的任何位置。当这成立时，我们也说序列λ0λ1是可连接的。因此，我们将通过连接遵守此约束的动作序列来构建跟踪定义5.1设λ0=（σ0，σJ）X且λ1=（σ1，σJ）X是脚步声。我们说0011λ1跟随λ0，记为λ0=λ1，如果• σJ× σ1，即 σJ|dom（σ1）= σ1|dom（σJ）0 0 0• σ0×（σ1−σJ）• 分配（λ1）dom（σJ）={}，即 dom（σJ）<$（dom（σJ）− dom（σ1））={}。0 0 1前两个条件保证λ 0产生的状态与λ 1所需的状态一致。第三个要求反映了这样一种假设，即对存储分配器的调用产生真正新鲜的存储。显然，这不是一个对称关系：λ0= λ1并不意味着λ1= λ0。这是一个唯一的集合平面，它可以确定下面的关系。然而，它们确实有助于定义可连接操作的组合效果当λ1跟在λ0之后时，我们可以构造一个单独的足迹，记为λ0; λ1，它表示连续步骤的组合效果。定义5.2设λ0=（σ0，σJ）X 且λ1=（σ1，σJ）X脚步声如此0011λ0= λ1。 我们将λ0; λ1定义为以下足迹：• 如果disc（λ0）dom（σ1）={}，我们令（σ0，σJ）X;（σ1，σJ）X=（σ0<$（σ1−σJ），σJ<$（σJ−σ1））X00110 1 0其中X=（X0−mod（λ1））<$（X1−mod（λ0））。• 如果disc（λ0）dom（σ1）/={}，则λ0布置了λ1所需的一些单元，因此我们设（σ0，σJ）X;（σ1，σJ）X=（σ0<$（σ1− σJ），abort）.00110我们以显而易见的方式将可连接关系=和排序运算符λ0;λ1扩展到更一般的动作对对于中止步骤，我们定义如下：• （σ0，σJ）X=（σ1，abort）如果σJ× σ1和（σ1−σJ）× σ0000 0（σ0，σJ）X;（σ1，abort）=（σ0<$（σ1−σJ），abort）000• （σ0，abort）=λ对于所有操作λ（σ0，中止）;λ=（σ0，中止）涉及非终止步骤的相应定义类似：• 设λ0=（σ0，σJ）X，λ1=（σ1，σ j）X。00 1（σ0，σJ）X=（σ1，σ j）X，若σJ×σ1且（σ1−σJ）×σ000 1 0 0S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277285（σ0，σJ）X;（σ1，<$）X=（σ0<$（σ1−σJ），<$）X，00 1 0其中X=（X0−mod（λ1））<$（X1−mod（λ0））。• （σ0，σ）X0=λ，对于所有λ（σ0，λ）X0;λ=（σ0，λ）X0.我们允许任何操作λ被任何资源操作跟随（或跟随），因此对于所有资源名称r，λ=try（r），λ=acq（r），λ=rel（r），try（r）=λ，等等。Remark5.3Letδbethefotsstep（[]，[]）{}. 对于所有足迹λ0和λ1，我们有λ0=δ，δ = λ1，和λ0; δ = λ0，δ; λ1= λ1。下面的例子说明了上述定义，展示了连续步骤的只读信息是如何组合的，并激发了前面开发中精心选择的副条件。例5.4相同变量的连续读段是可连接的，只要它们产生相同的值;结果也是读段。更正式地说：（[x：v]，[x：v]）{x}=（[x：vJ]，[x：vJ]）{x}当且仅当v=vJ（[x：v]，[x：v]）{x};（[x：v]，[x：v]）{x}=（[x：v]，[x：v]）{x}例5.5对同一个变量进行读操作后再进行写操作是合理的，当读操作产生的值与写操作开始时的值相同时，结果是写操作。（[x：v]，[x：v]）{x}=（[x：vJ]，[x：vJJ]）{}当且仅当v=vJ（[x：v]，[x：v]）{x};（[x：v]，[x：vJ]）{}=（[x：v]，[x：vJ]）{}例5.6不同变量的读取可以连接起来;它们的结果可以互换，结果是一个只读的步骤。（[x：v]，[x：v]）{x}=（[y：vJ]，[y：vJ]）{y}当x y（[x：v]，[x：v]）{x};（[y：vJ]，[y：vJ]）{y}=（[x：v，y：vJ]，[x：v，y：vJ]）{x，y}例5.7对不同变量的写操作可以被连接起来;它们的结果可以互换;结果是一个单独的操作，代表了组合的写操作。（[x：v0]，[x：vJ]）{}=（[y：v1]，[y：vJ]）{}当nx/=y时0 1（[x：v0]，[x：vJ]）{};（[y：v1]，[y：vJ]）{}=（[x：v0， y：v1]，[x：vJ， y：vJ]）{}0 1 0 1（[y：v1]，[y：vJ]）{};（[x：v0]，[x：vJ]）{}=（[x：v0， y：v1]，[x：vJ， y：vJ]）{}1 0 0 1例5.8一个堆单元的处理总是可以跟随着另一个单元的处理。尝试连续两次处置同一单元格会导致错误。（[v0：vJ]，[]）{}=（[v1：vJ]，[]）{}如果v0/=v1或（v0=v1&vJ=vJ）。0 1 0 1（[v0：vJ]，[]）{};（[v1，vJ]）{}=（[v0：vJ，v1：vJ]，[]）{}如果v0/=v10 1 0 1（[v：vJ]，[]）{};（[v：vJ]，[]）{}=（[v：vJ]，abort）286S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277注意，在错误的例子中，有一个ve（[v：vJ]，[]）{}=（[v：vJ]，[]）{}，因此动作是可连接的，但它们的连接表示运行时错误。例5.9假设存储分配是全局管理的，因此连续调用分配器总是返回不同的堆单元;因此我们不需要允许连续分配同一个堆单元。的确，根据上面的定义，我们有（[]，[v：vJ]）{}/=（[]，[v：vJJ]）{}。例5.10一个分配堆单元v的步骤可以跟在任何一个v没有被读、写或分配的步骤之后，这也是因为存储管理器总是分配“新”单元。我们有（σ，σJ）X=（[]，[v：vJ]）{}如果v/∈dom（σJ），在这种情况下，（σ，σJ）X;（[]，[v：vJ]）{}=（σ，σJ<$[v：vJ]）X\v。可挂序列如果λ0=λ1且λ1=λ2，则不一定得出（λ0;λ1）=λ2。例如，考虑以下足迹：λ0=（[v：0]，[]）{}λ1=（[y：0]，[y：0]）{}λ2=（[v：1]，[]）{}。我们有λ0=λ1和λ1=λ2，但λ0;λ1=（[v：0， y：0]，[y：0]）{}，所以有（λ0;λ1）/=λ2。实际上，在没有干扰的帮助下，显然不能执行脚步的序列λ0λ1λ2，这是因为第一步和第三步之间的v值因此，我们不应认为这一系列行动是可以联系起来的。相反，在足迹序列λ0λ1λ2可以无干扰地执行的所有情况下，我们将有λ0=λ1 和 （ λ0;λ1 ） =λ2 ， λ1=λ2 和 λ0= （ λ1;λ2 ） ， 以 及 （ λ0;λ1 ） ;λ2=λ0;（λ1;λ2）。我们希望简化我们的语义，以便我们只包括反映我们关于干扰的基本假设的痕迹，只允许外部干扰。通过同步干扰。因此，我们将可连接性关系扩展到有限迹和动作，如下所示，当动作λ可以跟随迹β时，使用符号β=λ。我们类似地扩展了连接运算，使得对于有限迹β和作用量λ，使得β=λ，我们得到迹β;λ的定义。该定义使用案例分析，跟踪的最终操作对于足迹序列，定义反映了上述关于可连接性的评论。S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277287nn定义5.11对于所有有限轨迹α，资源名称r和足迹λ，λJαλ=λJiλ=λJα try（ r ） =λJiα=λJα acq（r）=λJ始终α rel（r）=λJi <$α=λJ注意，在资源获取之后的步骤在此不受约束，允许在同步时干扰的可能性。定义5.12对于所有有限轨迹α，资源名称r和足迹λ，λJ（ αλ ） ;λJ=α（ λ;λJ ） 当 λ=λJ （ α try（ r）） ;λ=α try（ r）λJ当α=λJ（αacq（r））;λJ=α acq（r）λJ总是（α rel（r））;当α=λJ时，λJ=α rel（r）λJ我们现在可以给出可连接有限动作序列的形式特征，并且对于每个这样的序列α，我们可以指定通过连接其步骤而获得的迹cat（α定义5.13单个足迹λ是可连接的，cat（λ）=λ。形式为βλ的序列是可连接的当且仅当β是可连接的且cat（β）=λ，在这种情况下我们令cat（βλ）=cat（β）;λ。当α是序列λ0... λn且是可连接的，我们可以使用符号λ0;. ; λn表示cat（α）。可连接性的概念以明显的方式扩展到无限序列的动作：无限序列是可连接的，当且仅当每一个预设值都是可连接的。然而，连接四个步骤的无限序列λn=（σn，σJ）Xn的结果需要完全定义。有两种情况：• 如果对于ea chnwehaveλ0;. . ;λn=（τn， τJ）Yn第n个无限序列表示将由状态启用的非终止计算∞n=0例τn. 整个计算的只读变量可以取∞为Y ={v ∈n=0Xn|你好（v∈Xn<$v∈dom（λn））}。因此，我们定义λ0;. ; λn;. =（∞n=0例τn，τ n）Y.• 如果对于某个n，我们有λ0;... ; λn=（τn，abort）则对于所有较大的n也是如此，我们定义λ0;. ; λn;. 也是（τn，abort）。出现在由无限步序列连接而成的足迹中的状态很可能是无限的，即使所有的单个步λn288S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277T=1涉及国家的有限部分这有一个自然的计算解释：进程在执行期间需要访问堆的无限部分当然，这只能发生在无限计算中，因为计算轨迹的每个有限前缀只影响状态的有限部分。下面的示例演示了此行为。例5.14考虑步骤序列λn=（[x：n，n：0]，[x：n+ 1]）{}，其中n≥0;使用上述定义，我们有λ0; λ1;. ;λn;. =（[x：0，0：0，1：0，.，n：0，.. . ]，）{}.此足迹表示命令的可能行为while true do（dispose（x）; x：= x +1）.很容易将可连接性的概念和连接运算符扩展到迹对当α和β是迹时，我们写α=β表示β跟随α，我们写α;β表示连接它们得到的迹[4]然后，我们以通常的方式定义了迹集的连接和迭代，并进行了调整，以便只包括可连接的情况。对于迹集T0，T1和T，我们定义：• T0; T1={α0; α1|α0∈ T0&α1∈ T1&α0= α1}。•∗∞n=0例Tn，其中T0={δ}且Tn+1= Tn; T（n≥ 0）.• Tω={α0; α1;.αn;. | ∀n ≥ 0. αn∈T&α0;. αn= αn+1}。并联组成与其他线程并行运行的进程的行为取决于该进程所拥有的资源，并受到其环境所这些资源集开始为空，并且将始终保持不相交，因为我们假设通过信号量实现资源。 因此，我们为每个动作定义了一个资源，关系（A1，A2）−→λ（AJ，A2）在解集的离散子集上，当在保持A2的环境中保持资源A1的进程可以执行这个动作，以及动作对资源的影响。虽然A1和A2为空的特殊情况值得特别注意，因为它对应于典型的初始假设，但一般情况具有更简单的归纳公式。定义5.15设A1和A2是不相交的资源名称集合的4 注意，如果α是可连接的，那么cat（α）也是可连接的，并且cat（cat（α））=cat（α）。 如果α=β且α和β是可连接的，αβ也是，cat（αβ）=cat（α）;cat（β）。S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277289资源使能关系−→λ由下式给出：（A， A）−t−ry−（−r→）（A， A） always1 2 1 2acq（r）（A1，A2）−→（A1<${r}，A2）i <$r∈A1<$A2相对量（A1，A2）−→（A1−{r}，A2）i<$r∈A1（A1，A2）−→λ（A1，A2）总是，如果λ不是资源操作这以明显的方式概括为一系列动作，我们写道：（A1，A2）−→α· 表示在环境中持有资源A1的进程保持A2可执行跟踪α。定义5.16设λ0=（σ0，σJ）X λ1=（σ1，σJ）X。 我们说λ00011和λ1干扰，记作λ0daλ1，如果• σ0× σ1，即 σ0|dom（σ1）= σ1|dom（σ0）• dom（σ0）dom（σ1）/X0X1当λ0daλ1定义λ0·λ1=（σ0<$σ1，abort）时。如果重叠的变量对于两个足迹都是只读的，则不存在争用，因此我们不将其视为干扰情况。对于异常足迹，我们将干扰情况描述如下：定义5.17当λ0是（σ0，abort）和/或λ1是（σ1，abort）时，我们指定如果σ0×σ1，则λ0daλ1成立。如果λ0是（σ0，<$）X λ1是（σ1，σJ）X011如果σ0× σ1和dom（σ0）<$dom（σ1）/<$X0<$X1，则λ 0 da λ 1成立。对于（σ0，σ）X0 和（σ1，σ2）X1，和（σ0，σ 2）X0 和（σ1，a b或t）是类似的。我们现在定义，对于每对（A0，A1）不相交的资源集和每对（α0，α1）的序列，α 0的所有多个公平值的选择α0A0<$A1α1使用A0，α1使用A1。 这是α0与α1的所有公平交织的集合，其中每个步骤都遵守资源约束，并且竞争条件会导致错误。 有限迹的定义是归纳的，迹的长度的乘积，并且我们包括空序列，以允许更简单的公式化：基本情况是当迹之一为空时注意，对于初始化，其中nα0是序列，但α1是不允许的，因为它需要属于A0的资源。同样，尽管两个资源集都为空的情况在后续中起着特殊的作用，但更一般的情况具有自然的归纳公式。定义5.18对于有限迹α和β，以及不相交的资源集A0，A1，290S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277010101int迹线αA0<$A1β的集合由以下公式归纳给出：αA<$A<$={α| （A0 ， A1 ）−→α·}<$A<$Aβ={β| （ A1 ，A0 ） −→β·} （ λ0α0 ） A0<$A1（λ1α1）={λ0·λ1}，如果λ0daλ1λ0J={λ0;β|（A0，A1）−−→（A0，A1）&β∈α0AJ<$A1（λ1α1）&λ0=β}λ1J{λ1;β|（A1，A0）−−→（A1，A0）&β∈（λ0α0）A0<$AJα1&λ1=β}如果<$（λ0da λ1）我们再次注意到，并行组合的定义建立在资源约束的基础上，只包括可连接的情况，并结合相邻的足迹。互斥公平合并集合的定义以通常的方式扩展到无限迹[17，7，6]。迹对的fairmerge定义以明显的逐点方式扩展到迹的集合：当T0和T1是迹的集 合 时 ， T0A0<$A1T1是集合α0A0<$A1α1作为α0rangsoverT0和α1rangsoverT1 的并集。我们将主要关注A0=A1={}的情况，表示当两个进程在没有初始资源的情况下启动时会发生什么实际上，我们可以将T0{}<${}T1表示为T0<$T1，省略空下标。6表达式的语义设Tag=P（Var）为用于注释足迹的只读集的集合。记住，Var是Ide和Vint的联合。对于整数表达式e，我们将定义一个足迹迹集[e]]（St×Vint）Tag。类似地，对于布尔表达式，我们将定义一个足迹迹集[b]]（St×Vbool）Tag。整数表达式的足迹跟踪集[e]将包含以下形式的项（σ，v）X其中σ是状态的有限片段，其中e的值为整数值v，X是在求值期间读取其值的变量的集合我们也可以按照类似的方式给出列表表达式E的语义，使得列表表达式的值是整数值的列表：[E]]（St×V）Tag。我们省略了细节，这是直截了当的。5我们的表达式的语义子句可以通过插入和传播有关只读变量的相关信息从Reynolds语义[19]中的相应子句中5我也可以将一个函数包含到这个类似于“impure“expressions s u c h as [ e ]的模型中 ， 它 的 值 取 决 于 堆 。S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277291定义6.1语义功能[[−]]：Expint→ P（（St×Vint）Tag）[[−]]：Expbool→ P（（St×Vbool）Tag）由以下条款归纳定义[[n]]={（[]，n）{}}[[i]]={（[i：v]，v）{i}|v ∈ Vint}[[e1 + e2]] ={（σ1 <$σ2，v1 + v2）X1<$X2|（σ1，v1）X1∈[[e1]]（σ2，v2）X2∈[[e2]]σ1× σ2}[[true]]={（[]，true）{}}[[e1=e2]]={（σ1 <$σ2，v1= v2）X1<$X2|（σ1，v1）X1∈[[e1]]（σ2，v2）X2∈[[e2]]σ1× σ2}[[b1和b2]]={（σ1，false）X1|（σ1，false）X1∈[[b1]]}<${（σ1 <$σ2，t）X1<$X2|（σ1，true）X1 ∈ [[b1]]&（σ2，t）X2 ∈ [[b2]] &σ1 ×σ2}[[ifbthene1elsee2]]={（σ0 <$σ1，v1）X0<$X1|（σ0，true）X0 ∈ [[b]]&（σ1，v1）X1 ∈ [[e1]] &σ0 × σ1}{（σ0 <$σ2，v2）X0<$X2|（σ0，false）X0∈ [[b]]&（σ2，v2）X2∈ [[e2]] &σ0× σ2}在这里，我们指定了合取b1和b2是使用通常的短路来求值的;这个细节在下面的内容中并不重要，如果我们使用另一种解释，如严格的从左到右求值，那么随后的发展可以根据需要进行修改没有必要使用更精细的语义结构，允许在表达式评估期间干扰的可能性，因为该模型仅旨在描述遵守Dijkstra原则的环境中的执行：假设干扰仅发生在同步时。因此，忽略中间状态是安全在上面的定义中，我们还假设表达式求值总是终止，因此我们确实不需要包括形式（σ，σ）X的足迹来表示非终止例以这种方式扩展语义定义很简单包括非终止表达式。例6.2要计算x + y，我们需要一个x值和一个y值：[[x + y]]={（[x：v，y：vJ]，v + vJ）{x，y}|v，vJ∈ Vint}类似地，要计算x+x，我们只需要x的一个值：[[x + x]]={（[x：v]，2 v）{x}|v ∈ Vint}。注意，[x+y]]=[[y+x]，所以这个表达式的语义从求值顺序中抽象292S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277一个布尔表达式产生了一对单足迹轨迹集，以明显的方式：我们区分描述“真”情况的轨迹定义6.3对于一个布尔表达式b，令[b]]true，[[b]]false，则Tr由下式给出[[b]]tr ue={（σ，σ）X|（σ，true）X∈[[b]]}[[b]]f alse={（σ，σ）X|（σ，fals e）X∈[[b]]}实施例6.4[[true]]true={（[]，[]）{}}={δ}[[true]]false={}例6.5设b为表达式（x=y）和（y=z）。[[b]]f alse={[x：v，y：vJ]，[x：v，y：vJ]）{x，y}|vvJ}{（[x：v，y：v，z：vJJ]，[x：v，y：v，z：vJJ]）{x，y，z}|v/=vJJ}[[b]] true={（[x：v，y：v，z：v]，[x：v，y：v，z：v]）{x，y，z}|v ∈ Vint}7命令的语义对于每个命令c，我们通过结构归纳法定义足迹迹集[c]]ΔTr定义确保对于每个c，得到[c]中的每个迹从一个可连接的动作序列，因此跟踪集指定了程序定义7.1语义函数[−]]：Com→ P（Tr）被定义为诱导，S. Brookes/Electronic Notes in Theoretical Computer Science 155（2006）277293具体由以下条款规定：[[skip]]={（[]，[]）{}}[[i：= e]]={（σ[i：v]，[σ|i：vJ]）X\i|（σ，vJ）X∈[[e]]&σ×[i：v]}[e]：=eJ]]={（σ <$σJ<$[v：v0]，[ σ <$σJ|v：vJ]）（X<$X'）\v|（σ，v）X∈[[e]]（σJ，vJ）X'∈[[eJ]]σ×σJ（σ<$σJ）×[v;v0]}[[i：=[e]={（σ[i：v0，v：vJ]，[σ|i：vJ，v：vJ]）（X<${v}）\i|（σ，v）X∈[[e]]σ×[i：v0， v：vJ]}[[i：= cons（E）]] ={（σ[i：v]，σ[i：l，l：v0，...，l+ n：vn]）X\i|（σ，[v0，.，vn]）X ∈ [[E]]&σ × [i：v]&l，l+1，.，l+n/∈ dom（σ）}[[dis posee]]={（σ[v：vJ]，σ\v）X\v|（σ，v）X∈[[e]]&σ×[v：vJ]}[[c1; c2]]={α1; α2 |α1 ∈ [[c1]] &α2∈ [[c2]] &α1 = α2}=[[c1]];[[c2]][[ifbthenc1elsec2]]=[[b]]true;[[c1]][[b]]false;[[c2]][[whilebdoc]]=（[[b]]S真;[[c]]）;[[b]] 假[[b]真;[[c]]）ω[[c1<$c2]]={α1{}{}α2|α1∈[[c1]]&α2∈[[c2]]}[[withrwhenbdoc]] =等待;输入 等待ω其中