A Better Reduction Theorem for Store Buffers

Ernie Cohen, Norbert Schirmer

When verifying a concurrent program, it is usual to assume that memory is sequentially consistent. However, most modern multiprocessors depend on store buffering for efficiency, an…