Skip to content

TileFoundry Spec — semantic-analysis (per-Op semantic derivation)

This spec owns TileFoundry's concrete static analysis services — the semantic contracts that derive types, access relations, and shard layouts over the IR. Each service is a registry-backed derived visitor: the common registration and dispatch mechanism is owned by visitor-registry; this file owns each service's requirements, handler shape, required context, and the semantic rules it enforces. The forward relation's own result carrier is owned by visitor-registry §4.1; this file links to it rather than redefining it.

1. Type propagation

Type inference is registered per Op through @register_typeinfer(<OpClass>) and enforces its constraints via ctx.error(...) (visitor-registry §4). A handler receives the op and a typeinfer context, derives the output IRType, and reports violations through ctx.error. A hir.Function call composes these per-op rules under elaboration (hir §1.1): the callee body is reconstructed and each of its nodes re-derives through the same per-op rules under the call's actual argument types, so a relation-derived rule never needs its own function-boundary case.

A function boundary MUST NOT complete or reject a legal Partial. A function return MAY carry a Partial(reduction) in a TensorType, and a tuple return MAY carry it in any nested tensor field. Call elaboration MUST preserve the ShardLayout mesh-axis position and reduction on the actual value; completion remains the responsibility of an explicit Reshard or allreduce.

1.1 Relation-derived type behavior

An op's typeinfer MAY derive the output type from a forward access relation (visitor-registry §4.1) rather than from a hand-written rule. The relation describes one shared iteration domain and, per boundary, an access map from that domain to the tensor's index space. The relation carries no tensor shape: the output shape is typeinfer-side data, derived from the op's shape rule or (where implemented) from the relation by composing the output access map over the domain.

Within the relation:

  • A domain dim that appears in an input access map but not in the output access map is a reduction dim (it is eliminated in the output).
  • A tensor axis whose access maps to a constant (rather than a domain dim) is a broadcast axis.
  • A symbolic size is an isl parameter of the domain; the relation's rank is fixed and is read from the input types.

The shard consequences of these structural facts (how Split / Broadcast / Partial propagate, and the reduction effect) are defined in §3.2.

1.2 Domain construction and output shape derivation

The relation describes one shared iteration domain; a symbolic size is an isl parameter of that domain, and the relation's rank is fixed and read from the input types. Output shape is not carried by the relation — it is typeinfer-side data, derived from the op's shape rule or, where implemented, by composing the output access map over the domain. Output access-map arity is validated by the relation service (visitor-registry §4.1).

2. Access relation analysis

The forward access relation is the boundary model shared by relation-derived type behavior and shard propagation: one iteration domain plus, per boundary, an affine access map from that domain to a tensor's index space. Its result carrier AccessRelationResult and the registry that produces it are both defined in visitor-registry §4.1. The polyhedral model that lifts a whole Function body out of these per-op relations is owned by analysis §1. The rule reads only the access maps' affine structure (which domain dim each axis uses), never the domain bounds, so it is size-agnostic and identical for static and dynamic shapes.

3. Shard propagation

3.1 Logical shape to layout domain

  • TensorType.shape is the logical shape.
  • layout has its own domain shape.
  • The current interpretation is canonical regroup: linearize first along the logical shape's row-major order, then reinterpret along the layout domain's row-major order.

3.2 Relation-driven shard propagation

When an op's output ShardLayout is derived from a forward access relation (§1.1), the output ShardAttrs are determined from the input shards and the relation's access maps by a single rule, shared across ops.

Mesh-axis value state. ShardLayout.attrs is indexed by mesh axis. A Partial(reduction) is a value state at that exact index, not an unordered collection of reductions and not a layout position. Every propagation decision MUST retain that index and its reduction independently of every other mesh axis.

Reduction effect. A reduction dim (a domain dim absent from the output access map) carries one of two effects, declared by the op/relation:

  • partial — the per-shard result is a partial that still needs a cross-shard reduction (e.g. a contraction dim split across the mesh);
  • complete — the reduction is already complete within each shard (e.g. an explicit reduce over a sharded axis).

Propagation. Per input mesh axis, by its attr:

  1. Split(k) — map layout axis k to the input's logical tensor axis, then to a domain dim via the input access map.
  2. If that domain dim appears in the output access map, the output carries Split on the output layout axis the domain dim maps to.
  3. If that domain dim is a reduction dim, the output mesh axis becomes Partial(reduction) when the effect is partial, or Broadcast when the effect is complete. The resulting Partial carries no layout axis — it is a value state on that mesh axis.
  4. Partial(reduction) input — propagates on the same mesh axis, gated by commutation: the op MUST propagate Partial(reduction) unchanged only when its own math is proven to commute with reduction — op(reduction(x0..xn)) == reduction(op(x0)..op(xn)). This service reads only the relation's affine structure and MUST NOT make that mathematical judgment itself; each op's typeinfer rule owns it. On each mesh axis, two Partial inputs MUST be compatible with that op's rule. States on different mesh axes MUST NOT be compared as an unordered set; the op evaluates each axis independently. Partial resolves to Broadcast only via an explicit reduction / allreduce over that axis. There is no layout-axis mapping for a Partial.
  5. A Broadcast (size-1) input axis contributes no Split.
  6. Two inputs binding the same domain dim to incompatible mesh axes is an error.

A Partial MUST NOT be silently eliminated, nor silently carried through a non-commuting ordinary op; only an explicit Reshard / allreduce from Partial to Broadcast completes it.

An ordinary multi-input op MUST inspect every tensor input for a Partial. When its result type cannot represent a secondary input's axis-preserving state, typeinfer MUST reject that input and name the Reshard remedy rather than silently dropping the state.

A fully-Broadcast input ShardLayout (every attr Broadcast) is replicated: it carries no real sharding, so it contributes no Split / Partial and does not pin a mesh — it MAY combine with an input sharded on a different mesh. When no input carries real sharding the output carries none.

An input Split that accesses a non-projection domain dim, or an output-surviving dim reachable only through a non-projection output access, MUST fail closed rather than guess a mapping. The rule reads only the access maps' affine structure (which domain dim each axis uses), never the domain bounds, so it is size-agnostic and identical for static and dynamic shapes.

Owner axis. Split(axis) indexes an output layout axis, not the logical tensor axis. A reduction-induced Partial attaches to no layout axis — it is a value state on the mesh axis that was reduced.

3.3 Output storage and mesh/layout compatibility

A symmetric multi-input op (Binary, MatMul, Concat, Stack, Mma) resolves its output storage by anchoring on the concrete residency among its operands (types §2). The rule does not appeal to any ordering of storage kinds and is independent of operand order:

  • An unmaterialized operand (storage=umat) does not constrain the output — it abstains.
  • One concrete operand storage (alongside any unmaterialized operands) is the anchor; the output takes that storage.
  • Several concrete operands that agree on a storage → the output takes that storage.
  • Several concrete operands that disagree on storage → typeinfer MUST ctx.error, unless the op defines its own destination/mixed-storage resolution. There is no operand-order tie-break.
  • All operands unmaterialized → the output is unmaterialized (umat).

This resolution uses no memory-level lattice; output residency is a function of the concrete anchor(s) alone. (The rmem < smem < gmem hierarchy is a Reshard-direction notion and is unrelated to output-storage anchoring.)

A tensor value's mesh / layout is carried by its TensorType.layout (ShardLayout.mesh names the mesh instance) — that type is the source of truth, and the IR places no scope-based restriction on values from different meshes coexisting. Each op's registered typeinfer owns the operand layout / mesh compatibility it requires and its result layout; there is no uniform cross-op rule imposed from outside typeinfer. Reshard is the explicit op that changes a value's layout / mesh.

Per-op typeinfer owns layout compatibility and result layout. For example, Gather owns whether an indexed access is a pure slice or a layout-preserving data-dependent gather.