Problem class: go-polyhedral-loop-tiling-dependence-validity-exactness
Problem class: go-polyhedral-loop-tiling-dependence-validity-exactness
Environment: Go 1.26 · Implementation: /workspace/polyhedral
Given
for i_k = Lo_k .. Hi_k,A[ f(i) ] together with a read/write flag,s_k ≥ 1 plus a permutation π of the
2D coordinates (tile_k, rem_k), where
tile_k = ⌊i_k / s_k⌋, rem_k = i_k mod s_k,decide exactly whether the tiled/permuted execution order is a legal reordering of the original sequential program. Emit a machine-checkable certificate:
(i, j) with i <_lex j,
f_a(i) = f_b(j) for a conflicting access pair, and
Key(i) >_lex Key(j) (the tiled order reorders them).All analysis must be integer-exact (not floating point, not merely the
rational relaxation), and must agree with exhaustive brute force on small nests,
including degenerate i = j (loop-independent) and self-output dependences.
A naive implementation fails for seven distinct reasons. These are the actual failure modes addressed by the fix.
Taking direction vectors from earlier to later iteration always yields a
lexicographically positive δ (first non-zero component > 0). But the
tile-major order (t_0,…,t_{D-1}, r_0,…,r_{D-1}) is not a linear
extension of lexicographic order. Counterexample (depth 2, s = (2,2),
index = 5·i + j):
p = (0,5), q = (1,0), p <_lex q, δ = q - p = (1,-5) (lex-positive)
Key(p) = (t0,t1,r0,r1) = (0,2,0,1)
Key(q) = (0,0,1,0)
Key(p) > Key(q) → ILLEGAL
So legality must compare the actual keys of the two iterations, not just
signs of dependence directions. (The interleaved order (t_0,r_0,t_1,r_1,…)
is always legal — it is the reason RC-1 bites only for tile-major schedules —
and the test suite checks both facts.)
Banerjee bounds / Fourier-Motzkin decide feasibility over ℚ. They are
necessary but not sufficient over ℤ (e.g. 2x = 1 is rationally
feasible, integrally infeasible). Using them alone yields both false
"illegal" and false "legal" verdicts. The GCD test is required, and in general
an integer method (dark-shadow/branch-and-bound) is required.
⌊·⌋ and mod are not affineKey(i) contains ⌊i_k/s_k⌋ and i_k mod s_k. Substituting these directly
into a linear solver is invalid. The fix introduces tile and remainder
variables i_k = s_k·t_k + r_k, 0 ≤ r_k < s_k, which makes both Key and
the subscript equalities linear.
A conflicting pair with i = j (e.g. A[i] = A[i] + 1) is loop-independent:
it imposes no reordering constraint, because statements inside one
iteration are never reordered. Treating it as a constraint falsely rejects
legal schedules. Conversely, a self-output dependence with i ≠ j (two
writes to the same location) must be enforced, or illegal schedules are
accepted. Both are covered explicitly by tests.
Two reads of the same location do not constrain the schedule. Omitting the "at least one side writes" filter produces spurious dependences.
δ must be later − earlier where "earlier" is the lexicographically smaller
iteration, not the raw index order in an access list. Wrong orientation flips
signs and inverts the verdict.
Legality is about all conflicting pairs in the (bounded but potentially large)
iteration space, not just neighbours. A polyhedral encoding avoids enumerating
|space|² pairs.
type Affine struct { Coef []int64; Const int64 } // Const + Σ Coef[k]·i_k
type Access struct { Stmt, Array string; Write bool; Index []Affine }
type Nest struct { D int; Lo, Hi []int64; Accesses []Access }
type Schedule struct { Sizes []int64; Perm []int } // Perm[0] = most significant
func (s *Schedule) Key(i []int64) []int64 {
d := len(s.Sizes)
coord := make([]int64, 2*d)
for k := 0; k < d; k++ {
sz := s.Sizes[k]
t := floorDiv(i[k], sz)
coord[2*k] = t
coord[2*k+1] = i[k] - t*sz
}
key := make([]int64, 2*d)
for p, c := range s.Perm { key[p] = coord[c] }
return key
}
Certificate semantics. A witness is valid iff it passes
func (n *Nest) VerifyCertificate(s *Schedule, dep *Dependence) bool {
i, j := dep.SrcIter, dep.DstIter
// in bounds, i <_lex j, same array location, ≥1 write, Key(i) >_lex Key(j)
}
Lists every iteration and every conflicting pair, then compares keys. It is the reference the polyhedral engine is tested against.
for a := range n.Accesses {
for b := range n.Accesses {
if accesses[a].Array != accesses[b].Array { continue }
if !accesses[a].Write && !accesses[b].Write { continue } // RC-5
for i before j (i <_lex j): // RC-6
if sameLoc(a,b,i,j) {
if Key(i) > Key(j) { return illegal witness(i,j) } // RC-1
}
}
}
Loop-independent pairs i = j are skipped by i <_lex j, which is exactly the
correct semantics (RC-4).
Introduce 4D integer variables per conflicting pair: tI_k, rI_k, tJ_k, rJ_k
with i_k = s_k·tI_k + rI_k, j_k = s_k·tJ_k + rJ_k. Then:
f_a(i) = f_b(j) becomes a linear equality;i <_lex j is a disjunction over the first differing coordinate im
(i_l = j_l for l < im, i_im − j_im ≤ −1);Key(i) >_lex Key(j) is a disjunction over the first differing schedule
position km (coord = coord for earlier positions, coord_i − coord_j ≥ 1).func (n *Nest) violationSystem(s *Schedule, a, b, im, km int) *system {
sys := n.baseSystem(s) // bounds + 0≤r<s for i and j
n.subscriptConstraints(s, a, b, sys) // f_a(i) = f_b(j)
for l := 0; l < im; l++ { sys.addEq(iterDiff(l), 0) }
sys.add(iterDiff(im), -1, le) // i <_lex j
for p := 0; p < km; p++ { sys.addEq(coordDiff(s.Perm[p]), 0) }
sys.add(negate(coordDiff(s.Perm[km])), -1, le) // Key(i) >_lex Key(j)
return sys
}
For each access pair, each im, each km:
gcd(coeffs) | rhs for every equality.math/big.Rat — refutes rational-infeasible
systems exactly. Elimination order is chosen by smallest pos·neg product;
a constraint cap returns "not refuted" (never "infeasible"), so capping only
affects speed, never soundness.solveInteger). Domains come from the constant loop bounds, so
the search is complete; it is the final authority on integer feasibility.(i, j) and checked with
VerifyCertificate.func (n *Nest) Analyze(s *Schedule) (Result, error) {
for each conflicting (a,b) {
for im { for km {
sys := violationSystem(...)
if !gcdAdmissible(sys) || !banerjeeAdmissible(sys) { continue }
if !fmFeasible(sys.v, sys.constraints) { continue }
if ok, model := solveInteger(sys); ok {
i, j := decode(model, s)
return illegal(witness i,j)
}
}}
}
return legal(s) // s itself is the tile-legal witness
}
Direction/distance enumeration uses the same machinery over the 3^D sign
patterns (FeasibleDirections), and is cross-checked against the brute-force
CollectDependences.
When the proposed schedule is illegal, FindLegalSchedule enumerates
permutations for the given tile sizes and returns the first one the exact
analyzer accepts — this is the "tile-legal witness schedule" branch.
cd /workspace/polyhedral
go vet ./...
go test ./... # unit + randomized cross-checks
# analyze the classic 2-D illegal tile-major schedule
go run ./cmd/polytile examples/illegal2d.json
# find a legal permutation and dump all direction vectors
go run ./cmd/polytile -brute -find-legal examples/illegal2d.json
Input/output are JSON; see examples/. Illegal output for examples/illegal2d.json:
{
"Legal": false,
"Method": "fm+gcd+banerjee+bounded-integer-search",
"Verified": true,
"Witness": {
"Src": 0, "Dst": 0,
"SrcIter": [0,5], "DstIter": [1,0],
"Distance": [1,-5], "Dir": "+-"
}
}
$ go vet ./... # clean
$ go build ./... # BUILD_OK
$ go test -run 'TestClassic|TestLoop|Test2D|TestFindLegal|TestInterleaved' -v
--- PASS: TestClassic1DLegal (tiling A[i]=A[i-1]+1, s=1..8)
--- PASS: TestClassic1DIllegalSwap (rem-outside-tile reverses δ=+1)
--- PASS: TestLoopIndependentAndSelfOutput (A[i]=A[i]+1 plus A[i]=A[i-1])
--- PASS: Test2DTilingIdentityIllegal (δ=(1,-5), tile-major → illegal)
--- PASS: TestFindLegalSchedule (alternate schedule re-verified)
--- PASS: TestInterleavedAlwaysLegal (interleaved order, 300 nests)
PASS
The tests assert:
1,2,3,4,8;(rem,tile) schedule rejected and both brute-force and polyhedral
witnesses pass VerifyCertificate;δ=+1 dependence still does;(1,-5) dependence;(t_0,r_0,t_1,r_1,…) order accepted on 300 random nests —
proving the RC-1 subtlety is handled, not over-rejected.TestRandomCrossCheck builds 1500 random nests
(D ∈ {1,2,3}, bounds of width ≤ 3, 1–3 accesses, random affine subscripts,
random tile sizes ∈ {1,2,3}, random (2D)! permutation) and requires
BruteForce.Legal == Analyze.Legal
for every case, and that every polyhedral witness verifies. Result:
$ go test -run TestRandomCrossCheck -v
--- PASS: TestRandomCrossCheck
TestDirectionsCrossCheck additionally requires the polyhedral
FeasibleDirections direction set to equal the brute-force
CollectDependences set on 400 random nests:
--- PASS: TestDirectionsCrossCheck
Full suite:
$ go test ./...
ok example.com/polyhedral 38.5s
VerifyCertificate): bounds, order, array-location equality, write flag,
and key reversal.baseSystem to make it exact.D is small in practice (4D variables, O(D²) disjuncts). The rational
Fourier-Motzkin step is capped and is only a refutation aid; the exact integer
search always runs and decides.Source: /workspace/polyhedral/solver.go,
/workspace/polyhedral/solver_test.go,
/workspace/polyhedral/cmd/polytile/main.go. A copy of this document is at
/workspace/SOLUTION.md and ~/SOLUTION.md.
# Evidence - Problem class: go-polyhedral-loop-tiling-dependence-validity-exactness - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-25T10:25:16.472Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Given a perfectly nested affine loop nest and a proposed tiling plus permutation schedule, decide exact legality and emit a machine-checkable certificate. Compute all dependence distance and direction vectors from the affine subscript functions, decide integer feasibility of the violated-directions system (Banerjee/GCD bounds refined by Fourier-Motzkin elimination over exact rationals), and return either a tile-legal witness schedule or a concrete iteration pair that the tiled schedule illegally reorders. Cross-check by exhaustive simulation on small nests, where the analyzer verdict must match brute-force permutation testing including degenerate zero-distance (loop-independent) and self-output dependences.", "environment": "go1.26", "language": "go", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "go-polyhedral-loop-tiling-dependence-validity-exactness", "provider": "openrouter", "solved_at": "2026-09-25T10:25:16.474Z", "version": "1.26"}Problem class: go-polyhedral-loop-tiling-dependence-validity-exactness
Environment: Go 1.26 · Implementation: /workspace/polyhedral
Given
for i_k = Lo_k .. Hi_k,A[ f(i) ] together with a read/write flag,s_k ≥ 1 plus a permutation π of the
2D coordinates (tile_k, rem_k), where
tile_k = ⌊i_k / s_k⌋, rem_k = i_k mod s_k,decide exactly whether the tiled/permuted execution order is a legal reordering of the original sequential program. Emit a machine-checkable certificate:
(i, j) with i <_lex j,
f_a(i) = f_b(j) for a conflicting access pair, and
Key(i) >_lex Key(j) (the tiled order reorders them).All analysis must be integer-exact (not floating point, not merely the
rational relaxation), and must agree with exhaustive brute force on small nests,
including degenerate i = j (loop-independent) and self-output dependences.
A naive implementation fails for seven distinct reasons. These are the actual failure modes addressed by the fix.
Taking direction vectors from earlier to later iteration always yields a
lexicographically positive δ (first non-zero component > 0). But the
tile-major order (t_0,…,t_{D-1}, r_0,…,r_{D-1}) is not a linear
extension of lexicographic order. Counterexample (depth 2, s = (2,2),
index = 5·i + j):
p = (0,5), q = (1,0), p <_lex q, δ = q - p = (1,-5) (lex-positive)
Key(p) = (t0,t1,r0,r1) = (0,2,0,1)
Key(q) = (0,0,1,0)
Key(p) > Key(q) → ILLEGAL
So legality must compare the actual keys of the two iterations, not just
signs of dependence directions. (The interleaved order (t_0,r_0,t_1,r_1,…)
is always legal — it is the reason RC-1 bites only for tile-major schedules —
and the test suite checks both facts.)
Banerjee bounds / Fourier-Motzkin decide feasibility over ℚ. They are
necessary but not sufficient over ℤ (e.g. 2x = 1 is rationally
feasible, integrally infeasible). Using them alone yields both false
"illegal" and false "legal" verdicts. The GCD test is required, and in general
an integer method (dark-shadow/branch-and-bound) is required.
⌊·⌋ and mod are not affineKey(i) contains ⌊i_k/s_k⌋ and i_k mod s_k. Substituting these directly
into a linear solver is invalid. The fix introduces tile and remainder
variables i_k = s_k·t_k + r_k, 0 ≤ r_k < s_k, which makes both Key and
the subscript equalities linear.
A conflicting pair with i = j (e.g. A[i] = A[i] + 1) is loop-independent:
it imposes no reordering constraint, because statements inside one
iteration are never reordered. Treating it as a constraint falsely rejects
legal schedules. Conversely, a self-output dependence with i ≠ j (two
writes to the same location) must be enforced, or illegal schedules are
accepted. Both are covered explicitly by tests.
Two reads of the same location do not constrain the schedule. Omitting the "at least one side writes" filter produces spurious dependences.
δ must be later − earlier where "earlier" is the lexicographically smaller
iteration, not the raw index order in an access list. Wrong orientation flips
signs and inverts the verdict.
Legality is about all conflicting pairs in the (bounded but potentially large)
iteration space, not just neighbours. A polyhedral encoding avoids enumerating
|space|² pairs.
type Affine struct { Coef []int64; Const int64 } // Const + Σ Coef[k]·i_k
type Access struct { Stmt, Array string; Write bool; Index []Affine }
type Nest struct { D int; Lo, Hi []int64; Accesses []Access }
type Schedule struct { Sizes []int64; Perm []int } // Perm[0] = most significant
func (s *Schedule) Key(i []int64) []int64 {
d := len(s.Sizes)
coord := make([]int64, 2*d)
for k := 0; k < d; k++ {
sz := s.Sizes[k]
t := floorDiv(i[k], sz)
coord[2*k] = t
coord[2*k+1] = i[k] - t*sz
}
key := make([]int64, 2*d)
for p, c := range s.Perm { key[p] = coord[c] }
return key
}
Certificate semantics. A witness is valid iff it passes
func (n *Nest) VerifyCertificate(s *Schedule, dep *Dependence) bool {
i, j := dep.SrcIter, dep.DstIter
// in bounds, i <_lex j, same array location, ≥1 write, Key(i) >_lex Key(j)
}
Lists every iteration and every conflicting pair, then compares keys. It is the reference the polyhedral engine is tested against.
for a := range n.Accesses {
for b := range n.Accesses {
if accesses[a].Array != accesses[b].Array { continue }
if !accesses[a].Write && !accesses[b].Write { continue } // RC-5
for i before j (i <_lex j): // RC-6
if sameLoc(a,b,i,j) {
if Key(i) > Key(j) { return illegal witness(i,j) } // RC-1
}
}
}
Loop-independent pairs i = j are skipped by i <_lex j, which is exactly the
correct semantics (RC-4).
Introduce 4D integer variables per conflicting pair: tI_k, rI_k, tJ_k, rJ_k
with i_k = s_k·tI_k + rI_k, j_k = s_k·tJ_k + rJ_k. Then:
f_a(i) = f_b(j) becomes a linear equality;i <_lex j is a disjunction over the first differing coordinate im
(i_l = j_l for l < im, i_im − j_im ≤ −1);Key(i) >_lex Key(j) is a disjunction over the first differing schedule
position km (coord = coord for earlier positions, coord_i − coord_j ≥ 1).func (n *Nest) violationSystem(s *Schedule, a, b, im, km int) *system {
sys := n.baseSystem(s) // bounds + 0≤r<s for i and j
n.subscriptConstraints(s, a, b, sys) // f_a(i) = f_b(j)
for l := 0; l < im; l++ { sys.addEq(iterDiff(l), 0) }
sys.add(iterDiff(im), -1, le) // i <_lex j
for p := 0; p < km; p++ { sys.addEq(coordDiff(s.Perm[p]), 0) }
sys.add(negate(coordDiff(s.Perm[km])), -1, le) // Key(i) >_lex Key(j)
return sys
}
For each access pair, each im, each km:
gcd(coeffs) | rhs for every equality.math/big.Rat — refutes rational-infeasible
systems exactly. Elimination order is chosen by smallest pos·neg product;
a constraint cap returns "not refuted" (never "infeasible"), so capping only
affects speed, never soundness.solveInteger). Domains come from the constant loop bounds, so
the search is complete; it is the final authority on integer feasibility.(i, j) and checked with
VerifyCertificate.func (n *Nest) Analyze(s *Schedule) (Result, error) {
for each conflicting (a,b) {
for im { for km {
sys := violationSystem(...)
if !gcdAdmissible(sys) || !banerjeeAdmissible(sys) { continue }
if !fmFeasible(sys.v, sys.constraints) { continue }
if ok, model := solveInteger(sys); ok {
i, j := decode(model, s)
return illegal(witness i,j)
}
}}
}
return legal(s) // s itself is the tile-legal witness
}
Direction/distance enumeration uses the same machinery over the 3^D sign
patterns (FeasibleDirections), and is cross-checked against the brute-force
CollectDependences.
When the proposed schedule is illegal, FindLegalSchedule enumerates
permutations for the given tile sizes and returns the first one the exact
analyzer accepts — this is the "tile-legal witness schedule" branch.
cd /workspace/polyhedral
go vet ./...
go test ./... # unit + randomized cross-checks
# analyze the classic 2-D illegal tile-major schedule
go run ./cmd/polytile examples/illegal2d.json
# find a legal permutation and dump all direction vectors
go run ./cmd/polytile -brute -find-legal examples/illegal2d.json
Input/output are JSON; see examples/. Illegal output for examples/illegal2d.json:
{
"Legal": false,
"Method": "fm+gcd+banerjee+bounded-integer-search",
"Verified": true,
"Witness": {
"Src": 0, "Dst": 0,
"SrcIter": [0,5], "DstIter": [1,0],
"Distance": [1,-5], "Dir": "+-"
}
}
$ go vet ./... # clean
$ go build ./... # BUILD_OK
$ go test -run 'TestClassic|TestLoop|Test2D|TestFindLegal|TestInterleaved' -v
--- PASS: TestClassic1DLegal (tiling A[i]=A[i-1]+1, s=1..8)
--- PASS: TestClassic1DIllegalSwap (rem-outside-tile reverses δ=+1)
--- PASS: TestLoopIndependentAndSelfOutput (A[i]=A[i]+1 plus A[i]=A[i-1])
--- PASS: Test2DTilingIdentityIllegal (δ=(1,-5), tile-major → illegal)
--- PASS: TestFindLegalSchedule (alternate schedule re-verified)
--- PASS: TestInterleavedAlwaysLegal (interleaved order, 300 nests)
PASS
The tests assert:
1,2,3,4,8;(rem,tile) schedule rejected and both brute-force and polyhedral
witnesses pass VerifyCertificate;δ=+1 dependence still does;(1,-5) dependence;(t_0,r_0,t_1,r_1,…) order accepted on 300 random nests —
proving the RC-1 subtlety is handled, not over-rejected.TestRandomCrossCheck builds 1500 random nests
(D ∈ {1,2,3}, bounds of width ≤ 3, 1–3 accesses, random affine subscripts,
random tile sizes ∈ {1,2,3}, random (2D)! permutation) and requires
BruteForce.Legal == Analyze.Legal
for every case, and that every polyhedral witness verifies. Result:
$ go test -run TestRandomCrossCheck -v
--- PASS: TestRandomCrossCheck
TestDirectionsCrossCheck additionally requires the polyhedral
FeasibleDirections direction set to equal the brute-force
CollectDependences set on 400 random nests:
--- PASS: TestDirectionsCrossCheck
Full suite:
$ go test ./...
ok example.com/polyhedral 38.5s
VerifyCertificate): bounds, order, array-location equality, write flag,
and key reversal.baseSystem to make it exact.D is small in practice (4D variables, O(D²) disjuncts). The rational
Fourier-Motzkin step is capped and is only a refutation aid; the exact integer
search always runs and decides.Source: /workspace/polyhedral/solver.go,
/workspace/polyhedral/solver_test.go,
/workspace/polyhedral/cmd/polytile/main.go. A copy of this document is at
/workspace/SOLUTION.md and ~/SOLUTION.md.
# Evidence - Problem class: go-polyhedral-loop-tiling-dependence-validity-exactness - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-09-25T10:25:16.472Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Given a perfectly nested affine loop nest and a proposed tiling plus permutation schedule, decide exact legality and emit a machine-checkable certificate. Compute all dependence distance and direction vectors from the affine subscript functions, decide integer feasibility of the violated-directions system (Banerjee/GCD bounds refined by Fourier-Motzkin elimination over exact rationals), and return either a tile-legal witness schedule or a concrete iteration pair that the tiled schedule illegally reorders. Cross-check by exhaustive simulation on small nests, where the analyzer verdict must match brute-force permutation testing including degenerate zero-distance (loop-independent) and self-output dependences.", "environment": "go1.26", "language": "go", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "go-polyhedral-loop-tiling-dependence-validity-exactness", "provider": "openrouter", "solved_at": "2026-09-25T10:25:16.474Z", "version": "1.26"}