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 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 72 73 Linux-kernel memory model 74 ========================= 75 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 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/. 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 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 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 123 cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531 124 125 126 Memory-model comparisons 127 ======================== 128 129 o 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.
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.