|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| 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. | |||
| BibTex | x | ||
| @article{ 10.1109/TPDS.2005.86, author = {Jason F. Cantin and Mikko H. Lipasti and James E. Smith}, title = {The Complexity of Verifying Memory Coherence and Consistency}, journal ={IEEE Transactions on Parallel and Distributed Systems}, volume = {16}, number = {7}, issn = {1045-9219}, year = {2005}, pages = {663-671}, doi = {http://doi.ieeecomputersociety.org/10.1109/TPDS.2005.86}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Parallel and Distributed Systems TI - The Complexity of Verifying Memory Coherence and Consistency IS - 7 SN - 1045-9219 SP663 EP671 EPD - 663-671 A1 - Jason F. Cantin, A1 - Mikko H. Lipasti, A1 - James E. Smith, PY - 2005 KW - Hardware KW - memory structures KW - design styles KW - shared memory KW - reliability KW - testing KW - fault-tolerance KW - error-checking KW - theory of computation KW - nonnumerical algorithms and problems KW - sequencing and scheduling. VL - 16 JA - IEEE Transactions on Parallel and Distributed Systems ER - | |||
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.