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

Herd is a toolsuite written in OCaml to test/simulate memory models.


@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 is a nice general purpose instance. more