| LBCCP:一种符合UNIX语义的文件缓存一致性协议及其证明 |
| |
| 引用本文： | 吕毅,贺劲. LBCCP:一种符合UNIX语义的文件缓存一致性协议及其证明[J]. 微电子学与计算机, 2003, 20(6): 12-17 |
| |
| 作者姓名： | 吕毅 贺劲 |
| |
| 作者单位： | 中国科学院计算技术研究所智能中心,北京,100080 |
| |
| 基金项目： | 国家863计划项目基金(863-306-ZD01-01)，中科院计算所领域前沿青年基金(20026180-2) |
| |
| 摘 要： | 机群文件系统是机群操作系统的一个重要组成部分，而具有不同语义的文件系统的性能会有显著的差异。高效的客户端缓存协议是机群文件系统性能的关键问题之一。文章提出了一种新型文件缓存一致性协议，该协议通过扩展POSIX文件锁的API来实现UNIX语义模型，并利用I/O自动机理论证明了协议的正确性，在DCFS(Dawning Cluster Fils System)上实现了这个协议。
|
| 关 键 词： | 机群文件系统 机群操作系统 文件缓存一致性协议 LBCCP UNIX 语义 形式证明 |
| 修稿时间： | 2002-11-28 |
Proving Correctness of a Lock-based Cache Coherency Protocol for a Cluster File System |
| |
| LV Yi,HE Jin. Proving Correctness of a Lock-based Cache Coherency Protocol for a Cluster File System[J]. Microelectronics & Computer, 2003, 20(6): 12-17 |
| |
| Authors: | LV Yi HE Jin |
| |
| Abstract: | Cluster file system is an important component of cluster operating system,and client-side caching is one of the key issues that address the performance problem of cluster file system.However,there is little study on the formalization of file system semantics and verification of cache coherency proto-col in cluster file system.This paper presents a new cache co-herency protocol to achieve UNIX semantics in cluster file sys-tem by extending the capability of POSIX file lock API and gives the formal proof using I/O automata theory.This protocol has been implemented in DCFS(Dawning Cluster File System). |
| |
| Keywords: | Cluster file system Cache coherency protocol I/O automata Formal proof |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
