A Formal Model of Linux-Kernel Memory Ordering

January 22, 2020

These articles were contributed by multiple authors, including 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.

This repository contains backup materials for the LWN article on the Linux-kernel memory model:

  1. A Strong Formal Model of Linux-Kernel Memory Ordering
  2. A Weak Formal Model of Linux-Kernel Memory Ordering
  3. How herd Works
  4. Decoding the From-Read (fr) Relation
  5. RCU Guarantees
  6. The Linux-Kernel Memory Model by Example
  7. Adding SRCU to the Linux-Kernel Memory Model
  8. Adding Locking to the Linux-Kernel Memory Model