π-演算中的资源分析及分离逻辑的语义理论研究-简介与优势

∣可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）313-334www.elsevier.com/locate/entcsπ-演算的资源分析亚伦·图伦·米切尔·万德东北大学关闭MA，USA摘要我们给出了一个新的处理π演算的分离逻辑的语义理论的基础上，继续Hoare和O'Hearn开始的研究计划。使用一种新的资源模型，区分公共和私人所有权，我们重构的操作语义，使发送，接收和分配的命令，在accumuence拥有的资源。 这些想法自然会导致两个指称模型：一个是安全性模型，一个是活性模型。这两个模型都是完全抽象的相应的可观测量，但更重要的是，两者都非常简单。与分离逻辑的模型论的密切联系（在特别是Brookes关键词：分离逻辑，π演算，所有权，资源，范围挤压，完全抽象名称在π演算中扮演着主导角色：它们既是通信的手段，也是通信的数据。本文提出了一种新的名称管理机制，这反过来又植根于分离逻辑的基础上的π演算的这项研究的主要好处是一个非常简单，但完全抽象的指称语义的π演算。传统上，π演算中名称的使用是由词法但动态可扩展的作用域控制的。例如，在复合进程Pnewx.Q中，通道x由于作用域最初是Q私有的。prefixnewx不是命令式分配。它是一个绑定器，随着Q的发展而保持固定-不断提醒x是私有的-直到Q在消息中发送x在这一点上，活页夹被提升以覆盖P和Q，动态地π-微积分依赖于α重命名和关于新鲜度的附加条件，以确保其隐私叙述得到证实。相比之下，分离逻辑的工作导致了基于资源和所有权的动态结构并发模型，而不是名称和范围[3，5]。从这个角度来看，程序由命令组成，这些命令使用某些资源（它们的并发进程必须在它们之间分配资源，每个进程只使用它拥有的资源.所有权使得约束并发1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.028314A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313干扰，从而对过程行为进行成分上的推理。在本文中，我们从资源和所有权的角度重新分析了π演算，建立了与分离逻辑模型的清晰联系分析取决于资源的使用，不仅指定一个流程可以做某事，而且指定其他流程不能做某事。1具体地说，渠道是可以公有或私有的资源公共所有权只声明一个通道可以被拥有它的进程使用。此外，私有制还声称，一个通道不能被其他进程使用。prefixnewx变成了命令式动作，分配一个初始私有通道。有了这个简单的资源模型，我们为π演算（§1）给出了一个新的操作语义。语义分为两层。第一层生成基本的标记转换，而不考虑它们的全局可扩展性。然后，第二层将这些标签统一解释为资源转换器，过滤掉不可信的步骤。两层设置让人想起Brookes更重要的是，资源模型还支持对π演算的非常简单的指称处理。我们给出两种指称的解释，都是迹论的。第一个（§ 2）仅捕获安全属性，而第二个（§ 3）也对发散和一些分支行为敏感，沿着具有无限迹的故障/发散模型[18]。我们证明，每个模型是完全抽象的适当的可观的。语义基础使分离逻辑的模型理论与π演算协调一致;那么证明理论呢？我们勾画了分离逻辑与过程精化演算的集成（§ 4）。细化是由指称语义来判断的，因此演算对于上下文近似是合理的。资源推理使我们能够推导出一个无干扰的扩展法，使用隐私断言来排除信道上的干扰为了提供一个精确的π演算模型，公共/私有资源在某种意义上必须是保守的：一旦一个资源被公开，就不可能再将其私有化分离逻辑的工作已经表明了更“积极”的资源模型的有用性我们概述了几个这样的聚合资源模型（第5.1节），包括对部分权限[1]和会话类型[10]的解释Hoare和这项研究为我们的工作提供了动力，我们的工作通过（1）处理完整的演算，（2）处理活性，（3）证明完全抽象和（4）构建语义逻辑而进一步发展。也有几个完全抽象的π演算模型[20，8，7]基于函子范畴的建模范围。我们的模型补充这些提供了一个基本的行为帐户，围绕资源和抽象的分离逻辑结构。一[1]这种对资源的解读已经出现在例如：拒 绝 担保推理[6]。A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313315公司简介π∶∶=ee ′e（x）e ∶∶=xc，和，则是不确定的。∶∶=（）过程的一部分操作“”表示错误，由使用无主+ +----CUP-τ→P相关工作的完整讨论见§5.2。1资源驱动的操作语义π演算有许多变体P ∶∶= ∑πi.Pi<$P<$Q 公司简介 中国人民银行 阿雷克X.P†X我们区分了外部选择（）和内部选择（），这简化了活性语义（§3），但不是必需的。我们还区分通道（c，d）和通道变量（x，y，z），并包括一个简单的语法通道表达式（e）范围内的两者。关闭的进程没有未绑定的通道或进程变量。然而，封闭进程可以引用通道常数，从而与它们的环境通信。我们写0表示一个空的求和，这是一个惰性过程。1.1生成动作封闭进程的操作语义通过两个标记的变迁系统分两层给出在这两个系统中，标签都是（句法）动作，由以下语法给出：α c！d c？d νc τ A动作分别记录发送、接收和分配所涉及的具体通道。 动作τ，像往常一样，代表一个内部的（不可观察的）步骤，通道（§1.2）。通信操作是双重的：C！d=c？d和c？d=c！d，而νc，第一个转换系统生成与过程相关的所有可能的动作，而不考虑这些动作是否全局合理：操作语义：动作生成P-α→Qcd.pc！Dp +c（x）.P+ p-c？→dP12PP{d/x}我PαP′P<$Q-α→P′<$QQαQ′P<$Q-α→P<$Q′新x.P-ν→cP{c/x}P-α→P′Q-α→Q′记录X.P -τ→P{recX. P/X}P<$Q-τ→P′<$Q′根据这种语义，我们将有如下转换：新x。新y.xy. 0-ν→c纽约0-ν→cCC.0-c！→c0316A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313（）下⊺ı→⊺ı联系我们Q<$∶→因此，如果c∈dom（σ），则作用νc是不可能的。 同样，如果σ（c）=pri，（）（）操作的语义如下：⊺ı{⊺ı}ı≤≤⊺∈Qα<$σ=σ′，则特别是Qα<$σ=σ′，不允许的一个部分噪音失败，生成-行动c！C不可能。其中C被分配两次，并且用于与不知道它的环境通信。为过滤此类执行，我们使用资源。1.2资源和动作语义上面的执行在直觉上是不可能的，因为在第一个v c动作之后，进程已经拥有了通道c。类似地，对于新的x.xx. 0跟踪新x.xx. 0 -ν→cCC.0-c！→c0是不可能的，因为刚刚被分配的信道C对于环境是未知的，所以在通信的另一侧不可能有并行进程沿着C进行接收。形式上，资源是域的元素σ。 C韩pub，pri，其中pub和pri是不同的原子。如果一个进程使用资源σ执行，它拥有通道domσ，σ c告诉每个c，这个所有权是否是独占的。在特定时间点拥有的资源不仅决定了什么是可能的，而且也决定了什么是允许的。例如，进程CD。0立即尝试沿着信道C进行通信。如果该信道未被分配（即，，而不是拥有，即。，不在dom中σ），则该过程是错误的：它试图使用一个摇晃的指针我们将行动α解释为资源转换器类型的转换器。2.由于所有的不确定性都在动作的生成过程中得到了解决，因此这些转换器是确定性的。结果或表示一个动作是不允许的或不可能的。给定动作的语义α-α（定义如下），我们可以定义一个根据当前拥有的资源执行P-α→P′Qα<$σ=σ′P-α→P′Qα<$σ= σ ′αP，σDP′，σ′P，σd 0，σ成功的操作将正常进行，更新拥有的资源-注意，如果将出错的标签重新命名。 不可能的行动悄然失败。2符号表示集合Σ，，并且对于所有σ，蕴含一个排序σ。顺序结构遵循抽象分离逻辑[5]，并且与局部性有关（§ 2）。A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313317⎪⎪⊺{}⊆/ ()⎪⊺∉()⎪（）否则的话c. 事实上，c已经被分配了一个跟踪（防止它Q<$[]=采取不可能的步骤），但没有引入新的痕迹。同样地，动作语义学Qα<$∶Q→ Qα<$∶ QdomσQc！d<$σσ[dpub]σ（c） =pubC 多姆σQc？d<$σσ[dpub]σ（c） =pub，否则的 话⎪⎪⎩ıσ dpri否则Qνc<$σσ[cpri]cdom（σ）Q<$<$σQ<$<$σ总是允许分配，但如果通道已经分配，则不可能分配的信道最初是私有的。发送一个信道会公开它，但是只有在已经公开的信道上执行通信才是可能的，并且只允许在分配的信道上进行通信从环境接收的本地未知信道对于环境是已知的，并且因此是公共的;从环境接收的本地已知信道不可能是私有的。示例考虑新的X过程。0. 我们有新x。对于每个通道C，0。它遵循新x。0，000c-ν→c00，[cpri]对于每个通道c，同时使用更多资源执行新x。0，[cpri]v d0，[cpri][dpri]导致约束的所有操作：这里的D表示不相交的联合，意味着新x.xx. 0-ν→cCC.0-c！→c0但是，考虑到资源，新x.xx. 0，0.000000cc. 0，[cpri]在这一点上，程序是固定的：这是一个错误！C被防止发生，因为C！c cpri.这种死锁正是我们在进程试图通过私有通道进行通信时所我们终于有新x。（xx. 0x（y）.yx。0个）-ν→cCC .0c（y）.yc. 0318A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313-τ→0μcc。0-c！→d0∣0A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313319dom（σ），并具有：好吧⊢✓有了资源，新x。（xx. 0x（y）. yx。0），Bvccc. 0c（y）. yc. 0，[c pri]τ0cc. 0，[cpri]在这里，我们可以看到，可以沿主技术通道进行内部通信并且允许：这样的内部步骤对于资源敏感的步进关系表现为τ动作，并且因此总是通过。另一方面，内部通信也使c的所有权保持不变。因为它仍然是私有的，所以最终的通信CC被卡住了，这是应该的。1.3工艺安全对于简单的公共/私有资源模型，只有在使用未分配的通道时才会发生故障。我们的语义框架可以适应释放，但这样做会使完整的抽象结果复杂化，我们希望专注于标准的π演算。避免释放允许我们轻松地描述“安全”进程：我们说σPi P是闭合的，并且P中的所有通道常数都在引理1.1如果σ∈P，则P，σ→P′，如果进一步P，σ-α→P′，σ′，则σ′ →P ′，2指称语义：安全跟踪资源为π演算的操作语义提供了一个有趣的重构，但它们真正的价值在于它们支持的基本指称模型。我们从一个简单的跟踪模型开始，它只捕获（一些）安全属性，这使我们能够专注于资源的角色。然后，我们结合了活性（§3）及其与资源的相互作用对于安全模型，我们有轨迹t，轨迹集T和行为B：TRACEABEH≜Σ →TRACE SETT RACE S ET{T：TT竞赛，T预封闭}过程将表示行为：由最初可用的资源确定的动作轨迹集.不是所有的行为都是可观察的。我们遵循π演算的标准处理[19，8]，考虑τ步不可观测，并省略νc步，直到分配的信道c通过公共信道发送（我们的指称语义表明，π演算的算子对于这些观测量是动作α的可观测量是一个（可能是空的）迹，取决于可用的资源：320A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313∣ ∣ ≜∣☇∣≜ ☇⋅≜⎪⎨⋅() =D<$α<$t∈OPσσ▷∥产生最小的行为：λσ。{\fnSimHei\bord1\shad1\pos（200，288）}⊔⊔如果B（σ） <$B′（σ）对所有σ和（ ）（）=（）（）（1）新的x.PvcPc<$PQ）ρ （Ⅱ）ρ（Ⅲ）ρPβQXρρ（X）⊔▷安全观察O <$P）∶BEH作用观测量<$α <$σ∶T族指称语义（安全）<$P）∶E→BEHτσϵvcσ什么？dσc？D快！dσ去死吧！d σ dpri快！d否则我们写t u或tu来表示跟踪连接，而写tu或tu来表示空跟踪。 虽然νc不能立即观察到，但采取νc步骤会占用进程所拥有的资源，因此稍后暴露c将导致νc步骤可见地重新出现。一个进程的安全行为可以在操作上被读取和确定：（O∈P）σP，σαP′，σ′t∈OP′σ′（Ⅲ）指称语义的目标是在流程结构上计算相同的合成轨迹。T族SET是子集序下的完备格，行为继承有B B σ B σ Bσ 语义运算符是单调的（实际上是连续的），因此我们将rec定义为定点是合理的。对于基于有限观察的安全语义，它是最小定点。安全跟踪模型对进程的分支行为不敏感[21]，因此内部和外部选择无法区分。我们解释这两种形式的选择使用，合并所有的替代品的行为。对于空求和，表示函数由环境ρ参数化，这里将通道变量x取为通道c，将过程变量X取为行为B。它使用了两个额外的运算符和，我们将很快定义。是的！ρe′Pρ（x）.P）ρ ≜什么？cP）ρ[xc]（X.P）ρπμB。<$P）ρ[X<$B]<$∑πi.Pi）ρi<$πi.Pi）ρ<$P<$Q）<$P）<$P）<$P<$Q）<$（Ⅲ）前缀进程的解释类似于操作语义：指称语义的每个子句生成所有局部合理的动作，而不立即检查全局可扩展性。我们使用连接每个动作产生的行为-再一次反映不确定性-并且我们在必要时更新操作符α B以一种资源敏感的方式将一个动作α前置到一个行为B，扮演着类似于操作语义的第二层的角色A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313321Q <$Q <$={}{∶ ∈{}}∣（（））语义学，事实上，Qc！c<$[cpri] = 预先控制c！c从b开始记录步骤。▷（）={}{{\fnMicrosoftYaHei}也就是说，彼此。也就是说，x对于xc是私有的，而xc不能形式（σ）到组合的边界，产生两组迹。对于e eech对f（vcc！cλ σ。{}）（）={}{νct∶t∈（c！cλ σ。{}）[cpri]}语义前缀αB∶BEH（α<$B）（σ）<${αt∶α σ=σ′，t∈B（σ′）}<${<$∶α σ=<$}<${<$}为了保持prefix-closure，我们将fix-closure作为一个可能的跟踪。 举个简单的例子：新x.xx. 0）= v cxx. 0）xc = v c c！c0）xc = v c c！cλ σ。关于我们CCC这种定义的扩展类似于我们从操作语义的第一层看到的痕迹，没有考虑资源。外延，召回，是一种行为：为了提取它的轨迹集，我们必须将其应用于某些特定的资源σ。如果我们使用空资源，我们会看到cCv c t tC换句话说， 新x.xx. 0∅ϵcv c. 正如在操作在这里，前缀闭包（特别是，在的每个应用中包含了闭包）确保我们看到了跟踪，直到我们尝试了一个不可能的动作。最后，我们有并行组合-最有趣的语义操作符。在这里，我们必须问一个指称语义的关键问题：如果σ是资源属于P Q，我们提供什么资源给P和Q？这个问题不会出现在操作语义中，操作语义维护一个单一的全局资源状态，但是组合语义必须回答这个问题。考虑新的X过程。xc x z.当进程达到并行组合时，x仍然是私有的。x的私密性意味着子进程只能相互通信（产生τ），而不能与进程的外部环境通信。但是子进程与外部环境进行通信沿着它进行外部通信，但是它对于子进程xc和x（z）是公共的，这可以。语义平行合成B1（B∈（）（t其中，<$σ（c）<$pubc∈dom（σ）1 2tiBiσ1 2否则，给予行为的并行组合的资源σ以公共提升的方式馈送。迹t1和t2从这些集合，我们计算所有的交织t1和t2：形式上，我们将这一叙述描述如下：322A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313▷▷<$α<$（t′<$′u）如果t=αt={}如果t=αt，u=αu，则“tudc（σ） ={，d！c}相同的通信（产生λ<$σ. {1}）和两个可能的命令，如果它们是（）（）（2）（ ）（） ={} {∶ ∈}（=（（ ）（）=（）（）={}∅∥资源σ=[cpub][dpri]。很容易计算出，∣Q =={}∣预期 也就是说，新的X。xcx y）cpub.更一般地说，我们可以证明=迹线交织tu λ σ。{n}ift=n=u<$α<$（t<$u′）如果u=αu′乍看之下，交错似乎是标准的，但请注意语义前缀：交织并不是简单的另一组轨迹，它们是作为必须评估的行为给出的。 我们用原始资源σ进行评估。 结果是 每个交织都相对于由组合过程保持的资源进行检查。这个额外的检查是使“declare everything public”方法工作的关键一个例子有助于说明定义：取过程dc_d（z），d z σ d？e eCHANd！c d？c d！c d？c λσ。你说什么？c d！c λσ。λ σ。 ϵ交织D！Cd？c包括d！c和d？c是两个边没有 从σ的角度来看，它已经丢失了d是私有的信息这是我们能说的最多的。然而，交织是使用prefixing操作构建的，所以当我们相对于原始σ对其进行评估时，一些痕迹将被悄悄丢弃：d！c d？c σ=（d！cd？cλ σ。{}）（σ）（d？cd！cλ σ。{}）（σ）（λσ. {}）（σ）特别是对于任何一个B d！CBσd？CBσϵ因为σ d初级我们只留下了可能来自内部交流的痕迹，新x。当c∈dom（σ）时，（xc<$x（ y）σ=<$0）σ.因为σ，我们有Bλσ。，对于任何B。 当一个如果动作被交织，则交织以该动作终止总之，我们通过计算保守公开提升资源下P和Q的迹来计算P Q的迹，然后用关于P Q实际拥有什么资源的完整信息来实例计算在证明完全抽象之前，我们简要地检查了一些预期的法律。例如，为什么新的X。0）分 0）？ 将前者展开，我们得到A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313323分配。因为vc=。这个简单的例子揭示了α的重要性。（2）关键步骤是交换νc和νd，这依赖于引理νc<$νd<$B=νd<$(v)O <$iPi）=O<$iPi）你是谁？dO<$P{d/x}）：(ii)O <$cd.P）=c！dOP）O（）(iv)O <$newx.P）=cνc<$O<$P{c/x}）O < $）= O<$）（）=vcvdP）ρ[xc，yd]t∈O <$c（x）.P）σ：=vdvcP）ρ[xc，yd]下面是一个更复杂的例子c和dDλσ。{\fnSimHei\bord1\shad1\pos（200，288）} 当应用于特定的σ时，此行为产生简单集合{}，观察值−：对于忽略何时或在某些情况下是否存在通道新x。新y.P）ρ=新y.P）ρ[x<$c]CCD=vcvdP）ρ[xc，yd]=vdvcP）ρ[xc，yd]c和dDCP ρ[y <$d]=newy. 新x.Pρv c B. 这个引理的有效性同样依赖于可观测性：对于所有σ。2.1基本算子我们证明了充分的抽象证明语言中的每个操作符的同余结果。对于运算符而不是并行复合，我们证明：引理2.1（Core Congruences）以下所有关于闭过程的等价都成立：(i)O <$0）=<$0）(iii)O <$c（x）.P）=dc？dO<$P{d/x}）㈥P Q P Q这些等价性很容易证明;我们通过在两个方向上显示包含来证明每个等价性。为了说明，我们证明了：证据 设σ ∈ Σ，t ∈ O（c（x）.P）σ. 我们分析的情况下，推导情形：n∈O <$c（x）.P）σ324A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313很好。α=c？d，Qc？d<$σ=σ′，P′=P{d/x}其次是单调性。（Ⅲ）简单地说，就是定义了。◻⎨⎪() ==⇒() =∉()∣∈∥O <$）=O <$）O <$）完全不拥有资源（c_dom（σ2）），但两个进程都可能拥有一个资源（）=∣α∣σt′∈O <$c（x）.P）σ公开地D是一个频道。那么t=<$∈c？dO <$P {d/x}），定义为。结果c（x）。P，σ-α→P′，σ′ t′∈OP′σ′通过反演推理，我们看到有两种子情况：子病例：则t = αt′∈ φdc？dO P {d/x}由定义来简单地表示。子情形：α= α，c_dom（σ），P′=0则t=αt′= σb，因为O（0）σ′={σ}。 That∈dc？dO<$P{d/x}）再次2.2平行合成的同余我们对并行组合的处理可以追溯到本文开头的直觉：并发进程必须在它们之间划分资源，每个进程只使用它拥有的资源我们说σ分离成σ1和σ2，如果下列条件成立：平行的分离dom（σ） =dom（σ1）（σ1<$σ2）σ∈（σ1<$σ2）<$σ1cpriσ cpri，cdomσ2⎪⎩σ2(c) =pri=⇒σ(c) =pri,c∉dom(σ1)我们把这个定义理解为：如果σ1和σ2分别是P和Q持有的资源，那么σ可能是P Q持有的资源。子资源σi并不唯一地确定组合σ，因为对于子进程公共的资源3分离明确地捕获了公有和私有所有权的期望含义：如果一个子流程私有地拥有一个资源（σ1cpri），则另一个子流程执行为了证明P1P2P1P2，我们必须证明我们从公开提升的资源中交错跟踪的策略符合全局操作语义。一个关键的思想是，σ σ1σ2构成了子流程拥有的资源（在指称语义中）和复合流程拥有的资源（在操作语义中）之间的不变关系。不变3这就意味着带k的k不构成分离代数[5];参见§5.1。案例：A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313325∈̂∥I（）<$∈<$=<${∶（）= <$（）= }σ ∈ σ<$σ。12t∈（t1<$t2）（σden），其中ti∈ O<$Pi）σi.t∈（t1<$t2）（σden）则t ∈ O<$P1<$P2）σop.引理2.2（局部性）如果σ∈σ1<$σ2，则最初成立，因为σ σσ。νc步骤的不可观测性使问题变得有些复杂：这意味着复合过程对资源有一个额外的视角，称之为σden通常，σden低估了操作语义的真实资源σ考虑来自子过程的两个迹t1和t2 分别为P1和P2如果P1分配了一个通道，那么这个分配不会立即出现在t1中，因此也不会立即出现在资源σden的交织，而它会立即出现在σ，操作。在符号交织期间，甚至可以在σ1和σ2中私有地拥有相同的信道。这里的关键观察是，要么两个子过程最终都显示出给定的私有通道-在这种情况下，符号交织被过滤掉-要么至少有一个子过程没有-在这种情况下，它对通道的选择是无关紧要的。总而言之，四个资源-σop、σden、σ1和σ2-总是相关的σop，σden，σ1，σ2 σopσ1σ2，σdenσopc σ1cpriσ2cpri前提是，在证明中，我们应用适当的通道重命名以避免冲突。验证并行组合需要另一个重要的引理，抽象分离逻辑的局部性[5]。4● 若Qα<$σ=π′，则Qα<$σ1=π，且nd′′ ′ ′● 若Qα<$σ=σ，则Qα<$σ1= σ 2或Qα<$σ1=σ1，其中σ∈σ1<$σ2。该引理描述了一个动作在给定某些复合资源σ的情况下，根据它在子资源σ1上的行为可以进行的变换。提供广告资源永远不会引入新的错误，并且如果动作在仅给定σ1资源的情况下没有错误，则它对σ所做的改变必须仅改变σ1部分（框架）。局部性被引入来描述分离逻辑的框架规则[5]，但我们在这里使用它来描述并行组合中的交织步骤。我们有一个内部沟通步骤的相关引理Lem′ma2′.3（通信）若σ∈σ1<$σ2，Qα<$σ1=σ1′我们分别证明每个方向的同余：Qα<$σ2=σ2′然后引理2.4若I（σop，σden，σ1，σ2），σi<$Pi<$且t∈O <$P1<$P2）σop则引理2.5如果I（σop，σden，σ1，σ2），σi<$Pi<$，ti∈O <$Pi）σi，且[4]为了简单起见，我们在这里避免了序理论的定义，这需要将我们的一些构造提升到2π，否则就没有用了。326A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313⊢✓D0 cd.dc. 0，[cpub，dpri]Dcd。0c（y）. cy.dy. 0，[cpub，dpri]D[]νdd！CrecX.X和recn+1X. P P{recnX.P/X}。<$P[c/x]）ρ=<$P）ρ[x<$c]。这两个引理中的第一个更容易证明，因为我们给出了一个从复合过程的操作语义中导出的迹t这意味着保证子进程不会独立地分配相同的通道。第二个引理需要更加小心，使用上面提到的关于重命名未公开通道的见解。需要假设σiPi来确保我们正在处理的过程不会出错。在下面的例子中可以看出断层是有问题的原因新x.cx. 0 c（y）. cy.dy. 0），[c]τc！D0直流电。0，cpub，dpubd00，[cpub，dpub]这种推导的令人不舒服的方面是，通道d最初出现在过程中，即使它没有被拥有。结果，进程能够分配d，在某种意义上错误地捕获了最初出现的常数d。在进程分配了不同于d的通道的情况下，当它试图沿着恒定通道d通信时，它将出错。但在这种“幸运”的情况下然而，指称语义总是产生错误。它按组成计算轨迹，这意味着一个子进程分配的通道d不能立即供并行子进程使用我们的完全抽象结果只适用于非故障过程，这是一个微不足道的语法检查。然而，这确实限制了它对包含释放等特性的语言的适用性，这使得检查安全性更加困难。2.3全抽象为了完成完全抽象的证明，我们必须处理递归。我们从通常的展开引理开始，用标准的语法方法证明引理2.6（展开）我们有O <$recX.P）=<$nO <$recnX.P），其中rec0X.P<$n我们也有标准的替换引理：引理2.7（替换）我们有<$P[Q/X]）ρ=<$P）ρ[X<$Q]，将这些引理与前面的同余结果相结合，可以直接证明以下定理，该定理将观察到的操作迹与外延计算的操作迹相关联：定理2.8（同余）若P是闭的，σ <$P<$，则O <$P）σ =<$P）<$σ。A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313327̂（1 ）��O�O（1）（2）（3）（4）（5））O（）和σ<$C[Q]<$。 完整的抽象遵循组合性：̂定义P=Qi（P）σ=Q（Q）σ，其中所有σ都满足σ∈P ∈Q∈。DEN[客户为了证明这个定理，我们必须把它推广到处理开项。我们通过引入一个句法环境η来实现这一点，它是一个有限映射，将通道变量带到通道，将过程变量带到封闭过程。给定句法环境η，相应的语义环境η由下式给出：η x η x η X η X我们把η作为P上的一个句法替换来应用，写作ηP。那么，一致性所需的归纳假设是如果σ ηP，则ηP σPησ。ρ ρ对于所有C，设P=OPQi ∈O<$C[P]）σ=O<$C[Q]）σ，其中σ<$C[P] ≠ 0定理2.9（完全抽象）P=DENQiP=OPQ.3指称语义：添加活性为了完成我们对π演算的研究，我们必须考虑活性性质。进程代数中的活性以不同的形式出现，对分支行为和发散的敏感性不同[21]。每一个对活性的描述都对应于对基本可观察性的选择：给定一个过程P和一个上下文C，C P的什么行为是重要的？π演算的标准观测值是倒钩双相似性[13]，它位于线性分支时间谱的分支侧[21]。在这里，我们选择了一种更符合线性时间精神的处理方法：对接受痕迹的改编[8]。这种选择在一定程度上是一个品味问题，但它也允许我们坚持纯粹的迹论语义学，这使域理论保持在最低限度。我们没有看到任何直接的障碍，将我们的基于资源的处理名称的分支时间语义。分支敏感性和资源敏感性似乎基本上是正交的，尽管在给定所拥有的资源的情况下，当认为不可能时，分支当然可以被修剪。3.1活性观测量我们说一个过程是发散的，如果它可以执行一个不可观测的无限序列（即，内部）步骤，而不与其环境进行任何干预交互-也就是说，进程可以活锁。另一方面，一个不能再进行不可观察的步骤的进程被阻塞（等待来自其环境的交互）或死锁。我们的活性模型中的基本观测量是：相互作用的有限序列，在此之后过程偏离或出错;一个有限的交互序列，在此之后进程被阻塞，以及它被阻塞的通道（没有死锁）;以及●●328A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313●∣☇☇（2）∅∈LO []∈LO []即t∈LOP σ。我们仅假设t∈LOP σ，并导出ττσt=t∈活体观察LO（P）∶LBEH然后，我们定义一个无限的相互作用序列。请注意，我们把分歧和断层联系在一起：我们把两者都看作是错误的行为。特别是，我们认为任何能够立即发散或断层的过程都是等价的，而不管它们的其他潜在行为。这种观点是合理的，也就是说它产生了一致性，因为这种行为实际上是不可控的。例如，如果P可以立即发散，那么对于任何Q，P Q也可以立即发散。形式上，我们添加了一个新的动作δΔ，它记录了一个进程在沿着有限的方向集合Δ进行通信α ∶∶= α ΔΔ λ f inD IRλ {c！ ∶ c ∈ C HAN}<${c？ ∶c ∈CHAN}LT小种NTA;{，δΔ}NTAωLB嗯 中国→2LTRACE其中，NTA（表示因此，有限活性迹必须以δΔ动作或动作结束，而这两个动作都不能出现在无限迹中。每一个活动轨迹都包含了进程的一个完整行为：要么进程继续无限地相互作用，产生无限的轨迹，要么在有限的相互作用序列之后发散、出错或卡住因此，活性迹的集合不是预定闭合的。与安全跟踪一样，我们可以从操作语义中观察到活性跟踪。然而，我们使用以下规则中的最大α′ ′P，σ P，σα d t ∈ L O P ′ σ ′ gfp P，σ d <$P，σ阻滞Δ绿色荧光蛋白<$α<$σt∈LO <$P）σ<$∈LO <$P）σδΔ∈ LO<$P）σ其中，P，σ阻塞Δ意味着P，σ只能采取通信步骤，并且Δ精确地包含了可用通信的方向。由于所拥有的资源在通信可能的方向上是一致的，因此它们也在进程被阻塞的方向上δ{c！}cc。0cpubδcc。0cpri动作δ反映了一个完全死锁的进程，例如，它是惰性进程0的唯一轨迹。通过最大定点定义观测允许无限迹线被观察到，但也意味着如果一个进程在跟踪t之后发散，它的行为将包含所有迹线tu，特别是tτ。例如，假设P，στP，σ。如果t是任何生命跟踪发生了什么，我们可以使用第一个推理规则来跟踪，归纳，（2）A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313329（LO）⊑ ⊑ ⊆ ⊑ ☇⊑ ∀ ∈ ∃ ∈⊑其中Δ′=Δ{c∶σ（c） =pub}δσΔΔ否则，Q δ <$[cpri]= [c pri]δ<$= δ<${c！}{c！}[cpri]L<$−）L recX.P）ρρνB. L <$P）ρ[X<$B]▷我 我我 我C. c！ Δc？Δc 多姆σ方向ρπiP σ。 因此，发散是使这些可观察性连贯一致的重要一步是细化的概念。一般来说，说P精化Q（或P换句话说，P是Q的更确定性的版本。我们定义了一个关于迹的细化顺序t t tδΔtδΔ′ifΔ′Δtu t我们将其提升为迹集：U i不T.u联合不联合 这种细化的概念与接受痕迹的概念密切相关，它认为一个实现必须至少允许它的具体化所做的外部选择。它还将断层视为最允许的规范：如果Q断层，则任何P将精炼Q。此外，任何两个立即断裂过程是等效的。既然断层作用和发散作用被同等对待，那么发散作用也是如此。因此，跟踪上的简单细化排序具有与失败/分歧语义中强加的闭包条件非常相似的效果迹集的排序继承了2LTRACE上的完全格结构，也继承了LBEH上的逐点排序.在解释递归时，我们再次利用这一事实。3.2活性语义为了完成语义故事，我们需要解释阻塞动作。 我们定义QδΔ<$σδδ∃ （一）∈∨∈）（）下一页其示出了资源和阻塞之间的交互：在私有资源上的阻塞是可能的，但是不可观察（参见，在[2]中的δ上的投影）。比如我们有Qδ{c！}<$[cpub] =[cpub]{c！}[cpub]=δ{c！}活性的指称语义与安全性的指称语义基本相同，除了以下子句：L∑π.Pρ< $（δ{（）}<$λ σ. ）递归由一个最大定点给出，正如预期的那样。前缀动作的总和现在生成一个相应的阻塞集，记录外部选择（其中dir提取前缀的方向）。阻塞操作是使用前缀运算符“执行”的 因此，实际观察到的动作对应于 可用资源，如上面的示例330A. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313如果t=αt，u=αu，则“tu⋔⊔α<$（t<$u′）′如果u=αu，α不阻塞I（）δ=δ。σΔ∪ΔΔ1 2den∣● 若δΔi∈LO<$P1 <$P2）σi且Δ 1<$Δ 2，则有<$δΔ1<$Δ2<$σden∈LO<$P1<$P2）σop.⊢ ▸⊑最后，我们使用以下交织定义：t<$u<$gfpα<$（t′ <$u）如果t=αt′，α不阻断如果t=δΔ，u=δΔ′，Δ′，活的交织由最大的固定点给出因此，一个无限序列的内部通信（操作上，一个无限序列的τ移动）产生了所有可能的痕迹，包括断层的痕迹，因为它应该。仅当两个底层迹线都被阻挡时，并且仅当它们在相反方向上不被阻挡时，交织迹线才被 如果两个过程在相反的方向上被阻塞，那么它们的并行组合实际上并没有被阻塞，因为它们愿意相互交流（参见稳定性[4]）。3.3全抽象完全抽象的证明的结构类似于安全语义的证明。同余证明必须考虑阻塞动作，这在除了并行合成之外的所有情况下都是简单的。在这里，我们需要一个引理：引理3.1（阻塞同余）假设σop，σden，σ1，σ2. 然后● 若δΔ∈LO <$P1<$P2）σop，则δΔi∈LO <$P1）σi，其中Δ1<$Δ2，定义=LDEN和=LOP类似于安全语义，我们再次充分抽象：定理3.2（完全抽象）P=LDENQiP=LOPQ.4逻辑我们现在勾画一个逻辑推理的安全语义的进程。该逻辑证明了开放过程之间的细化--在外延上，跟踪包含;在操作上，上下文近似。精化由关于拥有资源的断言限定逻辑的基本判断是 p P Q，它说P的迹线是Q的迹线，只要初始资源和环境分别满足断言p和Γ（定义如下）。资源断言p如下：p ∶∶=真 假的 布拉克 布拉克 布拉克 小酒馆 普里斯河 x=yA. Turon，M.Wand/Electronic Notes in Theoretical Computer Science 276（2011）313