Fences in weak memory models (extended version)

A formal specification of Intel Itanium processor family memory ordering, October 2002. Intel Document 251429-001

Adir A, Shurek G (2002) Generating concurrent test-programs with collisions for multi-processor verification. In: HLDVT

Adir A, Attiya H, Shurek G (2003) Information-flow models for shared Memory with an application to the PowerPC architecture. In: TPDS

Adve SV, Gharachorloo K (1995) Shared memory consistency models: a tutorial. Computer 29:66–76

Ahamad M, Bazzi RA, John R, Kohli P, Neiger G (1993) The power of processor consistency. In: SPAA

Alglave J A shared memory poetics. PhD thesis, Université Paris 7 and INRIA, 26 November 2010. http://diy.inria.fr/alglave-thesis.pdf

Alglave J, Fox A, Ishtiaq S, Myreen MO, Sarkar S, Sewell P, Zappa Nardelli F (2009) The semantics of Power and ARM multiprocessor machine code. In: DAMP

Alglave J, Maranget L, Sarkar S, Sewell P (2010) Fences in weak memory models. In: CAV

Alpha Architecture Reference Manual, 4th edn (2002)

AMD64 Architecture Programmer’s Manual. Advanced Micro Devices, September 2007. (3 vols)

ARM Architecture Reference Manual (ARMv7-A and ARMv7-R), April 2008

Arvind, Maessen J-W (2006) Memory model = instruction reordering + store atomicity. In: ISCA. IEEE Comput Soc, Los Alamitos

Bertot Y, Casteran P (2004) In: Coq’Art. EATCS texts in theoretical computer science. Springer, Berlin

Boehm H-J, Adve SV (2008) Foundations of the C++ concurrency memory model. In: PLDI

Burckhardt S, Musuvathi M (2008) Effective program verification for relaxed memory models. In: CAV

Cantin J, Lipasti M, Smith J (2003) The complexity of verifying memory coherence. In: SPAA

Collier WW (1992) Reasoning about parallel architectures. Prentice Hall, New York

Hangal S, Vahia D, Manovit C, Lu J-YJ, Narayanan S (2004) TSOTool: a program for verifying memory systems using the memory consistency model. In: ISCA

Higham L, Kawash J, Verwaal N Weak memory consistency models part I: Definitions and comparisons. Technical Report98/612/03, Department of Computer Science, The University of Calgary, January 1998

Intel 64 and IA-32 Architectures Software Developer’s Manual (5 vols). Intel Corporation, March 2010. rev. 34

Lamport L (1979) How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans Comput 46(7):779–782

Landin A, Hagersten E, Haridi S (1991) Race-free interconnection networks and multiprocessor consistency. Comput Archit News 19(3):106–115

Manson J, Pugh W, Adve SV (2005) The Java memory model. In: POPL

Owens S, Sarkar S, Sewell P (2009) A better x86 memory model: x86-TSO. In: TPHOL

Power ISA version 2.06, January 2009

Sarkar S, Sewell P, Zappa Nardelli F, Owens S, Ridge T, Braibant T, Myreen M, Alglave J (2009) The semantics of x86-CC multiprocessor machine code. In: POPL

Sarkar S, Sewell P, Alglave J, Maranget L, Williams D (2011) Understanding Power multiprocessors. In: PLDI

Sewell P, Sarkar S, Owens S, Zappa Nardelli F, Myreen MO (2010) x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun ACM 53(7):89–97. (Research Highlights)

Shasha D, Snir M (1988) Efficient and correct execution of parallel programs that share memory. ACM Trans Program Lang Syst 10(2):282–312

Sparc Architecture Manual Versions 8 and 9, 1992 and 1994

Yang Y, Gopalakrishnan G, Linstrom G, Slind K (2004) Nemos: a framework for axiomatic and executable specifications of memory consistency models. In: IPDPS

Yang Y, Gopalakrishnan G, Lindstrom G (2007) UMM: an operational memory model specification framework with integrated model checking capability. In: CCPE