Loading...
Please wait, while we are loading the content...
Similar Documents
Lamport Clocks: Verifying a Directory Cache-Coherence Protocol (1998)
| Content Provider | CiteSeerX |
|---|---|
| Author | Plakal, Manoj Sorin, Daniel J. Condon, Anne E. Hill, Mark D. |
| Description | Modern shared-memory multiprocessors use complex memory system implementations that include a variety of non-trivial and interacting optimizations. More time is spent in verl$ving the correctness of such implementations than in designing the system. In particular; large-scale Distributed Shared Memory (DSM) systems usually rely on a directory cache-coherence protocol to provide the illusion of a sequentially consistent shared address space. Verifying that such a distributed protocol satisfies sequential consistency is a dificult task. Current formal protocol verification techniques [18] complement simulation, but are somewhat nonintuitive to system designers and verl$ers, and they do not scale well to practical systems. In this papes we examine a new reasoning technique that is precise and (we find) intuitive. Our technique is based on Lamport’s logical clocks, which were originally used in distributed systems. We make modest extensions to Lamport’s logical clocking scheme to assign timestamps to relevant protocol events to construct a total ordering of such events. Such total orderings can be used to verify that the requirements of a particular memory consistency model have been satisjed. We apply Lamport clocks to prove that a non-trivial directory protocol implements sequential consistency. To do this, we describe an SC1 Origin 2000~like protocol [12] in detail, provide a timestamping scheme that totally orders all protocol events, and then prove sequential consistency (i.e., a load always returns the value of the “last ” store to the same address in timestamp order). 1 |
| File Format | |
| Language | English |
| Publisher Date | 1998-01-01 |
| Publisher Institution | In Proceedings of the 10th Annual ACM Symposium on Parallel Architectures and Algorithms |
| Access Restriction | Open |
| Subject Keyword | Logical Clock Modest Extension Large-scale Distributed Shared Memory Total Ordering Particular Memory Consistency Model System Designer Current Formal Protocol Verification Technique Timestamping Scheme Timestamp Order Last Store Protocol Event Interacting Optimization New Reasoning Technique Sequential Consistency Distributed System Protocol Satisfies Sequential Consistency Dificult Task Complement Simulation Sc1 Origin Verl Er Modern Shared-memory Multiprocessor Practical System Address Space Complex Memory System Implementation Directory Cache-coherence Protocol Lamport Clock |
| Content Type | Text |
| Resource Type | Article |
