GPU Programming

Miri is GPU-first: running code on an accelerator is part of the language, not a library bolted on top. A GPU program in Miri reads top-to-bottom as a sequence of plain operations, and the cost of each line — upload, kernel launch, readback — is visible in the source.

This guide takes you from your first kernel to shared-memory tiling, atomics, warp-level reductions, and interactive browser demos. Every runnable snippet is the same one the compiler verifies in its test suite. The code you read here is code that compiles and runs today.

Introduction: residency is a binding attribute

Miri does not have a separate "GPU array" type. An Array<f32, 4> is the same type whether it lives on the host or the device — what differs is the binding's residency. Residency is an attribute on the binding, exactly like mutability:

let  x = [1.0, 2.0, 3.0, 4.0]      // host-resident, immutable
var  y = [1.0, 2.0, 3.0, 4.0]      // host-resident, mutable
gpu let a = [1.0, 2.0, 3.0, 4.0]   // device-resident, immutable  (uploaded)
gpu var d = [0.0, 0.0, 0.0, 0.0]   // device-resident, mutable

Two axes — mutability (let/var) and residency (host/gpu) — give four binding forms and zero new types. The gpu keyword is the only source of device residency. Reading any file, grep 'gpu let\|gpu var' enumerates every device-resident binding.

Here is a complete GPU program — two arrays added element-wise on the device:

use system.gpu
use system.collections.array

const N = 4

gpu let a = [1.0, 2.0, 3.0, 4.0]
gpu let b = [5.0, 6.0, 7.0, 8.0]
gpu var dst = [0.0, 0.0, 0.0, 0.0]

forall i in 0..N
    dst[i] = a[i] + b[i]

let host = dst
println(f'{host[0]} {host[1]} {host[2]} {host[3]}')

Output: 6.0 8.0 10.0 12.0. Five lines of GPU logic. The CUDA equivalent is roughly forty. Save it as add.mi and run it with miri run add.mi — that's the whole workflow.

The residency surface

A small set of forms covers the whole surface:

What may be device-resident

A type can be bound with gpu only if it implements the Accelerable capability trait. The standard library ships impls for Array<T, N> and List<T> over the accelerable scalars — int, i32, i64, u32, u64, f16, f32, f64, bool — plus the vector types, Tensor, and user structs declared implements Accelerable. String, Map, Set, and function values are not accelerable. Binding one with gpu is a compile error that names the missing trait.

Launching kernels — forall

A forall body is a data-parallel loop: every index runs independently. Where it runs is decided by what it captures:

• forall (bare) — routes automatically. If the body captures a device-resident binding, it launches on the GPU. If it captures only host data, it runs as a plain CPU loop. Same syntax, both worlds.
• gpu forall — explicitly a GPU launch. One GPU thread per index.

use system.gpu
use system.collections.array

fn main()
    gpu let g = [1, 2, 3]
    gpu var result = [0, 0, 0]
    forall i in 0..3
        result[i] = g[i] * 2
    let h = result
    print(f"{h[0]}")
    print(f"{h[1]}")
    print(f"{h[2]}")

Output: 246. The bare forall captures g and result, both device-resident, so it launches on the GPU. Change both bindings to plain let/var and the identical loop runs on the CPU.

What a kernel body may do

A forall kernel may capture device-resident bindings and index them, capture host scalars (int, bool, f32 — passed as read-only uniforms), call scalar functions and system.math intrinsics, and use arithmetic, if, and while. It may not do I/O or allocate.

2D and 3D launches

Multi-dimensional domains launch with one index per axis — the compiler picks the workgroup shape (256×1×1 for 1D, 16×16×1 for 2D, 8×8×4 for 3D):

gpu forall i, j in 0..W, 0..H          // 2D: one thread per (i, j)
    img[j * W + i] = i + j

gpu forall i, j, k in 0..2, 0..2, 0..2  // 3D
    voxels[i * 4 + j * 2 + k] = i + j + k

Bounds may be literals, consts, or runtime values — including a runtime start (forall i in a..n). Runtime bounds travel to the kernel as uniforms. Threads past the bound exit immediately, so over-dispatch is safe.

Safety checks at compile time

The compiler rejects kernels where two threads could write the same non-atomic element (dst[i / 2] = … is an error. dst[i] = … is fine). Scatter writes — indices computed from data — need atomics. It also validates kernel names against WGSL reserved words and checks that integer division operands fit the device's 32-bit range.

Getting data back

Assigning a device-resident binding to a host binding copies the bytes back to the host. The transfer is always visible at the assignment line:

use system.gpu

gpu var arr = [0, 0, 0, 0, 0, 0, 0, 0]

forall i in 0..8
    arr[i] = i * i

let h = arr

for j in 0..4
    println(f'{h[j]}')

Output:

0
1
4
9

There is no .to_host() method and no hidden transfer. The keyword on each side of the assignment marks the host/device boundary. The reverse direction works the same way — gpu let g = host_x uploads host_x, and re-assigning a host array into a gpu var re-uploads it (that is how a training loop pushes updated parameters back to the device).

Three sanctioned partial reads avoid the full copy:

• g.length() — free. The length is known on the host.
• g.slice(a..b) — fences and reads back just [a, b) as a host array.
• g.reduce(init, op) — reduces on the device. See On-Device Reduction.

Every other buffer-touching method on a gpu-resident binding in host code — element_at, contains, set, … — is a compile error with the same fix-it as the forbidden pattern: bulk-copy first.

The four cost classes

Every operation is one of four cost classes, and the surface form names the class. You can read the cost of a program straight from the source, without running it:

The runtime exposes counters so you can confirm the cost class of each line. After gpu_reset_telemetry(), the functions gpu_uploads(), gpu_launches(), gpu_readbacks(), and gpu_fences() return the cumulative counts. The buffer-reuse recipe below asserts them directly.

Two properties keep repeated launches cheap: a device buffer is persistent — uploaded once, reused by every subsequent kernel until the binding leaves scope (it is freed at scope exit) — and a gpu let b = g move transfers the device handle without copying.

The forbidden pattern — element cross-read

Reading a single element of a device-resident binding from host code is a compile error. It looks harmless, but each read would force its own readback — in a loop, that is N round-trips instead of one bulk copy:

gpu var arr = [0, 0, 0, 0, 0, 0, 0, 0]
forall i in 0..8
    arr[i] = i * i

let v = arr[0]     // COMPILE ERROR: a per-element read would require a readback

The fix the compiler points to is to bulk-copy first (let h = arr), then index the host copy — exactly the readback pattern above. This keeps the readback cost visible at one line.

Named kernels — gpu fn and .launch

A forall is an anonymous kernel with inferred launch geometry. When you need a reusable kernel, or explicit control over the grid and block shape (for shared-memory tiling or warp operations), declare a gpu fn and launch it yourself:

gpu fn scale(src Array<f32, 1024>, dst out Array<f32, 1024>)
    let i = kernel.global_idx.x
    if i < src.length()
        dst[i] = src[i] * 2.0

fn main()
    gpu let src = Array<f32, 1024>()
    gpu var dst = Array<f32, 1024>()
    scale(src, dst).launch(Dim3(4, 1, 1), Dim3(256, 1, 1))   // grid, block

Buffer parameters must be gpu-resident at the launch site (gpu let/gpu var). An out parameter is writable, everything else is read-only. .launch(grid, block) takes two Dim3s: the number of workgroups per axis and the threads per workgroup. The block shape must be a compile-time literal — it is stamped into the generated shader as @workgroup_size. Dispatch is synchronous.

The kernel context

Inside any kernel body — forall or gpu fn — the implicit kernel object exposes the launch geometry. All fields have .x, .y, and .z components:

In a forall, the loop index already is the global index, so you rarely touch kernel there. In an explicitly launched gpu fn, kernel.global_idx is how each thread finds its element.

Functions in kernels

A kernel body may call ordinary Miri functions, as long as they are device-representable: scalar parameters and return type, no I/O, no allocation, no recursion. The compiler checks all of this at the call site — a violation is a compile error naming the offending function, not a runtime surprise.

fn dbl(x float) float: x * 2.0

fn main()
    gpu let src = [1.0, 2.0, 3.0]
    gpu var dst = [0.0, 0.0, 0.0]
    forall i in 0..3
        dst[i] = dbl(src[i])       // compiled into the kernel

Residency-polymorphic functions

A function whose buffer access happens only inside a forall accepts both host and gpu-resident arguments — the launch specializes to wherever the data lives:

use system.gpu
use system.collections.array

fn scale(a out Array<int,8>)
    forall i in 0..a.length()
        a[i] = a[i] * 2

fn main()
    gpu var data = [1, 2, 3, 4, 5, 6, 7, 8]
    scale(data)
    let host = data
    println(f"{host[0]} {host[1]} {host[2]} {host[3]} {host[4]} {host[5]} {host[6]} {host[7]}")

Output: 2 4 6 8 10 12 14 16. scale mutates the device buffer in place — no copy in, no copy out. A function that touches a buffer in host context (say, return a[0]) stays host-only, and passing it a gpu-resident buffer is a compile error. The residency rules cannot be smuggled around through a call boundary.

On-device reduction

.reduce(init, fold) on a gpu-resident array runs as a single-launch tree reduction over workgroup shared memory — no host round-trip per element:

use system.gpu

gpu let data = [1, 2, 3, 4, 5, 6, 7, 8]
let sum = data.reduce(0, fn(a int, b int) int: a + b)
println(f'sum = {sum}')

Output: sum = 36. The result of a device reduce is a gpu-resident scalar. Binding it to a host let (as above) is the fence — a single-element readback brings the value over. Bind it with gpu let instead and it stays on the device:

use system.gpu
use system.io
use system.collections.array

fn main()
    gpu var data = [1, 2, 3, 4]
    gpu let sum = data.reduce(0, fn(a i32, b i32) i32: a + b)
    let host_sum = sum
    println(f'{host_sum}')

Output: 10. The fold must be an associative binary operator — + or * over the two parameters. init is folded in exactly once. Anything else is rejected at compile time. On a host array the same .reduce call falls through to the ordinary CPU fold, so one spelling covers both residencies.

Shared memory & barriers

Threads in one workgroup share a fast on-chip memory. Declare a shared array inside a gpu fn, and synchronize the workgroup with kernel.barrier() — every shared write must be followed by a barrier before another thread reads it. The classic use is tiling: stage a block of global memory into shared memory once, then let every thread in the workgroup read it many times.

Here is a complete tiled matrix multiply — the reference pattern for workgroup cooperation. Each 2×2 block cooperatively loads tiles of A and B, synchronizes, accumulates, and moves to the next tile:

use system.collections.array

gpu fn tiled_matmul(a Array<f32, 16>, b Array<f32, 16>, c out Array<f32, 16>)
    shared tileA Array<f32, 4>
    shared tileB Array<f32, 4>

    let tx = kernel.thread_idx.x
    let ty = kernel.thread_idx.y
    let bx = kernel.block_idx.x
    let by = kernel.block_idx.y

    let row = by * 2 + ty
    let col = bx * 2 + tx

    var acc = 0.0

    // Tile K-loop: process A and B in 2×2 tiles
    var tile_k = 0
    while tile_k < 2
        // Load tile from global memory into shared memory
        tileA[ty * 2 + tx] = a[row * 4 + tile_k * 2 + tx]
        tileB[ty * 2 + tx] = b[(tile_k * 2 + ty) * 4 + col]
        kernel.barrier()

        // Local multiply-accumulate loop over the tile (T=2 elements)
        var k = 0
        while k < 2
            acc = acc + tileA[ty * 2 + k] * tileB[k * 2 + tx]
            k = k + 1
        kernel.barrier()

        tile_k = tile_k + 1

    c[row * 4 + col] = acc

fn main()
    gpu let a = [1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0, 12.0, 13.0, 14.0, 15.0, 16.0]
    gpu let b = [1.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 1.0]
    gpu var c = Array<f32, 16>()

    // Launch with a 2×2 grid of 2×2 blocks (4 blocks total, 4 threads per block = 16 threads).
    tiled_matmul(a, b, c).launch(Dim3(2, 2, 1), Dim3(2, 2, 1))

    let host = c
    println(f"{host[0]} {host[1]} {host[2]} {host[3]} {host[4]} {host[5]} {host[6]} {host[7]} {host[8]} {host[9]} {host[10]} {host[11]} {host[12]} {host[13]} {host[14]} {host[15]}")

B is the identity, so the output is A itself: 1.0 2.0 3.0 … 16.0, computed with zero intermediate readbacks. The barrier placement is load → barrier() → accumulate → barrier() → next tile.

Atomics

When many threads write the same element — histograms, counters, scatter patterns — declare the buffer with Atomic elements and use the atomic intrinsics:

use system.gpu
use system.gpu.atomic

fn main()
    gpu var hist = Array<Atomic<u32>, 256>()
    forall i in 0..147456
        atomic_add(hist, i % 256, 1 as u32)
    let host = hist
    let bucket_0 = host[0]
    let bucket_1 = host[1]
    println(f"bucket_0={bucket_0} bucket_1={bucket_1}")

Output: bucket_0=576 bucket_1=576 — 147,456 threads increment 256 buckets concurrently, and every increment lands (147456 / 256 = 576).

Atomic<i32> and Atomic<u32> support atomic_add, atomic_sub, atomic_max, atomic_min, atomic_and, atomic_or, atomic_xor, atomic_exchange, and atomic_compare_exchange, each taking the buffer, the element index, and the operand (use system.gpu.atomic). Calling one on a plain buffer, or from host code, is rejected. Reading the result is the ordinary readback: let host = hist yields a plain host array.

See the Particle Flow demo for atomics driving a real scatter workload.

Warp (subgroup) operations

Threads execute in hardware groups — warps (NVIDIA), waves (AMD), SIMD-groups (Apple) — that can exchange registers without touching shared memory. kernel.warp exposes the portable subset: kernel.warp.size, kernel.warp.lane_id, and kernel.warp.shuffle_down(v, n) (the shuffle offset is a compile-time literal). The canonical use is a register-only tree reduction:

use system.gpu
use system.collections.array

gpu fn warp_reduce_sum(input Array<int, 32>, dst out Array<int, 1>)
    let lane = kernel.warp.lane_id
    var v = input[lane]

    v = v + kernel.warp.shuffle_down(v, 16)
    v = v + kernel.warp.shuffle_down(v, 8)
    v = v + kernel.warp.shuffle_down(v, 4)
    v = v + kernel.warp.shuffle_down(v, 2)
    v = v + kernel.warp.shuffle_down(v, 1)

    if lane == 0
        dst[0] = v

fn main()
    gpu let input = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
    gpu var dst = Array<int,1>()
    warp_reduce_sum(input, dst).launch(Dim3(1, 1, 1), Dim3(32, 1, 1))
    let result = dst
    println(f'{result[0]}')

Output: 528 — the sum of 1..32, reduced in five shuffle steps with no shared memory and no barrier. Warp ops require adapter subgroup support. A device without it refuses the kernel before dispatch rather than miscomputing.

Vector types — Vec2 / Vec3 / Vec4

Vec2<T>, Vec3<T>, and Vec4<T> (use system.gpu.vector) are value types with .x/.y/.z/.w component fields. Inside kernels they compile to native WGSL vectors, and the vector builtins — dot, length, normalize, cross, reflect, mix — plus scalar broadcast (v * 2.0) compile to the hardware's vector instructions:

use system.gpu
use system.gpu.vector
use system.math
use system.collections.array

fn main()
    gpu let ax = [1.0]
    gpu let ay = [0.0]
    gpu let az = [0.0]
    gpu let bx = [2.0]
    gpu let by = [3.0]
    gpu let bz = [4.0]
    gpu var result = [0.0]
    forall i in 0..1
        let a = Vec3<f32>(ax[i], ay[i], az[i])
        let b = Vec3<f32>(bx[i], by[i], bz[i])
        result[i] = dot(a, b)
    let host = result
    println(f'{host[0]}')

Output: 2.0. Arrays of vectors store their elements inline with std430 layout (Array<Vec3<f32>, N> has 16-byte stride), so a buffer of vectors round-trips host → GPU → host bit-exactly for f32, i32, and u32 elements. 64-bit vector components are rejected — WGSL has no portable 64-bit vectors. The type checker enforces dimensions and element types: cross is Vec3-only, integer normalize is an error.

The Raymarch, Black Hole, and Wormhole demos are built on Vec3 math.

Scalar widths & f16

Kernels support i32, u32, f32, and f16 natively on every adapter. Half precision works end-to-end on the device:

gpu let a = Array<f16, 4>()
gpu var dst = Array<f16, 4>()
forall i in 0..4
    dst[i] = a[i] * 2.0        // float literals narrow to f16 automatically

64-bit scalars (int/i64, u64, f64) are gated on device features: an adapter that supports them runs them natively. One that doesn't refuses the kernel before dispatch with a clear message — never a silent truncation. Two guardrails back this up at compile time: an i64 value that provably exceeds the 32-bit range cannot be uploaded into a narrow buffer, and float→int casts saturate identically on host and device.

system.math works inside kernels: abs, min, max, pow, sqrt, floor, ceil, round, sin, cos, tan, tanh, atan2, log, exp, step, clamp, mix. Casts (x as f32, f as int) convert between widths explicitly, and math-intrinsic results keep the width of their f32 arguments — no accidental promotion to f64 inside a kernel.

Tensor — statically ranked, dynamically sized

Tensor<T, Rank> (use system.collections.tensor) is a multi-dimensional array whose rank is fixed at compile time and whose extents are runtime values, stored flat in row-major order:

let t = Tensor<int, 2>(shape: [2, 3], data: List([1, 2, 3, 4, 5, 6]))
println(f"{t.rank()}")       // 2
println(f"{t.dimension(1)}") // 3
println(f"{t.size()}")       // 6

Tensor implements Accelerable and is defined entirely in the standard library — the compiler has no Tensor-specific logic. It is the intended carrier for ML data reaching the device.

Interactive frames — gpu frame

Everything so far launches once and finishes. gpu frame declares a kernel that re-runs every display frame — the construct behind every demo in the GPU Playground:

use system.io
use system.gpu

fn main()
    gpu let a = [0.0, 0.0, 0.0, 0.0]
    gpu var b = [0.0, 0.0, 0.0, 0.0]
    gpu frame i in 0..4:
        let t = frame.time
        let d = frame.dt
        b[i] = a[i] + t + d
    println("ok")

A frame kernel reads one immutable buffer (gpu let) and writes mutable ones (gpu var) — reading and writing the same buffer in one pass is a compile-time data-race error. Multi-pass frame graphs nest ordered gpu forall passes inside a gpu frame block. Each pass's read/write sets must be disjoint, and the compiler checks that per pass. The Game of Life (5 passes) and Fluid (pressure-solve chain) demos are the reference frame graphs.

Inside a frame body, the frame context carries per-frame inputs, delivered as one uniform block:

Building for the browser

The same program that runs natively compiles to a self-contained WebGPU bundle:

miri build --target web-gpu program.mi -o bundle/

The bundle contains:

• <name>.json — the manifest: compiled WGSL kernels, buffer layouts, frame passes, per-frame input layout, canvas size, and WGSL↔Miri source maps.
• miri-gpu.js — the embeddable runtime. mount(canvas, manifest) boots the program on any WebGPU-capable browser, wiring frame.* inputs to real pointer events and presenting the paint buffer without a CPU round-trip.
• index.html — a thin local-dev harness.
• miri-gpu-headless.js — a Node/Deno headless runner for CI.
• a native host binary of the same program, for running outside the browser.

Every demo in the GPU Playground is such a bundle, and the source shown next to each canvas is the verbatim program — a compiler test asserts the displayed code compiles to byte-identical kernels.

Cookbook

Each recipe below is verified by the compiler test suite. Copy one into a .mi file and run it with miri run yourfile.mi.

Vector add

The simplest kernel: two device buffers added element-wise into a third, then read back.

use system.gpu
use system.collections.array

const N = 4

gpu let a = [1.0, 2.0, 3.0, 4.0]
gpu let b = [5.0, 6.0, 7.0, 8.0]
gpu var dst = [0.0, 0.0, 0.0, 0.0]

forall i in 0..N
    dst[i] = a[i] + b[i]

let host = dst
println(f'{host[0]} {host[1]} {host[2]} {host[3]}')

Output: 6.0 8.0 10.0 12.0.

Buffer-reuse pipeline

Two kernels run over the same gpu var with no readback between them, so the device buffer is uploaded once and reused. The telemetry counters prove the cost model: one upload, two launches, one readback.

use system.gpu

const N = 8

gpu_reset_telemetry()
gpu var data = [0, 0, 0, 0, 0, 0, 0, 0]

forall i in 0..N
    data[i] = i + 8

forall i in 0..N
    data[i] = data[i] + 8

let host = data
println(f'{host[7]} {gpu_uploads()} {gpu_launches()} {gpu_readbacks()} {gpu_fences()}')

Output: 23 1 2 1 1 — data[7] = 7 + 8 = 15, then 15 + 8 = 23. Then 1 upload, 2 launches, 1 readback, 1 fence. No cross-residency assignment sits between the two forall blocks, which is the visible marker that the buffer is shared.

SAXPY (fused multiply-add)

The coefficient is a host scalar, captured into the kernel as a read-only uniform.

use system.gpu

gpu let x = [1.0, 2.0, 3.0, 4.0]
gpu let y = [5.0, 6.0, 7.0, 8.0]
gpu var dst = [0.0, 0.0, 0.0, 0.0]

let a = 2.0
forall i in 0..4
    dst[i] = a * x[i] + y[i]

let host = dst
println(f'{host[0]} {host[1]} {host[2]} {host[3]}')

Output: 7.0 10.0 13.0 16.0.

Matrix multiply (naive)

A 2×2 product mapped as one thread per output cell, with the dot product computed by an in-kernel while loop. This is the correctness illustration — every thread reads global memory directly.

use system.gpu
use system.collections.array

gpu let a = [1.0, 2.0, 3.0, 4.0]
gpu let b = [5.0, 6.0, 7.0, 8.0]
gpu var c = Array<f32, 4>()

forall idx in 0..4
    let row = idx / 2
    let col = idx - row * 2
    var sum = 0.0
    var k = 0
    while k < 2
        sum = sum + a[row * 2 + k] * b[k * 2 + col]
        k = k + 1
    c[idx] = sum

let host = c
println(f'{host[0]} {host[1]} {host[2]} {host[3]}')

Output: 19.0 22.0 43.0 50.0. For the optimized counterpart — shared-memory tiles, barriers, explicit workgroup shape — see Shared Memory & Barriers.

Parallel reduction

On-device tree reduction returning a scalar — one launch, one 4-byte readback.

use system.gpu

gpu let data = [1, 2, 3, 4, 5, 6, 7, 8]
let sum = data.reduce(0, fn(a int, b int) int: a + b)
println(f'sum = {sum}')

Output: sum = 36. The result is a gpu-resident scalar. The host let binding is the fence. See On-Device Reduction for keeping it on the device.

Atomic histogram

Concurrent scatter writes through Atomic<u32> buckets.

use system.gpu
use system.gpu.atomic

fn main()
    gpu var hist = Array<Atomic<u32>, 256>()
    forall i in 0..147456
        atomic_add(hist, i % 256, 1 as u32)
    let host = hist
    let bucket_0 = host[0]
    let bucket_1 = host[1]
    println(f"bucket_0={bucket_0} bucket_1={bucket_1}")

Output: bucket_0=576 bucket_1=576.

Warp shuffle reduction

Register-only tree reduction over one subgroup — no shared memory, no barrier.

use system.gpu
use system.collections.array

gpu fn warp_reduce_sum(input Array<int, 32>, dst out Array<int, 1>)
    let lane = kernel.warp.lane_id
    var v = input[lane]

    v = v + kernel.warp.shuffle_down(v, 16)
    v = v + kernel.warp.shuffle_down(v, 8)
    v = v + kernel.warp.shuffle_down(v, 4)
    v = v + kernel.warp.shuffle_down(v, 2)
    v = v + kernel.warp.shuffle_down(v, 1)

    if lane == 0
        dst[0] = v

fn main()
    gpu let input = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
    gpu var dst = Array<int,1>()
    warp_reduce_sum(input, dst).launch(Dim3(1, 1, 1), Dim3(32, 1, 1))
    let result = dst
    println(f'{result[0]}')

Output: 528.

API reference

Accelerable

The capability trait that gates device residency. The compiler dispatches on the trait, never on a type name, so adding a new GPU-eligible container is an .mi edit, not a compiler change. User structs opt in with struct Point implements Accelerable.

public trait Accelerable
    fn byte_size() int
    fn binding_kind() AcceleratorBindingKind   // Storage | Uniform | PushConstant

gpu let / gpu var

Declare a device-resident binding. gpu let is immutable, gpu var is mutable. The initializer is an array literal, a sized constructor (Array<f32, N>()), or another gpu-resident binding (a move — the device handle transfers). Upload is deferred to the first kernel that captures the binding. The buffer persists across launches and is freed when the binding leaves scope.

forall / gpu forall

Launch a kernel over an index range (1D, 2D, or 3D). Bare forall routes by captured residency. gpu forall forces the device. Bounds may be literals, consts, or runtime values, including a runtime start. The body may capture device buffers and host scalars, index buffers, call scalar functions, and use arithmetic, if, and while.

gpu fn + .launch(grid, block)

A named kernel with explicit dispatch. Parameters are device buffers (gpu-resident at the launch site. out = writable) and scalars. shared arrays declare workgroup memory. Launch with kernel_name(args).launch(Dim3(gx, gy, gz), Dim3(bx, by, bz)). The block shape must be a compile-time literal and consistent across all launches of the same kernel.

kernel context

thread_idx, block_idx, block_dim, grid_dim, global_idx (each .x/.y/.z), barrier(), and warp.size / warp.lane_id / warp.shuffle_down(v, n). All available today. See The kernel Context.

Atomics — system.gpu.atomic

Atomic<i32> / Atomic<u32> buffer elements with atomic_add / sub / max / min / and / or / xor / exchange / compare_exchange(buf, index, …). Kernel-only. Plain-buffer or host-context use is rejected.

Vectors — system.gpu.vector

Vec2<T> / Vec3<T> / Vec4<T> with component fields and the builtins dot, length, normalize, cross (Vec3-only), reflect, mix, plus scalar broadcast. Inline std430 storage in arrays.

system.math on the device

abs, min, max, pow, sqrt, floor, ceil, round, sin, cos, tan, tanh, atan2, log, exp, step, clamp, mix — all usable inside kernels, width-preserving on f32.

Telemetry

gpu_reset_telemetry(), then gpu_uploads() / gpu_launches() / gpu_readbacks() / gpu_fences() return cumulative counts — the executable form of the cost model.

WGSL backend limits

Miri's first GPU backend targets WebGPU (WGSL) through wgpu, the most portable GPU host driver. A few features sit outside WGSL's core. Each is gated explicitly — refused before dispatch with a clear message, never miscomputed:

Review checklist — verifying GPU code

A reviewer (human or LLM) verifying a Miri GPU change should answer these six questions in order. If any answer is "no" or "not visible", the change needs work.

1. Residency. Does every GPU-touching binding start with gpu let / gpu var? Does every kernel capture refer to a device-resident binding or a captured host scalar? Does every gpu fn parameter type implement Accelerable?
2. Cost classes in order. List the cost events (upload, launch, fence + readback). Does the order match the source top-to-bottom? Are there any unexpected fences beyond a cross-residency assignment or .slice?
3. Buffer reuse. Do adjacent kernels over the same gpu var share the buffer (no cross-residency assignment between them)? Is there any let h = g; …; some_kernel(g) where the readback is wasted?
4. Mutability. Is every captured gpu var element written by exactly one thread? Concurrent writes to a non-Atomic element are a compile error — scatter patterns need Atomic buffers. Is every shared write followed by a kernel.barrier() before another thread reads it?
5. Bounds + indexing. Does every in-kernel arr[i] have a visible bounds guard when the index isn't bounded by the iteration range? In host code, are all element reads of device-resident bindings either compiler-rejected or bulk-copied first?
6. Portability. Does the change rely on 64-bit scalars, subgroup ops, or another gated feature? If so, is each one necessary, and is the requirement stated near the kernel?

What's Next

You can now write the full GPU surface: residency bindings, forall and gpu fn kernels, on-device reduction, shared-memory tiling, atomics, warp shuffles, vectors, and interactive gpu frame programs that ship to the browser.

Coming next on the GPU roadmap:

• Async GPU — async gpu blocks and explicit streams, overlapping transfer with compute.
• Kernel debugging — a gpu simulate mode: CPU interpretation of kernels with race and divergence detectors, plus in-kernel printing.
• Zero-copy on unified memory — opt-in host views over device buffers on UMA hardware.
• Native backends — a SPIR-V / Vulkan path first, for the features WGSL core can't express: 64-bit atomics, cooperative matrix, bf16/fp8.
• Richer reductions — multi-workgroup hierarchical reduce, min/max and general closure folds.