The invariant that was wrong for seven years

In February 2015, five researchers at Karlsruhe were trying to do something unremarkable: verify Java’s Collections.sort with a program logic. It is a widely used, well-understood, thoroughly tested piece of code, and formal verification of such things is normally a matter of writing down what everyone already knows in a form a tool will accept.

The proof would not go through. They looked at why, and found that it would not go through because the property being proved was false.

Timsort’s merge policy is supposed to keep the stack of pending runs shallow. Java relied on that: it allocated a fixed-size array for the stack, sized from an argument about how deep the invariant permits it to get. De Gouw, Rot, de Boer, Bubel and Hähnle showed that the invariant is not maintained by the code that is supposed to maintain it, produced an input on which the stack overflows the array, and Java threw an ArrayIndexOutOfBoundsException on a call to sort.

The bug had shipped in Python since 2002 and in Java since 2009. It was on every Android phone.

What the invariant is for #

Timsort finds natural runs and pushes them onto a stack rather than merging them immediately. The reason for the stack is that merging in the wrong order is wasteful: merging a run of ten against a run of ten thousand costs a full pass over ten thousand and ten elements to place ten of them. A balanced merge tree does $n\log_2 r$ work; a maximally unbalanced one does $nr/2$.

The stack keeps the merges balanced by maintaining a shape. Writing $A$, $B$, $C$ for the three runs nearest the top with $A$ deepest, the intended invariant is

$$|A| > |B| + |C| \qquad\text{and}\qquad |B| > |C|.$$

The runs grow at least as fast as Fibonacci numbers going down the stack, so a stack of depth $d$ requires at least $F_d$ elements, so the depth is $O(\log n)$. That is the argument, and it is correct — given the invariant.

The rule that is supposed to maintain it, in the form CPython shipped and Java copied, is short. Look at the top three entries. If the deepest of them is not larger than the sum of the other two, merge. Otherwise, if the middle one is not larger than the top one, merge. Otherwise stop.

Two clauses, both looking at three entries, and the whole of the maintenance.

Why three is not enough #

The failure is easy to state once it has been seen. A merge changes the size of an entry, and the new size can violate the invariant against entries the rule never looks at.

Merging the top two entries of a stack of five leaves four, and the new top entry is the sum of two old ones. The rule then re-examines the top three of the four — positions 2, 3 and 4 — and never checks whether position 1 is still large enough relative to the new position 2. If it is not, the loop exits with the invariant broken, and it stays broken, because the loop only ever runs after a push and the check only ever looks at the top.

The fix Java adopted in 2015 is one extra clause: also merge if the fourth entry from the top is not larger than the sum of the two below it. That is the version labelled “four-entry rule” throughout this site’s code, and it is the version that collapses the counterexample.

The smallest counterexample #

The published counterexample uses run lengths 120, 80, 25, 20, 30 — 275 elements. This site’s own search finds a smaller one.

The policy can be studied without any data at all, because it consumes run lengths and produces a stack. mergeCollapsePolicy takes a list of lengths and returns the stack, and checks whether the invariant holds over the whole of it rather than over its top. So the search space is sequences of integers, not permutations of arrays, and it is small enough to enumerate.

Searching by increasing total, over three to six runs, the first sequence that the three-entry rule mishandles and the four-entry rule does not is:

$$14,\ 10,\ 3,\ 2,\ 4$$

Thirty-three elements. Every sequence of fewer than thirty-three elements, in any number of runs from three to six, leaves the stack in a state the invariant accepts. That search runs on every build — it examines 1,186,775 sequences and takes about a fifth of a second — because a constant nobody can reproduce is exactly the sort of thing this site does not print.

Following it through, with the stack written bottom-first:

At the last push both rules merge 3 and 2 into 5, because 3 is not greater than 2 + 4. The three-entry rule then examines 10, 5, 4: is 10 greater than 5 + 4? Yes, 10 > 9. Is 5 greater than 4? Yes. Stop.

And 14 is not greater than 10 + 5. The invariant is broken at the bottom of a four-entry stack, and the rule has already stopped looking.

The four-entry rule asks one more question — is the fourth entry, 14, greater than 10 + 5? — gets no, merges, and cascades to a single run of 33.

Both of them sort #

This is the part that matters most and it is easy to skip past.

Feed the counterexample to a real Timsort with the three-entry rule. The array comes out correctly sorted. Feed it the four-entry rule: correctly sorted. Feed it a policy that never merges anything until the very end: correctly sorted. Feed it any policy at all, and provided the final forced collapse merges everything, the output is right.

The merge policy does not affect correctness. It affects how much work is done and how deep the stack gets, and neither of those is visible in the output.

That is the essay’s whole point and it is the reason this defect survived for seven years across two languages. Every test that anybody would naturally write — sort this array, check it is sorted; sort a million random arrays, check they are sorted; sort with duplicates, check stability — passes. The comparison count barely moves. Only a check on the policy itself can see it, and nobody wrote one until somebody tried to prove the thing.

The site’s own gate makes both halves explicit. assertABrokenPolicyStillSorts requires the three-entry rule to leave the invariant broken and the output to be perfectly sorted, because that combination is what lets a defect survive every check. assertTheFourEntryRuleHoldsWhereTheThreeDoesNot requires the other rule to handle the same input. Neither is a test of correctness; both are tests of a property that correctness cannot reach.

Checking the machinery against the literature rather than against itself #

A search that finds a counterexample proves that the code being searched has a property. It does not prove that the code being searched is Timsort’s merge policy.

That distinction has bitten this site before — the pattern that defeats the pattern records an implementation that omitted one branch of pdqsort and measured as a bad algorithm rather than as a partial one. A merge policy is even easier to get subtly wrong, because almost any policy sorts.

So the published counterexample is checked as well as the found one. assertTheKnownBreachAgrees runs the lengths 120, 80, 25, 20, 30 through this site’s policy and requires the three-entry rule to break and the four-entry rule to hold. If the implementation had drifted — a comparison the wrong way round, an index off by one — it would very likely still find some counterexample by search, and it would not agree with the paper’s.

That is the general shape of the check and it is worth naming: a search that agrees with itself proves nothing; a search whose answer agrees with an independently published one is evidence about the machinery. The same reasoning is why the site’s information-theoretic floors are checked against Stirling’s approximation rather than only against measured sorts.

What actually broke #

The invariant being false does not by itself crash anything. What crashed was a consequence of it.

Java allocated the run stack as a fixed array, and sized it using a table derived from the invariant: for arrays under 120 elements, 5 entries; under 1,542, 10; under 119,151, 24; otherwise 49. Those numbers come from the Fibonacci argument, which depends on the invariant holding.

With the invariant broken the stack can grow deeper than the argument allows, and on a sufficiently large constructed input it overflows the array. java.lang.ArrayIndexOutOfBoundsException from inside Collections.sort, on a perfectly ordinary call, with no way for the caller to have done anything wrong.

Python did not crash, because CPython grows its run stack dynamically and had allocated 85 slots where the argument called for far fewer. The invariant was equally broken; the consequence was bounded by a defensive allocation nobody had thought of as defensive.

Two implementations of the same algorithm with the same defect, and one of them was a crash and the other was nothing at all, decided by an unrelated choice about memory management. That is worth sitting with. The bug’s severity was not a property of the bug.

The two fixes, and which one was chosen #

There were two ways out and both were proposed.

Fix the invariant maintenance — add the fourth-entry clause, restore the property, keep the stack-size table. This is what Java did.

Fix the stack size — leave the rule alone and allocate enough entries for the worst case the actual rule permits, which the paper computed. This is what Python did.

Neither is obviously right. Java’s restores the intended shape and keeps the merges balanced, at the cost of occasionally merging when the old rule would not have. Python’s leaves a policy that is known not to maintain its stated invariant and makes the consequence harmless.

The second is a more uncomfortable engineering decision than it looks, and it is defensible: the invariant exists to bound the stack depth, the bound was recomputed for the real rule, and the depth is bounded. What is lost is the reason to believe — the property that made the code reviewable is gone, replaced by a number from a proof about a specific implementation.

What a broken policy costs, when it costs anything #

The severity question deserves a measurement rather than a shrug, because “the array still sorts” can be read as “it does not matter”.

A merge policy that abandons the invariant does more work, and the amount is bounded by how unbalanced the merges get. The extreme case is a policy that never merges until the end, which then merges the runs in a single left-to-right sweep — the maximally unbalanced tree.

Run the counterexample’s shape at scale and the two rules differ by four merges against four merges — identical work, different stack. Run either on ordinary input and the stacks are the same depth and the merge counts are the same. The measured cost of the defect, on everything short of a constructed input, is zero.

Which is exactly what made it survivable and exactly what makes it interesting. A defect with a measurable cost gets found by benchmarking. A defect whose only symptom is that a stack array can overflow at a size nobody reaches by accident gets found by a proof or not at all.

Five runs is provable; thirty-three is what the search adds #

The search enumerates over three to six runs and reports a five-run answer, which invites the question of whether five was found or forced. It was forced, and the argument is short enough to give — which matters, because it says what the search is actually contributing.

The three-entry rule inspects the top three entries. For it to leave a violation, the violation has to be somewhere it never looks: at the fourth entry from the top. So the final stack must have at least four entries.

Now suppose no merge ever happened. Then the stack is the runs exactly as pushed, and every adjacent triple was checked at the moment its top was pushed, and nothing has changed any size since. Whatever was true when a triple was examined is still true. A stack that has never merged cannot be in violation, so at least one merge must have occurred, so at least five runs were pushed to leave four behind.

Five is therefore the minimum by construction. What the search supplies is the total: among all five-run sequences, and among six-run ones too, thirty-three elements is the smallest that does it. That is a genuinely searched number and it is the one worth printing.

The same argument bounds the other end of the enumeration. The invariant forces the sizes to grow at least like Fibonacci numbers going down the stack, so a deeper intermediate stack needs more elements, and a seven-run sequence cannot have a smaller total than a five-run one. Three to six is not an arbitrary window; it brackets the answer on both sides for a reason.

Which leaves the arithmetic that turns thirty-three elements into an array a real sort would exercise, and it is a fixed point rather than a multiplication.

Every run has to exceed minrun, or the run extension pads it and the ratios are destroyed. The smallest run in the counterexample is 2, so the scale factor must be at least minrun/2 — and minrun is itself computed from the array’s length, which is thirty-three times the scale factor. The smallest array that demonstrates the defect through a real Timsort is the solution of a small circular constraint, not a number anybody would guess, and it lands at 1,056 elements with the runs at 448, 320, 96, 64 and 128.

That is the sharpest available statement of why seven years was possible. The defect needs five runs in a specific ratio, every one of them above a threshold that depends on the array’s total length, in an array of about a thousand elements — and the five input kinds this collection uses produce either one run or runs that minrun immediately flattens to a uniform size. The counterexample is not rare in the space of arrays; it is rare in the space of arrays anybody generates, and the constant that makes it so is the same threshold somebody chose that the rest of Timsort’s behaviour turns on.

What the policy is for is easier to see on a whole sort than on the five runs that break it, and the two rules are drawn over the same input so the difference is the rule and nothing else.

What this site takes from it #

Three things, and the first is about this site rather than about Timsort.

A correctness check is not a check. Every algorithm in this collection is verified by run() confirming that the output is sorted, and that check has caught more implementation mistakes here than everything else combined. It cannot see a policy. The practice field’s algorithms are the first ones on this site where the output does not determine whether the code is doing what it says, and every one of them needed an assertion on its internal state as well as its result.

Seven years is not long for this class of defect. The invariant was published, the code was open, the algorithm was on every phone, and the property was still false. It was not found by testing, by review, by fuzzing or by use. It was found by someone trying to write down precisely what the code guarantees, in a form that does not permit hand-waving, and failing.

The counterexample is thirty-three elements. Not a pathological million-element construction, not something requiring an adversary with the source — five short runs, an array smaller than a screenful, discoverable by enumerating sequences of small integers in a fifth of a second. It was reachable the whole time by anybody who had thought to look for it, and the reason nobody looked is that there was no reason to think the property was false.

That figure is worth one more sentence, because it answers the obvious objection. If the counterexample is only thirty-three elements, why did random testing never find it? Because minrun pads every short run: an array of thirty-three elements is sorted entirely by binary insertion and the merge policy never runs at all. To exercise the policy with these ratios the runs must all exceed minrun, which means the smallest array that demonstrates the defect through a real Timsort is 1,056 elements with run lengths in the exact ratio 14 : 10 : 3 : 2 : 4 — and the chance of a random array of a thousand elements having that structure is nil.

The counterexample is small and the inputs that contain it are not random. Both halves are needed to explain seven years.

Which leaves the honest closing note. The three-entry rule handles random data, sorted data, nearly sorted data and everything else this site can construct without a search. It is wrong in the sense that it does not imply what it claims, and correct in the sense that almost nothing ever notices. Whether that combination is a bug is a question about what a guarantee is for — and the answer this collection keeps arriving at is that a guarantee nobody has tested is a sentence, and a sentence is what fails silently.