- 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, genetic improvement, SBSE, MCM test generation",
-
URL = "
http://hpca22.site.ac.upc.edu/index.php/program/conference-program/",
-
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 = "https://github.com/melver/mc2lib University of
Edinburgh
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. https://github.com/melver/mc2lib
Also known as \cite{7446099}",
