Verifying Correct Microarchitectural Enforcement of Memory Consistency Models

摘要

Memory consistency models define the rules and guarantees about the ordering and visibility of memory references on multithreaded CPUs and systems on chip. PipeCheck offers a methodology and automated tool for verifying that a particular microarchitecture correctly implements the consistency model required by its architectural specification.