Searching for pedagogical materials on memory models

Source: Lobsters Published: 11/11/2026, 03:51:19 Developers Reprinted 中文

Summary

Hi folks, I'm working on some supplementary materials for a course I'm TAing, my university's version of operating systems, that involves students developing an OS targeting a Raspberry Pi 3B+. One of the topics I'm trying to get at is strong and weak memory models (and why ARM has so many weird data/instruction buffer synchronization things students have to do when writing an MMU), so if you have any excellent example articles/passages/blogs on memory models that have helped you, please comment them so I can take a look! Thanks!

Original text(via Lobsters)

16 Searching for pedagogical materials on memory models ☶ ask osdev authored by spoonmilk 2026-11-10 13:51:19 | 7 comments

Searching for pedagogical materials on memory models

I'm working on some supplementary materials for a course I'm TAing, my university's version of operating systems, that involves students developing an OS targeting a Raspberry Pi 3B+. One of the topics I'm trying to get at is strong and weak memory models (and why ARM has so many weird data/instruction buffer synchronization things students have to do when writing an MMU), so if you have any excellent example articles/passages/blogs on memory models that have helped you, please comment them so I can take a look!

8 orib edited 2026-11-10 14:45:57 The classic is still relevant, and ties the semantics of memory models to why you may want to implement it that way in hardware quite effectively: https://shiftleft.com/mirrors/www.hpl.hp.com/techreports/Compaq-DEC/WRL-95-7.pdf I also think that the writeups that rsc did when updating the Go memory model are quite well presented: https://research.swtch.com/mm And, while I haven't rewatched it, I seem to remember this was also quite good: https://learning.acm.org/techtalks/multicore 3 polywolf 2026-11-10 17:41:02 unfortunately all the material i learned from that would be most relevant is locked behind a university login wall now :( if you'd take related things as inspiration instead: i wrote a short blog series that is tangentially related (about mutexes, which ends up talking about memory models) while that knowledge was still fresh, with a beginner-ish audience in mind: https://wolfgirl.dev/blog/2064554/ https://wolfgirl.dev/blog/2091838/ https://faultlore.com/blah/tower-of-weakenings/ (and prior article https://faultlore.com/blah/fix-rust-pointers/) helped me understand that memory models don't just affect hardware, but legal transformations in software too https://www.cs.umd.edu/~pugh/java/memoryModel/AlphaReordering.html and the wikipedia page https://en.wikipedia.org/wiki/Consistency_model#Relaxing_read_and_read_to_write_program_orders:_Alpha,_RMO,_and_PowerPC are full of very cursed examples of memory models, not great as introductory material tho ~ juliaaa 2026-11-10 19:47:57 UNSW's Adv. Operating Systems Course has a lecture on memory models: https://cgi.cse.unsw.edu.au/~cs9242/26/lectures.shtml (Week 4 Tuesday). Wk 8 Thu/Wk9 Tue night also be relevant. ~ juliaaa edited 2026-11-10 20:55:01 Added from a colleague: The slides and notes from the University of Cambridge's master-level course, and also slides from MPI-SWS's course. Regarding MMU synchronisation: It is beyond the scope of all existing lecture materials that I am aware of. It only appears in the ESOP paper http://arxiv.org/abs/2203.00642 and the casemate paper of EuroSys'27. ~ bgamari edited 2026-11-11 21:59:26 While it doesn't fill in a lot of background, "Correct and Efficient Work-Stealing for Weak Memory Models" (Minh Lê 2013) is a great example of designing and verifying a concurrent data structure under a weak memory model (including ARMv7's awfulness). While it is perhaps a stretch for an undergraduate course, the proofs that it sketches are a great introduction to this sort of reasoning for a more advanced reader. Also, CppMem is a great tool for understanding the implications of C++11 ordering semantics on concrete programs. The corresponding paper ("Mathematizing C++ Concurrency" Batty 2011) is a good read and may be accessible to an advanced undergraduate audience. ~ chc4 2026-11-11 00:50:43 The best resource I know of, and which I usually refer to people, is Herb Sutter's "atomic Weapons" talk recordings. https://youtu.be/A8eCGOqgvH4 https://youtu.be/KeLBd2EJLOU ~ kleidi 2026-11-11 01:48:13 Some links I go back to often: Linux kernel memory model explanation: https://raw.githubusercontent.com/torvalds/linux/refs/heads/master/tools/memory-model/Documentation/explanation.txt Chapter from Rust atomic and locks: https://mara.nl/atomics/memory-ordering.html

8 orib edited 2026-11-10 14:45:57 The classic is still relevant, and ties the semantics of memory models to why you may want to implement it that way in hardware quite effectively: https://shiftleft.com/mirrors/www.hpl.hp.com/techreports/Compaq-DEC/WRL-95-7.pdf I also think that the writeups that rsc did when updating the Go memory model are quite well presented: https://research.swtch.com/mm And, while I haven't rewatched it, I seem to remember this was also quite good: https://learning.acm.org/techtalks/multicore

The classic is still relevant, and ties the semantics of memory models to why you may want to implement it that way in hardware quite effectively: https://shiftleft.com/mirrors/www.hpl.hp.com/techreports/Compaq-DEC/WRL-95-7.pdf

I also think that the writeups that rsc did when updating the Go memory model are quite well presented: https://research.swtch.com/mm

And, while I haven't rewatched it, I seem to remember this was also quite good: https://learning.acm.org/techtalks/multicore

3 polywolf 2026-11-10 17:41:02 unfortunately all the material i learned from that would be most relevant is locked behind a university login wall now :( if you'd take related things as inspiration instead: i wrote a short blog series that is tangentially related (about mutexes, which ends up talking about memory models) while that knowledge was still fresh, with a beginner-ish audience in mind: https://wolfgirl.dev/blog/2064554/ https://wolfgirl.dev/blog/2091838/ https://faultlore.com/blah/tower-of-weakenings/ (and prior article https://faultlore.com/blah/fix-rust-pointers/) helped me understand that memory models don't just affect hardware, but legal transformations in software too https://www.cs.umd.edu/~pugh/java/memoryModel/AlphaReordering.html and the wikipedia page https://en.wikipedia.org/wiki/Consistency_model#Relaxing_read_and_read_to_write_program_orders:_Alpha,_RMO,_and_PowerPC are full of very cursed examples of memory models, not great as introductory material tho

unfortunately all the material i learned from that would be most relevant is locked behind a university login wall now :( if you'd take related things as inspiration instead:

i wrote a short blog series that is tangentially related (about mutexes, which ends up talking about memory models) while that knowledge was still fresh, with a beginner-ish audience in mind: https://wolfgirl.dev/blog/2064554/ https://wolfgirl.dev/blog/2091838/

https://faultlore.com/blah/tower-of-weakenings/ (and prior article https://faultlore.com/blah/fix-rust-pointers/) helped me understand that memory models don't just affect hardware, but legal transformations in software too

https://www.cs.umd.edu/~pugh/java/memoryModel/AlphaReordering.html and the wikipedia page https://en.wikipedia.org/wiki/Consistency_model#Relaxing_read_and_read_to_write_program_orders:_Alpha,_RMO,_and_PowerPC are full of very cursed examples of memory models, not great as introductory material tho

~ juliaaa 2026-11-10 19:47:57 UNSW's Adv. Operating Systems Course has a lecture on memory models: https://cgi.cse.unsw.edu.au/~cs9242/26/lectures.shtml (Week 4 Tuesday). Wk 8 Thu/Wk9 Tue night also be relevant. ~ juliaaa edited 2026-11-10 20:55:01 Added from a colleague: The slides and notes from the University of Cambridge's master-level course, and also slides from MPI-SWS's course. Regarding MMU synchronisation: It is beyond the scope of all existing lecture materials that I am aware of. It only appears in the ESOP paper http://arxiv.org/abs/2203.00642 and the casemate paper of EuroSys'27.

UNSW's Adv. Operating Systems Course has a lecture on memory models: https://cgi.cse.unsw.edu.au/~cs9242/26/lectures.shtml (Week 4 Tuesday). Wk 8 Thu/Wk9 Tue night also be relevant.

~ juliaaa edited 2026-11-10 20:55:01 Added from a colleague: The slides and notes from the University of Cambridge's master-level course, and also slides from MPI-SWS's course. Regarding MMU synchronisation: It is beyond the scope of all existing lecture materials that I am aware of. It only appears in the ESOP paper http://arxiv.org/abs/2203.00642 and the casemate paper of EuroSys'27.

Added from a colleague:

The slides and notes from the University of Cambridge's master-level course, and also slides from MPI-SWS's course.

Regarding MMU synchronisation:

It is beyond the scope of all existing lecture materials that I am aware of. It only appears in the ESOP paper http://arxiv.org/abs/2203.00642 and the casemate paper of EuroSys'27.

~ bgamari edited 2026-11-11 21:59:26 While it doesn't fill in a lot of background, "Correct and Efficient Work-Stealing for Weak Memory Models" (Minh Lê 2013) is a great example of designing and verifying a concurrent data structure under a weak memory model (including ARMv7's awfulness). While it is perhaps a stretch for an undergraduate course, the proofs that it sketches are a great introduction to this sort of reasoning for a more advanced reader. Also, CppMem is a great tool for understanding the implications of C++11 ordering semantics on concrete programs. The corresponding paper ("Mathematizing C++ Concurrency" Batty 2011) is a good read and may be accessible to an advanced undergraduate audience.

While it doesn't fill in a lot of background, "Correct and Efficient Work-Stealing for Weak Memory Models" (Minh Lê 2013) is a great example of designing and verifying a concurrent data structure under a weak memory model (including ARMv7's awfulness). While it is perhaps a stretch for an undergraduate course, the proofs that it sketches are a great introduction to this sort of reasoning for a more advanced reader.

Also, CppMem is a great tool for understanding the implications of C++11 ordering semantics on concrete programs. The corresponding paper ("Mathematizing C++ Concurrency" Batty 2011) is a good read and may be accessible to an advanced undergraduate audience.

~ chc4 2026-11-11 00:50:43 The best resource I know of, and which I usually refer to people, is Herb Sutter's "atomic Weapons" talk recordings. https://youtu.be/A8eCGOqgvH4 https://youtu.be/KeLBd2EJLOU

The best resource I know of, and which I usually refer to people, is Herb Sutter's "atomic Weapons" talk recordings.

https://youtu.be/A8eCGOqgvH4 https://youtu.be/KeLBd2EJLOU

~ kleidi 2026-11-11 01:48:13 Some links I go back to often: Linux kernel memory model explanation: https://raw.githubusercontent.com/torvalds/linux/refs/heads/master/tools/memory-model/Documentation/explanation.txt Chapter from Rust atomic and locks: https://mara.nl/atomics/memory-ordering.html

Some links I go back to often:

Linux kernel memory model explanation: https://raw.githubusercontent.com/torvalds/linux/refs/heads/master/tools/memory-model/Documentation/explanation.txt

Chapter from Rust atomic and locks: https://mara.nl/atomics/memory-ordering.html

The text above was extracted automatically from the source page and may miss images, tables or code blocks. The original is authoritative.

Published by Lobsters

This site only summarises and aggregates; copyright stays with the original author. Headlines and summaries follow the source — where they differ, the original wins.

Read the original ↗