Report Number: CSL-TR-96-696
Institution: Stanford University, Computer Systems Laboratory
Title: Computer Assisted Analysis of Multiprocessor Memory Systems
Author: Park, Seungjoon
Date: June 1996
Abstract: In a shared memory multiprocessor architecture, a memory model describes the behavior of the memory system as observed at the user-level. A cache coherence protocol aims to conform to a memory model by maintaining consistency among the multiple copies of cached data and the data in main memory. 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 these problems. Though weaker memory models for multiprocessor systems allow higher-performance implementation techniques, they are also very subtle. Hence, it is vital to specify memory models precisely and to verify that the programs running under a memory model satisfy desired properties. Our approach to these problems is to write an executable specification of the memory model using a high-level description language for concurrent systems. This executable description provides a precise specification of the machine architecture for implementors and programmers. Moreover, the availability of formal verification tools allows users to experiment with the effects of the memory model on small assembly-language routines. Running the verifier can be very effective at clarifying the subtle details of the models and synchronization routines. Cache coherence protocols, like other protocols for distributed systems, simulate atomic transactions in environments where atomic implementations are impossible. Based on this observation, we propose a verification method which compares an implementation with a specification representing the desired abstract behavior. The comparison is done through an aggregation function, which maps the sequence of implementation steps for each transaction to the corresponding transaction step in the specification. The aggregation approach is applied to verification of the cache coherence protocol in the FLASH multiprocessor system. The protocol, consisting of more than a hundred implementation steps, is proved to conform to a reduced description with six kinds of atomic transactions. From the reduced behavior, it is very easy to prove crucial properties of the protocol including data consistency of cached copies. The aggregation method is also used to prove that the reduced protocol satisfies a desired memory consistency model.