Specification and verification of the LC cache protocol (Extended
abstract)
In recent years, a number of relaxed memory models for parallel
machines with distributed shared memories have been proposed. One
interesting model is Gao and Sarkar's Location Consistency
memory model, a model that does not require the coherence property to
hold. In this paper, we use the Abstract State Machine
specification methodology to give formal operational semantics for
both the Location Consistency memory model and an associated
cache protocol also proposed by Gao and Sarkar. Using these formal
models, we prove that the cache protocol satisfies the memory model,
that is, any value that can be read by the cache protocol is also a
value allowed by the abstract memory model.
Pour obtenir la version postscript
Cliquez
ici pour obtenir la version postscript.