Tiled Matmul

[mstn]

Summary

Preliminary Tiled Matmul implementation.

Implementation

Stateful primitives taking runtime "wire" gpu.state

• gpu.shared.alloc: allocates a persistent block-local shared-memory slot and returns its identity, updated proof state, and slot value.
• gpu.shared.row-major.cooperative-load: cooperatively loads a logical 2D view into a row-major shared slot, with each block thread loading one element.
• gpu.sync: synchronizes all threads in the block.
• gpu.shared.materialize: exposes a synchronized, ready shared slot as a borrowed buffer.

gpu.state is an erased, linear description of the block’s execution history.

Each stateful primitive consumes the current state and produces a new state whose event records what happened:

alloc  → allocated(slot)
load   → loaded(slot)
sync   → synchronized(previous-event)

Operations requiring a particular slot condition also consume a proof tied to that exact state:

• Cooperative load requires allocated-at(slot, state).
• Materialization requires ready-at(slot, state).

Because the state is linear, operations cannot independently reuse an obsolete execution history. Because proofs mention both the slot identity and state event, a proof for one slot or an earlier state cannot justify access to another slot or later occurrence.

This is intended to prevent:

• loading into an unallocated slot;
• reading shared storage before cooperative loading and synchronization complete;

Both states and proofs are compile-time objects and are erased before GPU code generation. Currently, admit-allocated-at, admit-ready-at, and keyed-state operations are temporary axioms. Therefore, the types express the intended safety conditions, but full safety is not yet guaranteed: it will require deriving these proofs from allocation, loading, and synchronization events rather than admitting them.

Next

• existing materialize launches a kernel, imo it is wrong, only gpu.materialize should launch kernels. Hence, we need to change the implementation of materalize and rewrite tests using gpu.materialize
• sync should be changed to accept a closure corresponding to a phase. The reason is that we don't want phase "state" to escape the sync.
• proofs are "admitted" as true but not actually proved. We want to actually prove them. There are other proofs we want to investigate: barrier safety, race free etc... ideally a kernel should return a proof of "correctness"

[statusfailed]

Some questions added on the PR. Main confusion is around "slots" - these look sort of like memory pages, but I can't figure out why, or how the f32 / max 1024 slots limits were picked.

Another concern is perfect tiling only- with materialize in naive matmul one can launch more threads than actually write back to the output buffer (threads with indices out of range simply drop the final write value).
Is there a way to extend this to non-perfectly-tiling matmuls?

[statusfailed]

This has changed as of #141 , we now have device-only buffers.

[statusfailed]

What does it mean that 'lifetime can be determined by the operation that consumes the buffer'?

[statusfailed]

Does this assume perfect tiling? What would need to change to support non-perfect tiles?

[statusfailed]

This feels like a materialize; is this what you are referring to as a 'sequentialmaterialize' in PR #142 ?

[statusfailed]

What is this?

I can't really figure out what the 'slot' abstraction is, why it's limited to 1024, f32 only, etc.

[mstn]

closing for #152