Conversation

Wow, somebody had the audacity to do a formal & executable (!) memory model for the Linux kernel and they aptly named the paper „Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel“.

From the abstract: „We offer a model written in the cat language, making it not only formal, but also executable by the herd simulator.“

http://diy.inria.fr/linux/
https://paulmck.livejournal.com/

Herd is a toolsuite written in OCaml to test/simulate memory models.
https://github.com/herd/herdtools7