Merge Collapse

Timsort is Python's sort, Java's sort for objects, and the shape behind the sorts in Android and V8. It finds runs of already-ordered elements and keeps a stack of their lengths waiting to be merged, and it maintains an invariant about that stack which keeps the merges balanced. In 2015 a group set out to prove the routine correct and could not, because it is not: it checks the top of the stack and a violation can sit underneath.

New to merging sorted runs? Start here

Two lists already in order can be combined in one pass: look at the front of each, take the smaller, repeat. Real data arrives with stretches already sorted, so a good sort finds those runs and merges them rather than starting from nothing.

Which runs to merge, and in what order, is the whole question. Merging a tiny run into a huge one repeatedly is the expensive mistake, so the algorithm keeps a rule about the sizes it will allow on its stack. This page is about that rule being wrong from 2002, when Timsort was written, until 2015, when a proof attempt found it: thirteen years.

A stack of runs, an invariant, and the place it is not checked

1 Runs, and the stack they are pushed onto

Runs are pushed as they are found. After each push a routine called mergeCollapse merges things until the stack looks acceptable again.

Each push, the stack it produced, and how many merges it took
pushedstack aftermerges
100010000
4001000, 4000
1501000, 400, 1500
601000, 400, 150, 600
201000, 400, 150, 60, 200

2 The invariant the algorithm says it maintains

The invariant is written down in Tim Peters' own description of the algorithm. For the top of the stack: each length must exceed the sum of the two above it, and must exceed the one directly above it.

the first rule
each length exceeds the sum of the two above it
the second
each length exceeds the one directly above it

3 An input that breaks it, constructed rather than found

Now check it everywhere rather than only at the top. The routine looks at the last three entries; this looks at all of them, and that difference is the entire bug.

Each position, the three lengths involved, and whether the rule holds
atlengthsholds
01000 against 400 + 150 = 550yes
1400 against 150 + 60 = 210yes
2150 against 60 + 20 = 80yes
positions where it does not hold
0
how deep the stack got
5

4 The fix, and the second bug that was still in the fix

A stack sized by assuming the invariant holds will overflow when it does not, which is what the 2015 paper reported. The first fix raised the size of the array. The second fix, years later, changed the routine.

Every position satisfies the rule, which is what the algorithm assumes and what it usually gets. A random sequence of runs will not break it, and that is exactly why this survived in several standard libraries for years.

These ran in this browser when the page loaded. Each claim, whether it held, and the number behind it.

Each claim, whether it held, and the values behind it
claimheldmeasured
the 2015 counterexample leaves the invariant violated after 1 of 5 pushesyesfirst at [120, 80, 45, 30] after pushing 30
and the violation sits below the top three, where the routine never looksyesevery violation is at a position the collapse rule does not inspect
a well-behaved sequence keeps the invariant at every pushyes1000, 400, 150, 60, 20 never violates it, so the bug is a hole and not the rule
merging conserves the total length: 275 in, 275 on the stackyesa merge joins two runs into one; if this ever disagreed the sort would be dropping elements
the counterexample's stack never exceeds 4 entries, which is why nothing crashed and nobody noticedyesdeepest 4 on the counterexample and 5 on the well-behaved sequence

What is real here, and what is not

These are run lengths, not an array to be sorted

Nothing here sorts anything. Timsort's difficulty is not the merging, it is the bookkeeping about what to merge and when, so the page shows the stack of lengths and leaves the elements out entirely. A real run of the algorithm would produce these lengths from data; here they are given.

The breaking sequence is given, not discovered

The 2015 paper constructs a family of inputs that violate the invariant, and the numbers here are a small member of that family rather than something this page searched for. That is the honest framing: a random sequence will not find this, which is precisely why the bug survived in several standard libraries for years.

Two fixes, and the page only names them

The immediate response was to make the stack large enough that the overflow could not happen for any possible input, which leaves the invariant broken and papers over it. The routine itself was corrected later. Neither fix is implemented here; the page shows the state the algorithm was in when somebody tried to verify it.

Sources