mc2lib

A memory consistency model checking library implemented in C++11. This library provides the building blocks for the McVerSi framework¹.

The McVerSi guest workload can be found in contrib/mcversi.

Usage

The library is header-only.

API documentation can be found here.

The provided Makefile is for unit testing and static analysis.

Citation

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}
}

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 -- see EvtStateCats and guest_workload.

References

---

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