SPINモデルチェッカーを用いたCuTeカーネルにおけるデッドロック検出
SPINによるGPUカーネルGPUカーネルにおける同期バグやデッドロックは、ハードウェアからのエラー情報が乏しいためデバッグが極めて困難である。
本研究では、NVIDIA B200上のCuTe DSLカーネルの同期モデルをPromela DSLにエンコードし、SPINモデルチェッカーを用いてデッドロックの静的発見を試みた。
この手法は、デッドロックの存在をカウンター例として示し、または存在しないことを決定論的に証明することを可能にする。
これにより、従来の長時間かかるデバッグサイクルを劇的に短縮し、高速で信頼性の高いGPUカーネル開発を支援する。
原文の冒頭を表示（英語・3段落のみ）
Using SPIN model checker to statically find or prove the absence of deadlocks in CuTe DSL kernels on NVIDIA B200, and presenting a proof-of-concept github.com/cheshire/cute2promela lowering from CuTe to SPIN.
Synchronization bugs in GPU kernels are hard to debug. When a barrier deadlocks, the hardware yields no stack trace, and no error code until the benchmark times out. Hence each iteration of the debug loop starts to potentially cost tens of minutes.
As we’ve worked on FlashInfer MLSYS Challenge (our solution took 1st place in the mixture-of-experts track), we had to iterate on a persistent fused mixture-of-experts kernel for DeepSeek-V3, written in CUTLASS’s CuTe DSL for an NVIDIA B200 and stitched together from FF1, SwiGLU, and FF2 stages across clusters of CTAs. The pipeline is coordinated via mbarriers in shared memory, peer-CTA mbarriers reached via mapa-translated DSMEM pointers, and GMEM atomic counters across clusters. A bug in any of those can potentially result in a deadlock, which is hard to debug, especially when GPUs are only available via Modal.
※ 著作権に配慮し、引用は冒頭3段落までです。続きは元記事をご覧ください。