Commit | Line | Data |
---|---|---|
1c27b644 PM |
1 | This document provides background reading for memory models and related |
2 | tools. These documents are aimed at kernel hackers who are interested | |
3 | in memory models. | |
4 | ||
5 | ||
6 | Hardware manuals and models | |
7 | =========================== | |
8 | ||
9 | o SPARC International Inc. (Ed.). 1994. "The SPARC Architecture | |
10 | Reference Manual Version 9". SPARC International Inc. | |
11 | ||
12 | o Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture | |
13 | Reference Manual". Compaq Computer Corporation. | |
14 | ||
15 | o Intel Corporation (Ed.). 2002. "A Formal Specification of Intel | |
16 | Itanium Processor Family Memory Ordering". Intel Corporation. | |
17 | ||
18 | o Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures | |
19 | Software Developer’s Manual". Intel Corporation. | |
20 | ||
21 | o 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 | ||
26 | o IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM | |
27 | Corporation. | |
28 | ||
29 | o ARM Ltd. (Ed.). 2009. "ARM Barrier Litmus Tests and Cookbook". | |
30 | ARM Ltd. | |
31 | ||
32 | o 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 | ||
38 | o 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 | ||
44 | o ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8, | |
45 | for ARMv8-A architecture profile)". ARM Ltd. | |
46 | ||
47 | o 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 | ||
52 | o 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 | ||
59 | o 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 | ||
99c12749 AP |
66 | o 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 | ||
1c27b644 PM |
72 | |
73 | Linux-kernel memory model | |
74 | ========================= | |
75 | ||
38908de9 PM |
76 | o 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 | ||
82 | o 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 | ||
1a00b455 AP |
88 | o 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/. | |
1c27b644 PM |
94 | |
95 | o 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 | ||
99 | o 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 | ||
38908de9 PM |
103 | o 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 | ||
1c27b644 PM |
108 | |
109 | Memory-model tooling | |
110 | ==================== | |
111 | ||
112 | o 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 | ||
116 | o 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 | ||
121 | o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and | |
122 | semantics of the weak consistency model specification language | |
1e44e6e8 | 123 | cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531 |
1c27b644 PM |
124 | |
125 | ||
126 | Memory-model comparisons | |
127 | ======================== | |
128 | ||
129 | o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun | |
38908de9 PM |
130 | Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018). |
131 | http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html. |