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
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. ,
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
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
Foundations of the C++ concurrency memory model, Proc. PLDI Proc. POPL, 2008. ,
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
Reasoning about parallel architectures, 1992. ,
A formal specification of the PowerPC shared memory architecture, Scheurich, and F. Briggs. Memory access buffering in multiprocessors. In ISCA, 1986. ,
Checking Cache-Coherence Protocols with TLA+, Formal Methods in System Design, vol.22, issue.2, pp.125-131, 2003. ,
DOI : 10.1023/A:1022969405325
Power7: IBM's Next-Generation Server Processor, IEEE Micro, vol.30, issue.2, pp.7-15, 2010. ,
DOI : 10.1109/MM.2010.38
The JSR-133 cookbook for compiler writers ,
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
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. ,
Formal Specification of Memory Models, Scalable Shared Memory Multiprocessors, pp.25-42, 1991. ,
DOI : 10.1007/978-1-4615-3604-8_2
POWER5 system microarchitecture [Spa92] The SPARC Architecture Manual, IBM Journal of Research and Development, vol.49, issue.4-5 8, pp.505-522, 1992. ,
x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010. ,
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. ,