^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1) This document provides background reading for memory models and related
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 2) tools. These documents are aimed at kernel hackers who are interested
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 3) in memory models.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 4)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 5)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 6) Hardware manuals and models
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 7) ===========================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 8)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 9) o SPARC International Inc. (Ed.). 1994. "The SPARC Architecture
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 10) Reference Manual Version 9". SPARC International Inc.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 11)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 12) o Compaq Computer Corporation (Ed.). 2002. "Alpha Architecture
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 13) Reference Manual". Compaq Computer Corporation.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 14)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 15) o Intel Corporation (Ed.). 2002. "A Formal Specification of Intel
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 16) Itanium Processor Family Memory Ordering". Intel Corporation.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 17)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 18) o Intel Corporation (Ed.). 2002. "Intel 64 and IA-32 Architectures
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 19) Software Developer’s Manual". Intel Corporation.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 20)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 21) o Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 22) and Magnus O. Myreen. 2010. "x86-TSO: A Rigorous and Usable
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 23) Programmer's Model for x86 Multiprocessors". Commun. ACM 53, 7
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 24) (July, 2010), 89-97. http://doi.acm.org/10.1145/1785414.1785443
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 25)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 26) o IBM Corporation (Ed.). 2009. "Power ISA Version 2.06". IBM
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 27) Corporation.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 28)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 29) o ARM Ltd. (Ed.). 2009. "ARM Barrier Litmus Tests and Cookbook".
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 30) ARM Ltd.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 31)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 32) o Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 33) Derek Williams. 2011. "Understanding POWER Multiprocessors". In
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 34) Proceedings of the 32Nd ACM SIGPLAN Conference on Programming
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 35) Language Design and Implementation (PLDI ’11). ACM, New York,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 36) NY, USA, 175–186.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 37)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 38) o Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 39) Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 40) 2012. "Synchronising C/C++ and POWER". In Proceedings of the 33rd
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 41) ACM SIGPLAN Conference on Programming Language Design and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 42) Implementation (PLDI '12). ACM, New York, NY, USA, 311-322.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 43)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 44) o ARM Ltd. (Ed.). 2014. "ARM Architecture Reference Manual (ARMv8,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 45) for ARMv8-A architecture profile)". ARM Ltd.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 46)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 47) o Imagination Technologies, LTD. 2015. "MIPS(R) Architecture
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 48) For Programmers, Volume II-A: The MIPS64(R) Instruction,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 49) Set Reference Manual". Imagination Technologies,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 50) LTD. https://imgtec.com/?do-download=4302.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 51)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 52) o Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 53) Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 54) Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 55) Concurrency and ISA". In Proceedings of the 43rd Annual ACM
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 56) SIGPLAN-SIGACT Symposium on Principles of Programming Languages
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 57) (POPL ’16). ACM, New York, NY, USA, 608–621.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 58)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 59) o Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 60) Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 61) Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 62) and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 63) Principles of Programming Languages (POPL 2017). ACM, New York,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 64) NY, USA, 429–442.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 65)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 66) o Christopher Pulte, Shaked Flur, Will Deacon, Jon French,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 67) Susmit Sarkar, and Peter Sewell. 2018. "Simplifying ARM concurrency:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 68) multicopy-atomic axiomatic and operational models for ARMv8". In
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 69) Proceedings of the ACM on Programming Languages, Volume 2, Issue
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 70) POPL, Article No. 19. ACM, New York, NY, USA.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 71)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 72)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 73) Linux-kernel memory model
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 74) =========================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 75)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 76) o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 77) Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 78) Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 79) 2019. "Calibrating your fear of big bad optimizing compilers"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 80) Linux Weekly News. https://lwn.net/Articles/799218/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 81)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 82) o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 83) Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 84) Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 85) 2019. "Who's afraid of a big bad optimizing compiler?"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 86) Linux Weekly News. https://lwn.net/Articles/793253/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 87)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 88) o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 89) Alan Stern. 2018. "Frightening small children and disconcerting
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 90) grown-ups: Concurrency in the Linux kernel". In Proceedings of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 91) the 23rd International Conference on Architectural Support for
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 92) Programming Languages and Operating Systems (ASPLOS 2018). ACM,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 93) New York, NY, USA, 405-418. Webpage: http://diy.inria.fr/linux/.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 94)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 95) o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 96) Alan Stern. 2017. "A formal kernel memory-ordering model (part 1)"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 97) Linux Weekly News. https://lwn.net/Articles/718628/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 98)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 99) o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 100) Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 101) Linux Weekly News. https://lwn.net/Articles/720550/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 102)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 103) o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 104) Alan Stern. 2017-2019. "A Formal Model of Linux-Kernel Memory
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 105) Ordering" (backup material for the LWN articles)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 106) https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 107)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 108)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 109) Memory-model tooling
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 110) ====================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 111)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 112) o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 113) Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 114) 256–290. http://doi.acm.org/10.1145/505145.505149
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 115)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 116) o Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 117) Cats: Modelling, Simulation, Testing, and Data Mining for Weak
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 118) Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 119) 2014), 7:1–7:74 pages.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 120)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 121) o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 122) semantics of the weak consistency model specification language
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 123) cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 124)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 125)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 126) Memory-model comparisons
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 127) ========================
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 128)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 129) o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 130) Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 131) http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
Orange Pi5 kernel
Deprecated Linux kernel 5.10.110 for OrangePi 5/5B/5+ boards
3 Commits
0 Branches
0 Tags