H. [. Adir, G. Attiya, and . Shurek, Information-flow models for shared memory with an application to the powerPC architecture, IEEE Transactions on Parallel and Distributed Systems, vol.14, issue.5, 2003.
DOI : 10.1109/TPDS.2003.1199067

A. J. Alglave, S. Fox, M. O. Ishtiaq, S. Myreen, P. Sarkar et al., The semantics of power and ARM multiprocessor machine code, Proceedings of the 4th workshop on Declarative aspects of multicore programming, DAMP '09, 2009.
DOI : 10.1145/1481839.1481842

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Fences in Weak Memory Models, International Conference on Computer Aided Verification, 2010.
DOI : 10.1007/978-3-642-14295-6_25

URL : https://hal.archives-ouvertes.fr/hal-01100859

J. Alglave, L. Maranget, S. Sarkar, P. Sewell-[-csb93-]-f, J. M. Corella et al., Litmus: Running tests against hardware A formal specification of the PowerPC shared memory architecture Minisat -a SAT solver with conflict-clause minimization Memory consistency models for shared-memory multiprocessors, International Conference on Tools and Algorithms for the Construction and Analysis of Systems International Conference on Theory and Applications of Satisfiability TestingInt02] Intel. A formal specification of Intel Itanium processor family memory ordering, 1995.

P. [. Owens, F. Z. Böhm, P. Nardelli, and . Sewell, Lem: A lightweight tool for heavyweight semantics Rough Diamond " section), Proc. ITP: Interactive Theorem Proving, pp.363-369, 2011.

R. [. Stone and . Fitzgerald, Storage in the PowerPC, IEEE Micro, vol.15, 1995.

]. S. Ssa-+-11, P. Sarkar, J. Sewell, L. Alglave, D. Maranget et al., Understanding POWER multiprocessors [Sup] An axiomatic memory model for Power multiprocessors ? supplementary material, Programming Language Design and Implementation, 2011.

Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind, Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT, Correct Hardware Design and Verification Methods, 2003.
DOI : 10.1007/978-3-540-39724-3_9