Automatic generation of memory consistency tests for chip multiprocessing

Chip multiprocessing (CMP) changed the architectural landscape of PCs and servers and is now changing the way personal mobile devices are designed. CMP requires access to shared variables in private memories, leading to complex chains of interacting events that must offer a consistent view of shared memory. Checking if a memory system implements a specified memory consistency model (MCM) is a challenging verification problem. We propose a generator of multi-threading random-instruction sequences for MCM checking. It complies with an arbitrary MCM and can be used by most checkers. Its ability to provide full coverage was evaluated through 1200 test cases.