McVerSi: A Test Generation Framework for Fast Memory Consistency Verification in Simulation

Created by W.Langdon from gp-bibliography.bib Revision:1.4208

  author =       "Marco Elver and Vijay Nagarajan",
  title =        "{McVerSi}: A Test Generation Framework for Fast Memory
                 Consistency Verification in Simulation",
  booktitle =    "22nd IEEE Symposium on High Performance Computer
                 Architecture, HPCA 2016",
  year =         "2016",
  pages =        "618--630",
  address =      "Barcelona",
  keywords =     "genetic algorithms, genetic programming, SBSE, MCM
                 test generation",
  URL =          "",
  DOI =          "doi:10.1109/HPCA.2016.7446099",
  month =        "12-16 " # mar,
  size =         "13 pages",
  abstract =     "The memory consistency model (MCM), which formally
                 specifies the behaviour of the memory system, is used
                 by programmers to reason about parallel programs. It is
                 imperative that hardware adheres to the promised MCM.
                 For this reason, hardware designs must be verified
                 against the specified MCM. One common way to do this is
                 via executing tests, where specific threads of
                 instruction sequences are generated and their
                 executions are checked for adherence to the MCM. It
                 would be extremely beneficial to execute such tests
                 under simulation, i.e. when the functional design
                 implementation of the hardware is being prototyped.
                 Most prior verification methodologies, however, target
                 post-silicon environments, which when applied under
                 simulation would be too slow. We propose McVerSi, a
                 test generation framework for fast MCM verification of
                 a full-system design implementation under simulation.
                 Our primary contribution is a Genetic Programming (GP)
                 based approach to MCM test generation, which relies on
                 a novel crossover function that prioritizes memory
                 operations contributing to non-determinism, thereby
                 increasing the probability of uncovering MCM bugs. To
                 guide tests towards exercising as much logic as
                 possible, the simulator's reported coverage is used as
                 the fitness function. Furthermore, we increase test
                 throughput by making the test workload
                 simulation-aware. We evaluate our proposed framework
                 using the Gem5 cycle accurate simulator in full-system
                 mode with Ruby. We discover 2 new bugs due to the
                 faulty interaction of the pipeline and the cache
                 coherence protocol. Crucially, these bugs would not
                 have been discovered through individual verification of
                 the pipeline or the coherence protocol. We study 11
                 bugs in total. Our GP-based test generation approach
                 finds all bugs consistently, therefore providing much
                 higher guarantees compared to alternative approaches
                 (pseudo-random test generation and litmus tests)",
  notes =        " University of

                 p618 'one of the bugs discovered would not ... have
                 been discovered through individual verification of
                 either pipeline or coherence protocol.' chomosome is
                 DAG p621 'tests must be recombined in a way, such that
                 the resulting test is likely to be more racy than its
                 parents.' 'we design a selective crossover' crossover
                 with mutation.

                 Ruby GARNET x86-64 ISA. diy-litmus.

                 Also known as \cite{7446099}",

Genetic Programming entries for Marco Elver Vijay Nagarajan