4 ms·

Their corrected version: if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1] || n-1 > 0 && runLen[n-2] <= runLen[n] + runLen[n-1]) In the first clau

Their corrected version: if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1] || n-1 > 0 && runLen[n-2] <= runLen[n] + runLen[n-1]) In the first clause they add earlier to later runLen elements, but in the second they add later to earlier elements. Switching the order just makes the expression harder to understand, like reusing variables within a scope. Addition is commutative and there's nothing technically wrong with it, but this construction makes it appear like there may be something special about element n when there's not. The programmer also has to do mental arithmetic to check the bounds. Bounds checks can be written so that the largest index subtracted is also the value tested: if (n >= 1 && runLen[n-1] <= runLen[n] + runLen[n+1] || n >= 2 && runLen[n-2] <= runLen[n-1] + runLen[n]) This makes it easier to see that the bounds are correct. Formal methods found an important bug that would not have been found otherwise, but a lot of lesser bugs can be prevented just by writing clear and consistent code.

jonahx 12y ago
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"?
- stonemetal 12y ago
  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?
  - tomp 12y ago
    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).
    - stonemetal 12y ago
      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.
      - saidajigumi 12y ago
        > 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.
    - qznc 12y ago
      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.
- maxerickson 12y ago
  To me, https://mail.python.org/pipermail/python-dev/2002-July/026897.html 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.
  - bradleyjg 12y ago
    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.
    - ericfrederich 12y ago
      4.5 petabytes of RAM... that's what swap is for.
    - kragen 12y ago
      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”.

jonahx 12y ago

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"?

stonemetal 12y ago
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?
- tomp 12y ago
  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).
  - stonemetal 12y ago
    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.
    - saidajigumi 12y ago
      > 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.
  - qznc 12y ago
    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.
maxerickson 12y ago
To me, https://mail.python.org/pipermail/python-dev/2002-July/026897.html 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.
- bradleyjg 12y ago
  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.
  - ericfrederich 12y ago
    4.5 petabytes of RAM... that's what swap is for.
  - kragen 12y ago
    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”.