Two bugs the H100 did not show

Aditya Kumar · 27 October 2026

TL;DR — Vx has a formal memory model: the rules for what a thread may read while other threads write the same memory. Tools check the model, but nothing checked the GPU code that vxc generates. So we wrote five of the model's litmus tests as Vx programs and ran each for over a million rounds on an H100. Every count was 0. The two controls, whose result the model allows, also gave 0, so the runs showed no weak result at all. Reading the PTX found two bugs. vxc generated a relaxed load that the GPU may move after a later store, which the model forbids. And LLVM 22 dropped the order of every read-modify-write, such as fetch_add, in a kernel. vxc now fixes the first bug and works around the second. We have not measured the cost on a GPU yet.

A memory model says what one thread may read when other threads write the same memory at the same time. Vx's model is in formal/memory_model/, and herd7, memalloy and Lean check it in three different ways. This post is about the first time we tested it on a GPU. It covers what that test could not tell us, and the two bugs that reading the PTX found.

What the model forbids

An atomic access in Vx has an order. A relaxed atomic promises only that the access itself is atomic. A release write and an acquire read promise more. When an acquire read sees a release write, the reader also sees every write that came before the release write in the writer's thread.

A litmus test is a small concurrent program with one question about its result. This is the load buffering test, in the format of herd7, a tool that lists every result a model allows:

{ x = 0; y = 0; }
 P0                  | P1                   ;
 r[rlx] r0 x         | r[rlx] r1 y          ;
 w[rlx] y 1          | w[rlx] x 1           ;
exists (0:r0 = 1 /\ 1:r1 = 1)

Threads P0 and P1 each read one place and then write 1 to the other place. All four accesses are relaxed. Can both reads see 1? For that, each read must see a write that the other thread makes after its own read. The reads and the writes then form a cycle.

Vx forbids this cycle, as RC11 does. RC11 (Lahav and others, PLDI 2017) fixes known problems of the C11 memory model, and the Vx model builds on it. The rule exists for a worse case. Suppose that each thread writes the value it read, instead of 1. A model that allows the cycle then allows both threads to read 42, though no thread ever wrote 42. The value came out of thin air.

C++ allows the load buffering result for relaxed atomics. It asks implementations not to make values out of thin air, but it does not define such values precisely. RC11 uses a simpler rule. It forbids every such cycle, including the harmless one above.

The rule can cost something on real hardware. AArch64, and PTX, the assembly language of NVIDIA GPUs, may move a relaxed load after a later store in the same thread. Then both reads can see 1, so the compiler must add something to keep the order. memalloy, a tool that compares memory models, found the AArch64 case when we wrote the model. No one checked a GPU.

Five litmus tests on an H100

Pull request #2293 added five of the model's litmus tests as Vx programs that run on a GPU. Each program uses two blocks with one thread each. A block is a group of GPU threads that runs on one streaming multiprocessor, so two blocks can run on different parts of the chip. Each program repeats its test for 100,000 rounds in one kernel launch.

This is the load buffering program. At the start of round k, each block adds 1 to its own counter in go and waits for the counter of the other block. So both blocks reach the test at about the same time. At the end, the host counts the rounds where both reads saw 1.

import core::sync::atomic;

fn main() -> i32 {
  let x = transfer(Tensor<i32, [100000]>::fill(0), Memory::HBM);
  let y = transfer(Tensor<i32, [100000]>::fill(0), Memory::HBM);
  let go = transfer(Tensor<i32, [2]>::fill(0), Memory::HBM);
  let mut seen = transfer(Tensor<i32, [200000]>::fill(-1), Memory::HBM);
  spawn on(Topology::Device) {
    for b in 0..2 across blocks {
      for l in 0..1 across lanes {
        for k in 0..100000 {
          let _a = atomic_fetch_add_i32(&go, b, 1, AtomicOrdering::Relaxed);
          loop {
            if atomic_load_i32(&go, 1 - b, AtomicOrdering::Relaxed) > k {
              break;
            }
          }
          if b == 0 {
            seen[b * 100000 + k + l] = atomic_load_i32(&x, k, AtomicOrdering::Relaxed);
            atomic_store_i32(&y, k, 1, AtomicOrdering::Relaxed);
          } else {
            seen[b * 100000 + k + l] = atomic_load_i32(&y, k, AtomicOrdering::Relaxed);
            atomic_store_i32(&x, k, 1, AtomicOrdering::Relaxed);
          }
        }
      }
    }
  }
  let s = transfer(seen, Memory::CPU_DRAM);
  let mut both = 0;
  for k in 0..100000 {
    if s[k] == 1 && s[100000 + k] == 1 {
      both = both + 1;
    }
  }
  println!("lb_relaxed_blocks: {} of 100000 rounds read 1 in both blocks", both);
  return 0;
}

A weak result is one that no interleaving of the two threads can give, so the hardware must have reordered something. Two of the five tests are controls. A control counts a weak result that the model allows. If a control prints more than 0, the setup can show weak results, and a 0 from the other tests means something. Each program also has a stress version, with 14 more blocks that load and store to their own memory while the test runs.

Each of the ten programs, five plain and five stress, ran 11 times on an NVIDIA H100 80GB HBM3, with 100,000 rounds per run. Every run printed 0:

These runs used a vxc from before the fixes below. So lb_relaxed_blocks had the relaxed load that the GPU may move, and it still printed 0.

What the zeros mean

Both controls printed 0 too. So this setup did not show a weak result at all, and the zeros of the other three tests are weak evidence. Two causes are likely. Every atomic in core::sync::atomic has system scope, the widest scope that PTX has. And the wait at the start of each round orders the two blocks more than the test needs.

The next design runs many pairs of blocks at once, with no wait in each round. It also needs a control with plain loads and stores, to show that this GPU gives a weak result at all.

The 0 from lb_relaxed_blocks also says nothing about its PTX. vxc generated ld.relaxed and then st.relaxed, and the PTX memory model lets the GPU reorder these two. A GPU that did not reorder them in 2.2 million rounds may still reorder them in another program, or on the next GPU.

Reading the PTX

The same pull request added a test that needs no GPU. atomic_orders_and_fence_scopes_in_ptx.vx compiles a kernel that uses each atomic order and fence scope once. It checks each PTX line against the mapping that NVIDIA publishes for C++ atomics. To check the test itself, we broke nine of the mappings in core::sync::atomic, one at a time. Each break made the check line that covers it fail.

At first, the test checked what vxc generated, including the relaxed load that the model forbids. Pull request #2299 fixed that load, and the work on it found a second bug, in LLVM.

A relaxed read stays before later writes

#2299 made each relaxed atomic read an acquire read. An atomic read is a load, a read-modify-write such as fetch_add, or a compare-and-swap. An acquire read keeps every later access of its thread after it, so the cycle of load buffering cannot form. Relaxed stores did not change.

For a kernel, vxc changes the order in the LLVM code before it generates the PTX. In the PTX, ld.relaxed.sys.global.b32 became ld.acquire.sys.global.b32. For host code, a new compiler pass, vx-order-relaxed-reads, makes the same change. It is the last pass that vxc runs. On x86, an acquire load is the same instruction as a relaxed one. On AArch64 and on a GPU, an acquire load may cost more. We have not measured how much.

A program that prefers the weaker rule can compile with -fweak-relaxed-atomics. The flag is like -ffast-math for floats: the program gives up a guarantee, which may make it faster. With the flag, relaxed reads stay relaxed, and lb_relaxed_blocks may print more than 0.

LLVM 22 dropped the order of read-modify-writes

A relaxed fetch_add now needed an acquire order on the GPU, so we looked at the PTX for each order. Here are five atomicrmw add instructions in LLVM IR, one for each order, and one cmpxchg. We compiled them with llc from LLVM 22.1.4 for an H100 (sm_90), and added the comments:

atom.global.add.u32  %r1, [%rd1], 1;              // monotonic (relaxed)
atom.global.add.u32  %r2, [%rd1], 2;              // acquire
atom.global.add.u32  %r3, [%rd1], 3;              // release
atom.global.add.u32  %r4, [%rd1], 4;              // acq_rel
atom.global.add.u32  %r5, [%rd1], 5;              // seq_cst
atom.acquire.sys.global.cas.b32  %r6, [%rd1], 0, 6;  // cmpxchg, acquire

All five read-modify-writes are the same instruction. NVIDIA's PTX manual says that an atom with no order is relaxed, and one with no scope has GPU scope. So in a Vx kernel, a fetch_add with AcqRel or SeqCst order was relaxed. If one block used such an atomic to tell another block that data was ready, the other block could read stale data. The compare-and-swap kept its order.

vxc now puts the order in fences around a relaxed atom, which NVIDIA's mapping allows. A read-modify-write that releases gets a release fence before it, or fence.sc if it is SeqCst. One that acquires gets an acquire fence after it. A SeqCst fetch_add is now:

fence.sc.sys;
atom.global.add.u32  %r1, [%rd1], 5;
fence.acq_rel.sys;

LLVM writes both the release fence and the acquire fence as fence.acq_rel. The PTX test now checks a relaxed, a release and a SeqCst fetch_add, with and without -fweak-relaxed-atomics.

LLVM fixed this bug in llvm/llvm-project#179553, merged on 5 February 2026. That was after LLVM 22 branched for its release, so the fix is in LLVM 23. vxc builds with LLVM 22, so it adds the fences itself.

The LLVM fix also taught a lesson about cost. Clang compiled CUDA's __nvvm_atom builtins as seq_cst atomics, though CUDA means them to be relaxed. The LLVM bug hid that mistake, because every order became a relaxed atom. When LLVM fixed the order, code that used those builtins got what the Clang fix called a "severe performance regression" (llvm/llvm-project#185822). Clang then made the builtins relaxed.

Vx now pays this kind of cost too. A relaxed fetch_add is a read, so it became an acquire read-modify-write, and the GPU runs a fence after it. A kernel that counts with a relaxed fetch_add in a loop now runs one fence per add. We have not measured that cost yet. -fweak-relaxed-atomics removes the fence.

What the GPU could and could not find

Both bugs came from reading the PTX against the PTX model. The H100 runs could not find the second bug, because no litmus program used an ordered read-modify-write. They could have shown the first, and did not. A count of 0 is strong evidence only when a control in the same setup counts more than 0. The NUMA that wasn't there found the same thing on a CPU: every check passed, and the locality it checked was not there.

What is left

• The cost. We will measure both fixes on the next rented GPU.
• A GPU test that can show weak results. Many pairs of blocks at once, no wait in each round, and a control with plain loads and stores.
• Atomics of block scope. Every atomic in core::sync::atomic has system scope, so the GPU programs test only that scope.
• Async copies. raw::async_copy is a plain copy today, so the model's async copy tests have no copy engine to test on a GPU.
• LLVM 23. When vxc builds with LLVM 23, it may leave the order of a read-modify-write to LLVM again.

The GPU programs are in formal/memory_model/gpu/, and the PTX test is tests/optimizations/pass/atomic_orders_and_fence_scopes_in_ptx.vx. The H100 results are on Vx#2291. The changes are Vx#2293 and Vx#2299. Vx is Apache 2.0 with the LLVM exception — install it and try the examples.