基于网络的匿名通信与分布式进程的定时协调模型研究.

理论计算机科学电子笔记175（2007）3-17www.elsevier.com/locate/entcs基于网络的匿名通信Gabriel Ciobanu1ab和Cristian Prisacariub“A.I.Cuza”大学，计算机科学学院大道。Carol I no.11，700506 Iai，Romania.b罗马尼亚科学院，计算机科学研究所。Carol I no.8，700505 Iai，Romania摘要在本文中，我们提出了一个新的模型通信分布式进程的定时协调。所提出的模型是π演算的位置，类型和定时器的扩展。 类型用于表示对分布式资源的受限访问。定时器定义通信信道和资源的超时。我们定义了模型的语法及其操作语义，并提供了一些关于类型系统和计时器的结果。 定义了一个定时倒钩互模拟关系来比较进程。协调分两个阶段给出：通过策略性地为计时器分配值，然后通过采用一组附加的协调规则。 定时协调方面通过协调器对给出。 它由一个可动态改变的定时器分配函数和一个协调规则。作为一个说明性的例子，我们将我们的模型与Reo协调模型的渠道联系起来。保留字：计时器、打字系统、位置、协调器1介绍在过去的二十年中，许多协调语言和模型被开发出来。[21]中给出了关于协调模型和语言的全面调查。最近，在[20，7]中，作者调查了代理系统的协调模型的最新技术水平（在过去几年中已经变得非常感兴趣）。协调模型分为两大类：数据驱动（Linda类）和控制驱动或基于通道（Manifold类）模型。数据驱动模型的一个缺点是，它们通常缺乏复杂多组件应用程序所需的灵活性和控制，而这对于控制驱动模型来说是典型的。我们认为分布式代理的协调主要是一个消息通信和时间调度的问题。时间很重要，无论是限制1提交人得到CEEX项目47/2005的部分支助。2电子邮件：{gabriel，cprisacariu}@iit.tuiasi.ro1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.0024G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3通信可用性和用于实施有限的资源访问（从基于信道的协调的观点来看，通信信道表示资源）。在[15]中，Hennessy和Riely引入并研究了一种称为分布式π演算（Dπ）的形式，作为π演算的类型和位置的扩展[18]。Dπ提供了一个理论框架，用于描述具有受限资源访问的分布式进程之间的通信。我们采用Dπ（因此我们能够对受类型限制的通信进行建模），并在通道名称上引入计时器，以便定义通信的超时我们还将计时器附加到通道类型，以限制它们在进程的类型环境中的存在。所有的计时器都在减少。每当信道定时器达到值1时，该信道被丢弃（在该信道上不再可能进行通信，并且系统前进到另一状态）。类似地，每当信道类型的附加定时器到期时，该信道类型就会丢失。新的演算被称为时间分布π-演算（tDπ），它在[10]中被介绍在这种形式上，我们通过为定时器分配特定值并定义一组恒定的协调规则来定义定时协调该模型为我们设计协调系统提供了一个强有力的正式基础;协调语言将作为该模型的语言体现。进程代数的时间方面是一个非常重要的研究课题。在[6]中引入并研究了具有定时器构造的π-演算的扩展。在[5]中给出了基于离散时域的进程代数，在[24]中给出了定时互模拟的变体与我们的工作最相关的协调语言是Manifold [4]及其在[17]中的时间扩展，以及Reo [2]。流形是基于理想工人理想经理（IWIM）模型[1]，基本上有两种过程;经理和工人。经理协调工人和他们之间的沟通。工作者是计算过程，他们不知道谁需要他们的“工作”结果，也不知道他们与谁交流。Manifold是事件驱动的：管理器等待一些特定的事件来触发一些动作;这些动作决定管理器改变其状态。基于通道的协调语言的其他模型也基于π演算，是MoCha-π[14]和σπ[3]，我们在结论中更详细地描述了它们。Linda [9]是一种流行的数据驱动协调语言，它使用元组的数据空间。它将应用程序的计算部分和协调部分明确分开。在[8]中，作者使用进程代数来表示Linda的协调原语，并给出了关于观测等价性的几个结果。μKlaim [12]最近被提出作为KLAIM（数据驱动）协调语言的模型时间也被调查的数据驱动的协调模型。超时的一种形式可以用JavaSpaces或TSpaces表示。在Timed Linda [11]中，考虑了全局时钟，并且基本动作（in，out或rd）不需要时间来执行，即， 一个时间单位意味着执行这样的（原子）动作。引入了一个新的动作，该动作使得只在预定的时间内等待元组成为可能。G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）35时间单位的数量;进程在此数量的时间单位后改变其状态。在[16]中引入了Linda的几个具有不同时间概念的推广。最近，在[22]中提出了基于元组中心的模型ReSpecT随时间的扩展。在tDπ上引入的协调模型包括在控制驱动模型的大类中。tDπ中的触发事件是信道上的通信，或具有go的迁移，或定时器的到期一个tDπ进程是急切的，因为它需要尽可能多地进行通信在协调过程中使用定时器，tDπ仅通过在进程之间传输消息或通过使用信道类型限制信道上允许的动作来超越协调。定时器和它们施加的时间限制提供时间同步。在tDπ中，我们有外生配位。 一个进程（管理器）向其他进程发送消息，其中包含某些通道的权限（作为类型）通过这种行为，外部进程指示其他进程允许它们做什么。请注意，在我们的模型中，任何流程都可以成为管理器。我们从真实代理系统的许多细节中抽象出来，只关注与协调模型相关的基本功能。我们认为，作为主要行动的沟通渠道。在分布式环境中，进程也可以从一个位置移动到另一个位置。计时器和类型用于限制和协调这些操作。第二节简要介绍了时间分布π-演算的语法和语义。详细介绍见[10]。在第2.3节中，我们给出了一些技术性结果，表明对于归约规则和等价关系给出的动态语义，类型系统和类型规则是合理的。给出了一个时间倒钩互模拟关系。协调部分在第3节中讨论。与Reo模型相关的简单示例见第节3.1.最后，我们通过比较我们的协调模型与其他三个最近提出的模型的文件。2时间分布π-演算2.1语法在tDπ中，等待通道上的通信不再是无限的（就像在Dπ中一样）;如果在预定义的时间间隔内没有通信发生，等待过程将进入另一个状态。这种方法导致了一种及时共享信道的方法。每个通道的定时器Δt使通道仅在由离散值t确定的时间段内可用于通信。 我们认为计时器用于输入和输出通道。在输出中添加计时器的原因是，在分布式系统中，我们有多个客户端和多个服务器。这意味着客户端可以根据等待时间从一个服务器切换到另一个服务器。为了简化我们的演示，我们选择了一个更简单的π演算，并省略了匹配或求和的语法。通信信道被认为是6G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3X一个固定的资源在一个位置。输入和输出通信的语法使用一对进程。例如，输入表达式aΔt？（X：T）。（P，Q）在Δt给定的时间间隔内，只要建立了通信，就演化为P;否则，就演化为Q。变量X被认为只在P中有界，我们应该提供它的类型T;类型见表2。表1：tDπ的λu：：=x| aΔtl ::= x| Kv：：=bv| u | l| u@l|（v1，..，vn）X：：=x| X@l变量名称定时通道变量名称位置名称基值名称已定位的名称值元组变量定位变量P，Q：：=停止| P|Q| （ν u：A）P| 戈湖（P，Q）| u！你好（P，Q）| 你呢？（X：T）。（P，Q）|CUPM，N：：= M |N| （ν u@l：T）N| l[[P]]Γ终端合成通道限制移动输出输入复制组合定位限制定位过程| (X1,.., Xn）变量两个通道相等aΔt1=aΔt2当且仅当a1=a2且t1=t2。等待1 2通过将Δ t视为∞，允许在通道a上无限地进行。 例如一种输出过程由表达式a∞定义！你好（P，Q）永远等待发送值v，模拟无时π演算中输出过程的行为。 在下面的表达式，两个进程并行运行，并可以沿着公共通道a进行交互：aΔt！你好（P，Q）|aΔtJ？（X：T）。（PJ，QJ）−→P|PJ{v/}我们用一个类型环境Γ来标记每个被定位的进程，它是一组位置类型。与特定进程关联的类型环境的目的是限制进程可以访问的可访问资源的范围。 形式上，L×K是将位置名称与位置类型相关联的关系。位置类型是一组定位能力，其可以包含信道类型，移动能力（即，迁移到该位置的许可），或频道创建能力（即，创建频道）。通道类型可以包含通道能力读（r）、写（w）和只读（ro）。一个具有信道类型res{rT，wTJ，roTJ}的进程可以接收类型T的消息和发送类型T j的消息。ro能力的行为与r相同，不同之处在于接收到的消息的类型不添加到进程的类型环境当一个名字通过一个递归通道被接收时，一个类型我们描述的进程只有在其类型环境具有相应的信道类型时才可以使用接收到的信道在Dπ中，资源被积累，但它们永远不会丢失（丢弃）。我们用Δt形式的定时器扩展了Dπ的通道类型。现在仅在由定时器值t给定的时间间隔内允许信道上的通信（即，直到信道类型的定时器期满）。这些计时器定义了类型环境中通道类型的存在计时器随着通用时钟的每一个“滴答”而减少（我们假设我们有一个通用时钟）。 到期后，G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）37信道类型被丢弃。计时器使用通道类型创建一次，并在将类型添加到类型环境时激活表2：类型系统和子类型关系类型：K：：=loc{κε}A：：=res{α}Δt分型：κ：κa：A：a：B如果A<：BE：：= A| K|BK：L如果λ∈L：κ∈K：κ<：λT：：= E|（T1，..，Tn）A：B如果<$β∈B：<$α∈A：α<：β|A1，..， A n@K功能：κ：：= a：A|去|新的cα：：= rT|关于我们|罗TA@K<：B@L，如果K：L和A<：BrT：rTjifT<：TJwS：wSjifSJ ：SroT：roTJifT<：TJB表示一组基本类型（Boolean，Boolean等）。子类型关系<：类似于Dπ的子类型关系，除了新的类型Rπ。注意子类型关系的直观行为是集合包含的逆（类型的A<：B意味着集合的A<$B通常，进程移动到某个位置（通过执行go操作），并等待一段时间以建立通信一个特定的频道。固定资源的功能r/w/ro告诉进程当它到达一个位置时允许它做什么当进程接收到新的通道名时，新通道的类型就变得可用。这意味着进程可以根据新的类型在新的通道上进行通信。例如，如果进程通过输入接收信道A的位置名为a@k，则它获得移动到位置k的能力，并在信道A上通信。一个具有能力为r T的通道类型的进程只能接收（不产生错误）T类型的消息;错误系统如表3所示。当信道类型res{r<$T <$}扩展为r<$TJ<$时，自然地，进程现在能够接收更丰富类型的消息：T和TJ。与通道名称的情况相反，通道类型之间的相等性并不取决于它们关联的计时器。必须仅使用名称和功能来测试相等性，并且它保留旧的计时器。我们定义了一个函数，它只影响能力的集合。它减少通道类型的计时器，并删除计时器过期的类型。通过删除通道类型，可以获得仅具有go功能的位置类型（我们称之为空位置）。一个进程可以移动到一个空的位置，但在那里它没有能力执行任何操作，因此产生一个运行时错误。因此，删除也删除了空的位置。定义2.1（函数）P Δ：PΔ→PΔ定义在标记定位过程的集合PΔ上，使得n（ l[[ P]]r）= l[[ P]]rJ其中l可以是分布式系统中的任何位置，并且从其中，每个类型c：resΔt，t>1，t∞都变为c：resΔ（t−1），并且每个c：resΔ1消失。表单loc：{go}的位置类型已删除。8G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3>>>2.2语义时间的流逝通过时间步进函数φΔ来形式化，该函数定义在标记定位过程的集合PΔ上可能的通信在通用时钟的每一个滴答执行。活动信道是那些可能参与这些通信的信道。φΔ表示在通用时钟的滴答声中不进行通信的活动通道（参与通信的通道与其计时器一起消失）。由于定时器，功能可能会丢失，从而导致“错误”。我们定义φΔ来检查所需类型的存在性，并相应地改变过程。当φΔ减少通道计时器时，我们也通过应用清理函数φ来扩展它以照顾类型环境。在φΔ的定义中，为了简洁起见，我们省略了输入和输出过程中的信道类型和传输消息对于go k语法，如果位置类型包含go，则R被执行;如果k不在r中定义，则Q被执行。如果go不是当前，进程被认为做了违反其权限的事情，并生成错误。进程的良型性由一组静态规则定义（静态类型规则的详细介绍在[10]中给出这些规则表达了进程在其类型方面的行为如果一个进程想要在一个它没有能力的通道上进行通信，如果替代进程Q是良好类型的，那么它仍然可以是良好类型的。Q称为安全过程。定义2.2（标记的时间步进函数）我们定义φΔ：PΔ→PΔ，其中ΓJ是通过应用清除函数φ得到的。请注意，我们使用了一个简洁的符号aΔt。（R，Q）代表Δt！你好（R，Q）和Δt？（X：T）。（R，Q）。8>k[[R]]r '，如果P=gok。（R，Q）andr（k）：loc{go}>l[[Q]]r'，如果P=gok。（R，Q）anddk/∈dom（Γ）>Δ（t−1）Δt>l[[a>. （R，Q）]]Γ，如果P=a. （R，Q），t>1且t/=∞l[[Q]]r'，如果P=a>. （R，Q），t>1且Γ_（1，a）>φΔ（l[[R]]r）|φΔ（l[[Q]]Γ），如果P=R|Q>（νa@l：A）φΔ：（l[[R]]Γ{a@l：A}）如果P=（νa：A）Rl[[P]]r'otherwise我们写ΓP并说进程P相对于类型环境Γ是良好类型的;我们也写ΓkP并说P是良好类型的，可以在位置k运行。P=aΔt！你好（R，Q）在位置k处是良类型的，关于类型环境Γ，以下语句应该成立：（i）Γkv：T，这意味着v是类型T的位置k处的良型值;（ii）Γka：res{wT}Δt，这意味着通道a存在于位置k处，并且可以在另一个t个时间单位内传递类型T的值;（iii）ΓkR;ΓkQ，这意味着R和Q在位置k处是良类型的。由于函数f通过移除通道和位置类型来改变能力集r，我们感兴趣的是过程在新的rJ下是否仍然是良好类型的。的下面的引理将进程的键入环境与时间的流逝完整的证明见[10]。G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）39−→ΔΓΔΓ引理2.3（良型性由清除函数保持如果Γ D l [[P]] Δ，则Γ D <$（l [[P]] Δ）。我们考虑N和M范围内的标记定位过程（例如，N表示I[[P]]r）。我们用f →表示规则（RΓ-COM 1）和（RΓ-COM 2）不能被应用的事实。使用这些符号，我们给出以下约简规则，为tDπ提供动态语义。l[[P]]r/→（RΓ-IDLE）l[[P]]→φΔ （1[[P]]r）Γ（l，a）：res{r<$T <$}（Rr-COM1）l[[aΔt！你好（P，Q）]]|l[[aΔt'？（X：T）。（PJ，QJ）]]→（l[[P]]Δ）|n（l[[PJ{v/X}]]ΓH{v@l：T}）Γ（l，a）：res{roT}（Rr-COM2）l[[aΔt！你好（P，Q）]]|l[[aΔt'？（X：T）。（PJ，QJ）]]→（l[[P]]Δ）|n（l[[PJ{v/X}]]Γ）N→NJM→MJN→NJ（RΓ-PAR）N|M→N J|M J（Rr-RES）（νa@l：T）N→（νa@l：T）N JN< $NJN→ M M<$ MJ（RΓ-CONG）NJ→ MJ我们有两个通信规则，它们取决于信道的类型在（Rr-C 0 M2）中，我们考虑随机信道，并且该过程可以使用接收到的信息，而不将新类型添加到其类型环境r，如规则（RΓ-COM 1）。在这些情况下，类型环境由cleanup函数清除。在（RΓ-IDLE）中，函数φΔ减少通道上的定时器，并且对于定时器过期时，函数丢弃通道。 因为移动语法是在函数φΔ的应用下进入的，所以我们没有（RΓ-GO）规则。 在通用时钟的每一个节拍（R'-IDLE）被应用于进行进程和不进入任何通信的进程。 在规则（RΓ-PAR）中，如果进程M没有内部通信约简，则它通过（R Γ -IDLE）规则约简为Mj.在下表中，我们给出了tDπ的误差系统，其中err表示产生一个错误。表3：重复错误定义了Γ（k），并且Γ（k）/：loc { go }（E-GO）错误l [gok。（P，Q）]]Γ−→Γ（l）/：loc{new c}（E-SUBC）错误l[[（νa：A）P]]Γ−→定义了Γ（l，a），并且Γ（l，v）/：wobj（Γ（l，a））（E-SND）l[[aΔterr！你好（P，Q）]]Γ−→（E-RCV）定义了Γ（l，a），并且robj（Γ（l，a））l[[aΔt：T或roobj（r（l，a））/：Terr？（X：T）。（P，Q）]]Γ−→（E-COM）（1）A、B、C、 D、Ewobj（r（l，a））/：robj（Δ（l，a））或wobj（r（l，a））/：roobj（Δ（l，a））l[aΔt！你好（P，Q）]]err| l[[aΔt'? （X：T）。（P，Q）]]errerrΔ−→errN−→（E-NEW）错误（νa@k：T）N−→N−→（E-PAR）错误N|M −→门N−→（E-STR）错误M−→Γ10G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3robj（）、roobj（）、wobj（）是在信道类型集合上定义的部分函数，并返回发送的类型。例如，在类型环境中，G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）311→在位置l处，信道类型a：res{rTj，wTJ}，wobj（r（l，a））的应用返回TJ。 仅当通道或位置类型为在类型环境中（当一个进程试图对它的类型环境中积累的类型做一些事情时）。当一个类型不在进程的类型环境中时，通过φΔ函数选择安全进程2.3一些技术成果我们遵循[13]中介绍的方法。 这是一种句法方法，与阿巴迪、卡德利或米尔纳等作者开发的基于指称或结构操作语义的其他方法相反。我们可以在[10]中找到证据。引理2.4如果ΓDl[[P]]Δ，则ΓDφΔ（l[[P]]Δ）。证明：这个引理声称时间的流逝不会干扰打字系统。φΔ不改变过程在某个Γ下是良型的性质。为了证明这一点，我们从φ Δ的定义出发考虑P的形式。我们在推理树的深度上使用归纳法。Q定理2.5（主语归约）对于所有标记的已定位进程(a) 如果N <$N J，则ΓD N当且仅当ΓD N J。(b) 如果N → N J，则ΓD N当且仅当ΓD N J。校样：对于定理的第一部分，证明通过考虑所有 等价方程（等价方程[10]是米尔纳为π演算给出的方程的精神）。定理的（b）部分断言了静态语义（类型规则）和动态语义（归约规则）之间的一致性。我们对由N→NJ给出的推理树的深度进行归纳.我们还使用了引理2.3和引理2.4，引理2.3与时间和类型环境有关，引理2.4与时间和通道名称有关Q主题减少向我们保证，一旦类型良好，流程就保持类型良好。请注意，与函数式编程中的一般方法相反，在tD中，π良型性也必须通过结构等价关系来保持。下面我们给出一个类型安全的结果，这是得到一个完整的证明所需要的。tDπ的可靠性。 这个结果表明，如果系统是良好类型的，err则它不会引起运行时错误，这用P/−→表示。定理2.6对于所有的标记定位过程N和所有的类型环境Γ，err我们有N −→。证明：证明考虑了定理的逆命题，该定理指出，如果Ngivesristoaruntimeerror（N−er r），则在任何类型的环境Γ（Γ/DN，nΓ）下，N c都不为线性类型。我们用归纳法来分析N的结构，12G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3μ@kμ@kμ@kμ@kμ@kμ@k考虑表3 .第三章。Q时间倒钩互模拟：当操作语义由归约关系定义时（即，转换上没有标签），倒钩互模拟有助于比较两个系统的进化两个系统是等价的，如果一个观察者不能区分它们行为的差异在[19]中提出为了简化呈现，我们选择仅沿着所定位的信道名称的通信作为可观察在tDπ中，我们在固定位置的信道上进行同步通信因此，可观测量可以是输入和输出通信。我们认为，go的运动、时间步进函数φΔ的应用以及过程的内部相互作用直觉上，进程P的观察者是一个与P并行运行的进程O。tDπ中主要有四个观测坐标：一个涉及通信信道的名称（Milner和Sangiorgi抽象的可观测量（或倒钩）是过程上的一元谓词倒钩有时被称为承诺谓词，定义了进程在特定通道上立即通信的可能性一个自然的问题出现了：观察者应该有多大的权力？我们认为，一个不定时的观察者不能区分定时器的值另一方面，定时观察器监视类型环境内的通道类型的定时器，或/和通道名称的定时器。我们定义了一类倒钩，它观察通道名称和通道类型上的计时器。 此外，他们还观察通信频道 倒钩被限制在一个类型环境Δ;表示观察者对类型的区分能力倒钩↓t，tJΔ识别具有以下特征的过程：对于类型环境Δ，通道μ具有足够的权限。定义2.7定时全局类型倒钩谓词，↓t，tJΔ，其中μ∈ {a？，a！}，其中a是任何通道名称，由以下规则系统归纳定义。我们用μ表示输入或输出通道的名称。如果μ=a？则μ=a。Γ（k，a）：Δ（k，a）r（k，a）=res{.. . }ΔtJΓ（k，a）：Δ（k，a）r（k，a）=res{.. . }ΔtJk[[aΔt！你好（P，R）]]t，tJΔa！@ Kk[[aΔt？（X：T）。（P，R）]]t，tJΔa？@Kt，tJΔμ@kt，tJΔμ@ka/=μk[[P]]↓t，tJΔN|M ↓t，tJΔ（νa@l：A）N↓t，tJΔk[[P]]↓t，tJΔ定义2.8时间全局类型倒钩互模拟S是过程上的对称二元关系，对于每个（P，Q）∈S，↓↓N↓N↓G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）313.(1) 如果P↓t，tJΔ，则对于任何倒钩↓t，tJΔ，Q↓t，tJΔ;μ@ kμ@kμ@k(2) 若P→PJ则Q→QJ且（PJ，QJ）∈S..两个进程是赋时全局类型倒钩双相似的，记为PtGTBQ，如果和仅当对于某个时间全局类型倒钩互模拟S，（P，Q）∈ S。倒钩互模拟本身并不具有令人满意的性质。为了得到一个倒钩等价（倒钩同余），互模拟在所有静态（分别为正常）上下文中是封闭的[23]。同样，我们可以关闭在所有观察者下的互模拟关于类型环境Δ是良好类型的。因此N和M是定时全局类型倒钩等价的（N tGTBM）当且仅当如果对于所有Δ D O，我们有N |BM |O.3配合部由于tDπ使用分布式资源和代码迁移，我们很容易找到与Reo基于通道的协调的分布式资源是连接在单个位置的固定位置的信道。为了能够在特定通道上传递消息，进程必须迁移到通道的位置。在每一时刻，在通道的每一端只能有一个进程。通信是匿名的，因为每个进程都不关心它向谁发送或从谁那里接收消息。它只关心在另一个互补进程试图在所定位的通道的另一端进行通信时立即发送所需的消息等待实现沟通的时间并不像其他方法那样是无限的。tDπo允许定义一个截止时间计时器（或时间窗口），它定义了一个进程可以在通道上等待多长时间。一个经典的协调模型应该清楚地定义要协调的集、用于协调实体的媒体（协调架构）以及协调协议的规则。相同的间隔定义为tDπ。• 协调实体是分布式的移动通信过程;• 协调媒体由定时器分配功能TA（参见下面的定义）以及所定位的通信信道和类型组成;• 协调定律由tDπ的静态和动态语义给出（即，简化和类型化规则，以及时间步进和清除功能），以及一组协调规则CP。tDπ旨在模拟分布式架构（它具有移动性和位置等特性）。但是，tDπ也可以通过将系统限制在一个位置来建模单个平台架构。协调模型的其他要求涉及协调部分与计算部分的分离。在我们的模型中，tDπ代表计算部分。协调部分由协调对给出。第一个组件（TA）是为定时器分配值的函数，第二个组件（CP）是由一组规则（通常已知）给出的协调协议。14G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3tGTBtGTB在tDπ过程表达式的所有可能的约简（迹）中，我们可以通过对定时器施加某些值来选择子集我们定义了一个函数，它将从的值分配给定时器Δt。定义3.1（计时器的计数值）我们用Δ T表示通道上的定时器集合以及类型上的定时器。将自然值分配给Δ T中的计时器是通过函数TA：ΔT→ Δ T {∞}完成的。我们用Δ T表示|P是进程P的定时器集合;考虑到进程P，T A自然被限制为T A|P.在任意过程中，P = a Δ t!你好（R，Q），定时器可以取两个特殊值：∞和1。如果该值为∞，则进程可以永远在通道a上等待。如果值为1，我们在a上没有通信，过程简化为第二个备选过程Q（在这种情况下，我们称P为瞬态过程）。协调协议CP是由一组规则给出的，当我们在约简步骤中有多个通信选择时，这些规则提供了一个例子是在可以沿着名为a的公共通道发送或接收消息的进程中进行选择。协调规则可以定义为选择具有最低信道定时器值的发送方或接收方;这样的规则也可以扩展到类型定时器。定义3.2（协调员）配位部分用tDπ表示为一对C=（TA，CP），称为配位子.我们扩展了定义2.8中的时间互模拟，以纳入协调部分。 两个进程P和Q关于协调器C是双相似的，用PCQ表示，如果PtGTBQ以及P和Q的定时器都被控制，由同一个协调员C.等价关系可以在定时器分配函数上定义如下。首先我们需要一个映射（·，·）：PΔ× TA→ PΔ，它根据一个定时器分配函数改变一个标记定位进程的定时器。给定一个协议CP，我们说两个函数T A1和T A2是等价的，如果它们不改变任何两个系统的相关行为;即， Mrs. ∈PΔ，（N，TA1）<$tGTB（M，T A1）惠（N，T A2）惠B（M，T A2）.两个等价函数的例子T A1和T A2由简单的常数平移给出;即， TA2（Δt）=TA1（Δt）+c，其中c是常数。这种关于定时器分配函数的等价关系可以扩展到协调器：如果两个协调器C1，C2具有相同的规则集CP，并且对应的定时器分配函数是等价的，则它们等价的，记为C1<$C2。关于协调器的时间双相似关系CtGTB实验结果：）和等价关系在协调器上的关系如下：定理3.3对于每个带标记的定位过程N，M和协调器C1，C2，C1tGTB M和C1<$C2，然后N <$C2M。新定义的互模拟强调了定时器分配函数的作用（如果N是G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）315F协调一致。当算法方面在控制计算的策略中占主导地位时，规则集CP在协调语言中变得更加重要CP描述的方面在根据协调模型实现协调语言时是可见的3.1举例说明协调和建模能力在本节中，我们给出了一些简单的例子，tDπ过程将它们与Reo模型的连接器联系起来[2]。Reo是一种基于通道的外源协调模型，它基于由简单通道组成的复杂连接器连接器基于实体之间通过这些连接器机制进行的匿名通信来施加特定的协调模式信道由两端（源a和宿b）组成，并表示为ab。在每一端，在任何时候最多可以连接一个实体。渠道和实体被视为移动的。在源端可以写入消息，在接收端可以读取消息。通道上有一组操作，如创建、将一端移动到另一个位置或根据读取模式读取。take操作也会从通道中删除消息，这与read操作相反。一a b a b，c dCBa a b，e，cd cDa b c d e图1. Reo中的连接器示例图1.a中的简单通道可以用tDπ表示为Pa@k，b@k=k[[a∞？（X：T）。（b∞！你好。（停止，Q1），Q2）]]其中两个端部位于相同的位置k。上述tDπ过程的行为是异步类型的Reo通道。该过程在输入通道a上接收一个值，并在随后的过程中替换变量X;之后在输出通道b上发送接收到的值。注意，tDπ中的通道的概念不同于Reo中的概念。用tDπ过程模拟了源a和汇b分别位于不同位置k和l的Reo信道P a@k，b@l=k[[a∞？（X：T）。（去湖。（b∞！[X]，Q1），Q2）]]。该过程使用通过从一个位置移动到另一个位置而不同定位的两个通道a和b。请注意，如果我们为计时器使用离散值，那么我们将简单的Reo通道转换为定时通道。消息只能在有限的时间段内通过信道传输。图中的连接器1.b称为Flow-through，它允许数据从通道ab的源a传递到通道cd的宿d。将其平行放置就足够了BD16G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3两个进程Pa，b和Pc，d，它们代表两个Reo通道ab和cd。条件是信宿b和信源c相同;在tDπ中，这意味着信道名称b和c表示相同的信道。相应的过程是：PF=k[[a∞？（X：T）。（b∞！你好。（停止，Q1），Q2）|b∞？（XJ：T）。（d∞！你好。（停止，Q1），Q2）]]Reo的模式可以用通道类型在tDπ中建模。在tDπ通道上，不能接收比进程的类型环境中指定的类型更小的值。对于图中的连接器1.c称为合并，一个简单的tDπ过程可以以同样的方式给出，只是我们需要tDπ的扩展版本，其中求和算子用于非确定性选择（如Reo行为所要求的我们现在给出图1.d的复制器连接器的定时版本;它的行为是复制尽可能多的消息。考虑tDπ过程defRΔ20 Δ6不 =a？（X：T）。（（b！X|C！X通过结构同余，我们有|T.T. 当接收到消息时从v1到a，过程简化为bΔ20！100万美元|cΔ6！100万美元|T.T.如果在4个时间单位之后接收到另一个消息v2，则它被复制，并且系统减少到bΔ16！100万美元|cΔ2！100万美元|bΔ20！2012年2月|cΔ6！2012年2月|T.T.图1.e中的Take-cue复制器与图1.b的流通相关。这一次，信宿b和信源e和c是相同的（它们在tDπ中表示相同的信道名称）。在接收到来自源a的消息后，进程必须首先通过源e将消息发送到信道ef的接收器f，然后才允许沿着信道cd发送消息。k[[a∞？（X：T）。（b∞！你好。（b∞！你好。（停止，Q1），Q2）|b∞？（Y：T）。（f∞！你好。（停止，Q1），Q2）|b∞？（Z：T）。（d∞！你好（停止，Q1），Q2），Q2）]]4相关工作我们简要回顾了与我们的方法相关的三个协调模型。首先，我们考虑MoCha-π[14]，这是一种受π演算[18]启发并基于移动信道的协调演算。MoCha-π是MoCha中间件在分布式系统中的协调模型。通过π演算中描述的过程对通道进行建模，可以不断创建新类型的通道。这些通道与Reo中的通道类似，并且具有两个可能的不同位置的通信端。一个进程可以连接或断开连接，读取或写入数据到一个通道端。MoCha-π提供了匿名通信，并提供了在通道末端替换进程甚至进程之间这与我们的模型不同，首先是因为MoCha-Δ5G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）317π没有明确的位置概念，这在分布式系统中非常重要也没有明确的时间概念，因此对通信没有时间限制。此外，tDπo允许通过类型系统来定义资源访问限制MoCha-π虽然是π-演算的推广，但还没有重要的技术结果，也没有等价关系的概念文[8]用过程代数的方法对Linda协调语言进行了形式化.八种语言扩展琳达几个原语进行了比较。对于每一种语言，观察语义是由带刺的bisimulation。元组空间中的元组是唯一的可观察量。本文表明，进程代数是非常适合模型的协调语言的数据空间的基础上。然而，这些模型并不像tDπ（无数据访问限制方案）那样使用类型系统。没有时间概念，因此没有明确的时间限制。Linda语言的一些时间扩展在[16]中给出。μKlaim [12]最近被作为协调语言Klaim的模型给出。Klaim语言被设计用于对由通过多元组空间通信的移动组件组成的分布式系统进行编程。μKlaim的语法包含位置和定位组件的概念，类似于tDπ。故障是μKlaim实现的分布式网络的一个重要特性。通过给出一个等价性检验来研究观察语义.一个明显的区别，我们的方法是由定时器，这是不存在于μKlaim。与μKlaim相比，tDπ的类型系统和通道类型上的定时器使其成为一个适合于建模具有各种时间和资源访问约束的更广泛的分布式系统的模型。受μKlaim的启发，将来应考虑将tDπ扩展到故障引用[1] Arbab ， F. ， Iwim 并 行 活 动 协 调 模 型 ， 在 ： P.Ciancarini 和 C。 Hankin ， editors ， 1st InternationalConference on Coordination Languages and Models（COordination34比56[2] Arbab，F.，Reo：a channel-based coordination model for component composition，MathematicalStructures in Computer Science14：3（2004），pp. 329-366[3] Arbab，F.，M. M. Bonsangue和F. S. De Boer，A Coordination Language for Mobile Components，1（2000），pp. 166-173。[4] Arbab，F.，I. Herman and P. Spilling，An overview of manifold and its implementation，Concurrency：Practice and Experience5：1（1993），pp. 23比70[5] Baeten ， J. 和 j.A. Bergstra ， 离 散 时 间 过 程 代 数 ： 绝 对 时 间 、 相 对 时 间 和 参 数 时 间 ， FundamentaInformaticae29：1（1997），pp.51比76[6] 伯杰，M.， 两个定时异步pi演算约化同余的基本理论。，in：P.Gardner和N. Yoshida，editors，15thInternational Conference On Concurrency Theory（CONCUR115-130[7] Busi，N.， P. Ciancarini，R. 戈列里 和 G. 萨瓦塔罗， 协调模式：导游，在：A. Omicini，F. Zambonelli，M. Klusch和R. Tolksdorf，editors，Coordination of Internet Agents：Models，Technologies，and Applications，Springer，2001. 6比24[8] Busi，N.，R. Gorrieri和G. Zavattaro，A process algebraic view of linda coordination primitive. ，Theoretical Computer Science192：2（1998），pp. 167-199.18G. 乔巴努角Prisacariu/理论计算机科学电子笔记175（2007）3[9] Carriero，N.和D.葛兰特，琳达在上下文中。，Communications of ACM32：4（1989），pp. 444-458[10] 乔巴努湾和C. Prisacariu，Timers for Distributed Systems，in：A. Di Pier