Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 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 | |
Andrea Parri | 99c1274 | 2018-05-14 16:33:57 -0700 | [diff] [blame] | 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 | |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 72 | |
| 73 | Linux-kernel memory model |
| 74 | ========================= |
| 75 | |
Andrea Parri | 1a00b455 | 2018-05-14 16:33:56 -0700 | [diff] [blame] | 76 | o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and |
| 77 | Alan Stern. 2018. "Frightening small children and disconcerting |
| 78 | grown-ups: Concurrency in the Linux kernel". In Proceedings of |
| 79 | the 23rd International Conference on Architectural Support for |
| 80 | Programming Languages and Operating Systems (ASPLOS 2018). ACM, |
| 81 | New York, NY, USA, 405-418. Webpage: http://diy.inria.fr/linux/. |
Paul E. McKenney | 1c27b64 | 2018-01-18 19:58:55 -0800 | [diff] [blame] | 82 | |
| 83 | o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and |
| 84 | Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)" |
| 85 | Linux Weekly News. https://lwn.net/Articles/718628/ |
| 86 | |
| 87 | o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and |
| 88 | Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)" |
| 89 | Linux Weekly News. https://lwn.net/Articles/720550/ |
| 90 | |
| 91 | |
| 92 | Memory-model tooling |
| 93 | ==================== |
| 94 | |
| 95 | o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling |
| 96 | Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002), |
| 97 | 256–290. http://doi.acm.org/10.1145/505145.505149 |
| 98 | |
| 99 | o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding |
| 100 | Cats: Modelling, Simulation, Testing, and Data Mining for Weak |
| 101 | Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July |
| 102 | 2014), 7:1–7:74 pages. |
| 103 | |
| 104 | o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and |
| 105 | semantics of the weak consistency model specification language |
| 106 | cat". CoRR abs/1608.07531 (2016). http://arxiv.org/abs/1608.07531 |
| 107 | |
| 108 | |
| 109 | Memory-model comparisons |
| 110 | ======================== |
| 111 | |
| 112 | o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun |
| 113 | Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016). |
| 114 | http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html. |