tools/memory-model/Documentation/references.txt

   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
  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
  72
  73 Linux-kernel memory model
  74 =========================
  75
  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/.
  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.