NiccoloN
54 lines
2.5 KiB
Markdown
54 lines
2.5 KiB
Markdown
# Pipeline Scheduling Invariant
|
|
|
|
## Scope
|
|
|
|
This invariant applies to pipeline stage partitioning, physical-core
|
|
assignment, scheduled materialization, deferred transfers, and pipeline
|
|
synchronization.
|
|
|
|
## Invariant
|
|
|
|
A scheduled compute operation and all of its lanes belong to exactly one
|
|
pipeline stage. An operation may consume results produced in its own stage or
|
|
the immediately preceding stage only. Therefore every compute-graph edge from
|
|
stage `S` targets stage `S` or `S + 1`; backward edges and dependencies that
|
|
skip a stage are invalid.
|
|
|
|
Dynamic function inputs are stage-zero sources. Any operation that directly
|
|
consumes one must belong to stage 0. A later stage may consume that data only
|
|
through an explicit result forwarded by the preceding stage.
|
|
|
|
Each logical core belongs to exactly one stage capacity range before physical
|
|
placement. Those ranges cover every core but may have different sizes when the
|
|
initial partitioner predicts a lower maximum stage interval. Physical placement
|
|
may map a stage to arbitrary core IDs using the injected target topology.
|
|
Synchronization and deferred transfers consume the explicit stage identity;
|
|
they must not infer it from a physical core number after placement.
|
|
|
|
## Ownership
|
|
|
|
Logical PEFT remains pipeline-agnostic. Stage partitioning is the first phase
|
|
of pipeline scheduling and owns this invariant. It must construct a valid
|
|
operation-level partition before physical-core packing. Operations split for
|
|
physical capacity retain one shared stage identity. Repacking may move work
|
|
only within its assigned stage. Deferred-transfer planning and
|
|
synchronization consume the verified stage assignment; they must not repair
|
|
or reinterpret it.
|
|
|
|
## Verification
|
|
|
|
Before scheduled materialization, verify that:
|
|
|
|
- every compute instance has one valid physical core and stage;
|
|
- all lanes of one compute operation have the same stage;
|
|
- every direct dynamic-function-input consumer belongs to stage 0;
|
|
- every compute-graph edge stays within a stage or advances exactly one stage;
|
|
- every stage-local resident-weight set fits its assigned physical core; and
|
|
- stage capacities cover all logical cores exactly once; and
|
|
- physical placement is a permutation of all target cores.
|
|
|
|
Pipeline scheduling tests must include an uneven physical-core layout and a
|
|
graph with a long-lived dependency that would cross multiple naive stage
|
|
cuts. End-to-end validation must preserve functional results and exercise the
|
|
existing synchronization lowering without simulator changes.
|