SentryWard is a static verifier for NVIDIA PTX kernels, built for the warp-specialized kernels of Blackwell GPUs. Given a kernel's PTX and a launch configuration, it proves that the kernel synchronizes correctly and is free of data races in every schedule. Given a PyTorch reference as well, it also proves that the kernel computes the same function.

Features

• Well-synchronization. Barriers and mbarriers, including TMA byte counts, behave the same way in every schedule. This also rules out deadlocks.
• Race freedom. Every pair of conflicting accesses to global, shared or tensor memory is ordered. Footprints follow exact layouts, including swizzling, and an SMT solver decides overlap for symbolic addresses.
• Resource lifetimes. Tensor memory and barriers are never used after they are freed or invalidated.
• Equivalence to a reference. The kernel's outputs equal those of a PyTorch reference, in real arithmetic.
• Witnesses. Every failed check comes with evidence, such as the two unordered accesses of a race. Anything SentryWard cannot decide is reported as unsupported, never as a pass.
• Blackwell coverage. TMA, tcgen05 MMA and tensor memory, mbarriers, thread-block clusters and asynchronous copies.

Results

Results for every kernel in our benchmark, with diagnostics and evidence, are in Kernel verification results.

Bugs in popular kernel libraries

SentryWard has found synchronization bugs in popular kernel libraries, such as a signal sent before the asynchronous write it announces has completed, and a buffer reused while the tensor core is still reading it. We have reported some of them upstream.

Removing redundant synchronization

Because SentryWard checks every schedule, it can also show that a synchronization operation is unnecessary: if the kernel still verifies without it, the operation is redundant. We applied this test greedily, one operation at a time, to 50 verified kernels from our benchmark.

Which synchronization is redundant may depend on the input shape. These results hold for the shapes we verified; other shapes may allow fewer removals.

Getting started

Install

pip install sentryward                # synchronization and memory checks
pip install "sentryward[reference]"   # adds PyTorch for reference equivalence

Wheels include the native verifier. Building from source needs CMake 3.27+, a C++20 compiler, OpenSSL, Boost headers and, optionally, Z3.

Verify a kernel

# Check synchronization and memory
sentryward kernel.ptx --input input.json > output.json

# Also check equivalence to a PyTorch reference
sentryward kernel.ptx \
  --input input.json \
  --reference reference.py \
  --reference-binding reference_binding.json \
  --timeout 500 \
  --memory-limit-mib 81920 > output.json

The same check from Python:

from sentryward import verify

result = verify(
    "kernel.ptx",
    input="input.json",
    reference="reference.py",                    # optional
    reference_binding="reference_binding.json",  # optional
    timeout_seconds=500,
    memory_limit_mib=None,                       # unlimited
)
print(result["result"], result["checks"])

The reference takes no separate input file. Its arguments are derived from the kernel's input configuration and the binding; anything that cannot be derived goes in the binding's reference section.

Read the result

The CLI prints a JSON result to stdout, and verify returns the same structure as a dictionary:

• result is the overall verdict. race_free means the synchronization and memory checks passed and no reference was given; verified means equivalence to the reference was proved as well. Other values name a finding, such as potential_race, or the reason the analysis stopped, such as unsupported or timeout.
• checks gives the status of each check: synchronization, memory and equivalence.
• diagnostics and warnings hold the details, including witnesses.
• equivalence holds the complete equivalence result.

How it works

For details, see our blog post or the paper (coming soon).

Limitations

• Problem sizes and the launch configuration are fixed.
• Branches and loop bounds may depend on the launch configuration, but not on tensor data unless explicit representative-control assumptions are enabled; see A006 and A007, both off by default.
• Fences and the full PTX memory model are not modeled. The hardware model follows our reading of the PTX documentation, which does not specify every detail.
• Equivalence treats floating-point values as real numbers, and the check is incomplete: finding no proof does not mean the kernel is wrong.

Repository layout

cpp/                C++ frontend, verifier and equivalence engine
sentryward/         Python CLI and process interface
corpus/             Compiled Blackwell PTX kernels of the benchmark
examples/<kernel>/  Input configuration and recorded output.json for each kernel
references/         PyTorch references and reference bindings
config/             Default and available analysis assumptions
skills/             Agent skills: prepare inputs, write reports, extend the PTX frontend
tools/              Example regression and reference-capture tooling
tests/              C++, Python, frontend and end-to-end tests

License

Apache License 2.0; see LICENSE.