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

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

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

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

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

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