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

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

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).
Original languageEnglish
Title of host publication2016 IEEE International Symposium on High Performance Computer Architecture (HPCA)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages618-630
Number of pages13
ISBN (Electronic)978-1-4673-9211-2
DOIs
Publication statusPublished - Mar 2016
Event2016 IEEE International Symposium on High Performance Computer Architecture - Barcelona, Spain
Duration: 12 Mar 201616 Mar 2016
http://hpca22.site.ac.upc.edu/

Conference

Conference2016 IEEE International Symposium on High Performance Computer Architecture
Abbreviated titleHPCA 2016
CountrySpain
CityBarcelona
Period12/03/1616/03/16
Internet address

Fingerprint

Dive into the research topics of 'McVerSi: A Test Generation Framework for Fast Memory Consistency Verification in Simulation'. Together they form a unique fingerprint.

Cite this