Flow control

Credit-based per-stream flow control is the mechanism that bounds in-flight data end-to-end and makes unbounded streams (live video in or out) safe: a sender can never run further ahead of its receiver than the granted window.

The laws

• L9: The credit unit is one CHUNK frame. A sender holds a per-stream window initialized to the negotiated initial_credit (default 32 chunks ≈ 8 MiB at the default max_chunk); each CHUNK sent decrements it; at zero the sender MUST wait (async or blocking, per language).
• L10: The receiving endpoint grants credit by sending a CREDIT frame after consuming chunks; grants are batched (recommended trigger: consumed ≥ window/2). Flush-before-block corollary: a party holding pending sub-batch grants MUST flush them before ANY blocking wait: an empty-input recv, a quiet poll tick, or a downstream credit acquire (forwarders grant upstream and acquire downstream; blocking on either while holding grants can starve the very producer that would unblock the chain). Batch thresholds are derived from the receiver’s own link negotiation, while the sender’s window may come from a different link, so a sender can therefore legally stall below the receiver’s batch threshold, and only the flush guarantees progress under any window/batch mismatch. Granted credit is a buffer guarantee: the receiver must hold queue capacity ≥ its outstanding grants, so data frames can never block the delivery of control frames. This is the deadlock-freedom invariant that lets bounded-queue implementations (Go, Python) participate safely; the Rust reference keeps unbounded internal channels and enforces the window by count instead, which gives the same wire-visible law.
• L11: Credit is end-to-end. Intermediaries (host runtime, relay switch) forward CREDIT frames along the request’s route exactly like Cancel; they never originate or absorb credit.
• L12: Receiving a CHUNK beyond the granted window is a fatal protocol error: the receiver fails the request with CREDIT_VIOLATION.
• L13: A request terminal (END/ERR/Cancel) releases all credit waiters with an error, promptly. A sender blocked on credit must never hang.
• L14: Credit applies in both directions: engine→cartridge input streams (the cartridge’s InputStream consumption grants), cartridge→engine output streams (the executor’s consumption grants), and peer↔peer argument / response streams. LOG, ERR, END, STREAM_START, and STREAM_END are never credited: progress and errors always flow, even when data windows are exhausted.
• L15: An endpoint that sends and receives on the same request MUST service inbound frames concurrently with sending; a sequential send-then-collect loop deadlocks the moment a handler produces output while its input is still flowing.

Wire elements

The proved model

What a credit window does is stated and proved in formal/CapDAG/Bifaci/Credit.lean (laws in Laws/Credit.lean), and every mirror runs the code generated from it, so no runtime computes a window on its own:

• the sender’s side, Gate: acquire (taken, wait, or closed with the reason), grant, close;
• the receiver’s side, Window: arrive (accepted, or a violation when nothing is left of what was granted), consume (the grant now due: once half the window has been consumed, at least 1), flush (whatever is pending), continued (a chunk that only continues an item, granted back at once);
• negotiate (the smaller proposal; zero is refused) and grantTarget (the stream a grant names, or the request’s only one when it names none).

Over a link of one sender and one receiver it is proved that credit is conserved (Conserved: what the sender may send, what is in flight, what the receiver holds unconsumed and what it has consumed but not yet granted always add up to the window), that a sender following the gate never overruns the receiver (never_overruns, L12), that the receiver never holds more than the window (buffer_bounded, L10), and that a sender blocked at zero is always waited for by a grant the receiver owes or a chunk still to be consumed (blocked_sender_is_waited_for).

Each runtime’s own objects are replayed against the model’s scripts (formal/conformance-bifaci.json), so what stands between the generated decisions and the wire (counters, containers, the order things are done in) is held to the model too.

Reference implementation map (Rust)

• capdag-rs/src/bifaci/credit.rs: CreditGate (the sender’s window: acquire/blocking_acquire/grant/close), CreditWindow (the receiver’s: arrive/consumed/flush/continued) and CreditRouter (delivers inbound CREDIT frames to registered gates; close_request releases a request’s waiters, L13). Each holds the model’s state and adds only the waiting and waking: mutex + notify in Rust, threading.Condition in Python, a broadcast channel in Go, a continuation queue in Swift.
• Cartridge output: OutputStream::write / emit_list_item / emit_cbor are async and acquire one credit per chunk; blocking_write / blocking_emit_list_item serve FFI threads; StreamSender (detached emitter) acquires blocking-ly. Gates register with the runtime’s router on start(); the run loop routes inbound CREDIT frames to them and closes them on handler completion or Cancel.
• Cartridge input: the demux tracks a per-stream window (initial_credit + grants); InputStream::recv emits batched grants as the handler consumes (window/2). An over-window chunk surfaces as a CREDIT_VIOLATION stream error (L12).
• Engine: send_one_stream registers a gate per input stream and acquires per chunk; collect_terminal_output / TerminalOutput grant for consumed response chunks and route inbound CREDIT frames to the send gates (CreditPlumbing). execute_fanin runs input-feed and response-collect concurrently (L15).
• Pipelined chains (forward_frames, both the reference executor and the MachineFabric engine): every hop acquires from the downstream cap’s window and grants the upstream cap as it consumes.

What is not flow-controlled

LOG/progress frames (L14). A stalled data window must never silence progress reporting. LOG volume is unbounded and observable via the drop counters.

The teardown race, and how unroutable frames are classified

Credit crosses the wire in the opposite direction to the chunks it credits, so a grant can always be in flight when the request’s terminal lands (two sockets, opposite directions), and no sender-side check can close the window. Receivers therefore discriminate every unroutable frame two ways, and the two outcomes are DIFFERENT KINDS of event, counted in different families (see the stats module: StragglerCounters vs DropCounters):

• Benign post-terminal straggler: the frame’s RID belongs to a RECENTLY TERMINATED request: it crossed END/ERR in flight. This is the ordinary, protocol-legal teardown race of credit-based flow control (a grant, a duplicate terminal, a straggling LOG, a callee that ENDed before draining its input). Nothing went wrong and no data was lost, and the frame is moot. It is NOT a drop: it is counted in the straggler counters, per frame type (so a trace says “late credit” vs “late chunk”), logged at debug level, and indicated as benign in every stats surface (stragglers beside drops in snapshots and traces, stragglers_total beside drops_total on heartbeats).
• no_route drop: the runtime has never known the RID. A genuine routing anomaly worth alarming on: counted in the drop counters (per reason × frame type) and logged as a warning.

The discriminator is the bounded recently-terminated ring every routing runtime already keeps (64 entries: the relay switch’s request table ring, the hosts’ terminal-released ring). The race window is milliseconds, so ring eviction cannot misclassify a real race; a pathologically late frame ages back into no_route, where something that stale belongs. GC-evicted routing entries are not in the ring: an evicted entry never saw its terminal, so its frames are real routing loss.

Sender-side gates exist too, and are exactly two: the relay switch hard-errors UnknownRequest back to direct API callers (the engine must observe that a request no longer exists and stop sending), and the engine’s upstream-credit sender treats exactly that error as moot, since credits for a finished request carry no meaning, and failing a body for one would turn the teardown race into a spurious execution failure. Every other send failure stays hard.

Overrun: the live-capture category

A live capture source cannot stall: the device keeps producing whether or not anyone granted credit. When the consumer’s window lags reality, frames must go somewhere, and the somewhere is defined: never “buffer forever” and never a silent loss.

Overrun is the third narrow accounting category, distinct from both drops and stragglers because it means a third thing:

The mechanics: the full backpressure chain is wire credit → op output → op input consumption → the feed’s bounded delivery channel → the provider’s feeder → the capture ring buffer → the capture edge. Every stage except the last blocks; the last cannot, so it applies the feed’s declared policy:

• drop-oldest (default): evict the oldest ring entry, count one overrun, and stamp the next delivered item with a gap marker ({dropped, duration_us}; see 12.4 §Live feeds). Real-time consumers prefer fresh data over complete data.
• fail: end the feed with a classified error (FEED_OVERRUN, class resource). Pipelines that need every frame opt in explicitly.

Accounting: overruns are counted per feed and runtime-wide (overruns_total rides heartbeat meta beside drops_total and stragglers_total), and each gap is visible in-band via item meta, so a downstream cap, the trace, and the operator all see exactly what was lost and when, indicated as what it is: the consumer being slower than reality, not a malfunction.

The stats ledger is a window

The per-stream credit_outstanding in protocol-stats snapshots is the stream’s REMAINING WINDOW as observed by that runtime: seeded with the request’s destination-negotiated initial_credit when the stream’s ledger entry is created, minus one per CHUNK in either direction (a stream’s chunks all flow one way; its grants flow the other), plus each grant’s count. Engine-originated outbound frames are recorded in the same ledger at the switch’s send path. Non-negative in healthy operation; a negative value means the producer overran its window. Diagnostic only: the endpoints hold the authoritative windows.