The Location Consistency Memory Model and Cache Protocol: Specification
and Verification
Charles Wallace, Guy Tremblay, and José Nelson Amaral
We use the Abstract State Machine methodology to give formal
operational semantics for the Location Consistency memory model
and cache protocol. With these formal models, we prove that the cache
protocol satisfies the memory model, but in a way that is strictly stronger
than necessary, disallowing certain behavior allowed by the memory model.
Return to José Nelson Amaral's
Publications
Send comments to: amaral AT cs DOT ualberta DOT ca
Return to Amaral's home
page