A memory consistency model checking library implemented in C++11. This library provides the building blocks for the McVerSi framework [1].
The McVerSi guest workload can be found in contrib/mcversi.
The library is header-only.
API documentation can be found here.
The provided Makefile is for unit testing and static analysis.
If you use this library or the McVerSi framework in your work, we would appreciate if you cite the McVerSi paper:
@inproceedings{ElverN2016,
author = {Marco Elver and Vijay Nagarajan},
title = {{McVerSi}: {A} {T}est {G}eneration {F}ramework for {F}ast
{M}emory {C}onsistency {V}erification in {S}imulation},
booktitle = {IEEE International Symposium on
High Performance Computer Architecture (HPCA)},
month = mar,
year = {2016},
venue = {Barcelona, Spain}
}
Notable extensions that have been added after publication of the McVerSi paper:
- Support for synonym sets of virtual addresses mapping to same physical address -- see EvtStateCats and guest_workload.
| [1] | Marco Elver and Vijay Nagarajan. McVerSi: A Test Generation Framework for Fast Memory Consistency Verification in Simulation. In IEEE International Symposium on High Performance Computer Architecture (HPCA). Barcelona, Spain, March 2016. |