MIP conflict analysis can walk past the start of a column's bound-change chain: segfault or hang

[EamonHetherton]

MIP conflict analysis can walk past the start of a column's bound-change chain: segfault or hang

Version: the unguarded code below predates v1.15.1 and is unchanged on current latest. Our reproducer input reaches it on latest but not at the v1.15.1 tag (details in Reproducer); whether some other input can reach it on v1.15.1 is unknown, since the loop is unguarded there too and the older compensated comparison only makes the terminal harder to hit, not unreachable.

Intermittent SIGSEGV (or a hang at 100% CPU) during branch-and-bound. Crash stack:

#0 HighsDomain::ConflictSet::resolveLinearLeq   highs/mip/HighsDomain.cpp:3200
     while (relaxUb >= localdom.prevboundval_[locdomchg.pos].first)
#1 explainInfeasibilityLeq → conflictAnalysis → HighsSearch::addBoundExceedingConflict

Observed in production on three model instances (five symbolized crash records: three cores, two kernel-log fault offsets), all on latest-based builds, including at default options (no tolerance override). The same instances sometimes hang at 100% CPU instead (the walk below can cycle through garbage indices rather than fault), and one core shows a second signature consistent with the walk surviving on garbage: a stack position that indexes domchgreason_ out of range, faulting later in explainBoundChange when the reason type indexes cutpoolpropagation.

Cause

A column's bound-change chain terminates with prevboundval_[pos].second == -1. Eight walks of the form

while (relaxUb >= localdom.prevboundval_[locdomchg.pos].first)
  locdomchg.pos = localdom.prevboundval_[locdomchg.pos].second;

assume the terminal is unreachable: HighsDomain.cpp:3046, :3081 (resolveLinearGeq), :3166, :3200 (resolveLinearLeq), and, guarded only by assert(pos != -1) with the comment "pos should never become -1", :3368, :3380 (explainInfeasibilityConflict), :3649, :3662 (explainBoundChangeConflict).

The invariant is numeric and can break under extreme proofs (observed proof rhs down to ≈ 8e-08; objective coefficients spanning 1e-6…2e7; failures seen both at default options and, more readily, at mip_feasibility_tolerance=1e-9). I know this model is badly scaled (HiGHS duly warns about it on load), but the range is inherent to the market rules being modelled and is what I have to work with; hostile numerics should surface as degraded cuts or a warning, not an unbounded memory walk. When the invariant breaks, pos becomes -1 in an optimized build (asserts compiled out), the loop reads prevboundval_[-1] and follows the garbage .second as its next index: wild reads until a fault, a hang, or a poisoned explanation.

Reproducer

Reduced to a single Highs_run: one MPS (anonymised, 3.5 MB) plus the options file, in a driver that does Highs_readModel + Highs_readOptions + Highs_run. On an optimized build of current latest, unmodified, this input hangs at 100% CPU, 10 of 10 runs (killed at 600 s). Under AddressSanitizer, same unmodified source, it deterministically reports heap-buffer-overflow READ of size 8 at HighsDomain.cpp:3200, address 16 bytes before a live allocation, i.e. prevboundval_[-1], on the stack shown above (highs-conflict-walk-reproducer.zip). The official v1.15.1 release does not hit the defect on this input: the released binary completes it, and an ASan build at the v1.15.1 tag (04024d7) runs it with no report. Bisecting v1.15.1..latest with the guarded build as the oracle identifies bce30f0 ("Clean up") as the commit that makes the terminal reachable: it truncates relaxUb/relaxLb from HighsCDouble to double before this comparison, so a hair-below tie at the chain's base value now rounds onto exact equality and the inclusive >= steps past the first entry. The truncation is not the bug; in v1.15.1 the compensated comparison was accidentally protecting an unguarded loop, which is why I propose the structural guard rather than a numeric tweak. Please test against latest, ideally under ASan. A build of latest with the walks guarded solves the input in ~5 s, 10 of 10 runs, identical objective every time.

Replication caveat: the model must round-trip at 17 significant digits. HiGHS's MPS writer emits %.15g, which perturbs the solve path enough to miss the breach; this file was written with a %.17g writer and reproduces deterministically.

Suggested fix

Stop the four relaxation walks at the chain's first entry (keeping it in the explanation, which stays valid as a superset):

while (relaxUb >= localdom.prevboundval_[locdomchg.pos].first) {
  HighsInt prevPos = localdom.prevboundval_[locdomchg.pos].second;
  if (prevPos == -1) break;
  locdomchg.pos = prevPos;
}

and have the four assert-guarded walks return false (conflict cut skipped). Both only forgo optional strengthening. Validated on the full application workload that originally exposed the crash; this is a different, larger model than the reproducer above, solved inside a long-running process, so heap state and therefore the symptom vary run to run (in the bare single-solve driver above the heap is stable and the symptom is too). 10 identical runs per library: unpatched, 10 out of 10 failed (6 SIGSEGV at ~2 min, 4 hangs killed at 25 min); patched, 10 out of 10 ran to completion at the identical optimum, matching the independent reference answer, with ASan/UBSan silent. PR available.

[jajhall]

Thanks for this observation. I guess that one of @fwesselm and @Opt-Mucca will look at it indue course, but performance enhancement is our priority