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, pp.13-24, 2008.
DOI : 10.1145/1481839.1481842

D. Amit, N. Rinetzky, T. W. Reps, M. Sagiv, and E. Yahav, Comparison Under Abstraction for Verifying Linearizability, LNCS, vol.4590, pp.477-490, 2007.
DOI : 10.1007/978-3-540-73368-3_49
URL : http://www.cs.tau.ac.il/~msagiv/cav07d.pdf

S. Burckhardt, A. Gotsman, M. Musuvathi, and H. Yang, Concurrent Library Correctness on the TSO Memory Model, LNCS, vol.2012, issue.7211, pp.87-107, 2012.
DOI : 10.1007/978-3-642-28869-2_5

C. Calcagno, M. Parkinson, and V. Vafeiadis, Modular safety checking for finegrained concurrency, SAS 2007, pp.233-238, 2007.
DOI : 10.1007/978-3-540-74061-2_15

J. Derrick, G. Schellhorn, and H. Wehrheim, Mechanically verified proof obligations for linearizability, ACM Transactions on Programming Languages and Systems, vol.33, issue.1, pp.1-4, 2011.
DOI : 10.1145/1889997.1890001

J. Derrick, G. Schellhorn, and H. Wehrheim, Verifying linearisabilty with potential linearisation points, FM 2011, pp.323-337, 2011.
DOI : 10.1007/978-3-642-21437-0_25

J. Derrick and G. Smith, A Framework for Correctness Criteria on Weak Memory Models, FM 2015, pp.178-194, 2015.
DOI : 10.1007/978-3-319-19249-9_12

J. Derrick, G. Smith, and B. Dongol, Verifying Linearizability on TSO Architectures, LNCS, vol.8739, pp.341-356, 2014.
DOI : 10.1007/978-3-319-10181-1_21
URL : http://bura.brunel.ac.uk/bitstream/2438/9719/1/Fulltext.pdf

S. Doherty, L. Groves, V. Luchangco, and M. Moir, Formal Verification of a??Practical Lock-Free Queue Algorithm, LNCS, vol.121, pp.97-114, 2004.
DOI : 10.1006/inco.1995.1134

J. Fitzpatrick, An interview with Steve Furber, Communications of the ACM, vol.54, issue.5, pp.34-39, 2011.
DOI : 10.1145/1941487.1941501
URL : http://dl.acm.org/ft_gateway.cfm?id=1941501&type=pdf

A. Gotsman, M. Musuvathi, and H. Yang, Show No Weakness: Sequentially Consistent Specifications of TSO Libraries, LNCS, vol.2012, issue.7611, pp.31-45, 2012.
DOI : 10.1007/978-3-642-33651-5_3

M. Herlihy and J. M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems, vol.12, issue.3, pp.463-492, 1990.
DOI : 10.1145/78969.78972

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

W. Reif, G. Schellhorn, K. Stenzel, and M. Balser, Structured Specifications and Interactive Proofs with KIV, Automated Deduction, pp.13-39, 1998.
DOI : 10.1007/978-94-017-0435-9_1
URL : http://www.informatik.uni-augsburg.de/swt/fmg/papers/struct_specs.ps.gz

G. Schellhorn, H. Wehrheim, and J. Derrick, A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, ACM Transactions on Computational Logic, vol.15, issue.4, pp.311-3137, 2014.
DOI : 10.1145/1122971.1122992

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

G. Smith, B. Derrick, and . Dongol, Admit Your Weakness: Verifying Correctness on TSO Architectures, FACS 2014, pp.364-383, 2014.
DOI : 10.1007/978-3-319-15317-9_22

D. J. Sorin, M. D. Hill, and D. A. Wood, A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture, 2011.

O. Travkin, A. Mütze, and H. Wehrheim, SPIN as a Linearizability Checker under Weak Memory Models, LNCS, vol.8244, pp.311-326, 2013.
DOI : 10.1007/978-3-319-03077-7_21

O. Travkin and H. Wehrheim, Handling TSO in Mechanized Linearizability Proofs, LNCS, vol.8855, pp.132-147, 2014.
DOI : 10.1007/978-3-319-13338-6_11

V. Vafeiadis, Modular fine-grained concurrency verification, 2007.