Loading...
Please wait, while we are loading the content...
Similar Documents
Using lamport clocks to reason about relaxed memory models (1999)
| Content Provider | CiteSeerX |
|---|---|
| Author | Condon, Anne E. Plakal, Manoj Sorin, Daniel J. Hill, Mark D. |
| Description | In Proceedings of the 5th International Symposium on High Performance Computer Architecture |
| Abstract | 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 requiring the write to be immediately written to cache. Analysis shows how to apply Lamport clocks to verify TSO and Alpha specifications at the architectural level. |
| File Format | |
| Publisher Date | 1999-01-01 |
| Access Restriction | Open |
| Subject Keyword | Logical Clock Sparc Total Store Order Alpha Specification Cache Coherence Protocol Architectural Level Sgi Origin 2000-like Directory Protocol Alpha Implementation Current Shared-memory Multiprocessor Sun Gigaplane-like Split-transaction Bus Protocol Many Commercial Multiprocessor Relaxed Memory Model First-in-first-out Write Buffer Weak Consistency Write Buffer Processor Consistency Tso Implementation Read Request Relaxed Model Lamport Clock |
| Content Type | Text |
| Resource Type | Proceeding Conference Proceedings Article |
