0001 This document provides background reading for memory models and related
0002 tools. These documents are aimed at kernel hackers who are interested
0003 in memory models.
0004
0005
0006 Hardware manuals and models
0007 ===========================
0008
0009 o SPARC International Inc. (Ed.). 1994. "The SPARC Architecture
0010 Reference Manual Version 9". SPARC International Inc.
0011
0012 o Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture
0013 Reference Manual". Compaq Computer Corporation.
0014
0015 o Intel Corporation (Ed.). 2002. "A Formal Specification of Intel
0016 Itanium Processor Family Memory Ordering". Intel Corporation.
0017
0018 o Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures
0019 Software Developer’s Manual". Intel Corporation.
0020
0021 o Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli,
0022 and Magnus O. Myreen. 2010. "x86-TSO: A Rigorous and Usable
0023 Programmer's Model for x86 Multiprocessors". Commun. ACM 53, 7
0024 (July, 2010), 89-97. http://doi.acm.org/10.1145/1785414.1785443
0025
0026 o IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM
0027 Corporation.
0028
0029 o ARM Ltd. (Ed.). 2009. "ARM Barrier Litmus Tests and Cookbook".
0030 ARM Ltd.
0031
0032 o Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and
0033 Derek Williams. 2011. "Understanding POWER Multiprocessors". In
0034 Proceedings of the 32Nd ACM SIGPLAN Conference on Programming
0035 Language Design and Implementation (PLDI ’11). ACM, New York,
0036 NY, USA, 175–186.
0037
0038 o Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty,
0039 Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams.
0040 2012. "Synchronising C/C++ and POWER". In Proceedings of the 33rd
0041 ACM SIGPLAN Conference on Programming Language Design and
0042 Implementation (PLDI '12). ACM, New York, NY, USA, 311-322.
0043
0044 o ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8,
0045 for ARMv8-A architecture profile)". ARM Ltd.
0046
0047 o Imagination Technologies, LTD. 2015. "MIPS(R) Architecture
0048 For Programmers, Volume II-A: The MIPS64(R) Instruction,
0049 Set Reference Manual". Imagination Technologies,
0050 LTD. https://imgtec.com/?do-download=4302.
0051
0052 o Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit
0053 Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter
0054 Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally:
0055 Concurrency and ISA". In Proceedings of the 43rd Annual ACM
0056 SIGPLAN-SIGACT Symposium on Principles of Programming Languages
0057 (POPL ’16). ACM, New York, NY, USA, 608–621.
0058
0059 o Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis,
0060 Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter
0061 Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11,
0062 and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on
0063 Principles of Programming Languages (POPL 2017). ACM, New York,
0064 NY, USA, 429–442.
0065
0066 o Christopher Pulte, Shaked Flur, Will Deacon, Jon French,
0067 Susmit Sarkar, and Peter Sewell. 2018. "Simplifying ARM concurrency:
0068 multicopy-atomic axiomatic and operational models for ARMv8". In
0069 Proceedings of the ACM on Programming Languages, Volume 2, Issue
0070 POPL, Article No. 19. ACM, New York, NY, USA.
0071
0072
0073 Linux-kernel memory model
0074 =========================
0075
0076 o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
0077 Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
0078 Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
0079 2019. "Calibrating your fear of big bad optimizing compilers"
0080 Linux Weekly News. https://lwn.net/Articles/799218/
0081
0082 o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
0083 Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
0084 Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
0085 2019. "Who's afraid of a big bad optimizing compiler?"
0086 Linux Weekly News. https://lwn.net/Articles/793253/
0087
0088 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
0089 Alan Stern. 2018. "Frightening small children and disconcerting
0090 grown-ups: Concurrency in the Linux kernel". In Proceedings of
0091 the 23rd International Conference on Architectural Support for
0092 Programming Languages and Operating Systems (ASPLOS 2018). ACM,
0093 New York, NY, USA, 405-418. Webpage: http://diy.inria.fr/linux/.
0094
0095 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
0096 Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)"
0097 Linux Weekly News. https://lwn.net/Articles/718628/
0098
0099 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
0100 Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)"
0101 Linux Weekly News. https://lwn.net/Articles/720550/
0102
0103 o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
0104 Alan Stern. 2017-2019. "A Formal Model of Linux-Kernel Memory
0105 Ordering" (backup material for the LWN articles)
0106 https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
0107
0108
0109 Memory-model tooling
0110 ====================
0111
0112 o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
0113 Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
0114 256–290. http://doi.acm.org/10.1145/505145.505149
0115
0116 o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding
0117 Cats: Modelling, Simulation, Testing, and Data Mining for Weak
0118 Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July
0119 2014), 7:1–7:74 pages.
0120
0121 o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
0122 semantics of the weak consistency model specification language
0123 cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531
0124
0125
0126 Memory-model comparisons
0127 ========================
0128
0129 o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
0130 Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
0131 http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
