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]

The same analysis runs from the command line:

A recording of a terminal running the MoRDor CLI on the same program: mordor interpret prints the symbolic event structure; mordor run reports 14 events, 3 executions, Valid: true and Undefined Behavior: true, one execution freeing the cell another thread is still reading; diff -u against the fixed program shows the one changed line, the relaxed store *rcu := 0 becoming the release store *rcu :rel= 0, plus an added forbid (ub) assertion; mordor run on the fixed program reports Undefined Behavior: false with fewer executions; finally mordor visual-es with --output-mode dot exports an event structure as a Graphviz digraph.
The same use-after-free found and fixed with the CLI, every command really run. [fig2]

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