二元會話類型系統中演進特性研究＊

鐘發榮，楊振國

(浙江師范大學 數理與信息工程學院，浙江 金華 321004)

0 引言

網絡技術的快速發展促進了分布式的應用和服務.在以通信為中心的程序設計中，通信協議較為復雜，涉及大量的狀態和狀態遷移，它們可由不同的消息類型產生.在實現分布式應用系統的進程時，必須保證進程間所傳遞的消息的結構和序列與通信協議保持一致.

會話類型理論［1-3］是基于Pi-演算［4-5］的一種形式化方法，能夠結構化交互和解釋通信行為.進一步地，會話類型的子類型［6］能使會話參與者，即使它們分別遵循不同的協議描述，仍能相互兼容地通信，從而增強了會話類型理論的表達力.然而，程序員很難保證在準確、嚴格的時間點發送或接收消息.為了處理這個問題，Dezani-Ciancaglini 等［7］在MOOSE 語言中定義了演進特性，即通信會話一旦開始，合式進程在會話通道上不會發生死鎖.

本文分析了二元同步會話類型系統中進程通信可能產生的死鎖情形，并結合會話類型的子類型和松弛對偶關系，給出了類型一致性法則，同時證明了當前二元同步會話類型系統保持演進特性.

1 會話類型理論基礎

1.1 會話類型

實現涉及復雜通信序列的應用程序時，必須確保消息的序列和結構與通信協議保持一致.然而，標準的編程語言并不支持這一驗證.一種主流的驗證方法是將通信行為先抽象為類型，然后利用這些類型檢查應用程序中實際使用的通道，這就是會話類型的思想.例如，在客戶機-服務器系統中，服務器端的類型為begin.?［int］.!［bool］.end，表示服務器首先接收一個整型值，然后返回一個布爾值，從而結束通信.假設服務器提供的服務分別為求平方和退出，與客戶機端在會話通道x 上發生通信，會話通道的2 個端口分別記為x+和x-，用來表達進程中會話發生的位置，這里+和-為會話通道的極性.通常地，用x+表示服務器端，x-表示客戶機端，2 個端口所對應的會話類型分別為Server1和Client1.例如:

很顯然，Server1| Client1歸約不存在任何問題.＆{…}是分支構造子，表示服務器的外部選擇功能，sqr 和quit 是2 個標號，每個標號有一個后繼類型，用于表示消息序列，?表示輸入，!表示輸出，⊕{…}是選擇構造子，表示客戶機的內部選擇功能.

1.2 會話類型子類型

上例中的服務器端升級后，原先通信協議中的消息序列已經發生了改變.如果此時客戶機端進程的消息序列保持不變，那么兩者又如何繼續通信呢?例如，服務器端消息序列由原來的Server1升級到Server2，即

而客戶機端仍然保持消息序列Client1不變，Server2| Client1歸約如何進行?Gay 等［6］通過定義子類型的概念解決了這個問題:即在服務器端進程升級后、原先的協議和會話類型已經改變的條件下，服務器端仍能夠兼容原來的客戶機進程，使兩者安全地通信，但要求輸入、分支和后繼會話類型具有協變性，輸出和選擇會話類型具有逆變性(?［int］≤?［real］，!［real］≤!［int］).例如，服務器端的會話類型從?［int］升級到?［real］，表明服務器端當前期待接收一個實型值.由于子類型的定義，服務器端也能夠接收諸如整型等類型的值，從而在相同的通道中，2 種不同會話類型相互兼容.升級后的服務器端與保持不變的客戶機端仍可以安全地通信.

會話類型子類型能夠解決服務器端升級的問題.利用傳統對偶規則，可以推斷與升級后的服務器相匹配的客戶機端的會話類型，直接得到Client2，即

事實上，客戶機端的類型仍然保持Client1不變.由于引入了子類型概念，使得Server2和Client1在通信過程中不會產生錯誤，因此定義了松弛對偶關系概念，將Server2和Client1也視為對偶的，這樣不僅進一步提高了系統的靈活性，也有助于演進特性的研究.

1.3 演進特性

首先，通信通道被區分成共享通道和活動通道2 種，其中共享通道用于通信時建立連接.連接建立以后，約束通道名字由活動通道替換，這里活動通道是新私有名字.演進特性要求類型系統中進程通信一旦發生，合式進程在通道上不會發生死鎖.演進特性能確保在運行前發現通信進程中所隱含的錯誤，以及通信歸約的安全性，是各種應用程序安全的基本要求.為了解釋此通信安全問題，考慮下面的客戶機-服務器交互模式的進程，假設服務器端進程為

首先通過共享通道a 接收一個活動通道，然后活動通道替換x 并執行如下通信:輸出一個整型值，輸入一個整型值，輸出一個字符串，最后繼續P1進程.客戶端進程為

請求共享通道a 上的會話通信，然后通過活動通道x 執行與服務器端類型對偶的動作.一旦會話建立，很顯然，活動通道上的通信總能繼續.

上面例子僅局限在2 個參與者在一個會話中的交互.實際上，在Web 服務通信中，在2 個甚至多個參與者中建立多個會話的情況是很常見的.這種情況下，當2 個或多個會話交織時，安全性很容易被破壞，最簡單的例子如下:

由x 和y 替換的活動通道導致了死鎖.盡管在會話類型系統中，客戶機端進程上的2 個通道分別為x 和y，分別考察2 個進程，它們的結構是正確的且是可類型指派的，但是在活動通道上的通信不能確保演進特性.

2 二元會話類型系統

2.1 語法和概念

下面首先定義消息類型和會話類型，然后定義松弛的對偶關系.

類型的語法如圖1 所示.假設端口x+的會話類型為S，那么，端口x-的會話類型則為，稱其為類型S 的對偶.圖2 定義了非遞歸類型的松弛對偶關系，對于遞歸類型，給出余歸納的定義.

圖1 語法

圖2 松弛的對偶關系

定義1 一個關系R1?Type×Type 被稱為松弛的對偶關系，如果滿足下面條件:

1)如果unfold(T)=?［T］.S1且unfold(U)=!［U］.S2成立，那么(S1，S2)∈R1且U≤cT 一定成立;

2)如果unfold(T)=!［T］.S1且unfold(U)=?［U］.S2成立，那么(S1，S2)∈R1且T≤cU 一定成立;

3)如果unfold(T)=＆{l1:S1，l2:S2，…，ln:Sn}且unfold(U)=⊕{l1:V1，l2:V2，…，lm:Vm}成立，那么(Si，Vi)∈R1一定成立;

4)如果unfold(T)=⊕{l1:S1，l2:S2，…，lm:Sm}且unfold(U)=＆{l1:V1，l2:V2，…，ln:Vn}成立，那么(Si，Vi)∈R1一定成立;

5)如果unfold(T)=end 成立，那么unfold(U)=end 一定成立.

定義2 余歸納的松弛對偶關系⊥c由T⊥cU 定義，當且僅當存在一個類型模擬R1使得(T，U)∈R1成立.

2.2 進程

進程的語法如圖3 定義，其中大多數語法是標準的.名字是極化的，表示為x+或x-，或直接用xp表示.其中:p 表示可選擇的極性;0 是空進程，表示該進程不做任何動作;|是并行復合.

圖3 進程

2.3 會話類型的子類型指派

非遞歸會話類型的子類型指派規則如圖4 所示，其中有界類型變量X1，X2，…，Xn都滿足環境△=L1≤X1≤U1，L2≤X2≤U2，…，Ln≤Xn≤Un.對于遞歸會話類型的子類型，給出余歸納的定義.

圖4 子類型指派

定義3 一個關系R2?Type×Type 被稱為松弛的對偶關系，如果滿足下面條件:

1)若unfold(T)=?［T］.S1且unfold(U)=!［U］.S2成立，則(S1，S2)∈R2且(T，U)∈R2一定成立;

2)若unfold(T)=!［T］.S1且unfold(U)=?［U］.S2成立，則(S1，S2)∈R2且(U，T)∈R2一定成立;

3)若unfold(T)=＆{l1:S1，l2:S2，…，ln:Sn}且unfold(U)=⊕{l1:V1，l2:V2，…，lm:Vm}成立，則(Si，Vi)∈R2一定成立;

而據宮寶田弟子回憶，師父給許世友展示了刀法，水潑不進，而許世友也展示了刀法，快準狠絕，師父給許世友展示了輕功，警衛用槍都打不到他，而許世友則展示了暗器飛蝗石的絕技，用石子兒打中了師父的氈帽。

4)若unfold(T)=⊕{l1:S1，l2:S2，…，lm:Sm}且unfold(U)=＆{l1:V1，l2:V2，…，ln:Vn}成立，則(Si，Vi)∈R2一定成立;

5)若unfold(T)=end 成立，則unfold (U)=end 一定成立.

定義4 余歸納的松弛對偶關系≤c由T≤cU 定義，當且僅當存在一個類型模擬R2使得(T，U)∈R2成立.

3 二元同步會話類型系統的通信安全性

3.1 通信中的死鎖情形

注意上述2 個進程所遵循的協議中的消息類型是不同的.由于引入了會話類型的子類型概念，兩者通信歸約不會產生錯誤，松弛的對偶關系很好地解決了此類問題.

例2(類型一致性) 盡管引入了會話類型的子類型，然而2 個進程所遵循的協議并不總是相互兼容的.例如:

其中，y?［int］和y!［real］類型不兼容，P2| Q2不能繼續下去.為了處理這種不當的通信行為，Acciai等［8］將類型一致性引進到會話類型理論中.進一步，結合會話類型的松弛對偶關系，給出了新的定義，作為結果，認為P2和Q3符合類型一致性法則.其中

上述2 個進程中，每個進程有2 個共享通道a 和b，分別限制了x 和y 兩個活動通道，2 個進程使用活動通道的順序恰好相反，在同步通信中P3| Q4可導致死鎖，此情形在類型一致性法則的定義中得到了解決，它允許進程P3與進程Q5等并行復合.其中

例4(雙線性條件) 設進程P4和Q6為:

P4| Q6不能完成通信，雙線性條件阻止了此類情形的發生.雙線性條件是指有且僅有2 個進程包含相同名字的活動通道.

3.2 演進特性的保持

定義5(演進特性) 稱進程P 保持演進特性，當P→P′蘊含要么P′中不包含活動通道，要么Q/→，使得P′ | Q→且P′ | Q 是合式的.

若一個進程P 不死鎖，則它能保持演進特性，而某些“壞”形式的進程可能產生死鎖.不可歸約進程，如果能與其他不可歸約進程Q 交互，那么它也保持演進特性.下面給出二元同步會話中的類型一致性法則.

法則1 對于發生在二元同步會話中的通信進程，所有會話類型必須滿足如下要求:

1)共享通道名字是自由的;

2)進程兩端的活動通道上的端口滿足雙線性條件;

3)相同通道名字的2 個端口滿足類型一致性法則.

定理1(演進特性) 二元同步通信中，如果客戶機-服務器交互進程P|Q 滿足上述法則，那么P|Q保持演進特性.

證明 假設P0=P | Q 是一個進程，并且P0→*P1，考慮P1的如下3 種可能情形:

1)P1不包含活動通道，或者P1→P′，則P1直接保持演進特性.

2)P1是不可歸約表達式，其前綴動作是自由共享通道a 上的接收或發送動作.根據松弛對偶關系的定義，總能建立一個不可歸約表達式Q2作為共享通道a 上的請求進程，這也是不能將所有不可歸約表達式視為死鎖的原因.即使一個不可歸約的表達式P1，只要它能夠與某個進程Q2進行并行復合，并且使得P1| Q2是合式的，那么該表達式保持演進特性.

3)P1的前綴動作在共享通道上既不包含接收也不包含發送動作，但包含活動通道kp.由于共享通道滿足雙線性條件和類型一致性法則，所以kp一定會在P1中發生，這意味著它與P1能夠歸約的情形相同.

4 結論

本文提出了保持演進特性的二元同步會話類型系統，該類型系統確保一旦會話開始，參與者能夠完成所有通信動作而不會陷入死鎖狀態.為了確保當前類型系統保持演進特性，本文分析了二元同步會話類型系統中進程之間通信可能產生的死鎖情形，并結合會話類型的子類型和松弛對偶關系定義了類型一致性法則，最后證明了當前類型系統的演進特性.

［1］Honda K.Types for dyadic interaction［C］//Eike Best.Proceedings of the 4th International Conference on Concurrency Theory (CONCUR′93)，Lecture Notes in Computer Science 715.Berlin:Springer-Verlag，1993:509-523.

［2］Takeuchi K，Honda K，Kubo M.An interaction-based language and its typing system［C］//Halatsis C，Maritsas D，Philokyprou G，et al.Proceedings of the 6th International PARLE Conference on Parallel Architectures and Languages Europe (PARLE′94)，Lecture Notes in Computer Science 817.Berlin:Springer-Verlag，1994:398-413.

［3］Honda K，Vasconcelos V，Kubo M.Language primitives and type discipline for structured communication-based programming［C］//Chris Hankin.Proceedings of the 7th European Symposium on Programming(ESOP′98)，Lecture Notes in Computer Science 1381.Berlin:Springer-Verlag，1998:122-138.

［4］Sangiorgi D，Walker D.The π-calculus:a theory of mobile processes［M］.Cambridge:Cambridge University Press，2003.

［5］Milner R，Parrow J，Walker D.A calculus of mobile processes，I and II［J］.Information and Computation，1992，100(1):1-77.

［6］Gay S，Hole M.Types and subtypes for client-server interactions［C］//Swierstra S.Proceedings of the 8th European Symposium on Programming(ESOP′99)，Lecture Notes in Computer Science 1576.Berlin:Springer-Verlag，1999:640-640.

［7］Dezani-Ciancaglini M，Mostrous D，Yoshida N，et al.Session types for object-oriented languages［C］//Thomas D.Proceedings of the 20th European Conference on Object-Oriented Programming (ECOOP′2006)，Lecture Notes in Computer Science 4067.Berlin:Springer-Verlag，2006:328-352.

［8］Acciai L，Boreale M.A type system for client progress in a service-oriented calculus［J］.Lecture Notes in Computer Science，2008，5065:642-658.