Heterogeneous targets · P0-2: async transfer tokens (transfer_async / wait)

P0-2 — Async transfer tokens

The single common denominator across TPU, B200, and Rubin. transfer is a blocking move today, so DMA double-buffering / TMA / tcgen05.mma pipelines are inexpressible. On a TPU this is correct-but-slow; on Blackwell you cannot express the machine at all. This is the precondition for any credible performance claim.

Today

let va = transfer(a, Memory::VMEM);
compute(va);                          // no way to overlap the next DMA

Proposed

transfer_async returns a linear Token<T, Memory::X>; wait consumes it and yields the placed tensor.

fn stream(tiles : &Vec<Tensor<f32, [128, 128]>>) -> void on Topology::TensorCore {
  let mut inflight = transfer_async(tiles[0], Memory::VMEM);
  for i in 1..tiles.len() {
    let next = transfer_async(tiles[i], Memory::VMEM);   // issue before consuming
    let cur  = wait(inflight);                           // token consumed here
    matmul_acc(cur);
    inflight = next;
  }
  matmul_acc(wait(inflight));
}

Diagnostics (both reuse machinery that exists)

• Dropped token — pure linearity. Type::is_linear() already returns true for Tensor/Pinned/Ref, so Token joins that list and the borrow checker raises it:

  E60xx: transfer token for 'inflight' is dropped without `wait`; the DMA may not have completed
  

• Read before wait — the existing seam obligation, with Transfer::Relaxed selected by "token not yet waited" instead of by the _relaxed method name (reuses the P0-3 path):

  E6004: 'cur' is read before its transfer token is waited — a consumer may read stale data
    note: z3 counterexample: ((tag_cur #b11) (val_cur #x00))
  

Lowering

Where it lands

src/lexer.rs (2 keywords), src/parser/expr.rs, src/syntax/types.rs (Type::Token), src/hir/expr.rs (typecheck, linearity, seam selection), src/dialect/VxDialect.cpp + VxLowering.cpp (2 ops), src/codegen/.

Note: deliberately deferred from the recent P0 push as the pivotal mid-size item that deserves its own focused session; it shares the QF_LIA/QF_BV solver with P1-1.

From the Heterogeneous Target Gap Analysis (§9). Status tracked there and in the P0 decision log. Sibling to the landed P0 work (P0-1 fa056b4e, P0-3 33ce0b64, P0-4 5e10637a, P1-4a-core 34b31902).

Start with src/lexer.rs, src/parser/expr.rs, src/syntax/types.rs, and src/hir/expr.rs, then inspect the existing P0-3 seam path and shared QF_LIA/QF_BV solver. Trace the corresponding lowering entry points in src/dialect/VxDialect.cpp, VxLowering.cpp, and src/codegen/. Done means transfer_async and wait parse and typecheck, enforce token linearity and read-before-wait diagnostics, and lower correctly for TPU, B200, and CPU.