Hacker News Reader

Comment by jonahx | Hacker News Reader

Question: Formal methods found the bug, but now that we know about it, what lessons can human programmers learn? That is, in the spirit of "20/20 hindsight," can we see the false assumption that made the bug possible as an instance of a certain kind of mistake, which we can look for and avoid in the future?

Or do you think the only lesson here is "Never fully trust anything that hasn't been formally verified"?

View on HN

To me, https://mail.python.org/pipermail/python-dev/2002-July/02689... reads like the bug was known (err, the possibility of running out of slots in the bookkeeping stack was understood). That indicates that it could be an intentional tradeoff.

The source code for the python version has this comment:

  /* The maximum number of entries in a MergeState's pending-runs stack.
  * This is enough to sort arrays of size up to about
  *     32 * phi ** MAX_MERGE_PENDING
  * where phi ~= 1.618.  85 is ridiculouslylarge enough, good for an array
  * with 2**64 elements.
  */

According to the linked article that's incorrect, it is only good enough for an array with 2^49 elements. So, if the (implicit) design guarantee is for lists up to 2^64, the implementation is technically bugged. But it'd be pretty hard to run into it in practice. 2^49 of python's plain integers consume more than 4.5 petabytes of RAM.

4.5 petabytes of RAM... that's what swap is for.

2⁴⁹ item references in a Python list will consume about 2⁵² bytes of RAM on an LP64 system, which is 4 pebibytes (4.5 petabytes, as you said). You might also need to allocate space for the objects that the references refer to, which will almost certainly be bigger. I don’t understand the bug well enough to know if it will work with large numbers of duplicate/identical items.

Nitpick: the idiomatic term is “buggy”, not “bugged”. Something is “bugged” if it has a hidden microphone in it transmitting to spies, not if it contains a software “bug”.

I would say both are correct. From a psychological\SE standpoint know your faults and develop defenses for them. That could be use a language that doesn't allow them to even be thought in the first place, or develop defensive coding standards that prevent them. But that answer is more stochastic, it helps but anything short of formal proof is just raising the likely hood of success not a guarantee.

I also wonder if a static analysis tool would have caught the bug. Are there any good static analysis tools for Java or Python that might have caught the bug without the overhead of writing the formal proof?

As I understand, they didn't write a formal proof, but only the pre- and post-conditions, along with loop invariants. The formal proof was then completed by automatic theorem provers.

There has been some research into contracts inference, but with very limited results. Even if you added all the pre- and post-conditions manually, I'm not sure loop invariants could be inferred (especially as they can get pretty complex).

True, I more meant their method required O(n) effort since they had to write pre\post conditions and invariant for the tool. Whereas something like codeSonar or PVS Studio requires O(1) effort, just point it at your build and press go. The bug they found was an implementation defect, something I believe the low effort tools would have caught. Where their tool should shine would be in detecting something the low effort analysis tools miss.

> something I believe the low effort tools would have caught.

It's worth noting that the formal verification method brought to light the root cause, where prior attempts at fixing this bug in TimSort had merely made it less common.

Would codeSonar or PVS Studio actually have provided the insight, in "O(1)", required to fix the root cause? I'm not familiar with those tools, but I sincerely doubt it.

Working with KeY is similar to writing a proof. The development of pre-, post-conditions and invariants is done interactively with the theorem prover, which shows you what is missing.

Reply on news.ycombinator.com