Verifying Memory System Protocols

We have proposed a framework for verifying that multiprocessor memory systems satisfy the requirements of memory consistency models. As an increasing number of optimizations and relaxed consistency models are being used in modern multiprocessors, a methodology for proving system correctness is necessary to convince memory system designers that their systems behave correctly. The verification framework utilizes a logical clocking scheme to define a total ordering on the events occurring in the system. We then prove properties of this ordering that guarantee the satisfaction of a particular memory consistency model. In this report, we provide proofs that show that two simple memory systems (a bus-based system and a directory-based system) observe sequential consistency. We also outline the ways in which this method could be applied to prove that more aggressive memory systems observe more relaxed consistency models. 1 Introduction Memory systems for parallel computers are becoming incre..