We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
Automatable Verification of Sequential Consistency.
- Authors
Condon, Anne E.; Hu, Alan J.
- Abstract
Sequential consistency is a multiprocessor memory model of both practical and theoretical importance. Designing and implementing a memory system that efficiently provides a given memory model is a challenging and error-prone task, so automated verification support would be invaluable. Unfortunately, the general problem of deciding whether a finite-state protocol implements sequential consistency is undecidable. In this paper we identify a restricted class of protocols for which verifying sequential consistency is decidable. The class includes all real sequentially consistent protocols that are known to us, and we argue why the class is likely to include all real sequentially consistent protocols. In principle, our method can be applied in a completely automated fashion for verification of all implemented protocols.
- Subjects
SEQUENTIAL scheduling; MEMORY
- Publication
Theory of Computing Systems, 2003, Vol 36, Issue 5, p431
- ISSN
1432-4350
- Publication type
Article
- DOI
10.1007/s00224-003-1082-x