1 This document provides background reading for 1 This document provides background reading for memory models and related
2 tools. These documents are aimed at kernel ha 2 tools. These documents are aimed at kernel hackers who are interested
3 in memory models. 3 in memory models.
4 4
5 5
6 Hardware manuals and models 6 Hardware manuals and models
7 =========================== 7 ===========================
8 8
9 o SPARC International Inc. (Ed.). 1994. 9 o SPARC International Inc. (Ed.). 1994. "The SPARC Architecture
10 Reference Manual Version 9". SPARC Int 10 Reference Manual Version 9". SPARC International Inc.
11 11
12 o Compaq Computer Corporation (Ed.). 200 12 o Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture
13 Reference Manual". Compaq Computer Co 13 Reference Manual". Compaq Computer Corporation.
14 14
15 o Intel Corporation (Ed.). 2002. "A Form 15 o Intel Corporation (Ed.). 2002. "A Formal Specification of Intel
16 Itanium Processor Family Memory Orderi 16 Itanium Processor Family Memory Ordering". Intel Corporation.
17 17
18 o Intel Corporation (Ed.). 2002. "Intel 18 o Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures
19 Software Developer’s Manual". Intel 19 Software Developer’s Manual". Intel Corporation.
20 20
21 o Peter Sewell, Susmit Sarkar, Scott Owe 21 o Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli,
22 and Magnus O. Myreen. 2010. "x86-TSO: 22 and Magnus O. Myreen. 2010. "x86-TSO: A Rigorous and Usable
23 Programmer's Model for x86 Multiproces 23 Programmer's Model for x86 Multiprocessors". Commun. ACM 53, 7
24 (July, 2010), 89-97. http://doi.acm.or 24 (July, 2010), 89-97. http://doi.acm.org/10.1145/1785414.1785443
25 25
26 o IBM Corporation (Ed.). 2009. "Power IS 26 o IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM
27 Corporation. 27 Corporation.
28 28
29 o ARM Ltd. (Ed.). 2009. "ARM Barrier Lit 29 o ARM Ltd. (Ed.). 2009. "ARM Barrier Litmus Tests and Cookbook".
30 ARM Ltd. 30 ARM Ltd.
31 31
32 o Susmit Sarkar, Peter Sewell, Jade Algl 32 o Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and
33 Derek Williams. 2011. "Understanding 33 Derek Williams. 2011. "Understanding POWER Multiprocessors". In
34 Proceedings of the 32Nd ACM SIGPLAN Co 34 Proceedings of the 32Nd ACM SIGPLAN Conference on Programming
35 Language Design and Implementation (PL 35 Language Design and Implementation (PLDI ’11). ACM, New York,
36 NY, USA, 175–186. 36 NY, USA, 175–186.
37 37
38 o Susmit Sarkar, Kayvan Memarian, Scott 38 o Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty,
39 Peter Sewell, Luc Maranget, Jade Algla 39 Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams.
40 2012. "Synchronising C/C++ and POWER". 40 2012. "Synchronising C/C++ and POWER". In Proceedings of the 33rd
41 ACM SIGPLAN Conference on Programming 41 ACM SIGPLAN Conference on Programming Language Design and
42 Implementation (PLDI '12). ACM, New Yo 42 Implementation (PLDI '12). ACM, New York, NY, USA, 311-322.
43 43
44 o ARM Ltd. (Ed.). 2014. "ARM Architectur 44 o ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8,
45 for ARMv8-A architecture profile)". AR 45 for ARMv8-A architecture profile)". ARM Ltd.
46 46
47 o Imagination Technologies, LTD. 2015. " 47 o Imagination Technologies, LTD. 2015. "MIPS(R) Architecture
48 For Programmers, Volume II-A: The MIPS 48 For Programmers, Volume II-A: The MIPS64(R) Instruction,
49 Set Reference Manual". Imagination Tec 49 Set Reference Manual". Imagination Technologies,
50 LTD. https://imgtec.com/?do-download=4 50 LTD. https://imgtec.com/?do-download=4302.
51 51
52 o Shaked Flur, Kathryn E. Gray, Christop 52 o Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit
53 Sarkar, Ali Sezgin, Luc Maranget, Will 53 Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter
54 Sewell. 2016. "Modelling the ARMv8 Arc 54 Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally:
55 Concurrency and ISA". In Proceedings o 55 Concurrency and ISA". In Proceedings of the 43rd Annual ACM
56 SIGPLAN-SIGACT Symposium on Principles 56 SIGPLAN-SIGACT Symposium on Principles of Programming Languages
57 (POPL ’16). ACM, New York, NY, USA, 57 (POPL ’16). ACM, New York, NY, USA, 608–621.
58 58
59 o Shaked Flur, Susmit Sarkar, Christophe 59 o Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis,
60 Luc Maranget, Kathryn E. Gray, Ali Sez 60 Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter
61 Sewell. 2017. "Mixed-size Concurrency: 61 Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11,
62 and SC". In Proceedings of the 44th AC 62 and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on
63 Principles of Programming Languages (P 63 Principles of Programming Languages (POPL 2017). ACM, New York,
64 NY, USA, 429–442. 64 NY, USA, 429–442.
65 65
66 o Christopher Pulte, Shaked Flur, Will D 66 o Christopher Pulte, Shaked Flur, Will Deacon, Jon French,
67 Susmit Sarkar, and Peter Sewell. 2018. 67 Susmit Sarkar, and Peter Sewell. 2018. "Simplifying ARM concurrency:
68 multicopy-atomic axiomatic and operati 68 multicopy-atomic axiomatic and operational models for ARMv8". In
69 Proceedings of the ACM on Programming 69 Proceedings of the ACM on Programming Languages, Volume 2, Issue
70 POPL, Article No. 19. ACM, New York, N 70 POPL, Article No. 19. ACM, New York, NY, USA.
71 71
72 72
73 Linux-kernel memory model 73 Linux-kernel memory model
74 ========================= 74 =========================
75 75
76 o Jade Alglave, Will Deacon, Boqun Feng, 76 o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
77 Lustig, Luc Maranget, Paul E. McKenney 77 Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
78 Piggin, Alan Stern, Akira Yokosawa, an 78 Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
79 2019. "Calibrating your fear of big ba 79 2019. "Calibrating your fear of big bad optimizing compilers"
80 Linux Weekly News. https://lwn.net/Ar 80 Linux Weekly News. https://lwn.net/Articles/799218/
81 81
82 o Jade Alglave, Will Deacon, Boqun Feng, 82 o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
83 Lustig, Luc Maranget, Paul E. McKenney 83 Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
84 Piggin, Alan Stern, Akira Yokosawa, an 84 Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
85 2019. "Who's afraid of a big bad optim 85 2019. "Who's afraid of a big bad optimizing compiler?"
86 Linux Weekly News. https://lwn.net/Ar 86 Linux Weekly News. https://lwn.net/Articles/793253/
87 87
88 o Jade Alglave, Luc Maranget, Paul E. Mc 88 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
89 Alan Stern. 2018. "Frightening small 89 Alan Stern. 2018. "Frightening small children and disconcerting
90 grown-ups: Concurrency in the Linux ke 90 grown-ups: Concurrency in the Linux kernel". In Proceedings of
91 the 23rd International Conference on A 91 the 23rd International Conference on Architectural Support for
92 Programming Languages and Operating Sy 92 Programming Languages and Operating Systems (ASPLOS 2018). ACM,
93 New York, NY, USA, 405-418. Webpage: 93 New York, NY, USA, 405-418. Webpage: http://diy.inria.fr/linux/.
94 94
95 o Jade Alglave, Luc Maranget, Paul E. Mc 95 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
96 Alan Stern. 2017. "A formal kernel m 96 Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)"
97 Linux Weekly News. https://lwn.net/Ar 97 Linux Weekly News. https://lwn.net/Articles/718628/
98 98
99 o Jade Alglave, Luc Maranget, Paul E. Mc 99 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
100 Alan Stern. 2017. "A formal kernel m 100 Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)"
101 Linux Weekly News. https://lwn.net/Ar 101 Linux Weekly News. https://lwn.net/Articles/720550/
102 102
103 o Jade Alglave, Luc Maranget, Paul E. Mc 103 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
104 Alan Stern. 2017-2019. "A Formal Mod 104 Alan Stern. 2017-2019. "A Formal Model of Linux-Kernel Memory
105 Ordering" (backup material for the LWN 105 Ordering" (backup material for the LWN articles)
106 https://mirrors.edge.kernel.org/pub/li 106 https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
107 107
108 108
109 Memory-model tooling 109 Memory-model tooling
110 ==================== 110 ====================
111 111
112 o Daniel Jackson. 2002. "Alloy: A Lightw 112 o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
113 Notation". ACM Trans. Softw. Eng. Meth 113 Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
114 256–290. http://doi.acm.org/10.1145/ 114 256–290. http://doi.acm.org/10.1145/505145.505149
115 115
116 o Jade Alglave, Luc Maranget, and Michae 116 o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding
117 Cats: Modelling, Simulation, Testing, 117 Cats: Modelling, Simulation, Testing, and Data Mining for Weak
118 Memory". ACM Trans. Program. Lang. Sys 118 Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July
119 2014), 7:1–7:74 pages. 119 2014), 7:1–7:74 pages.
120 120
121 o Jade Alglave, Patrick Cousot, and Luc 121 o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
122 semantics of the weak consistency mode 122 semantics of the weak consistency model specification language
123 cat". CoRR abs/1608.07531 (2016). http 123 cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531
124 124
125 125
126 Memory-model comparisons 126 Memory-model comparisons
127 ======================== 127 ========================
128 128
129 o Paul E. McKenney, Ulrich Weigand, Andr 129 o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
130 Feng. 2018. "Linux-Kernel Memory Model 130 Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
131 http://www.open-std.org/jtc1/sc22/wg21 131 http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.