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

HPCA 2016 Paper

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).

mc2lib: Simulator Independent C++ Library

mc2lib — C++ library for the simulator-independent aspects of McVerSi. It includes:

• Memory consistency descriptions and a checker;

• Test generation integrating MCM descriptions;

• A simple GA/GP library.

API documentation.

Extensions

Notable extensions that have been added after publication of the McVerSi paper:

• Support for synonym sets of virtual addresses mapping to same physical address.

Gem5 Integration

A cleaned up version (with empty coverage computation to be filled by designer) of our McVerSi implementation for Gem5 is currently provided as a patch (includes mc2lib). Steps to use this patch with Gem5:

1. The patch has been tested on top of changeset 11520;

2. Compile with supported architecture, currently ARM or X86;

3. Compile the guest workload in contrib/mcversi with the correct version of m5op in target FS disk image; if you are in a hurry, you can get pre-compiled binaries here;

4. Take a checkpoint with cpu-type=timing;

5. Restore from checkpoint and run with cpu-type=detailed and load guest_workload with appropriate parameters (other CPU types need adding the same hooks as is done for O3).

The debug flag McVerSi is provided to monitor progress if needed, as well as the current test’s threads are written to m5out/mcversi_*.bin (only in debug builds). Upon finding a MCM violation, the cyclic relation is output to m5out/mcversi_*.dot. Debugging would involve:

1. Inspecting the cycle and gathering the events and their addresses involved;

2. Identifying the corresponding instructions in mcversi_*.bin and understand what should have happened;

3. Identify the last verify() step that passed, and its curTick;

4. Re-run Gem5 with the same parameters and set a break point at the tick of the verify() before the violation;

5. Record relevant trace of test iteration that is causing a violation;

6. Analyze trace …

Known Found Bugs

The 2 bugs in Gem5 from the McVerSi paper:

1. http://reviews.gem5.org/r/2840 (patch in upstream)

2. http://reviews.gem5.org/r/2842

Gem5

3. Classic cache not forwarding invalidation to CPU after replacement

4. LSQ does not respect virtual address synonyms when forwarding from SQ