Three Runs Deep Is Not Deep Enough — Java Bug Hunt

Briefing

Modelled on the TimSort bug found in 2015 by Stijn de Gouw and colleagues while formally verifying the sort used by CPython and OpenJDK: mergeCollapse, which merges runs to restore the run-stack invariant after each new run is pushed, only checked the top three runs. The invariant could therefore break deeper in the stack, and because the size of Java's run stack had been derived from that invariant, a carefully constructed input could overflow it and throw ArrayIndexOutOfBoundsException. CPython adopted the corrected check; OpenJDK enlarged the stack.

This reconstruction models only the run stack: run lengths are pushed and merged, and RunInvariant checks the whole stack.

Fix mergeCollapse so the invariant holds over the whole stack after every push.

Bug report

BUG-TIMSORT-2015 · Priority: High · Reported by: formal verification

The run-stack invariant (RunInvariant.holds, locked) must hold for EVERY position of runLen after each push: runLen[i] > runLen[i+1] + runLen[i+2] and runLen[i] > runLen[i+1]

mergeCollapse() must use the corrected rule, looping while more than one run remains, with n = size - 2:

• if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) || (n > 1 && runLen[n-2] <= runLen[n-1] + runLen[n]): if runLen[n-1] < runLen[n+1] then n = n - 1; mergeAt(n)
• else if runLen[n] <= runLen[n+1]: mergeAt(n)
• else stop

mergeAt(i) replaces runs i and i+1 by their sum and records i in merges.

Example: RunStack.of(120, 80, 25, 20) then push(30) must end as [275] with merges [2, 2, 1, 0].

Observed: that example ends as [120, 80, 45, 30] — 120 <= 80 + 45.

Logs

[sort] run stack [120, 80, 45, 30] violates invariant at depth 0
[sort] java.lang.ArrayIndexOutOfBoundsException in pushRun (run stack sized from the invariant)

The code as shipped

src/sort/RunStack.java (editable)

class RunStack {
    final List<Integer> runLen = new ArrayList<>();
    final List<Integer> merges = new ArrayList<>();

    static RunStack of(int... lens) {
        RunStack s = new RunStack();
        for (int l : lens) s.runLen.add(l);
        return s;
    }

    void push(int len) {
        runLen.add(len);
        mergeCollapse();
    }

    void mergeAt(int i) {
        runLen.set(i, runLen.get(i) + runLen.get(i + 1));
        runLen.remove(i + 1);
        merges.add(i);
    }

    // Merges adjacent runs until the stack invariant is re-established.
    void mergeCollapse() {
        while (runLen.size() > 1) {
            int n = runLen.size() - 2;
            if (n > 0 && runLen.get(n - 1) <= runLen.get(n) + runLen.get(n + 1)) {
                if (runLen.get(n - 1) < runLen.get(n + 1)) n--;
                mergeAt(n);
            } else if (runLen.get(n) <= runLen.get(n + 1)) {
                mergeAt(n);
            } else {
                break;
            }
        }
    }
}

Read-only context: src/sort/RunInvariant.java.