132 lines · plain
1This document provides background reading for memory models and related2tools. These documents are aimed at kernel hackers who are interested3in memory models.4 5 6Hardware manuals and models7===========================8 9o SPARC International Inc. (Ed.). 1994. "The SPARC Architecture10 Reference Manual Version 9". SPARC International Inc.11 12o Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture13 Reference Manual". Compaq Computer Corporation.14 15o Intel Corporation (Ed.). 2002. "A Formal Specification of Intel16 Itanium Processor Family Memory Ordering". Intel Corporation.17 18o Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures19 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 Usable23 Programmer's Model for x86 Multiprocessors". Commun. ACM 53, 724 (July, 2010), 89-97. http://doi.acm.org/10.1145/1785414.178544325 26o IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM27 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, and33 Derek Williams. 2011. "Understanding POWER Multiprocessors". In34 Proceedings of the 32Nd ACM SIGPLAN Conference on Programming35 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 33rd41 ACM SIGPLAN Conference on Programming Language Design and42 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) Architecture48 For Programmers, Volume II-A: The MIPS64(R) Instruction,49 Set Reference Manual". Imagination Technologies,50 LTD. https://imgtec.com/?do-download=4302.51 52o Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit53 Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter54 Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally:55 Concurrency and ISA". In Proceedings of the 43rd Annual ACM56 SIGPLAN-SIGACT Symposium on Principles of Programming Languages57 (POPL ’16). ACM, New York, NY, USA, 608–621.58 59o Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis,60 Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter61 Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11,62 and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on63 Principles of Programming Languages (POPL 2017). ACM, New York,64 NY, USA, 429–442.65 66o 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". In69 Proceedings of the ACM on Programming Languages, Volume 2, Issue70 POPL, Article No. 19. ACM, New York, NY, USA.71 72 73Linux-kernel memory model74=========================75 76o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel77 Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas78 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 82o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel83 Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas84 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 88o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and89 Alan Stern. 2018. "Frightening small children and disconcerting90 grown-ups: Concurrency in the Linux kernel". In Proceedings of91 the 23rd International Conference on Architectural Support for92 Programming Languages and Operating Systems (ASPLOS 2018). ACM,93 New York, NY, USA, 405-418. Webpage: http://diy.inria.fr/linux/.94 95o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and96 Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)"97 Linux Weekly News. https://lwn.net/Articles/718628/98 99o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and100 Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)"101 Linux Weekly News. https://lwn.net/Articles/720550/102 103o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and104 Alan Stern. 2017-2019. "A Formal Model of Linux-Kernel Memory105 Ordering" (backup material for the LWN articles)106 https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/107 108 109Memory-model tooling110====================111 112o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling113 Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),114 256–290. http://doi.acm.org/10.1145/505145.505149115 116o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding117 Cats: Modelling, Simulation, Testing, and Data Mining for Weak118 Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July119 2014), 7:1–7:74 pages.120 121o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and122 semantics of the weak consistency model specification language123 cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531124 125 126Memory-model comparisons127========================128 129o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun130 Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).131 http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.132