MTraceCheck: Validating Non-Deterministic Behavior of Memory Consistency Models in Post-Silicon Validation

Abstract

This work presents a minimally-intrusive, high-performance, post-silicon validation framework for validating memory consistency in multi-core systems. Our framework generates constrained-random tests that are instrumented with observability-enhancing code for memory consistency verification. For each test, we generate a set of compact signatures reflecting the memory-ordering patterns observed over many executions of the test, with each of the signatures corresponding to a unique memory-ordering pattern. We then leverage an efficient and novel analysis to quickly determine if the observed execution patterns represented by each unique signature abide by the memory consistency model. Our analysis derives its efficiency by exploiting the structural similarities among the patterns observed.

We evaluated our framework, MTraceCheck, on two platforms: an x86-based desktop and an ARM-based SoC platform, both running multi-threaded test programs in a bare-metal environment. We show that MTraceCheck reduces the perturbation introduced by the memory-ordering monitoring activity by 93% on average, compared to a baseline register flushing approach that saves the register's state after each load operation. We also reduce the computation requirements of our consistency checking analysis by 81% on average, compared to a conventional topological sorting solution. We finally demonstrate the effectiveness of MTraceCheck on buggy designs, by evaluating multiple case studies where it successfully exposes subtle bugs in a full-system simulation environment.

References

1. Allon Adir, Maxim Golubev, Shimon Landa, Amir Nahir, Gil Shurek, Vitali Sokhin, and Avi Ziv. 2011. Threadmill: A Post-Silicon Exerciser for MultiThreaded Processors. In Proceedings of the 48th Design Automation Conference. 860--865.
2. Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared Memory Consistency Models: A Tutorial. Computer 29, 12 (1996), 66--76.
3. Sarita V. Adve and Mark D. Hill. 1990. Weak Ordering--A New Definition. In Proceedings of the 17th Annual International Symposium on Computer Architecture. 2--14.
4. Jade Alglave. 2012. A Formal Hierarchy of Weak Memory Models. Formal Methods in System Design 41, 2 (2012), 178--210.
5. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in Weak Memory Models. In Computer Aided Verification: 22nd International Conference, CAV 2010. 258--272.
6. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011. Litmus: Running Tests Against Hardware. In Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, TACAS 2011. 41--44.
7. ARM. 2009. Barrier Litmus Tests and Cookbook.
8. ARM. 2011. Embedded Trace Macrocell Architecture Specification.
9. ARM. 2012. ARM Architecture Reference Manual -- ARMv7-A and ARMv7-R edition.
10. Arvind and Jan-Willem Maessen. 2006. Memory Model = Instruction Reordering + Store Atomicity. In Proceedings of the 33rd Annual International Symposium on Computer Architecture. 29--40.
11. Thomas Ball and James R. Larus. 1996. Efficient Path Profiling. In Proceedings of the 29th Annual ACM/IEEE International Symposium on Microarchitecture. 46--57.
12. Nathan Binkert, Bradford Beckmann, Gabriel Black, Steven K. Reinhardt, Ali Saidi, Arkaprava Basu, Joel Hestness, Derek R. Hower, Tushar Krishna, Somayeh Sardashti, Rathijit Sen, Korey Sewell, Muhammad Shoaib, Nilay Vaish, Mark D. Hill, and David A. Wood. 2011. The gem5 Simulator. ACM SIGARCH Computer Architecture News 39, 2 (2011), 1--7.
13. Harold W. Cain, Mikko H. Lipasti, and Ravi Nair. 2003. Constraint Graph Analysis of Multithreaded Programs. In Proceedings of the 12th International Conference on Parallel Architectures and Compilation Techniques. 4--14.
14. Kaiyu Chen, Sharad Malik, and Priyadarsan Patra. 2008. Runtime Validation of Memory Ordering Using Constraint Graph Checking. In 2008 IEEE 14th International Symposium on High Performance Computer Architecture. 415--426.
15. Yunji Chen, Lei Li, Tianshi Chen, Ling Li, Lei Wang, Xiaoxue Feng, and Weiwu Hu. 2012. Program Regularization in Memory Consistency Verification. IEEE Transactions on Parallel and Distributed Systems 23, 11 (2012), 2163--2174.
16. Yunji Chen, Yi Lv, Weiwu Hu, Tianshi Chen, Haihua Shen, Pengyu Wang, and Hong Pan. 2009. Fast Complete Memory Consistency Verification. In 2009 IEEE 15th International Symposium on High Performance Computer Architecture. 381--392.
17. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). The MIT Press.
18. Das U-Boot -- the universal boot loader. Retrieved April 30, 2017 from http://www.denx.de/wiki/U-Boot
19. Marco Elver and Vijay Nagarajan. 2016. McVerSi: A Test Generation Framework for Fast Memory Consistency Verification in Simulation. In 2016 IEEE International Symposium on High Performance Computer Architecture. 618--630.
20. Nikos Foutris, Dimitris Gizopoulos, Mihalis Psarakis, Xavier Vera, and Antonio Gonzalez. 2011. Accelerating Microprocessor Silicon Validation by Exposing ISA Diversity. In Proceedings of the 44th Annual IEEE/ACM International Symposium on Microarchitecture. 386--397.
21. Nikos Foutris, Dimitris Gizopoulos, Xavier Vera, and Antonio Gonzalez. 2013. Deconfigurable Microprocessor Architectures for Silicon Debug Acceleration. In Proceedings of the 40th Annual International Symposium on Computer Architecture. 631--642.
22. gem5 mercurial repository host. Retrieved April 30, 2017 from http://repo.gem5.org
23. GNU coreutils version 8.25. Retrieved April 30, 2017 from http://ftp.gnu.org/gnu/coreutils/
24. Sudheendra Hangal, Durgam Vahia, Chaiyasit Manovit, Juin-Yeu J. Lu, and Sridhar Narayanan. 2004. TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model. In Proceedings of the 31st Annual International Symposium on Computer Architecture. 114--123.
25. Intel. 2015. Intel 64 and IA-32 Architectures Software Developer's Manual.
26. k-medoids algorithm. Retrieved April 30, 2017 from https://en.wikipedia.org/wiki/K-medoids
27. Jagannath Keshava, Nagib Hakim, and Chinna Prudvi. 2010. Post-Silicon Validation Challenges: How EDA and Academia Can Help. In Proceedings of the 47th Design Automation Conference. 3--7.
28. Rakesh Komuravelli, Sarita V. Adve, and Ching-Tsun Chou. 2014. Revisiting the Complexity of Hardware Cache Coherence and Some Implications. ACM Transactions on Architecture Code Optimization 11, 4 (2014), 37:1--37:22.
29. Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (1979), 690--691.
30. Penny Li, Jinuk L. Shin, Georgios Konstadinidis, Francis Schumacher, Venkat Krishnaswamy, Hoyeol Cho, Sudesna Dash, Robert Masleid, Chaoyang Zheng, Yuanjung D. Lin, Paul Loewenstein, Heechoul Park, Vijay Srinivasan, Dawei Huang, Changku Hwang, Wenjay Hsu, and Curtis McAllister. 2015. A 20nm 32-Core 64MB L3 Cache SPARC M7 Processor. In 2015 IEEE International Solid-State Circuits Conference - (ISSCC) Digest of Technical Papers. 1--3.
31. David Lin, Ted Hong, Yanjing Li, Eswaran S, Sharad Kumar, Farzan Fallah, Nagib Hakim, Donald S. Gardner, and Subhasish Mitra. 2014. Effective Post-Silicon Validation of System-on-Chips Using Quick Error Detection. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 33, 10 (2014), 1573--1590.
32. Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2014. PipeCheck: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models. In Proceedings of the 47th Annual IEEE/ACM International Symposium on Microarchitecture. 635--646.
33. Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi. 2015. ArMOR: Defending Against Memory Consistency Model Mismatches in Heterogeneous Architectures. In Proceedings of the 42nd Annual International Symposium on Computer Architecture. 388--400.
34. Sela Mador-Haim, Rajeev Alur, and Milo M.K. Martin. 2010. Generating Litmus Tests for Contrasting Memory Consistency Models. In Computer Aided Verification: 22nd International Conference, CAV 2010. 273--287.
35. Biruk W. Mammo, Valeria Bertacco, Andrew DeOrio, and Ilya Wagner. 2015. Post-Silicon Validation of Multiprocessor Memory Consistency. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 34, 6 (2015), 1027--1037.
36. Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2015. CCICheck: Using μhb Graphs to Verify the Coherence-Consistency Interface. In Proceedings of the 48th International Symposium on Microarchitecture. 26--37.
37. Luc Maranget, Susmit Sarkar, and Peter Sewell. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. Retrieved April 30, 2017 from http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf
38. Albert Meixner and Daniel J. Sorin. 2009. Dynamic Verification of Memory Consistency in Cache-Coherent Multithreaded Computer Architectures. IEEE Transactions on Dependable and Secure Computing 6, 1 (2009), 18--31.
39. Subhasish Mitra, Sanjit A. Seshia, and Nicola Nicolici. 2010. Post-Silicon Validation Opportunities, Challenges and Recent Advances. In Proceedings of the 47th Design Automation Conference. 12--17.
40. Eberle A. Rambo, Olav P. Henschel, and Luiz C. V. dos Santos. 2011. Automatic Generation of Memory Consistency Tests for Chip Multiprocessing. In 18th IEEE International Conference on Electronics, Circuits, and Systems. 542--545.
41. Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, and John C. Huang. 2006. Fast and Generalized Polynomial Time Memory Consistency Verification. In Computer Aided Verification: 18th International Conference, CAV 2006. 503--516.
42. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Z. Nardelli, and Magnus O. Myreen. 2010. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Commun. ACM 53, 7 (2010), 89--97.
43. Ofer Shacham, Megan Wachs, Alex Solomatnikov, Amin Firoozshahian, Stephen Richardson, and Mark Horowitz. 2008. Verification of Chip Multiprocessor Memory Systems Using a Relaxed Scoreboard. In Proceedings of the 41st Annual IEEE/ACM International Symposium on Microarchitecture. 294--305.
44. Daniel J. Sorin, Mark D. Hill, and David A. Wood. 2011. A Primer on Memory Consistency and Cache Coherence (1st ed.). Morgan & Claypool Publishers.
45. The Coq proof assistant. Retrieved April 30, 2017 from https://coq.inria.fr
46. Ilya Wagner and Valeria Bertacco. 2008. Reversi: Post-Silicon Validation System for Modern Microprocessors. In IEEE International Conference on Computer Design. 307--314.
47. David Weaver and Tom Germond. 1994. The SPARC Architectural Manual (Version 9). Prentice-Hall, Inc.
48. Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. 2010. Fractal Consistency: Architecting the Memory System to Facilitate Verification. IEEE Computer Architecture Letters 9, 2 (2010), 61--64.

Index Terms

• Computer systems organization

  • Architectures

    • Parallel architectures

      • Multicore architectures

• Hardware

  • Hardware validation

    • Post-manufacture validation and debug

      • Bug detection, localization and diagnosis