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, pp.502-515, 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 Shared memory consistency models: A tutorial, Proc. DAMPAlg10] Jade Alglave. A Shared Memory Poetics, pp.66-76, 1996.

L. [. Alglave, S. Maranget, P. Sarkar, and . Sewell, Fences in Weak Memory Models, Proc. CAV, 2010.
DOI : 10.1007/978-3-642-14295-6_25

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

L. [. Alglave, S. Maranget, P. Sarkar, and . Sewell, Litmus: Running Tests against Hardware, Proc. TACAS, 2011. [ARM08] ARM. ARM Barrier Litmus Tests and Cookbook, 2008.
DOI : 10.1145/1785414.1785443

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

H. Boehm, S. Adve, S. Owens, S. Sarkar, P. Sewell et al., Foundations of the C++ concurrency memory model, Proc. PLDI Proc. POPL, 2008.

N. Chong and S. Ishtiaq, Reasoning about the ARM weakly consistent memory model, Proceedings of the 2008 ACM SIGPLAN workshop on Memory systems performance and correctness held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '08), MSPC '08, 2008.
DOI : 10.1145/1353522.1353528

W. W. Collier, Reasoning about parallel architectures, 1992.

[. Corella, J. M. Stone, and C. M. Barton, A formal specification of the PowerPC shared memory architecture, Scheurich, and F. Briggs. Memory access buffering in multiprocessors. In ISCA, 1986.

L. R. Joshi, J. Lamport, S. Matthews, M. Tasiran, Y. Tuttle et al., Checking Cache-Coherence Protocols with TLA+, Formal Methods in System Design, vol.22, issue.2, pp.125-131, 2003.
DOI : 10.1023/A:1022969405325

B. [. Kalla, W. J. Sinharoy, M. Starke, and . Floyd, Power7: IBM's Next-Generation Server Processor, IEEE Micro, vol.30, issue.2, pp.7-15, 2010.
DOI : 10.1109/MM.2010.38

]. D. Lea and . Lea, The JSR-133 cookbook for compiler writers

W. J. Le, J. S. Starke, F. P. Fields, D. Q. O-'connell, B. J. Nguyen et al., IBM POWER6 microarchitecture, IBM Journal of Research and Development, vol.51, issue.6, pp.639-662, 1994.
DOI : 10.1147/rd.516.0639

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.6020

. S. Obzns, P. Owens, F. Z. Böhm, P. Nardelli, S. Sewell et al., Lightweight tools for heavyweight semantics Submitted for publication http://www.cl.cam.ac.uk/ ~so294 A better x86 memory model: x86-TSO Storage in the PowerPC, Proc. TPHOLs, pp.391-40750, 1995.

J. [. Sindhu, M. Frailong, and . Cekleov, Formal Specification of Memory Models, Scalable Shared Memory Multiprocessors, pp.25-42, 1991.
DOI : 10.1007/978-1-4615-3604-8_2

. Skt-+-05-]-b, R. N. Sinharoy, J. M. Kalla, R. J. Tendler, J. B. Eickemeyer et al., POWER5 system microarchitecture [Spa92] The SPARC Architecture Manual, IBM Journal of Research and Development, vol.49, issue.4-5 8, pp.505-522, 1992.

]. P. Sso-+-10, S. Sewell, S. Sarkar, F. Z. Owens, M. O. Nardelli et al., x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.

S. Sarkar, P. Sewell, F. Zappa-nardelli, S. Owens, T. Ridge et al., The semantics of x86-CC multiprocessor machine code Analyzing the Intel Itanium memory ordering rules using logic programming and SAT, Proc. POPL Proc. CHARME, LNCS 2860, 2003.