From 4c6fc1173e5be0e03277185b1470808bbc3f0d5d Mon Sep 17 00:00:00 2001 From: ilgeco Date: Tue, 28 Jul 2026 12:10:31 +0200 Subject: [PATCH] New invariant for many to many conumer producer lanes --- .../GRAPH_COMPUTE_BATCH_INVARIANT.md | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/.agents/invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md b/.agents/invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md index c969d1b..a2b0958 100644 --- a/.agents/invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md +++ b/.agents/invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md @@ -225,6 +225,26 @@ compile-time shaping needed for a scheduled consumer must be encoded inside the corresponding `spat.deferred_communication` body. Phase 2 must not recover missing graph semantics by inspecting consumers after the deferred operation. +### Consumer and producer lanes are many-to-many + +A graph consumer lane may read fragments from several producer lanes. Several +consumer lanes may also read the same producer lane. Therefore: + +- consumer and producer batches need not have the same lane count; +- consumer lane `i` must not be assumed to depend on producer lane `i`; +- scheduling dependencies must follow the statically analyzable physical-slot + projections expressed by the consumer body; +- an unproven projection must not silently drop producer dependencies or + reclassify a produced graph value as a host input. + +For example, one output-row lane of a `3x3` convolution normally reads up to +three input-row lanes. Output-channel tiling adds another projection dimension: +several output-channel-tile lanes may read the same set of input-row lanes. + +When exact projected dependencies cannot be proven, scheduling may conservatively +depend on the complete producer batch, but communication realization must still +preserve the consumer body's actual selection semantics. + ## Graph lane, scheduled lane, and physical core are different identities These concepts must never be conflated: