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...

• Type: Conference
• Year: 1999
• Where: HPCA
• Authors: Anne Condon, Mark D. Hill, Manoj Plakal, Daniel J. Sorin
• Keywords: Distributed And Parallel Computing, HPCA 1999, Lamport Clocks, Split-transaction Bus Protocol, Write Buffers