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

• Type: Conference
• Year: 1998
• Where: SPAA
• Authors: Manoj Plakal, Daniel J. Sorin, Anne Condon, Mark D. Hill
• Keywords: Distributed And Parallel Computing, Protocol Events, Satisfies Sequential Consistency, Sequential Consistency, SPAA 1998