理论计算机科学电子笔记172（2007）545-587www.elsevier.com/locate/entcs通过资源和过程的系统建模：哲学，微积分，语义学和逻辑David Pym大卫·皮姆1，2惠普实验室英国布里斯托尔克里斯·托夫特3惠普实验室英国布里斯托尔摘要我们描述了一个方案的研究资源语义，并发理论，集束逻辑，随机过程，适用于数学系统建模。出于对结构和语义严格的离散事件建模工具，适用于企业规模以及组件规模的系统的愿望，我们介绍了一种新的方法，组成推理的基础上开发的SCCS与一个明确的资源模型。我们的演算模型的资源和进程的同步约束的可用资源的共同进化。我们提供了一个简单的指称语义作为参数化的阿布拉姆斯基的同步树SCCS语义。我们还提供了一个逻辑表征，类似于Hennessy-Milner逻辑的我们讨论应用程序的想法，如位置和访问控制。关键词：资源，语义，同步，进程演算，集束逻辑，模型检测，离散事件仿真，位置，访问控制，场论。献给戈登普洛特金在他60岁生日之际1引言：建模哲学这是一篇关于一个研究项目的论文，其目标是提供数学方法，用于建模系统，这些系统适用于部署以提供服务的大型复杂资源集合。例如，一个大公司可能需要一个统一的全球环境，比如说，100000个桌面[1]这项工作得到了英国皇家学会派姆工业研究金和巴斯大学的部分支持2电子邮件：david. hp.com3电子邮件：chris. hp.com1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.020546D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545机器，由数百台服务器支持，并连接到数千个其他外围设备，所有这些设备都连接在具有适当容量的安全全球基础设施上，能够接受来自各种移动计算平台的远程连接。这种系统的目的是向用户提供服务。例如，该公司将需要对其业务流程、制造业务以及研发工作的支持。在这样的规模下，我们不太关心形式上的正确性，比如说，关于一个小系统组件（如微处理器）的非常详细的规范也就是说，我们的方法应该能够在（很少）必要的情况下处理精确的正确性参数。建模任务的预期规模，以及我们希望从中获得的预测信息，表明在适当的抽象层次上构建模型至关重要[49]，无论是在系统的结构还是其动力学方面。这类系统的动力学通常部分地由它们的环境决定。然而，在我们预期的建模规模下，我们不可能希望捕捉到环境的精确行为及其对系统行为的影响一个很好的解决方案是使用随机方法。具体地说，我们假设环境事件按照给定的概率分布发生，并且必须处理事件和数据的系统组件可以通过嵌入网络来描述这些假设是基于操作系统理论和性能建模的大量经验[23，28]。我们将在第2节中对这些观点进行简要的讨论。转向系统的结构，我们认为的总体观点是，一个系统可以被有效地建模为一个位置或地点的集合，在这些位置或地点可以找到资源。给定这样的结构，我们可以执行流程，只要它们由所需位置的可用资源启用。执行流程的行为通常会导致资源的结构甚至它们的位置发生变化。因此，这主要是一篇关于实用系统建模的语义上有充分依据的方法的哲学论文。虽然受到企业级建模挑战的激励-例如捕获广域网的关键性能和完整性特征-我们关心的是确保我们的技术适用于解决组件和协议规模的正确性问题，以及从非IT领域提取的系统示例在第2节中，我们首先简要介绍了离散事件建模工具Demos 2000 [17]，这个系统在精确意义上可以看作是随后的结构（以及隐含的随机）理论的部分实例。它也为我们的建模哲学和数学发展提供了启示在§3中，我们介绍了资源和进程的同步演算SCRP，具有显式资源。演算的过程部分是米尔纳的资源部分是基于Kripke资源幺半群的，这些幺半群是D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545547聚束逻辑BI的语义[38，42，45，43，44]。两者之间的交互-即资源访问-由描述演算的操作如何修改可用资源的函数处理。SCRP的操作语义利用BI在第4节中，我们继续给出一系列基本系统的例子，旨在演示如何使用SCRP。在§5中，我们给出了SCRP的一个简单的域理论指称语义，表示为Abramsky正如Hennessy-Milner逻辑[48]提供了一种与CCS密切相关的逻辑，因此有一种模态逻辑，称为MBI，与SCRP密切相关。特别地，MBI通过BIMBI的基本定义在§6中给出，我们的系统例子在§7中重新讨论，基本的逻辑元理论在§8中描述。在第10节中，我们解释了我们的框架如何扩展到包含一个明确的、相当普遍的位置概念，在第11节中，我们解释了我们的结构如何提供对访问控制和身份概念的逻辑分析，例如阿巴迪、伯罗斯、兰普森和普洛特金[1]引入的概念在第12节中，我们对资源空间的场论作了一个简短的推测。SCRP和MBI的基本思想--尽管不是Demos 2000的讨论，不是指称语义，不是固定点，不是位置的讨论，也不是安全应用的讨论--已经在[41]中提出。本文件直接借鉴了该文件的几个章节。2灵感：Demos2k虽然我们对资源和过程之间相互作用的研究可以从基本的哲学和数学分析中得到启发-从历史上看，这就是它是如何发生的-它也可以被视为受到Demos 2000 [17]（以下简称Demos 2k）系统的启发。Demos2k是一种语义合理的离散事件仿真语言，已被用作复杂IT系统的大规模属性建模的基础。从概念上理解Demos2k的一种方便方法是将其作为进程代数和嵌入理论的优雅组合。出于我们的目的，这可以通过一个例子（一个经典的例子，取自[5]）来解释，图1中给出了Demos2k代码。考虑一个港口，有两个码头停靠船只。每个码头一次可供一艘船卸货。船只定期到达港口，如果有码头可用，并且有两艘拖船可以将其带到码头，则可以卸货。卸货后，船只离开码头，前提是有拖船将其从码头移走。港口有三艘拖船。在图1的模型描述中捕获了这种非正式描述，用于计算评估。考虑到Demos2k的正式语义，548D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545Cons arrival= 10.0; Consdocking=2.0;Cons卸载=正常（14，3）;Cons离开=2.0;缺点tug=3;缺点码头=2;Cons simdur=1000;Res（tugs，tug）; Res（jetties，jetty）;船类={ Entity（Boat，boat，arrival）; getR（jettes，1）;getR（tugs，2）;hold（docking）;putR（tugs，2）;getString（String，String，String）;hold（left）;putR（tugs，1）;int n（1）;}（*boat*）int n（int n，int n，int n）;关闭;Fig. 1. Demos2k用于停靠船只的代码[5]Birtwistle和Tofts [7，8]，我们如何从数学上考虑这个计算模型，在过程和资源方面？示范文本已经为如何考虑这些要素提供了直接的线索。船被表示为主动实体，其动态被表示为类定义。实际上，在演示文献中，实体和过程这两个术语可以互换使用。在本演示中，拖船和码头被定义为船只为了完成其功能而开发的资源程序中的常量只是提供了某些活动的持续时间的定义（由“hold”命令指定在boat类中定义boat实体的递归调用建立了一个由到达时间分隔的船只队列。由于等待被服务，船只然后可以竞争系统内的有限服务资源。的D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545549本例中的服务规程很复杂，它需要多种类型的服务和多个服务器实例。此外，服务实体与相同的服务元件（拖船）重复交互，但在其生命周期的不同点有源元件的这种选择是任意的。港口模型同样可以被认为是拖船，它们必须结合起来为码头提供一艘船，以及需要拖船才能移走船只的码头。在这种观点中，船只是拖船和码头所依赖的有趣的是，这种双重模型在像Demos这样的语言中表达和捕获要困难得多虽然进程代数模型似乎通过将系统的所有元素视为活动进程来避免这种困难，但实际情况并非如此。上述模型的两个抽象版本在进程代数中都有不同的解释模型中主动和被动元素的特定选择可能对分析的难度产生重大影响。通过使所有的模型元素都是活动的，直接过程代数方法不允许利用模型的简单部分来简化计算。这种方法也不允许在多个呈现之间进行简单的转换，这将表明可以进行多么简单的计算。请注意，在这个模型中，没有明确表示端口的结构，也就是说，没有明确表示系统的结构。事实上，在这个例子中，甚至系统的隐式表示也是非常弱的，很简单，是不必要的。然而，在其他示例中，系统的结构至少隐含地被表示是重要的。例如，在涉及系统安全的示例中，诸如当表示对系统的各种组件的访问的控制的方面时，必须表示各种组件之间的连接性我们将在第10和11节中再次讨论这些观点。我们的结论是，我们随后的结构发展并没有解决的问题，提供随机组件相媲美的Demos2k。这种发展超出了我们目前的范围。我们在这里只注意到，[7，8，9，10，11]中提供的Demos2k的语义清楚地表明了Demos2k的随机组件“包裹”结构核心的意义。3资源与进程在本节中，我们将描述一个简单的资源和进程的同步演算（简称SCRP），它基于(i) 基本资源语义可以被解释为集束蕴涵逻辑（BI）的基础[38，42，45，43，44]，以及(ii) Milner的通信系统同步演算（SCCS）的适当改编我们对资源语义学的方法--也就是我们对资源概念的解释--有两个关键方面。首先，它本质上是语义的，而不是句法的;550D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545其次，它是通过数学建模的经典方法获得的，也就是说，我们对我们所需的资源的属性给出了公理化的描述，并通过支持良好的示例验证了我们的选择。我们发现以下资源的公理化是合理和有用的[38，42，45，43，46，27]：• 资源元素的集合R• A（部分）组合，R：资源要素的R×R-R• 资源要素的比较;以及• 零资源元素，e。在数学上，我们可以方便地捕捉这些性质作为一个预序部分交换幺半群，R=（R，E，E，±），服从以下与幺半群结构和阶相关的双函性条件对所有的r1，r2，s1，s2，若r1±s1，r2±s2，则r1<$r2±s1<$s2.根据我们的一些技术发展，我们称这样的结构为Kripke资源幺半群。这一定义得到了广泛的自然发生的例子的支持我们在下面讨论其中的一些。(i) 一个简单的例子是自然数，这里包括0，N=（N，+，0，≤），其中，组合是以0为单位的加法给出的，比较是以小于或等于给出的。就我们预期的资源语义而言，这个例子可以被看作是一个基本的成本模型。(ii) 更一般的例子是monoidal范畴（C，n，I），其序由箭头的存在给出。(iii) 一个计算上更丰富的例子是Petri网[45]。形式上，一张网N =（P，T，术前，术后）由位置和变迁的集合P和T以及两个函数前、后：T→ M，从过渡到标记，其中标记是位置的有限多集，M表示所有标记的集合。 一个标记相当于一个功能M：P→N从地方到自然数，在所有地方都是零，但有有限多个地方。标记的添加由（M + N）p = Mp + Np。D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545551Petri网的这种形式化可以在几个方面被视为Kripke资源幺半群。一种方法是内化标记上的可达性关系。如果M和N是标记，则定义MNi there aret，MJ s. t.M=pre（t）+MJ，N=post（t）+MJ。然后，我们可以在标记上定义一个前序±，M±N i ≠有M1，.，M ns.t. M=M1···Mn=N。我们让[−]，+的单位，表示空标记。 它遵循 （M，+，[−]，±）是一个预序交换幺半群。(iv) 最后，基本不相交模型，或BDM，它是分离逻辑工作的核心[45，46，27]，为我们的子系统开发提供了一个起点。假设我们给定一个无限集合Res ={r0，r1，. . }。我们认为Res的元素是可以分配和释放的原始资源或资源ID。部分幺半群的结构是通过把世界看作是Res的有限子集，而Res是不相交集合的并集来给出的。更详细地说，”吴彦祖说。⎧mmn=↑否则。的单位是{e}，我们取±表示相等。 这个例子是Ishtiaq和组成和排序结构提升到资源元素的集合。 让设R，S∈R（R）为R 然后定义，例如，.{r s|r∈Rands∈ S}如果每个r <$s ↓RS=↑否则，对于单元{e}，例如，4R±S i ≠对所有r∈R，存在s∈S使得r± s。等式=则由±的对称闭包给出。在进程代数[35，4，26，36]中，资源的常见表示是作为一个分离的进程。例如，一个信号量被表示为一个两态过程，表示令牌当前是否可用。已经有一些扩展[12]试图显式地对资源进行建模，但是这些方法同时携带进程代数的通信结构和资源的表示我们认为资源是组织的根本4 注意，这里给出的关于R（R）的排序只是许多可能的选择之一;例如，参见[22]。552D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545基本演算的原理，在面向过程的离散事件语言中采用的方法[5，6]。已经有一个证明，米尔纳然而，很明显，这种方法仍然包含SCCS的所有基本行动结构。我们的方法是在SCCS的意义上考虑资源和过程的共同进化，同步受到资源可用性的约束对于我们目前的开发，直接建立在[41]上，BDM中的资源集是一个方便的抽象层次，我们最初不需要进一步的特殊属性。 我们也可以要求R S只有在R和S不相交时才被定义。 我们把R1和R2的并集写成R1，R2，并强调复合与并集是完全不同的。更一般地说，我们可能会采取更复杂的资源结构。例如，我们可以取R= R1×...×Rm，其中有一个共同的立场，并根据±i的每一个chRi。我们的资源和进程演算的起点是米尔纳注意，异步演算CCS是SCCS [35]的子演算. 我们的主要发展它通过使用我们的查询来查看状态元素E−a→EJamening对于要启用的动作a，过程E演化为EJ，并相应地修改可用资源。我们通过假设存在一个部分修改函数μ来实现这种观点的改变，该函数为每个动作a和每个资源集合R分配资源集合μ（a，R），该资源集合是用资源R执行a的结果。因此，我们的动作前缀的运算规则基本上采取以下形式：R ，a：E−a→μ（a，R），Eμ（a，R）的定义。如果资源R不足以使动作a被启用，则μ（a，R）将被定义。同步是通过要求动作的并行组合a#b来实现的，只有当资源环境可以分解为单独支持a和b时因此，我们的并行组合操作规则基本上采取以下形式R，E→a1μ（a， R），EJR，E→a2μ（a， R），EJμ（a1#a2，R1<$R2）1 1 1 11 2 2 2 22a1#a2R，E×E μ（a#a，R），EJ×EJ已定义;1 2→1 21 2也就是说，必须有可能将R分解为资源R1和R2，使得R=R1<$R2，即同时支持a1和a2所需的资源，尽管我们承认R1和R2之间可能相等，因此允许根据需要共享。请注意，同步是由资源调节的，在ACSR [12]中，瞬时事件提供了基本的同步机制。还要注意的是，与我们当地的条件相反，Gastin和MisloveD. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545553→[21]机制需要一个全局构造来实现同步。同时合成规则的另一种表现形式是“函子”形式，这取决于合成的定义R1，E1→a1 RJ，EJR2，E2→a2RJ，EJ1122，RR ，E×Ea1#a2RJ◦ RJ，EJ×EJ1 2 12→1 2 1 2其中，由调制函数的相干条件所隐含的对函性的限制是，RJ<$RJ= μ（a #b，R1<$R2）.1 2正如我们将在本节末尾看到的那样，这种方便的表述确实是可能的。这种方法的一个基本结果是，我们应该希望在一个过程中保持导致当前资源使用转换的所有交互。从某种意义上说，我们需要知道如何分解当前的资源利用率。因此，我们必须放弃在SCCS中优雅地使用自由阿贝尔作用群来描述作用，将自己限制在更基本的自由阿贝尔幺半群[35]，A =（Act，#，1）。如果我们取一个阿贝尔群，那么动作a可能由a#b−1和b的合成产生，因此，在某种意义上，使用了更多的资源（因为b#b−1变得隐藏）。以资源为基本组织原则，这种隐藏形式使然而，我们的公式允许复合原子动作的公式化，这些动作能够模拟离散事件模拟语言（如Demos [5]）的困难等待直到构造。SCCS与CCS一样，使用了限制的概念。 在我们的背景下，一个更自然的概念是局部行动，其中资源的集合只可用于它所绑定的过程。非正式地说，应该采取的形式R<$S ，E−a→RJ<$SJ，EJ、R，（νS）E（νS）aRJ，（νSJ）EJ其中，这些组件在随后的进化中被“隐藏”。这里描述的演算，首先在[41]中公式化，被称为资源进程的同步演算，或SCRP（发音为'scrap'）。在SCCS和π演算的基础上，给出了π演算的过程元素的语法.语言的限定部分如下：• 1.单位行动;• a：E-执行动作a成为进程E的进程;554D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545i=1i=1我• E+F-一个过程，演变为E或F，单位0;• E×F--一个同时使用E和F资源的进程;• （νS）E-相对于资源S和修改函数μ具有局部或隐藏演化的过程，如下所述。我们抑制重新标记，将其视为元理论操作。该语言的递归部分具有以下语法：• 过程变量X和固定点fixX.E.为了实际的目的，我们使用常数C的定义固定点。def=E，而不是与标准进程代数不同，我们必须定义进程演化的资源环境这是作为从幺半群中提取的一组允许的动作给出的因此，我们的操作判断基本上是这样的形式R ，E−a→RJ，EJ并且意图被理解为R被假定为从Kripke资源幺半群中提取的资源元素的集合。但仅此还不够。正如我们已经看到的，我们必须在幺半群的行为和系统中的资源之间建立一个关联。现在，我们采取以下措施：• 部分函数μ：Act×R（R）-R（R），• μ（1，R）=Rand，如果μ（a，R）↓anddμ（b，S）↓，则nμ（a#b，R<$S）=μ（a，R）<$μ（b，S），并且，• 对于所有的a和R，恒等式id（a，R）=R。在我们对SCRP我们把动作集a写成μ−1S，使得μ（a，S）↓。为了给出隐藏的规则，我们需要一个删除的辅助定义：• 令A ={ai，.一个动作是一组有限的动作。 然后定义A= a i= a1 #. #上午。如果b是A的一个子集上的乘积，那么我们称之为• 设αs和βs表示原子作用。 让a = α1k1 #. #α mkmb= β1l1 #. #β nln.然后定义a/b=m{α ki|对所有1 ≤ j ≤ n，α i/= β j}.D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545555法一R，a：E−→μ（a，R），Eμ（a，R）↓aJbJProdR，E−→μ（a，R），E S，F−→μ（b，S），Fa#bJR<$S，E×F−→μ（a#b，R<$S），E×F一个J夏天我R，Ei−→μ（a，R），Ei一个Ji= 1， 2R，E1+E2−→μ（a，R），EiaJ J JRS，E−→R S，E隐藏μ（a/μ−1S，R）=RJa /μ−1SJJJR，（νS）E−→R，（νS）E表1有限SCRP出于理论和语义的目的，我们采用递归过程项，由操作语义中的固定点规则定义。一个JR，E [fixX. E/X]−→μ（a，R），ERecaJR，fixX.E−→μ（a，R），E表2递归SCRP在实践中，遵循Milner [36]，我们使用常量规则定义递归过程：ConR ，E−a→μ（a，R），EJR ，C−a→μ（a，R），EJCdef=E.显然，所得到的系统等价于用不动点法则所得到的系统.定义3.1互模拟，<$μ，是资源-过程对R，E上最大的二元关系(i) R ，E−a→μ（a，R），EJimplies，forsomeFJ，R ，F−a→μ（a，R）， FJanddμ（a，R），EJ<$μ μ（a，R），FJ，和(ii) R，F−a→μ（a，R），FJ意味着，对于某个EJ，R ，E−a→μ（a，R），EJanddμ（a，R），EJ<$μμ（a，R），FJ.我们将需要互模拟是一个同余的熟悉性质，也就是说，在我们的设置中，如果对所有R，R，E<$μR，F，则对所有明显项R，a，G，和S，R ，a：E<$μR ，a：F，R ，E+G<$μR ，F+G，R<$S ，E×G<$μR<$S ，F×G，和R，（νS）E <$μR，（νS）F.556D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545→命题3.2互模拟是一个同余。证据通过归纳对资源-过程对结构的直接论证Q我们用一个简单但相当有用的性质的正式声明来结束本节，即由动作引起的资源修改完全由μ决定：命题3.3设a是一个带有修正项μ（a，−）的作用。若R，E RJ，EJ，则RJ= μ（a，R）.−a→证据通过对SCRP操作语义中派生结构的归纳，得出（临界）基例是直接的。对于示例归纳步骤，假设应用的最后一个规则是Prod，R ，E−a→RJ，EJS ，F−→bSJ，FJ.R<$S，E×Fa#bRJ<$SJ，EJ×FJ根据归纳假设，我们有RJ=μ（a，R）和SJ=μ（b，S）.所以，RJ<$SJ=μ（a，R）<$μ（b，S），因此，根据μ上的相干条件，RJ<$SJ=μ（a#b，R<$S）。Q在续集中，在没有明显的混乱可能发生的地方，我们只写RJ为μ（a，R）.4一些系统示例我们提出了一些例子，取自[41]，以说明在并发设置中通常需要的交互：• 相互排斥;• 资源转移;• 握手;• 私人渠道;• 异步切换这些例子--参见[3]关于并发系统基本组件的讨论--被选择来说明我们如何在这个简单的设置中指定核心并发前四个例子可以说得足够清楚，而不需要详细描述所涉及的克里普克资源幺半群。对于最后一个示例-异步切换-我们采用以下Kripke资源幺半群：假设资源元素R的基本集合，对于R的n≥0个不同副本，好的。-是的-是的其中hR0={e}。我会将剩余的资源分配给Rm±Rnn次i ≠m≤n，则紧接着是双函性，并且满足一定的要求D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545557= 临界：E关于修正函数的定义和预测的解释，我们在§6中讨论过，我们得到一个本质上是直觉主义的模型。如果我们采用离散排序，这并不适用于所有的例子，我们应该得到一个本质上经典的模型，一个类似于分离逻辑[46]中得到的情况。虽然我们在[41]中解释过，将“使能”函数（指定动作发生所需的最小资源）与修改函数区分开来在逻辑上是有问题的，但我们仍然发现将这个想法用作符号化的解释是有帮助的。具体来说，我们写ρ（a）= min {R|μ（a，R）↓}存在这样的最小值。在异步切换示例中使用的上述Kripke资源幺半群的上下文中，该缩写特别方便。互斥在这个例子中，我们有两个（或更多）进程和计算中的一些点，在这些点上，它们中的最多一个可能是活动的，通常被为此，我们以下列方式定义一个过程defE=nc：E+临界：E临界E临界值关键为了给出足够的细节，我们假设要启用的各种动作所需的最小资源由ρ（nc）={e}（nc是现在，资源过程R，E×E，其中μ（a，R）=R，对于所有的a，定义了一个表现出互斥的系统。重要的一点是，在应用Prod规则时，我们有R=R<${e}。换句话说，该资源在作为空资源的同时作为其自身可用。因此，我们的系统的演变如下：R、E×ENC#NC→R，E ×ER、E×Enc#关键→R、E ×E临界nc#关键R、E×E临界R、E×E临界→R、E×E临界nc#关键→R，E × E。请注意，在任何时候都没有执行action critical #critical，也没有看到两个过程都处于状态E critical× E critical。+ 临界：E558D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545=1：E2+put注意，在这个例子中，我们使用的资源扮演了一个信号量的角色;这证明了演算直接利用资源的能力。对于这个问题，一个更标准的进程代数解决方案是通过握手进行通信;我们将在下一个示例中演示如何在这个演算中实现这一点。资源转移作为上述信号量示例的扩展，我们可能希望建立一个系统，在该系统中，在任何一个时间只有一个并行任务是实现这一点的一种方式描述如下。我们将资源集R1和R2作为资源集。然后我们定义以下修改函数：μ（put1，R1）=R2 μ（get1，R1）=R1μ（put2，R2）= R1μ（get2，R2）= R2.我们采用以下最小要求，ρ（get1）=R1和ρ（get2）=R2。我们还取ρ（put1）=R1和ρ（put2）=R2。我们采用以下过程定义：defE1 = 得到1：E1critical+1：E1E1临界定义临界1= 1：E1def+put：E1E2 = 得到2：E2临界+1：E2E2临界值关键2其中，当然，我们取ρ（1）={e}。则系统R1<${e}，E1 ×E2表示其中过程E1和E2交换资源的所有权，以便它们可以进入各自的临界区：R，E1× E2得到1#1R ，E1×E2.1→2关键这个系统有两个明确的概括：我们可以扩展资源的数量defE1 = 得到1：E1critical+swap1：E1+1：E1，其中μ（swap1，R1）=R2，我们有ρ（swap1）=R1，以及明显的对称定义。然后，我们获得一个具有指定或可转让令牌的互斥系统从这些例子中可以清楚地看出，修改函数的形式μ：Act×R（R）-R（R）允许并发进程之间的资源转移的非常灵活的模型：E2，D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545559握手在这个例子中，我们希望两个进程只有在相互同意进展的情况下才能继续进行。换句话说，在计算中有一个点，该点之前是相互协议或“联合”的点。以下过程定义将说明这一点：E1定义JE1E等Edef1 ：E+go1 ：E1J2 =等待E2：E2+开始E2 ：E2我们取ρ（goE1）=R1和ρ（goE2）=R2，但重要的是R=R1<$R2，记住这与R1，R2不同（回忆一下，我们对并集使用这个列表表示法并且只能通过使用Prod规则来我们取ρ（wait1）=ρ（wait2）={e}。R，E1×E2的演化如下：R、E1 ×E2waitE1#waitE2→R，E1×E2GoE1#GoE2R，E× ER，EJ × EJ。1 2→ 1 2请注意，E1和E2要么等待，要么一起进行。显然，在一个更大的系统中，状态E1和E2不需要同时到达隐私在前面的示例中，我们可能希望确保只有E1和E2可以通过使用组合资源进行交互。所以我们会形成一个过程（νR1<$R2）（E1×E2），其中E1、E2和ρ如上所述。注意，每个go Ei由可用资源启用的要求本质上导致每个Ri和E i的关联。非同步越区切换这个例子的经典形式是生产者-消费者问题：也就是说，有一个流程可以生成工作，然后将其留给另一个流程稍后处理。考虑以下过程定义：产品缺点def= nowwork：Prod+work：Proddef= wait：Cons+cons：Cons，560D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545→→→→其中，我们要求ρ（nowork）={e}，ρ（wait）={e}，ρ（work）={e}，ρ（cons）=R，并且，对于R的n>0的分布，，R`Or.-是的-是的Rx，n次μ（nowork，{e}）={e}μ（nowork，Rn）vv=Rn μ（wait，{e}）={e}μ（wait，Rn）=Rnμ（功，{e}）={R}μ（功，Rn）=Rn+1μ（cons，R n）= R n−1。因此，该系统{e}，产品 ×缺点表现为具有计数器R的给定系统的一般状态，我们有以下演化{e}，产品 ×缺点不工作#等待→ {e}，产品 ×缺点{e}，产品 ×缺点工作#等待→R，产品 ×缺点Rn，Prod×Consnowwork#waitRn，Prod×ConsRn，Prod×Consnowwork#consRn−1，Prod×ConsRn，Prod×Conswork#consRn，Prod×ConsR n，Prod × Cons work#wait R n+1，Prod × Cons.5一个简单的指称语义我们为SCRP提供了一个指称语义，它是完全抽象的，相对于通常的操作前序[35，24，2]对SCRP的明显适应。我们的语义是一个参数化的资源Abramksy我们的参数化相当于包含SCRP对SCCS施加的资源约束，关键情况是动作前缀，并发合成和隐藏。Abramsky我们不再重复阿布拉姆斯基建筑的细节为了本节的目的，我们明确说明了我们迄今为止省略的不确定过程。我们假设存在一个基本的未定义过程Ω（遵循[2]），基本操作假设ΩR，Ω ↑。D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）5455610α+1α→ααμ然后，我们采用表示每个组合子的unfinedness的明显规则比如说，R，Ei↑R，E1E2↑i= 1， 2，其中，x是+或×。隐藏的处理方式类似。为了本节的目的，我们还假设每个μ（a，−）：（R）→（R）是连续的（即，，单调，保持ω-链的lubs，使得μ（a，iRi）=iμ（a，Ri））。我们从SCRP的必要操作前序开始[24，2]。这个关系的对称闭包是定义3.1中的（强）互模拟。定义5.1[运算前序]设R，E和R，F是闭的SCRP-项。我们定义运算前序R，E≤μR，F归纳定义如下，其中α是序数：(i) R，E≤μR，F，对所有的R，E，F;(ii) R、E≤μR，F，如果，对于每一个，a∈Act，(a) R ，E−a→μ（a，R），EJimplies，对于omeFJs.t.R ，F μ（a，R），EJ≤μμ（a，R），FJ，和−a→μ（a，R），FJand(b) E↓意味着F↓，以及R ，F−a→μ（a，R），FJimplies，对于omeEJs.t. R ，Eμ（a，R），EJ和μ（a，R），EJ≤μμ（a，R），FJ;(iii) 对极限序数λ，R，E≤μR，Fi ∈α λ，R，E≤μR，F;λα(iv) R，E≤μR，F，若对任意α≥0，R，E≤μR，F.进程被解释为资源的幂集幺半群上的连续函数。因此，相对于过程变量的解释I，我们有[[E]]D，I：I（R）→ D，其中D是SCCS的同步树的Abramsky当只考虑有限项时，我们去掉上标I我们的SCRP语义和Abramsky的SCCS语义之间的关键差异• SCRP• SCRP然而，这些变化都不需要修改阿布拉姆斯基相反，它们是通过在R上的参数化来处理的。因此，我们勾勒出Abramsky562D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545=阿布拉姆斯基SFP是代数域的一个范畴，在下面列出的结构下是封闭的Σ• 分离的总和。a∈ADa是通过取一个可数的域的家族。元素记作a，da，其中a∈A，d∈D a.这种结构是解释同步背景下动作前缀的关键。• 普洛特金的权力领域。P[D] -对于具有± -阶的域D，具有Egli-Milner阶：对X，Y∈D，X±EMYi ∈ N，对所有x∈X，存在y∈Ys. t. x±y，且对所有y∈Y，存在x∈Xs. t. x±y。我们需要回忆一下域理论中的一些辅助定义[40]。设X为零。def(i) Con（X）={d|有d1，d2∈X s. t.d1±d±d2}。(ii) XdefCl（X），其中Cl（X）是与Lawson相关的闭包=Contopology [2].X是凸闭的，如果X=Cl（X）; X是闭的，如果X=X。P[D]与它有几个连续的操作：· P是函子：如果f：D→E，则P（f）：P[D]→P[E];· Singleton：{|− |D → P [D]，定义为{|D|} def {0};· 联轴节：：P[D]2→P[D]，定义为XYdef=Con（XY）;· 大并集：：P[P[D]→P[D]]，定义为：def· 张量积，定义如[25]。（Θ）2016年05月05日05：05：05Θ）;• 空集合的邻接。具有空集的Plotkin幂整环P0[D]同构于（1）P[D]，其中（1）是提升单点整环，是合并和.我们现在可以描述确定域D的域方程（D实际上是D（Act）的形式，其中Act是我们的载体动作集，但是，如在[2]中，我们抑制了Act）。我们定义D为初始解，ΣD=P0[a∈Act0ΣP [a∈ActD]的底元素是{|⊥|}。D]。Abramsky提供了D的结构的一些相当详细的细节，其中大部分然而，拼出有限元素K（D）D是有用的，定义如下：• n ∈ D• {|⊥|} ∈ K（D）• 如果a ∈ Act且d ∈ K（D），则{|阿查，d|} ∈ K（D）• 若d1，d2∈ K（D），则d1d2∈K（D）.注意到D可以被看作是一个过渡系统，≤μ，D. 皮姆角Tofts/Electronic Notes in Theoretical Computer Science 172（2007）545563μ采取如下行动• d−a→DJi<$a，dj<$∈d;• d↑i∈d。然后，我们可以根据SCRP在开始引理5.3之前，我们回过头来考虑这个转移系统的结构。利用到目前为止总结的思想，我们现在可以描述第一个关键命题，这个结果完全关于域D，不需要任何调整来处理我们的资源语义。命题5.2（内部完全抽象）对所有d1，d2∈D，d1≤μd2≤d1±d2。下一步是在D中解释SCRP。 回想一下，SCRPR ，E−a→RJ，EJ，其中RJ=μ（a，R）。SCRP• 唐飞[2][2][3][4][5][6][7][a∈Act产品条款中使用的，定义为ΣD) 2→a∈ActD]，• 地图fΦ（x，n）=fΦ（n，x）=nfΦ（da，db，eb）= dab，Φ（d，e）n.Σ[001 pdf 1st-31files]gS：[D → D] →[（a∈Act用于隐藏的子句，定义为D）→D]，g SΦ={|⊥|}⎧{|a，Φ d|}如果a ∈ μ−1SgSΦa，d=否则的话。注意我们的定义与Abram-sky的限制情
我的内容管理
展开
