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.
|
