Sciweavers

Share
SPAA
1998
ACM

Lamport Clocks: Verifying a Directory Cache-Coherence Protocol

10 years 4 months ago
Lamport Clocks: Verifying a Directory Cache-Coherence Protocol
Modern shared-memory multiprocessors use complex memory system implementations that include a variety of non-trivial and interacting optimizations. More time is spent in verifying 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 difficult task. Current formal protocol verification techniques [18] complement simulation, but are somewhat nonintuitive to system designers and verifiers, and they do not scale well to practical systems. In this paper, 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...
Manoj Plakal, Daniel J. Sorin, Anne Condon, Mark D
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where SPAA
Authors Manoj Plakal, Daniel J. Sorin, Anne Condon, Mark D. Hill
Comments (0)
books