Many short tapes

Aditya Kumar · 23 September 2026

TL;DR — C, C++, Rust, Java and Python each define themselves against an abstract machine with a single memory: one array of bytes, addressed by one kind of integer, large enough for whatever is asked of it. That is Turing's tape. The machines we run on have many memories, each with a size, each reachable from some processors and not others. Vx takes a description of those memories as input and checks programs against it.

Turing needed a tape that never runs out, because his question was what can be computed at all. Ours is what can be computed on this machine, and the answer depends on sizes.

The tape

The C standard describes a program's meaning in terms of “an abstract machine”, and C++ and Rust follow it. The details differ. The memory is the same in all three: one flat space of bytes, where every object has an address and every address is a number of the same kind.

That memory has no size the program can talk about. It can only be found by running out:

In every row, capacity is an event at run time. None of these languages lets a type say “this fits”, because there is nothing for it to fit into.

Strictly, C's tape does end. Pointers have a fixed width, so a 64-bit C implementation can name at most 2⁶⁴ bytes, and people have argued on those grounds that C is not Turing complete. But 16 EiB is a limit no program meets. The limit a GPU program does meet is 80 GiB, and the type system has no way to mention it.

The machine

Here is one node with an H100 in it, from the outside in:

• host DRAM, split into NUMA domains, each attached to one socket;
• 80 GiB of HBM on the GPU, reached from the host over PCIe;
• 50 MiB of L2 inside that;
• 228 KiB of shared memory in each of 132 streaming multiprocessors;
• and, on bigger systems, a peer GPU over NVLink, a CXL memory expander, or another node's memory over RDMA.

Three properties of this list have no counterpart on the tape.

Every memory is bounded, and the small ones matter most. Host DRAM is large enough that the tape is a fair approximation. Shared memory is 228 KiB, and a kernel's whole performance depends on what fits in it.

The memories are disaggregated. They are separate pools on separate devices, joined by links, each with its own bandwidth. Moving a byte from host DRAM to shared memory is three hops at three different speeds.

They do not form one linear space. A host address and a device address can be the same number and name different bytes. Shared-memory address 0 exists 132 times at once, once in each SM. A processor can address some of these memories and has no way to address others.

How languages keep the tape

On the host, the operating system maintains the illusion. Virtual memory, paging, overcommit and the OOM killer let a program behave as if memory were one large array, and when the illusion fails it fails at run time, often somewhere unrelated to the allocation that caused it.

On a GPU there is less illusion to maintain. cudaMalloc returns cudaErrorMemoryAllocation. Managed memory extends the illusion across the bus by migrating pages on demand, which is correct and shows up later as time in a profile. A framework like PyTorch keeps a caching allocator in front of all of it, and the usual way to learn a model does not fit is CUDA out of memory, some time after the job started.

Describing the machine instead

Vx drops the single memory. A machine file declares the memories a part has, their sizes, how they nest, who can see them, and which links join them. This is the H100 description that ships with the compiler, without its citations:

Memory HBM {
  capacity: 80 GiB, bandwidth: 3.35 TB/s, managed: explicit, scope: device
}
Memory L2 {
  within: Memory::HBM, capacity: 50 MiB, bandwidth: 12 TB/s, managed: cached, scope: device
}
Memory SMEM {
  within: Memory::L2, capacity: 228 KiB, bandwidth: 128 B/cyc, clock: 1.98 GHz,
  granule: 1 KiB, managed: explicit, scope: sm, replicas: 132
}
Topology Device {
  arch: nvptx64,
  memory: Memory::HBM,
  visible: [Memory::HBM, Memory::L2, Memory::SMEM],
  transfer Memory::CPU_DRAM -> Memory::HBM : 63 GB/s,
  transfer Memory::HBM -> Memory::CPU_DRAM : 63 GB/s,
  transfer Memory::HBM -> Memory::L2,
  transfer Memory::L2 -> Memory::SMEM copy_engine
}

Each of the three properties is a field. capacity is the bound. transfer edges are the links between separate pools. visible, scope and replicas say who can address what, and how many copies of a space exist.

Programs are checked against that description. A 256×256 tile of f32 is 256 KiB:

fn main() -> i32 {
  let host : Tensor<f32, [256, 256]> = Tensor<f32, [256, 256]>::new();
  let tile = transfer(host, Memory::SMEM);
  return 0;
}

$ vxc --machine fleet/h100-sxm.vx --host default tile.vx
Error[E6009]: transferred tensor needs 262144 bytes but memory space 'SMEM' has capacity 233472 bytes

A weight tensor of 2³⁵ floats is 128 GiB, and HBM holds 80:

Error[E6009]: variable 'weights' needs 137438953472 bytes but memory space 'HBM' has capacity 85899345920 bytes

Both errors came from a laptop with no GPU in it. The same description also routes: the single transfer(host, Memory::SMEM) above, at a size that fits, becomes three hops, CPU_DRAM to HBM to L2 to SMEM, each costed from the declared bandwidths. A transfer between two memories with no declared path is a compile error. And because the spaces are finite, the compiler can ask a question the tape never raises: how much is live at the same time. For a Llama-2-7B prefill that is 15.94 GiB, against 58.93 GiB allocated.

Where Vx still uses a tape

The host. A host description declares no capacity on purpose: host memory is virtual, and a tensor larger than physical RAM pages rather than failing. A hard limit there would reject programs that run. So the one memory where the operating system maintains the illusion is the one where Vx accepts it.

Two more limits. A tensor whose shape is only known at run time cannot be checked against a capacity; the compiler says so with W1029 and leaves the placement unverified. And the description is only as good as its numbers. The files that ship in fleet/ cite a source for every figure and mark the ones not yet measured on hardware, so when a prediction is wrong it is clear whether to blame the model or the program.

Machine files covers every field and what the compiler derives from it; E6009 is the capacity error's own page. For NUMA domains described with the same vocabulary, see The NUMA that wasn't there.