An executable specification and verifier for relaxed memory order

The Mur phi description language and verification system for finite-state c oncurrent systems is applied to the problem of specifying a family of multi processor memory models described in the SPARC Version 9 architecture manua l. The description language allows for a straightforward operational descri ption of the memory model which can be used as a specification for programm ers and machine architects. The automatic verifier can be used to generate all possible outcomes of small assembly language multiprocessor programs in a given memory model, which is very helpful for understanding the subtleti es of the model. The verifier can also check the correctness of assembly la nguage programs including synchronization routines. This paper describes th e memory models and their encoding in the Mur phi description language. We describe how synchronization routines can be verified and how finite stale programs can be analyzed. We also present some interesting findings from th e verification and the analysis.