Visitar URL original
[cl] Model barrier phases and UMMA operand liveness in the exhaustive… · NVIDIA/cutile-python@6f7099f · GitHub
Skip to content

Commit 6f7099f

Browse files
author
Cong Zhang
committed
[cl] Model barrier phases and UMMA operand liveness in the exhaustive checker
1 parent 6e2411c commit 6f7099f

4 files changed

Lines changed: 1250 additions & 116 deletions

File tree

‎experimental/task_scheduling/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,6 @@ The exhaustive checker is bounded by `max_states`. Its result reports `hit_state
202202

203203
## Current limitations
204204

205-
The current 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.
205+
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.
206206

207207
Pipeline groups, interleave strides, multicast signaling, and deferred barrier storage are validated as host metadata. Generic device materialization for those combinations is not implemented. The copy and GEMM tutorials exercise the shared TMA-to-async, TMA-to-UMMA, and UMMA-to-async lowering while their callbacks contain only pipeline payload work. Static pipeline auditing recognizes the corresponding CUDA Lang calls but does not infer effects hidden behind arbitrary user wrappers.

0 commit comments

Comments
 (0)