L. Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Transactions on Computers, vol.28, issue.9, pp.690-691, 1979.
DOI : 10.1109/TC.1979.1675439

L. M. Censier and P. Feautrier, A New Solution to Coherence Problems in Multicache Systems, IEEE Transactions on Computers, vol.27, issue.12, pp.1112-1118, 1978.
DOI : 10.1109/TC.1978.1675013

W. W. Collier, Principles of architecture for systems of parallel processes, 1981.

M. Dubois, C. Scheurich, and F. A. Briggs, Memory access buffering in multiprocessors, Proceedings of the 13th Annual Symposium on Computer Architecture, pp.434-442, 1986.

J. Misra, Axioms for memory access in asynchronous hardware systems, ACM Transactions on Programming Languages and Systems, vol.8, issue.1, pp.142-153, 1986.
DOI : 10.1145/5001.5007

D. Shasha and M. Snir, Efficient and correct execution of parallel programs that share memory, ACM Transactions on Programming Languages and Systems, vol.10, issue.2, pp.282-312, 1988.
DOI : 10.1145/42190.42277

J. R. Goodman, Cache consistency and sequential consistency, IEEE Scalable Coherent Interface (SCI) Working Group, 1989.

V. Sarita, M. D. Adve, and . Hill, Weak ordering ? a new definition, Proceedings of the 17th Annual International Symposium on Computer Architecture, ISCA '90, pp.2-14, 1990.

K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta et al., Memory consistency and event ordering in scalable shared-memory multiprocessors, Proceedings of the 17th Annual International Symposium on Computer Architecture, ISCA '90, pp.15-26, 1990.

W. W. Collier, Reasoning About Parallel Architectures, 1992.

S. Pradeep, J. Sindhu, M. Frailong, and . Cekleov, Formal Specification of Memory Models, pp.25-41, 1992.

P. Kohli, G. Neiger, and M. Ahamad, A Characterization of Scalable Shared Memories, 1993 International Conference on Parallel Processing, ICPP'93 Vol1, pp.332-335, 1993.
DOI : 10.1109/ICPP.1993.15

F. Corella, J. M. Stone, and C. M. Barton, A formal specification of the PowerPC shared memory architecture, 1993.

L. David, S. Dill, A. G. Park, and . Nowatzyk, Formal specification of abstract memory models, Proceedings of the 1993 Symposium on Research on Integrated Systems, pp.38-52, 1993.

H. Attiya and R. Friedman, Programming DEC-Alpha based multiprocessors the easy way (extended abstract), Proceedings of the sixth annual ACM symposium on Parallel algorithms and architectures , SPAA '94, pp.157-166, 1994.
DOI : 10.1145/181014.192323

M. José, V. Bernabéu-aubán, and . Cholvi-juan, Formalizing memory coherency models, Journal of Computing and Information, vol.1, pp.653-672, 1994.

K. Gharachorloo, Memory consistency models for shared-memory multiprocessors, WRL Research Report, vol.95, issue.9, 1995.

M. Ahamad, G. Neiger, J. E. Burns, P. Kohli, and P. W. Hutto, Causal memory: definitions, implementation, and programming, Distributed Computing, pp.37-49, 1995.
DOI : 10.1007/BF01784241
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.3356

L. Higham, J. Kawash, and N. Verwaal, Weak memory consistency models. Part I: Definitions and comparisons, 1998.

P. Chatterjee and G. Gopalakrishnan, Towards a formal model of shared memory consistency for Intel Itanium/sup TM/, Proceedings 2001 IEEE International Conference on Computer Design: VLSI in Computers and Processors. ICCD 2001, pp.515-518, 2001.
DOI : 10.1109/ICCD.2001.955081

. Intel, A formal specification of Intel Itanium processor family memory ordering, 2002.

A. Adir, H. Attiya, and G. 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

Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind, Nemos: a framework for axiomatic and executable specifications of memory consistency models, 18th International Parallel and Distributed Processing Symposium, 2004. Proceedings., 2004.
DOI : 10.1109/IPDPS.2004.1302944

L. Higham, L. Jackson, and J. Kawash, Programmercentric conditions for Itanium memory consistency, Proceedings of the 8th International Conference on Distributed Computing and Networking, ICDCN'06, pp.58-69, 2006.
DOI : 10.1007/11947950_7

A. Arvind and J. Maessen, Memory model = instruction reordering + store atomicity, Proceedings of the 33rd Annual International Symposium on Computer Architecture, ISCA '06, pp.29-40, 2006.
DOI : 10.1145/1150019.1136489
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.88.5131

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

S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge et al., The semantics of x86-CC multiprocessor machine code, Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.379-391, 2009.

J. Alglave, A. Fox, S. Ishtiaq, M. O. Myreen, S. 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, Proc. CAV, 2010.
DOI : 10.1007/978-3-642-14295-6_25
URL : https://hal.archives-ouvertes.fr/hal-01100859

S. Owens, S. Sarkar, and P. Sewell, A Better x86 Memory Model: x86-TSO, Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, pp.391-407, 2009.
DOI : 10.1007/11817963_46
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.6657

P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen, x86-TSO, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.
DOI : 10.1145/1785414.1785443

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams, Understanding POWER multiprocessors, Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation, pp.175-186, 2011.
DOI : 10.1145/2345156.1993520
URL : https://hal.archives-ouvertes.fr/hal-01100824

M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell, Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER, Proceedings of POPL 2012: The 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Philadelphia), pp.509-520, 2012.
DOI : 10.1145/2103656.2103717

L. Maranget, S. Sarkar, and P. Sewell, A tutorial introduction to the ARM and POWER relaxed memory mod- els. Draft available from http, 2012.

J. Alglave, L. Maranget, and M. Tautschnig, Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory, ACM TOPLAS, vol.36, issue.2, pp.7-8, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01081413

K. E. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar et al., An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors, Proceedings of the 48th International Symposium on Microarchitecture, MICRO-48, 2015.
DOI : 10.1145/2830772.2830775

S. Flur, K. E. Gray, C. Pulte, S. Sarkar, and A. Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: Concurrency and ISA, Proceedings of POPL: the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016.

S. Zhang, A. , and M. Vijayaraghavan, Taming weak memory models. CoRR, abs, 1606.

A. Ltd, ARM Architecture Reference Manual (ARMv8, for ARMv8- A architecture profile, 2015. ARM DDI 0487A.h (ID092915)

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Litmus: Running Tests against Hardware, Proceedings of TACAS 2011: the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.41-44, 2011.
DOI : 10.1145/1785414.1785443
URL : https://hal.archives-ouvertes.fr/hal-01100851

H. Boehm and S. Adve, Foundations of the C++ concurrency memory model, Proc. PLDI, 2008.

P. Cenciarelli, A. Knapp, and E. Sibilio, The Java Memory Model: Operationally, Denotationally, Axiomatically, ESOP, 2007.
DOI : 10.1007/978-3-540-71316-6_23

J. ?ev?ík and D. Aspinall, On Validity of Program Transformations in the Java Memory Model, 2008.
DOI : 10.1007/978-3-540-70592-5_3

M. Batty, K. Memarian, K. Nienhuis, J. Pichon-pharabod, and P. Sewell, The Problem of Programming Language Concurrency Semantics, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, pp.283-307, 2015.
DOI : 10.1007/978-3-662-46669-8_12

J. Pichon-pharabod and P. Sewell, A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions, Proceedings of POPL, 2016.
DOI : 10.1145/2914770.2837616

S. Flur, S. Sarkar, C. Pulte, K. Nienhuis, L. Maranget et al., Supplementary material, 2016.

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, Lem: reusable engineering of real-world semantics, Proceedings of ICFP 2014: the 19th ACM SIGPLAN International Conference on Functional Programming, pp.175-188, 2014.

M. Batty, The C11 and C++11 sConcurrency Model, 2014.

P. E. Mckenney and R. Silvera, Example POWER implementation for C/C++ memory model, 2011.

J. Alglave and L. Maranget, The diy tool

M. Batty, M. Dodds, and A. Gotsman, Library abstraction for C/C++ concurrency, Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL '13, pp.235-248, 2013.
DOI : 10.1145/2429069.2429099
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.261.2459

A. Turon, V. Vafeiadis, and D. Dreyer, GPS: Navigating weak memory with ghosts, protocols, and separation, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA, 2014.

R. Bornat, J. Alglave, and M. J. Parkinson, New lace and arsenic: adventures in weak memory with a program logic, 1416.