Abstract
The problem of verifying multi-threaded execution against the memory consistency model of a processor is known to be an NP hard problem. However polynomial time algorithms exist that detect almost all failures in such execution. These are often used in practice for microprocessor verification. We present a low complexity and fully parallelized algorithm to check program execution against the processor consistency model. In addition our algorithm is general enough to support a number of consistency models without any degradation in performance. An implementation of this algorithm is currently used in practice to verify processors in the post silicon stage for multiple architectures.
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
Hangal, S., Vahia, D., Manovit, C., Lu, J.-Y.J.: Tsotool: A program for verifying memory systems using the memory consistency model. In: ISCA 2004: Proceedings of the 31st annual international symposium on Computer architecture, Washington, DC, USA, p. 114. IEEE Computer Society, Los Alamitos (2004)
Gibbons, P.B., Korach, E.: The complexity of sequential consistency. In: SPDP: Proceedings of the Fourth IEEE Symposium on Parallel and Distributed Processing, pp. 317–325 (1992)
Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence. In: SPAA 2003: Proceedings of the fifteenth annual ACM symposium on Parallel algorithms and architectures, pp. 254–255. ACM Press, New York (2003)
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)
Manovit, C., Hangal, S.: Efficient algorithms for verifying memory consistency. In: SPAA 2005: Proceedings of the 17th annual ACM symposium on Parallelism in algorithms and architectures, pp. 245–252. ACM Press, New York (2005)
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer 29(12), 66–76 (1996)
Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P.B., Gupta, A., Hennessy, J.L.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: 25 Years ISCA: Retrospectives and Reprints, pp. 376–387 (1998)
IA-32 Intel Architecture Software Developer’s Manual, vol. 3: System Programming Guide. Intel Corporation (2005), http://www.intel.com/design/pentium4/manuals/index_new.htm
Intel Itanium Architecture, vol. 1: Application Architecture. Intel Corporation (2005), http://www.intel.com/design/itanium/manuals/iiasdmanual.htm
Cain, H.W., Lipasti, M.H., Nair, R.: Constraint graph analysis of multithreaded programs. In: PACT 2003: Proceedings of the 12th International Conference on Parallel Architectures and Compilation Techniques, Washington, DC, USA, p. 4. IEEE Computer Society, Los Alamitos (2003)
Gopalakrishnan, G., Yang, Y., Sivaraj, H.: Qb or not qb: An efficient execution verification tool for memory orderings. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 401–413. Springer, Heidelberg (2004)
A Formal Specification of Intel Itanium Processor Family Memory Ordering. Intel Corporation (2005), http://www.intel.com/design/itanium/downloads/251429.htm
Warshall, S.: A theorem on boolean matrices. J. ACM 9(1), 11–12 (1962)
Fleckenstein, C.J., Huang, J.C., Roy, A., Zeisset, S.: Fast and Generalized Polynomial Time Memory Consistency Verification. Technical Report arXiv:cs.AR/0605039 (May 2006)
Banerjee, U.K.: Loop Parallelization. Kluwer Academic, Norwell (1994)
Bentley, B.: Validating the intel pentium 4 microprocessor. In: DAC 2001: Proceedings of the 38th conference on Design automation, pp. 244–248. ACM Press, New York (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roy, A., Zeisset, S., Fleckenstein, C.J., Huang, J.C. (2006). Fast and Generalized Polynomial Time Memory Consistency Verification. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_46
Download citation
DOI: https://doi.org/10.1007/11817963_46
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)