V. Sarita, M. D. Adve, and . Hill, Weak Ordering -A New Definition, ISCA, pp.2-14, 1990.

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

URL : http://arxiv.org/abs/1207.7264

A. Bouajjani, E. Derevenetc, and R. Meyer, Checking and Enforcing Robustness against TSO, 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

D. Stephen and . Brookes, Full Abstraction for a Shared Variable Parallel Language, LICS, pp.98-109, 1993.

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

M. Dodds, X. Feng, M. J. Parkinson, and V. Vafeiadis, Deny-Guarantee Reasoning, ESOP, pp.363-377, 2009.
DOI : 10.1007/978-3-642-00590-9_26

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

D. Doligez and G. Gonthier, Portable, unobtrusive garbage collection for multiprocessor systems, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.70-83, 1994.
DOI : 10.1145/174675.174673

D. Doligez and X. Leroy, A concurrent, generational garbage collector for a multithreaded implementation of ML, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.113-123, 1993.
DOI : 10.1145/158511.158611

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

T. Domani, E. K. Kolodner, E. Lewis, E. E. Salant, K. Barabash et al., Implementing an On-the-Fly Garbage Collector for Java, ISMM, pp.155-166, 2000.

T. Elmas, S. Qadeer, A. Sezgin, O. Subasi, and S. Tasiran, Simplifying Linearizability Proofs with Reduction and Abstraction, TACAS, pp.296-311, 2010.
DOI : 10.1007/978-3-642-12002-2_25

T. Elmas, S. Qadeer, and S. Tasiran, A calculus of atomic actions, POPL, pp.2-15, 2009.

X. Feng, Local rely-guarantee reasoning, POPL, pp.315-327, 2009.
DOI : 10.1145/1480881.1480922

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

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.3-463, 1990.
DOI : 10.1145/78969.78972

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

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

A. Hobor, A. W. Appel, and F. Z. Nardelli, Oracle Semantics for Concurrent Separation Logic, ESOP, pp.353-367, 2008.
DOI : 10.1007/978-3-540-78739-6_27

C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems, vol.5, issue.4, pp.4-596, 1983.
DOI : 10.1145/69575.69577

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4

URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert Memory Model, Version 2, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703441

H. Liang, X. Feng, and M. Fu, A rely-guarantee-based simulation for verifying concurrent program transformations, POPL, pp.455-468, 2012.

H. Liang, X. Feng, and M. Fu, A rely-guarantee-based simulation for verifying concurrent program transformations, 2012.

A. Lochbihler, Verifying a Compiler for Java Threads, ESOP, pp.427-447, 2010.
DOI : 10.1007/978-3-642-11957-6_23

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

A. Mccreight, T. Chevalier, and A. P. Tolmach, A certified framework for compiling and executing garbage-collected languages, ICFP, pp.273-284, 2010.

T. Ridge, A Rely-Guarantee Proof System for x86-TSO, VSTTE, pp.55-70, 2010.
DOI : 10.1007/978-3-642-15057-9_4

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams, Understanding POWER multiprocessors, PLDI, pp.175-186, 2011.
DOI : 10.1145/2345156.1993520

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

J. ?ev?ík, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell, Relaxed-memory concurrency and verified compilation, POPL, pp.43-54, 2011.

J. ?ev?ík, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell, CompCertTSO, Journal of the ACM, vol.60, issue.3, p.22, 2013.
DOI : 10.1145/2487241.2487248

. Inc, . Corporate, and . Sparc, The SPARC Architecture Manual (version 9), 1994.

K. Treiber, Systems Programming: Coping with Parallelism -RJ 5118, 1986.

A. Joseph-turon and M. Wand, A separation logic for refining concurrent objects, POPL, pp.247-258, 2011.

V. Vafeiadis and M. J. Parkinson, A Marriage of Rely/Guarantee and Separation Logic, In CONCUR, pp.256-271, 2007.
DOI : 10.1007/978-3-540-74407-8_18