The lack of precise, well-defined Memory Models and Cache Coherence Protocols has bothered me for many years, especially while teaching the graduate architecture subject. There is also a problem in defining the meaning of certain memory related instructions in modern processors. This lack of precision may have lead to several "MP-challenged" microprocessors. Using Term Rewriting techniques, I will present models for modern processors and discuss in what sense a processor with register renaming or speculative execution is a correct implementation of an instruction set.
We have already had considerable success in using our technique to prove the correctness of a cache-coherence protocol to implement Lamport's Sequential Consistency on a system with hierarchical caches and non-FIFO networks.
This talk is about work-in-progress which is being done jointly with Xiaowei Shen.
No prior knowledge of Term Rewriting will be assumed.
Back to LESS
Last modified: September 12, 1997