Computer Assisted Analysis of Multiprocessor Memory Systems. Stanford University, June 1996.
Parallel architecture becomes more and more attractive as the demand for performance increases.
One of the most important classes of parallel machines is that of shared memory architectures, which are perceived as easier to program than other parallel architectures. Memory models and cache coherence protocols can be quite complex and subtle, creating a real possibility of misunderstandings and actual design errors. In this thesis, we will present solutions to the problems of specifying memory models and verifying the correctness of cache coherence protocols. Weaker memory models for multiprocessor systems allow higher-performance implementation techniques for memory systems. However, weak memory models are also very subtle.