| This document provides background reading for memory models and related |
| tools. These documents are aimed at kernel hackers who are interested |
| in memory models. |
| |
| |
| Hardware manuals and models |
| =========================== |
| |
| o SPARC International Inc. (Ed.). 1994. "The SPARC Architecture |
| Reference Manual Version 9". SPARC International Inc. |
| |
| o Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture |
| Reference Manual". Compaq Computer Corporation. |
| |
| o Intel Corporation (Ed.). 2002. "A Formal Specification of Intel |
| Itanium Processor Family Memory Ordering". Intel Corporation. |
| |
| o Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures |
| Software Developer’s Manual". Intel Corporation. |
| |
| o Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, |
| and Magnus O. Myreen. 2010. "x86-TSO: A Rigorous and Usable |
| Programmer's Model for x86 Multiprocessors". Commun. ACM 53, 7 |
| (July, 2010), 89-97. http://doi.acm.org/10.1145/1785414.1785443 |
| |
| o IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM |
| Corporation. |
| |
| o ARM Ltd. (Ed.). 2009. "ARM Barrier Litmus Tests and Cookbook". |
| ARM Ltd. |
| |
| o Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and |
| Derek Williams. 2011. "Understanding POWER Multiprocessors". In |
| Proceedings of the 32Nd ACM SIGPLAN Conference on Programming |
| Language Design and Implementation (PLDI ’11). ACM, New York, |
| NY, USA, 175–186. |
| |
| o Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, |
| Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. |
| 2012. "Synchronising C/C++ and POWER". In Proceedings of the 33rd |
| ACM SIGPLAN Conference on Programming Language Design and |
| Implementation (PLDI '12). ACM, New York, NY, USA, 311-322. |
| |
| o ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8, |
| for ARMv8-A architecture profile)". ARM Ltd. |
| |
| o Imagination Technologies, LTD. 2015. "MIPS(R) Architecture |
| For Programmers, Volume II-A: The MIPS64(R) Instruction, |
| Set Reference Manual". Imagination Technologies, |
| LTD. https://imgtec.com/?do-download=4302. |
| |
| o Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit |
| Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter |
| Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally: |
| Concurrency and ISA". In Proceedings of the 43rd Annual ACM |
| SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
| (POPL ’16). ACM, New York, NY, USA, 608–621. |
| |
| o Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, |
| Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter |
| Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11, |
| and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on |
| Principles of Programming Languages (POPL 2017). ACM, New York, |
| NY, USA, 429–442. |
| |
| o Christopher Pulte, Shaked Flur, Will Deacon, Jon French, |
| Susmit Sarkar, and Peter Sewell. 2018. "Simplifying ARM concurrency: |
| multicopy-atomic axiomatic and operational models for ARMv8". In |
| Proceedings of the ACM on Programming Languages, Volume 2, Issue |
| POPL, Article No. 19. ACM, New York, NY, USA. |
| |
| |
| Linux-kernel memory model |
| ========================= |
| |
| o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and |
| Alan Stern. 2018. "Frightening small children and disconcerting |
| grown-ups: Concurrency in the Linux kernel". In Proceedings of |
| the 23rd International Conference on Architectural Support for |
| Programming Languages and Operating Systems (ASPLOS 2018). ACM, |
| New York, NY, USA, 405-418. Webpage: http://diy.inria.fr/linux/. |
| |
| o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and |
| Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)" |
| Linux Weekly News. https://lwn.net/Articles/718628/ |
| |
| o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and |
| Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)" |
| Linux Weekly News. https://lwn.net/Articles/720550/ |
| |
| |
| Memory-model tooling |
| ==================== |
| |
| o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling |
| Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002), |
| 256–290. http://doi.acm.org/10.1145/505145.505149 |
| |
| o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding |
| Cats: Modelling, Simulation, Testing, and Data Mining for Weak |
| Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July |
| 2014), 7:1–7:74 pages. |
| |
| o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and |
| semantics of the weak consistency model specification language |
| cat". CoRR abs/1608.07531 (2016). http://arxiv.org/abs/1608.07531 |
| |
| |
| Memory-model comparisons |
| ======================== |
| |
| o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun |
| Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016). |
| http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html. |
