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