Metadata-Version: 2.4
Name: sentryward
Version: 0.1.0
Summary: Static verifier for synchronization, memory lifetime, and memory races in PTX kernels
Keywords: verification,static-analysis,data-race,synchronization,gpu-kernels
Author: Zhihao Jia
License-Expression: Apache-2.0
License-File: LICENSE
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Operating System :: MacOS
Classifier: Operating System :: POSIX :: Linux
Classifier: Programming Language :: C++
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Software Development :: Quality Assurance
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.10
Provides-Extra: reference
Requires-Dist: torch>=2.5; extra == "reference"
Provides-Extra: dev
Requires-Dist: ijson<4,>=3.5; extra == "dev"
Description-Content-Type: text/markdown

<div align="center">

# SentryWard: Formal verification of warp-specialized GPU kernels

*Reveal hidden bugs in GPU kernels.*

[![License](https://img.shields.io/badge/license-Apache--2.0-blue)](LICENSE)
[![Python](https://img.shields.io/badge/python-3.10%2B-blue)](pyproject.toml)
[![Target](https://img.shields.io/badge/target-NVIDIA%20Blackwell%20sm__100-76B900)](corpus/)

[Features](#features) ·
[Results](#results) ·
[Getting started](#getting-started) ·
[How it works](#how-it-works) ·
[Blog](#) <!-- TODO: blog URL -->

</div>

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](docs/kernel-verification-results.md).

### 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.

| Measure | Result |
| --- | --- |
| Synchronization operations found redundant | **48.7%** of those tried |
| Kernels faster on a B200 after removal | **35 of 44** reduced kernels |
| Median reduction in kernel time | **6.8%** |
| Output check | Identical outputs to the original over 500,000 random launches |

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

```bash
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

```bash
# 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:

```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"])
```

| CLI | Python | Description |
| --- | --- | --- |
| `--input` | `input` | Required. The kernel's input configuration (JSON). |
| `--reference` | `reference` | Optional. A Python file that defines a `reference(...)` function. |
| `--reference-binding` | `reference_binding` | Optional. Maps the reference to the kernel's inputs and outputs. Defaults to `reference_binding.json` next to the reference, then in its parent directory. |
| `--timeout` | `timeout_seconds` | Total budget for the whole call, including reference capture. Default: 600 seconds. |
| `--memory-limit-mib` | `memory_limit_mib` | Memory budget as a positive integer in MiB, e.g. 81920 for 80 GiB. Default: unlimited. |

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

<p align="center">
  <img src="assets/pipeline.svg" alt="How SentryWard verifies a kernel: specialization, the event and value views, the well-synchronization check, the race and lifecycle check, memory elimination, and the expression check" width="900">
</p>

For details, see our [blog post](#) <!-- TODO: blog URL --> 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](ASSUMPTIONS.md#a006--representative-data-dependent-control) and
  [A007](ASSUMPTIONS.md#a007--terminating-spin-waits), 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

```text
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](LICENSE).
