Yatin Manerkar will present his General Exam on Monday, January 11, 2016 at 2pm in CS 302.
The members of his committee are: Margaret Martonosi (adviser), Aarti Gupta, and David August.
Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below.
Title:
CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface
Abstract:
Memory consistency models define the rules that govern which values are visible to instructions of parallel programs. Today's multiprocessors are complex machines, and this complexity is set to increase in the future with increases in heterogeneity and system scale. As such, it can be difficult to comprehensively verify that a microarchitecture correctly implements the consistency model that it is supposed to. My research aims to conduct such microarchitectural consistency verification in a comprehensive and yet tractable manner. My work recently focused on bugs that occur due to the interaction of coherence and consistency at the coherence-consistency interface (CCI) of a microarchitecture. These bugs can be very subtle and difficult to detect. In this talk, I will discuss CCICheck, a methodology and tool for verifying a microarchitecture's implementation of a consistency model in a CCI-aware manner. CCICheck builds on the microarchitectural verification effort of the PipeCheck tool and methodology, but extends and generalizes it to be able to handle a much wider range of microarchitectures and ordering constraints. My work has used CCICheck to tractably model a variety of CCI scenarios, including partial incoherence, lazy coherence, and coherence protocol optimizations.
Reading List:
1. John L. Hennessy and David A. Patterson. 2007. Computer Architecture, Fourth Edition: A Quantitative Approach. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.
2. Daniel J. Sorin, Mark D. Hill, and David A. Wood. 2011. A Primer on Memory Consistency and Cache Coherence (1st ed.). Morgan & Claypool Publishers.
3. Daniel Lustig, Michael Pellauer, and Margaret Martonosi, “PipeCheck: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models”, 47th International Symposium on Microarchitecture (MICRO), Cambridge, UK, December 2014.
4. Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface. The 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), December 2015.
5. Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Comput. 28, 9 (September 1979), 690-691.
6. Sarita V. Adve and Kourosh Gharachorloo. "Shared Memory Consistency Models: A Tutorial", Western Research Laboratory, Tech. Rep. 95/7, September 1995.
7. Hans-J. Boehm and Sarita V. Adve. 2008. Foundations of the C++ concurrency memory model. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation (PLDI '08). ACM, New York, NY, USA, 68-78.
8. Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July 2014), 74 pages.
9. Albert Meixner and Daniel J. Sorin, "Dynamic Verification of Memory Consistency in Cache-Coherent Multithreaded Computer Architectures," in Dependable and Secure Computing, IEEE Transactions on , vol.6, no.1, pp.18-31, Jan.-March 2009.
10. S. Hangal, D. Vahia, C. Manovit, J.-Y.J Lu, S. Narayanan, "TSOtool: a program for verifying memory systems using the memory consistency model," in Computer Architecture, 2004. Proceedings. 31st Annual International Symposium on , vol., no., pp.114-123, 19-23 June 2004.
