Execution calculus and compositional refinement

This page specifies the proposed formal foundation, not a completed verified compiler. It connects the language’s execution nests, layout algebra, mutable TileIR, and optimization formulation. The bounded compiler families and their tests are implementations of parts of this model. General scope fusion, proof certificates, distributed execution, and the complete cost evaluator below remain extensions.

Scope of the claims

There are four different questions; none implies the others:

Distinct correctness and optimization claims

Claim	Precise scope
Representation closure	Typed maps/relations and region composition remain representable after composition
Soundness	An admitted transformation preserves observable behavior under the source contracts and numerical policy
Relative mapping completeness	Every mapping in a declared, bounded map/atom/protocol vocabulary is representable and enumerable
Search optimality	The returned plan minimizes the stated objective within that encoded candidate set

We do not claim a complete optimizer for arbitrary C++, every equivalent algorithm, every layout with efficient code generation, or actual hardware runtime. An exhaustive finite table establishes expressibility, not an efficient normal form, useful search space, or publication-worthy result.

The first tractable fragment specializes extents and strides at JIT time and uses finite integer domains, pure index expressions, typed SSA, explicit memory effects, and registered arithmetic/atom contracts. For symbolic reasoning, Presburger-definable sets and relations provide closure under composition, projection and restriction; constant division/modulo encode mixed-radix factors. The isl manual provides an established representation and operations for integer sets and relations, not a required compiler dependency. Products of two unrestricted runtime parameters are outside that core. Fixed-width bit-linear layouts use a separate GF(2)/bit-vector procedure; arbitrary data-dependent indices and opaque calls keep explicit, weaker contracts. A solver timeout means unknown, not false.

Program, events, and contracts

The region grammar is:

P ::= op | P ; P | if predicate then P else P
    | parallel(D, P) | serial(D, P) | pipeline(D, Pi, P)
    | reduce(R, g, A, P)

Sequence and conditionals are ordinary region structure, not additional execution primitives. A function body can contain several sibling scopes; it is an ordered region tree, not necessarily a single perfect loop nest. Within a spatial path, prefixes and ancestor projections form the nest described by the language. Temporal/reduction axes remain separately typed.

For specialization parameters p, define a semantic instance domain Omega_p as the tagged union of operation occurrences and their active spatial, temporal, and local element coordinates. Tags distinguish two identically shaped operations. An operation may be expanded into a reference scalar program for reasoning, without forcing the compiler to scalarize its IR.

Gamma records source assumptions, selected numerical semantics, and target capabilities. The reference program determines value/effect labels and required ordering, including reaching definitions, temporal carries and observable memory order. A load creates a value snapshot; later stores do not retroactively change it. Values assigned at the end of a temporal iteration are updated simultaneously, including swaps.

For ordinary memory effects, the parallel contract is noninterference between distinct active child instances. In a simple read/write model it implies:

for i != j: W(i) intersect (R(j) union W(j)) = empty

Read-only sharing is permitted. This is not global argument noalias: C[i] may be loaded and then overwritten through an aliased output in the same instance. Nor does it remove ordering between two operations inside that instance. Explicit atomic/collective extensions would carry their own effect contracts; arbitrary colliding stores are not implicitly reductions.

The compiler assumes this language contract for valid inputs. It checks a new distribution’s address coverage, communication and storage reuse; it does not run dependence analysis to ask whether the user really meant parallel. If a transformation changes operation boundaries, its newly crossed effects still need analysis. Contract provenance survives lowering: semantic facts, derived facts and unchecked invocation preconditions are different things.

Strength is a product order, not an enum order

Fix the same events, effect labels, arithmetic semantics and assumptions. Ordering constraints form a partial order by inclusion of their transitive closures:

H1 <=order H2  iff  closure(H1) subset closure(H2)
then: linear_extensions(H2) subset linear_extensions(H1)

An unordered independent domain admits more schedules than one with added order; a total order is a maximal restriction. Two partial pipeline orders may be incomparable. Adding order must still produce an acyclic, implementable schedule. This relation is not permission to erase observable edges from a sequential program.

Assumptions form a separate implication order. parallel has weak ordering but a strong noninterference precondition. Serial execution does not require that precondition. Thus a valid parallel can be serialized; a serial recurrence cannot be parallelized merely by changing its constructor.

Reduction is an additional algebraic dimension, not a position between parallel and serial. For contributions R and output groups G:

g : R -> G
fiber(o) = [r0, ..., rn-1] in source contribution order
fold_left(o)  = update_left(...update_left(seed[o], r0)..., rn-1)
fold_right(o) = update_right(r0, ...update_right(rn-1, seed[o])...)

The fiber uses active coordinates in lexicographic source-axis order, not memory or lane order. Left/right folds specify different update structures and operand orientations; right fold is not simply the unchanged left update run backwards. Empty fibers return the incoming seed. Masks omit contributions; physical replicas never create additional semantic occurrences.

The source default is unordered_tree. For a compatible reducer, it permits merge trees and contribution permutations, including order-dependent floating-point results. Ordered trees and strict folds are explicit restrictions. These choices define sets of admitted computations; they do not oblige the backend to use a tree. A serial realization can be in that set too. The typed local policy is implemented; the standalone Metal candidate flag now controls availability only. This does not make the general reducer-law calculus below an implemented decision procedure.

For an exact left-reference tree rewrite, a sufficient contract is:

update_left(s, r) = merge(s, lift(r))
merge is associative; identity is a two-sided identity
result[o] = merge(seed[o], ordered_merge(identity, map(lift, fiber(o))))

A right-reference rewrite instead has update_right(r, s) = merge(lift(r), s) and the seed on the right. These sufficient monoid laws are not prerequisites for a strict fold. Nor can an arbitrary State x Elem -> State update be treated as a State x State -> State merge. Default/tree policies without a compatible merge must be diagnosed, not silently assigned an invented algebra.

For y[m] = reduce_k f(m,k), R = M x K and g(m,k)=m: distinct m groups are independent; contributions along k combine. Several reduction axes or a non-coordinate grouping map use the same definition. A pure recurrence without a merge may use an explicit fold; general ordered effects use serial. A scan also exposes prefix results and cannot be replaced by a final-result reduction.

For exact equivalence, associativity permits changing parentheses while retaining contribution order. Arbitrary permutation additionally requires commutativity or an explicit permutation-invariant contract. A worker-striped fold can change order, so associativity alone is insufficient for an exact rewrite. Floating-point add is not an exact monoid: the default tree policy authorizes its changed grouping/order without claiming such a proof. FMA behavior, precision and exceptional-value handling remain separate requirements. parallel never supplies reduction permission. See the language contract for the policy boundary and edge cases.

Typed mapping witness

A plan uses the existing layout algebra in five different roles:

Typed components of a mapping witness

Map/record	Domain and meaning
Execution remap tau	active new logical occurrences to original occurrences
Binding beta	logical prefixes to target participant prefixes plus virtual/temporal context
Distribution delta_v	participant/local-slot occurrences to logical elements of SSA value v
Resource maps mu_s, addr_s	logical owner/version to resource instance, then local coordinate to address
Schedule/protocol Theta	realized events to issue order/time, completion and communication

These are compiler records, not five new public DSL entities. A target prefix means a controllable launch/cooperation coordinate, not an invented mapping to an undisclosed physical GPU core. Multiple logical programs may share a group; their virtual context and allocation-instance identities must remain distinct. Memory capabilities are an access relation, not another copy of the execution containment order.

For a bijective remap and each semantically observed old cut j, retain the existing prefix-factorization condition:

pi_j o tau = tau_j o pi'_rho(j)

An identity-defining cut needs a bijective tau_j on active prefixes. Crossing that boundary requires an explicit re-anchoring/re-homing refinement, not just equal flattened cardinalities. Binding retains compatible prefix projections, including virtual and temporal context. Resource-specific address composition then satisfies, for each logical access:

logical element = delta_v(participant, local_slot)
logical access  = access_s(logical_context, logical element)
physical access = (mu_s(owner, version), addr_s(logical access))

There is no unique map from hierarchy to memory: access_s, materialization and addr_s are independently chosen for every resource. A/B/accumulator may therefore share participants while having unrelated layouts and lifetimes. Copies/repartitioning implement mismatched producer and consumer distributions.

Plan phases before value placement

The execution schedule is phase-local, not one distinguished axis for the whole program. An explicit child parallel exposes an independent domain; a tile-level map, reduce or mma already exposes a domain from which the compiler can construct an internal phase. These are two ways to express work, not competing programming models or additional user-visible scope kinds.

source scopes / tile operations
             |
             v
E_p: phase instances -> (program, participant, local time)
             |
             v
L_v: reaching SSA definition -> element/owner/slot relation
             |
             v
C_(v,p): producer-to-consumer communication
             |
             +------ joint cost / resource feedback ------> E_p, L_v

For each use, the selected source in L_v and its communication must deliver the element requested by that phase’s access map. A value keeps its definition-time meaning across phases; a new schedule does not authorize reloading it after a write. Replication is a placement choice, not duplicated semantic contributions. Phase selection and value placement are jointly optimized: the arrows explain the semantic derivation, not a mandatory greedy solver order.

For example, QK can distribute output keys, a row reduction can distribute its key contributions, and PV can distribute output value channels, using the same team at different times. Neither dimension labels nor a global “last axis” rule determine these choices. The complete access projection matters: reading K[key_of_this_lane, channel] from a channel-distributed snapshot is not a uniform broadcast merely because channel % W is uniform.

Communication also constrains control flow. A lane without a valid output in a ragged phase can still own a value needed by another lane. Uniform broadcasts must therefore execute with the required participants converged; guard local reads/writes without predicating away the source participant. Padding never becomes a reduction contribution.

Execution determines participants and context. Each resource independently supplies its access and address maps; there is no single hierarchy-to-memory function shared by every buffer.

Observations, not syntax, determine preserved cuts

A lexical region boundary is not automatically a hardware boundary, allocation, barrier, or persistent semantic identity. If no value, resource, effect or collective contract observes a cut, a pass may remove or factor it while preserving its logical coordinates. An observed owner or participant identity must remain distinguishable, possibly through virtual context rather than a dedicated hardware level.

Explicit bindings constrain admissible plans; they do not require one physical level for every unbound lexical nest. The prefix law above is a sufficient check for identity-preserving remaps, not the only admissible transformation. Re-homing is a separate refinement with resource/effect obligations. Rejecting all remaps that fail that simple law would make the compiler unnecessarily rigid. Unknown legality should retain a conservative plan, not redefine the source.

Bridge compatibility is a relation check

For a value, represent its realized distribution as a relation:

L_v subset LogicalElement x (ParticipantContext, LocalSlot)
L_v = {(e, p, s) | delta_v(p, s) = e, and (p, s) is active}

One logical element may have multiple physical copies; inactive slots need not denote an element. An adapter to a logical-to-physical storage interface uses this relation, not a functional inverse that loses replicas. For each resource/version context it must preserve the same active pairs, offset, resource instance and participant meaning. The TIRx shard/replica/offset formulation is a relevant destination representation; see the versioned comparison.

This is an extension obligation for adapters, not a claim that every LayoutCorr already lowers to every bridge. A plan outside a destination’s supported normal forms requires an available explicit realization, another candidate, or a diagnostic. It must not silently discard replication or substitute a convenient flattened layout.

Established rectangular task product

For independent rectangular work, use the task construction formalized in Hidet, Section 5.1, rather than inventing a second spatial/temporal algebra. Let f: worker -> ordered task list have shape d1 and n1 workers; let h have shape d2 and n2 workers:

(f tensor h)(w) = [x*d2 + y | x in f(w div n2), y in h(w mod n2)]
shape(f tensor h) = d1*d2; workers(f tensor h) = n1*n2

Products on coordinates are componentwise. This product is associative, not commutative. spatial contributes worker factors; repeat contributes ordered local tasks. This is an internal construction, not additional DSL primitives. It builds a binding/schedule witness, whereas tau remaps semantic occurrences. Observed prefixes, cross-task effects and asynchronous protocols still need their separate contracts; a rectangular product alone does not prove them.

For replication or collectives, use LayoutCorr rather than a fictitious functional inverse. One semantic contribution may have several storage replicas, but a reduction consumes it exactly once. A collective atom refines a whole semantic subgraph, so it is not modeled as a bijection between scalar FLOPs and machine instructions. Its contract connects input/output values, participant convergence, effects, and numerical policy.

Constructive rules and proof obligations

Write Gamma |- P =>[w] P' for a transformation carrying witness w. The primitive rewrite basis is small; compound schedules compose it:

Refinement rules and their additional obligations

Rule	Construction	Additional obligation
Reindex	identity, product, composition, permutation, unit insertion/removal	active-domain bijection and observed-cut factorization
Split/fuse	i = q*b + r, 0 <= r < b, q*b+r < N	positive factor, exact active coverage, integer representability
Bind/serialize	assign independent instances to participant and local time factors	exact coverage, preserved identity, target containment
Repartition/materialize	compose distribution and resource maps, insert transfers	each use observes its reaching value; copies, publication and lifetimes
Retiming/versioning	move issue times and select version slots	all dependence distances, completions and reuse hazards preserved
Reduction factorization	partition each grouping fiber and merge partial states	contribution accounting, merge/order/numerical laws
Atom refinement	replace a matching semantic subgraph	target atom’s value, layout, convergence, effect and arithmetic contract
Scope fusion/fission	combine or split sibling region implementations	preserved cross-region dependences and valid synchronization

Some useful laws have short proof arguments in this restricted model:

1. Reindex soundness. A bijection gives exactly one new occurrence for each old one. Pulling labels, accesses and required edges back through it leaves the labeled event graph isomorphic. Prefix factorization preserves every referenced owner and value identity. Thus observations are unchanged.

2. Composition. Two such remaps compose by ordinary map composition; bijections and the commuting prefix equations compose. Contextual refinement rules compose only when their effect and numerical contracts are preserved. An arbitrary per-kernel allclose tolerance is not a transitive contextual equivalence and cannot replace that condition.

3. Reduction factoring. Partition a fiber into disjoint contribution subsets with no omissions. For a commutative monoid, folding partials equals folding the original set. For a noncommutative monoid, require contiguous, order-preserving pieces and an ordered merge. Floating-point realization requires its separate admitted numerical semantics.

4. Resource remapping. If every read is supplied with the same logical version, publication precedes use, and simultaneously live distinct values do not collide without a permitted alias, changing physical placement does not change observations. Capacity and target access checks establish that this placement can actually be emitted; they do not follow from parallel.

These are proof sketches, not mechanically checked theorems about the current C++ implementation or TVM/LLVM. The finite reference tests check task-product associativity, exact coverage, prefix preservation, fusion, reduction ordering and version lifetimes. They exercise examples and counterexamples, not arbitrary-domain soundness or the production emitters.

python3 scripts/test_tile_execution_calculus.py

Multiple scopes and fusion

Ancestor access is not forbidden by lexical nesting

An inner scope may access an outer resource. Declaration scope determines the logical resource instance and lifetime; it does not, by itself, prohibit inner reads or writes. A target mapping must make the required access implementable, possibly with communication or another materialization. An implementation’s missing capture/lowering support is not a new language restriction.

Do not equate execution participants with logical operation instances. Under the anchor/frontier model, an ancestor-anchored acc = mma(a, b, acc) may be one logical update executed collectively through a deeper frontier. It is not a set of competing whole-Tile writes, and it must not require a new partial-update API. A distinct case is independent logical instances contributing different regions to an ancestor Tile; their partial results need assembly at completion.

For a parallel partial update of an outer Tile, the semantic model is a join of patches, not a sequential loop recurrence. With entry value T0, instance i produces a write footprint R_i and values V_i:

T1[e] = V_i[e]  when e belongs to R_i
        T0[e]   when no instance writes e

Ordinary parallel supplies the cross-instance noninterference contract. For mutable Memory effects this includes reads versus writes to the same storage. Reading an immutable entry Tile snapshot T0, however, does not conflict with another instance contributing a patch to the new value T1; the compiler must preserve that distinction when choosing storage. It is not necessary to ask the user to prove the contract again. The compiler must represent each write’s footprint, preserve untouched elements and entry snapshots, and may provide optional overlap validation. Overlapping cross-instance Tile updates need an explicit supported combiner; conflicting mutable Memory effects need an appropriate explicit contract, such as atomics. There is no unspecified winning instance. Changes within one instance retain their ordinary local order.

Implementation boundary: capture currently rejects changed ancestor ValueSlots when exiting parallel or tile.map; the IR verifier also rejects parallel operands/results. This is broader than the model above. Outer TensorView .store() effects already work, whereas an outer explicit Memory’s state update can hit that guard. Tile extraction is currently read-only: a partial-update/parallel-join representation is still required. Deleting the guard alone would not implement assembly or repair the verifier/lowerers. The missing protocol must cover direct collective assignment as well as explicit partial updates; implementing only the latter would not fulfill the model’s ancestor-access semantics.

Preserve cross-phase observations

Sibling scopes have sequential composition semantics. Initially A ; B makes the observations of A precede B; analysis may remove only observationally redundant ordering. This is distinct from choosing an implementation of an already-independent parallel domain.

For producer instances A(i) and consumer instances B(j), derive the cross-region dependence relation Dep_AB. It includes RAW, WAR, WAW, state, opaque-effect and protocol constraints, not only tensor shapes. A simple sufficient rule for vertical pointwise fusion is:

parallel_D(A) ; parallel_D(B)  =>  parallel_D(A ; B)
when Dep_AB subset {(i,i) | i in D}, with compatible ownership and effects

There is no new proof that A’s own instances or B’s own instances are independent. The diagonal check concerns new interleavings between A and B. Different domains can first be matched through a typed map; equality of their extents is neither necessary nor sufficient.

Pointwise dependence                 Cross-instance dependence
A(0) -> B(0)                         A(0) -----> B(1)
A(1) -> B(1)                         A(1) -----> B(0)
each pair can become one worker      per-worker fusion loses a required edge

For example, tmp[i]=f(x[i]); out[i]=g(tmp[i]) admits pairwise fusion. out[i]=tmp[(i+1)%N] does not admit that mapping even though both original parallel scopes are individually independent. A shared group with a complete barrier might handle the second case; otherwise retain a launch boundary. Likewise, a scalar consumer of a global reduction must wait for every required contribution. It may fuse into a final reduction stage, not execute once per arbitrary producer worker.

Ordered time has a different sufficient rule:

serial_i(A(i)) ; serial_j(B(j)) => serial_i(A(i); B(i))
when domains align and every cross edge A(i)->B(j) satisfies i <= j

This rule assumes the same increasing total order and no additional crossed effects; more general cases use event-order preservation directly. Pipeline fusion replaces these inequalities with dependence-distance and version constraints. Horizontal fusion of independent siblings is a tagged disjoint union, not pointwise zipping. Fusion is optional: saved launches/traffic may lose to increased live state, barriers, reduced parallelism or a slower atom.

Single source kernel versus physical execution plan

A source kernel is one invocation with a region tree and explicit effects. It need not always become one physical kernel launch. A general compiled plan contains supported code artifacts plus their launch/copy/completion DAG and temporary lifetimes. Fusing nodes produces one device kernel only when the target supplies the necessary within-kernel synchronization.

An ordinary GPU threadgroup barrier is not a device-wide phase boundary. Unless a supported cooperative launch/protocol provides that boundary, global dependences require separate launches. Busy-waiting resident groups while other groups have not been scheduled is not a valid universal implementation. The current Tile Runtime is a single-artifact path; multi-artifact execution is an explicit future Runtime extension, not a feature inferred from the DSL.

The same formulation extends to multiple devices without new semantic nest primitives. Binding adds device/rank coordinates; resource capabilities say which buffers are local, remotely accessible, or require transfers. A crossing edge becomes a supported copy/collective protocol with participants, matching epochs, completion and visibility. Ordinary buffer pointers do not acquire remote accessibility. The cost policy supplies topology-specific service and latency; the solver also checks link contention and version capacity.

Fine-grained streaming partitions a dependence relation into ready subsets and overlaps their producer/consumer epochs. Global reductions select a merge topology consistent with the arithmetic policy. Neither distribution nor pipelining invents associativity, ignores deterministic reduction order, nor removes deadlock/progress requirements. Multi-node failures/retries and distributed allocation ownership require a separate Runtime contract; no current single-device proof establishes those properties.

Validation, implementation and research obligations

Always validate IR ownership/use lists, types, dominance, state flow and explicit target constraints. Pass-local checks validate the new map/protocol; failure means another implementation or a diagnostic. Optional debug checks can test invocation bounds, disjointness contracts, complete outputs and canaries without making such checks an optimization prerequisite. A future race/contract instrumentation mode must report its checked domain; sampling does not prove absence of races. The current verifier is structural, and the Runtime has bounded argument/range checks, not a universal race validator.

The current automatic Metal group admission, singleton-axis projection and pipeline capacity reservation exercise reindex/bind/resource rules. Numerical tests cover permuted program coordinates, leading/interleaved unit axes, same-instance input/output aliases, explicit worker bindings, disabled planning, arithmetic permission, and multi-phase attention states. They do not establish general sibling fusion or a joint planner for every intra-group reduction/distribution alternative. Limited collective emitters are not that general composition result.

To support a paper, the deliverables should be: a small reference interpreter; formal judgments and proofs for a stated fragment; a typed transformation witness checked independently of search; backend refinements; and held-out multi-operator experiments with mapping/communication/materialization ablations. Compare model regret, search gap, compile budget, GPU timing and dispatch separately. A theorem about map coverage is not a speedup theorem.

Closest prior work and the open contribution

The focused literature survey compares Hidet’s composed task mappings, Cypress’s task/resource model, Hexcute’s layout/atom synthesis, verified scheduling rewrites, concurrency algebras and constrained mapping optimization. Execution-oriented tensor programming is not an unexplored alternative to layout algebra. We should reuse established components and test the combined effect/resource/time model against these close precedents.

The research hypothesis is compositional, prefix-aware refinement of an execution-first SSA program, coupled to a resource/time optimization problem and reusable backend policies. Novelty, useful relative completeness, and cross-target performance still need to be demonstrated against these systems.