共享消息通信：结合消息传递和共享内存优点的通信模型

理论计算机科学电子笔记192（2007）77-92www.elsevier.com/locate/entcs共享消息通信阿斯特丽德·基恩印度理工学院计算机科学与工程系印度新德里摘要共享消息通信（SMC）在[9]中被引入作为一种通信模型，它通过允许任务通过特殊的共享内存区域进行数据通信来降低通信成本（在通信延迟和内存使用方面）。将引用发送到否则该模型将不可访问的内存区域而不是数据本身，结合了消息传递和共享内存的优点。实验结果表明，SMC在大数据负载的情况下，明显优于经典的消息传递。在本文中，我们给出了一个正式的操作语义SMC展示明确的效果执行SMC命令的本地和共享存储器。基于这种语义，我们证明了任何使用消息传递的程序都可以被证明与基于SMC的程序弱双相似，并且就通信成本而言，后者的摊销成本更低，[7]。关键词：共享消息通信，操作语义，成本评估，消息传递。1介绍为了实现高性能，现代计算机应用程序在（多）处理器网络上执行。像数字信号处理这样的高数据速率处理在微架构上最有效地实现，该微架构采用共享存储器作为进程间通信的手段然而，共享内存编程必须明确地处理正确的数据访问和数据完整性，忽视这些会导致错误的计算。基于消息传递的体系结构通过禁止共享地址空间以及明确分离计算和通信来防止此类错误。但消息传递存在数据延迟大、数据传输冗余等缺点。共享消息通信（SMC）旨在结合消息传递的优点，同时利用共享内存的可用性来降低通信成本。在SMC架构中，通信是通过对共享存储器的引用（称为令牌）来执行的，共享存储器由网络提供，并确保互斥访问。为了进行通信，一个进程需要一个1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.02178A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77token（通过获取未使用的内存），将其数据写入授权的内存区域，然后通过消息传递将token发送到目标节点（发送token）。在接收端，进程接收令牌（receivetoken），在分配的内存区域上读取或写入，然后将令牌发送到另一个节点或释放它（使用结束）。一般来说，当传输的数据量非常高时，与授予、释放、发送或接收令牌的费用相比，共享消息通信的整体性能可能比直接数据通信好得多。通信1的SMC模型已在[9]中介绍它通过图1中的前置条件和后置条件描述了SMC通信原语的语义，并报告了实验结果，这些结果表明，如果要传输大数据项，SMC的性能优于消息传递SMC支持系统级设计，其中一类实现的某些功能已抽象到可进行形式验证的级别[6]）。使用SMC，超越了纯粹的定性行为描述。当前使用SMC作为通信模型的程序不仅指定了关于功能的（定性）计算，而且还通过决定数据传输的底层模式应该依赖于共享内存来做出（定量）假设。本文的贡献是一个类的形式化操作语义构成顺序组件的集合被划分为区域并且区域内的通信通过SMC执行区域划分反映了预期有效实施的（定量）假设。SMC作为一种通信模型的使用保证了它在概念上可以被认为是消息传递（本文中正式证明了这一点）。语义是基于本地和共享内存之间的明确分离，并显示如何管理和处理令牌时，发送到或接收相同区域的其他进程基于这种语义，我们能够证明[9]中提出的要求，即新的SMC计算模型不会由于底层网络的共享内存区域分配而引入非确定性特别地，我们证明了任何基于消息传递的程序都可以重写为基于SMC的程序，使得这两个程序是观测等价的（[8]）。此外，我们表明，如果考虑到通信成本，则消息传递程序（摊销）比基于SMC的对应物更昂贵，从而支持[9]的实验结果。后一种比较是基于[7]中引入的摊销双相似性概念。其他基于双向模拟的行为前序，如[10]和[2]的效率前序，被证明不能充分表达这种关系。[1]文[9]中给出的广播变式在本文中不作讨论A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7779访问方法令牌句柄的先决条件令牌句柄上的后置条件援引操作得到未使用的记忆（令牌句柄）不应持有任何令牌持有代币拥有RW特权发送者块，如果未使用的内存不可用，否则将创建发送令牌（令牌句柄）应持有RW令牌特权不持有任何令牌发送者如果令牌缓冲器已满，则阻止，否则从令牌缓冲器的令牌句柄接收令牌（令牌句柄）不应持有任何令牌持有具有RW权限的令牌接收器如果令牌缓冲器为空，则阻止，否则任何最早的令牌令牌缓冲器被转移到令牌句柄使用超过（令牌句柄）应持有RW令牌特权不持有任何令牌接收器令牌被销毁，相关的内存区域被标记为未使用图1.一、[9]中给出的SMC命令的语义2共享消息通信（SMC）SMC程序由一组有限的顺序程序组成，这些程序被划分为所谓的区域。一个区域的进程--类似于我们称之为节点的网络--使用SMC通信原语相互通信。直观地说，一个区域包括那些节点，这些节点在最终映射到一个网络时应该被定位成使得它们可以通过共享存储器有效地通信。我们在这里假设，我们只处理一个普适区域，以保持符号开销尽可能小一般情况将在结论中讨论。为了描述单个节点的行为，我们使用命令式语言的核心命令，并将它们与SMC通信原语穿插在一起。因此，SMC程序（假设一个全局区域）是一组顺序程序p1，...，p n从以下语法导出：p i：== skip|l：= a|第一，第二|如果b那么p i否则p i|whilebdop i|胶I（t，k）|uoi（t，k）|stj（t，k）|rti（t，k）|cpsi（t，a）|csmi（t，l）I j每个节点在其私有内存空间上操作，而进程间通信基于SMC，它占用整个区域的共享内存。相应地，操作语义在两个层中给出。首先定义了单节点的语义，并在此基础上给出了区域的语义2.1节点的操作语义SMC程序语法第一行中的命令语义是完全标准的（参见例如：[11]），我们假设熟悉它的介绍由一组规则。在记法中，我们用a表示算术表达式，b表示布尔值80A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77我J表达式和l∈Loci。由于在我们的上下文中，对这些表达式的值的计算并不感兴趣，因此我们在这里采用了一个大步语义。我们假设一个关系~，它将算术表达式a评估为（非指定的）值v，并将布尔表达式b评估为真或假，对于给定的位置σ的分配：a，σ~v和b，σ~真或b，σ~假。一个节点的状态由一对pi，σi给出，其中pi是要执行的程序，σi是提供位置的实际值的映射。我们在这里给出了一个小步骤的语义，以清楚地展示本地和共享内存的变化与计算步骤。为了简化后面的行为分析，我们用执行步骤执行的赋值或求值来修饰转换。skip跳过，σi<$−→σia，σi~vl：=a，σiαJ JαJpi，σipi;qi，σI我我我如果b，则pb，σi~trueelseq， σb=−t→ruep， σb，σi~假b=假我我我i i <$ifbthenpielseqi，σi<$−→qi，σib，σi~true当b做p时 ， σb=−t→rueσp;当b做p时， σ b= − t → ru eσ pb，σi~假b=假我我我ii whilebthenpi，σi−→σi标记句柄形成第三个语法类别，范围为t。通过Thdlsi，我们表示节点πi的令牌句柄。SMC命令直观地具有以下含义，其中我们假设节点i的视图：gumi（t）给出未使用的存储器（要绑定到t）uoi（t）在（由t给出的存储器的）stj（t）上的使用发送令牌到节点jrti（t）从节点j接收令牌cpsi（t，a）组成标记：将a的值写入由t指定的内存中csmi（t，l）消耗令牌：将由t指定的存储器的内容写入位置l。A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7781我我JJJGUMiσi（t），σi树胶i（m）−→σi{t：=m}（σi（t）=σ i）UOiuoi（t），σiuoi（m）−→σi{t：=}（σi（t）=m）STjstj（t），σistj（m）−i→σi{t：=}（σi（t）=m）RTIi（t），σirti（m）−→σi{t：=m}（σi（t）=σ i）CPSia，σi~vcps（m，v）（σi（t）=m）我cpsi（t，a），σi<$−→ σiCSMicsmi（t，l），σicsmi（m，v，l）−→σi{l：=v}（σi（t）=m）图二. 节点规则形式上，节点是一对2πi= pi，σi，其中σi：（位置i<$Thdlsi）→（值<${<$}<$SM）σi（Loci）值{}和σi（Thdlsi）SM{}。符号“0”表示局部位置或SMC位置的由于我们没有指定表达式和位置，因此也可以假设并发分配，并且通过这种方式，我们可以假设非标量数据结构。这种建模无疑淡化了SMC的一个关键属性，即并非所有由源进程写入共享内存的数据都不一定会被目标进程（通过csm）访问。然而，由于我们建模的重点是代币的管理，我们在这里没有给出一个细化的模型。[9]中描述的模型假设了预定义大小的代币（我们假设是一个）。共享内存的状态由σ给出。它并不存在于某个特定的节点，而是存在于该区域的某个地方。只有当我们描述整个区域的语义时，它才会可见。描述节点语义所需的其余规则是SMC命令的规则，见图2。对规则的一些评论：规则CPSi：随着cpsi（t，a）的执行，共享存储器单元m绑定到t82A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）772如 果 一个程序已经被完全执行，语义简单地产生一个状态σ i。 我们将其与对σnil，σiσ i等同起来，以确保我们总是可以假设结果有两个分量。A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7783我我我我我我将被更新为σi（a），但由于m不是π的局部，因此该更新仅在其区域的上下文中可见。规则U Oi，STj：本地执行uoi（t）或stj（t）的结果相同。我我规则CSMi：该规则的附带条件表示令牌句柄已被分配了一个共享内存位置。2.2区域一个区域由一组节点{π1，.，π n}，其共享本地存储器SM。 对于从区域的节点i到节点j的每个（单向）信道，存在通道变量cj在C={cj| i, j ∈ {1,...，n}，i = j}。 为了简单起见，我们假设信道容量仅是一个令牌项，并且我们不考虑通向区域外的信道。信道也充当缓冲器（图1中提到的令牌缓冲器）;如果容量有界，则可以强制发送过程的数据速率遵守接收器的处理时间。这是阻塞网络的一个特征。假设容量为1，信道可以简单地描述为变量，这简化了整体所需的符号。形式上，区域R由R= π（π1π···πn），σπ给出，其中σ提供SM的当前状态和通道变量：σ：SMC→值{}{available}满足σ（SM）<${available}的<$SM <${empty}，σ（C）<$SM <${empty}. 所有的状态映射的集合σ是由ΣSM给出的。操作语义是这样的，如果存储单元m没有绑定到令牌句柄或包含在通道之一中，则存储单元m被给予σ可用的值。对于具有n个节点的给定区域，状态映射σ及其局部对应物σi对于所有节点i，j，i=j应该是一致的：(a)σ i（t）= m 意味 σ（m）/=可用(b)σ（cj）=m意味着σi（t）/=mσj（tJ）和σ（m）可用(c) σi（t）/=σ i/=σj（tJ） 意味 σi（t）/=σj（tJ）其中t和tJ是任何令牌句柄，m∈SM。一致性表达了SMC的关键属性：在程序执行的任何状态下，令牌最多只能绑定到一个令牌句柄，属性（c），如果它驻留在通道中，（b），它不会绑定到任何句柄，也不是可用的。显然，初始程序图3中给出了区域SMC命令的转换规则。关于规则的一些评论：令σJ表示更新的状态映射。 在R-GUM i中，令牌m被授予节点π i，节点π i将其状态从可用变为可用。在R-UO i中，令牌m被释放，因此σJ（m）=可用。在R-ST j中令牌被发送到节点πj，即发送到连接信道cj如果后者为空.当我们假设信道容量为1时，非空性与信道满性一致。对于R-CPSi，由于局部84A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77我我我J我IJ我我πgumi（m）JR −GUMi−→πi（σ（m）=）我（··· （·· ·），σ{m：= π} Π，σ{m：=π} π可用i−→iuoi（m） JR− UOiπiuoi（m）−→πiJ（···πi−→ <$（···<$πi <$·· ·），σ{m：=available}<$stj（m）−i→πJR −STj我stj（m）（σ（cj）=空）J（···−i→（·· · <$πJ <$· · ·），σ{c：=m}我我rtj（m）R− RTjπj−i→πJrtj（m）（σ（cj）=m）（···−i→<$（·· ·<$πJ <$· ··），σ{cj：=empty}<$J Iπcpsi（m，v）Ji−→πiR−CPSi（···cps（m，v）− →（···πi·· ·），σ{m：=v}πcsmi（m，v，l）JR− CSMii−→πicsmi（m，v，l）J（σ（m）=v）（···图三. 区域规则实现CPSi（t，a）的执行。最后，R-CSMi描述了对令牌m内容的访问;它不改变状态映射。让PROGSMC表示所有共享消息传递通信程序的集合（这些程序可能处于初始状态或已经执行了一段时间）。形式上，PROGSMC是包含在变迁下封闭的初始状态程序的最小集合程序的初始状态由σ（cj）=空，σi（l）=空，σ（m）=对所有cj，l，m都可用。命题2.1（操作语义的良好定义）(i) PROGSMC中的所有程序都是一致的。(ii) 图1中SMC命令的条件由操作语义满足。证据（i）通过归纳确定PROGSMC成员资格的过渡序列的长度。(ii)通过检查相应的转换规则可以很容易地验证。Q请注意，给定的信道条件可能看起来比图1中所需的条件更强，然而，这只是因为我们假设信道的容量为1。A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7785我J我我JπJ我3从消息传递到SMC对于具有高数据速率的应用，在其最终实现中采用共享消息传递通信是可行的。在本节中，我们正式证明任何使用消息传递作为通信机制的程序都可以重写为SMC程序，使得这两个程序是弱双相似的（直到一些通信动作的重命名），这表明，特别是MP程序的（非）确定性结构被翻译保留。我们首先给出了一个正式的消息传递模型的描述，然后将其与双相似性的SMC表示。3.1消息传递模型使用消息传递的程序的语法是SMC程序的语法的直接变体p i：= skip|l：= a|如果b那么p i否则p i|whilebdop i|第一，第二|smj（a）|rmi（l）I jMP命令的直观含义是SM_j（a）发送消息：将a的值发送到节点j，RMi（l）从位置l处的节点j读取/保存消息。如前所述，区域由一组节点{π1，. ，π n}和C ={c j|i，j ∈{1，.，n}，i = j}是节点之间的（单向）信道的集合。我们采用与SMC相同的简化，假设信道容量为1，没有信道通向区域外，只有一个通用区域。通道的当前状态通过映射σ：C→值<${空}<${空}给出。为了描述操作语义，SMC命令的规则分别被节点和区域的消息传递规则所SMja，σi~vJRMii我smj（a），σismi（v）−→σiJrmi（l），σirmj（v，l）−→ σi{l：=v}R− SMjsmj（v）πi−→iJ（σ（cj）=空）我 （···smj（v）−→i我（···<$πJ <$·· ·），σ{cj：=v}<$我我rmj（v，l）R− RMjπj −i→πJv=σ（cj），（一）irmj（v，l）j空（···−i→（·· ·：=空}J I86A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77我我我ββ根据SMC的定义，集合PROGMP表示包含初始状态MP-程序的最小集合，该初始状态MP-程序在转换下是封闭的。初始地，对于所有j，σi（cj）=空。3.2MP-和SMC-程序PROGMP到PROGSMC的转换非常简单。我们替换每个命令smj（a）bygumi（t）;cpsi（t，a）;stj（t）和我我rmj（l）byrtj（t）;csmj（t，l）;uoj（t）我我其中对于每个节点仅使用一个令牌句柄这种替换由映射T描述，我们稍后将其推广到MP-和SMC-区域的状态之间的关系。如上所述，MP-程序将通过弱双相似性与它们的SMC-对应物相关。到目前为止，我们只考虑了所谓的强转移，而不是弱转移，弱转移是指转移之前和之后有任意数量的内部动作。在我们的设定中，内部行为是那些仅涉及令牌句柄的管理。 让Act表示所有第1节中出现的转换标签，Act_adm={gum_i（t），st_j（t），rt_j（t），uo_j（t）} |i，j≤n，i =j}，我我ActSMC= Act adm {cpsi（m，a），csmi（v，l）|i ≤n，m，a，v，larbitrary}对于β∈Act{\displaystyle\Act}，弱跃迁由下式给出：p=pJ 如果p− →pJ哪里ppJ 如果p→npJ，如果α∈Act adm满足atp−α→pJ，则P → P J。对于消息传递模型，我们定义ActMP={sm，j（v），rm，j（v，l）|i，j≤n，ij，v，l任意}我我上述替换T被扩展到图4中的关系T。它将MP程序与基于SMC的计算等价程序相该关系不是一对一的，因为特定令牌句柄的存储单元是任意选择的。注意，通过T，所有使用中的m∈SM（即，σm（m）/=available）都表示为该字符串的一个整数。这是因为事实上，SMJRMJ是原子行为。 与“中途”相对应的国家稍后将在SMC侧添加这种操作的“执行限制于初始MP-程序，T是一个函数，我们用T（Rummp）来表示唯一的SMC-程序。本节的主要结果是，A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7787我SMCSMCMPMPSMCIJMPSMCSMC−→ΠMPMPMPMPMPMPMP哪里（π1，π2 ） . πn），σ<$T<$（T（π 1），π n），σ<$T<$（T（π 1），πn ） . . T（πn）），σπi=πpi，σi<$，T（πi）=<$T（pi），T（σi）<$，T（σi）（l）=σi（l），其中l∈Loci且T（σi）（t）=σ i，⎧如果σ（cj）=空，则为空σ（cj）=ii∈m，则有σ_i（m）=σ（c_j）o_（w）σ1，T（σ1）， .. . ， T（σn）是一个连续的函数an d |{m |σ（m）/=available}|为|{cj|σ（cj）空}|.我我图四、关系TPROGMP×PROGSMC初始程序T_（？）mp∈PROG_（？）MP与T（T_（？）mp）是弱双相似的.实际上，我们建立了一个更强的结果，即，T（T（T））和T（T（T））处于效率预序关系≤，[2]（适用于我们的设置）。直觉上，这意味着--SMC模型，而实验结果表明相反。然而，这并不矛盾，因为我们忽略了通过通道发送大数据项的相关成本。命题3.1（MP-程序与SMC-程序之间的效率关系）设MP∈PROGMP，SMC∈PROGSMC.则当α MP≤ α SMC时，α MP比α SMC更有效如果有关系，R<$PROGMP×PROGSMC使得对于所有的（PROMP，PROsmc）∈R(i)如果γJ，γ∈Act则为：γJ和（γJ，）∈R，mp−→mmpsmj（v）SMCsmc=最大值smccps（m，v）MP SMC(ii)如果不匹配，−i→J然后是，m：λsmc==i=J和（JJSMC）∈R，(iii) 如果不匹配，rmj（v，l）−i→拉吉然后，，m：λsmccsm（m，v，l）=中国和（JJSMC）∈R，(iv) 如果smc−→J则（n，n，J）∈R，(v)如果γJ，γ∈Act则<$J：<$γJ和（，）∈R.smc−→smccps（m，v）mpmp−→mmpsmj（v）MP SMC(vi) 如果不确定，IJSMCcsmi（m，v，l）然后，：cummp−i→Jrmj（v，l）和（JJSMC）∈R.(vii) 如果不确定，JSMC然后，Π，，−→Π，88A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77：cummp−i→拉吉和（JJSMC）∈R.且（α MP，α SMC）包含在R中。证据直接从[2]中给出的效率预序的定义中得出，其中我们将sm-actions与cps-actions匹配，并且分别将rm-actions与，A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7789我我我我MP我我我我MP我MPcsm-行动。实际上，我们在这里考虑的是[1]中定义的ρ-σQ通过下一节中概述的冗长的案例分析，可以建立MP-程序的前序结果及其作为SMC-程序的表示。因为，最终，我们的目标是证明SMC-程序比原始MP-程序更具成本效率，而效率前序表明相反的结果，我们不把它作为一个定理。然而，下面的直接推论表明了我们翻译的正确性定理3.2设φ = φ（p1φ. 其中，σn是一个消息传递程序，SM是一个大小至少为n的共享存储器。然后，它与它的SMC-翻译T（T）是弱双相似的，其中内部转换仅是那些与令牌句柄的管理有关的转换。(a)定理的证明我们定义一个满足命题3.1的七个条件的关系R。这就证明了mp≤smc。 由于主要原因，满足效率预序≤的每对过程都是弱双相似的，参见[2]。这证明了定理对于R，我们详细验证了情况（ii）。 根据对其他项目的相应分析， 在命题3.1中，它遵循λmp≤ λsmc我们定义R为包含T的最小集合，它在以下条件下是封闭的：若 （ Rmp ， Rsmc ） ∈R 且 Rmp= Rmp （ . [001 pdf 1st-31files][001 pdf 1st-31files][001 pdf 1st-31files] . ），σ，s mc= . T（smj（a））; T（pi）， T（σi）均为零. . . ），σ然后（mp，（.. . cpsi（t，a）;stj（t）;T（pi）， T（σi）{t：=m} . . ），σ<${m：=<$}<$）∈R，J，（.. . tj（t）;T（pi）， T（σi）{t：=m}均为零。 . . ），σ<${m：=σi（a）}<$）∈RwhereJ=（. . 你看我，我看你。 . . ），σanddσ（m）=availablee.若（Rmp，Rsmc）∈R且Rmp= Rmp（. rmj（l）; p j，σ j . ），σ，s mc= . ǁ⟨T(rmj(l)); T(pj), T(σj)⟩ǁ. . . ），σ然后（mp，（.. . ǁ⟨csmj(t,l);u oj(t);T(pj), T(σj){t:=m}⟩ǁ. . . ），σ<${cj：=empty}<$）∈R，J，（.. . ǁ⟨u oj(t);T(pj), T(σj){l:=σ(m)}⟩ǁ. . . ），σ<${cj：=empty}<$）∈R（（90A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77MP其中，=（.. . ǁ⟨pj，σj⟩ǁ. . . ），σ_nndσ_n（c_j）=m.A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7791I2我我我我我我引理3.3设pi，σi是MP-节点，使得pi，σismj（v）−i→σpJ，σJ<$。你好我我是过程q1，q2，q3和局部状态映射σ1， σ2和 σ3，使得伊伊T（pi），T（σi）树胶i（m）−→q1，σ1cps（m，v）− →q，σistj（m）−i→q3，σ3我我q3 = T（PJ），σ3 = T（σ i）= T（σJ），m是某个共享存储单元。我我我证据我们证明了p i= smj（a）的引理。一般情况很容易推导出来。当σi ∈j（a）时，σi∈ j（a）smj（v）−i→σiwehaveσi（a）=v.现在，对于三个过渡1. n（t）;cps（t，a）;stj（t），T（σ）n（m）n（t，a）;stj（t），σ1n我我我i−→ii i2.cps（t，a）; stj（t），σ1 最小j（t），σ2我我我J−→i istj（m）3 .第三章。σst（t），σ2−i→ σ3。我我我通过检查相应的转移规则，很容易证明σ1=T（σi）{t：=m}，σ2=σ1和σ3=σ2{t：=m}=T（σi）{t：=m}=T（σi）。Q我我我接下来，我们示出，该局部转变序列在区域的上下文中也是可能的，只要存在可用的空闲共享存储器单元引理3.4设mp=（. ǁ π iǁ.. . ），σ∈ PROGMP和（PROMP，PROsmc）∈ T. 如果（. ǁπ iǁ.. . ），σsmj（v）−i→（.. . 你好。 . . ），σj且m∈SM使得 σ（m）=available，则s mc= . T（πi）.......................................胶i（m）1 1 1− →（.ǁ ⟨qi, σi⟩，ǁ.. . ），σcpsi（m，v）2 2 2−→（. ǁ ⟨qi, σi⟩，ǁ.. . ），σstj（m）−i→（.. . σ3σ4σ5 σ 6 σ 7 σ8σ9 . . ），σ3我我其中qj和σ j由以下公式给出：a，σ3=σj{m：=v，cj：=我我我m}和T（σ1），.，T（σ n）和σ3是一致的。证据 第一个跃迁是可能的，通过选择m和规则R-GUM i。因此，σ1=σ{m：=}。当σ1（t）= m时，从最优解和最优解R-CPS i出发的经济性定理如下。 所以，σ2=σ1{m：=v}。 最后一次跃迁可以推断以规则R-STj作为其边条件，满足σ2，因为σ（cj）=空我我否则，局部的smj（v）-跃迁是不可能的92A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77我T. S0，σ3=σn{m：=v，cj：=m}。Q引理3.5设k ∈PROGSMC，使得每个节点使用至多一个令牌句柄。 如果n有n个节点，全局状态映射σ和n个节点，则n ≥ |{m ∈ SM|A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7793我MP我MPσ（m）/=可用}|.证据 通过对PROGSMC中建立成员关系的过渡序列长度的归纳。关键的规则是R-GUMi和R-UOi以及底层的节点转换。Q命题3.6设mp=（. ǁπ iǁ.. . ），σ∈PROGMP和（PROMP，PROsmp）∈T.让，|SM| ≥ n。如果你（. ǁπiǁ.. . ），σsmj（v）−i→（.. . 你好。 . . ），σj“我的天，JMP=. T（π） . . ），σ_n_cps_i（m，v）（.. . T（πJ）. . ），σj然后SMCi=“我的天，JesussmcJ和（J拉吉）∈T，其中σJ=σ{m：=v，cj：=m}。证据根据引理3.5和引理3.4。Q4成本分析前一节的讨论表明，仅基于匹配动作的比较然而，如果一个人分配成本的行动和匹配的行动，同时保持跟踪当前的成本平衡，量化的性能也可以观察。为此，在[7]中引入了摊销双相似性。简而言之，它将双相似性与定量成本评估相结合。其主要思想是考虑行动及其成本，并修改互模拟等价的方式，使行动与“功能等价”的行动相匹配。它们的成本差异增加了在相互模拟期间如果一个系统p被认为比另一个系统q花费少，那么包含（p，q）的摊销互模拟应该处处具有非负信用。我们感兴趣的应用程序中，一些额外的内部活动在这种情况下，由于内部活动对应于不可见的τ-作用，因此弱摊销双相似性是有趣的。因此，我们允许一个可见的动作被一个动作模拟，这个动作之前和之后是一系列代价高昂的动作，这些动作在功能上等价于τ。函数等价由关系ρ给出。一般来说，只有一小部分行为的ρ不降为恒等式，并且成本被认为不同于0。一UAV弱转移是一个序列p=p其中a是可见动作，u和v是作用在函数上等价于τ，即u = b1. b n，v = d1. d m和b i ρτ，d j ρτ对于所有i，j。简而言之，uρε和vρε。每个动作a都有一个非负成本ca∈N。对于单词u = u1.我们有c u= c u1+··+c un。定义4.1设Aτ，−→ A τ是一个标号转移系统，其转移标号在Aτ=A τ {τ}，ρ∈Aτ× Aτ中，且每个动作a∈ Aτ都带有成本ca（由Π，J94A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77UBV布乌阿我MPSMCMPSMCADMγMPMPJMP定义cτ= 0）。 环P上的二元关系族（Ri）i∈N是弱摊销的ρ-互模拟，如果对所有i∈N，（p，q）∈Ri：aJ Jubv jJ J(i) p−→ p蕴含<$q，b，u，v[aρb，ερ uv，q=<$q且（p，q）∈Ri+c<$−ca]，(ii) q−b→qJimpliesvpJand（pJ，qJ）∈Ri+c−c]，其中rea，b∈Aτandu，v∈Aτandaτ =aifa/=τand τ =ε. ppis（wekly）比q摊销得更便宜（成本效率更高），直到贷项i，p<$ρq，如果（p，q）∈Ri对于弱摊销ρ-互模拟（Ri）i∈N.在我们的应用程序中，与τ在功能上等价的代价动作是Actadm中的那些动作。它的成本为1。 cps和csm类型的操作分别映射到sm和rm，但是对于前者，我们将成本分配为0，因为它们是本地读写操作，而对于后者，我们将成本分配为2。这里应该注意的是，由于SMC的正式建模的简化，SMC的真正好处被稀释了。然而，读者应该很容易看到，如果大数据包通过信道发送，那么摊销互模拟中的信用我们还忽略了，在非常小的数据项的情况下，令牌管理的成本可能超过简单地通过消息传递发送数据的成本当然，总体加速也取决于计算与通信的比率。为了给出一些真实的数据，对于用SMC实现的JPEG编码器的应用，已经显示了整体加速比1.77在消息传递模型上，参见[9]。我们所考虑的迁移系统是由MP-和SMC-程序的操作语义所引起的迁移系统的不相交的联合我们定义了一个摊销互模拟，对于每个对（smc，mp）∈Ri满足(i)若α∈ACT，，则（，mp）∈Ri−1，−→smcADMSMCγ(ii)如果nJ，γ∈Act，则存在nJ：smc−→smc mpjJ Jmp− → mp且（smc，mp）∈Ri.(iii) 如果cpsi（m，v）则存在，j，v：SMC−→布吕姆普SMCsmj（v）−i→J和（JMPJ）∈Ri+2.(iv) 如果csmi（m，v，l）J JSMC−→smc则存在mp，j，v，l：rmj（v，l）布吕姆普−i→拉吉和（JJ）∈Ri+2.γ(v)如果，，γ∈Act则存在u∈Act<$，2011年：mp−→mmpuγΠADMJ JSMCsmj（v）smc=smc且（smc，mp）∈Ri−cu，(vi) 如果不匹配，−i→J则存在u，w∈ActJSMC，m：，，，A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）7795（m，v）wJ J Jsmc=−→=smc且（smc，mp）∈Ri+2 −cuw，Π96A. Kiehn/Electronic Notes in Theoretical Computer Science 192（2007）77MPADMnni(vii) 如果不匹配，rmj（v，l）−i→拉吉则存在u，w∈ActJSMC，m：ucsmi（m，v，l）wJ J Jsmc=−→=smc且（smc，mp）∈ Ri+2 −cuw。注意，（i）(i) – (iii) given in Proposition 这两个组在这里交换，因为我们考虑了反向排序。由于Actadm中的所有动作都通过ρ映射到τ，因此需要验证条件（i）利用上一节中定义的关系R，我们建立了族（Ri）i∈N：（λsmc， λmp）∈Ri当且仅当（λmp， λsmc）∈R且i≥D（λsmc）其中，D（）定义为D（卢恩 D（p）和SMC⎧smc）=i=1i如果pcpsi（m，v），则为0csmi（m，v）拉吉吉−→或piJ−→对于某个m，vD（pi）=2如果pi⎪⎪sti（m）−→ 或piuoi（m）- →对于某个j，m01否则D（pi）给出了执行初始令牌管理所需的最大信用需求。很容易证明条件（i）-（vii）确实成立。由于每个具有n个节点的初始程序在其SMC版本中具有最大需求n，因此以下命题是直接的。定理4.2如果Rummp是具有n个序列分量的初始MP-程序，SSMc是其SMC表示，即SSMc=T（SSMp），则SSMc的摊销成本较低而不是用信用N进行循环，|SM |≥ n：T（n）<$ρ<$其中ρ定义在Def之后。4.1.5结论我们已经给出了并发程序的操作语义，其顺序进程被划分为区域，以方便高效的实现。在最终实现中，假设形成区域的进程通过共享内存进行通信。我们已经限制了正式的模型，只有一个区域，但设置很容易推广。在这种情况下，整个系统被描述为由（π1. π1），σ1，（π m. <$πm），σm<$，C<$其中每个<$（πi我... ǁ1n11nm1i），σi是如第2节中所述的区域。 映射C提供当前状态对于每个区域间信道。区域间通道的语义在消息传递部分中定义，通道访问操作为sm和rm。SMC程序支持一种系统设计方法使用消息传递作为通信模型的程序（仅）可以被证明功能正确，而与效率无关。数据传输。一旦确定了这一点，就可以处理业绩问题。 我们在这篇论文中已经表明，一个人可以从消息传递转移到，π