docs/spec-dataflow-part-1-streaming.md

← all documents
not measured0highlighted source passages0/0PBTs with runs0draft PRs
Not estimatedcombined confidence estimate0 considered · 0 missing
How combined confidence is computed

max(0, 1 − sum of PBT residual-risk estimates). Uses each distinct available PBT’s latest-run estimate and its own sampling scope; PBTs without estimates are reported and omitted. An observed violation remains the suite result; when other PBTs have estimates, their estimate is still shown. Assumes no independence. This is a combined point estimate, not a statistical confidence bound or deployment reliability. Uncovered passages are outside its scope.

No PBTs registered for this file.

Code coverageNot measured

Coverage added over the baseline, grouped by PBT. Only files with gains appear below.

No added coverage recorded.

Files without added coverage and unmeasured PBTs
Source fileBaseline coverageBaseline + inputContributing input
–

docs/spec-dataflow-part-1-streaming.md · pinned revision 48615bc5925ef4b9db8b4550b5d4322933cf4b7b

1

Loom Dataflow Part 1: Streaming And Channel Ops

3

This document specifies the precise token timing semantics of the stream-shaping ops in the dataflow dialect: dataflow.stream, dataflow.carry, dataflow.invariant, and dataflow.gate.

8

It also owns the thread-level ordered-channel type and endpoint semantics for dataflow.channel.create, dataflow.channel.send, and dataflow.channel.receive. Graph-local SSA streams and thread-level channels are related at dataflow.graph.launch, but they are not the same IR object.

13

Vector stream grouping and scalar/packed stream adaptation are specified separately in docs/spec-dataflow-vectorization.md. This document owns the scalar stream-shaping primitives that those vectorization ops build on.

18

This document owns the semantic contract for these operations. include/Dataflow/IR/DataflowOps.td and lib/Dataflow/IR/DataflowOps.cpp plus lib/Dataflow/IR/DataflowChannelOps.cpp are implementation projections and must conform to it. Compiler specs that use these operations, especially docs/spec-compiler-part-3-dfg.md, reference this contract rather than redefining it.

26breadth-20 · sampled attempt

1. Token Stream Model

A dataflow SSA value denotes an ordered token stream. A token may carry ordinary data, such as an integer, floating point value, vector, or none, or it may represent a control event. Multiple SSA uses of the same stream are token broadcast: each use observes the same ordered token sequence.

34

The four ops in this document shape streams. They do not define memory regions. A memref<...> value in the compiler frontend represents a memory-region binding. It must not be duplicated, delayed, or phase-normalized by dataflow.carry, dataflow.invariant, or dataflow.gate. Dynamic control chooses address, data, operation, and none ordering streams; it does not choose the frontend memref binding itself. Memory accesses use the memref as the static binding operand of dataflow.load / dataflow.store; ordering is carried by explicit none tokens.

44

2. Phase Streams

46

A phase : i1 stream is loop control, not a validity bit. For one normally closed activation:

49
K = number of true decisions and body executions
M = K + 1
phase = true^K, false
55

The final false token is an ordinary close transition. It resets the stateful actors driven by that phase stream, but it does not imply an IV, body value, feedback value, or body execution. Repeated activations are represented by concatenated phase segments; each false token closes one segment and returns the actors to their initial states.

61

3. dataflow.stream

63

dataflow.stream produces a valid IV stream and a loop-level phase stream from scalar integer recurrence operands:

66
%iv, %phase = dataflow.stream %init, %limit, %step
  step add while slt : iN
71

The operation starts in Idle. Idle consumes one %init, %limit, %step triple and establishes a current value initialized to %init.

74
  • If the while predicate holds for (current, limit), it emits current on %iv, emits true on %phase, advances the current value with the selected step kind, and remains active.
  • If the while predicate does not hold, it emits only false on %phase and returns to Idle.
80

The step kind is a dataflow::StreamStepKind value: add, sub, mul, sdiv, udiv, shl, ashr, or lshr. The continuation predicate is the upstream mlir::arith::CmpIPredicate enum. These generated enums are the shared implementation representation of the closed choices specified here. The parser, verifier, simulator, and hardware-configuration projection must consume that representation rather than maintain string-based copies.

87

The canonical operation requires %init, %limit, %step, and %iv to share a scalar signless integer type. %phase is always i1.

90

For init = 0, limit = 5, step = 1, step kind add, and predicate slt:

93
Result Tokens
%iv [0, 1, 2, 3, 4]
%phase [T, T, T, T, T, F]
98

For a zero-trip activation with init = limit = 5:

100
Result Tokens
%iv []
%phase [F]
105

Because %iv already has exactly K tokens, body address computation and memory effects consume it directly. Pairing %phase and %iv through a dataflow.gate is incorrect: the two streams have different cardinalities.

109

4. dataflow.carry

111

dataflow.carry is a two-state token element for loop-carried values or hidden loop-carried none state:

114
%output = dataflow.carry %phase, %init, %next : T
118

The operation starts in init state.

120
  • In init state, it waits for one %init token, forwards it to %output, and transitions to carry state.
  • In carry state, it first inspects the head %phase : i1 token.
  • If %phase is true, it requires and consumes one %next token, consumes the phase token, forwards %next to %output, and stays in carry state.
  • If %phase is false, it consumes only the phase token, emits no output, and returns to init state.
128

%init, %next, and %output have the same type. %phase is i1.

130

For %phase = [T, T, F], carry consumes two next values and produces three outputs:

133
Event %phase consumed %next consumed %output
init none none init
first transition true next0 next0
second transition true next1 next1
close false none none
140

For one closed activation, carry consumes one init, K next values, and M phase tokens, and emits M outputs: [init, next0, ..., next(K-1)].

143

5. dataflow.invariant

145

dataflow.invariant latches one initial value and replays it while a condition stream remains true:

148
%output = dataflow.invariant %cond, %init : T
152

The operation starts in init state.

154
  • In init state, it waits for one %init token, records the value, forwards it to %output, and transitions to running state.
  • In running state, it waits for one %cond : i1 token. It does not consume another %init token in this state.
  • If %cond is true, it re-emits the recorded value and stays in running state.
  • If %cond is false, it emits no output, clears the recorded value, and returns to init state.
163

%init and %output have the same type. %cond is i1.

165

For a loop-level condition stream [true, true, false], the output is three copies of the initial value: one immediate copy, one for the first true condition, and one for the second true condition. The false condition resets the op and emits nothing.

170

For a zero-trip loop-level condition stream [false], the output is one copy of the initial value. That copy belongs to loop phase, not body phase; a selector such as dataflow.demux can route it to the loop-exit path, leaving the body path empty.

175

dataflow.invariant is appropriate for scalar values, index-like values, vector values, and none control tokens. It is not appropriate for frontend memref<...> bindings.

179

Initialized Feedback Projection

181

The registered actor semantics own one closed projection of inputs that are not consumed by an actor's initialization transition but are consumed after the actor has published initialized state. These are initialized feedback inputs:

186
Actor Initialized feedback inputs Timing recurrence
dataflow.carry phase, next next, distance one
dataflow.invariant cond none
191

No other registered actor currently contributes an initialized feedback input. In particular, statefulness alone is insufficient: dataflow.gate requires both of its inputs for its first productive transition, and dataflow.stream consumes its complete activation tuple before producing a stream.

197

Dataflow exposes this projection from the same transition-case descriptors used by handshake, simulation, and RTL. Mapping progress and recurrence timing must consume it rather than recognize operation names or operand ordinals independently. An edge entering one of these inputs is a cycle breaker only when its consumer can reach its producer after all initialized feedback edges are removed. Removing those edges must leave a DAG; otherwise the current progress proof is not established.

205

The projection establishes logical initialization and recurrence distance. It does not establish physical storage. Mapping must separately prove a finite durable disposition for every initialized feedback edge that actually closes a cycle.

210

6. dataflow.gate

212

dataflow.gate converts a (cond, value) stream into a region-local phase:

215
%after_cond, %after_value = dataflow.gate %before_cond, %before_value : T
219

The operation starts in init state. It always consumes %before_cond and %before_value together when it fires.

222
  • In init state, (false, X) emits nothing and stays in init.
  • In init state, (true, X) emits X on %after_value, emits no %after_cond token, and transitions to continue.
  • In continue state, (true, X) emits true on %after_cond, emits X on %after_value, and stays in continue.
  • In continue state, (false, X) emits false on %after_cond, emits no %after_value token, and returns to init.
230

%before_value and %after_value have the same type. The condition operands and results are i1.

233

For a parent input with K true tokens and one trailing false close, %after_value has exactly K tokens. %after_cond is empty when K is zero; otherwise it has K tokens and is phase-shifted:

237
Input %before_cond %after_value %after_cond
[false] [] []
[true, false] [v0] [false]
[true, true, false] [v0, v1] [true, false]
243

The %after_cond result is not a validity bit for %after_value. Instead, it is the local close stream for the region whose values have already been gated:

247
  • %after_cond = true means this region execution is not the last one.
  • %after_cond = false means this region execution is the last one.
250

The parent false-lane input value is intentionally dropped by gate. If a lowering needs that value, as with the false scf.condition operands that become scf.while loop results, it must preserve the value with a separate projection such as dataflow.demux.

255

Canonical Transition Cases

257

The registered operation schema for each stateful actor exposes a closed set of schema-local transition cases:

260
Operation Transition cases
dataflow.stream StartTrue, StartClose, ContinueTrue, ContinueClose
dataflow.carry Init, Next, Close
dataflow.invariant Init, Replay, Close
dataflow.gate ClosedDrop, FirstTrue, ContinueTrue, Close
267

Each transition case is a typed descriptor owned by the operation schema. It determines the required logical state, consumed operand heads, produced results and their value sources, and next logical state. The descriptors are the sole bridge from the logical state machines above to Fabric UsePatterns, simulators, and RTL providers. Those consumers must not decode the condition operands again through operation-name switches or parallel state-machine tables.

275

Transition cases are schema vocabulary, not Dataflow operations, attributes, Artifact identities, Mapping records, or runtime event identities. A blocked transition is not another case: if the physical resource cannot atomically accept the case's active obligations, no logical operand is consumed and no logical state transition occurs.

281

7. Compiler Usage Rules

283

Lowering passes that use these ops must preserve the following rules:

285
  • Loop-level phase streams keep the final false close token.
  • dataflow.stream IVs already have body cardinality and are consumed directly; they are not paired with phase through dataflow.gate.
  • Parent-domain carry and invariant outputs are projected through dataflow.gate before body arithmetic or memory use.
  • Loop results and exit frontiers are projected from the false lane of dataflow.demux %phase, %parent_value.
  • Carry feedback contains exactly K real next values. The false close transition never consumes a dummy feedback token.
  • Body-local state whose values have already been gated may be driven by the body-local close stream from dataflow.gate.
  • False-lane values are not recovered from dataflow.gate; they must be routed separately if they are semantically needed.
  • Phase fanout is independent per use. One blocked consumer does not prevent another phase consumer from firing when its own operands are ready.
  • Frontend memref<...> values are bindings, not stream values shaped by these ops. Dynamic control shapes the address, data, operation, and none order streams instead.
304

8. Thread-Level Ordered Channels

306

The sole logical channel type is:

308
!dataflow.channel<T>
312

T is an ordinary typed message payload and may be scalar, vector, tile, descriptor, coordinate/value pair, or another finite value type. It must not contain a channel, !dataflow.thread_token, or a memory capability. A channel handle is connectivity identity, not a FIFO pointer or payload; it cannot be loaded, stored, nested in another channel, or sent as a message.

318

Each dynamic execution of dataflow.channel.create creates a fresh logical channel instance. Creation occurs outside loom.spatial_region and dataflow.graph; it cannot be CSE'd as a pure value. Dataflow has no channel-level open, close, reset, or EOS operation. Known logical domains or an explicit payload protocol own program termination.

324

Runtime may reuse one already admitted channel service through the bounded generation profile in docs/spec-runtime-abi.md. Its session is the transient execution of this exact logical channel lineage; its generation spans one complete logical channel invocation and preserves the endpoint membership, source_map, service, and route already selected for that lineage. A generation cannot split one endpoint-instance contribution, group messages by arrival order, add an endpoint, allocate a route, or create a Mapping identity. The optional terminal marker is an ABI lifecycle result after the declared flat event counts retire. It is not a message, a Dataflow value, or an EOS operation in the program.

335

The reusable profile is available only when the selected execution owner can derive finite producer and per-consumer flat event counts from the existing launch and endpoint correspondence. A missing or inconsistent derivation is a typed Runtime refusal; it does not authorize an inferred count or hidden payload sentinel. DynamicWorkDomain quiescence is owned by docs/spec-compiler-part-4-partitioned-data.md and may retire its launch token; it does not close a channel or manufacture an EOS message. A concurrently receiving consumer that cannot otherwise know when to stop remains unsupported unless its payload protocol expresses termination explicitly.

346

A bounded Runtime scheduler may relocate a queued DynamicWork item between transient worker deques, but queue emptiness, worker idleness, cancellation requests, and scheduling trace contents are not quiescence. Only the DynamicWorkDomain responsibility set owns completion.

351

dataflow.channel.send and dataflow.channel.receive are InstructionCore stored-program operations inside a dataflow.thread body and are forbidden in a canonical dataflow.graph. Send blocks as required to submit one message in program order. Receive blocks until it can consume and return the oldest message. Logical capacity, occupancy, physical latency, and physical buffering are unobservable; physical stalls may change performance but never content or order. The initial profile has no try-send, try-receive, size, empty/full, or select-any-ready operation.

360

The initial channel profile is restricted to DenseRectangular thread domains. A DynamicWork definition cannot own a channel endpoint or graph stream binding. Its WorkItemId and responsibility-set termination do not define FIFO message identity, source-map coordinates, a channel session, or an EOS event.

366

Stealing a queued DynamicWork item is not a send, receive, competitive channel arbitration, endpoint binding, EOS event, or source_map correspondence. It does not relax the DynamicWork channel restriction or create another route to domain completion.

371

A logical channel has at most one producer/output binding and may have several consumer/input bindings. Each consumer binding owns a total deterministic source_map from its logical consumer domain to the producer domain. Several consumers may select one producer, yielding multicast in which every branch observes the same ordered sequence. Many-to-one competitive receive requires an explicit merge, router, reduction actor, or memory-backed work queue; it is not implicit channel arbitration.

379

The persistent endpoint references are owned by the closed structural catalog in docs/spec-compiler-part-3-dfg.md. A graph stream binding uses its RootedGraphLaunchRef and stream ordinal. A direct send or receive uses the Dataflow finalizer's role-specific canonical site ordinal under the RootThreadLaunchRef. This document owns the channel and source_map semantics behind those references; it does not assign endpoint entities, reinterpret the ordinals, or add a channel identity to Mapping.

387

8.1 Dynamic Message Correspondence

389

This section describes dynamic events produced by repeated execution of statically related dense endpoints. "Dynamic" here refers to runtime message occurrences; it does not admit the DynamicWork thread-domain kind.

393

A channel pairs dynamic message events, not thread activations. For one dynamic channel instance, producer point p, consumer binding b, and consumer point q, the sole correspondence is:

397
p = source_map_b(q)

SendSeq(channel_instance, p)
RecvSeq(channel_instance, b, q)

RecvSeq[n] consumes SendSeq[n]
406

For one endpoint binding and logical point, the complete dynamic event sequence concatenates each thread-instance contribution in the deterministic dynamic issue order of the enclosing thread launches. Within one thread instance, the normalized binding-local order is the order already derived from structured control. An instance may contribute zero, one, or several events. There is no one-to-one producer-activation to consumer-activation pairing and no activation-owned message segment.

414

Conceptually, an event position is the total cardinality of all preceding endpoint-instance contributions plus the event's local ordinal. This position is derived semantics, not an IR value, Artifact record, payload sideband, Physical Tag, session, or generation. A static proof may represent the position symbolically. Runtime may maintain transient counters and ordered-commit state, but those values do not become program identity. A new Runtime generation restarts the transient counters for a new complete logical channel invocation; it never inserts a boundary into this invocation's event sequence.

424

Overlapping endpoint instances may execute physically out of order, but their messages must commit in the defined sequence. A physical implementation may serialize them or use independent contexts, queues, and deterministic reorder state. If the program provides no deterministic total order for occurrences sharing one endpoint sequence, it must use separate channels or an explicit merge or reorder actor; otherwise publication fails closed. Runtime arrival order never defines logical message order.

432

This rule permits rate conversion. For example, one producer instance may send four messages while four ordered consumer instances each receive one; the four receive events consume producer events zero through three. Introducing activation segments would incorrectly reject this program. Multicast applies the same rule independently to every consumer branch, so branch event n observes producer event n.

439

At a graph launch, channel input bindings derive graph-local stream inputs and channel output bindings consume graph-local stream outputs. Channel handles do not enter the graph body. A graph-local stream close is not a channel message, consumer EOS, channel close, or thread completion. Channel message delivery is an ordinary causal edge; conflicting shared-memory visibility must respect that causality without adding a channel-specific memory-order mode.

446

Mapping selects a physical path or network that preserves FIFO behavior. It may use NoC links, switches, buffers, virtual channels, fabric.fifo, or a memory-backed ordered queue when Fabric declares the capability. The logical channel does not prescribe one physical FIFO, route, capacity, or protocol. Mapping must preserve the dynamic event correspondence above when endpoint instances overlap. Physical Tags remain local resource-sharing interpretation keys and cannot encode launch or message identity.

454

Stable verification anchors cover payload-type rejection, fresh creation, send/receive placement and type agreement, one-producer/multi-consumer source mapping, repeated-launch event ordering, rate conversion, ordered blocking behavior, generation terminal counts, cancellation, reset, and rejection of stale generation tickets. EOS remains a lifecycle result rather than a hidden payload or graph-stream close, and logical code still cannot observe physical capacity. Tests do not enumerate physical transports, message types, activation-count matrices, or report formatting.

463

9. References

465
  • docs/spec-compiler-part-3-dfg.md -- SCF-to-DFG lowering templates that use these streaming semantics.
  • docs/spec-dataflow-part-2-control.md -- firing semantics for dataflow.mux, dataflow.demux, dataflow.sync, and dataflow.constant.
  • include/Dataflow/IR/DataflowOps.td -- operation declarations that implement this contract.
  • lib/Dataflow/IR/DataflowOps.cpp and lib/Dataflow/IR/DataflowChannelOps.cpp -- verifier implementations.
  • test/dataflow/unit/stream/, test/dataflow/unit/carry/, test/dataflow/unit/invariant/, test/dataflow/unit/gate/, and test/dataflow/unit/channel/ -- unit-level syntax and verifier tests.