What a pointer forgets

10 September 2026

TL;DR — a float * cannot tell host memory from device memory. That is a hole in the type system, and no amount of analysis closes it across a compilation boundary. Vx puts the memory space in the type, so a 'placement' bug becomes a compile error.

A helper stages a tensor onto the GPU and hands it back. Everything the caller needs to use that value safely was known inside the helper, one line before the return. Whether any of it survives the return is a property of the language.

The program, in C++

Here it is the way it is usually written — allocate on the device, copy the host data over, return the pointer:

float *stage_to_device() {
    float *host_data = new float[16];
    float *d;
    cudaMalloc(&d, 16 * sizeof(float));
    cudaMemcpy(d, host_data, 16 * sizeof(float), cudaMemcpyHostToDevice);
    return d;
}

int main() {
    float *kv = stage_to_device();
    printf("%f\n", kv[0]);   // compiles. faults at run time.
}

That last line reads GPU memory from the host thread. It compiles clean, at any warning level, and faults when you run it. The question this post is about is whether anything could have stopped it.

The fact dies at the return

Inside stage_to_device the compiler has everything you would want it to have: d came from cudaMalloc, it is device memory, it is not addressable from the host. At the return statement all of it is discarded, because the return type is float * and float * has room for exactly one fact — the element type.

A host buffer and a device buffer are the same type. They are mutually assignable, and the read in main is a well-formed C++ expression.

Why a better analysis does not fix this

It is tempting to say an interprocedural pass should catch it. Here the fact is out of reach for a reason that survives any amount of analysis effort.

One definition of stage_to_device can be linked into a program whose caller has a device context, and into one whose caller does not. Compile it separately — into a shared library, or behind a kernel launch — and the analysis sees one body and must return one verdict covering every caller. The only verdict sound for all of them is the conservative one.

Inlining is the one mechanism that crosses a scope, and it works by deleting the boundary. It gives up in three places:

• at the inliner's budget;
• at an opaque framework op;
• completely, at a separately compiled launch, which cannot be inlined at all.

So the fact is not underdetermined at the boundary. It is absent. Recovering it is not the job. Carrying it is.

In Vx, the return type carries it

The same program, nine lines, with the whole point in the first one:

fn stage_to_device() -> Tensor<f32, [4, 4], Memory::GPU_HBM> {
  let host_data : Tensor<f32, [4, 4]> = Tensor<f32, [4, 4]>::new();
  return transfer(host_data, Memory::GPU_HBM);
}

fn main() -> i32 {
  let kv = stage_to_device();
  print(kv[0][0]);
  return 0;
}

The memory space sits in the type right next to the element type and the shape:

Tensor<f32, [4, 4], Memory::GPU_HBM>   ≠   Tensor<f32, [4, 4]>

Two different types. The signature states residency as part of the contract, so the caller's read is refused:

Error[E6003] at 43:9: 'kv' lives in GPU_HBM but CPU sees only [CPU_DRAM, NPU_HBM];
insert an explicit transfer to CPU_DRAM (cost 50 on the declared path)

The diagnostic names the space the value is in, the spaces the reader can address, and the repair. It arrives on a laptop with no GPU attached, because the machine Vx checks against is a declared file rather than the box the compiler happens to be running on.

The repair is one line

  let kv = stage_to_device();
  let home = transfer(kv, Memory::CPU_DRAM);
  print(home[0][0]);

That compiles, and the transfer survives into the emitted MLIR as a real operation rather than an assumption:

%0 = call @stage_to_device() : () -> memref<4x4xf32>
%1 = "vx.transfer"(%0) <{target_topology = 0 : i32}> : (memref<4x4xf32>) -> memref<4x4xf32>

This is the copy the C++ version also needed. It did not get told about it, and it is the same line either way — the difference is which day you write it, and whether you are paying for a rented GPU while you work out why the numbers are wrong.

One more thing the diagnostic knew:

cost 50 on the declared path

The same machine file that lets the compiler refuse the read is the file that prices the repair.

Six boundaries, five refusals

Residency across a function return is one case. The repository ships six, each about a different relation and a different place programs normally lose it:

Five of them are refusals. The fifth, the launch that carries a proof, is the other kind: nothing is wrong with the program, but the host has proved something the device compiler cannot see, so the proof is re-materialized inside the kernel as llvm.intr.assume and a 256-trip FMA chain that -O3 otherwise has to keep disappears. Both versions print the same answer.

All six are written up in Carrying facts across boundaries, with the code, the verdict the compiler gives, and a script that runs them. Vx is Apache 2.0 with the LLVM exception — install it, or read the heterogeneous model for how placement and reachability are checked.