MLIR-MRacle

A metamorphic testing harness for OpenMP concurrency programs in MLIR.

Overview

MLIR-MRacle is a metamorphic testing tool for OpenMP MLIR programs. It applies memory model-related metamorphic relations (MRs) to transform a program, runs both the original and the transformed versions on LLJIT, and compares their outcome sets. Drastic changes in results across the source and transformed programs point to a bug in OpenMP lowering.

This project investigates a metamorphic-testing approach for concurrency and memory models, developed during an MLSystems research internship. Conventional testing assumes single-thread execution and falls short on reproducibility because of nondeterminism and varying memory models across hardware. Metamorphic relations sidestep these problems, alongside the oracle problem.

MLIR-MRacle is (afaik) the first MLIR fuzzer that can generate valid concurrent programs with respect to concurrency constructs and the native memory model, allowing the systematic exploration of a whole class of MLIR programs that was previously out of reach.

Repository layout

.
├── mlir-mracle/
│   ├── include/mlir-mracle/   # public headers
│   └── src/
│       ├── app/               # mlir_mracle_opt CLI driver
│       └── lib/
│           ├── agitation/     # perturbs modules (basic-block layout) and generates runtime configs
│           ├── backend/
│           │   ├── jit/       # JIT-compiles LLVM modules for execution
│           │   └── lowering/  # lowers MLIR to LLVM IR
│           ├── context/       # shared data structures and outcome-set types
│           ├── execution/     # runs compiled binaries and collects observed outcomes
│           ├── io/            # serializes results and dumps IR artifacts
│           ├── legacy/        # legacy thread-group oracle pipeline (--mode=legacy)
│           ├── oracle/        # compares outcome sets and derives verdicts
│           ├── pipeline/      # pipeline orchestration, emit and execution modes
│           └── passes/        # metamorphic transformation passes
├── fuzzing/
│   ├── fuzz_mracle.py         # primary campaign runner
│   └── corpus/
│       └── seeds/             # litmus-style MLIR seed programs
├── debug-progs/               # small MLIR programs for manual debugging
├── CMakeLists.txt
├── Dockerfile
└── requirements.txt

Architecture

flowchart LR
    A[Parse MLIR and clone] --> B[Apply metamorphic transforms]
    B --> C[Lower to LLVM IR]
    C --> D[Agitate clones]
    D --> E[Execute on LLJIT]
    E --> F[Compare outcome sets]

Loading

1. Parse the input module and clone it.
2. Apply one or more seeded, semantics-preserving transforms from the registry to the clone.
3. Lower both modules to LLVM IR.
4. Agitate clones and execute both sides on LLJIT.
5. Compare the observed outcome sets.

Features

• 20+ seeded metamorphic transformations (see Transforms).
• A statistical oracle over equality/subset/superset relations (see Oracle).
• An agitation sweep across codegen and runtime parameters (see Agitation sweep).
• Structured campaign output with per-run JSON reports and artifacts (see Output layout).
• Campaign checkpointing and resuming, so an interrupted campaign can be continued via --campaign-dir.
• Python runner and over 30+ litmus-style seeds in ./fuzzing/corpus/seeds.
• Extensible to any memory model; ARMv8 currently supported

Quick start

Prerequisites

• Docker, or natively: uv (provides Python 3.12, CMake, and Ninja), a C++23 compiler, and OpenMP (Homebrew libomp on Apple Silicon is auto-detected).
• LLVM/MLIR come from the mlir-wheel package pinned in requirements.txt.

Native build

uv python install 3.12
uv venv --python 3.12
uv pip install -r requirements.txt

.venv/bin/cmake -G Ninja -S . -B build -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_PREFIX_PATH=$(.venv/bin/python -m mlir_wheel --root-dir)

.venv/bin/cmake --build build --target mlir_mracle_opt -j

Tip

The Python runner builds mlir_mracle_opt for you on first use, so the native build is optional for normal use.

Docker

git clone https://github.com/dakaidan/MLIR-MRacle.git
docker build -t mlir-mracle .
docker run -it --rm mlir-mracle /bin/bash

Note

mlir_mracle-smoke is a stable Docker build target that currently just echoes configuration success.

Running MLIR-MRacle

Python runner (recommended)

.venv/bin/python fuzzing/fuzz_mracle.py fuzzing/corpus/seeds

Examples:

# single litmus test
.venv/bin/python fuzzing/fuzz_mracle.py fuzzing/corpus/seeds/iriw.mlir

# fixed seed, one random file from the corpus per run
.venv/bin/python fuzzing/fuzz_mracle.py --seed=7 --multi fuzzing/corpus/seeds

# restrict to fence transforms
.venv/bin/python fuzzing/fuzz_mracle.py --transform=insert-fence,remove-fence fuzzing/corpus/seeds/iriw.mlir

# add ARMv8-specific commutations
.venv/bin/python fuzzing/fuzz_mracle.py --model=armv8 fuzzing/corpus/seeds/iriw.mlir

# emit transformed MLIR only
.venv/bin/python fuzzing/fuzz_mracle.py --mode=emit --transform=insert-fence fuzzing/corpus/seeds/iriw.mlir

# resume an interrupted campaign
.venv/bin/python fuzzing/fuzz_mracle.py --campaign-dir=path/to/campaign fuzzing/corpus/seeds

Using the binary directly

.venv/bin/cmake --build build --target mlir_mracle_opt -j
build/mlir-mracle/src/app/mlir_mracle_opt [options] <path-to-mlir-file>

The binary prints the campaign directory on stdout and accepts the same options as the Python driver.

Options

Option	Meaning
--mode	pipeline mode(s), comma-separated: emit, execution, legacy, compare (default compare)
--model	memory model gate: empty = generic transforms only, armv8 adds ARMv8-specific ones
--reps	executions per program per thread count (default 5000)
--iter	number of pipeline repetitions (default 1)
--transform	restrict the transform set (repeat or comma-separate)
--apply	max transform applications per run
--multi	pick a random .mlir file from a folder per run
--seed	fixed RNG seed
--campaign-dir	resume/continue a campaign, or the emit-mode output directory
--threshold	novelty threshold, 0–100 (default 5)
--reruns	replay-round budget (default 5000)
--max-runs	hard cap for source runs per baseline (default 100000)
--no-cache	disable the persistent on-disk cache

See .venv/bin/python fuzzing/fuzz_mracle.py --help for the full list.

Pipeline Modes

Mode	What it does
compare (default)	compare source vs transformed under the agitation sweep and oracle
execution	execute each file as-is; no oracle comparison, .ll artifacts only
emit	apply transforms and emit the transformed MLIR only; requires --transform
legacy	legacy thread-group oracle pipeline

Environment variables

Variable	Default	Meaning
MLIR_MRACLE_BUILD_DIR	<repo>/build	Where the runner locates (and on first use builds) mlir_mracle_opt.
MLIR_MRACLE_CACHE_DIR	cache/v2	Root of the artifact cache; an explicitly empty value disables caching.

Transforms

Transforms are the seeded, semantics-preserving mutations applied to the cloned program; each one declares the outcome-set relation it preserves and the memory model it targets.

Each transform declares the outcome-set relation it preserves; a run compares in the direction given by the composition of the transforms actually applied. Transforms also declare a memory-model target, and the set of applicable transforms is resolved from the requested model (--model): generic transforms are always included, and a non-empty model adds the transforms targeting that model.

Generic concurrency transforms

Always available and valid under every memory model.

Transform	Effect	Relation
insert-fence	insert omp.flush inside a thread region	subset
remove-fence	remove a random omp.flush	superset
insert-fence-between-mem-ops	insert omp.flush between atomic memory ops	subset
insert-fence-around-seq-cst	omp.flush around a seq_cst atomic op	equality
insert-atomic-cas	no-op CAS on a fresh thread-local location	equality
insert-atomic-write	atomic write of 0 to a thread-local dummy	equality
insert-atomic-read	atomic read of an in-scope memref	equality
insert-read-arith	wrap an atomic write expr in add/sub 0	equality
insert-random-arith	fresh memref + arith chain in a thread region	equality
insert-random-memref	fresh memref load/store chain in a thread region	equality
insert-jitter	delay chains in gaps around shared-memory ops	equality
insert-comparison	self-comparisons after a thread value	equality
insert-both-arms-if	duplicate a chain into both arms of scf.if	equality
insert-parallel	new omp.parallel with random sections	equality
insert-critical	wrap a thread-local chain in omp.critical	subset
local-store-duplication	duplicate a thread-local store	equality
load-reordering	shuffle eligible loads inside threads	equality
relax-operation	weaken atomic memory order one stage	superset
restrict-operation	strengthen atomic memory order one stage	subset
unroll-single-thread	unroll a single-section omp.parallel	equality

Memory-model-specific transforms

Transforms for a specific memory model live under mlir-mracle/src/lib/passes/transforms/<model>/ e.g. the ARMv8 relaxed commutations in transforms/arm/ArmTransforms.cpp.

Each declares its target via getTarget() (MetamorphicTransform.h), and getTransforms() in MetamorphicTransform.cpp adds it to the applicable set only when the requested --model matches.

Agitation sweep

The agitation sweep perturbs execution across codegen and runtime axes to widen the set of observable outcomes and surface rare interleavings.

Each LLVM module is compiled into 5 in-memory JIT variants and run under configCount (default 5) OpenMP team-size configs.

• Codegen axis — each variant clones the module and shuffles non-entry basic blocks; CodeGen opt levels use all of {0,1,2,3}. On ELF, per-BB sections preserve the shuffled layout in machine code.
• Runtime axis — team sizes are drawn from {2,3,4,6,8} without replacement.
• Replay rounds — rare states re-run with fresh team-size mixes, without recompiling.
• TSan triage — when the --max-runs cap is reached with rare states still unresolved, one TSan-instrumented binary per side runs a final --reruns round; TSan's scheduling perturbation either surfaces the state or confirms it absent before the final verdict.

Oracle

The oracle compares the outcome sets of source and transformed runs and issues the final verdict, using a Poisson model to judge statistical deviations.

• A single-thread probe of both sides must produce the same deterministic outcome, or the run fails.
• Outcome sets are compared under the run's relation (equality, subset, superset). A state present on one side only, or a rate shift on a shared state, is tested against a Poisson model of the source-side counts (p < 1e-6 flags a deviation).
• Rare novel states are not immediately judged; replay rounds merge more data before the final verdict.
• Verdicts are OK, WARN (statistical deviation below the fail bar), or FAIL (hard behavioural change).

Output layout

A campaign is written to <campaign-dir>/<status>/run<N>_seed<S>/:

• source.mlir, transformed.mlir, lowered.mlir
• source.ll, transformed.ll
• run_info.json — transform applications, per-thread/outcome-set breakdown, verdict, and structured issues (each with status FAIL/WARN, outcome, and reason)

<campaign-dir>/result.json aggregates the per-binary results, and sanitizer.log records any TSan reports. --mode=execution writes a bare source.ll per run; --mode=emit writes run<N>_seed<S>.mlir variants.

Testing

.venv/bin/cmake --build build --target mlir_mracle_oracle_test mlir_mracle_legacy_oracle_test -j
ctest --test-dir build --output-on-failure

Troubleshooting

• Apple Silicon OpenMP: Homebrew libomp is auto-detected; ensure it is installed before configuring.
• Repeated re-lowering: delete the cache dir (cache/v2) to force fresh lowering of all modules.
• ThreadSanitizer: the tool and JIT'd code always run under TSan (-fsanitize=thread); sanitizer.log records TSan reports from the campaign run.

Pull requests

This is an emerging codebase, so PRs do not need to be polished. Metamorphic transformations for other hardware targets or memory models are especially appreciated.

Contact me at aarongaba05@gmail.com if you have any questions.