Residuals from the review of lukstafi#674 (gh-ocannl-950), deferred at its close-out (round 13) as non-blocking: the PR's criterion covers Set, Set_dynamic and Set_from_vec under a bound Workgroup_reduce; neither item makes it wrong for the shapes it claims.
-
Tile_mma under a bound Workgroup_reduce. Low_level.racing_lane_invariant_update falls through on Tile_mma, so a tensorized microkernel whose device-resident d base omits the outer reduction lane — Tile_mma is itself a read-modify-write of d, and its fallback holds the equivalent accumulating Set — is not judged, and the outer lane takes the hardware binding: several simdgroups would accumulate into one tile concurrently. validate_parallel accepts the write because it sits under both annotated loops. The natural fix is to walk the fallback in both traversals (go and stmt_reads), which delegates the judgement to the Set the fallback already spells; pin it with a leg that builds a Tile_mma whose d omits the lane under reduce_transform in test/operations/hardware_warp_shuffle.ml and expects the workgroup_reduce_race refusal. Whether the tensorize path can mint this shape (a split-K Workgroup_reduce above an mma nest with d indexed by the tile only) is the first thing to establish; if it cannot, refusing conservatively is enough.
-
Static-slot disjointness in has_accumulating_cell. reads_cell counts every Get_dynamic from the written node as a read of the written cell, so with peel censusing a store such as a[0,0] = a[1,dyn] is classified self-recurring although the fixed first slot proves the gather cannot reach the written cell. The race criterion already uses may_alias ~except:dyn_axis (round 11 of the PR); the recurrence helper should apply the same static-slot test (compare every slot but dyn_axis, with the PR's may_alias shape rather than exact equality). It is a precision refinement in the conservative direction — a false "recurrence" registers an ordinary level as a reduction site in census-based tests and experiments; it never lets a race through.
Residuals from the review of lukstafi#674 (gh-ocannl-950), deferred at its close-out (round 13) as non-blocking: the PR's criterion covers
Set,Set_dynamicandSet_from_vecunder a boundWorkgroup_reduce; neither item makes it wrong for the shapes it claims.Tile_mmaunder a boundWorkgroup_reduce.Low_level.racing_lane_invariant_updatefalls through onTile_mma, so a tensorized microkernel whose device-residentdbase omits the outer reduction lane —Tile_mmais itself a read-modify-write ofd, and itsfallbackholds the equivalent accumulatingSet— is not judged, and the outer lane takes the hardware binding: several simdgroups would accumulate into one tile concurrently.validate_parallelaccepts the write because it sits under both annotated loops. The natural fix is to walk thefallbackin both traversals (goandstmt_reads), which delegates the judgement to theSetthe fallback already spells; pin it with a leg that builds aTile_mmawhosedomits the lane underreduce_transformintest/operations/hardware_warp_shuffle.mland expects theworkgroup_reduce_racerefusal. Whether the tensorize path can mint this shape (a split-KWorkgroup_reduceabove an mma nest withdindexed by the tile only) is the first thing to establish; if it cannot, refusing conservatively is enough.Static-slot disjointness in
has_accumulating_cell.reads_cellcounts everyGet_dynamicfrom the written node as a read of the written cell, so with peel censusing a store such asa[0,0] = a[1,dyn]is classified self-recurring although the fixed first slot proves the gather cannot reach the written cell. The race criterion already usesmay_alias ~except:dyn_axis(round 11 of the PR); the recurrence helper should apply the same static-slot test (compare every slot butdyn_axis, with the PR'smay_aliasshape rather than exact equality). It is a precision refinement in the conservative direction — a false "recurrence" registers an ordinary level as a reduction site in census-based tests and experiments; it never lets a race through.