Abstract
We study the problem of formally verifying shared memory multiprocessor executions against memory consistency models—an important step during post-silicon verification of multiprocessor machines. We employ our previously reported style of writing formal specifications for shared memory models in higher order logic (HOL), obtaining intuitive as well as modular specifications. Our specification consists of a conjunction of rules that constrain the global visibility order. Given an execution to be checked, our algorithm generates Boolean constraints that capture the conditions under which the execution is legal under the visibility order. We initially took the approach of specializing the memory model HOL axioms into equivalent (for the execution to be checked) quantified boolean formulae (QBF). As this technique proved inefficient, we took the alternative approach of converting the HOL axioms into a program that generates a SAT instance when run on an execution. In effect, the quantifications in our memory model specification were realized as iterations in the program. The generated Boolean constraints are satisfiable if and only if the given execution is legal under the memory model. We evaluate two different approaches to encode the Boolean constraints, and also incremental techniques to generate and solve Boolean constraints. Key results include a demonstration that we can handle executions of realistic lengths for the modern Intel Itanium memory model. Further research into proper selection of Boolean encodings, incremental SAT checking, efficient handling of transitivity, and the generation of unsatisfiable cores for locating errors are expected to make our technique practical.
Supported by NSF Grant CCR-0081406 and SRC Contract 1031.001
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer 29(12), 66–76 (1996)
A Formal Specification of Intel(R) Itanium(R) Processor Family Memory Ordering (2002), http://www.intel.com/design/itanium/downloads/251429.htm
Gibbons, P.B., Korach, E.: Testing shared memories. SIAM Journal on Computing 26(4), 1208–1244 (1997)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers C-28(9), 690–691 (1979)
Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence. In: Proceedings of the fifteenth annual ACM symposium on Parallel algorithms and architectures (SPAA), San Diego, pp. 254–255 (2003)
Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company (1997)
Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)
Hanna, F.K., Daeche, N.: Specification and verification using higher-order logic. In: 7th International Conference on Computer Hardware Description Languages and their Applications, pp. 418–419 (1985)
Gordon, M.: Why higher-order logic is a good formalism for specifying and verifying hardware. In: Formal aspects of VLSI design (1986)
Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design (November 2002)
Dill, D.L., Park, S., Nowatzyk, A.: Formal specification of abstract memory models. In: Research on Integrated Systems, pp. 38–52. MIT Press, Cambridge (1993)
Weaver, D.L., Germond, T.: The SPARC Architecture Manual – Version 9. P T R Prentice-Hall, Englewood Cliffs (1994)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 522–525. Springer, Heidelberg (1993)
Chatterjee, P., Gopalakrishnan, G.: Towards a formal model of shared memory consistency for Intel Itanium. In: ICCD, pp. 515–518 (2001)
Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: International Parallel and Distributed Processing Symposium (2004)
Personal Communication with Yuan B. Yu.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Analyzing the intel itanium memory ordering rules using logic programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 81–95. Springer, Heidelberg (2003)
Condon, A., Hill, M., Plakal, M., Sorin, D.: Using Lamport Clocks to Reason About Relaxed Memory Models. In: Fifth International Symposium On High Performance Computer Architecture (HPCA-5) (January 1999)
Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Design Automation Conference (DAC), pp. 425–430 (2003)
Gordon, M.: Programming Language Theory and Implementation. Prentice-Hall, Englewood Cliffs (1993)
Een, N.: Satzoo Incremental SAT Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004), http://www.math.chalmers.se/~een/Satzoo/AnExtensibleSATsolver.ps.gz
Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Computer Aided Verification. LNCS, vol. 2402, pp. 17–36 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gopalakrishnan, G., Yang, Y., Sivaraj, H. (2004). QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive