You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Link: timefold's PillarSwapMoveSelectorFactory.buildBaseMoveSelector trips the work ceiling with the #23 fix, and is taken as modifying #97
Found while measuring the #23 fix (302b074, gate NOMIRRORSOURCES). On timefold, with the fix:
PillarSwapMoveSelectorFactory.buildBaseMoveSelector changes from nonModifying=true to false;
the change repeats in two runs per setting, and it is the only verdict that changes.
MODREACH_EXPLAIN shows four nodes, each reached in one step from the same seed:
receiver: PillarSwapMoveSelectorFactory.buildBaseMoveSelector(..)
param 0:configPolicy, 1:minimumCacheType (an enum), 2:randomSelection (a boolean)
seeded by RuinRecreateConstructionHeuristicPhaseBuilder.create(..) modified this.phaseConfig.moveSelectorConfigList
The seed is real: the phase factory fills a fresh config's move selector list.
The reach is not: a boolean and an enum cannot be modified. The method itself only reads config, builds two selectors, and hands them to PillarSwapMoveSelector, whose constructor registers them as listeners on its own support object.
Likely mechanism, not yet confirmed: the factory's config is an element of that list. The mirror fix makes a field-level link more precise and exposes that relation. The reachability pass then treats a structural modification of the list (adding elements) as a modification of the objects that hold its elements, and of every node of the method it reaches.
Next: print the BFS edges between the seed and the receiver. MODREACH_EXPLAIN prints only the seed here, so the chain has length one. Then find which edge kind lets a list's structural change reach an element's holder.
changed the title [-]MODREACH: a list's modification reaches the receiver and all parameters of a method holding one of its elements (timefold PillarSwapMoveSelectorFactory)[/-][+]Link: timefold's PillarSwapMoveSelectorFactory.buildBaseMoveSelector trips the work ceiling with the #23 fix, and is taken as modifying[/+]on Nov 5, 2026
tripped at statement 16, return new PillarSwapMoveSelector(..)
126
10,476
23,334
buildBaseMoveSelector is the only method that trips only with the fix (131 → 141 trip lines). Its analysis is abandoned (DEGRADED_ANALYSIS_METHOD), and the soundness seeds mark its receiver and all its parameters as modified. That is why the boolean and the enum appeared.
MODREACH_EXPLAIN named RuinRecreateConstructionHeuristicPhaseBuilder.create because the soundness seeds had no origin: the next method's summary seeding labelled them with its own name. 599a0d3 on ws/maddi-null fixes the label.
The real question is why a 16-statement method needs a closure of about 10k facts and 21k witnesses, already at 89% of the ceiling before the fix. Same family as #92 (fernflower). Next: LINKDUMP of this method's closure.
Where the work goes (LINKDUMP, 6567473, timefold, gate set so the method completes: 10,672 closure facts, work 8.9M of 10M):
nature
facts
∩
7,920
≈
1,800
everything else
under 1,000 together
The 7,920 ∩ facts sit among 100 variables, close to a complete pairwise relation (100·99 = 9,900). The variables involved most often are the virtual fields of the type parameter Solution_:
Almost every object in timefold's configuration layer is generic in Solution_, so the engine derives that each one may share Solution_ content with every other one, one ∩ fact per pair. The closure grows with the square of the number of such variables. The #23 fix adds a few, which takes this method from 89% to over the ceiling.
Directions, for discussion:
Represent "shares content of type parameter T" as membership of one class per type parameter, instead of pairwise ∩ facts: linear, not quadratic.
Derive no ∩ between two variables whose only common content is an unbounded type parameter that the method never reads or modifies. Cheaper, but it loses facts that modification through T would need.
The variables in the middle are not specific to type parameters:
timefold: §solution_ (a type parameter), list content §$s, the content behind an interface field (probabilityWeightFactory.§$), plain objects;
fernflower: collection and map content (§$$s[-2], first1.mapPredStates.§$$s), call results ($__rv45).
Any variable that many others may share content with does it.
Two multipliers, the same in both methods:
Materialization (IncrementalFixpointEngine.materializeWitnessOrphans, the determinism fix). When a temporary leaves the graph, every fact derived through it becomes a raw edge, including the whole pairwise ∩ set through that temporary. About half the ∩ facts in both methods are these. As raw edges they feed every later derivation.
∩ copied along aliases.∩ composed with ←, → or ≡ gives each alias of a variable its own copy of each overlap.
∩ composed with ∩ (not transitive in truth) contributes 1–2%. Removing that rule alone would not help.
Direction: keep overlap implicit through the shared variable instead of storing it pairwise. Where a materialization would create n² ∩ edges through a dying variable, keep that variable, or a stand-in for the content, with n edges, and answer "do a and b overlap?" through it. Likewise, ∩ along an alias group belongs on the group's representative, once. This covers type parameters, interface- and abstract-typed content, collections and plain objects alike.
Lazy materialization for ∩ (fdc6552 on ws/maddi-null, gate NOLAZYMAT; laser1, NOLAZYMAT=1 vs default):
When a temporary leaves the graph, an orphaned ∩ fact is no longer promoted to a raw edge if one surviving middle vertex re-derives it from two facts that are not orphans and do not depend on the removed vertices. The check uses propagateForward's rules and decides for all orphans before any promotion.
It is restricted to ∩. Applied to every label (diagnostic LAZYMATANY), it changed verdicts: a re-derived ⊆/≥ fact stays tied to its support, so witness-following rewrites such as replaceReturnAffected (⊆ to ~) reach it.
530/0 (one expectation updated: two ∩ facts are derived instead of materialized)
Verdict differences:
timefold: only buildBaseMoveSelector.
fernflower: DomHelper.detectStatement and MergeHelper.matchDoWhile become non-modifying. MODREACH_EXPLAIN (with 599a0d3's origins) shows both receivers were seeded only because their own analysis was abandoned. They are exactly the two methods that trip only without the change.
The other five OSS corpora (laser1, NOLAZYMAT=1 vs fdc6552):
corpus
verdict changes
trips
methods tripping only with the rule
elasticsearch
0
24 → 24
0
guava
0 (see below)
14 → 14
0
langchain4j
0
15 → 16
0
jenkins
0
8 → 8
0
activemq
0
0 → 0
0
Guava's first pair differed in one field, CycleDetectingLockFactory.LockGraphNode.allowedPriorLocks (@Independent with the gate set, @Dependent without). Two more runs per setting all give @Dependent and identical verdict files. So the @Independent was run-to-run variance in the old setting, about one run in three; that is a residual nondeterminism of its own.
The change set is ready to merge: 599a0d3 (MODREACH_EXPLAIN origins), 6567473 (LINKDUMP from the environment), d4931d4 + fdc6552 (lazy ∩ materialization). It fixes this issue's symptom: buildBaseMoveSelector no longer trips. It cuts timefold's trips 149 → 130 and fernflower's 301 → 276. #92 stays open for the derivation of the pairwise ∩ itself.
Merged into devel: d4931d4 + fdc6552 (∩-only lazy materialization, gate NOLAZYMAT), 599a0d3 (degraded-seed origin), 6567473 (LINKDUMP from env), 4aca117 (SCCJOIN removed). buildBaseMoveSelector no longer trips (93–95% of the ceiling) and is non-modifying again. The structural fix for the ∩ closure growth stays with #92.
Activity
[-]MODREACH: a list's modification reaches the receiver and all parameters of a method holding one of its elements (timefold PillarSwapMoveSelectorFactory)[/-][+]Link: timefold's PillarSwapMoveSelectorFactory.buildBaseMoveSelector trips the work ceiling with the #23 fix, and is taken as modifying[/+]bnaudts commentedon Nov 5, 2026
The reachability pass is not the cause; this issue's first diagnosis was wrong (laser1, timefold, gate
NOMIRRORSOURCESset vs the fix):return new PillarSwapMoveSelector(..)buildBaseMoveSelectoris the only method that trips only with the fix (131 → 141 trip lines). Its analysis is abandoned (DEGRADED_ANALYSIS_METHOD), and the soundness seeds mark its receiver and all its parameters as modified. That is why thebooleanand the enum appeared.MODREACH_EXPLAINnamedRuinRecreateConstructionHeuristicPhaseBuilder.createbecause the soundness seeds had no origin: the next method's summary seeding labelled them with its own name. 599a0d3 on ws/maddi-null fixes the label.The real question is why a 16-statement method needs a closure of about 10k facts and 21k witnesses, already at 89% of the ceiling before the fix. Same family as #92 (fernflower). Next:
LINKDUMPof this method's closure.bnaudts commentedon Nov 5, 2026
Where the work goes (
LINKDUMP, 6567473, timefold, gate set so the method completes: 10,672 closure facts, work 8.9M of 10M):∩≈The 7,920
∩facts sit among 100 variables, close to a complete pairwise relation (100·99 = 9,900). The variables involved most often are the virtual fields of the type parameterSolution_:§$solution_s[-1],§$solution_s[-2],§$solution_ss[-2]0:configPolicy.§solution_0:configPolicy.solutionDescriptor.genuineEntityDescriptorList.§solution_ss$__sv_leftPillarSelector.pillarDemand.variableDescriptors.§solution_s0:configPolicy.valueMimicRecorderMap.§$solution_sAlmost every object in timefold's configuration layer is generic in
Solution_, so the engine derives that each one may shareSolution_content with every other one, one∩fact per pair. The closure grows with the square of the number of such variables. The #23 fix adds a few, which takes this method from 89% to over the ceiling.Directions, for discussion:
∩facts: linear, not quadratic.∩between two variables whose only common content is an unbounded type parameter that the method never reads or modifies. Cheaper, but it loses facts that modification throughTwould need.MODREACH: the soundness seeds of an abandoned method carry their own …
Link: LINKDUMP=<method> in the environment dumps the closure, as madd…
bnaudts commentedon Nov 6, 2026
Where the
∩facts come from, timefold and fernflower (LINKDUMP, every closure fact classified by its witness):PillarSwapMoveSelectorFactory.buildBaseMoveSelectorDomHelper.findGeneralStatement(#92)∩∩materialized (mat)∩derived∩composed with←/→/≡∩composed with∩∩inserted by a statementbuildPillarSelector(..)calls)The variables in the middle are not specific to type parameters:
§solution_(a type parameter), list content§$s, the content behind an interface field (probabilityWeightFactory.§$), plain objects;§$$s[-2],first1.mapPredStates.§$$s), call results ($__rv45).Any variable that many others may share content with does it.
Two multipliers, the same in both methods:
IncrementalFixpointEngine.materializeWitnessOrphans, the determinism fix). When a temporary leaves the graph, every fact derived through it becomes a raw edge, including the whole pairwise∩set through that temporary. About half the∩facts in both methods are these. As raw edges they feed every later derivation.∩copied along aliases.∩composed with←,→or≡gives each alias of a variable its own copy of each overlap.∩composed with∩(not transitive in truth) contributes 1–2%. Removing that rule alone would not help.Direction: keep overlap implicit through the shared variable instead of storing it pairwise. Where a materialization would create n²
∩edges through a dying variable, keep that variable, or a stand-in for the content, with n edges, and answer "do a and b overlap?" through it. Likewise,∩along an alias group belongs on the group's representative, once. This covers type parameters, interface- and abstract-typed content, collections and plain objects alike.bnaudts commentedon Nov 6, 2026
Lazy materialization for
∩(fdc6552 on ws/maddi-null, gateNOLAZYMAT; laser1,NOLAZYMAT=1vs default):When a temporary leaves the graph, an orphaned
∩fact is no longer promoted to a raw edge if one surviving middle vertex re-derives it from two facts that are not orphans and do not depend on the removed vertices. The check usespropagateForward's rules and decides for all orphans before any promotion.It is restricted to
∩. Applied to every label (diagnosticLAZYMATANY), it changed verdicts: a re-derived⊆/≥fact stays tied to its support, so witness-following rewrites such asreplaceReturnAffected(⊆to~) reach it.PillarSwapMoveSelectorFactory.buildBaseMoveSelectorDomHelper.findGeneralStatement∩facts are derived instead of materialized)Verdict differences:
buildBaseMoveSelector.DomHelper.detectStatementandMergeHelper.matchDoWhilebecome non-modifying.MODREACH_EXPLAIN(with 599a0d3's origins) shows both receivers were seeded only because their own analysis was abandoned. They are exactly the two methods that trip only without the change.detectStatement's parameterheadstays modified, throughIfStatement.<init>andStatement.removeSuccessor, the real modification of Modification through a call result that is a field of the receiver (≺) does not reach the receiver #80.Elasticsearch, guava, langchain4j, jenkins and activemq are being measured.
bnaudts commentedon Nov 6, 2026
The other five OSS corpora (laser1,
NOLAZYMAT=1vs fdc6552):Guava's first pair differed in one field,
CycleDetectingLockFactory.LockGraphNode.allowedPriorLocks(@Independentwith the gate set,@Dependentwithout). Two more runs per setting all give@Dependentand identical verdict files. So the@Independentwas run-to-run variance in the old setting, about one run in three; that is a residual nondeterminism of its own.The change set is ready to merge: 599a0d3 (
MODREACH_EXPLAINorigins), 6567473 (LINKDUMPfrom the environment), d4931d4 + fdc6552 (lazy∩materialization). It fixes this issue's symptom:buildBaseMoveSelectorno longer trips. It cuts timefold's trips 149 → 130 and fernflower's 301 → 276. #92 stays open for the derivation of the pairwise∩itself.Link engine: an orphan that a surviving middle vertex re-derives is n…
Link engine: lazy materialization for '∩' orphans only; LAZYMATANY fo…
bnaudts commentedon Nov 7, 2026
Merged into devel: d4931d4 + fdc6552 (∩-only lazy materialization, gate NOLAZYMAT), 599a0d3 (degraded-seed origin), 6567473 (LINKDUMP from env), 4aca117 (SCCJOIN removed). buildBaseMoveSelector no longer trips (93–95% of the ceiling) and is non-modifying again. The structural fix for the ∩ closure growth stays with #92.