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, 50 LTD. https://imgtec.com/?do-download=4302. 51 52o 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 59o 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 67Linux-kernel memory model 68========================= 69 70o Andrea Parri, Alan Stern, Luc Maranget, Paul E. McKenney, 71 and Jade Alglave. 2017. "A formal model of 72 Linux-kernel memory ordering - companion webpage". 73 http://moscova.inria.fr/∼maranget/cats7/linux/. (2017). [Online; 74 accessed 30-January-2017]. 75 76o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and 77 Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)" 78 Linux Weekly News. https://lwn.net/Articles/718628/ 79 80o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and 81 Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)" 82 Linux Weekly News. https://lwn.net/Articles/720550/ 83 84 85Memory-model tooling 86==================== 87 88o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling 89 Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002), 90 256–290. http://doi.acm.org/10.1145/505145.505149 91 92o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding 93 Cats: Modelling, Simulation, Testing, and Data Mining for Weak 94 Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July 95 2014), 7:1–7:74 pages. 96 97o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and 98 semantics of the weak consistency model specification language 99 cat". CoRR abs/1608.07531 (2016). http://arxiv.org/abs/1608.07531 100 101 102Memory-model comparisons 103======================== 104 105o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun 106 Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016). 107 http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html. 108