An Axiomatic Memory Model for POWER Multiprocessors

Abstract : The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and dis-allowed behaviors, posing challenges in specifying their memory models formally and accurately, and in understanding and analyzing the behav-ior of concurrent software. This complexity is particularly evident in the IBM R Power Architecture R , for which a faithful specification was pub-lished only in 2011 using an operational style. In this paper we present an equivalent axiomatic specification, which is more abstract and con-cise. Although not officially sanctioned by the vendor, our results indicate that this axiomatic specification provides a reasonable basis for reasoning about current IBM R POWER R multiprocessors. We establish the equiva-lence of the axiomatic and operational specifications using both manual proof and extensive testing. To demonstrate that the constraint-based style of axiomatic specification is more amenable to computer-aided ver-ification, we develop a SAT-based tool for evaluating possible outcomes of multi-threaded test programs, and we show that this tool is signifi-cantly more efficient than a tool based on an operational specification.
Type de document :
Communication dans un congrès
Computer Aided Verification - 24th International Conference, CAV, Jul 2012, Berkely, United States. pp.495 - 512, 2012, 〈10.1007/978-3-642-31424-7_36〉
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01100773
Contributeur : Luc Maranget <>
Soumis le : mercredi 7 janvier 2015 - 09:37:26
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 00:55:56

Fichier

cav12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, et al.. An Axiomatic Memory Model for POWER Multiprocessors. Computer Aided Verification - 24th International Conference, CAV, Jul 2012, Berkely, United States. pp.495 - 512, 2012, 〈10.1007/978-3-642-31424-7_36〉. 〈hal-01100773〉

Partager

Métriques

Consultations de la notice

106

Téléchargements de fichiers

74