MoRDor Manual

1. Introduction

MoRDor is a tool for exploring weak memory. You give it a concurrent program as a litmus test, and it computes the program's justified executions. Each one is a way the program's reads and writes can resolve when memory is relaxed. It is backed by justifications that say what every write in it depends on. A memory model then decides which of these executions are coherent.

Every execution carries the justifications it was built from. MoRDor can therefore tell you why an outcome is allowed, not just whether it is: which reads a write really depends on, which accesses a compiler could reorder or forward, and which synchronisation rules out the rest.

MoRDor implements Symbolic MRD (Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice, Richards, Wright, Cooksey and Batty, OOPSLA 2025). It adds a check for episodic loops and a use-after-free analysis. Values are symbolic, so one execution stands for every run that resolves the same way, whatever the concrete values.

This manual covers the concepts behind MoRDor, the web UI, and the litmus test language.

2. Concepts

Events and event structures

MoRDor interprets a program as an event structure: one event for every memory access and control point the program can perform, however it runs. An event is written label:type location value, as in 3:R x α or 4:W y 1.

Values are symbolic. A read does not read a number: it reads a fresh symbol, written as a Greek letter (α, β, …). An allocation returns a symbolic address, written as a CJK numeral (一, 二, …). Constraints on those symbols decide which values they take.

Events are ordered by program order (po), the order the source imposes within a thread. Where a program branches, the events on the two sides are in conflict: no execution contains both.

Justifications

A justification for a write says which reads the write depends on, and under what condition. Initially a write depends on every read its value or location mentions. Elaborations then derive further justifications that depend on less:

• Value assignment replaces a symbol by the value the condition forces, so the write no longer depends on the read that produced it.
• Forwarding lets a read take its value directly from an earlier write in the same thread, so the read is no longer performed. Write elision removes a write that a later write overwrites before anything reads it. Neither applies to a volatile access, or to the read or write of a cas or fadd: those are always performed, and an update's read reads from memory, which is what keeps it atomic.
• Lifting merges justifications that hold on both sides of a branch, so the write no longer depends on what the branch tested.
• Weakening drops the parts of a justification's condition that the program's de facto guarantees already imply.

Together these capture what an optimising compiler may do to a program. A dependency that survives every elaboration is a real one, and the justification set is everything the elaborations derive for the program. The web UI shows the set with the elaboration step behind each justification (see Graph controls).

Justified executions

An execution chooses one side of every branch, one justification for every write, and for every read the write it reads from. It records:

An execution also carries predicates: the conditions of the branches it takes, and the equalities its rf edges impose on symbols. It must be complete, meaning every read reads from some write, and free of thin air: dp ∪ ppo ∪ rf may not have a cycle. A cycle would mean a value justified only by itself.

Memory models and coherence

Justified executions describe what relaxed memory permits. A memory model says which of them a platform or language standard admits. MoRDor admits an execution under a model when some coherence order co satisfies the model's axioms.

Every model is a check on the executions MoRDor generates. Those are free of thin air unless a model of the run allows it, as only c11, c17, c20, wasm and jam do; then the other models reject the thin-air executions themselves. The names follow the Relaxed Memory Model Zoo; a name with a hyphen, such as [x86-TSO], is written as the zoo spells it. Each model name in the table links to its page in the zoo.

Promising semantics is operational rather than axiomatic. A thread may promise a write before it reaches it, other threads may read the promise, and the promise stands only if the thread can be certified to fulfil it running alone. So ps1 and ps2 compute their own executions, one per distinct outcome, instead of checking sMRD's. An execution's relations are those promising defines: rf, which message each read took, and co, the order of timestamps per location. dp and ppo are sMRD's and have no counterpart. Loops need the step counter. A test annotated [PS1] or [PS2] runs under that version; [Promising] names none and needs one chosen. On the command line, --semantics ps1 or ps2 chooses it for a whole run.

A test names its model in its assertion, as in forbid (…) [RC11], or several, as in forbid (…) [RA, SRA]. Some names map onto a model: [Power] onto IMM, and [UB11], [RC11UB] and [IMMUB] also allow the undefined-behaviour fold e / !r → e. An unknown model name is an error. [_] means any model.

Assertions

allow C holds when some admitted execution satisfies C. forbid C holds when none does. Conditions can mention registers, final values of memory (@x is the value finally stored at x), and an execution's relations, as in (3,2) ∈ .co or (1,4) ∈ .rf. A refinement chain ~~> compares the observable behaviours of two programs.

MoRDor reports assertion instances that explain the verdict:

Loops and episodicity

A loop can be explored in two ways. Under step-counter semantics MoRDor unrolls each loop a fixed number of times, and the executions are those of the bounded program. Under symbolic loop semantics one iteration stands for all of them.

The episodicity analysis checks whether a loop is episodic: whether each iteration behaves as an independent episode, so that analysing one iteration is enough for any number of them. It checks four conditions, and reports which fail and where:

1. Register condition: how the iteration accesses registers
2. Write condition: which writes a read in the loop may read from
3. Branching condition: what the loop's branching conditions pin down
4. Events condition: how events are ordered across iterations

The analysis always interprets loops symbolically, whichever loop semantics the settings choose.

Use-after-free

An execution exhibits a use-after-free when it accesses a location that a deallocation frees, and nothing orders the access before the deallocation: no chain of dp, ppo and rf edges leads from the access to the free. Program order alone does not count, since relaxed memory does not preserve it. Which executions exist depends on the memory model, so a program can be free of use-after-free under RC11 and exhibit one under sMRD.

An unbounded pointer dereference is the counterpart for allocations: an access through a pointer to allocated memory that nothing orders after the allocation.

Both are sMRD's. Under promising semantics there is no use-after-free; what counts as undefined behaviour there is a dereference of something that is not an address, or a division by zero. The run aborts at that point, is reported as undefined behaviour, and has no final state for a condition to hold of.

3. Getting started

1. Pick a program from Examples… above the editor, such as Classics › MP, or type your own.
2. Press Visualize. MoRDor parses and interprets the program, derives its justifications, and computes and checks its executions. Results stream in as each stage finishes.
3. The graph panel first shows the event structure. Step through the executions with ‹ and ›.
4. Read the execution's predicates, final registers and justifications in the box at the top left of the graph.
5. Open Assertions in the Analysis sidebar for the verdict, and click an instance to jump to its execution.

x := 0; y := 0;
{
  r1 := x;
  y := 1
} ||| {
  r2 := y;
  x := 1
}
%%
allow (r1 = 0 && r2 = 0) [RC11]

Two threads each read a variable and then write the other. The assertion asks whether both reads can see the initial 0.

4. The web UI

Layout

Drag the gaps between the three columns to resize them. The theme choice is remembered in the browser.

Actions

The action button runs the program in the editor. The arrow beside it chooses which action the button runs, and marks the current one:

The status in the top bar reads Processing... while an action runs, then Complete, or Error if the run fails. The error itself appears in the log and in the graph panel. For a parse error the log quotes the offending line with a caret under the token, and the editor marks the token in red until you edit the program or run it again.

The editor

• Examples… offers programs from MoRDor's test corpus, grouped by what they illustrate: classic weak-memory tests, coherence, fences and access modes, dependencies and thin air, and programs only MoRDor can express.
• Open loads a .lit file from your computer.
• ? next to the panel title opens this manual at the language reference.

Share, in the top bar, copies a link that carries the program and the selected action. Opening the link restores both, but does not run the action. The link does not carry the settings.

Syntax is highlighted as you type.

Event structure and executions

The graph panel holds a carousel. Its first graph is the event structure. The graphs after it are the admitted executions, labelled Execution i of n at the top. Move through them with ‹ and ›.

Hover over an event to highlight the source code it came from. The log also names the event. You can drag events to rearrange the graph.

The event structure shows program order (po), plus lock order (lo) and fork-join (fj) edges where the program has them. Conflict (cf), between events on different sides of a branch, is drawn as a red zig-zag with an arrowhead at each end, since it is symmetric. Only the po-minimal pairs are drawn: those where no event before either one in program order conflicts with the other. Every other conflict follows from these, as the events after two conflicting events conflict too, up to where the threads join. An execution graph shows the execution's events and relations:

A fwd or we edge points at an event the execution does not contain: elision is what removed it. That event is drawn with a dashed outline. Fences are not drawn in executions.

Execution information

The box at the top left of the graph describes what is on screen:

Graph controls and export

Below the graph:

• Layout arranges the graph: Hierarchical (the default), fCoSE (fast, force-directed), COSE (slower, often tidier) or Circle.
• Relations chooses which kinds of edge to draw, with All and None shortcuts. The choice carries over from one execution to the next.
• Fit zooms the whole graph into view.
• Export saves the graph as you see it: the current layout, including events you dragged, and only the relations you chose to draw.
  • PNG: an image at twice screen resolution.
  • DOT: Graphviz with node positions. neato -n -Tpdf graph.dot -o graph.pdf reproduces the layout.
  • TikZ: a tikzpicture for LaTeX, with Greek letters in math mode. The file's header lists the packages it needs. Labels with allocation names need xelatex or lualatex.
• Save JSON saves the whole run: the program, every graph, and the analysis results. Load JSON (above the graph) restores a saved run without contacting the server, at the execution that was on screen.

At the bottom right, the statistics box counts the nodes and edges on screen and the executions of the run. Expand Justification set there for the program's whole justification set, each with the elaboration step that derived it.

Analysis panels

Episodicity

One entry per loop, with its source range and a verdict: ✓ Episodic, ✗ Non-episodic, ⋯ checking while the analysis runs, or — not analysed when the analysis could not evaluate the loop's conditions. Verdicts appear loop by loop as each finishes. Expand a loop to see its four conditions, and expand a failed condition for the violations and where in the source they occur. Hovering over a loop highlights it in the editor.

Assertions

The overall verdict (Valid or Invalid), then the assertion instances behind it, each with its execution, the instantiated condition, its result and any set-membership tests it made. Click an instance to show its execution.

Use-After-Free

Every execution with a use-after-free, and the pairs of events that make it one. Click an entry to show its execution, where the pairs are drawn as uaf edges.

Settings

Settings in the top bar opens the settings; beside it, a summary names the models and loop semantics the next run uses. Apply & Regenerate applies them and reruns the last program you ran.

Loop Semantics

• Step-counter semantics unrolls every loop Loop unravellings times (2 by default).
• Symbolic loop semantics interprets loops symbolically.

Memory Model

• Primary model is the model executions are shown for, and the model the assertion is checked under. Default is the model the test's assertion names, or sMRD if it names none. Choosing any other model replaces the test's own model, for every assertion the test has.
• Also compute executions under checks every execution against further models, any of those in the table above except RC11c. The primary model is greyed out here, as there is nothing to compare it with; under Default that is the model the test's first assertion names, or sMRD. The log reports how many executions each model admits. The information box lists, for the execution on screen, the compared models that also admit it.
• PS1.0 and PS2.0, under Promising (operational), compute the executions under promising semantics instead of sMRD's. As the primary model, each execution's graph shows its events with their rf and co edges; there are no justifications to show. Symbolic loops are unavailable while either is the primary or a compared model.

Execution Filtering

Show executions with use-after-free and Show executions with unbounded pointer dereference are sent with each request, but the server does not act on them yet. Every admitted execution is shown whichever way they are set.

Test runner

Tests opens the test runner over MoRDor's corpus. Tests are listed in three trees: Litmus Tests (litmus-tests/), Episodicity Tests (programs/episodicity/) and Programs (programs/).

• Filter tests… narrows the trees by path.
• ▶ next to a test runs it. ▶ Run All Tests runs every litmus and episodicity test in turn.
• A litmus test's result shows whether its assertion is valid, how many executions it has, and whether it has undefined behaviour. An episodicity test's shows how many loops were analysed and whether all are episodic. A directory is marked ✓ when every result in it passed.
• Click a test for its output and source, each with 📋 Copy. 📝 Load in Editor puts the source in the editor and selects the matching action.
• 🔄 Refresh reloads the lists, 🗑️ Clear Results forgets results, and 📊 View Summary returns to the overview of results.

The test runner runs each test under the model its assertion names, not the settings.

Log

The log at the bottom of the page records each step of a run as it arrives: the stages, the executions received, per-model counts when models are compared, and settings changes. Errors are shown in red: a program that does not parse, a model name MoRDor does not know, a failure anywhere in the pipeline, or a run that ended without completing.

5. Common tasks

Is an outcome allowed?

Write the outcome as an assertion: allow (r1 = 1 && r2 = 0) [RC11]. Run Visualize and open Assertions. For allow, a Witnessed instance is an execution that produces the outcome. For forbid, a Contradicted instance is one that should not exist. Click it to see the execution.

Why is an execution allowed?

Show the execution, then:

1. Read its Predicates and Final registers to see which outcome it is.
2. Use Relations to draw only rf, dp and ppo. A read that sees an old value is one whose rf edge crosses a later write that nothing in dp or ppo orders before it.
3. Press the Justifications button for what each write depends on. A write with fewer dependencies than its source suggests got them removed by an elaboration. The Justification set in the statistics box names the step.
4. Turn on fwd and we to see reads that were forwarded and writes that were elided.

Which models allow an execution?

In Settings, choose a primary model and tick the models to compare. Executions of the primary model the others also admit say so under Also allowed by. An execution that lists no other model is one only the primary admits: on load buffering with sMRD as primary and RC11 compared, those are exactly the load-buffering witnesses RC11 rules out. To step through just those, press the funnel button beside Also allowed by.

Is a loop episodic?

Choose the Episodicity action, or run Visualize, and open Episodicity. A failed condition lists its violations with source positions. Hover over the loop to find it in the editor.

Does a program use memory after freeing it?

Run Visualize and open Use-After-Free. Each entry is an execution and its offending pairs. In the graph they are uaf edges. An access that synchronisation should order before the free, but does not, typically lacks a release or acquire annotation. Compare MoRDor only › Use after free with Use after free (fixed) in the examples.

A figure for a paper

Show the execution, choose a layout, drag events where you want them, and use Relations to draw only what the figure needs. Then Export › TikZ. The figure keeps the positions and relations on screen.

Keeping a result

Share gives a link to the program, to rerun later. Save JSON keeps the computed run itself, which Load JSON reopens without recomputing.

6. Command line

The pipeline behind the web UI is also available from the mordor command. mordor --help lists its commands and options.

mordor run --single test.lit
mordor run --all-litmus-tests litmus-tests -r

The web server's HTTP API is described in web/README.md in the MoRDor repository.

7. Language reference

The rest of this manual describes the litmus test language.

Overview

A litmus test states a concurrent program, whose justified executions MoRDor explores, and an assertion about the outcomes it may have. The program consists of threads performing memory operations.

Litmus Test Structure

A complete litmus test has three optional parts:

// Optional configuration
name = TestName
model = rc11
values = {0, 1, 2}
[de facto guarantees]
[[constraints]]
%%

// Program (required), optionally initialising memory first
x := 0;
{ thread1_statements } ||| { thread2_statements }

// Optional assertion
%%
allow final_condition [model]

Configuration Section

The configuration section appears before the program and is terminated by %%.

Name Declaration

name = StorBuffering
name = "Message Passing Test"

Model Selection

model = rc11
model = smrd
model = imm

Values Domain

Specify the set of possible values for variables:

values = {0, 1, 2, 3}
values = {0x0, 0x10, 0xFF}

De Facto Guarantees

Facts that hold in every run of the program, as expressions in square brackets. Weakening may drop the part of a justification's condition these imply. They do not initialise memory: to give a location an initial value, write it before the threads, as in x := 0;.

[x = 0]
[y = 0]
[ptr = 0]

Constraints

Add constraints using double square brackets:

[[x != y]]
[[ptr != 0]]

Variables and Identifiers

Registers

Registers start with r followed by alphanumeric characters:

r0, r1, r2, rax, rtmp, rResult

Global Variables

Global variables start with a letter and contain alphanumeric characters:

x, y, flag, data, pointer

A program touches a global only through a load or a store, and each is an event of its own. A global cannot appear in an expression: load it into a register first, as in r0 := x; r1 := r0 + 1, not r1 := x + 1. Its address is taken only by a reference, r0 := &x, and a pointer held in a global is loaded into a register before it is used. A program that breaks these rules is refused with a parse error.

AtLoc Variables

Special variables prefixed with @, used in assertions to name the value at a location:

@x, @thread1, @location

Labels

Labels are enclosed in backticks and used to mark statements:

`label1` r0 := x;
`critical` *rp := 1;

Statements

Register Assignment

// Register to register
r0 := r1;

// Register from an expression over registers
r0 := r1 + 1;

// Reference: the address of global x
r0 := &x;

A reference is the only way to take an address, and it is not an event. Store it, dereference it, or pass it to cas or fadd through the register.

Skip Statement

skip;

Parallel Threads

Use ||| to separate parallel threads:

{ r0 := x; y := 1 } ||| { r1 := y; x := 1 }

Memory Operations

Loads

From Global Variables

From Pointers

The address is an expression over registers: a reference, a pointer from malloc, or a pointer loaded from memory, optionally with an offset, as in *(rp + 1).

Stores

To Global Variables

To Pointers

Allocation

The size is not used, and offsets into an allocation are assumed not to reach another object. free takes a register: to free a pointer held in a global, load it first, r0 := x; free(r0).

Memory Orders

Atomic Operations

Compare-and-Swap (CAS)

Atomically compares the value at an address with an expected value and, if they are equal, stores the desired value. The register is set to 1 if the swap happened and 0 if it did not. As for every expression in a program, the address, expected and desired values are over registers: to swap a global, pass a reference to it.

r0 := cas(load_order, store_order, address, expected, desired)

// Basic CAS on global x
rx := &x;
r0 := cas(relaxed, relaxed, rx, 0, 1);

// With acquire/release, through a pointer
r1 := cas(acquire, release, rp, r2, r3);

// Sequential consistency
r0 := cas(sc, sc, rx, 0, 1);

Fetch-and-Add (FADD)

Atomically adds the operand to the value at an address. The register is set to the sum, the value written. The address and operand are over registers, as for cas:

r0 := fadd(rmw_mode, load_order, store_order, address, operand)

r0 := fadd(load_order, store_order, address, operand)

// Basic FADD on global counter
rc := &counter;
r0 := fadd(relaxed, relaxed, rc, 1);

// With strong semantics
r1 := fadd(strong, acquire, release, rc, 5);

// Normal semantics
r2 := fadd(normal, relaxed, relaxed, rc, -1);

Fences

Memory fence/barrier operations:

fence(relaxed);
fence(acquire);
fence(release);
fence(sc);

Locks

// Global lock operations
lock mutex;
unlock mutex;

// Default unnamed lock
lock;
unlock;

Control Flow

If-Else Statements

// Single statement
if (r0 = 1) r1 := 2;

// Block
if (r0 != 0) {
    r1 := x;
    y := r1
}

// With else
if (r0 > 0) {
    x := 1
} else {
    x := 0
}

While Loops

// Single statement
while (r0 < 10) r0 := r0 + 1;

// Block: a condition over a global needs a load into a register
r0 := flag;
while (r0 = 0) {
    r0 := flag
}

Do-While Loops

do {
    r0 := r0 + 1;
    x := r0
} while (r0 < 10)

Expressions

In a program, an expression is over registers and constants: a global is loaded into a register first, and an address is taken only by r0 := &x. Assertions are not programs, and their expressions may also name globals, @ locations and sets.

Arithmetic Operators

Comparison Operators

Logical Operators

Bitwise Operators

Set Operators

Special Operators

Literals

// Decimal integers
0, 1, 42, 255

// Hexadecimal integers
0x0, 0x10, 0xFF, 0xDEADBEEF

// Booleans: allow (true) asks whether the model admits any execution
true, false

// Strings
"message", "test name"

// Set literals (with dot or quote prefix)
.'eventset'
'eventset'
.name

Assertions

Assertions specify expected outcomes of litmus tests. They appear after the %% delimiter.

Simple Outcome Assertions

%%
allow r0 = 0 && r1 = 0

%%
forbid r0 = 1 && r1 = 1

Model-Specific Assertions

%%
allow r0 = 0 && r1 = 0 [rc11]

%%
forbid r0 = 1 && r1 = 1 [smrd]

Several Models

An assertion can name several models, and a test can have several assertions, one per line. Each assertion is checked under each model it names, and the test is valid when every one holds. Executions are enumerated once and each model checks them, so the models of one test must agree on the undefined-behaviour fold. PS1 and PS2 compute executions of their own: naming one beside a coherence model, as in allow (…) [RC11, PS1], runs both, and each verdict is its own model's. --semantics chooses one semantics for every assertion. The first model named is the one executions are shown for.

%%
allow (r0 = 1 && r1 = 2 && r2 = 1) [WRA, CC]
forbid (r0 = 1 && r1 = 2 && r2 = 1) [RA, SRA, SC, RC11]

Chained Assertions

Test the same program under different models:

%%
~~> allow [rc11] %%
// Another test definition here

Model-Only Assertions

%%
[rc11]

%%
[smrd]

Which model an assertion is checked under in the web UI, and how to compare models, is described under Settings.

Complete Examples

Store Buffering (SB)

name = SB
model = rc11
%%

x := 0; y := 0;
{ x := 1; r0 := y } ||| { y := 1; r1 := x }

%%
allow r0 = 0 && r1 = 0

Message Passing (MP)

name = MP
model = rc11
%%

data := 0; flag := 0;
{
    data := 1;
    flag :rel= 1
} ||| {
    r0 :acq= flag;
    r1 := data
}

%%
forbid r0 = 1 && r1 = 0

Load Buffering (LB)

name = LB
model = rc11
%%

// RC11 forbids load buffering; under model = smrd it is allowed
x := 0; y := 0;
{ r0 := x; y := 1 } ||| { r1 := y; x := 1 }

%%
forbid r0 = 1 && r1 = 1

CAS Example

name = CAS_Test
model = rc11
%%

m := 0;
rm := &m;
{
    // r0 is 1 if this thread's swap happened, 0 if not
    r0 := cas(acquire, release, rm, 0, 1)
} ||| {
    r1 := cas(acquire, release, rm, 0, 1)
}

%%
forbid r0 = 1 && r1 = 1

Pointer Operations

name = PointerTest
model = rc11
%%

x := 0; ptr := 0;
{
    rp := malloc(4);
    *rp := 42;
    ptr := rp;
    x := 1
} ||| {
    r0 := x;
    if (r0 = 1) {
        rq := ptr;
        r1 := *rq
    }
}

%%
allow r0 = 1 && r1 = 42

Loop Example

name = SpinLock
model = rc11
%%

flag := 0;
{
    flag :rel= 1
} ||| {
    r0 :acq= flag;
    while (r0 = 0) {
        r0 :acq= flag
    };
    r1 := flag
}

%%
allow r1 = 1

Quick Reference Card

Additional Resources

For more information about weak memory models and litmus testing:

• RC11: The C11 Relaxed Memory Model
• C11 Standard: ISO/IEC 9899:2011
• Memory Model Papers and Research