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

diy.inria.fr/linux/
paulmck.livejournal.com/

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

Follow

@Kensan isn't the cat language the one where any program starting with "#!/bin/cat" is both syntactically valid and a quine?

Sign in to participate in the conversation
Octodon

Octodon is a nice general purpose instance. more