Abstract
A specification and verification methodology for Distributed Shared Memory consistency protocols implementing weak shared memory consistency models is proposed. Our approach uniformly describes a wide range of weak memory models in terms of a single concept—the visibility order of loads, stores, and synchronization operations, as perceived by all the processors. A given implementation is correct with respect to a weak memory model if it produces executions satisfying the visibility order for that memory model. Given an implementation, the designer annotates it with events from the visibility order, and runs reachability analysis to verify it against a specification that is also similarly annotated. A specification is obtained in two stages: first, the designer reverse engineers an intermediate abstraction from the implementation by replacing the coherence network with a logically equivalent concurrent data structure. The replacement is selected in a standard way, depending almost exclusively on the memory model. Verification of the intermediate abstraction against a visibility order specification can be accomplished using theorem-proving. The methodology was applied to four snoopy-bus protocols implementing aspects of the Alpha and Itanium memory models, with encouraging results.
This work was supported by NSF Grants CCR-9987516 and CCR-0081406
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
The ASCI White Computer http://www.llnl.gov/asci/.
The Sun MAJC Microarchitecture http://www.sun.com/microelectronics/MAJC/.
The IBM Power4 Microarchitecture http://www-1.ibm.com/servers/eserver/pseries/hardware/whitepapers/power4.html.
L.A. Barroso, K. Gharachoroloo, R. McNamara, A. Nowatzyk, S. Qadeer, B. Sano, S. Smith, R. Stets, and B. Verghese, “Piranha: A scalable architecture based on single-chip multiprocessing,” in 27th International Symposium on Computer Architecture (ISCA), June 2000.
Mark D. Hill, “Multiprocessors should support simple memory-consistency models,” IEEE Computer, vol. 31, no. 8, pp. 28–34, 1998.
David L. Weaver and Tom Germond, The SPARC Architecture Manual-Version 9, P T R Prentice-Hall, Englewood Cliffs, NJ 07632, USA, 1994.
Intel, The IA-64 Architecture Software Developer’s Manual Vol. 2 rev. 1.1: Itanium (TM); System Architecture, Intel, 2000, Volume 2, Chapter 13, “Coherence and MP Ordering.” http://developer.intel.com/design/ia-64/downloads/24531802.htm.
Sarita V. Adve and Kourosh Gharachorloo, “Shared memory consistency models: A tutorial,” Computer, vol. 29, no. 12, pp. 66–76, Dec. 1996.
M. Ahamad, R. A. Bazzi, R. John, P. Kohli, and G. Neiger, “The power of processor consistency (extended abstract),” in Proc. of the 5th ACM Annual Symp. on Parallel Algorithms and Architectures (SPAA’93), June 1993, pp. 251–260.
Leslie Lamport, “How to make a multiprocessor computer that correctly executes multiprocess programs,” IEEE Transactions on Computers, vol. 9, no. 29, pp. 690–691, 1979.
Leslie Lamport, “The wildfire challenge problem,” http://research.microsoft.com/users/lamport/tla/wildfire-challenge.html.
Gil Neiger, “ 2001, http://www.cs.utah.edu/mpv/papers/neiger/fmcad2001.pdf.
Anne Condon, Mark Hill, Manoj Plakal, and David Sorin, ”Using lamport clocks to reason about relaxed memory models,“ in Proceedings of the Fifth International Symposium On High Performance Computer Architecture (HPCA-5), Jan. 1999.
Martín Abadi and Leslie Lamport, “The existence of refinement mappings,” Theoretical Computer Science, vol. 82, no. 2, pp. 253–284, 1991.
Rajeev Alur, Ken McMillan, and Doron Peled, “Model-checking of correctness conditions for concurrent objects,” in 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 1996, pp. 219–228.
Hemanthkumar Sivaraj, “Parallel and distributed model checking,” M.S. thesis, School of Computing, University of Utah, 2002, In progress.
Ulrich Stern and David Dill, “Parallelizing the Vlunp verifier,” Formal Methods in System Design, vol. 18, no. 2, pp. 117–129, 2001, (Journal version of their CAV 1997 paper).
Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, “The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors,” in Computer Aided Verification98, Alan J. Hu and Moshe Y. Vardi, Eds., Vancouver, BC, Canada, June/July 1998, vol. 1427 of Lecture Notes in Computer Science, pp. 464–476, Springer-Verlag.
Seungjoon Park, Computer Assisted Analysis of Multiprocessor Memory Systems, Ph.D. thesis, Stanford University, jun 1996, Department of Computer Science.
Prosenjit Chatterjee, ” Tool available at http://www.cs.utah.edu/formalverification/ESGtool.
G. J. Holzmann, “The model checker spin,” IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279–295, May 1997, Special issue on Formal Methods in Software Practice.
Leslie Lamport, “Time, clocks, and the ordering of events in a distributed program,” Communications of the ACM, vol. 21, no. 7, pp. 558–565, 1978.
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark Tuttle, and Yuan Yu, “Cache coherence verification with tla+,” in World Congress on Formal Methods, 1999, vol. LNCS 1709, pp. 1871–1872.
Thomas Henzinger, Shaz Qadeer, and Sriram Rajamani, “Verifying sequential consistency on shared-memory multiprocessor systems,” in Computer Aided Verification99, Nicolas Halbwachs and Doron Peled, Eds., Trento, Italy, July 1999, vol. 1633 of Lecture Notes in Computer Science, pp. 301–315, Springer-Verlag.
Shaz Qadeer, ”Verifying sequential consistency on shared-memory multiprocessors by model checking,“ Tech. Rep., SRC, Dec. 2001, Research Report 176.
Michael Merritt, “Guest editorial: Special issue on shared memory systems,” Distributed Computing, vol. 12, no. 12, pp. 55–56, 1999.
Jason F. Cantin, Mikko H. Lipasti, and James E. Smith, “Dynamic verification of cache coherence protocol,” in Workshop on Memory Performance Issues, in conjunction with ISCA, June 2001.
W. W. Collier, Reasoning About Parallel Architectures, Prentice-Hall, Englewood Cliffs, NJ, 1992.
Rajnish Ghughal and Ganesh Gopalakrishnan, “Verification methods for weaker shared memory consistency models,” in Proc. of the workshop FMPPTA (Formal Methods for Parallel Programming: Theory and Applications), Cancun, Mexico. LNCS # 1800, José Rolim et al., Ed., May 2000, pp. 985–992.
Rajnish Ghughal, “Test model-checking approach to verification of formal memory models,” M.S. thesis, Department of Computer Science, University of Utah, 1999, Also available from http://www.cs.utah.edu/formal_verification.
Christoph Scheurich, Access Ordering and Coherence in Shared Memory Multiprocessors, Ph.D. thesis, University of Southern California, May 1989.
D. Sorin, M. Plakal, A. E. Condon, M. D. Hill, M. M. Martin, and D. A. Wood, “Specifying and verifying a broadcast and a multicast snooping cache coherence protocol,” Tech. Rep. #1412, Computer Sciences Department, U. Wisconsin, Madison, Mar. 2000.
Prosenjit Chatterjee, “Formal specification and verification of memory consistency models of shared memory multiprocessors,” M.S. thesis, Department of Computer Science, University of Utah, 2002, Also available from http://www.cs.utah.edu/formal_verification
Leslie Lamport, “How to make a correct multiprocess program execute correctly on a multiprocessor,” Tech. Rep., Digital Equipment Corporation, Systems Research Center, Feb. 1993.
Richard L. Sites, Alpha Architecture Reference Manual, Digital Press, 1992.
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), May 1990, pp. 15–26.
R. J. Lipton and J. S. Sandberg, “Pram: A scalable shared memory,” Tech. Rep. CS-TR-180-88, Dept. of Computer Science, Princeton University, Sept. 1988.
P. W. Hutto and M. Ahamad, “Slow memory: Weakening consistency to enhance concurrency in distributed shared memories,” in Proc. of the 10th Int’l Conf. on Distributed Computing Systems (ICDCS-10), May 1990, pp. 302–311.
Prosenjit Chatterjee and Ganesh Gopalakrishnan, “Towards a formal model of shared memory consistency for intel itanium,” in International Conference on Computer Aided Design, Austin, USA, 2001.
A. Singhal, D. Broniarczyk, F Cerauskis, J. Price, L. Yuan, C. Cheng, D. Doblar, S. Fosth, N. Agarwal, K. Harvey, E. Hangersten, and B. Liencres, “Gigaplane: A high performance bus for large smps,” in Proc. of the 4th Annual Symposium on High Performance Interconnects at Stanford University, 1996, pp. 41–52.
Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, “The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors,” in Computer Aided Verification, Alan J. Hu and Moshe Y. Vardi, Eds., Vancouver, BC, Canada, June 1998, vol. 1427 of Lecture Notes in Computer Science, pp. 464–476, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, P., Gopalakrishnan, G. (2002). A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_18
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive