Skip to content

fix: check a barrier against its own participants, not always the block's - #137

Merged
vyncint merged 1 commit into
mainfrom
fix/133-scoped-uniformity
Sep 10, 2026
Merged

vyncint merged 1 commit into
mainfrom
fix/133-scoped-uniformity

Conversation

@vyncint

@vyncint vyncint commented Sep 10, 2026

Copy link
Copy Markdown
Owner

Closes #133. Not a releasemain carries this unreleased until 0.7.0 is cut.

The defect

A guard uniform within a block settles sync_threads and settles nothing wider. blockIdx and cluster::block_rank() are constant on every thread of a block and different on the next one, so

#[cluster_launch(2, 1, 1)]
pub fn only_rank_zero() {
    if cluster::block_rank() == 0 { cluster::cluster_sync(); }
}

is entered by one block of the cluster and skipped by the other, and the block that arrived waits forever. 0.6.x reported nothing at all — exit 0, no findings, zero opaque, even with --strict.

Reproducing it showed the report was narrower than the defect: grid::sync() under a blockIdx guard was equally silent. Not a cluster quirk — BlockUniform conflated block-uniformity with cluster- and grid-uniformity, and every barrier wider than a block inherited it.

The model

A second lattice beside lane uniformity. LaunchScopeBlock ⊑ Cluster ⊑ Grid — records how far a value is actually constant; the dialect answers barrier_scope for how far each barrier reaches. A finding is raised when the guard's scope does not cover the barrier's.

The two axes stay separate on purpose. Uniformity answers a lane question and is what RC001 has always keyed on; nothing about divergent barriers changes. The scope axis speaks only where the lane axis has nothing to say — a lane-uniform branch over a barrier wider than a block.

Always warning, never promoted. The witness replays the lanes of one block; it cannot execute the second block this needs to show, so there is no concrete hang to confirm and confirmed would claim more than the evidence carries.

Precision — the harder half, and four of the six samples

Everything starts grid-constant and is narrowed only by what it reads:

kernel verdict
cluster_sync() under block_rank() RC001/warning
grid::sync() under blockIdx RC001/warning
sync_threads() under blockIdx clean — block guard, block barrier
grid::sync() under a kernel argument + blockDim clean — the false positive most worth not having
cluster_sync() under cluster_idx() clean — cluster guard, cluster barrier
cluster_sync() unguarded clean

Also verified: n + blockDim_x() stays grid-constant (clean), n + blockIdx_x() does not (fires). Arithmetic carries scope correctly.

That required splitting what BlockUniform used to cover — blockDim/gridDim, nsmid, gridid, nwarpid, the launch environment registers and the cluster's shape are GridUniform; cluster_idx is ClusterUniform; smid, blockIdx, block_rank and the cluster coordinates stay BlockUniform. An interprocedural site keeps the narrow default, since the callee's scope is not knowable from the call.

Breaking, deliberately — hence the label

reconverge-core's Callee, BarrierSite and Analysis gain fields; CallKind gains ClusterUniform and GridUniform. SimtDialect::barrier_scope has a Block default, so an existing dialect keeps compiling and keeps the narrow answer — reporting a block barrier as cluster-wide would invent a hazard, and a dialect that says nothing should not be made to.

cargo-semver-checks agrees: major passes, minor fails (exit 100) — the 0.x break this is.

Deep test

just ci green · conformance green · mutation corpus precision 1.0, published table unchanged · MSRV 1.88 · surface gate vs upstream 26754ae5 + its self-test · witness count unchanged (a warning gets no witness) · fixtures re-recorded, lesson copies refreshed, one golden blessed for a line shift.

Docs: explain RC001 and the README flip from "this is a known gap" to what is now checked, and the README's remaining gap is restated honestly — value flow through memory is still unmodelled, so a per-block value read back from global memory can guard a cluster barrier unremarked.

Closes #133

Signed-off-by: Vyncint Ng 115854244+vyncint@users.noreply.github.com

…ck's

A guard uniform within a block settles `sync_threads` and settles nothing
wider. `blockIdx` and `cluster::block_rank()` are constant on every thread
of a block and different on the next one, so

    #[cluster_launch(2, 1, 1)]
    pub fn only_rank_zero() {
        if cluster::block_rank() == 0 { cluster::cluster_sync(); }
    }

is entered by one block of the cluster and skipped by the other, and the
block that arrived waits forever. 0.6.x reported nothing at all -- exit 0,
no findings, zero opaque, even with --strict (#133).

Reproducing it showed the report was narrower than the defect: `grid::sync()`
under a `blockIdx` guard was equally silent. It is not a cluster quirk;
`BlockUniform` conflated block-uniformity with cluster- and grid-uniformity,
and every barrier wider than a block inherited that.

## The model

A second lattice beside lane uniformity. `LaunchScope` -- `Block` ⊑
`Cluster` ⊑ `Grid` -- records how far a value is actually constant, and the
dialect answers `barrier_scope` for how far each barrier reaches. A finding
is raised when the guard's scope does not cover the barrier's.

The two axes stay separate on purpose. `Uniformity` answers a lane question
and is what RC001 has always keyed on; nothing about divergent barriers
changes. The scope axis only speaks where the lane axis has nothing to say
-- a branch that is lane-uniform, over a barrier wider than a block.

Always `warning`, never promoted. The witness interpreter replays the lanes
of one block; it cannot execute the second block this needs to show, so
there is no concrete hang to confirm and `confirmed` would claim more than
the evidence carries.

## Precision, which is the harder half

Everything starts grid-constant and is narrowed only by what it reads, so
the common shapes report nothing:

  - a kernel argument (`if n > 0 { grid::sync() }`) -- the same on every
    block, and the false positive most worth not having;
  - `blockDim`/`gridDim`, and arithmetic over them or over an argument;
  - `cluster::cluster_idx()` guarding a *cluster*-wide barrier, since every
    block of the cluster reads the same value.

Which required splitting what `BlockUniform` used to cover:
`blockDim`/`gridDim`, `nsmid`, `gridid`, `nwarpid`, the launch environment
registers and the cluster's shape are `GridUniform`; `cluster_idx` is
`ClusterUniform`; `smid`, `blockIdx`, `block_rank` and the cluster
coordinates stay `BlockUniform`, which is what makes the check fire where it
should. An interprocedural site keeps the narrow default -- the callee's
scope is not knowable from the call -- so it is never asked the cross-block
question.

## Breaking, deliberately

`reconverge-core`'s `Callee`, `BarrierSite` and `Analysis` gain fields and
`CallKind` gains two variants. `SimtDialect::barrier_scope` has a `Block`
default, so an existing dialect keeps compiling and keeps the narrow answer
-- reporting a block barrier as cluster-wide would invent a hazard, and a
dialect that says nothing should not be made to.

cargo-semver-checks agrees: `major` passes, `minor` fails, which is the
0.x break this is.

## Tests

Six end-to-end lint samples, two that must fire and four that must not,
plus the dialect's scope classifications and `barrier_scope` by receiver.
The four negatives are the point: a check like this earns its keep by what
it stays quiet about.

Verified against the reporter's kernel and the grid-scope sibling; the
witness count is unchanged, since a warning gets no witness.

Signed-off-by: Vyncint Ng <115854244+vyncint@users.noreply.github.com>
@vyncint vyncint added the breaking Changes a promised public item; the semver gate runs as a minor for this PR label Sep 10, 2026
@vyncint
vyncint merged commit 1ad0eb5 into main Sep 10, 2026
14 checks passed
@vyncint
vyncint deleted the fix/133-scoped-uniformity branch September 10, 2026 06:55
vyncint added a commit that referenced this pull request Sep 10, 2026
…uest (#138)

`github.event.pull_request` does not exist on a push, so the `breaking` label expression silently yielded `patch` there. #137 merged a deliberate break with the label, was green as a pull request, and turned main red on the very next push — and would have stayed red until 0.7.0 moved the baseline.

A break is declared twice now, and the second declaration is the CHANGELOG: a `### Breaking` heading under `## [Unreleased]`, scoped to that section so a heading in a released one does not count. That is the document a release is cut from, so tying the gate to it means merging a break without recording it fails — a better rule than the label alone, which said nothing after the merge.

Exercised against three trees: [Unreleased] with the heading gives major, without it gives patch, and the heading present only under [0.6.1] gives patch.

Signed-off-by: Vyncint Ng <115854244+vyncint@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

breaking Changes a promised public item; the semver gate runs as a minor for this PR

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Uniformity is block-scoped: cluster- and grid-wide barriers under a block-uniform guard report clean

1 participant