Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
torvalds
GitHub Repository: torvalds/linux
 Path: blob/master/tools/memory-model/Documentation/references.txt
26285 views
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, LTD.

50


51
o	Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit

52
	Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter

53
	Sewell. 2016. "Modelling the ARMv8 Architecture, Operationally:

54
	Concurrency and ISA". In Proceedings of the 43rd Annual ACM

55
	SIGPLAN-SIGACT Symposium on Principles of Programming Languages

56
	(POPL ’16). ACM, New York, NY, USA, 608–621.

57


58
o	Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis,

59
	Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter

60
	Sewell. 2017. "Mixed-size Concurrency: ARM, POWER, C/C++11,

61
	and SC". In Proceedings of the 44th ACM SIGPLAN Symposium on

62
	Principles of Programming Languages (POPL 2017). ACM, New York,

63
	NY, USA, 429–442.

64


65
o	Christopher Pulte, Shaked Flur, Will Deacon, Jon French,

66
	Susmit Sarkar, and Peter Sewell. 2018. "Simplifying ARM concurrency:

67
	multicopy-atomic axiomatic and operational models for ARMv8". In

68
	Proceedings of the ACM on Programming Languages, Volume 2, Issue

69
	POPL, Article No. 19. ACM, New York, NY, USA.

70


71


72
Linux-kernel memory model

73
=========================

74


75
o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel

76
	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas

77
	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.

78
	2019. "Calibrating your fear of big bad optimizing compilers"

79
	Linux Weekly News.  https://lwn.net/Articles/799218/

80


81
o	Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel

82
	Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas

83
	Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra.

84
	2019. "Who's afraid of a big bad optimizing compiler?"

85
	Linux Weekly News.  https://lwn.net/Articles/793253/

86


87
o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and

88
	Alan Stern.  2018. "Frightening small children and disconcerting

89
	grown-ups: Concurrency in the Linux kernel". In Proceedings of

90
	the 23rd International Conference on Architectural Support for

91
	Programming Languages and Operating Systems (ASPLOS 2018). ACM,

92
	New York, NY, USA, 405-418.  Webpage: http://diy.inria.fr/linux/.

93


94
o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and

95
	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 1)"

96
	Linux Weekly News.  https://lwn.net/Articles/718628/

97


98
o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and

99
	Alan Stern.  2017.  "A formal kernel memory-ordering model (part 2)"

100
	Linux Weekly News.  https://lwn.net/Articles/720550/

101


102
o	Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and

103
	Alan Stern.  2017-2019.  "A Formal Model of Linux-Kernel Memory

104
	Ordering" (backup material for the LWN articles)

105
	https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/

106


107


108
Memory-model tooling

109
====================

110


111
o	Daniel Jackson. 2002. "Alloy: A Lightweight Object Modelling

112
	Notation". ACM Trans. Softw. Eng. Methodol. 11, 2 (April 2002),

113
	256–290. http://doi.acm.org/10.1145/505145.505149

114


115
o	Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. "Herding

116
	Cats: Modelling, Simulation, Testing, and Data Mining for Weak

117
	Memory". ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July

118
	2014), 7:1–7:74 pages.

119


120
o	Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. "Syntax and

121
	semantics of the weak consistency model specification language

122
	cat". CoRR abs/1608.07531 (2016). https://arxiv.org/abs/1608.07531

123


124


125
Memory-model comparisons

126
========================

127


128
o	Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun

129
	Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018).

130
	http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html.

131


132