An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol

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.

Fichier(s) associé(s) à ce document :

Prévisualisation	PDF Télécharger (249kB)

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.

Type:	Article de revue scientifique
Mots-clés ou Sujets:	Requirements/Specifications, Multiprocessors, Shared Memory, Cache Memories
Unité d'appartenance:	Faculté des sciences > Département d'informatique
Déposé par:	Guy Tremblay
Date de dépôt:	14 avr. 2016 13:09
Dernière modification:	27 avr. 2016 18:08
Adresse URL :	http://archipel.uqam.ca/id/eprint/8133

Modifier les métadonnées (propriétaire du document)

Statistiques