Ingest: Efficiently intertwining widening and narrowing

Type: types/ingest-report.md

Classification

A scientific paper in programming-language theory: it defines an operator, states and proves soundness and termination theorems, gives counterexamples to naive constructions, and reports an implementation evaluation in the Goblint analyzer. The captured observation is the arXiv v1 preprint (March 2015, marked "Preprint submitted to Elsevier"); the published journal version may differ. The PDF also carries an appended internal note, "Some notes on localized widening and hierarchical orderings" ("No Author Given"), which is working material rather than part of the paper's argument. Author: Amato and Scozzari (Chieti-Pescara), Seidl (TU München), Apinis and Vojdani (Tartu) — established static-analysis researchers; the paper extends their PLDI 2013 paper and Amato and Scozzari's SAS 2013 localized-widening work, and the evaluation runs in the authors' own analyzer.

Summary

Static analysis computes program invariants as solutions of equation systems over ordered value domains. When the domain has infinite ascending chains, plain iteration may not terminate, so Cousot and Cousot's classic scheme runs a widening phase, which forces termination by jumping to coarser values, and then a narrowing phase, which walks back down to recover precision. The two trades are explicit in the definitions. A widening result is an upper bound of both inputs, so a widened solution stays sound (it over-approximates every true behaviour) while losing precision. A narrowing result for a ⊒ b lies between the current value a and the recomputed value b, and narrowing is only defined for descending steps from a post-solution, so it can improve precision without dropping below what the equations still produce. The paper argues that the strict two-phase split wastes precision, because over-approximations are fully propagated before narrowing starts and "in general" cannot be recovered afterward. It defines a combined operator that narrows whenever the new value is below the current one and widens otherwise, and proves that any solver that terminates with it returns a post-solution, even for non-monotonic systems. Termination is harder: standard round-robin and worklist iteration with the combined operator can fail to terminate even on monotonic systems. The paper therefore gives priority-ordered solvers (structured round-robin, structured worklist, and a local solver, SLR, with a side-effecting extension) that terminate for monotonic systems with finitely many encountered unknowns. It shows by a one-equation example that non-monotonic systems can oscillate forever and proposes bounding, per unknown, how often iteration may switch from narrowing back to widening. Extensions apply the operator only at dynamically detected loop heads, which may also be removed again during solving, and restart iteration below a loop head whose value decreased. In Goblint on interval analysis, the combined solver beat two-phase solving at many program points on WCET benchmarks. Localized application with removable widening points improved precision further and cut right-hand-side evaluations by about 30%. Restarting gave mixed precision and sometimes large slowdowns. All of these results are bounded to one abstract domain (32-bit intervals) and one analyzer.

Quotes

No source quotes have been retained yet.

Connections Found

The source's role is a formal counterpart, not direct evidence: it gives exact definitions for the two trades that the KB's claim-revision notes describe informally. Widening spends precision to guarantee termination, as defensive abstraction in generality bought to avoid counterexamples is paid for in precision spends precision to guarantee survival of counterexamples — compares-with on the axis "precision spent to buy a guarantee". Two findings line up with that note's repairs. Precision lost at one point and propagated through the system is generally unrecoverable by later narrowing, which matches the note's claim that diffuse abstraction cannot be audited or undone site by site. Applying the operator only at loop heads, and removing a loop head from that set once it is stable, raised precision, which matches the note's section on localizing abstraction. The comparison is structural: the paper's widening is a sound operator with a formal specification, while the note's widening is a rhetorical move with no ordering that guarantees soundness.

Narrowing bought to survive review is paid for in content shares the word but not the direction — compares-with on the axis "what bounds a narrowing step", with a term clash any citing text must resolve. In the paper, narrowing shrinks an over-approximation, so the invariant says more and precision rises; the constraint prevents it from claiming too much (falling below the recomputed value). In the KB note, narrowing shrinks a claim's subject, so the claim says less; the failure it guards against is saying too little (an analytic claim). The paper's bound therefore answers the opposite failure. Its transferable part is the form of the constraint: a narrowing step is admissible only when bounded by a fresh re-derivation from the governing constraints, and it reverts to widening when that re-derivation rises.

The source is evidence for the family list in cost-sensitive formalisms for tentative theory search, which has no family for accelerated fixpoint iteration, where termination is bought with precision rather than with search work or memory. The transfer caveat is strong: the paper's guarantees depend on a partial order over values and on operators with exact algebraic properties, and a tentative theory has no such ordering by default. Automated note refinement as search over a source bundle is a see-also: that proposal relies on a budget to stop a loop it calls non-convergent, and the paper gives the precise assumptions under which an up-and-down refinement loop terminates, plus examples where it cycles without them.

No KB note yet uses abstract interpretation as a source; this is the first ingest on the topic. Derived-from: arXiv 1503.00883v1.

Extractable Value

1. The three-way trade, stated exactly -- widening guarantees convergence and keeps soundness (every result is an upper bound) but gives up precision; narrowing recovers precision and its descending sequences must stabilize, but it keeps soundness only on descending steps from a post-solution with monotonic equations; the combined operator keeps soundness on any terminating run but needs iteration order and monotonicity for termination. This answers the occasion's first question with definitions rather than analogy, and gives the KB's widen/narrow notes a precise vocabulary for which guarantee each move buys and which it spends. [quick-win]
2. What stops narrowing from dropping what is true -- two conditions together: the narrowed value must stay at or above the value freshly recomputed from the equations (a ⊒ a∆b ⊒ b), and narrowing fires only when that recomputation is at or below the current value; otherwise the operator widens. Under monotonicity from a post-solution, the sequence stays a post-solution. For claim revision, the transferable form is that a sharpening step is licensed only by re-deriving from the evidence, and must back off when the re-derivation contradicts it. The direction of "narrowing" is reversed relative to the KB's subject-narrowing note, so the transfer is to claim sharpening, not to subject shrinking. [quick-win]
3. Correct before loss propagates -- the paper's central motivation: over-approximation propagated through dependent unknowns generally cannot be recovered by a later downward pass, so correction is interleaved with growth. This is a formal precedent for the generality note's localization repair and for correcting a widened claim before citers import it. Context-bound: in the paper the damage mechanism is monotone propagation through equations; in a KB it is citation, which has no comparable guarantee. [quick-win]
4. Alternating widen and narrow can cycle forever -- Example 8 (one non-monotonic equation alternating 0 and ∞) and Example 20 (narrowing immediately cancelling each widening) show that interleaving improvement and coarsening can fail to terminate, and standard round-robin or worklist order fails even on monotonic systems. The remedy is a per-unknown cap on switches from narrowing back to widening, or progressively weaker narrowing until the step leaves the value unchanged. This is a candidate design constraint for review-and-repair loops that alternately broaden and sharpen a claim. [experiment]
5. Localize the lossy operator, and let the set shrink -- restricting the operator to an admissible set of points preserves termination only if the set respects the iteration order; dynamically removing a stable point from the set (SLR3) raised precision at many program points and also reduced work. This refines the generality note's "localize abstraction" repair: where the lossy move is allowed should be revisited once the local problem has stabilized. [experiment]
6. A missing family for the cost-sensitive catalogue -- accelerated fixpoint iteration prices termination in precision, a budget the catalogue does not yet name. Its value there is conditional on stating the ordering assumptions the transfer lacks. [just-a-reference]

Limitations (our opinion)

The theorems hold for monotonic right-hand sides and finitely many encountered unknowns; for the non-monotonic systems that motivate the paper (context-sensitive inter-procedural analysis), termination is evidence from experiments, not a guarantee, and the largest benchmark (445.gobmk, 412 kloc) did not finish within five hours. The precision comparison against two-phase solving was run context-insensitively on one domain (32-bit intervals with standard widening and narrowing), on small WCET programs plus four programs from Amato and Scozzari chosen because they are hard cases; the authors themselves defer other domains and more sophisticated operators to future work. Precision is reported as the share of program points improved, without an effect size per point. Restarting shows the operator's non-monotonicity cutting both ways: it lost precision at some points and made results incomparable at up to 31% of points in one benchmark.

For KB transfer, the central caution is that every guarantee rests on a partial order in which "bigger" means "admits more behaviours" and on operators with exact algebraic properties. KB claims have no such order, and "widening" and "narrowing" in the KB's notes are metaphors with a reversed direction in the narrowing case. The paper supplies structural precedent and exact vocabulary for the trades; it does not show that any claim-revision loop terminates or preserves truth.

The pdftotext capture dropped the glyphs for the widening, narrowing, and combined operators and flattened the iteration tables and algorithm figures into scattered lines. Formulas involving those operators must be read from context or the PDF; the appended internal note is unattributed working material and should not be cited as the authors' published position.

Recommended Next Action

Add a paragraph of at most 200 words to the "Abstraction must be localized to be auditable" section of generality bought to avoid counterexamples is paid for in precision, citing this ingest as formal precedent. The paragraph would say that abstract interpretation's widening buys termination by spending precision, that propagated loss is generally unrecoverable, and that localized, removable widening points restored precision. It would include one sentence stating that the formal narrowing operator is bounded below by fresh recomputation and runs in the precision-recovery direction, so it is not the subject-narrowing of the companion note.