Skip to content

Commit 2fcfb43

Browse files
ChrisRackauckas-ClaudeChrisRackauckasclaude
authored
Move the SupernodalLU sweep proof to a QA-only file (#1121)
`test/runtests.jl` includes `qa/allocations.jl` from two groups, and they do not cover the same Julia versions: [QA] versions = ["lts", "1"] [AppleAccelerate] versions = ["lts", "1", "pre"] So AllocCheck ran on `pre` through a group that was never meant to carry it. The file mixes two things with different portability. The direct-BLAS refactorization proofs hold on every release - that contract is why the AppleAccelerate group exists. The SupernodalLU sweep proof does not: above `PANEL_BLAS_CUTOFF` the sweeps hand off to LinearAlgebra's `ldiv!`/`mul!`, whose wrappers leave a `generic_trimatdiv!` dynamic dispatch plus boxed `MulAddMul`/`SubArray` values that AllocCheck reports on 1.10 and 1.13. Only the second one belongs behind QA's version set, so only it moves. Measured, same two matrices as the testset: Julia 1.10.11 x86_64-Linux 18 static findings runtime 0 B / 0 B Julia 1.12.6 x86_64-Linux 0 static findings runtime 0 B / 0 B 18 findings on 1.10 x86_64-Linux is the same count #1119 measured on 1.10 aarch64-Darwin, and 1.12 is clean on both, so this is the stdlib and the Julia version - not the platform, and not this package's code. Worth noting the coverage is narrower than the toml suggests: only one QA job materialises (`QA (julia 1)`), so the static proof runs on 1.12 alone. The static proof keeps a version guard, since that is a limit of the prover. `RUNTIME_MULTIRHS_ZERO` is dropped: it gated a *runtime* allocation assertion, and on 1.11 that assertion fails because the multi-RHS path really does allocate (6144 B, per #1119's table). Skipping it hides a regression rather than a prover limitation, so it should fail there until the allocation is fixed. Verified: `qa/allocations.jl` completes on Julia 1.10, the version that was failing; `GROUP=QA` and `GROUP=Core` both pass on 1.12, which is what CI runs. Stacked on #1119 - it carries the `_lu_from_cacheval` fix this needs. Claude-Session: https://claude.ai/code/session_017rr42T1vFRRT8D7DMAmJzf Co-authored-by: ChrisRackauckas-Claude <accounts@chrisrackauckas.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent e9d545e commit 2fcfb43

3 files changed

Lines changed: 82 additions & 66 deletions

File tree

‎test/qa/allocations.jl‎

Lines changed: 4 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -63,69 +63,7 @@ if LinearSolve.appleaccelerate_isavailable()
6363
end
6464
end
6565

66-
# SupernodalLU: the triangular sweeps run entirely off buffers owned by the
67-
# factorization, whose sizes are known from the symbolic analysis, so they
68-
# carry no growth branch and AllocCheck can prove them allocation-free
69-
# statically (rather than sampling `@allocated`). The user-facing `solve!`
70-
# keeps a one-time scratch sizing, so it is asserted at runtime instead.
71-
@check_allocs allocation_checked_supernodal_sweeps!(y, F) =
72-
LinearSolve.SupernodalLU._solve_panels!(y, F)
73-
74-
# What the sweeps can be *proved* about depends on the Julia version, because
75-
# above `PANEL_BLAS_CUTOFF` they hand off to LinearAlgebra's `ldiv!`/`mul!`,
76-
# whose wrappers are not statically clean on every release: 1.10 and 1.13 leave
77-
# a `generic_trimatdiv!` dynamic dispatch plus boxed `MulAddMul`/`SubArray`
78-
# values that AllocCheck reports (`triangular.jl`, `matmul.jl` — stdlib frames,
79-
# no SupernodalLU code involved), and 1.11 allocates them for real on the
80-
# `SubArray`-matrix path the multi-RHS sweep takes. 1.12 folds all of it away.
81-
# So pin each assertion to the versions that can carry it rather than weakening
82-
# it everywhere; the sweeps carry no growth branch on any version, which is what
83-
# these are here to protect.
84-
const STATIC_SWEEP_PROOF = v"1.12" <= VERSION < v"1.13"
85-
const RUNTIME_MULTIRHS_ZERO = VERSION < v"1.11" || VERSION >= v"1.12"
86-
87-
function poisson2d_qa(k)
88-
n = k * k
89-
Is = Int[]; Js = Int[]; V = Float64[]
90-
idx(i, j) = (j - 1) * k + i
91-
for j in 1:k, i in 1:k
92-
c = idx(i, j)
93-
push!(Is, c); push!(Js, c); push!(V, 4.0)
94-
i > 1 && (push!(Is, c); push!(Js, idx(i - 1, j)); push!(V, -1.0))
95-
i < k && (push!(Is, c); push!(Js, idx(i + 1, j)); push!(V, -1.0))
96-
j > 1 && (push!(Is, c); push!(Js, idx(i, j - 1)); push!(V, -1.0))
97-
j < k && (push!(Is, c); push!(Js, idx(i, j + 1)); push!(V, -1.0))
98-
end
99-
return sparse(Is, Js, V, n, n)
100-
end
101-
102-
@testset "SupernodalLU solve sweeps are provably allocation-free" begin
103-
for A in (
104-
SparseArrays.spdiagm(
105-
0 => fill(4.0, 200), 1 => fill(-1.0, 199), -1 => fill(-1.0, 199)
106-
),
107-
poisson2d_qa(30), # real panels: maxnu > 1
108-
)
109-
n = size(A, 1)
110-
F = LinearSolve.SupernodalLU.snlu(A)
111-
LinearSolve.SupernodalLU._ensure_panel_scratch!(F, 1)
112-
y = ones(n)
113-
if STATIC_SWEEP_PROOF
114-
allocation_checked_supernodal_sweeps!(y, F) # throws if it can allocate
115-
@test true
116-
end
117-
# the full solve!, which owns the one-time sizing, is zero at runtime
118-
b = ones(n)
119-
x = similar(b)
120-
LinearSolve.SupernodalLU.solve!(x, F, b; refine = 0)
121-
@test @allocated(LinearSolve.SupernodalLU.solve!(x, F, b; refine = 0)) == 0
122-
@test norm(A * x - b) <= 1.0e-8 * norm(b)
123-
# multi-RHS reuses the factor-owned scratch once sized
124-
B = ones(n, 3)
125-
X = similar(B)
126-
LinearSolve.SupernodalLU.solve!(X, F, B; refine = 0)
127-
if RUNTIME_MULTIRHS_ZERO
128-
@test @allocated(LinearSolve.SupernodalLU.solve!(X, F, B; refine = 0)) == 0
129-
end
130-
end
131-
end
66+
# SupernodalLU's sweep proof lives in `qa/supernodal_allocations.jl`, which only
67+
# the QA group includes: this file also runs under `[AppleAccelerate]`, which
68+
# covers `pre`, and that proof only holds on 1.12 (it bottoms out in stdlib
69+
# `ldiv!`/`mul!` wrappers). The direct-BLAS proofs above hold on every release.

‎test/qa/supernodal_allocations.jl‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
# SupernodalLU allocation coverage.
2+
#
3+
# Separate from `qa/allocations.jl` because the two are included by different
4+
# groups: `allocations.jl` also runs under `[AppleAccelerate]`, which covers
5+
# `pre`, while this file is QA-only. The direct-BLAS refactorization proofs
6+
# over there hold on every release; the sweep proof here does not, because
7+
# above `PANEL_BLAS_CUTOFF` the sweeps hand off to LinearAlgebra's
8+
# `ldiv!`/`mul!`, whose wrappers are not statically clean on every version.
9+
# Keeping them in one file put a 1.12-only proof inside a file that `pre` runs.
10+
11+
using AllocCheck, LinearAlgebra, LinearSolve, SparseArrays, Test
12+
13+
# The triangular sweeps run entirely off buffers owned by the factorization,
14+
# whose sizes are known from the symbolic analysis, so they carry no growth
15+
# branch and AllocCheck can prove them allocation-free statically (rather than
16+
# sampling `@allocated`). The user-facing `solve!` keeps a one-time scratch
17+
# sizing, so it is asserted at runtime instead.
18+
@check_allocs allocation_checked_supernodal_sweeps!(y, F) =
19+
LinearSolve.SupernodalLU._solve_panels!(y, F)
20+
21+
# The *static proof* is version-dependent: 1.10 and 1.13 leave a
22+
# `generic_trimatdiv!` dynamic dispatch plus boxed `MulAddMul`/`SubArray` values
23+
# that AllocCheck reports (`triangular.jl`, `matmul.jl` — stdlib frames, no
24+
# SupernodalLU code involved); 1.12 folds all of it away. Measured identically
25+
# on x86_64-Linux and aarch64-Darwin (18 findings on 1.10 on both, 0 on 1.12),
26+
# so this is the stdlib, not the platform, and not this package's code.
27+
#
28+
# The *runtime* assertions below are deliberately NOT gated: those measure real
29+
# allocations, and skipping one would hide a genuine regression rather than a
30+
# limitation of the prover.
31+
const STATIC_SWEEP_PROOF = v"1.12" <= VERSION < v"1.13"
32+
33+
function poisson2d_qa(k)
34+
n = k * k
35+
Is = Int[]; Js = Int[]; V = Float64[]
36+
idx(i, j) = (j - 1) * k + i
37+
for j in 1:k, i in 1:k
38+
c = idx(i, j)
39+
push!(Is, c); push!(Js, c); push!(V, 4.0)
40+
i > 1 && (push!(Is, c); push!(Js, idx(i - 1, j)); push!(V, -1.0))
41+
i < k && (push!(Is, c); push!(Js, idx(i + 1, j)); push!(V, -1.0))
42+
j > 1 && (push!(Is, c); push!(Js, idx(i, j - 1)); push!(V, -1.0))
43+
j < k && (push!(Is, c); push!(Js, idx(i, j + 1)); push!(V, -1.0))
44+
end
45+
return sparse(Is, Js, V, n, n)
46+
end
47+
48+
@testset "SupernodalLU solve sweeps are provably allocation-free" begin
49+
for A in (
50+
SparseArrays.spdiagm(
51+
0 => fill(4.0, 200), 1 => fill(-1.0, 199), -1 => fill(-1.0, 199)
52+
),
53+
poisson2d_qa(30), # real panels: maxnu > 1
54+
)
55+
n = size(A, 1)
56+
F = LinearSolve.SupernodalLU.snlu(A)
57+
LinearSolve.SupernodalLU._ensure_panel_scratch!(F, 1)
58+
y = ones(n)
59+
if STATIC_SWEEP_PROOF
60+
allocation_checked_supernodal_sweeps!(y, F) # throws if it can allocate
61+
@test true
62+
end
63+
# the full solve!, which owns the one-time sizing, is zero at runtime
64+
b = ones(n)
65+
x = similar(b)
66+
LinearSolve.SupernodalLU.solve!(x, F, b; refine = 0)
67+
@test @allocated(LinearSolve.SupernodalLU.solve!(x, F, b; refine = 0)) == 0
68+
@test norm(A * x - b) <= 1.0e-8 * norm(b)
69+
# multi-RHS reuses the factor-owned scratch once sized
70+
B = ones(n, 3)
71+
X = similar(B)
72+
LinearSolve.SupernodalLU.solve!(X, F, B; refine = 0)
73+
@test @allocated(LinearSolve.SupernodalLU.solve!(X, F, B; refine = 0)) == 0
74+
end
75+
end

‎test/runtests.jl‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -230,6 +230,9 @@ else
230230
@time @safetestset "Quality Assurance" include("qa/qa.jl")
231231
@time @safetestset "JET Tests" include("qa/jet.jl")
232232
@time @safetestset "Allocation QA" include("qa/allocations.jl")
233+
@time @safetestset "SupernodalLU Allocation QA" include(
234+
"qa/supernodal_allocations.jl"
235+
)
233236
end
234237
return nothing
235238
end,

0 commit comments

Comments
 (0)