Projects

A living survey of weak memory models: 101 models spanning 47 years — hardware, programming language, distributed and transactional — and 145 relations between them, ordered by the inclusion of the behaviours they allow. Every ordering claim states how it is known, and 65 herd7 litmus tests run on every push.

A CLI and web UI for weak memory analysis of C-like programs, and the reference implementation of Symbolic Modular Relaxed Dependencies (sMRD): it parses litmus tests, calculates symbolic dependencies between memory operations, decides episodicity of unbounded loops, visualises event structures and executions, and runs symbolic verification.