A Knowledge Based Analysis of Cache Coherence
A Knowledge Based Analysis of Cache Coherence
复制标题
基于知识的缓存一致性分析
DOI：
10.1007/978-3-540-30482-1_15
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
R. V. D. Meyden
中科院分区：
文献类型：
--
作者：
K. Baukus;R. V. D. Meyden
本文提出了一个案例研究的应用知识为基础的方法，并发系统的规格说明，设计和验证。一个高度抽象的解决方案，该高速缓存一致性问题的第一次提出，在一个基于知识的程序的形式，形式化的直觉基本的MOESI [Sweazey和史密斯，1986年]表征的高速缓存一致性协议。它表明，任何具体的实施，这种基于知识的程序，涉及到一个高速缓存的行动，其知识的状态，其他高速缓存，是一个正确的解决方案的该高速缓存一致性问题。三个现有的协议在MOESI类被证明是这样的实现。基于知识的表征还提出了这些协议是否是最佳的，在他们使用的信息提供给缓存的问题。这个问题的研究使用的模型检查器MCK，它能够验证规格的知识和时间的逻辑。
This paper presents a case study of the application of the knowledge-based approach to concurrent systems specification, design and verification. A highly abstract solution to the cache coherence problem is first presented, in the form of a knowledge-based program, that formalises the intuitions underlying the MOESI [Sweazey & Smith, 1986] characterisation of cache coherency protocols. It is shown that any concrete implementation of this knowledge-based program, which relates a cache’s actions to its knowledge about the status of other caches, is a correct solution of the cache coherence problem. Three existing protocols in the MOESI class are shown to be such implementations. The knowledge-based characterisation furthermore raises the question of whether these protocols are optimal in their use of information available to the caches. This question is investigated using by the model checker MCK, which is able to verify specifications in the logic of knowledge and time.