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.
Coverage added over the baseline, grouped by PBT. Only files with gains appear below.
No added coverage recorded.
| Source file | Baseline coverage | Baseline + input | Contributing input |
|---|
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.
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.
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.
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.
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.
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.
A phase : i1 stream is loop control, not a validity bit. For one
normally closed activation:
K = number of true decisions and body executions
M = K + 1
phase = true^K, false
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.
dataflow.streamdataflow.stream produces a valid IV stream and a loop-level phase stream
from scalar integer recurrence operands:
%iv, %phase = dataflow.stream %init, %limit, %step
step add while slt : iN
The operation starts in Idle. Idle consumes one %init, %limit, %step
triple and establishes a current value initialized to %init.
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.while predicate does not hold, it emits only false on %phase
and returns to Idle.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.
The canonical operation requires %init, %limit, %step, and %iv to
share a scalar signless integer type. %phase is always i1.
For init = 0, limit = 5, step = 1, step kind add, and predicate
slt:
| Result | Tokens |
|---|---|
%iv |
[0, 1, 2, 3, 4] |
%phase |
[T, T, T, T, T, F] |
For a zero-trip activation with init = limit = 5:
| Result | Tokens |
|---|---|
%iv |
[] |
%phase |
[F] |
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.
dataflow.carrydataflow.carry is a two-state token element for loop-carried values or
hidden loop-carried none state:
%output = dataflow.carry %phase, %init, %next : T
The operation starts in init state.
init state, it waits for one %init token, forwards it to
%output, and transitions to carry state.carry state, it first inspects the head %phase : i1 token.%phase is true, it requires and consumes one %next token, consumes
the phase token, forwards %next to %output, and stays in carry state.%phase is false, it consumes only the phase token, emits no output,
and returns to init state.%init, %next, and %output have the same type. %phase is i1.
For %phase = [T, T, F], carry consumes two next values and produces three
outputs:
| Event | %phase consumed |
%next consumed |
%output |
|---|---|---|---|
| init | none | none | init |
| first transition | true | next0 |
next0 |
| second transition | true | next1 |
next1 |
| close | false | none | none |
For one closed activation, carry consumes one init, K next values, and M
phase tokens, and emits M outputs: [init, next0, ..., next(K-1)].
dataflow.invariantdataflow.invariant latches one initial value and replays it while a
condition stream remains true:
%output = dataflow.invariant %cond, %init : T
The operation starts in init state.
init state, it waits for one %init token, records the value,
forwards it to %output, and transitions to running state.%cond : i1 token. It does not
consume another %init token in this state.%cond is true, it re-emits the recorded value and stays in
running state.%cond is false, it emits no output, clears the recorded value,
and returns to init state.%init and %output have the same type. %cond is i1.
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.
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.
dataflow.invariant is appropriate for scalar values, index-like
values, vector values, and none control tokens. It is not appropriate
for frontend memref<...> bindings.
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:
| Actor | Initialized feedback inputs | Timing recurrence |
|---|---|---|
dataflow.carry |
phase, next |
next, distance one |
dataflow.invariant |
cond |
none |
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.
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.
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.
dataflow.gatedataflow.gate converts a (cond, value) stream into a region-local
phase:
%after_cond, %after_value = dataflow.gate %before_cond, %before_value : T
The operation starts in init state. It always consumes
%before_cond and %before_value together when it fires.
init state, (false, X) emits nothing and stays in init.init state, (true, X) emits X on %after_value, emits no
%after_cond token, and transitions to continue.continue state, (true, X) emits true on %after_cond,
emits X on %after_value, and stays in continue.continue state, (false, X) emits false on %after_cond,
emits no %after_value token, and returns to init.%before_value and %after_value have the same type. The condition
operands and results are i1.
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:
Input %before_cond |
%after_value |
%after_cond |
|---|---|---|
[false] |
[] |
[] |
[true, false] |
[v0] |
[false] |
[true, true, false] |
[v0, v1] |
[true, false] |
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:
%after_cond = true means this region execution is not the last one.%after_cond = false means this region execution is the last one.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.
The registered operation schema for each stateful actor exposes a closed set of schema-local transition cases:
| 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 |
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.
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.
Lowering passes that use these ops must preserve the following rules:
dataflow.stream IVs already have body cardinality and are consumed
directly; they are not paired with phase through dataflow.gate.dataflow.gate before body arithmetic or memory use.dataflow.demux %phase, %parent_value.dataflow.gate.dataflow.gate; they must
be routed separately if they are semantically needed.memref<...> values are bindings, not stream values shaped
by these ops. Dynamic control shapes the address, data, operation,
and none order streams instead.The sole logical channel type is:
!dataflow.channel<T>
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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:
p = source_map_b(q)
SendSeq(channel_instance, p)
RecvSeq(channel_instance, b, q)
RecvSeq[n] consumes SendSeq[n]
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.
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.
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.
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.
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.
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.
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.
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.