客戶機(jī)—服務(wù)器交互模式類型系統(tǒng)的演進(jìn)特性研究.pdf

1、隨著計(jì)算機(jī)網(wǎng)絡(luò)及通信技術(shù)的發(fā)展，以分布性、并發(fā)性、異構(gòu)性和互操作性等為主要特征的并發(fā)分布式計(jì)算已成為計(jì)算機(jī)研究中的主流方向。確保并行分布式系統(tǒng)進(jìn)行安全交互的結(jié)構(gòu)化通信，是并發(fā)分布式計(jì)算理論和實(shí)踐的中心問(wèn)題?；赑i-演算的會(huì)話類型理論為結(jié)構(gòu)化通信提供了理論基礎(chǔ)，是結(jié)構(gòu)化交互和解釋通信行為的一種有效的形式化方法。在分布式計(jì)算場(chǎng)景中，存在大量通過(guò)消息傳遞進(jìn)行通信的程序，會(huì)話類型理論能夠驗(yàn)證傳遞消息的結(jié)構(gòu)和序列，并分析其與協(xié)議描述是否一致。以

2、會(huì)話類型理論為基礎(chǔ)的類型系統(tǒng)，是研究如何將編程語(yǔ)言中的數(shù)值和表達(dá)式歸為類型，以及類型之間互相作用的形式化方法。類型系統(tǒng)能夠分析和禁止程序中非正常的行為，避免發(fā)生運(yùn)行時(shí)錯(cuò)誤，確保語(yǔ)言的安全性。會(huì)話類型理論及類型系統(tǒng)，是以通信為中心的分布式程序設(shè)計(jì)研究的關(guān)鍵問(wèn)題。
　　本文的工作主要圍繞有界多態(tài)的類型系統(tǒng)中，描述無(wú)限次重復(fù)行為、同步和異步通信中保持演迸特性，以及異步交互序列的局部?jī)?yōu)化等問(wèn)題而展開(kāi)，其主要研究?jī)?nèi)容及貢獻(xiàn)如下:
　　

3、(1)研究了會(huì)話類型和Pi-演算的當(dāng)前工作以及已有的類型系統(tǒng)，提出帶有遞歸類型的有界多態(tài)類型系統(tǒng)。遞歸會(huì)話類型允許協(xié)議描述不定次數(shù)的重復(fù)行為，在客戶機(jī)-服務(wù)器交互模式中，服務(wù)器端進(jìn)程不僅能提供一次服務(wù)，而且能提供任意次數(shù)的服務(wù)，提高了系統(tǒng)的靈活性。同時(shí)，結(jié)合會(huì)話類型子類型，定義了松弛對(duì)偶關(guān)系，該關(guān)系不僅使得通信兩端交互的類型更加靈活，而且有助于定義類型一致性則和研究演進(jìn)特性。此外，遞歸會(huì)話類型本身是會(huì)話類型的一種，因此定義了遞歸會(huì)話類型

4、的子類型及其松弛的對(duì)偶關(guān)系。
　　(2)研究了演進(jìn)特性分別在同步和異步通信中的保持，并證明了系統(tǒng)可靠性和通信安全性。通道類型被區(qū)分為共享通道和活動(dòng)通道，并分析了在同步和異步環(huán)境下，以及在不同類型通道中，可能產(chǎn)生死鎖的情形。進(jìn)一步地，分析了產(chǎn)生死鎖的原因并給出了解除死鎖的方法，結(jié)合松弛的對(duì)偶關(guān)系定義了類型一致性法則等法則，確保類型系統(tǒng)保持演進(jìn)特性。此外，證明類型系統(tǒng)保持主題歸約理論、類型安全理論和演進(jìn)特性等，確保了系統(tǒng)可靠性和通信安

5、全性。
　　(3)特別地，對(duì)于部分可交換的異步二元會(huì)話及多元會(huì)話，通過(guò)引入異步通信子類型，使每一位參與者上的動(dòng)作序列可以進(jìn)行排列和局部?jī)?yōu)化，提高通信效率的同時(shí)，有效地解除了通信過(guò)程中發(fā)生的死鎖。此外，消息類型被區(qū)分成依賴和非依賴的類型，并分別定義了動(dòng)作異步子類型指派規(guī)則。同時(shí)，由于異步動(dòng)作排列和優(yōu)化將改變接收和發(fā)送消息的序列和結(jié)構(gòu)，為了確保通信安全性，本文通過(guò)具體例子揭示了其中產(chǎn)生死鎖的情形，并保持了演進(jìn)特性。此外，為了使動(dòng)作排列