多方会话中的部分和完整进程翻译与类型检查算法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记322（2016）135-151www.elsevier.com/locate/entcs多方会话中的部分和完整进程1Mario Coppo Mariangiola Dezani-CiancagliniInes Margaria Maddalena Zacchi2DipartimentodiInformaticaUniversita`diTorino，corsoSvizzera185，10149Torino，Italy摘要多方会话描述了分布式环境中多个代理之间的交互，基本上需要两个步骤：通信协议的指定和将这些协议实现为进程。多方会话类型解决了这种方法：全局和会话类型提供了通信协议，而进程描述了会话中涉及的对等体的行为。由于类型和进程之间的密切关系，一些信息（如接收者和接收者的名称）在类型和进程中都是复制的在多方对话中，具有基本相同角色的参与者通过遵循相同模式的过程来实现是很自然的，仅在通信行为的发起者和接收者方面有所不同。为了允许更轻和更少的严格的过程开发，我们提出了一个翻译工具，它允许人们以简化的语法编写过程，称为部分语法，其中省略了输入/输出操作的接收器/接收器的名称。通过添加缺失的信息，部分流程可以自动转换为完整的流程，并为其定义操作语义。特别是，部分语法允许使用相同的过程模板来实现类似的参与者。在本文中，我们提出了一个翻译和类型检查算法，从部分到完整的进程，如果成功，也确保目标进程是良好的类型。 该算法是从基于规则的自然语义描述的翻译合成，它被证明是健全的和完整的翻译规则。保留字：π演算，会话类型，多方会话。1介绍会话类型是用来描述通信过程和研究其行为的最成功的形式主义之一其基本思想首先出现在[11]和[6]中，是引入一种新的多态形式，它允许通过类型的结构化序列来输入通道名，抽象地表示跟踪1这项工作得到了ICT COST Action IC1201 Betty、MIUR PRIN Project CINA Prot的部分支持。2010年LHT 4KM和都灵大学/Compagnia San Paolo项目SALT。2电邮地址：@di.unito.ithttp://dx.doi.org/10.1016/j.entcs.2016.03.0101571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。136M. Coppo等人/理论计算机科学电子笔记322（2016）135渠道的使用。在对分布式系统建模时，其中进程通过消息传递进行交互，允许在遵循规范协议的私有通道范围像往常一样，我们把会话称为私有交互，把会话类型称为描述它们的协议在最简单的形式中，会话是在两个对等体之间建立的，例如客户端与服务器连接一般来说，一个会话可能涉及任何（通常是固定的）数量的对等体。在这些情况下，我们称之为多方会话和多方会话类型[7]，以描述它们的协议。多方会话类型理论由三部分组成：全局类型、进程和局部类型，也称为会话类型。全局类型根据对等体之间的交互、这些交互的顺序以及交换的消息的类型来描述通信协议。全局类型给出的描述是中立的，独立于对等体及其观点。过程通过一种形式化的语言来描述会话中参与的对等体的行为对于每个对等体，会话类型描述与全局类型相同的通信协议，但从对等体的角度来看。局部类型和全局类型通过从全局类型中提取局部类型的投影操作相关联，并且类型系统确保进程根据其本地类型使用其拥有的通信信道。在对等体之间交互的更有趣的特性中，会话委托是一个关键操作，它允许以类型安全的方式依赖其他方透明地完成特定任务。 协议给出了一个典型的场景 服务器/客户端分布式系统的远程过程调用。在这种情况下，服务器在接收到来自客户端的请求之后，将与客户端的剩余交互客户端和应用程序进程最初彼此不知道，但随后通过通信信道的动态移动性直接地、透明地与客户端通信。这种协议通常是同步的，因为通信中涉及的进程保持紧密耦合。关于进程的语法，为每个输入/输出操作指定发送者和接收者的需要使得代码编写变得繁琐;此外，在分布式应用程序中，许多进程通常执行完全相同的输入/输出操作模式，仅对参与者进行区分。例如，在远程过程调用协议中，提供服务的应用程序进程在许多有趣的情况下只在通信中涉及的进程名称上有所不同。在本文中，我们提出了一个翻译算法，允许一个简单的语法编码过程，称为部分语法，它不需要指定输入/输出操作的接收器/接收器的名称。部分代码编写起来更简单，可以由会话中的不同参与者共享，但它是不完整的，不能直接执行。通过利用全局类型给出的信息，可以从部分代码中自动获得以完整语法编写的进程的可执行代码（即，包括通信中涉及的进程的名称）。只有当目标进程根据多方会话的标准类型化规则正确类型化时，转换才成功，因此转换算法还包括类型检查。M. Coppo等人/理论计算机科学电子笔记322（2016）135137从部分过程到完整过程的转换是由一组规则在自然语义中形式化的。这些规则隐式地定义了一个递归转换和类型检查函数，其代码是用类似ML的语言给出的。自然语义规则和相应算法的可靠性和完备性都可以很容易地得到证明。在本文中，进程执行由同步操作语义定义。然而，转换不依赖于通信执行的方式，并且也可以应用于像[1]中定义的异步演算。多方会议的出现是由于在语言Scribble [12]的发展背景下对金融协议的应用。第一个关于多方会话类型的理论工作是[2]和[7]。论文[2]使用了分布式演算，其中每个通道将主端点连接到一个或多个从端点。[7]中的进程和类型都共享一个通道向量，每个通信都使用其中一个通道。本文中的进程语法与[1]中的类似;主要区别是[1]中的通信是异步的。文[4]利用部分语法灵活性来处理自适应协议参与者。在[9]中研究了同步多方会话演算的互模拟，其中演算语法与我们的完整语法不同，只是因为缺少多个接收者。我们参考[5，3，8]以了解相关工作的全面概述。纲要第二节通过例子介绍了全局类型和部分语法。整个演算和类型系统分别在第3节和第4节中给出。第5节以自然语义规则结束，将用部分语法编写的进程映射到用完整语法编写的进程。最后给出了一个翻译和类型检查算法。2激励实例我们提出的演算的语法的帮助下的例子，为了给一个基本的想法的功能和语言特征。涉及经理（M）、意大利工厂（IF）、美国工厂（AF）和两个运输公司（IC）和（AC）的总体场景如下进行。(i) 经理向工厂发送一份供应项目的标识。(ii) 工厂把他们能提供的产品数量通知经理。(iii) 如果总数量令人满意，经理会通知工厂和运输公司安排细节，并等待两家运输公司的发货日期。否则，管理器通知所有参与者退出协议。138M. Coppo等人/理论计算机科学电子笔记322（2016）135M=a [5]（y）.y！“identifier”是什么意思？（x1）.y？（x2）。如果好（x1，x2），那么y是好的。y？（d1）.y？（d2）。0否则你就退出。0F[j]=a[j]（y）。y？（同上）。y！第100号y&{ok：y！第100号0，退出：0}C[k]=a[k]（y）。y&{ok：y？（n）。y！请填写日期。0，退出：0}Fig. 1. 以工厂经理为例。多方会话编程包括两个步骤：通过全局类型指定预期的通信协议，并将这些协议作为过程实现。管理器工厂协议的规范由全局类型Ga给出。 参与者实际上是用数字编码的：在Ga中，我们有M=5，IF=1，AF=2，IC=3，AC=4。Ga=1. 5−→ {1，2}：string。2. 1−→ {5}：自然数。3. 2−→ {5}：nat。4. 5−→ {1，2，3，4}：{ok：1−→{3}：nat。5.2−→ {4}：无条件。6.3−→ {5}：确定日期。7.4−→ {5}：确定日期。端8.quit：end}在Ga中，行1表示M向IF和AF多播相同的串。第2行和第3行表示IF和AF都向M发送一个自然值。在第4-8行中，M向所有其他参与者发送ok或quit。在第一种情况下，IF和AF分别向IC和AC发送要交付的物品数量（第4-5行），运输公司直接向M发送交付日期（第6-7行）;在第二种情况下，没有进一步的通信。图1给出了部分语法中参与者的代码，与Ga相关我们只需要三个部分过程，因为两个工厂IF和AF由相同部分过程F[j]的两个实例实现，并且类似地，两个运输公司由部分过程C [k]的两个实例实现。会话名称a建立对应于Ga的会话。进程M启动一个包含五个参与者的会话，由a[5]（y）作为第五个参与者;第一个和第二个参与者是通过分别在F[j]中分别由1和2实例j得到的，第三个和第四个参与者是作为C[k]的两个实例（k= 3和k= 4）每个参与者使用绑定变量作为通信中将使用交换数据的接收者和接收者由全局类型指定。G a的第一行由输出和输入操作y实现！M和y的代码中的“标识符”是什么？（id）在F[j]的c o de中。 第2和第3行是由YY？（x1）。y？（x2）在M和y的坐标中！F[j]（j=1，2）的c_d中的n个n。G a的下一行是通过选择和分支来实现的：actionsyok。y？（d1）。y？（d2）。0和y= 0。在M的代码中，y&{ok：y！第100号0，退出：0}在F[j]和y&{ok：y}的代码中？（n）。y！请填写日期。0，退出C[k]的代码中的0 }。M. Coppo等人/理论计算机科学电子笔记322（2016）135139F[j]=a[j]（y）。y？（同上）。y！第100号y&{ok：b[j]（z）. z！第100号z！很好0，退出：0}C=b[3]（z）.z？（n）.z？（（t））.t！你是谁？（n）.z？（（t））.t！请填写日期。0图二. 带有委托的管理器工厂示例。我们现在丰富这个协议，引入授权。在初始会话a中，参与者只有经理和两个工厂，根据新的全局类型Ga，这两个工厂还将交货日期发送给经理。实际上，在收到OK后，两家工厂都接受了由一家独特的运输公司提供的新会话。在这个会话中，由全局类型Gb描述，每个工厂向运输公司发送的不仅是物品的数量，还有用于与经理沟通的通道。通过这种方式，每个工厂委托运输公司将交货日期发送给经理。这种授权对管理者来说是透明的新的全局类型Ga和Gb是：Ga=1. 3−→ {1，2}：string。2. 1−→ {3}：自然数。3.第三章。2−→ {3}：无条件。4. 3−→ {1，2}：{ok：1−→{3}：确定日期。5.2−→ {3}：确定日期。端6.quit：end}Gb=1. 1−→{3}：自然数。2. 1−→{3}：T。3. 2−→{3}：无条件。4. 2−→{3}：T。端T=！{3}，日期端其中会话类型T表示交换的信道必须用于发送向会话A中的参与者3（即，向管理者）发送日期。工厂和运输公司的新代码如图2所示。请注意，“不改”，“不改”。这个例子还展示了部分语法如何允许编写可以适应不同全局类型的进程在本例中，与前一个示例不同，如果管理员决定退出协议，会话b不会打开，因此运输公司不会参与会话。在最后一个例子中，我们将递归分支行为添加到具有委托的协议中。特别是，我们允许M与IF和AF工厂反复谈判供应的项目数量。场景基本上是一样的，唯一的变化是，如果工厂可以提供的产品数量太少，经理会与工厂进行谈判，以增加数量。经理开始要求工厂提供第一批产品。在每一步，每个工厂都有一个新的供应商。管理者可以接受上级的命令，要求一个新的提议或者放弃。当经理决定结束谈判时（接受最后一批工人或放弃谈判），他就把他的决定通知工厂;在第一种情况下，和以前一样，联系运输公司通信协议由以下全局类型描述，其中G不同于递归部分的先前示例中的一个，其表示管理器和工厂之间的（可能的）递归协商。140M. Coppo等人/理论计算机科学电子笔记322（2016）135M=a [3]（y）.y！（“identifier”） def X（t）= t？（x1）.t？（x2）。 如果good（x1，x2），则t是ok.t？（d1）.t？（d2）。0else ifnegotiable（x1，x2） thent = 0.X（t= 0.否则就别退出。0在X（y）F[j]=a[j]（y）。y？（同上）。 defX'（x，t'）=t'！（x∈.t'&{ok：b[j]（z）. z！（x）z！（（t'。0，more：X'（newnumber（x），t'，退出：0}在X'（数量，y）中，图3.第三章。带有委托和递归的管理器工厂示例Ga=1.3−→ {1，2}：string。2. μt。 1−→ {3}：自然 数。3.2−→ {3}：无条件。4.3−→ {1，2}：{ok：1 −→ {3}：确定日期。5.2−→ {3}：确定日期。端6.更多：t}6.quit：end}Gb=1. 1−→{3}：自然数。2. 1−→{3}：T。3. 2−→{3}：无条件。4. 2−→{3}：T。端T=！{3}，日期端图3所示的参与者代码与前一个代码类似，但过程M和F[j]中的递归定义不同。3多方会话正如引言中所解释的，我们考虑两种不同的语法，第一种称为部分语法，用于编写可伸缩的代码，可用于实现会话中涉及的不同参与者，另一种用于描述最终代码。我们称后者为完全语法，因为它为任何输入/输出操作指定了发送者和接收者。3.1部分语法P、Q所覆盖的部分过程。. . ，和表达式，由e，eJ，. ，由表1中的语法给出。为了简化形式处理，我们假设每个递归定义的过程有一个数据参数和一个通道参数。然而，对多个数据和信道参数的概括是直接的。形式为u [p]（y）.P的一个部分进程通过由u与其他进程定义的服务名启动一个新的会话，每个进程的形式为u[q]（y）。Pq，其中1 ≤q≤p− 1。（绑定）变量y表示将用于通信的信道。我们称之为p，q，...（范围大于自然数）会议的参与者会话通信，即在已建立的会话内部发生的通信，使用以下三对原语来执行：值的发送和接收，会话委托和接收，其中前者通过传递与会话相关联的信道;以及选择和分支，其中前者选择由后者所分支的分支之一。请注意，隐藏服务名指定了它们的全局类型。其余的语法是标准的[6]。M. Coppo等人/理论计算机科学电子笔记322（2016）135141a、b服务名称x值变量y，z，t通道变量p， q参与者编号X，Y过程变量D：：=X（x，y）=P声明l标签u：：= x |a鉴别器：：=a|真正价值|假e：：= 0|X|e和e'表达式|不是...表1进程和命名约定的部分语法P：：=c！电子邮件，e.P Value sending|c?（p，x）.P值接收|c! 会议代表团|c?（（p，y））.P会话接收|c⊕ ⟨Π, l⟩.PSelection|c& (p, {l i: P i}i∈I)Branching|(νs) PHiding session% s会话名称c：：= y |s [p]通道表2完整语法：其他语法形式如表1所示。M=a[5]（y）.y！{1，2}，“identifier”（1，x1）.y？（2，x2）。ifgood（x1，x2）theny={1，2， 3，4}，ok =.y？（3，d1）.y？（4，d2）。0elsey {1，2，3，4}，quit. 0IF=a[1]（y）。y？（5，同上）。y！{5}，编号y&（5，{ok：y！{3}，编号0，退出：0}）AF=a[2]（y）。y？（5，同上）。y！{5}，编号y&（5，{ok：y！{4}，编号0，退出：0}）IC=a[3]（y）.y（5，{ok：y？（1，n）.2005年12月15日0，退出：0}）AC=a[4]（y）.y（5，{ok：y？（2，n）.y！2005年12月15日0，退出：0}）图四、完整语法的manager-factories示例3.2完整语法为了定义操作语义，必须通过添加关于全局类型提供的消息的可执行接收者的信息，将部分进程置于可执行形式中（参见第5节）。 完整的语法定义见表2。它与表1的语法不同，因为输入/输出操作（包括委托/接收和分支/选择）分别指定了发送者和我们使用RNN来覆盖非空的参与者集合。因此，C！，e（p，x）表示从参与者p接收值。这同样适用于选择/分支和委托/接收，但在最后一种情况下只有一个接收者。像往常一样，我们称s[p]为具有角色的通道：它表示会话s中参与者p的输入/输出端口。图4以完整的语法给出了实现第一个示例的管理器-工厂协议的过程根据全局类型Ga，所有输入/输出操作也分别指定发送者和接收者P：：=u[p]（y）.P多播请求|u[p]（y）.P接受|y！（e）P价值发送|y？（x）.P值接收|y！（（z.P会议代表团|y？（（z））.P会话接收|yl.P选择|y{li：Pi}i∈I分支|如果e那么P否则Q条件|P|Q平行|0不作为|（νa：G）P隐藏|X（e，c）进程调用|defD inP递归142M. Coppo等人/理论计算机科学电子笔记322（2016）135a[1]（y）.P1|......这是什么？ |a[n − 1]（y）.Pn−1|a [n]（y）.Pn −→（νs）（P1 {s[1]/y}|......这是什么？ |Pn−1{s[n − 1]/y}|Pn{s[n]/y}）[链接]s[p]！（{q}，e.P|s[q]？（p，x）.Q−→s[p]！（，e.P|Q{/x}（e↓）if和q∈/s[p]！（{q}，e.P |s[q]？（p，x）.Q −→ P |Q{/x}（e↓）[Comm1]s[p]！（（q，s'[p'].P |s [q]？（（p，y））.Q −→ P |Q{s'[p']/y}[Deleg]s[p]（{q}，li0.P|s[q]&（p，{li：Pi}i∈I）−→s[p]<$（p，li0P<$. |Pi0（i0∈I）ifn和q∈/n[Label]s [p]（{q}，li0.P |s [q]&（p，{li：Pi}i∈I）−→ P |Pi0（i0 ∈ I）[Label1]if e then P else Q −→ P（e↓ true）if e then P else Q−→Q（e↓false）[If-T]，[If-F]defX（x，y）= P in（X（e，s[p]）|Q）−→ def X（x，y）= P in（P {x/x}{s[p]/y} |Q）（e ↓<$）[ProcCall] P−→P'（νr）P−→（νr）P 'P−→P'P|Q−→P'|Q[Scop]，[Par]P−→P'在P−中定义D→在P'中定义D[定义]P <$P'和P' −→ Q'和Q <$Q'QP−→Q[Str]表3减少规则。P|0 PP|QQ |P（P|Q）|RP|（Q |R） （νr）P|Q（νr）（P|Q）（νrr′）P <$（νr′r）P（νr）0 <$0defDin0 <$0defDin（νr）P<$（νr）defDinP（defDinP）|在（P）中的Q定义D|Q）def D in（def D′in P）定义D′in（def D in P）表4结构等同性。3.3操作语义通常，操作语义由归约规则（表3）和结构等价规则（表4）组成，这些规则允许重新排列术语以应用归约规则。在编写过程中，我们使用规则[Link]描述了在n个参与者之间发起新会话，这些参与者同步服务名称a。最后一个变量是a[n]（y）。Pn，通过服务名称上的overbar来区分，指定参与者的数量n。因此，它被称为会话的发起者显然，每届会议都必须有一个独特的启动器。连接后，参与者共享私有会话名称。然后，每个参与者p中的变量y将被替换为具有角色s[p]的相应通道通信规则[Comm]、[Comm1]、[Deleg]、[Label]和[Label1]将会话中两个进程之间的通信形式化我们用e↓<$表示表达式e的求值为值<$。我们需要从接收者集合中删除接收参与者，以避免多次交换相同的消息。如果只有一个接收方（规则[Comm1]、[Deleg]和[Label1]），则整个发送操作将被删除。规则[Link]是同步的和原子的，一次涉及所有参与者。消息发送者和接收者必须同步，但多播通信不是原子的，因为接收者在不同的缩减步骤中获得相同的消息。这些选择是有争议的，但它们在文献中很常见[5]。在下文中，我们使用−→的预期含义。M. Coppo等人/理论计算机科学电子笔记322（2016）135143⎧⎨∈.†J∈（p→p：（U.G'）<$q=！（，U。（G'tq）如果q=p，？（p，U）。（G'<$q）如果q你好，不然的话，⎧⎪⎨⊕(Π,{li:Gi†q}i∈I⟩如果q=p（p→n：{li：Gi}i∈I）<$q=&（p，{li：Gi<$q}i∈I）如果q∈<$Gi0<$q其中i0∈I如果qp，q/∈I，且对所有i，j ∈ I，Gi<$q= Gj<$q。（μt.G）q=μt。（G<$q）如果Gtqi= t，否则结束。t <$q = tend<$q= end。表5将全局类型投射到参与者上。4类型系统本节介绍确保通信可靠性的类型系统。4.1全局类型全局类型，范围为G，GJ，. 描述多方会话的整个会话场景。语法是：全局G：：=p→ G：U.G′ 交换U：：=S|不|......这是什么？|... | G|μt.G|不|端全局类型p→n：U.GJ表示参与者p多播 输入U到参与者集合中，然后G中描述的交互发生。 交换类型U、U J、. 由排序S，SJ，.组成。 对于值（基本类型或全局类型），以及会话类型T，TJ，. 通道（在§4.2中讨论）。全局类型p→ n：{l i：G i}i∈I表示参与者p多播标签l i之一参 与 者的集合。如果lj被发送，则发生全局类型Gj中描述的交互。在这两种情况下，我们假设p/p。全局类型μt.G是一个递归类型，假设类型变量（t，tJ，. ）以标准方式进行保护，即，类型变量只出现在某些前缀下。我们假设G在排序文法中是封闭的没有自由类型变量。类型end表示会话的终止。4.2会话类型进程的本地类型，称为会话类型，定义如下：会话T：：=！好吧，你。不送|?（p，U）。没有收到|⊕⟨ Π, {l i: T i}i∈I⟩selection|&(p, {l i: T i}i∈I)branching|μt.Trecursive|t变量|结束结束全局类型代表整个协议，而会话类型对应于会话中单个参与者的观点。发送类型！好吧，你。T表示将一个值或一个U类型的通道发送给所有参与者，随后是T的通信。选择类型，{l i：T i}i∈I表示在集合{ l i：T i}中选择的标签l i向中的所有参与者的传输|i∈I}之后是由T i描述的通信。接收和分支是⎪144M. Coppo等人/理论计算机科学电子笔记322（2016）135语言1：bool语言2：boolr，u：Su：S[Namertrue，false：bool[BoolΓe1和e2：bool[和表6表达式的一些类型规则中文（简体）γP <$Δ，y：G<$pp= pn（G）Γu：GγP <$Δ，y：G<$pp

下载后可阅读完整内容，剩余1页未读，立即下载