Raised by the review of lukstafi#674 (gh-ocannl-950), out of that PR's scope.
A Set under bound hardware axes whose cell MENTIONS every bound index is treated as per-thread by the binding: validate_parallel checks that writes are nested under every active hardware dimension, and gh-950's race criterion (Low_level.racing_lane_invariant_update) exempts a cell that mentions the lane. Neither proves the index map injective. acc[i + j] += x[i, j] under Workgroup j and Workgroup_reduce i mentions both, yet threads (i=0, j=1) and (i=1, j=0) hit one cell, and every GPU backend emits the hardware binding, which then races silently. The same holds for a plain Workgroup axis without any accumulation, so this is the binding's legality question rather than the accumulator-width or race-refusal one.
What would close it: an injectivity (or Affine.separates-style separation) proof of the written cell's index map over all concurrently active hardware axes at the binding decision, refusing (or serializing) where it cannot be shown; Ir.Affine already has the legality queries (gh-ocannl-485 family). Filed by the wave coordinator from Codex's round-7 finding on staging#674.
Raised by the review of lukstafi#674 (gh-ocannl-950), out of that PR's scope.
A
Setunder bound hardware axes whose cell MENTIONS every bound index is treated as per-thread by the binding:validate_parallelchecks that writes are nested under every active hardware dimension, and gh-950's race criterion (Low_level.racing_lane_invariant_update) exempts a cell that mentions the lane. Neither proves the index map injective.acc[i + j] += x[i, j]underWorkgroup jandWorkgroup_reduce imentions both, yet threads(i=0, j=1)and(i=1, j=0)hit one cell, and every GPU backend emits the hardware binding, which then races silently. The same holds for a plainWorkgroupaxis without any accumulation, so this is the binding's legality question rather than the accumulator-width or race-refusal one.What would close it: an injectivity (or
Affine.separates-style separation) proof of the written cell's index map over all concurrently active hardware axes at the binding decision, refusing (or serializing) where it cannot be shown;Ir.Affinealready has the legality queries (gh-ocannl-485 family). Filed by the wave coordinator from Codex's round-7 finding on staging#674.