+The checker simulates each pipeline's full and empty barriers per ring stage. A full barrier flips after every producer task of the resource has committed the stage and an empty barrier after every consumer task has released it, so one producer feeding several consumers is a broadcast, several producers feeding one consumer must all arrive, and a task that commits or releases fewer times than its partners is reported as a deadlock whose witness names the stage, phase, and arrival count. Operands of `TmaUmma`, `AsyncUmma`, and `UmmaUmma` consumers stay live past `release()`: the read hold ends at the next `acquire()` of that stage or at a `wait()` on a `UmmaAsync` or `UmmaUmma` resource that the same task commits after the reads (the `tcgen05.commit` pairing), so an aliased write issued in between is reported as a race. The checker proves acquire/wait availability and physical-range alias safety across expanded domain/work-tile loops and opaque assignments. It does not yet model PDL launch ordering or scheduler-specific CLC queue state. PDL and CLC metadata can be retained on host objects, but they are not currently part of the interleaving state, so those configurations require an external check.
0 commit comments