Bibliographic Details
| Title: |
Automatable Verification of Sequential Consistency. |
| Authors: |
Condon, Anne E.1 {condon,ajh}@cs.ubc.ca, Hu, Alan J.1 |
| Source: |
Theory of Computing Systems. Sep/Oct2003, Vol. 36 Issue 5, p431. 30p. |
| Subjects: |
Sequential scheduling, Memory |
| 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. [ABSTRACT FROM AUTHOR] |
|
Copyright of Theory of Computing Systems is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
