diff options
Diffstat (limited to 'tools/memory-model/Documentation/references.txt')
| -rw-r--r-- | tools/memory-model/Documentation/references.txt | 114 |
1 files changed, 114 insertions, 0 deletions
diff --git a/tools/memory-model/Documentation/references.txt b/tools/memory-model/Documentation/references.txt new file mode 100644 index 000000000..b177f3e4a --- /dev/null +++ b/tools/memory-model/Documentation/references.txt @@ -0,0 +1,114 @@ +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. |