Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking

Shaz Qadeer

The memory model of a shared-memory multiprocessor is a contract between the designer and programmer of the multiprocessor. The sequential consistency memory model specifies a tota…