证明和测试分布式系统的功能正确性 ——机群文件系统共享语义和网格使用模式研究

发布时间：2021-10-04 23:36

　　由于分布式系统的固有复杂性,结合分布式系统的领域背景来证明和验证分布式系统的功能正确性一直是计算机科学领域的重要问题。机群系统和网格系统均是高度复杂的分布式系统,其中机群文件系统共享语义和网格使用模式的研究分别是涉及各自领域的功能正确性、性能和易用性的关键问题。本文首先从文件系统共享文件语义和计算机使用模式这两个方面系统地综述了机群文件系统语义和网格使用模式领域的主要研究成果。作为本文的研究重点之一,在机群文件系统共享语义研究方面,从文件缓存协议构造、语义正确性证明和共享语义测试等方面对机群文件系统共享语义的关键问题进行了深入探讨。在网格的用户使用模式研究方面,本文对用户和服务网格系统进行理论建模,提出并证明了用户3A使用服务网格必须满足的一些性质和条件。本文创造性的工作主要有三个方面:（1）提出了一种基于POSIX文件锁的缓存一致性协议LBCCP,该协议能够在文件粒度支持动态调整文件共享语义。本文给出了LBCCP协议的I/O自动机模型并证明了LBCCP协议的正确性,在证明过程中找到并改正了DCFS文件系统协议中的几处错误。（2）提出了文件系统共享语义测试概念并实现了一个文件语义测试系... 

【文章来源】：中国科学院大学(中国科学院计算技术研究所)北京市

【文章页数】：135 页

【学位级别】：博士

【部分图文】：

K/G使用模式结构模型图（摘自参考文献[Yang03]）

证明和测试分布式系统的功能正确性-机群文件系统共享语义和网格使用模式研究；而远程服务模型相对简单，无需在机群文件系统客户节点上增加，因此开发难度大大降低，系统正确性较容易验证，另外其出错处单。件缓存实现文件缓存所在位置，机群文件系统中的文件缓存可以划分为以下两缓存与服务器缓存。前者位于机群文件系统客户节点上，既可以在，也可以在客户节点本地磁盘中；后者位于服务器节点上。它们构示的缓存层次结构[He02]。

Data-Consistency Semantics），即如果进程从文件的某个偏，则当写操作完成后，则写入结果对所有其他进程所见显式的缓存同步操作；②原子语义，如果底层文件系统不，则性能将好于提供原子语义的系统，但由于存在需要原此底层文件系统应提供用户选择的机会。原则①和②实义，但 MPI-IO 标准对它有一些放松，即更新后的内容 I/O 的通信子内的其他进程立即可见，而对于系统实现者区别。因此底层文件系统必须提供 UNIX 语义支持才能应用是机群文件系统的另一个重要应用领域。在这一应用中文件的形式存储在机群文件系统中，页面的并发更新表而 Web 客户的页面请求表现为文件的读操作。IBM 公司统建立了奥林匹克运动会 Web 网站并提供给全球用户服在 Web 服务方面的一个典型应用[Bur00-1]。

【参考文献】：
期刊论文
[1]FSbench:一个机群文件系统基准程序[J]. 吕毅,马捷,唐荣锋.  计算机工程. 2004(02)
[2]K/G:一种网格的使用模式体系结构及应用[J]. 杨宁,李晓林,周浩杰,潘高峰.  计算机研究与发展. 2003(12)
[3]GSML网格编程语言的一种实现方法[J]. 李丙辰,徐志伟.  计算机研究与发展. 2003(12)
[4]普适计算[J]. 徐光祐,史元春,谢伟凯.  计算机学报. 2003(09)
[5]织女星网格的体系结构研究[J]. 徐志伟,李伟.  计算机研究与发展. 2002(08)



本文编号：3418554