鐘發(fā)榮，楊振國

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

0 引言

網(wǎng)絡(luò)技術(shù)的快速發(fā)展促進(jìn)了分布式的應(yīng)用和服務(wù).在以通信為中心的程序設(shè)計中，通信協(xié)議較為復(fù)雜，涉及大量的狀態(tài)和狀態(tài)遷移，它們可由不同的消息類型產(chǎn)生.在實現(xiàn)分布式應(yīng)用系統(tǒng)的進(jìn)程時，必須保證進(jìn)程間所傳遞的消息的結(jié)構(gòu)和序列與通信協(xié)議保持一致.

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

本文分析了二元同步會話類型系統(tǒng)中進(jìn)程通信可能產(chǎn)生的死鎖情形，并結(jié)合會話類型的子類型和松弛對偶關(guān)系，給出了類型一致性法則，同時證明了當(dāng)前二元同步會話類型系統(tǒng)保持演進(jìn)特性.

1 會話類型理論基礎(chǔ)

1.1 會話類型

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

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

1.2 會話類型子類型

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

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

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

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

1.3 演進(jìn)特性

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

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

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

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

由x 和y 替換的活動通道導(dǎo)致了死鎖.盡管在會話類型系統(tǒng)中，客戶機(jī)端進(jìn)程上的2 個通道分別為x 和y，分別考察2 個進(jìn)程，它們的結(jié)構(gòu)是正確的且是可類型指派的，但是在活動通道上的通信不能確保演進(jìn)特性.

2 二元會話類型系統(tǒng)

2.1 語法和概念

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

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

圖1 語法

圖2 松弛的對偶關(guān)系

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

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 余歸納的松弛對偶關(guān)系⊥c由T⊥cU 定義，當(dāng)且僅當(dāng)存在一個類型模擬R1使得(T，U)∈R1成立.

2.2 進(jìn)程

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

圖3 進(jìn)程

2.3 會話類型的子類型指派

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

圖4 子類型指派

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

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一定成立;

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

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 余歸納的松弛對偶關(guān)系≤c由T≤cU 定義，當(dāng)且僅當(dāng)存在一個類型模擬R2使得(T，U)∈R2成立.

3 二元同步會話類型系統(tǒng)的通信安全性

3.1 通信中的死鎖情形

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

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

其中，y?［int］和y!［real］類型不兼容，P2| Q2不能繼續(xù)下去.為了處理這種不當(dāng)?shù)耐ㄐ判袨?，Acciai等［8］將類型一致性引進(jìn)到會話類型理論中.進(jìn)一步，結(jié)合會話類型的松弛對偶關(guān)系，給出了新的定義，作為結(jié)果，認(rèn)為P2和Q3符合類型一致性法則.其中

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

例4(雙線性條件) 設(shè)進(jìn)程P4和Q6為:

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

3.2 演進(jìn)特性的保持

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

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

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

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

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

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

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

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

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

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

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

4 結(jié)論

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

［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.