Verifying sequentially consistent memory
Ed Brinksma, Jim Davies, Rob Gerth, Susanne Graf, Wil Janssen, Bengt Jönsson, Shmuel M. Katz, Gavin Lowe, Mannes Poel, Amir Pnueli, Camilla Østerberg Rump, Job Zwiers · University of Twente Research Information · 1994
In distributed shared memory architectures, memory usually obeys weaker constraints than that of ordinary memory in (cache-less) single processor systems. One popular weakening is that of sequential consistency. Proving that a memory is sequentialy consistent does not easily fit the standard refinement and verification strategies. This paper takes a sequential consistent memory-the lazy caching protocol-and verifies it using a number of verification approaches. In almost all cases, existing approaches have to be generalized first.