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