Title :
Verifying Correct Microarchitectural Enforcement of Memory Consistency Models
Author :
Lustig, Daniel ; Pellauer, Michael ; Martonosi, Margaret
Abstract :
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.
Keywords :
memory architecture; multi-threading; system-on-chip; PipeCheck; correct microarchitectural enforcement; memory consistency models; memory references; multithreaded CPU; systems on chip; Analytical models; Buffer storage; Load modeling; Microarchitecture; Pipelines; Program processors; Radio frequency; PipeCheck; computer architecture; formal verification; memory architecture; memory consistency model; processor microarchitecture;
Journal_Title :
Micro, IEEE
