linux/tools/memory-model/Documentation/references.txt
<<
>>
Prefs
   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\xE2\x80\x99s 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 \xE2\x80\x9911). ACM, New York,
  36        NY, USA, 175\xE2\x80\x93186.
  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 \xE2\x80\x9916). ACM, New York, NY, USA, 608\xE2\x80\x93621.
  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\xE2\x80\x93442.
  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". In
  69        Proceedings of the ACM on Programming Languages, Volume 2, Issue
  70        POPL, Article No. 19. ACM, New York, NY, USA.
  71
  72
  73Linux-kernel memory model
  74=========================
  75
  76o       Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
  77        Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
  78        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, Daniel
  83        Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
  84        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, and
  89        Alan Stern.  2018. "Frightening small children and disconcerting
  90        grown-ups: Concurrency in the Linux kernel". In Proceedings of
  91        the 23rd International Conference on Architectural Support for
  92        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, and
  96        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, and
 100        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, and
 104        Alan Stern.  2017-2019.  "A Formal Model of Linux-Kernel Memory
 105        Ordering" (backup material for the LWN articles)
 106        https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/
 107
 108
 109Memory-model tooling
 110====================
 111
 112o       Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
 113        Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
 114        256\xE2\x80\x93290. http://doi.acm.org/10.1145/505145.505149
 115
 116o       Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding
 117        Cats: Modelling, Simulation, Testing, and Data Mining for Weak
 118        Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July
 119        2014), 7:1\xE2\x80\x937:74 pages.
 120
 121o       Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
 122        semantics of the weak consistency model specification language
 123        cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531
 124
 125
 126Memory-model comparisons
 127========================
 128
 129o       Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
 130        Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
 131        http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
 132