1/11 and 1/18:

Presenters: Ganesh Gopalakrishnan and Xiaofang Chen.

Slides for 1/11 are HERE.

Slides for 1/18 are HERE.

The goal is to understand the basics of cache coherence, sequential consistency, and verification techniques.

• Papers in a special issue in Distributed Computing 1999 on Sequential consistency are available HERE. We shall mainly read Rob Gerth's paper in gerth.pdf.
• Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, 9(29):690--691, 1979.
  
  
• Xiaowei Shen and Arvind. Specification of memory models and design of provably correct cache coherence protocols. Technical report, Massachusetts Institute of Technology, January 1997. Computation Structures Group, Memo 398.
  
  
• Ali Sezgin and Ganesh Gopalakrishnan, ``On the decidability of shared memory consistency verification,'' Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2005, 199-208. (We show alternative views of the Alur, Peled, McMillan work.)
  [.pdf] [.bib]
  
  
• Ali Sezgin and Ganesh Gopalakrishnan, ``On the definition of sequential consistency,'' Inf. Process. Lett. 96(6): 193-196 (2005).
  A preliminary version [.pdf]
  
  
• Jesse Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, and Zhichuan Zhang. Automatic verification of sequential consistency for unbounded addresses and data values. In CAV (Computer Aided Verification), pages 427--439, 2004. LNCS 3113.
  
  
• Xiaofang Chen, Yu Yang, Michael DeLisi, Ganesh Gopalakrishnan, and Ching-Tsun Chou, ``Hierarchical Cache Coherence Protocol Verification One Level at a Time Through Assume Guarantee,'' IEEE Int'l High Level Design Validation and Test Workshop (HLDVT), 2007, 107-114.
  [.pdf] [.bib] [.ppt] [Hierarchical Protocol Benchmarks of This Paper in Murphi]

1/25 and 2/1:

Presenters: Subodh Sharma and Sarvani Vakkalanka

The goal is to understand work on weak memory models and techniques to preserve the SC view.

• M. Dubois, C. Scheurich, and F. Briggs. Synchronization, coherence and event ordering in multiprocessors. IEEE Computer, 21(2):9--21, February 1988.
  
  
• Sarita V. Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, December 1996.
  
  
• Mark D. Hill. Multiprocessors should support simple memory consistency models. IEEE Computer, 25:28--34, August 1998.
  
  
• S. V. Adve and M. D. Hill. Weak ordering---a new definition. In Proc. of the 17th Annual Int'l Symp. on Computer Architecture (ISCA'90), pages 2--14, May 1990.
  
  
• K. Gharachorloo, D. E. Lenoski, J. Laudon, P. Gibbons, A. Gupta, and J. L. Hennessy. Memory consistency and event ordering in scalable shared-memory multiprocessors. In Proc. of the 17th Annual Int'l Symp. on Computer Architecture (ISCA'90), pages 15--26, May 1990.
  
  
• Dennis Shasha and Mark Snir. Efficient and correct execution of parallel programs. ACM TOPLAS, 10(2), 1988.
  
  
• Zehra Sura, Xing Fang, Chi-Leung Wong, Samuel P. Midkiff, Jaejin Lee, and David Padua. Compiler techniques for high performance sequentially consistent java programs. In Proceedings of the 10th ACM SIGPLAN symposium on Principles and practice of parallel programming (PPoPP), pages 2--13, 2005.

2/8 and 2/15:

Presenters: Anh Vo and Guodong Li

The goal is to see the definitions of some weak memory models that have been defined using various approaches.

• Prosenjit Chatterjee and Ganesh Gopalakrishnan, ``Towards a Formal Model of Shared Memory Consistency for Intel Itanium,'' International Conference on Computer Design, Austin, TX, October 2001, 515-518.
  [Prosenjit's Directory]
  
  
• Lisa Higham, LillAnne Jackson, and Jalal Kawash. What is itanium memory consistency from the programmer's point of view? Electronic Notes in Theoretical Computer Science (ENTCS), 174:63--84, August 2006. Proceedings of the Thread Verification Workshop (TV 2006), Seattle, WA, USA. (Points out a flaw in our ICCD 2001 model.)
  
  
• Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind, ``Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT,'' Correct Hardware Design and Verification Methods, LNCS 2860, L'Aquila, Italy, 2003 pp. 81-95.
  [.pdf] [.ppt]
  
  
• Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind, ``Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models,'' International Parallel and Distributed Processing Symposium, 2004.
  [.pdf]
  
  
• (Ideally read the journal paper based on MPEC that is being written) Ganesh Gopalakrishnan, Yue Yang, and Hemanthkumar Sivaraj, ``QB or not QB: An Efficient Execution Verification Tool for Memory Orderings,'' Computer Aided Verification (CAV 2004), pp. 401-413, LNCS 3114.
  [.pdf] [.bib] [.ppt] [Itanium Spec of Intel] [Itanium HOL Spec Undelying MPEC]
  
  
• Greg Bronevetsky and Bronis de Supinski. Complete formal specification of the openmp memory model. International Journal of Parallel Programming, 35(4):335--392, August 2007.
  
  
• Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In Principles of Programming Languages, pages 378--391, 2005.

2/22, 2/29, and 3/7:

Presenters: Yu Yang and Ganesh Gopalakrishnan

This is a 70-page paper, so should be nice juicy reading for a while.

• Kier Fraser and Tim Harris. Concurrent programming without locks. ACM Transactions on Computer Systems, 25(2), May 2007.

3/14:

3/28:

4/4:

4/11:

4/18:

This document was translated from L^AT_EX by H^EV^EA.