SentryWard introduced as an open-source formal verifier for GPU kernels

SentryWard's creators say the tool checks possible GPU execution schedules within a specified configuration and hardware model. They found 32 of 85 GPU kernels they analyzed had potential data races, synchronization bugs or resource lifetime violations. On evaluated kernels with specific input configurations on NVIDIA B200 GPUs, they say 42% of synchronization operations could be safely eliminated, with kernels running up to 1.4× faster after unnecessary waits were removed.