Module choreography 

The control plane of a spatial pipeline: the tokens and credits that make a metapipeline run, and the buffer depth that follows from them.

A dataflow stage does not simply “have a buffer of depth 2”. A channel between a producer and a consumer is a credit loop: the producer spends a credit to send an item, the item crosses the fabric, the consumer reads it and returns the credit, and the credit crosses back. While that loop is in flight the producer may only keep sending if it holds further credits. So the depth a channel needs to sustain one item every II cycles is the loop’s bandwidth-delay product,

    credits = ceil((forward latency + backward latency) / II)

and nothing else: fewer stalls the producer, more is dead scratchpad. credit_depth is that solve, synthesize applies it per channel from the pipeline and its placement, and eval_credit_flow is the executable meaning — a cycle-exact token/credit simulation whose steady state runs at exactly 1/II when the depth is right and stalls the moment a single credit is taken away. That two-sided property is what separates a solve from a guess, and plasticine_choreography_lock holds both sides over a corpus.

The shipped depth is the deeper of this solve and Spatial’s published writer-to-reader N-buffer rule (Koeplinger et al., PLDI 2018: a value written in stage i and read in stage j must survive j - i + 1 stage-times), because a channel must satisfy both: enough credits to never stall, and enough buffers to keep every live value alive.

Control is not free and not invisible. Every channel carries two nets — data-valid forward, space-available backward — and they are budgeted on the mesh’s SCALAR network, separately from the vector network the data itself crosses, against the PCU’s own control ports. An over-subscribed control plane is reported, never silently ignored. MODELED: these are the model’s cycles, never a Plasticine simulation.

Structs

Channel

A credit-controlled channel between two stages.

Choreography

The synthesized control plane of a metapipeline.

ControlNet

One control net of a channel.

CreditRun

What a credit-flow run did.

Enums

ControlKind

Which way a control net runs.

Functions

credit_depth

Credits a channel needs to sustain one item every ii cycles: the loop’s bandwidth-delay product. A channel always holds at least one credit — without one nothing can be sent at all.

eval_credit_flow

Run the pipeline as a cycle-exact token/credit machine for iters iterations.

synthesize

Synthesize the control plane of mp given the mesh distance of each edge (hops[i] for mp.edges[i]). Forward latency is producing the item plus carrying it; backward latency is the credit’s return trip.