Per-SDFG symbol registry with explicit facts by ThrudPrimrose · Pull Request #2673 · spcl/dace

ThrudPrimrose · 2026-10-09T09:26:01Z

A symbol carried its dtype and sign assumptions in its identity, so the same name parsed twice could become two different symbols and assumptions such as positivity never reached the passes that needed them. Symbols are now just names: each SDFG keeps a symbol registry with dtypes and facts, and subset, propagation and transformation proofs take the facts that hold where they are asked, replacing the global symbolic_positive assumption.

A nested SDFG connector used to describe the window its edge memlet selects out of the container it is connected to, with the memlets inside written relative to that window. Make the connector the container itself: dace.sdfg.dealias integrates a nested SDFG into its parent by adopting the parent's descriptors, restating the memlets inside in the parent's coordinates, and expressing the narrowing to the part that is actually used as a view. Validation rejects a connector that is not equivalent to the container connected to it, and convert_legacy_nested_sdfgs restates nested SDFGs built under the earlier semantics.

Under the contract a connector spans its whole container, so the memlets on the outer edges no longer say which part is accessed and the narrowing sits in a view inside. Propagate out of a nested SDFG by renaming equivalent descriptors, look through the views that integration inserts, and collect the memlets that interstate edges and control flow regions read.

A connector is the container it is connected to, so the containers of a nested SDFG are renamed into the parent's namespace and the memlets inside need no composition. Views of a container stay in the tree as view nodes, which removes the need for the nested SDFG view (NView) nodes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

The frontend passed a squeezed descriptor of each argument into the nested SDFG it builds for a call, a map or a loop body. Pass the container itself and let integration express the slice as a view, so a sliced argument keeps one descriptor at every level. Re-propagate the memlets afterwards, since the outer edges then only state the container.

…iners A transformation that puts a container somewhere else -- a local copy, a per-iteration buffer, a compressed intermediate, a rank's block -- has to carry that into the nested SDFGs connected to it, since their connectors are that container. RefineNestedAccess is removed: the accesses it refined are now stated by the views inside.

A connector now names the container, and the memlet on its edge says which part is moved. Take that into account when pushing to a stream, when a write with conflict resolution goes through a view, and when a library node hands its implementation a nested SDFG.

gt4py's origin/domain wrapper is built under the earlier nested SDFG semantics and is inlined by gt4py itself. Convert it before that, so the regression tests run against an unmodified gt4py until gt4py builds the wrapper to the contract or stops building it altogether.

An edge inside a scope may name a buffer the scope gathers into, whose storage says nothing about the schedule the scope should have: a map writing a shared buffer out to global memory was left with GPU_ThreadBlock and GPU_Device to choose between. The schedule now follows what crosses the scope boundary. Also restore the stream case of out connector typing, which came from the SVE fixes and was reverted here by mistake. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…ving unnecessary modification of symbol_mapping in add_nested_sdfg

Connector descriptors are written in the nested SDFG's symbols, so comparing them with the outer containers as written rejected valid mappings such as {'N': 'M + 1'} and accepted invalid ones whose names merely coincide (e.g., swapped or shadowed symbols). NestedSDFG.validate now requires every symbol of a connector descriptor to be declared in the nested SDFG and present in the symbol mapping, and compares the outer container with the connector restated through the mapping (dealias.restate_in_parent_symbols, which replaces symbols simultaneously). Mapped symbols used by the nested SDFG must also be declared in it. _same_container uses the same helper, fixing its sequential substitution. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

newast.py: the non-affine index handling of #2621 patches the offset-and-squeeze logic that this branch removed, so the branch's version is kept. vector_inference.py: kept the Indices-to-Range conversion and adopted the name-based loop parameter lookup from main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Restating a connector descriptor in the parent's symbols deep-copied it and replaced its symbols twice through safe_replace. Data.is_equivalent now takes an optional symbol mapping and replaces the symbols of the properties it compares in one simultaneous xreplace, so every descriptor type maps exactly what it compares. symbolic.symbol_replacements converts a mapping once per nested SDFG node, skipping identity entries by name. NestedSDFG.validate also reuses the symbol sets of connector descriptors instead of recomputing them. On a synthetic SDFG of 300 non-integrated nested SDFGs (2400 connectors), the connector checks take 55 ms instead of 1.98 s. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…w widening test (#2641) Code generation now treats a parent symbol as defined in a nested SDFG only when it reaches it through `symbol_mapping`, which fixes the allocation placement that re-enabled the skipped inlining test (Fixes #2072). The symbol-widening test now passes the element of A to its nested SDFG through an explicit View, as the no-view rule of this branch requires.

…e checks `visit_For` filtered `self.defined` with `hasattr(v, 'dtype')` and `getattr(v, 'transient', True)`. Use `isinstance` on the descriptor types instead, and materialize the defined names once through `defined_dict()` rather than looking each name up again. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Treating a Stream memlet like a Scalar made a dynamic tasklet push to a stream get a value-typed connector instead of a pointer. It came with an unrelated SVE fix without a rationale or a test, and the stream, consume and SVE stream tests pass without it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The description listed three representations, while the property stores and serializes every value as a string; say what the strings may encode and that consumers parse them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`SDFG.states()` builds a list of `all_states()`; iterate the generator directly in the code this branch added. None of these loops adds or removes states. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`replace_dict` derived `symrepl` from the string mapping whenever it was falsy, so an explicit `{}` was overridden. Only derive it when it is None. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

`full_data` was always True; drop the subset union, the inner memlet offsetting and the window-shaped descriptors that only the False path used. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…eplacement The single-step shortcut of `safe_replace` only checked whether symbolic values mention other symbolic keys, but keys mapped to constants are replaced in the same step, so `{A: B, B: 5}` turned A into 5. Check against every replaced key. Add tests for swaps, chains, self-referential expressions and user functions for both `symbol_replacements` and `safe_replace`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The step's sign is asked under the facts at the loop: a provably negative step flips the range, and a sign that cannot be proven keeps main's assumption that it is positive, now with a warning.

… its facts External builders of schedule trees (gt4py) construct ScheduleTreeRoot without facts; with none, nothing is assumed, which is sound. Propagation simplifies images and volumes under the facts it already holds instead of none, and simplify keeps an expression unchanged when the facts would rewrite it into a renamed outer symbol, which has no name inside the nested SDFG.

A bare integer sympy.Symbol for an index is a second identity for the same name; sympy indexes an IndexedBase by any expression, so the index is the same DaCe symbol as everywhere else.

…r unused nested mappings MapToForLoop leaves a nested SDFG mapping the dynamic-range symbols of the removed map, which the nested SDFG never uses; NestedSDFG.validate only warns about such mappings, so the declaration check follows used_symbols.

# Conflicts: # dace/subsets.py # dace/transformation/dataflow/map_fusion_vertical.py # dace/transformation/passes/relax_integer_powers.py # dace/transformation/subgraph/subgraph_fusion.py # tests/subset_covers_precise_test.py

tbennun · 2026-10-11T02:46:50Z

+
+
+class RelationKind(enum.Enum):
+    LT = enum.auto()


I wonder if we want a "much smaller than" (<<) relation here too. This can help inform dimensions that could be tiled etc. Might be redundant with LT and ranking but worth asking. @ThrudPrimrose

Maybe for solving simplification equations not much but it would make sense for deciding axis of parallelism, a good example:

foreach i in KLEV # small foreach j in NPROMA # huge

With an << relation we can calculate more easily which of these maps to parallelize.

A parameter of Scale.SMALL is much smaller than every default one. A proof that needs this records the order as a runtime assumption of its SDFG; the program exports __dace_check_assumptions_<name>, which __dace_init calls and CompiledSDFG calls on every call, raising with the values that break it. LoopToMap leaves a loop over SMALL symbols sequential by default.

# Conflicts: # dace/transformation/interstate/loop_to_map.py # tests/transformations/interstate/loop_to_map_test.py

# Conflicts: # dace/sdfg/dealias.py # tests/transformations/interstate/loop_to_map_test.py

…() was removed

add_datadesc declares every free symbol of a shape, so a transient sized by a loop iterator declared the iterator as an SDFG symbol before the loop existed. A scope that binds such a name now removes it; an explicitly declared symbol stays and validation reports the collision.

The symbol-side optimizations leave this PR: memoized assignment-RHS names, the per-call interstate type environment in defined_symbols, the library-expansion defined-symbols memo, the nested-SDFG argument-symbol cache and the in-place symbol table in SDFGState.to_json. Kept: dominator trees built once per SDFG for allocation lifetimes, Range.replace handing SymPy only reachable substitutions, the frozen node_id index (now entered by region serialization), the block-name ledger, the explicit-stack region walk, the linear cfg-list merge, call-site debug info, subgraph-view ordering and history-free lowering.

Cached proofs replay the runtime assumptions they relied on and are keyed on whether scales may prove; inverted loops derive no iterator range; covers_precise compares exact starts and subsets of other rank do not cover; shape-declared symbols live in the repository and keep the dtype of their symbol object; replacing by an expression declares no data or scope names and retypes nothing; divisibility facts are solved after order facts; name probes walk the graph once per search; solved facts are cached.

A divisibility quotient is written back by simplify; NE of equal expressions is FALSE; parameter facts do not hold for a symbol an interstate edge assigns; the assumption check runs with the library loaded; type inference reads the declared type of a symbol; LoopToMap refuses a step of unknown sign; scopes of removed owners are ignored and failed changes leave none behind; an iterator read after a loop that may not run is the copy; a shape takes the dtype of a whole-dimension symbol and refuses an undeclared typed one inside an expression.

… evaluate to a number The interval pattern refuses an expression it cannot prove monotone, such as the Modulo of CShift; the constant-range pattern then compared unevaluated function values. It now refuses too, and the whole array is propagated.

…test asserts the refusal Refusing typed symbols inside shape expressions broke every expansion that sizes a nested array by an expression of its parent's symbols.

…ng into them

- StateFusion (and the happens-before variant) compared a copy's read against the OTHER container's subset when the edge had none for this side; with facts that proved them disjoint the read fused into the wrong node (TSVC s118 miscompile). The endpoint's own subset is used, a missing one being the copy's shape at index 0, and an empty (ordering) memlet is no access. - Facts.assumptions carries a proven nonzero, not only a sign. - The prover bounds SymPy's floor and ceiling for any sign of their argument, and decides a Min/Max case split whose cases hold a division by generalizing each division to a fresh symbol. - _as_integers kept two proof slacks of one name apart: merged, int_floor(s1 - s2, 8) folded as exact and satisfiable facts raised InconsistentAssumptionsError. - ceiling_div rounds a non-integral numerator over a unit step ([0:N/2] holds ceiling(N/2) elements). - LoopLifting drops the declaration of the counter it turns into a loop iterator. - LoopToMap orients a loop whose step is proven >= 0 (or <= 0): a zero step never terminates. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

# Conflicts: # dace/codegen/targets/cpp.py # dace/codegen/targets/cuda.py # dace/codegen/targets/framecode.py # dace/data/core.py # dace/dtypes.py # dace/frontend/python/newast.py # dace/frontend/python/preprocessing.py # dace/frontend/python/replacements/filtering.py # dace/frontend/python/replacements/operators.py # dace/frontend/python/replacements/utils.py # dace/libraries/standard/helper.py # dace/libraries/standard/nodes/reduce.py # dace/sdfg/analysis/schedule_tree/sdfg_to_tree.py # dace/sdfg/infer_types.py # dace/sdfg/propagation.py # dace/sdfg/sdfg.py # dace/sdfg/state.py # dace/sdfg/utils.py # dace/subsets.py # dace/symbolic.py # dace/transformation/dataflow/gpu_grid_stride_tiling.py # dace/transformation/dataflow/map_fission.py # dace/transformation/dataflow/map_fusion_helper.py # dace/transformation/dataflow/map_fusion_vertical.py # dace/transformation/dataflow/strip_mining.py # dace/transformation/helpers.py # dace/transformation/interstate/loop_overwrite_elimination.py # dace/transformation/interstate/loop_to_map.py # dace/transformation/interstate/move_loop_into_map.py # dace/transformation/interstate/multistate_inline.py # dace/transformation/interstate/state_fusion.py # dace/transformation/interstate/state_fusion_with_happens_before.py # dace/transformation/passes/analysis/loop_analysis.py # dace/transformation/passes/loop_local_memory_reduction.py # dace/transformation/passes/loop_to_reduce.py # dace/transformation/passes/pattern_matching.py # dace/transformation/passes/relax_integer_powers.py # dace/transformation/passes/scalar_to_symbol.py # dace/transformation/passes/symbol_propagation.py # dace/transformation/subgraph/stencil_tiling.py # dace/transformation/subgraph/subgraph_fusion.py # tests/codegen/gpu_error_drain_test.py # tests/codegen/gpu_nested_grid_barrier_test.py # tests/codegen/view_allocation_test.py # tests/library/copy_node_test.py # tests/library/reduce_cub_workspace_test.py # tests/memlet_propagation_test.py # tests/passes/lift_trivial_if_test.py # tests/python_frontend/unroll_test.py # tests/scoped_symbol_serialization_test.py # tests/symbolic_serialization_test.py

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…clared global A symbol is its name, so SymPy's cache can hand an annotation such as 2 * N back holding an N built elsewhere, without the predicates this program declared. The argument types' free symbols overwrote the global, and the SDFG lost the declaration (a callee's 0 < N unprovable at its call site; order-dependent). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- ipow of integer operands is integer arithmetic: a shape extent, and a ceiling/floor that needs no rounding (TSVC offload "ipow(LEN_2D, 2) is not integral", stockham_fft's ceil() loop bounds). - Printing reads what it may not see in an expression from its surroundings, and its memos key on it: a symbol's dtype comes from the SDFG being generated (the scope's declared types), and symstr / sym2cpp key on those types and on the printing facts. A modulo printed as C's % where the facts proved it was served from the memo where they did not. - Canonicalization holds back a DOALL sibling of a sibling-loop chain with a refused sibling until WavefrontSkew (lu/ludcmp keep their (i, j) wavefront now that LoopToMap proves the j >= i loop). - Frontend: an annotation's free symbol never replaces the program's declared global (backported to #2673); a promoted symbol already declared is not re-declared from the visitor scope; an extent respelled as its source is undeclared once. - Tests stop asserting the pre-registry contract (dtype as symbol identity, simplify's own cache, sympy assumptions, declared iterators) and read signs from printing facts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

# Conflicts: # dace/transformation/dataflow/map_fission.py # dace/transformation/interstate/multistate_inline.py # dace/transformation/passes/relax_integer_powers.py

… integer The frontend sizes arange(R**i) as ceiling(R**i): with i of unknown sign the power may be a fraction. Once i >= 0 relaxes it to ipow, the ceiling is the identity; left in place it printed as libm ceil, a double loop bound OpenMP rejects (npbench stockham_fft, after main's #2689 met name-only symbols). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Brings the rounding drop around a relaxed ipow; extended keeps its facts-based exponent_relaxes_to_ipow and astutils.unparse. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

A chunk count ceil(N / max(ceil(N / M), 2)) loses its Max when the outer division is generalized; prove() must still answer instead of indexing a Max that is gone.

tbennun and others added 30 commits September 17, 2026 22:04

Merge branch 'main' into nested-sdfg

3a23b4d

Review fixes

cd7a57c

Revert changes to test

6ef1879

More tests to ensure correctness endures

a5fd526

Move symbol mapping integration into integrate_nested_sdfg, thus remo…

b3fc726

…ving unnecessary modification of symbol_mapping in add_nested_sdfg

Update/revert IR docs

bd926f7

Merge branch 'main' into nested-sdfg

37ede25

Fix tests, improve dealias for expressions such as "N": "N + 1"

3173eb8

Fix inlining requiring integrate_nested_sdfg within

a3f0a42

Merge branch 'main' into nested-sdfg

b98d3b1

Clarify that code node locations are stored as strings

1acb8ab

The description listed three representations, while the property stores and serializes every value as a string; say what the strings may encode and that consumers parse them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Iterate states with all_states() instead of states()

76fc865

`SDFG.states()` builds a list of `all_states()`; iterate the generator directly in the code this branch added. None of these loops adds or removes states. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Respect an explicitly passed empty symbolic replacement dictionary

12de776

`replace_dict` derived `symrepl` from the string mapping whenever it was falsy, so an explicit `{}` was overridden. Only derive it when it is None. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove the unused partial-data paths of nest_state_subgraph

d998df6

`full_data` was always True; drop the subset union, the inner memlet offsetting and the window-shaped descriptors that only the False path used. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Update copyright years of modified files to 2026

54eb285

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ThrudPrimrose added 5 commits October 9, 2026 12:57

LoopToMap warns when it assumes a symbolic step is positive

316417f

The step's sign is asked under the facts at the loop: a provably negative step flips the range, and a sign that cannot be proven keeps main's assumption that it is positive, now with a warning.

Autodiff indexes its symbolic tasklets by DaCe symbols

f973599

A bare integer sympy.Symbol for an index is a second identity for the same name; sympy indexes an IndexedBase by any expression, so the index is the same DaCe symbol as everywhere else.

Merge remote-tracking branch 'origin/main' into HEAD

025f2b6

# Conflicts: # dace/subsets.py # dace/transformation/dataflow/map_fusion_vertical.py # dace/transformation/passes/relax_integer_powers.py # dace/transformation/subgraph/subgraph_fusion.py # tests/subset_covers_precise_test.py

tbennun reviewed Oct 11, 2026

View reviewed changes

ThrudPrimrose added 6 commits October 12, 2026 16:21

Merge remote-tracking branch 'origin/main' into symbol-registry

e34b7c2

# Conflicts: # dace/transformation/interstate/loop_to_map.py # tests/transformations/interstate/loop_to_map_test.py

Merge remote-tracking branch 'origin/main' into symbol-registry

189e9c3

# Conflicts: # dace/sdfg/dealias.py # tests/transformations/interstate/loop_to_map_test.py

Merge branch 'symbol-scales' into symbol-registry

7856b68

Call states() in the symbol repository, as main does since all_states…

a8d6a97

…() was removed

ThrudPrimrose mentioned this pull request Oct 13, 2026

Faster code generation, serialization and library expansion of large SDFGs #2679

Open

ThrudPrimrose and others added 8 commits October 13, 2026 21:27

Merge remote-tracking branch 'origin/main' into symbol-registry

b7a9886

Declare a shape symbol with the dtype of its object again; LoopToMap …

731fb6c

…test asserts the refusal Refusing typed symbols inside shape expressions broke every expansion that sizes a nested array by an expression of its parent's symbols.

Check constant-range bounds that are plain numbers without substituti…

c2a4052

…ng into them

State that a symbol name has one dtype in a process

719862c

ThrudPrimrose added a commit that referenced this pull request Oct 15, 2026

Merge the registry backports (#2673) into extended

b2c6ce6

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ThrudPrimrose and others added 2 commits October 16, 2026 09:57

Merge remote-tracking branch 'origin/main' into symreg-backports

7f3e5d2

# Conflicts: # dace/transformation/dataflow/map_fission.py # dace/transformation/interstate/multistate_inline.py # dace/transformation/passes/relax_integer_powers.py

Test a relation whose only extremum sits inside a division

149cae1

A chunk count ceil(N / max(ceil(N / M), 2)) loses its Max when the outer division is generalized; prove() must still answer instead of indexing a Max that is gone.

Navigation Menu

Repository navigation

Per-SDFG symbol registry with explicit facts - #2673

Per-SDFG symbol registry with explicit facts#2673
ThrudPrimrose wants to merge 120 commits into
mainfrom
symbol-registry

ThrudPrimrose commented Oct 9, 2026

Uh oh!

tbennun Oct 11, 2026

Uh oh!

ThrudPrimrose Oct 11, 2026

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

ThrudPrimrose commented Oct 9, 2026

Uh oh!

tbennun Oct 11, 2026

Choose a reason for hiding this comment

Uh oh!

ThrudPrimrose Oct 11, 2026

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants