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