摘要
基于信念逻辑，分析了曙光超级服务器单一映象文件系统中所采用的基于目录的无效使能Ｃａｃｈｅ一致性协议．首先介绍了Ｃａｃｈｅ一致性协议的目标，并为之建立了系统模型及逻辑，然后以基于目录的无效使能协议为例演示了运用信念逻辑对Ｃａｃｈｅ一致性进行正确性证明的过程．
The notion of belief has been used to reason about authentication protocols, and later it was adopted and extended to check cache coherence in a distributed file system. Using variant of the logic of authentication, the directory based invalidate cache coherence protocol used in the single image file system designed for dawning super server is analyzed in this paper. This paper first introduces the goal of the cache coherence protocol, and builds the system model and logic, then presents some runs from the directory based invalidate protocol, and demonstrates this protocol's correctness.
出处
《计算机学报》
EI
CSCD
北大核心
1999年第5期460-466,共7页
Chinese Journal of Computers
基金
国家八六三高技术研究发展计划
关键词
CACHE
一致性
分布式文件系统
UNIX
操作系统
Belief, cache coherence, directory based invalidate protocol, distributed file system.
