P. Aziz-abdulla, M. F. Atig, Y. Chen, C. Leonardsson, and A. Rezine, Counter-Example Guided Fence Insertion under TSO, Proceedings of TACAS, pp.204-219, 2012.
DOI : 10.1007/978-3-642-28756-5_15

P. Aziz-abdulla, M. F. Atig, Y. Chen, C. Leonardsson, and A. Rezine, Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO, Proceedings of TACAS, pp.530-536, 2013.
DOI : 10.1007/978-3-642-36742-7_37

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

V. Sarita, H. Adve, and . Boehm, Memory models: A case for rethinking parallel languages and hardware, Communications of the ACM, vol.53, issue.8, pp.90-101, 2010.

V. Sarita, K. Adve, and . Gharachorloo, Shared memory consistency models: A tutorial, IEEE Computer, vol.29, issue.12, pp.66-76, 1996.

J. Alglave, A Shared Memory Poetics, 2010.

J. Alglave, A formal hierarchy of weak memory models, Formal Methods in System Design 41, pp.178-210, 2012.
DOI : 10.1007/s10703-012-0161-5

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

J. Alglave, D. Kroening, J. Lugton, V. Nimal, and M. Tautschnig, Soundness of Data Flow Analyses for Weak Memory Models, Proceedings of APLAS, pp.272-288, 2011.
DOI : 10.1145/186025.186043

J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig, Software Verification for Weak Memory via Program Transformation, Proceedings of ESOP, pp.512-532, 2013.
DOI : 10.1007/978-3-642-37036-6_28
URL : http://arxiv.org/abs/1207.7264

J. Alglave, D. Kroening, and M. Tautschnig, Partial Orders for Efficient Bounded Model Checking of??Concurrent??Software, Proceedings of CAV, pp.141-157, 2013.
DOI : 10.1007/978-3-642-39799-8_9

J. Alglave and L. Maranget, Stability in Weak Memory Models, Proceedings of CAV, pp.50-66, 2011.
DOI : 10.1007/978-3-540-30482-1_11
URL : https://hal.archives-ouvertes.fr/hal-01100806

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Fences in Weak Memory Models, Proceedings of CAV, pp.258-272, 2010.
DOI : 10.1007/978-3-642-14295-6_25
URL : https://hal.archives-ouvertes.fr/hal-01100859

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Litmus: Running Tests against Hardware, Proceedings of TACAS, pp.41-44, 2011.
DOI : 10.1145/1785414.1785443
URL : https://hal.archives-ouvertes.fr/hal-01100851

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Fences in weak memory models (extended version) Formal Methods in System Design 40, pp.170-205, 2012.

A. Ltd, ARM Architecture Reference Manual: ARMv7-A and ARMv7-R Edition, 2010.

A. Ltd, Cortex-A9 MPCore, Programmer Advice Notice, Read-after-Read Hazards, 2011.

A. and J. Maessen, Memory Model = Instruction Reordering + Store Atomicity, Proceedings of ISCA, pp.29-40, 2006.

M. Faouzi-atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi, On the verification problem for weak memory models, Proceedings of POPL, pp.7-18, 2010.

M. Faouzi-atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi, What's decidable about weak memory models, Proceedings of ESOP, pp.26-46, 2012.

M. Faouzi-atig, A. Bouajjani, and G. Parlato, Getting rid of store-buffers in TSO analysis, Proceedings of CAV, pp.99-115, 2011.

M. Batty, M. Dodds, and A. Gotsman, Library abstraction for C/C++ concurrency, Proceedings of POPL, pp.235-248, 2013.
DOI : 10.1145/2429069.2429099
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.261.2459

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber, Mathematizing C++ concurrency, Proceedings of POPL, pp.55-66, 2011.
DOI : 10.1145/1925844.1926394
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.185.4736

Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

H. Boehm and S. V. Adve, Foundations of the C++ concurrency memory model, Proceedings of PLDI, pp.68-78, 2008.

H. Boehm and S. V. Adve, You don't know jack about shared variables or memory models, Communications of the ACM, vol.55, issue.2, pp.48-54, 2012.
DOI : 10.1145/2076450.2076465

A. Bouajjani, E. Derevenetc, and R. Meyer, Checking and Enforcing Robustness against TSO, Proceedings of ESOP, pp.533-553, 2013.
DOI : 10.1007/978-3-642-37036-6_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.670.9758

A. Bouajjani, R. Meyer, and E. Möhlmann, Deciding Robustness against Total Store Ordering, Proceedings of ICALP, pp.428-440, 2011.
DOI : 10.1145/42190.42277

G. Boudol and G. Petri, Relaxed memory models: An operational approach, Proceedings of POPL, pp.392-403, 2009.
DOI : 10.1145/1480881.1480930
URL : https://hal.archives-ouvertes.fr/inria-00420352

G. Boudol, G. Petri, and B. P. Serpette, Relaxed Operational Semantics of Concurrent Programming Languages, Proceedings of EXPRESS/SOS, pp.19-33, 2012.
DOI : 10.4204/EPTCS.89.3

S. Burckhardt, R. Alur, and M. M. Martin, CheckFence: Checking consistency of concurrent data types on relaxed memory models, Proceedings of PLDI, pp.12-21, 2007.

S. Burckhardt, A. Gotsman, and H. Yang, Understanding eventual consistency, 2013.

S. Burckhardt, A. Gotsman, H. Yang, and M. Zawirski, Replicated data types, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.271-284, 2014.
DOI : 10.1145/2535838.2535848
URL : https://hal.archives-ouvertes.fr/hal-00934311

S. Burckhardt and M. Musuvathi, Memory Model Safety of Programs, Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC) 2, 2008.

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

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, pp.16-19, 2008.
DOI : 10.1145/1353522.1353528

E. M. Clarke, D. Kroening, and F. Lerda, A Tool for Checking ANSI-C Programs, Proceedings of TACAS, pp.168-176, 2004.
DOI : 10.1007/978-3-540-24730-2_15

W. Collier, Reasoning About Parallel Architectures, 1992.

K. Gharachorloo, D. Lenoski, J. Laudon, P. B. Gibbons, A. Gupta et al., Memory consistency and event ordering in scalable shared-memory multiprocessors, Proceedings of ISCA, pp.15-26, 1990.

J. Goodman, Cache consistency and sequential consistency, 1989.

G. Gopalakrishnan, Y. Yang, and H. Sivaraj, QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings, Proceedings of CAV, pp.401-413, 2004.
DOI : 10.1007/978-3-540-27813-9_31

J. C. Michael and . Gordon, Relating event and trace semantics of hardware description languages, Computer Journal, vol.45, issue.1, pp.27-36, 2002.

R. Grisenthwaite, ARM Barrier Litmus Tests and Cookbook, 2009.

S. Hangal, D. Vahia, C. Manovit, J. Lu, and S. Narayanan, TSOtool, Proceedings of ISCA, pp.114-123, 2004.
DOI : 10.1145/1028176.1006710

C. A. Hoare and P. E. Lauer, Consistent and complementary formal theories of the semantics of programming languages, Acta Informatica, vol.3, issue.2, pp.135-153, 1974.
DOI : 10.1007/BF00264034

D. Howells and P. E. Mackenney, Linux Kernel Memory Barriers, 2013 version, 2013.

I. Corp, A Formal Specification of Intel Itanium Processor Family Memory Ordering, IntelCorp, 2002.

I. Corp, Intel 64 and IA-32 Architectures Software Developer's Manual, ISO/IEC 9899:2011 Information technology ? Programming languages ? C. International Organization for Standardization, 2009.

D. Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology, vol.11, issue.2, pp.256-290, 2002.
DOI : 10.1145/505145.505149

Y. Vineet-kahlon, S. Yang, A. Sankaranarayanan, and . Gupta, Fast and accurate static datarace detection for concurrent programs, Proceedings of CAV, pp.226-239, 2007.

M. Kuperstein, M. T. Vechev, and E. Yahav, Automatic inference of memory fences, Proceedings of FMCAD. IEEE Computer Society, pp.111-119, 2010.
DOI : 10.1145/2261417.2261438

M. Kuperstein, M. T. Vechev, and E. Yahav, Partial-coherence abstractions for relaxed memory models, Proceedings of PLDI, pp.187-198, 2011.

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

J. Richard, J. S. Lipton, and . Sandberg, PRAM: A scalable shared memory, 1988.

F. Liu, N. Nedev, N. Prisadnikov, M. T. Vechev, and E. Yahav, Dynamic synthesis for relaxed memory models, Proceedings of PLDI, pp.429-440, 2012.

S. Mador-haim, R. Alur, and M. M. Martin, Generating Litmus Tests for Contrasting Memory Consistency Models, Proceedings of CAV, pp.273-287, 2010.
DOI : 10.1007/978-3-642-14295-6_26

S. Mador-haim, L. Maranget, S. Sarkar, K. Memarian, J. Alglave et al., An Axiomatic Memory Model for POWER Multiprocessors, Proceedings of CAV, pp.495-512, 2012.
DOI : 10.1007/978-3-642-31424-7_36
URL : https://hal.archives-ouvertes.fr/hal-01100773

J. Manson, W. Pugh, and S. V. Adve, The Java memory model, Proceedings of POPL, pp.378-391, 2005.

E. Paul, J. Mckenney, and . Walpole, What is RCU, fundamentally?, 2007.

G. Neiger, A taxonomy of multiprocessor memory-ordering models, Tutorial and Workshop on Formal Specification and Verification Methods for Shared Memory Systems, 2000.

S. Owens, P. Böhm, F. Z. Nardelli, and P. Sewell, Lem: A Lightweight Tool for Heavyweight Semantics, Proceedings of ITP, pp.363-369, 2011.
DOI : 10.1007/978-3-540-68237-0_21

S. Owens, S. Sarkar, and P. Sewell, A Better x86 Memory Model: x86-TSO, Proceedings of TPHOLs, pp.391-407, 2009.
DOI : 10.1007/11817963_46

S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell et al., Synchronising C/C++ and POWER, Proceedings of PLDI, pp.311-322, 2012.
DOI : 10.1145/2254064.2254102
URL : https://hal.archives-ouvertes.fr/hal-01100798

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams, Understanding power multiprocessors, Proceedings of PLDI, pp.175-186, 2011.
DOI : 10.1145/2345156.1993520
URL : https://hal.archives-ouvertes.fr/hal-01100824

S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge et al., The semantics of x86-CC multiprocessor machine code, Proceedings of POPL, pp.379-391, 2009.

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

. Sparc-international-inc, The SPARC Architecture Manual Version 8. SPARC International Inc. SPARC International Inc. 1994. The SPARC Architecture Manual Version 9, 1992.

C. Robert, G. J. Steinke, and . Nutt, A unified theory of shared memory consistency, Journal of the ACM, vol.51, issue.5, pp.800-849, 2004.

R. Tarjan, Enumeration of the Elementary Circuits of a Directed Graph, SIAM Journal on Computing, vol.2, issue.3, pp.211-216, 1973.
DOI : 10.1137/0202017

J. M. Tendler, J. Steve-dodson, J. S. Fields-jr, H. Le, and B. Sinharoy, POWER4 system microarchitecture, POWER4 system microarchitecture, pp.5-26, 2002.
DOI : 10.1147/rd.461.0005

E. Torlak, M. Vaziri, and J. Dolby, MemSAT: Checking axiomatic specifications of memory models, Proceedings of PLDI, pp.341-350, 2010.

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

F. Zappa-nardelli, P. Sewell, J. Sevcik, S. Sarkar, S. Owens et al., Relaxed memory models must be rigorous, Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC) 2, 2009.