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
66o	Christopher Pulte, Shaked Flur, Will Deacon, Jon French,
67	Susmit Sarkar, and Peter Sewell. 2018. "Simplifying ARM concurrency:
68	multicopy-atomic axiomatic and operational models for ARMv8". In
69	Proceedings of the ACM on Programming Languages, Volume 2, Issue
70	POPL, Article No. 19. ACM, New York, NY, USA.
71
72
73Linux-kernel memory model
74=========================
75
76o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
77	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
78	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
79	2019. "Calibrating your fear of big bad optimizing compilers"
80	Linux Weekly News.  https://lwn.net/Articles/799218/
81
82o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
83	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
84	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
85	2019. "Who's afraid of a big bad optimizing compiler?"
86	Linux Weekly News.  https://lwn.net/Articles/793253/
87
88o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
89	Alan Stern.  2018. "Frightening small children and disconcerting
90	grown-ups: Concurrency in the Linux kernel". In Proceedings of
91	the 23rd International Conference on Architectural Support for
92	Programming Languages and Operating Systems (ASPLOS 2018). ACM,
93	New York, NY, USA, 405-418.  Webpage: http://diy.inria.fr/linux/.
94
95o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
96	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 1)"
97	Linux Weekly News.  https://lwn.net/Articles/718628/
98
99o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
100	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 2)"
101	Linux Weekly News.  https://lwn.net/Articles/720550/
102
103o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
104	Alan Stern.  2017-2019.  "A Formal Model of Linux-Kernel Memory
105	Ordering" (backup material for the LWN articles)
106	https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
107
108
109Memory-model tooling
110====================
111
112o	Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
113	Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
114	256–290. http://doi.acm.org/10.1145/505145.505149
115
116o	Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding
117	Cats: Modelling, Simulation, Testing, and Data Mining for Weak
118	Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July
119	2014), 7:1–7:74 pages.
120
121o	Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
122	semantics of the weak consistency model specification language
123	cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531
124
125
126Memory-model comparisons
127========================
128
129o	Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
130	Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
131	http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
132