[linux-block.git] / tools / memory-model / Documentation / references.txt

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, Will Deacon, Boqun Feng, David Howells, Daniel
	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
	2019. "Calibrating your fear of big bad optimizing compilers"
	Linux Weekly News.  https://lwn.net/Articles/799218/

o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel
	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas
	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.
	2019. "Who's afraid of a big bad optimizing compiler?"
	Linux Weekly News.  https://lwn.net/Articles/793253/

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/

o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and
	Alan Stern.  2017-2019.  "A Formal Model of Linux-Kernel Memory
	Ordering" (backup material for the LWN articles)
	https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/


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). https://arxiv.org/abs/1608.07531


Memory-model comparisons
========================

o	Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
	Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
	http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.
Commit	Line	Data
1c27b644 PM	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
99c12749 AP	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
1c27b644 PM	72
	73	Linux-kernel memory model
	74	=========================
	75
38908de9 PM	76	o 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
	82	o 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
1a00b455 AP	88	o 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/.
1c27b644 PM	94
	95	o 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
	99	o 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
38908de9 PM	103	o 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
1c27b644 PM	108
	109	Memory-model tooling
	110	====================
	111
	112	o Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling
	113	Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),
	114	256–290. http://doi.acm.org/10.1145/505145.505149
	115
	116	o 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–7:74 pages.
	120
	121	o Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and
	122	semantics of the weak consistency model specification language
1e44e6e8	123	cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531
1c27b644 PM	124
	125
	126	Memory-model comparisons
	127	========================
	128
	129	o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun
38908de9 PM	130	Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).
38908de9 PM	131	http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.