Processors, Caches and Memory Models:
Specification and Verification


MIT Laboratory for Computer Science

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
Robert Blumofe