1This document provides background reading for memory models and related
  2tools.  These documents are aimed at kernel hackers who are interested
  3in memory models.
  4
  5
  6Hardware manuals and models
  7===========================
  8
  9o	SPARC International Inc. (Ed.). 1994. "The SPARC Architecture
 10	Reference Manual Version 9". SPARC International Inc.
 11
 12o	Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture
 13	Reference Manual".  Compaq Computer Corporation.
 14
 15o	Intel Corporation (Ed.). 2002. "A Formal Specification of Intel
 16	Itanium Processor Family Memory Ordering". Intel Corporation.
 17
 18o	Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures
 19	Software Developer’s Manual". Intel Corporation.
 20
 21o	Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli,
 22	and Magnus O. Myreen. 2010. "x86-TSO: A Rigorous and Usable
 23	Programmer's Model for x86 Multiprocessors". Commun. ACM 53, 7
 24	(July, 2010), 89-97. http://doi.acm.org/10.1145/1785414.1785443
 25
 26o	IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM
 27	Corporation.
 28
 29o	ARM Ltd. (Ed.). 2009. "ARM Barrier Litmus Tests and Cookbook".
 30	ARM Ltd.
 31
 32o	Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and
 33	Derek Williams.  2011. "Understanding POWER Multiprocessors". In
 34	Proceedings of the 32Nd ACM SIGPLAN Conference on Programming
 35	Language Design and Implementation (PLDI ’11). ACM, New York,
 36	NY, USA, 175–186.
 37
 38o	Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty,
 39	Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams.
 40	2012. "Synchronising C/C++ and POWER". In Proceedings of the 33rd
 41	ACM SIGPLAN Conference on Programming Language Design and
 42	Implementation (PLDI '12). ACM, New York, NY, USA, 311-322.
 43
 44o	ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8,
 45	for ARMv8-A architecture profile)". ARM Ltd.
 46
 47o	Imagination Technologies, LTD. 2015. "MIPS(R) Architecture
 48	For Programmers, Volume II-A: The MIPS64(R) Instruction,
 49	Set Reference Manual". Imagination Technologies,
 50	LTD. https://imgtec.com/?do-download=4302.
 51
 52o	Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit
 53	Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter
 54	Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally:
 55	Concurrency and ISA". In Proceedings of the 43rd Annual ACM
 56	SIGPLAN-SIGACT Symposium on Principles of Programming Languages
 57	(POPL ’16). ACM, New York, NY, USA, 608–621.
 58
 59o	Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis,
 60	Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter
 61	Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11,
 62	and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on
 63	Principles of Programming Languages (POPL 2017). ACM, New York,
 64	NY, USA, 429–442.
 65
 66
 67Linux-kernel memory model
 68=========================
 69
 70o	Andrea Parri, Alan Stern, Luc Maranget, Paul E. McKenney,
 71	and Jade Alglave.  2017. "A formal model of
 72	Linux-kernel memory ordering - companion webpage".
 73	http://moscova.inria.fr/∼maranget/cats7/linux/. (2017). [Online;
 74	accessed 30-January-2017].
 75
 76o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
 77	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 1)"
 78	Linux Weekly News.  https://lwn.net/Articles/718628/
 79
 80o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
 81	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 2)"
 82	Linux Weekly News.  https://lwn.net/Articles/720550/
 83
 84
 85Memory-model tooling
 86====================
 87
 88o	Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
 89	Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
 90	256–290. http://doi.acm.org/10.1145/505145.505149
 91
 92o	Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding
 93	Cats: Modelling, Simulation, Testing, and Data Mining for Weak
 94	Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July
 95	2014), 7:1–7:74 pages.
 96
 97o	Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
 98	semantics of the weak consistency model specification language
 99	cat". CoRR abs/1608.07531 (2016). http://arxiv.org/abs/1608.07531
100
101
102Memory-model comparisons
103========================
104
105o	Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
106	Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016).
107	http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html.