Mithril_

1Why Mithril

Your machine has many CPU cores and a GPU with thousands of lanes, and a plain loop uses one core. Using the rest usually means threads and locks, and with them the hard bugs: two threads update the same value at once, and the program gives a different answer from one run to the next. A GPU means rewriting the code again as CUDA kernels^[16].

Mithril lets you write the program once, the plain way: functions, loops, tuples and arrays in a subset of Python, with no threads, locks or kernels. The compiler finds the work that can happen at the same time (independent calls, independent loop iterations, sums it can prove may be split), and the same source runs on one thread, every core, or an NVIDIA GPU, returning the same answer, bit for bit, on all of them. That guarantee comes from what a Mithril program is underneath: a graph of small nodes, an interaction net.

Each step replaces exactly two connected nodes and touches nothing else. Steps on different nodes share no variable to fight over, so they can run in any order, or at once, with the same result.

The idea has a long lineage, and Mithril stands on it:

1. 1987Jean-Yves Girard's linear logic^[2] treats every value as used exactly once.
2. 1990Yves Lafont defines interaction nets^[1], where every step is local.
3. 1997Lafont shows that three kinds of node, the interaction combinators^[3], compute anything.
4. HVM, BendVictor Taelin and HigherOrder Co. make the theory run: HVM^[4] evaluates interaction combinators across CPU cores and GPUs, and Bend^[5] shows that ordinary-looking programs parallelize with no annotations. They also find the catch: rewriting a graph one pair of nodes at a time costs far more per step than plain machine code, and Bend 2^[6] leaves nets behind to compile to C.

Mithril bets the other way: nets pay off once you change when the rewriting happens. The same rules run at two times (chapter 4):

• Compile timeEvery rewrite whose inputs are written in the source runs while compiling, the idea behind partial evaluation^[8]: constants computed, small functions inlined, decided if tests settled. These are the program's own rules applied early, not separate optimizations, so they cannot change what it means.
• Run timeWhat depends on the input, such as each pixel's colour in a ray tracer, becomes ordinary machine code. The net stays only to share computed values and hand independent work to idle cores.

Mithril holds itself to the strict test: how many cores it needs to beat a good sequential C program of the same algorithm^[7]. It is a research language: its core rules are proved confluent in Lean^[9], every backend is checked against a reference interpreter, and its open problems (vectorizing independent work, keeping GPU lanes busy, irregular machine-learning workloads, chapter 10) are the problems nets must solve to scale.

2Mithril in ten minutes

If you read Python, you can already read every program in this guide. Mithril keeps Python's syntax and changes what three things mean: a value never changes once it is made, two parts of a program never share a value by changing it, and you never write a thread, a task or a device. The eight pieces below are all the syntax there is.

def fib(n):
    if n < 2:
        return n
    return fib(n - 1) + fib(n - 2)

if c > 0:
    return a
return b

for i in range(n):
    s = s + f(i)

p = (x, y, z)
a, b, c = p

@data
class L:
    Nil: ()
    Cons: (h, t)

def stage(c):
    return lambda x: x * 3 + setup(c)

a = array_new(n, 0)
a = array_set(a, i, v)

r = sqrt(f32(d))

A first program

The black hole in the header is about 800 lines of plain functions: the equations of a light ray near a spinning hole, a Runge-Kutta step, a recursive function that follows one ray until it falls in, crosses the disk or reaches the stars. Its image is made by a few loops in a row; the first fires one ray through every pixel of a strip of frames.

def main():
    ...
    m = width() * height() * frames()
    base = array_new(m, 0)
    for i in range(m):
        base = array_set(base, i, first_ray(i, cams, tab))
    ...

Nothing here names a thread. Each first_ray(i, cams, tab) reads only the camera table, the colour table and its own i, so Mithril may compute the pixels in any order, on any core or on the GPU. The writes into base form a chain, but each is a single store; the cost lives in first_ray. The device and the thread count are chosen when the program runs.

The whole system

The map below follows one program from its source file to running code, top to bottom. Each box names the crate that implements it, and the § mark gives the chapter that explains it. The dashed boxes beside the main path are the checks: the reference interpreter every run is compared with, the two Lean proofs, model checking of the CPU's lock-free handoffs, and the test gates. The copper dashed box is the command that shows what the compiler did to your program. Notice that the rule table appears only once, inside compile-time reduction, and a dotted line carries it to both runtimes: the compiler, the CPU and the GPU all fire the same rules.

How Mithril reads a program

Mithril runs two calculations at once whenever neither needs the other's result. So to see where a program can run in parallel, ask three questions about its shape: which calculations can start together, which must wait for an earlier answer, and what do they share? The six problems below each have a different shape. Each animation runs the real problem and schedules it the way Mithril's runtime does: a task starts as soon as its inputs exist and a worker is free.

Rendering: every pixel on its own

A ray tracer colours a pixel by firing a ray from the camera through it, following the ray as it bounces off the mirror sphere or bends through the glass one, and adding up the light it collects. The calculation reads only the scene description and the pixel's own coordinates; no pixel needs another pixel's answer. The program loops over the image row by row, but Mithril sees that the pixel(x, y) calls are independent and hands them to whichever worker is free.

Pixels are not equal. A ray that hits the back wall stops after one shadow test, while a ray that strikes glass splits into a reflected and a refracted ray, each traced further. The tiles over the spheres below cost several times more than the tiles over the walls. With one worker the frame fills in reading order. With more, a worker that finishes a tile takes the next one in the queue, so a slow tile over the glass sphere never delays the wall tiles queued behind it.

Merge sort: split, solve, combine

Merge sort orders a list by halving it until each piece is trivially small, sorting the pieces, and merging sorted halves back together; merging two sorted lists only ever compares their front elements. The two halves of any split have separate inputs, so they can be sorted at the same time. The merges cannot start until both of their halves are sorted.

That gives the computation a diamond outline. Each split doubles the work available, so four workers are busy while the pieces sort, and each merge halves it again until the last merge runs on a single worker. The busy-worker trace under the tree shows that rise and fall.

Four queens: a search that grows as it runs

The puzzle asks for every way to place four queens on a 4 × 4 board so that no two share a row, column or diagonal. A backtracking search places one queen per row. Each legal placement opens a branch for the next row, and a board with no legal square left is a dead end.

Nobody knows the shape of this tree in advance; a branch exists only once its parent has been checked. A first queen in the corner leads to a dead end a row or two later; a first queen in the second column leads all the way to a solution. Mithril starts each new board as a task the moment it appears, so a worker that finishes checking a board immediately takes one of the boards the search has just produced. The search finds the puzzle's two solutions.

Nearest neighbours: many searches, one shared map

Given a set of stored points, find the closest one to each of many query locations. A k-d tree^[13] makes this fast by cutting the plane in half again and again, alternating vertical and horizontal cuts, until each cell holds a few points. A query descends to the cell containing it, then backs out and checks a neighbouring cell only if that cell could hold something closer than the best point found so far.

The tree is built once and only read afterwards. Every query walks the same tree with its own best-so-far, so queries run side by side without locks or copies. Inside one query the visits are ordered, because each one decides whether the next cell is worth opening. Queries in crowded or awkward spots visit more cells, which gives the scheduler jobs of different sizes.

Collatz: a chain no worker can shorten

The Collatz rule halves an even number and replaces an odd one with three times itself plus one. Repeat it and the numbers rise and fall like hailstones until they reach 1. Starting at 6 gives 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.

def steps(n):
    count = 0
    while n != 1:
        if n % 2 == 0:
            n = n // 2
        else:
            n = 3 * n + 1
        count = count + 1
    return count

Each step needs the number the previous step produced, so the chain is strictly serial: worker 1 computes the whole chain from 6 down to 1 while workers 2, 3 and 4 sit idle. A batch of different starting numbers is a different story, because chains for 6, 7, 8 and 9 never consult each other. They run side by side, and the longest chain sets the finishing time. A loop can take either shape; the dependencies decide which.

A spinning black hole: the compiler does the heavy lifting

The video at the top of this guide is a Mithril program of about 800 lines. For every pixel it follows a ray of light backward from the camera through the curved spacetime around a black hole spinning at 0.99 of the maximum. Each ray is pushed forward by a Runge-Kutta step, again and again, until it falls through the horizon, crosses the glowing disk of gas or escapes to the stars. The colour it brings back includes the Doppler and gravitational shifts of the light.

The program's shape is simple: ten loops in a row, each filling an array (the colour table, the camera path, a first ray per pixel, extra rays at sharp edges, four blur passes for the glare, the final image). Inside a fill, pixel i reads only arrays made by earlier fills and writes only its own slot, so every pixel is an independent task. The work per pixel is very uneven, as the map below shows. A ray that hits the near side of the disk stops after about ten steps, a ray that escapes to the stars takes a few hundred, and a ray that spirals into the shadow takes more than a thousand. Idle workers take the next pixels as they finish, so the expensive rays around the shadow never hold up the cheap ones.

Many of the black hole's inputs are written in the source: the spin, the camera's path, the size of the disk, the image size. Mithril fires every rule that depends only on those while it compiles, and the results are large. The radius of the innermost stable orbit, a formula with three cube roots and two square roots of the spin, becomes the single constant 1.4545 inside disk and march. The spin's square 0.9801 and the camera's tilt (its cosine and sine, 0.035 and 0.99939) appear as numbers in ray. cbrt, whose loop of Newton steps runs a fixed number of times, unrolls from 4 agents into 321 with no call left inside. None of this is a separate optimizer: each step is one firing of the rules from chapter 3, the same rules the runtime fires (chapter 4). What reaches the processor is the physics that depends on the pixel, in straight-line native code.

3Why the answer never changes

The glass shader in the ray tracer traces a reflected ray and a transmitted ray, then blends their colours. Either ray may finish first; the blend waits for both.

# From glass(); surface geometry and the total-reflection branch omitted.
mirror = trace(add(p, scale(n, eps())), reflect(d, n), depth - 1)
through = trace(sub(p, scale(n, eps())), rd, depth - 1)
return add(scale(mirror, f), scale(through, 1.0 - f))

To see why the order cannot matter, look at how Mithril holds this program: as an interaction net. A net is made of agents (the nodes) joined by wires. Each agent has one special port, its principal port. When the principal ports of two agents are wired together, the two form an active pair, and a rule replaces the pair with a small new net, reconnecting the wires that led into it. One replacement is one step of computation.

Mithril's rules are few. An erasure agent meeting a number deletes both, because nothing uses the number. Other rules apply a function, compute an arithmetic operation, select a branch or copy a shared value to two consumers. Because two active pairs never share an agent, firing one cannot disturb another.

That local guarantee is the diamond property, and it implies confluence: every order of reduction that finishes ends at the same net. The scheduler can fire any ready pair on any core at any moment. For Mithril's core rules the property is proved in Lean^[9] (chapter 8).

One kind of change is not covered by reordering. Summing an array in chunks changes how the additions are grouped: (a + b) + c becomes a + (b + c). That is safe only when the operation is associative and has an identity, so Mithril splits a sum like this only after proving both facts for the numbers it actually uses. Integer addition passes. Floating-point addition does not, because its rounding depends on the grouping.

4One rule table at compile time and run time

A program's inputs arrive at two different times. Some are already written in the source: constants, flags, helper functions. Others, such as n in the example below, arrive only when the program runs. While compiling, Mithril fires every rule whose inputs are in the source; it keeps the rules that need run-time input for later. The program that is left after compiling, the one that actually runs, is called the residual program.

In shade(n) below, only n comes from the program's input. The flag 1, the number 3 and the two helper functions are written in the source, so the compiler evaluates pick(1, square(3), n) to 9 before the program ever runs.

def square(x):
    return x * x

def pick(c, a, b):
    if c > 0:
        return a
    return b

def shade(n):
    return square(n) + pick(1, square(3), n)

MITHRIL_NET_CORE=1 target/release/mithril net docs/examples/specialize.py
# shade = Op2(Add, Op2(Mul, Var(0), Var(0)), Num(9))

cargo run --release -p mithril-cli --example dump_gen -- \
  docs/examples/specialize.py /tmp/mithril-specialize.rs

fn s_2(fuel: &mut i64, v0: i64) -> i64 {
    let fl: i64 = 1i64;
    let s1: i64 = v0.wrapping_mul(v0);
    let s2: i64 = s1.wrapping_add(9i64);
    return s2;
}

Evaluating a program when part of its input is already known is called specialization^[8]. The compiler does it on a work budget. If the budget runs out, the unfinished part simply stays in the residual program, and the program still means the same thing: the Lean proof covers half-reduced nets too.

Next, the compiler turns the residual program into code for the hardware, a step called lowering. The residual n * n + 9 is straight-line arithmetic, so it becomes two machine instructions on a register: no agents are allocated and no rules are dispatched. A call that opens independent work becomes a task that another core can take. A value whose consumers are still waiting for it stays in the net.

Sharing work through closures

A data pipeline is built from stages. Each stage is configured once, with a setting c read at run time, and then applied to thousands of inputs. Preparing a stage is expensive: setup(c) folds a large table from the configuration. Applying it is cheap.

def stage(c):
    return lambda x: (x * 3 + setup(c)) & 1048575

Written this way, a strict language recomputes setup(c) inside every call, because the expression sits in the body of the lambda. A programmer can hoist it by hand. Mithril does not need that: setup(c) depends only on the captured configuration, so the sharing rules compute it once per stage and wire the result to every application. Nothing is cached by comparing expressions; the value has one producer and many consumers.

5What Mithril gives you

Rendering on 1 thread, 16 threads and a GPU

A spinning black hole

Path tracing^[12]

Ryzen 7 7800X3D and RTX 4090. Path tracing, 4 October 2026: FPS is 24-frame batch throughput, median of three runs after a warmup. Compilation excluded; returned pixels, GPU context setup and readback included. All frame pixels match across CPU and GPU. Measurements and reproduction.

Medians of three built-artifact runs after a warmup, same machine, 4 October 2026 (the black hole's 1-thread time is one run). Compilation excluded; GPU wall includes context creation and readback. Raw samples.

Read each row from left to right. The same unchanged source runs about ten times faster on sixteen threads than on one. On the GPU, one path-traced frame takes as long as on sixteen threads, and a black-hole frame runs five times faster still. Every lane returns identical pixels.

Against a sequential C program

Chapter 1 set a strict test: how many cores does Mithril need to beat a good sequential C program of the same algorithm? Here it is on a batch of nearest-neighbour queries over a shared k-d tree. On one thread Mithril runs level with C; on sixteen it is four times faster. The GPU is slower on this program, because the queries branch unpredictably and leave most lanes of each warp idle (chapter 10).

gcc -O2; minimum wall-clock time of five runs (GPU: three) on 4 October 2026, builds excluded, outputs checked. A parallel C version has not been measured. Methods and samples.

Against Rust, on programs a general-purpose language must handle

Exploratory corpus at e8441a9, 4 October 2026, one wall-clock sample per lane (the slower rows repeated within 0.02 s), checked against a Python oracle. The Rust twins follow the shape of the Mithril source (Rc lists, boxed closures); a hand-tuned Rust program could be faster. Design §11.1 · harness.

The wins come from two places. Recursive work spreads across cores without any code to arrange it, and sharing rules keep a closure from repeating setup that depends only on what it captured. The losses are chapter 7's subject.

6Where to use it

To decide whether Mithril fits your problem, look at the shape of the computation rather than its domain. Mithril pays off when there is plenty of independent work, each piece big enough to be worth handing to another core, and most of all when that work is irregular: you cannot know a piece's size until it runs, or the pieces read shared data that would otherwise need locks.

• Rendering and simulation batches. Ray and path tracing, per-element simulation steps, Monte Carlo sampling with hashed random numbers that reproduce exactly on any device.
• Recursive search and divide and conquer. Game-tree and constraint search, branch-and-bound, sorting and tree algorithms, where branches appear at run time and differ in size.
• Many queries over shared read-only structures. Spatial indexes, lookup tables, rule sets checked against many inputs.
• Code that needs locks elsewhere. Five programs that require locks or atomics in C and Rust are written in Mithril without either, each with C and Rust versions for comparison. Lockless programs.
• Irregular planning in machine-learning systems. Mixture-of-experts routing^[17,18] (top-k gating, capacity limits, overflow), sparsity patterns and graph traversals share the k-d tree's shape: a read-only structure, partitioning and data-dependent branching, balanced by the scheduler instead of by atomics and sorts.
• Executable specifications of distributed algorithms. Ring and tree all-reduce^[19] or expert all-to-all exchange are local rules on a graph. Mithril runs such an algorithm with the same rules on CPU and GPU and checks it against the oracle, as a specification and schedule simulator.
• Compiler passes and planning. A rewrite system over an intermediate representation is a rule table, and the compile-time reducer runs it.

python3 demos/compiler_planning/demo.py --out target/compiler-planning/demo
# Open target/compiler-planning/demo/demo.html

7Where not to use it

You can see these limits in chapter 5's tables. Serial mutual recursion is a chain: extra threads have nothing to take, so sixteen threads run no faster than one. Copy-on-write array versions and the persistent map keep old versions of their data alive, which forces copies, so they trail Rust at any thread count. The closure interpreter builds new work for every input and loses by two orders of magnitude. And on one thread Mithril trails sequential C on four of the seven benchmark ports in the README, by up to 2.6× on the histogram, so on those its advantage appears only once there are cores to use.

On the GPU the picture is mixed. A black-hole frame runs five times faster than on sixteen CPU threads and a path-traced frame runs level with them, but the k-d tree, whose queries branch unpredictably, is nearly four times slower than on one CPU thread. Today the GPU's sure benefit is running the same program with the same results; closing its speed gap on irregular work runs through the vectorization and per-lane work in chapter 10.

Memory needs watching too. Storage is reused when ownership allows, but keeping old versions of a value can force copies, and task records, net agents and queues all take space. A different reduction order can change peak memory even though the answer stays the same.

8Proved and checked

Some of this guide's claims are proved and some are checked by running programs. The three guarantees below are proved or model-checked. Each is stated in plain words first, then shown on an example, then bounded by what it does not cover. The compiler, the extra rules and both runtimes are checked by tests, listed at the end of the chapter.

Checked by running programs

The compiler, the extra rules and both runtimes are checked by comparing their answers with an independent reference interpreter that evaluates the source directly.

• Compiled code gives the interpreter's answer. Every test program runs at 1, 4 and 16 threads and with tiny work budgets that force pausing, on CPU and GPU. Parity checks.
• Compile-time reduction keeps the meaning. Each test program is evaluated before and after the compiler's reduction, and the answers must match. Specializer tests.
• The extra rules also agree in any order. 10,000 randomly generated programs, each reduced in five different orders using the production rules, all match the interpreter. Schedule test.

The GPU engine implements its rules separately from the CPU rule source, and these tests hold the two together. The verification notes list each property that is checked only by tests and not yet proved.

9Related work

10Future work

The problems below are not specific to Mithril: any system that runs interaction nets has to solve them to scale. Mithril is built to make them measurable, so every change is run against a sequential C program, the reference interpreter and every backend.

Auto-vectorization of independent work

Mithril's CPU code is scalar (baseline x86-64 with no AVX or FMA, and arm64 on macOS), and independent calls such as neighbouring pixels run as separate scalar tasks. Yet the net has already proved those calls independent, which is the fact an ordinary vectorizer works hardest to establish. The next step is to group tasks that run the same function on different inputs into SIMD lanes. The same grouping matters on the GPU, where 32 lanes of a warp execute in lockstep: profiles show that on irregular programs most warp instructions run with only a few of their 32 lanes active, while regular ones such as bitonic sort fill far more.

Per-lane efficiency

On one thread Mithril still trails sequential C on most programs, so it needs several cores to pass it^[7]. Closing that gap is a lowering problem: native code should use representations chosen from types instead of mirroring the net's cells, through general rules rather than per-program tuning.

One rule source for every device

The GPU engine's rules are a second implementation, held equal to the CPU's by tests. Generating both from one table, and linking that table to the Lean model, would turn a checked property into a constructed one. The Lean proof itself is still to be extended to Mithril's extended rules.

Machine-learning workloads

The planned probe is a mixture-of-experts router^[17,18]: top-2 gating with capacity overflow over hashed logits, checked against a C twin on CPU and GPU, whose output is a dispatch plan of index buffers. Beyond it lies a division of labour with dense-kernel compilers, in which Mithril decides the irregular structure of a computation and the kernel compiler runs its dense math. Collective-communication algorithms as executable specifications and compiler passes as rule tables follow the same path.

Scaling the substrate

GPU startup spends tens of milliseconds creating a context, and rounds of global synchronization still serialize the device scheduler. Beyond one device, distributing a net across several GPUs or machines is an open research question; confluence says the answer will not change, and the work is to make it fast.

11Try it

Start with a computation you can check: render the tracer on one thread, sixteen threads and the GPU, and compare the images.

git clone https://github.com/maderix/mithril && cd mithril

# Drop --features gpu for a CPU-only build.
cargo build --release -p mithril-cli --features gpu

target/release/mithril run demos/cornell_whitted.py --threads 1  --image one.ppm
target/release/mithril run demos/cornell_whitted.py --threads 16 --image many.ppm
target/release/mithril run demos/cornell_whitted.py --gpu        --image gpu.ppm
cmp one.ppm many.ppm && cmp one.ppm gpu.ppm

The build instructions cover the GPU requirements. The generality corpus has interpreters, persistent maps and closures to read, and the design notes record every mechanism and open obligation.

12References

1. Y. Lafont. Interaction nets. Proc. 17th ACM Symposium on Principles of Programming Languages (POPL), 95–108, 1990. doi.org/10.1145/96709.96718
2. J.-Y. Girard. Linear logic. Theoretical Computer Science 50(1):1–101, 1987. doi.org/10.1016/0304-3975(87)90045-4
3. Y. Lafont. Interaction combinators. Information and Computation 137(1):69–101, 1997. doi.org/10.1006/inco.1997.2643
4. V. Taelin and HigherOrder Co. HVM: a massively parallel evaluator for interaction combinators. github.com/HigherOrderCO/HVM
5. HigherOrder Co. Bend: a massively parallel, high-level programming language (Bend 1, on HVM2). github.com/HigherOrderCO/Bend1
6. HigherOrder Co. Bend 2. github.com/HigherOrderCO/bend
7. F. McSherry, M. Isard and D. G. Murray. Scalability! But at what COST? 15th Workshop on Hot Topics in Operating Systems (HotOS), 2015. www.usenix.org/conference/hotos15/workshop-program/presentation/mcsherry
8. N. D. Jones, C. K. Gomard and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
9. L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. 28th International Conference on Automated Deduction (CADE), 2021. lean-lang.org
10. Tokio project. loom: concurrency permutation testing for Rust. github.com/tokio-rs/loom
11. T. Whitted. An improved illumination model for shaded display. Communications of the ACM 23(6):343–349, 1980.
12. J. T. Kajiya. The rendering equation. Proc. SIGGRAPH, 143–150, 1986.
13. J. L. Bentley. Multidimensional binary search trees used for associative searching. Communications of the ACM 18(9):509–517, 1975.
14. S. Marlow, P. Maier, H.-W. Loidl, M. K. Aswad and P. Trinder. Seq no more: better strategies for parallel Haskell. Proc. Haskell Symposium, 2010. hackage-content.haskell.org/package/parallel-3.3.0.0/docs/Control-Parallel-Strategies.html
15. K. C. Sivaramakrishnan, S. Dolan, L. White, T. Kelly, S. Jaffer and A. Madhavapeddy. Retrofitting parallelism onto OCaml. Proc. ACM on Programming Languages 4 (ICFP), 2020. ocaml.org/manual/5.5/parallelism.html
16. NVIDIA. CUDA C++ Programming Guide: writing CUDA kernels. docs.nvidia.com/cuda/cuda-programming-guide/02-basics/writing-cuda-kernels.html
17. N. Shazeer, A. Mirhoseini, K. Maziarz, A. Davis, Q. Le, G. Hinton and J. Dean. Outrageously large neural networks: the sparsely-gated mixture-of-experts layer. ICLR, 2017. arxiv.org/abs/1701.06538
18. W. Fedus, B. Zoph and N. Shazeer. Switch Transformers: scaling to trillion parameter models with simple and efficient sparsity. Journal of Machine Learning Research 23(120):1–39, 2022. arxiv.org/abs/2101.03961
19. P. Patarasuk and X. Yuan. Bandwidth optimal all-reduce algorithms for clusters of workstations. Journal of Parallel and Distributed Computing 69(2):117–124, 2009.