A Knowledge Based Analysis of Cache Coherence
作者： Kai Baukus , Ron van der Meyden
DOI: 10.1007/978-3-540-30482-1_15
关键词: Shared memory 、 Parallel computing 、 Cache invalidation 、 Concurrency 、 Cache coherence 、 Cache algorithms 、 CPU cache 、 Knowledge base 、 Cache coloring 、 MESIF protocol 、 Theoretical computer science 、 Write-once 、 Computer science 、 Cache
摘要: This paper presents a case study of the application knowledge-based approach to concurrent systems specification, design and verification. A highly abstract solution cache coherence problem is first presented, in form program, that formalises intuitions underlying MOESI [Sweazey & Smith, 1986] characterisation coherency protocols. It shown any concrete implementation this which relates cache’s actions its knowledge about status other caches, correct problem. Three existing protocols class are be such implementations. The furthermore raises question whether these optimal their use information available caches. investigated using by model checker MCK, able verify specifications logic time.
springer.com
sci-hub.st 参考文章(22)
Kai Engelhardt, Ron van der Meyden, Yoram Moses, A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents international conference on logic programming. pp. 125- 141 ,(2001) , 10.1007/3-540-45653-8_9
Ron van der Meyden, Yoram Moses, On Refinement and Temporal Annotations FTRTFT '00 Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. pp. 185- 201 ,(2000) , 10.1007/3-540-45352-0_16
Jim Handy, The Cache Memory Book ,(1993)
Peter Gammie, Ron van der Meyden, MCK: Model Checking the Logic of Knowledge Computer Aided Verification. ,vol. 3114, pp. 479- 483 ,(2004) , 10.1007/978-3-540-27813-9_41
Ron van der Meyden, Yoram Moses, Kai Engelhardt, Knowledge and the logic of local propositions theoretical aspects of rationality and knowledge. pp. 29- 41 ,(1998)
Kai Engelhardt, Ron van der Meyden, Yoram Moses, A Program Refinement Framework Supporting Reasoning about Knowledge and Time foundations of software science and computation structure. pp. 114- 129 ,(2000) , 10.1007/3-540-46432-8_8
Ron van der Meyden, Yoram Moses, Kai Engelhardt, A Refinement Theory that Supports Reasoning About Knowledge and Time LPAR '01 Proceedings of the Artificial Intelligence on Logic for Programming. pp. 125- 141 ,(2001)
Ian Hodkinson, Frank Wolter, Michael Zakharyaschev, Monodic fragments of first-order temporal logics: 2000-2001 A.D international conference on logic programming. pp. 1- 23 ,(2001) , 10.1007/3-540-45653-8_1
Formal Techniques in Real-Time and Fault-Tolerant Systems Kluwer Academic Publishers. ,(1993) , 10.1007/978-1-4615-3220-0
Ronald Fagin, Yoram Moses, Joseph Y. Halpern, Moshe Y. Vardi, Knowledge-based programs principles of distributed computing. pp. 153- 163 ,(1995) , 10.1145/224964.224982