JUCS - Journal of Universal Computer Science 7(11): 1088-1112, doi: 10.3217/jucs-007-11-1088
An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol
expand article infoCharles Wallace‡, Guy Tremblay§, Jose N. Amaral|
‡ Computer Science Dept., Michigan Technological University, Houghton, MI, United States of America§ Dept. d'informatique, Université du Québec à Montréal, Montréal, Canada| Computing Science Dept., University of Alberta, Edmonton, Canada

Corresponding author: Charles Wallace ( wallace@mtu.edu )

© Charles Wallace, Guy Tremblay, Jose Amaral.
This article is freely available under the J.UCS Open Content License.
Citation: Wallace C, Tremblay G, Amaral JN (2001) An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol. JUCS - Journal of Universal Computer Science 7(11): 1088-1112. https://doi.org/10.3217/jucs-007-11-1088
Open Access
Abstract
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.
Keywords
requirements/specifications, multiprocessors, shared memory, cache memories