This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Complexity of Verifying Memory Coherence and Consistency
July 2005 (vol. 16 no. 7)
pp. 663-671

Abstract—The problem of testing shared memories for memory coherence and consistency is studied. First, it is proved that detecting violations of coherence in an execution is NP-Complete, and it remains NP-Complete for a number of restricted instances. This result leads to a proof that all known consistency models are NP-Hard to verify. The complexity of verifying consistency models is not a mere consequence of coherence, and verifying sequential consistency remains NP-Complete even after coherence has been verified.

[1] D. Siewiorek and R. Swarz, Reliable Computer Systems, Design and Evaluation, third ed., M.A. Natick, ed. pp. 79-219, A.K. Peters, 1998.
[2] The IBM e-server pSeries 690, “Reliability, Availability, Serviceability (RAS),” technical white paper, IBM, Sept. 2001.
[3] P. Gibbons and E. Korach, “On Testing Cache-Coherent Shared Memories,” Proc. Sixth ACM Symp. Parallel Algorithms and Architectures, pp. 177-188, 1994.
[4] P. Gibbons and E. Korach, “The Complexity of Sequential Consistency,” Proc. Fourth IEEE Symp. Parallel and Distributed Processing, pp. 317-325, 1992.
[5] P. Gibbons and E. Korach, “Testing Shared Memories,” SIAM J. Computing, pp. 1208-1244, Aug. 1997.
[6] P. Gibbons and E. Korach, “New Results on the Complexity of Sequential Consistency,” technical report, AT&T Bell Laboratories, Murray Hill, N.J., Sept. 1993.
[7] A. Gontmakher, S. Polyakov, and A. Schuster, “Complexity of Verifying Java Shared Memory Execution,” Parallel Processing Letters, World Scientific Publishing Company, 2003.
[8] R. Alur, K. McMillan, and D. Peled, “Model-Checking of Correctness Conditions for Concurrent Objects,” Proc. 11th Symp. Logic in Computer Science, pp. 219-228, 1996.
[9] A. Condon and A. Hu, “Automatable Verification of Sequential Consistency,” Proc. Symp. Parallel Algorithms and Architectures, pp. 113-121, 2001.
[10] J. Bingham, A. Condon, and A. Hu, “Toward a Decidable Notion of Sequential Consistency,” Proc. 15th ACM Symp. Parallel Algorithms and Architectures, 2003.
[11] S. Qadeer, “Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model-Checking,” IEEE Trans. Parallel and Distributed Systems, vol. 14, no. 8, Aug. 2003.
[12] C. Papadimitriou, The Theory of Database Concurrency Control. pp. 31-42, Computer Science Press Inc., 1986.
[13] R. Taylor, “Complexity of Analyzing the Synchronization Structure of Concurrent Programs,” Acta Informatica 19, pp. 57-84, 1983.
[14] M. Garey and D. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, pp. 38-39, 95-107, 259, W.H. Freeman and Company, 1979.
[15] L. Lamport, “How to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs,” IEEE Trans. Computers, vol. 28, no. 9, pp. 690-691, Sept. 1979.
[16] SPARC International, Inc., http:/www.sparc.org, 2005.
[17] Intel Corporation, http:/www.intel.com, 2005.
[18] The PowerPC Architecture: A Specification for a New Family of RISC Processors, second ed., C. May, E. Silha, R. Simpson, and H. Warren, eds., Morgan Kaufmann Publishers, Inc. 1994.
[19] X. Shen, Arvind, and L. Rudolph, “Commit-Reconcile & Fences (CRF): A New Memory Model for Architects and Compiler Writers,” Proc Int'l Symp. Computer Architecture, 2000.
[20] K. Gharachorloo, “Memory Consistency Models for Shared-Memory Multiprocessors,” WRL Research Report 95/9, 1995.
[21] P. Keleher, A. Cox, and W. Zwaenepoel, “Lazy Release Consistency for Software Distributed Shared Memory,” Proc. Int'l Symp. Computer Architecture, 1992.
[22] J. Cantin, “The Complexity of Verifying Memory Coherence,” Technical Report ECE-03-01, Univ. of Wisconsin-Madison, 2003.

Index Terms:
Hardware, memory structures, design styles, shared memory, reliability, testing, fault-tolerance, error-checking, theory of computation, nonnumerical algorithms and problems, sequencing and scheduling.
Citation:
Jason F. Cantin, Mikko H. Lipasti, James E. Smith, "The Complexity of Verifying Memory Coherence and Consistency," IEEE Transactions on Parallel and Distributed Systems, vol. 16, no. 7, pp. 663-671, July 2005, doi:10.1109/TPDS.2005.86
Usage of this product signifies your acceptance of the Terms of Use.