This Article 
 Bibliographic References 
 Add to: 
Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking
August 2003 (vol. 14 no. 8)
pp. 730-741

Abstract—The memory model of a shared-memory multiprocessor is a contract between the designer and the programmer of the multiprocessor. A memory model is typically implemented by means of a cache-coherence protocol. The design of this protocol is one of the most complex aspects of multiprocessor design and is consequently quite error-prone. However, it is imperative to ensure that the cache-coherence protocol satisfies the shared-memory model. This paper presents a novel technique based on model checking to tackle this difficult problem for the important and well-known shared-memory model of sequential consistency. Surprisingly, verifying sequential consistency is undecidable in general, even for finite-state cache-coherence protocols. The key insight of this paper is that, in practice, cache-coherence protocols satisfy the properties of causality and data independence. Causality is the property that values of read events flow from values of write events. Data independence is the property that all traces can be generated by renaming data values from traces where the written values are pairwise distinct. We show that, if a causal and data independent system also has the property that the logical order of write events to each location is identical to their temporal order, then sequential consistency is decidable. We present a novel model checking algorithm to verify sequential consistency on such systems for a finite number of processors and memory locations and an arbitrary number of data values.

[1] Y. Afek, G. Brown, and M. Merritt, “Lazy Caching,” ACM Trans. Programming Languages and Systems, vol. 15, no. 1, pp. 182-205, Jan. 1993.
[2] R. Alur, K.L. McMillan, and D. Peled, Model-Checking of Correctness Conditions for Concurrent Objects Proc. 11th Ann. IEEE Symp. Logic in Computer Science, pp. 219-228, 1996.
[3] T. Arons, Using Timestamping and History Variables to Verify Sequential Consistency Proc. CAV 01: Computer-Aided Verification Conf., G. Berry, H. Comon, and A. Finkel, eds., pp. 423-435, 2001.
[4] E.E. Bilir, R.M. Dickson, Y. Hu, M. Plakal, D.J. Sorin, M.D. Hilland, D.A. Wood, “Multicast Snooping: A New Coherence Method Using a Multicast Address Network,” Proc. 26th Ann. Int'l Symp. Computer Architecture, pp. 294-304, May 1999.
[5] L.A. Barroso et al., "Piranha: A Scalable Architecture Based on Single-Chip Multiprocessing," Proc. 27th ACM Int'l Symp. Computer Architecture, ACM Press, 2000, pp. 282-293.
[6] E.M. Clarke and E.A. Emerson, "Synthesis of synchronization skeletons for branching time temporal logic," Logic of Programs: Workshop, Lecture notes in Computer Science. vol. 131. Yorktown Heights, N. Y.: Springer-Verlag, May 1981.
[7] E.M. Clarke,O. Grumberg,H. Hiraishi,S. Jha,D.E. Long,K.L. McMillan,, and L.A. Ness,“Verification of the Futurebus+ cache coherence protocol,” Proc. Eleventh Int’l Symp. Computer Hardware Description Languages and Their Applications, Apr. 1993.
[8] A.E. Condon and A.J. Hu, Automatable Verification of Sequential Consistency Proc. 13th ACM Symp. Parallel Algorithms and Architectures, pp. 113-121, 2001.
[9] Alpha Architecture Committee, Alpha Architecture Reference Manual. Digital Press, 1998.
[10] G. Delzanno, Automatic Verification of Parameterized Cache Coherence Protocols CAV 2000: Computer Aided Verification, E.A. Emerson and A.P. Sistla, eds., pp. 53-68, 2000.
[11] A.T. Eiriksson and K.L. McMillan, “Using Formal Verification/Analysis Methods on the Critical Path in Systems Design: A Case Study,” Proc. Computer Aided Verification Conf., pp. 367-380, 1995.
[12] P.B. Gibbons and E. Korach, Testing Shared Memories SIAM J. Computing, vol. 26, no. 4, pp. 1208-1244, 1997.
[13] M. Glusman and S. Katz, Extending Memory Consistency of Finite Prefixes to Infinite Computations Proc. CONCUR 01 Conf.: Theories of Concurrency, K.G. Larsen and M. Nielsen, eds., pp. 411-425, 2001.
[14] T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems,” Lecture Notes in Computer Science, pp. 301-315, 1999.
[15] C.N. Ip and D.L. Dill, “Better Verification through Symmetry,” Formal Methods in System Design, vol. 9, 1996.
[16] M. Heinrich et al. “The Stanford FLASH Multiprocessor,” Proc. 21th Int'l Symp. Computer Architecture, pp. 302-313, April 1994.
[17] S. Katz and D. Peled, Verification of Distributed Programs Using Representative Interleaving Sequences Distributed Computing, vol. 6, no. 2, pp. 107-120, 1992.
[18] L. Lamport, "Time, clocks and the ordering of events in a distributed system," Comm. ACM, vol. 21, no. 7, pp. 558-565, July 1978.
[19] L. Lamport, How to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs IEEE Trans. Computers, vol. 28, no. 9, pp. 690-691, 1979.
[20] L. Lamport and S. Owicki, "The Temporal Logic of Actions," ACM Trans. Programming Languages and Systems, vol. 16, pp. 872-923, May 994.
[21] A. Globus, C. Levit, and T. Lasinski, "A Tool for Visualizing the Topology of Three-Dimensional Vector Fields," Proc. IEEE Visualization '91, pp. 33-40, 1991.
[22] D. Lenoski et al., "The directory-based cache coherence protocol for the dash multiprocessor," Proc. 17th Int'l Symp. Computer Architecture,Los Alamitos, Calif., pp. 148-159, 1990.
[23] P. Ladkin, L. Lamport, B. Olivier, and D. Roegel, Lazy Caching in TLA Distributed Computing, vol. 12, nos. 2/3, pp. 151-174, 1999.
[24] K.L. McMillan, Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking Proc. CHARME 01: IFIP Working Conf. Correct Hardware Design and Verification Methods, 2001.
[25] K.L. McMillan and J. Schwalbe, Formal Verification of the Encore Gigamax Cache Consistency Protocol Proc. Int'l Symp. Shared Memory Multiprocessors, pp. 242-251, 1991.
[26] R.P. Nalumasu, Formal Design and Verification Methods for Shared Memory Systems PhD thesis, Univ. of Utah, 1999.
[27] R. Nalumasu, R. Ghughal, A. Mokkedem, and G. Gopalakrishnan, “The `Test Model-checking' Approach to the Verification of Formal Memory Models of Multiprocessors,” Proc. Computer Aided Verification, 10th Int'l Conf., A.J. Hu and M.Y. Vardi, eds., pp. 464-476, June 1998.
[28] S. Owre, J.M. Rushby, and N. Shankar, "PVS: A Prototype Verification System," E. Kapur, ed., Proc. 11th Conf. Automated Deduction, Lecture Notes in Computer Science 607. Springer-Verlag, 1992.
[29] F. Pong and M. Dubois, "A New Approach for the Verification of Cache Coherence Protocols," IEEE Trans. Parallel and Distributed Systems, vol. 6, no. 8, pp. 773-787, Aug. 1995.
[30] S. Park and D.L. Dill, Protocol Verification by Aggregation of Distributed Transactions Proc. CAV 96 Conf.: Computer Aided Verification, R. Alur and T.A. Henzinger, eds., pp. 300-310, 1996.
[31] M. Plakal, D.J. Sorin, A.E. Condon, and M.D. Hill, “Lamport Clocks: Verifying a Directory Cache-Coherence Protocol,” Proc. 10th ACM Symp. Parallel Algorithms and Architectures, pp. 67-76, June 1998.
[32] J.-P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Int'l Symp. Programming, pp. 337-351, Lecture Notes in Computer Science 137, Springer-Verlag, Apr. 1982.
[33] The SPARC Architecture Manual, D.L. Weaver and T. Germond, eds. Prentice Hall, 1999.
[34] P. Wolper, "Expressing Interesting Properties of Programs in Propositional Temporal Logic," Proc. 13th ACM Symp. Principles of Programming Languages, pp. 148-193,St. Petersburg, Fla., Jan. 1986.
[35] Y. Yu, P. Manolios, and L. Lamport, Model Checking TLA+ Specifications Proc. CHARME 99: IFIP Working Conf. Correct Hardware Design and Verification Methods, pp. 54-66, 1999.

Index Terms:
Logic design, verification, multiprocessors, model checking, specifying and verifying and reasoning about programs.
Shaz Qadeer, "Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking," IEEE Transactions on Parallel and Distributed Systems, vol. 14, no. 8, pp. 730-741, Aug. 2003, doi:10.1109/TPDS.2003.1225053
Usage of this product signifies your acceptance of the Terms of Use.