Parallel Methods for Verifying the Consistency of Weakly-Ordered Architectures

Adam McLaughlin, Duane Merrill, Michael Garland, David A. Bader

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations


Contemporary microprocessors use relaxed memory consistency models to allow for aggressive optimizations in hardware. This enhancement in performance comes at the cost of design complexity and verification effort. In particular, verifying an execution of a program against its system's memory consistency model is an NP-complete problem. Several graph-based approximations to this problem based on carefully constructed randomized test programs have been proposed in the literature, however, such approaches are sequential and execute slowly on large graphs of interest. Unfortunately, the ability to execute larger tests is tremendously important, since such tests enable one to expose bugs more quickly. Successfully executing more tests per unit time is also desirable, since it allows for one to check for a greater variety of errors in the memory subsystem by utilizing a more diverse set of tests. This paper improves upon existing work by introducing an algorithm that not only reduces the time complexity of the verification process, but also facilitates the development of parallel algorithms for solving these problems. We first show performance improvements from a sequential approach and gain further performance from parallel implementations in OpenMP and CUDA. For large tests of interest, our GPU implementation achieves an average application speedup of 26.36x over existing techniques in use at NVIDIA.

Original languageEnglish (US)
Title of host publicationProceedings - 24th International Conference on Parallel Architecture and Compilation, PACT 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages12
ISBN (Electronic)9781467395243
StatePublished - Mar 8 2016
Externally publishedYes
Event24th International Conference on Parallel Architecture and Compilation, PACT 2015 - San Francisco, United States
Duration: Oct 18 2015Oct 21 2015

Publication series

NameParallel Architectures and Compilation Techniques - Conference Proceedings, PACT
ISSN (Print)1089-795X


Conference24th International Conference on Parallel Architecture and Compilation, PACT 2015
Country/TerritoryUnited States
CitySan Francisco

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


  • Graph Algorithms
  • Memory Consistency Verification
  • Parallel Algorithms
  • Relaxed Memory Models


Dive into the research topics of 'Parallel Methods for Verifying the Consistency of Weakly-Ordered Architectures'. Together they form a unique fingerprint.

Cite this