An executable specification and verifier for relaxed memory order
- 1 February 1999
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. 48 (2) , 227-235
- https://doi.org/10.1109/12.752664
Abstract
The Mur/spl psi/ description language and verification system for finite-state concurrent systems is applied to the problem of specifying a family of multiprocessor memory models described in the SPARC Version 9 architecture manual. The description language allows for a straightforward operational description of the memory model which can be used as a specification for programmers 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 subtleties of the model. The verifier can also check the correctness of assembly language programs including synchronization routines. This paper describes the memory models and their encoding in the Mur/spl psi/ description language. We describe how synchronization routines can be verified and how finite state programs can be analyzed. We also present some interesting findings from the verification and the analysis.Keywords
This publication has 10 references indexed in Scilit:
- Transparent and scalable client-side server selection using NetletsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Weak ordering-a new definitionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Memory consistency and event ordering in scalable shared-memory multiprocessorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The Mur ϕ verification systemPublished by Springer Nature ,1996
- Formal verification for fault-tolerant architectures: prolegomena to the design of PVSIEEE Transactions on Software Engineering, 1995
- Programming for different memory consistency modelsJournal of Parallel and Distributed Computing, 1992
- Proving sequential consistency of high-performance shared memories (extended abstract)Published by Association for Computing Machinery (ACM) ,1991
- Correct memory operation of cache-based multiprocessorsPublished by Association for Computing Machinery (ACM) ,1987
- Memory access buffering in multiprocessorsACM SIGARCH Computer Architecture News, 1986
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess ProgramsIEEE Transactions on Computers, 1979