An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol
Fiche du document
28 novembre 2001
- handle: 10670/1.giqspz
- Wallace, Charles; Tremblay, Guy et Amaral, José N. (2001). « An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol ». Journal of Universal Computer Science, 7(11), pp. 1088-1112.
Ce document est lié à :
http://archipel.uqam.ca/8133/
Ce document est lié à :
http://www.jucs.org/doi?doi=10.3217/jucs-007-11-10 [...]
Ce document est lié à :
doi:10.3217/jucs-007-11-1088
Sujets proches
Retention (Psychology)Citer ce document
Charles Wallace et al., « An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol », UQAM Archipel : articles scientifiques, ID : 10670/1.giqspz
Métriques
Partage / Export
Résumé
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.