MoRDor

Symbolic weak memory analysis for C-like programs

MoRDor is a CLI and web UI tool for weak memory analysis of C-like programs. It analyses weak memory models by calculating symbolic dependencies between memory operations — parsing litmus tests, deciding episodicity of unbounded loops, visualising event structures and executions, and running symbolic verification.

A recording of the MoRDor web UI: a litmus test is typed into the source panel, in which one thread frees a pointer once it observes a flag, while the other thread reads through that pointer and then clears the flag with a relaxed store; running the analysis draws the event structure and steps through the three consistent executions MoRDor derives, with program order, preserved program order and reads-from edges drawn between the events; the Use-After-Free panel reports one execution in which the read of the freed location is ordered after the free, and selecting the finding jumps to that execution's graph; the relaxed store is then changed to a release store, and re-running leaves two executions and no use-after-free. — From a racy reclamation pattern to a use-after-free and back to a verified fix. [fig1]

It is a reference implementation of Symbolic Modular Relaxed Dependencies (sMRD), following “Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice” by Jay Richards, Daniel Wright, Simon Cooksey, and Mark Batty (OOPSLA 2025).