Merge Collapse
Timsort is the sort in Python, in Java, in Android and in 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.
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.
| pushed | stack after | merges |
|---|---|---|
| 1000 | 1000 | 0 |
| 400 | 1000, 400 | 0 |
| 150 | 1000, 400, 150 | 0 |
| 60 | 1000, 400, 150, 60 | 0 |
| 20 | 1000, 400, 150, 60, 20 | 0 |
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 same document is where the failure is recorded, by the author, in his own words: “It worked OK, but it was hard to reason about, and was subtle enough that the intended invariants weren’t actually preserved. Researchers discovered that when trying to complete a computer-generated correctness proof.”
- 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.
| at | lengths | holds |
|---|---|---|
| 0 | 1000 against 400 + 150 = 550 | yes |
| 1 | 400 against 150 + 60 = 210 | yes |
| 2 | 150 against 60 + 20 = 80 | yes |
- 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.
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.