Sciweavers

HPCA
1999
IEEE

Using Lamport Clocks to Reason about Relaxed Memory Models

13 years 8 months ago
Using Lamport Clocks to Reason about Relaxed Memory Models
Cache coherence protocols of current shared-memory multiprocessors are difficult to verify. Our previous work proposed an extension of Lamport's logical clocks for showing that multiprocessors can implement sequential consistency (SC) with an SGI Origin 2000-like directory protocol and a Sun Gigaplane-like split-transaction bus protocol. Many commercial multiprocessors, however, implement more relaxed models, such as SPARC Total Store Order (TSO), a variant of processor consistency, and Compaq (DEC) Alpha, a variant of weak consistency. This paper applies Lamport clocks to both a TSO and an Alpha implementation. Both implementations are based on the same Sun Gigaplane-like split-transaction bus protocol we previously used, but the TSO implementation places a first-in-first-out write buffer between a processor and its cache, while the Alpha implementation uses a coalescing write buffer. Both write buffers satisfy read requests for pending writes (i.e., do bypassing) without requir...
Anne Condon, Mark D. Hill, Manoj Plakal, Daniel J.
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where HPCA
Authors Anne Condon, Mark D. Hill, Manoj Plakal, Daniel J. Sorin
Comments (0)