The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.11 - Nov. (2012 vol.23)
pp: 2163-2174
Yunji Chen , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
Lei Li , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
Tianshi Chen , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
Ling Li , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
Lei Wang , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
Xiaoxue Feng , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
Weiwu Hu , Chinese Academy of Sciences and Loongson Technologies Corporation Limited, Beijing
ABSTRACT
A widely adopted methodology for verifying the memory subsystem of a Chip Multiprocessor (CMP) is to verify executions of parallel test programs on the CMP against the given memory consistency model, which has been long known to be time consuming in both theory and practice. To accelerate memory consistency verification, previous approaches have to bear the cost of availability (e.g., relying on dedicated hardware supports that have not been offered by many commodity CMPs) or completeness (e.g., missing some bugs). In the meantime, the impact of parallel programs on memory consistency verification has more or less been overlooked. One piece of evidence is that few investigations have been dedicated to finding appropriate test programs enabling more efficient verification From a novel perspective of test program, we devise a practical technique called “program regularization,” which can effectively reduce the computation time of memory consistency verification. The key intuition behind program regularization is that any parallel program, if being reformed appropriately, can enable efficient memory consistency verification. More specifically, for an original program, program regularization introduces some auxiliary memory addresses, and periodically inserts load/store operations accessing these addresses to the original program. With the regularized program, memory consistency verification can be accomplished in linear time (with respect to the number of memory operations) when the number of processors is fixed. Experimental results show that program regularization can significantly accelerate memory consistency verification. Last but not least, our technique, which does not rely on concrete verification algorithm or dedicated hardware support, can be smoothly integrated into existing presilicon/postsilicon verification platforms of industrial CMPs to speed up memory consistency verification.
INDEX TERMS
Program processors, Law, Complexity theory, Memory management, Receivers, Hardware, VSC-read, Memory consistency verification, frontier graph, parallel program, program regularization
CITATION
Yunji Chen, Lei Li, Tianshi Chen, Ling Li, Lei Wang, Xiaoxue Feng, Weiwu Hu, "Program Regularization in Memory Consistency Verification", IEEE Transactions on Parallel & Distributed Systems, vol.23, no. 11, pp. 2163-2174, Nov. 2012, doi:10.1109/TPDS.2012.44
REFERENCES
[1] D. Abts, S. Scott, and D. Lilja, "So Many States, So Little Time: Verifying Memory Coherence in the Cray X1," Proc. 17th Int'l Parallel and Distributed Processing Symp. (IPDPS '03), 2003.
[2] S. Baswana, S. Mehta, and V. Powar, "Implied Set Closure and Its Application to Memory Consistency Verification," Proc. 20th Int'l Conf. Computer Aided Verification (CAV '08), 2008.
[3] H. Cain and M. Lipasti, "Verifying Sequential Consistency Using Vector Clocks," Proc. 14th ACM Symp. Parallel Algorithms and Architectures (SPAA '02), 2002.
[4] J. Cantin, M. Lipasti, and J. Smith, "The Complexity of Verifying Memory Coherence," Proc. 15th ACM Symp. Parallelism in Algorithms and Architectures (SPAA '03), 2003.
[5] J. Cantin, M. Lipasti, and J. Smith, "The Complexity of Verifying Memory Coherence and Consistency," IEEE Trans. Parallel and Distributed Systems, vol. 16, no. 7, pp. 663-671, July 2005.
[6] P. Chatterjee, H. Sivaraj, and G. Gopalakrishnan, "Shared Memory Consistency Protocol Verification against Weak Memory Models: Refinement via Model-Checking," Proc. 14th Int'l Conf. Computer Aided Verification (CAV '02), 2002.
[7] K. Chen, S. Malik, and P. Patra, "Runtime Validation of Memory Ordering Using Constraint Graph Checking," Proc. 14th IEEE Int'l Symp. High-Performance Computer Architecture (HPCA '08), 2008.
[8] Y. Chen, Y. Lv, W. Hu, T. Chen, H. Shen, P. Wang, and H. Pan, "Fast Complete Memory Consistency Verification," Proc. 15th IEEE Int'l Symp. High-Performance Computer Architecture (HPCA '09), 2009.
[9] Y. Chen, T. Chen, and W. Hu, "Global Clock, Physical Time Order and Pending Period Analysis in Multiprocessor Systems," CoRR abs/0903.4961, http://arxiv.org/pdf0903.4961, 2009.
[10] Y. Chen, W. Hu, T. Chen, and R. Wu, "LReplay: A Pending Period Based Deterministic Replay Scheme," Proc. 37th ACM/IEEE Int'l Symp. Computer Architecture (ISCA '10), 2010.
[11] E. Clarke, "Model Checking - My 27-Year Quest to Overcome the State Explosion Problem," Proc. 15th Int'l Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR '08), 2008.
[12] W. Collier, Reasoning About Parallel Architectures. Prentice-Hall Press, 1992.
[13] A. Condon, M. Hill, M. Plakal, and D. Sorin, "Using Lamport Clocks to Reason about Relaxed Memory Models," Proc. Fifth IEEE Int'l Symp. High-Performance Computer Architecture (HPCA '99), 1999.
[14] A. DeOrio, I. Wagner, and V. Bertacco, "Dacota: Post-Silicon Validation of the Memory Subsystem in Multi-Core Designs," Proc. 15th IEEE Int'l Symp. High-Performance Computer Architecture (HPCA '09), 2009.
[15] D. Dill, "The Murphi Verification System," Proc. Eighth Int'l Conf. Computer Aided Verification (CAV '96), 1996.
[16] M. Dubois, C. Scheurich, and F. Briggs, "Memory Access Buffering in Multiprocessors," Proc. 13th ACM/IEEE Int'l Symp. Computer Architecture (ISCA '86), 1986.
[17] C. Fidge, "Timestamps in Message-Passing Systems that Preserve the Partial Ordering," Proc. 11th Australian Computer Science Conf. (ACSC '88), 1988.
[18] S. Fine and A. Ziv, "Coverage Directed Test Generation for Functional Verification Using Bayesian Networks," Proc. 40th Design Automation Conf. (DAC '03), 2003.
[19] K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta, and J. Hennessy, "Memory Consistency and Event Ordering in Scalable Shared-Memory Multi Processors," Proc. 17th ACM/IEEE Int'l Symp. Computer Architecture (ISCA '90), 1990.
[20] P. Gibbons and E. Korach, "The Complexity of Sequential Consistency," Proc. Fourth IEEE Symp. Parallel and Distributed Processing (SPDP '92), 1992.
[21] P. Gibbons and E. Korach, "On Testing Cache-Coherent Shared Memories," Proc. Sixth ACM Symp. Parallel Algorithms and Architectures (SPAA '94), 1994.
[22] P. Gibbons and E. Korach, "Testing Shared Memories," SIAM J. Computing, vol. 26, no. 4, pp. 1208-1244, 1997.
[23] J. Goodman, "Cache Consistency and Sequential Consistency," Technical Report No. 61, SCI Committee, 1989.
[24] G. Gopalakrishnan, Y. Yang, and H. Sivaraj, "QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings," Proc. 16th Int'l Conf. Computer Aided Verification (CAV '04), 2004.
[25] S. Hangal, D. Vahia, C. Manovit, J. Lu, and S. Narayanan, "TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model," Proc. 31st ACM/IEEE Int'l Symp. Computer Architecture (ISCA '04), 2004.
[26] T. Henzinger, S. Qadeer, and S. Rajamani, "Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems," Proc. 11th Int'l Conf. Computer Aided Verification (CAV '99), 1999.
[27] W. Hu, J. Wang, X. Gao, Y. Chen, Q. Liu, and G. Li, "Godson-3: A Scalable Multicore RISC Processor with x86 Emulation," IEEE Micro, vol. 29, no. 2, pp. 17-29, Mar./Apr. 2009.
[28] W. Hu and Y. Chen, "GS464V: A High-Performance Low-Power XPU with 512-Bit Vector Extension," Proc. 22nd IEEE Symp. High Performance Chips (HOTCHIPS '10), 2010.
[29] W. Hu, R. Wang, Y. Chen, B. Fan, S. Zhong, X. Gao, Z. Qi, and X. Yang, "Godson-3B: A 1GHz 40W 8-Core 128GFlops Processor in 65nm CMOS," Proc. 58th IEEE Int'l Solid-State Circuits Conf. (ISSCC '11), 2011.
[30] W. Hu, Y. Chen, T. Chen, C. Qian, and L. Li, "Linear Time Memory Consistency Verification," IEEE Trans. Computers, vol. 61, no. 4, pp. 502-516, http://doi.ieeecomputersociety.org/10.1109 TC.2011.41, Apr. 2012.
[31] L. Lamport, "Time, Clocks, and the Ordering of Events in a Distributed System," Comm. ACM, vol. 21, no. 7, pp. 558-565, 1978.
[32] L. Lamport, "How to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs," IEEE Trans. Computers, vol. C-28, no. 9, pp. 690-691, Sept. 1979.
[33] L. Li, T. Chen, Y. Chen, L. Li, C. Qian, and W. Hu, "Brief Announcement: Program Regularization in Verifying Memory Consistency," Proc. 23rd ACM Symp. Parallel Algorithms and Architectures (SPAA '11), 2011.
[34] J. Ludden, W. Roesner, G. Heiling, J. Reysa, J. Jackson, B. Chu, M. Behm, J. Baumgartner, R. Peterson, J. Abdulhafiz, W. Bucy, J. Klaus, D. Klema, T. Le, F. Lewis, P. Milling, L. McConville, B. Nelson, V. Paruthi, T. Pouarz, A. Romonosky, J. Stuecheli, K. Thompson, D. Victor, and B. Wile, "Functional Verification of the POWER4 Microprocessor and POWER4 Multiprocessor Systems," IBM J. Research and Development, vol. 46, no. 1, pp. 53-76, 2002.
[35] S. Mador-Haim, R. Alur, and M. Martin, "Generating Litmus Tests for Contrasting Memory Consistency Models," Proc. 22nd Int'l Conf. Computer Aided Verification (CAV '10), 2010.
[36] C. Manovit and S. Hangal, "Efficient Algorithms for Verifying Memory Consistency," Proc. 17th ACM Symp. Parallelism in Algorithms and Architecture (SPAA '05), 2005.
[37] C. Manovit and S. Hangal, "Completely Verifying Memory Consistency of Test Program Executions," Proc. 12th IEEE Int'l Symp. High-Performance Computer Architecture (HPCA '06), 2006.
[38] D. Marino, M. Musuvathi, and S. Narayanasamy, "LiteRace: Effective Sampling for Lightweight Data-Race Detection," Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI '09), 2009.
[39] K. McMillan, "Symbolic Model Checking," doctoral dissertation, Carnegie Mellon Univ., 1993.
[40] A. Meixner and D. Sorin, "Dynamic Verification of Sequential Consistency," Proc. 32nd ACM/IEEE Int'l Symp. Computer Architecture (ISCA '05), 2005.
[41] A. Meixner and D. Sorin, "Dynamic Verification of Memory Consistency in Cache-Coherent Multithreaded Computer Architectures," IEEE Trans. Dependable and Secure Computing, vol. 6, no. 1, pp. 18-31, Jan.-Mar. 2009.
[42] S. Park and D. Dill, "An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order)," Proc. Seventh ACM Symp. Parallel Algorithms and Architectures (SPAA '95), 1995.
[43] S. Park, S. Lu, and Y. Zhou, "CTrigger: Exposing Atomicity Violation Bugs from Their Hiding Places," Proc. 14th Int'l Conf. Architectural Support for Programming Languages and Operating Systems (ASPLOS '09), 2009.
[44] M. Plakal, D. Sorin, A. Condon, and M. Hill, "Lamport Clocks: Verifying a Directory Cache-Coherence Protocol," Proc. 10th ACM Symp. Parallel Algorithms and Architectures (SPAA '98), 1998.
[45] A. Roy, S. Zeisset, C. Fleckenstein, and J. Huang, "Fast and Generalized Polynomial Time Memory Consistency Verification," Proc. 18th Int'l Conf. Computer Aided Verification (CAV '06), 2006.
[46] C. Scheurich and M. Dubois, "Correct Memory Operation of Cached-Based Multiprocessors," Proc. 14th ACM/IEEE Int'l Symp. Computer Architecture (ISCA '87), 1987.
[47] O. Shacham, M. Wachs, A. Solomatnikov, A. Firoozshahian, S. Richardson, and M. Horowitz, "Verification of Chip Multiprocessor Memory Systems Using a Relaxed Scoreboard," Proc. 41st ACM/IEEE Int'l Symp. Microarchitecture (MICRO '08), 2008.
[48] D. Shasha and M. Snir, "Efficient and Correct Execution of Parallel Programs that Share Memory," ACM Trans. Programming Languages and Systems, vol. 10, no. 2, pp. 282-312, 1988.
[49] D. Victor, J. Ludden, R. Peterson, B. Nelson, W. Sharp, J. Hsu, B. Chu, M. Behm, R. Gott, A. Romonosky, and S. Farago, "Functional Verification of the POWER5 Microprocessor and POWER5 Multiprocessor Systems," IBM J. Research and Development, vol. 49, no. 4, pp. 541-554, 2005.
94 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool