reconverge

Static reconvergence analysis for Rust GPU kernels — catches divergent barriers and non-convergent warp operations at compile time, and shows you why, lane by lane, in your terminal. No GPU required.

The analysis, the four terminal views, and the CI integration are complete and tested, and every crate is on crates.io. Works with kernels written using cuda-oxide.

The problem

A GPU runs your kernel once per thread, and the hardware drives those threads in groups of 32 called warps. The 32 slots of a warp are its lanes. Two mistakes in that model are unusually hard to debug:

• A divergent barrier. sync_threads() waits for every thread in the block. If a branch lets only some threads reach it, the rest never arrive and the block waits forever. There is no error, no log line, and no stack trace — just a kernel that never finishes. Or, because it is undefined behavior, a kernel that finishes and lies: on a Tesla T4 the same probe ran to completion (docs/hardware/results/), which is a compiler's mercy, not correctness.
• A non-convergent warp collective. Operations like ballot_sync take a mask naming which lanes take part. If a named lane is not there, the result is undefined. This one often does not even hang: it returns a wrong value and your data carries it onward.

Neither bug is visible in the source, because what goes wrong — 32 lanes disagreeing about where they are — is never written down in the program. And owning the hardware does not help: a hung GPU cannot tell you which lanes are missing or which branch sent them away.

reconverge finds both at compile time, on any laptop, and shows you the disagreement:

#[kernel]
pub fn rc001_divergent_barrier(mut out: DisjointSlice<u32>) {
    let i = thread::index_1d();
    if i.get() % 2 == 0 {
        thread::sync_threads();   // only the even lanes ever arrive
    }
    // …
}

$ cargo reconverge check
error[RC001]: kernel `rc001_divergent_barrier` may execute `sync_threads()` under thread-divergent control
   --> src/lib.rs:184:9
    |
184 |         thread::sync_threads();
    |         ^^^^^^^^^^^^^^^^^^^^^^
    = note: lanes that skip the barrier never arrive, and the lanes that reach it wait for them forever — on hardware this is undefined behavior, usually a permanent hang with no error
    = note: witness: replayed with grid (1,1,1) x block (32,1,1), warp 0 — 16 of 32 lanes wait at `sync_threads()` while 16 never arrive; the barrier cannot be satisfied — undefined behavior on hardware, usually a permanent hang
    = note: lanes 0..31 at the failure point: W.W.W.W. W.W.W.W. W.W.W.W. W.W.W.W.
    = note: (W = reaches the call, . = never arrives)
    = provenance: thread-divergent branch (src/lib.rs:183)
    = provenance: _7: result of `ThreadIndex::<'kernel, IndexSpace>::get` on divergent _8 (src/lib.rs:183)
    = provenance: _8: derived from divergent `i` (src/lib.rs:183)
    = provenance: `i`: thread-index witness `index_1d()` (src/lib.rs:182)
    = help: make every thread of the block reach the barrier: hoist it out of the divergent branch, or make the branch condition uniform

Three things in that output are worth pointing at:

• witness: means this was not a guess. An interpreter ran your kernel's own compiled form for 32 lanes, with a concrete launch configuration, and watched the barrier starve.
• lanes 0..31 is the warp at the moment it stops: W waits forever, . left without arriving.
• provenance: walks backwards from the branch to the thread index that made it differ per lane — one hop at a time, so you can see why the condition is not the same for every thread.

Why this cannot be a runtime check

You might expect to catch these by running the kernel. You cannot, reliably: these are exactly the bugs a GPU is worst at reporting.

	needs a GPU	needs the failing input	sees the mask	points at the source	explains why
reconverge	no	no	yes	yes, with provenance	yes, and replays it
the vendor's dynamic checker (compute-sanitizer synccheck)	yes	yes	partly	at the launch	no
running it and watching	yes	yes	no	no	no
GPUVerify (research, pre-Volta)	no	no	no — predates masked warp primitives	yes	partly
Clippy and friends	no	no	no — no SIMT model at all	yes	n/a

A runtime checker only sees the launch you happened to run. A static analysis sees every launch your code allows. reconverge does both at once: it proves the problem exists for some launch, then produces one concrete launch that triggers it.

How it works

flowchart TB
  src["your kernel crate<br/>#[kernel] fn reduce(…)"]

  subgraph check["cargo reconverge check — one wrapped cargo build, on any laptop"]
    direction TB
    mir["Stable MIR · rustc_public<br/>your own source, never PTX / cubin / SASS"]
    dialect["dialect layer · recognizes items by path, and by receiver<br/>index witnesses · barriers · collectives · uniform sources"]
    core["uniformity engine · Uniform ⊑ Divergent<br/>post-dominator regions · provenance recorded as it goes"]
    wit["witness interpreter · 32 lanes<br/>replays a concrete hang, or declines to guess"]
    mir --> dialect --> core --> wit
  end

  subgraph art["versioned artifacts — what every front-end reads"]
    direction LR
    f["findings.v1"]
    u["unimap.v1"]
    w["witness.v1"]
  end

  base["baseline.v1<br/>reviewed suppressions,<br/>each with a written reason"]
  text["diagnostics · JSON · SARIF<br/>exit 0 / 1 / 2"]
  views["reconverge-tui<br/>inspect · witness · learn · triage"]

  src --> mir
  core --> f
  core --> u
  wit --> w
  f --> text
  f --> views
  u --> views
  w --> views
  base -. applied by check .-> text
  views -. triage writes .-> base

Loading

Nothing on that path touches a GPU vendor SDK. The analysis reads your Rust through the compiler's own intermediate form, and the warp rules it checks against come from public documentation. That is why it runs anywhere: in CI, on a laptop, in a container, with no driver installed. (Your crate still has to build: one that links the CUDA host API needs the toolkit's headers for that — see Using it.)

What it catches

Code	Tier	Finding	Explain
RC001	confirmed / warning	a block-, cluster- or grid-wide barrier — sync_threads(), cluster_sync(), this_thread_block().sync(), block_reduce — reachable under thread-divergent control	read
RC002	confirmed / warning	warp collective at a non-convergent point, or a mask naming absent lanes	read
RC003	deny	&mut [T] as a #[kernel] parameter — one exclusive reference handed to every thread	read
RC004	deny	static shared memory over the target's limit	read
RC005	warning	launch-contract inconsistency	read

RC006/RC007 (coalescing and bank-conflict lints) are reserved for v1.1. Every code has an explain page you can read in the terminal: cargo reconverge --explain RC001.

The confidence ladder

Findings are ranked by how they were established, not by how alarming they sound. The goal is that every finding shown by default is one you would defend in code review.

flowchart LR
  finding(["a finding"]) --> q1{"proven from<br/>syntax alone?"}
  q1 -- yes --> deny["<b>deny</b><br/>always shown · gates CI"]
  q1 -- no --> q2{"witness replayed<br/>a concrete hang?"}
  q2 -- yes --> conf["<b>confirmed</b><br/>always shown · gates CI<br/>carries the launch config and lane diagram"]
  q2 -- no --> warn["<b>warning</b><br/>hidden unless --strict<br/>never gates"]
  deny --> q3{"accepted in<br/>baseline.v1?"}
  conf --> q3
  q3 -- yes --> supp["<b>suppressed</b><br/>never gates, always counted<br/>SARIF suppression carries the reason"]
  q3 -- no --> rep["reported · exit 1"]

Loading

Zero false positives at default confidence is a requirement, not a goal. Every CI run pushes all of upstream's example kernels through the tool; any finding that has not been reviewed fails the build. Precision and recall are measured against a corpus of mechanically injected bugs and published in conformance/MUTATION.md, which CI regenerates so the numbers cannot quietly go stale. The other direction is gated too: a public function in upstream's warp, thread, barrier, grid, cooperative_groups or cluster module that the dialect neither classifies nor lists in conformance/SURFACE_ALLOW with a reason fails the build — an unrecognized call is a coverage note, never a finding, so "unknown" has to be a decision someone wrote down.

Four views in the terminal

How threads actually execute is invisible in source code, so half of this project is about making it visible. All four views read the same artifacts the analysis writes; none of them re-runs the analysis, and all work offline.

$ cargo reconverge witness            # step one warp through a recorded replay

┌ reconverge witness ──────────────────────────────────────────────────────────┐
│witness 1/2 — kernel `rc001_divergent_barrier` — RC001 — grid (1,1,1) block   │
│(32,1,1) warp 0                                                               │
│                                                                              │
│          0        8        16       24                                       │
│lanes     WoWoWoWo WoWoWoWo WoWoWoWo WoWoWoWo                                 │
│mask      (not at a warp collective)                                          │
│                                                                              │
│          o active   W waiting   . exited                                     │
│                                                                              │
│step 2/3  [=>.]                                                               │
│sync_threads() — 16 of 32 lanes arrive and wait                               │
│at lib.rs:184                                                                 │
│barrier: 16 of 32 threads arrived                                             │
│                                                                              │
│                                                                              │
│   0  launch                                                                  │
│   1  lanes evaluate the guarding branch — 16 continue toward `sync_threads`,…│
│▸  2  sync_threads() — 16 of 32 lanes arrive and wait             16 waiting  │
│   3  the other 16 lanes exit or move past reconvergence without ever reachin…│
│                                                                              │
│verdict: undefined behavior (at step 3)                                       │
│                                                                              │
└ h/l step  g/G ends  d split  v verdict  n/N witness  q quit ─────────────────┘

View	Command	What it is for
inspect	cargo reconverge inspect	browse source with uniformity labels; walk a value's provenance to its divergence source
witness	cargo reconverge witness	step one warp through the replay: 32 lanes, barrier arrivals, mask vs. active — with the whole run listed beside it, so the shape of the bug is legible without stepping
learn	cargo reconverge learn	four lessons — divergence, barriers, masks, reconvergence — driving the same replay engine over shipped recordings, fully offline
triage	cargo reconverge triage	review findings and record the accepted ones, with reasons, in the baseline

Every view takes --ascii for a terminal or font without the box-drawing glyphs: borders become +, - and |, and the other marks (—, …, the ▸ cursor) get ASCII stand-ins. The lane letters (o, W, .) are ASCII already, so the diagram reads the same in both.

An asciinema recording of the debugger walking the canonical hang and the mask mismatch is in docs/demo/.

Install

Three binaries cooperate: the CLI, the analysis driver, and the terminal views. Install the CLI, then let it fetch its own matching pieces:

$ cargo install cargo-reconverge
$ cargo reconverge setup

setup installs the pinned nightly toolchain — a rustc-driver tool must be built by the exact rustc it wraps — and reconverge-driver + reconverge-tui at the CLI's own version, into the install root that holds the CLI (a cargo install --root ~/.local cargo-reconverge keeps all three in ~/.local/bin), printing every command before it runs. The CLI looks for its two companions beside itself first, then on PATH. Prefer to do it yourself? The equivalent is (the @VERSION pins matter — all three binaries must be the same version, so pin both to the version of cargo-reconverge you installed):

$ rustup toolchain install nightly-2026-08-28 --profile minimal --component rustc-dev --component llvm-tools --no-self-update
$ rustup run nightly-2026-08-28 cargo install --locked reconverge-driver@VERSION reconverge-tui@VERSION

The driver links rustc's own crates, so it must be built by exactly the pinned nightly, with rustc-dev, the component that ships them. A git checkout inherits both from this repository's rust-toolchain.toml; a crates.io install carries no toolchain file, so they have to be asked for. The driver's build script checks both — the compiler's commit against the pin, then the component — and stops with the command to paste rather than a build that fails later: on stable or on any other nightly it says reconverge-driver must be built by nightly-2026-08-28 and ends with rustup run nightly-2026-08-28 cargo install --locked reconverge-driver@VERSION.

Prebuilt binaries

Each GitHub release carries one archive per target, built by release.yml, for exactly two: x86_64-unknown-linux-gnu and aarch64-apple-darwin. Anywhere else — Intel macOS, Linux on ARM, Windows — install from crates.io as above.

$ shasum -a 256 -c reconverge-vX.Y.Z-<triple>.tar.gz.sha256
$ tar -xzf reconverge-vX.Y.Z-<triple>.tar.gz
$ rustup toolchain install nightly-2026-08-28 --profile minimal --no-self-update
$ cp reconverge-vX.Y.Z-<triple>/{cargo-reconverge,reconverge-driver,reconverge-tui} ~/.cargo/bin/

Two things make or break it:

• Keep the three binaries in one directory on your PATH. cargo-reconverge looks for the driver and the views beside its own executable first.
• The pinned nightly must be installed. The driver links that toolchain's librustc_driver dynamically and does not ship it; cargo-reconverge puts the toolchain's library directory on the driver's search path when it runs it. rustc-dev is needed to build the driver, not to run it, so the minimal profile is enough here. If it is missing, check says so and names that one command — not setup, which would rebuild what the archive already holds.

Using it

$ cargo reconverge check                       # analyze; exit 1 on deny/confirmed findings
$ cargo reconverge check --strict              # include warning-tier findings
$ cargo reconverge check --cc 8.6              # target capacity context for RC004
$ cargo reconverge check --cc sm_90a           # the CUDA spellings work: sm_86, compute_86, 86, sm_90a
$ cargo reconverge check --sarif out.sarif     # SARIF 2.1.0 for code scanning
$ cargo reconverge check --message-format json # one findings.v1 document per target
$ cargo reconverge check --package my-kernels  # only this member (repeatable); --exclude for the rest
$ cargo reconverge check --require-kernels     # exit 2 when no #[kernel] was analyzed
$ cargo reconverge watch                       # re-run on every save
$ cargo reconverge --explain RC002             # why it is a bug, and the idiomatic fix

Exit codes: 0 clean, 1 findings at deny/confirmed confidence, 2 tool error. Every lib and bin target of the workspace is analyzed and gated, under the target's own crate name, so kernels in src/bin/*.rs count too. A run that found no #[kernel] at all still exits 0, but says so — no #[kernel] functions found in 1 crate — nothing was analyzed — rather than reading like a clean pass; --require-kernels makes it a failure.

The build always runs under the pinned nightly, whatever toolchain rustup picked for your project; set RECONVERGE_TOOLCHAIN only for a driver you built with another one (RECONVERGE_DRIVER).

No GPU is needed, but the build has to succeed. check builds the crates it analyzes the way cargo check does, build scripts included. A single-source crate that links the CUDA host API (cuda-host, cuda-core) runs cuda-bindings' build script, which needs the CUDA toolkit's headers — not a GPU, not a driver, but the toolkit. Either install the toolkit where check runs, or keep the kernels in a device-only crate and check that one: cargo reconverge check --package my-kernels.

In CI, the GitHub Action is three lines:

- uses: actions/checkout@v7
- uses: vyncint/reconverge/action@v0
  with:
    cc: "8.6"

Accepting a finding

A finding you have reviewed and decided to live with goes in reconverge-baseline.json, written by cargo reconverge triage, which requires a reason for every entry. An accepted finding is a decision, not a disappearance: it stops gating CI, but it is still counted in every summary, still printed by --show-suppressed with its reason, and still exported to SARIF as a suppression carrying that reason as the justification. Entries match on (crate, kernel, code) — never on line numbers, which move the first time anyone edits above them.

Limitations

What reconverge does not do. A tool that overstates its reach is worse than one that does less.

• The decidable slice only. Uniformity is computed as dataflow; there is no SMT solver and no general race freedom. Data races are out of scope — deleting a barrier is a race, and no static tier here will flag it.

• Not in scope, by decision. Register budgeting: #[launch_bounds] is read as a uniform marker and nothing here models register pressure — that needs ptxas output, which is a build tool's concern, not a MIR analysis's. Memory and DisjointSlice<T>: exclusivity is the type's guarantee in cuda-oxide; RC005 checks the index-uniqueness half (declared domain against the proven index formula) and RC003 the parameter shape, and no rule here reasons about which thread writes which address across warps.

• Uniformity is scoped, and the value lattice is still two-valued. Since 0.7.0 a barrier is checked against its own participant set, so cluster_sync() under a cluster::block_rank() guard and grid::sync() under a blockIdx guard are both reported — at warning, never promoted, because the witness replays one block and cannot execute the second. What is still not modelled is value flow through memory: a value loaded from global memory is treated as constant wherever its address is, so a per-block value written by another kernel and read back can guard a cluster barrier without a word from this rule. That is the same recall gap the interprocedural note below describes, in a new place.

• Split barriers are checked at the wait. The mbarrier family and the raw barrier.cluster.arrive/.wait pair are phase-counted: partial participation at an arrival is the designed use, so only the blocking half is RC001's subject. if c { arrive() } wait() is a real hang this does not report, recorded in explain RC001 and in conformance/SURFACE_ALLOW with the reason.

• Reducible CFGs. An irreducible control-flow graph degrades to all-divergent for that function, and the diagnostic says so rather than pretending otherwise.

• Interprocedural analysis is per kernel and context-insensitive. Since 0.8.0 every local function a kernel reaches is analyzed — its body, its parameters and its return value (#188) — so a divergent barrier inside a helper, a barrier guarded by a parameter the kernel passes a thread index, and a branch on a helper that returns one are all reported, against each kernel that reaches them. Inside one kernel a helper is analyzed once, each parameter joined over every call to it; two kernels never share a join, so a helper a second kernel calls with uniform arguments is not blamed on it. A return value is summarized on its own (divergent, and how widely constant) and added to the call's arguments, never substituted for them. Trait methods, generic functions and closures resolve to the body they run, per instance (#189).

  A finding reached this way stays at warning unless a replay confirms it, and the replay splices the helper into the kernel — the bounded inliner: non-recursive callees, at most two frames, and a ceiling on the spliced result. That replays the actual calls, not the join the static finding rests on. Nothing is promoted on a summary; the summary raises the finding, a trace confirms it. A call the inliner left in place is never stepped over either: when a lane's path meets one whose summary says it may synchronize, the replay stops and the finding carries a replay: note naming the call — until 0.8.0 such a call read as a statement with no barrier, and a recursion every thread completed was "confirmed" with one lane waiting.

  What is not followed: a call through a function pointer or a dyn method, a trait method on a generic kernel's type parameter, and a function in another crate of the workspace — each crate is compiled, and analyzed, on its own. Those calls are counted as opaque (below) rather than read as barrier-free, and their results are divergent rather than guessed. A closure handed to a library function (for_each, map) is analyzed and counts toward the call, but nothing says how often the library runs it, so such a finding is never promoted. Library code that calls back into a local trait impl (Iterator::sum over a local iterator) is not followed, and value flow through memory is not tracked here any more than inside one function.

• RC001 covers the all-threads barriers — thread::sync_threads, cluster::cluster_sync and the blocking half of the raw pair behind it (barrier_cluster_wait*; the arrival half signals and returns, so it cannot hang and is not a barrier here — explain RC001), grid::sync, and the cooperative-groups barriers this_thread_block(), this_grid() and this_cluster() .sync() (told apart by receiver, since ThreadGroup::sync is one path for five barriers) plus block_reduce and block_scan, which carry a barrier inside. The shared contract is that every thread of the scope must reach the call — and since 0.7.0 scope is taken literally: each barrier is checked against its own participant set, so a guard that is only block-uniform is enough for sync_threads and not for cluster_sync or grid::sync. Deliberately out, each with its reason in conformance/SURFACE_ALLOW: the mbarrier arrive/wait family and the counted CTA barrier (barrier_cta_*), where partial participation is the designed use; and the tile-scoped WarpTile<N>::sync, warp_reduce, warp_scan and coalesced_threads(), whose participant set is a tile or the active lanes rather than the warp.

• RC002 covers the whole collective surface — every *_sync function of cuda-device's warp module (mask-first by convention, including the f32 redux_sync_* family upstream added in September 2026), plus sync_mask, plus the unmasked convenience wrappers (warp::shuffle, warp::ballot, all, any, popc, the reduce_* helpers). The wrappers take no mask argument, but they are the thing that supplies one — each delegates to its *_sync counterpart with u32::MAX — so the mask is known from the call rather than inferred from a callee the analysis cannot see, and warp::ballot(x) under divergence is treated exactly like warp::ballot_sync(0xffff_ffff, x).

  The reduce_*_partial helpers are the one collective whose mask is neither full nor an argument: they build it from a runtime live_lanes value. They are still reported, with the mask named as not evaluable — a warning that says "found this, cannot check the mask" rather than the silence of not looking at all.

• A construct the declared launch cannot reach is reported at warning and never promoted. The syntactic recognizer speaks — a launch contract is a declaration, not a proof, and a kernel launched outside its declared shape would otherwise lose the diagnostic entirely — while the replay finds no lane that arrives and so has nothing to confirm. Such findings never gate, and they carry a replay: note naming that outcome — "unreachable under the declared launch" is close to knowledge, and is now distinguishable, by a reader and by anything consuming findings.v1, from a construct the replay simply could not evaluate.

• RC002's replay compares the mask against the lanes present. A literal mask at a divergent call promotes to confirmed exactly when it names a lane the replay proves absent; a mask naming exactly the arriving lanes — the guarded partial-warp idiom — is never promoted and never gates, and now says so: the finding carries a replay: note recording that the mask was checked against the lanes present and matched, so a verified idiom no longer reads like a mask the tool could not evaluate. What the replay does not do is mask arithmetic against launch shapes other than the one it runs (one full warp).

• active_mask guards stay warnings; the positional mask registers do not. The five lanemask_* registers are closed forms of the lane's own ordinal — lanemask_lt is every lane below it, and so on — so they do not depend on which lanes are still running, and the replay evaluates them. The lane-ordinal idiom warp::lanemask_lt().count_ones() replays, and a guard on it is witness-promoted like any other. warp_id and live_lanes_1d are exact under the replayed launch too.

  active_mask is the exception, and for a different reason: its value is the set of lanes still live at that point, which changes as lanes diverge. That is path-dependent rather than positional, so it stays unknown, findings under such a guard are never witness-promoted, and a finding below one with a barrier inside it stays at warning too.

  The arithmetic a 32-bit mask flows through is width-typed: integer ! is the complement at the operand's own width, casts truncate to their target width, and overflow-checked arithmetic was already width-typed. Every binary operator carries its operand's type too, signedness included, so x < 0, x / 2 and x >> 1 on an i32 are the signed operations — they were unsigned until 0.8.0, which made -(lane as i32) < 1 false on 31 lanes. Where a type is unavailable the interpreter yields unknown rather than assuming one.

• Every site is attempted, but an unknown branch over a barrier stops the ones below it. Promotion is per site, so a function with several divergent sites can carry several witnesses, whatever mix of divergence sources they use. An unevaluable guard upstream does not by itself cost the sites below it either: when the branch's paths rejoin without touching a synchronization point, the choice cannot change who arrives, so the replay skips it.

  Two things do stop a later site, and both are cases where no lane reaches it rather than cases the replay gave up on:

  • an unevaluable branch whose paths contain a barrier or collective — those lanes may be waiting there and may never arrive, so the replay declines rather than naming a lane split it cannot stand behind; and
  • earlier barriers that already deadlock the block between them. If one guard sends half the lanes to a barrier and its complement sends the other half to a different one, both halves wait forever and nothing continues past them. A third site below is unreachable in fact, not merely unproven.

  In both, the finding stays at warning and the upstream barrier is itself reported — which is where the reader should be looking anyway.

• The replay runs the declared block, and only that. A kernel whose #[launch_contract] declares block = (x, y, z) is replayed in that shape — 2-D and 3-D included, lane n being the thread at linear index n with x fastest, which is how warps are formed — so threadIdx_y() under (16, 2, 1) is 1 on lanes 16..31, and a warp_id()-guarded barrier that is safe at one warp and undefined at two gates exactly when the contract says two. A kernel with no contract is replayed as one warp, (32, 1, 1). A declared block the replay cannot run — not a whole number of warps, or wider than 128 threads — is not replayed at all: the finding stays at warning with a replay: note naming the shape. Until 0.8.0 such a block was replayed as (32, 1, 1), a launch the contract excludes, and a (16, 16, 1) kernel whose every thread passed a threadIdx_x() < 16 guard was "confirmed" as a hang. A collective on a lane's path does not stop the replay: collectives are modeled per warp, so a warp whose still-running lanes are all at the same collective passes it whatever the other warps are doing, while the barrier remains the only construct that synchronizes across warps. A configuration that would need warps to interact — a warp split between a warp-scoped collective and a block-scoped barrier — is declined rather than approximated. The site itself must still be a barrier beyond one warp: a mask comparison is a per-warp question, and an error there would produce a witness that looks exactly like a correct one. A collective site under a declared multi-warp block therefore stays at warning, with a replay: note saying so.

• A warp-uniform guard is not a divergent one for a collective. A warp collective's participants are one warp, so a guard that every lane of a warp reads the same — warp_id() == 0, threadIdx_x() / 32 == k, threadIdx_x() >> 5 — lets each warp take the branch whole, and a full-mask collective under it is not RC002. A barrier under the same guard still is RC001: whole warps skipping sync_threads() is the hang. Whether threadIdx_x() / 32 is a warp number depends on the block — under (48, 2, 1) one warp holds x 32..47 of one row and 0..15 of the next — so it counts only when the declared block is 1-D, has rows of whole warps, or has rows no wider than the divisor. A kernel with no contract keeps the warning, with a note that declaring the block settles it.

• Opaque regions are reported, not guessed at. asm!, unmodeled intrinsics, and calls the analysis cannot follow (a function pointer, a dyn method, a sibling workspace crate, an extern device function) are counted, and the tally is a property of the run, not of a finding: it rides in findings.v1 as coverage, is printed as a note on every finding in the affected kernel, and closes the summary line whenever anything was left unread — including a run with no findings at all. That last case is the one it exists for: a bar.sync 0 inside an asm! block under a divergent guard is a real barrier this tool cannot see, and 0 deny, 0 confirmed, 0 warning findings on its own does not say whether the kernel is clean or whether a twentieth of it was never read.

• Masks that are not literals — a named const, or anything computed — cannot be evaluated through rustc_public at the pinned toolchain, so RC002 reports convergence and says the mask was not evaluable rather than guessing at it. The boundary is the exposed surface rather than the compiler's ability: a named const arrives as ConstantKind::Unevaluated where a literal arrives as Allocated, ConstDef offers no way to read the initializer, and the one evaluation entry point on MirConst, eval_target_usize(), assumes a usize and ICEs on a u32 mask ("expected int of size 8, but got size 4") — after resolving the value, so what is missing is an API that returns it at its own width.

• The pinned nightly is not optional. A rustc-driver tool and the rustc it wraps must be the same build. The pin is the toolchain upstream cuda-oxide used at the commit this release is verified against (conformance/PIN), not necessarily the one upstream pins today: upstream has since split into a monorepo whose device crate is on 1.99.1. Until the pin moves, analyze kernels written against that commit. pins.yml checks every week and keeps one issue current with what moved — the commit, the toolchain governing upstream's device crate, or a device-surface function this dialect has not decided.

• Platforms: Linux, macOS and Windows, all gated in CI. Nothing here needs a GPU or a vendor SDK on any of them (a crate that links the CUDA host API needs the toolkit to build at all; see Using it), and the analysis, check, the artifact round-trip, the schemas and the CLI contract are tested on all three. The four terminal views are gated on Linux and macOS only. They are believed to work on Windows and are not held to it: under ConPTY the PTY suites time out waiting for a frame boundary while the screen they print is correct and complete, which is a difference in how that console delivers what an application wrote rather than in what these views render. Root-causing it needs a Windows machine (#162). A Windows clone also needs the lesson prose checked out with LF, which .gitattributes handles here. Prebuilt archives exist for two targets only (see Prebuilt binaries); every platform installs from crates.io.

Status

Everything on this page is implemented and gate-tested: the five diagnostics with their witness promotions, the four terminal views, the GitHub Action, the conformance gate, and the mutation corpus behind the published numbers. reconverge is released and published on crates.io.

Both hardware sessions have now run. Session #1 on a Tesla T4 (2026-09-09) and session #2 on an A10G (2026-09-22), with the data in docs/hardware/results/.

Session #2 is the external check, because everything else here is measured against a corpus this project wrote for itself: the same injected bugs, run under NVIDIA's own compute-sanitizer --tool synccheck. Three results from it are worth knowing before you choose a tool.

• The dynamic checker did not report RC003 at all. Seven mutants that hand one &mut [T] to every thread ran clean under it; reconverge denies all seven from syntax alone.
• Three of nine injected barrier-divergence bugs passed on hardware — no hang, nothing reported. That is the accidental pass this page describes, measured: a dynamic tool sees the launch you ran, not the launches your code allows.
• delbar is where the vendor's tool wins. synccheck flagged two deleted-barrier mutants; a deleted barrier is a data race, which is outside the decidable slice here by design. The two approaches are complementary, not ranked.

Next on the engineering side: RC006/RC007, the coalescing and bank-conflict lints, with the lanes-to-address-grid visualizer that goes with them.

Documentation

Document	What is in it
docs/ARCHITECTURE.md	how the pieces fit: crate graph, the analysis pipeline in detail, the artifact contract, isolation invariants, test strategy
docs/explain/	one page per diagnostic code: a minimal failing kernel, the hardware reason, the idiomatic fix
docs/learn/	the four SIMT lessons (also embedded in cargo reconverge learn)
schemas/	the versioned JSON Schemas — the contract between the engine and every front-end
docs/hardware/	the hardware sessions — how a true positive is run on a real GPU under a watchdog, and what a Tesla T4 actually did
conformance/	how the zero-false-positive gate, the surface gate (SURFACE_ALLOW) and the mutation corpus work, plus the published precision/recall table
CONTRIBUTING.md	dev setup, testing policy, commit conventions, review rules for the baseline
CHANGELOG.md	what has landed, and the corpus and found-in-the-wild numbers behind it

Contributing

Issues and pull requests are welcome — including, especially, false positives: there is a dedicated issue form for them, and every confirmed one becomes a permanent regression test before it is fixed.

Development needs the pinned toolchain and just:

$ just setup    # materialize the toolchain, wire the local hooks
$ just ci       # everything CI gates on: fmt, clippy, tests, docs, deny, isolation

AI assistance is welcome; AI attribution is not. Remove the trailer and recommit — you are the author of record.

License

Dual-licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE)
• MIT license (LICENSE-MIT)

at your option. Contributions are accepted under the same terms, signed off under the Developer Certificate of Origin (git commit -s).