12 ms·

Proving that Android’s, Java’s and Python’s sorting algorithm is broken

608 points by amund 12y ago

imaginenore 12y ago
And I always thought sort functions are always tested with millions of randomly generated sequences and the results are compared with the results of other implementations known to be good.
- thomasahle 12y ago
  Very often random sequences are very different from sequences encountered in the wild.
- TillE 12y ago
  As long as your < operator works, you don't really need another sort implementation to compare with. Also, it seems like the bug is only truly present in the Java version due to a slightly different implementation, even though the original Python (and the "fixed" Java) is technically incorrect.
  - imaginenore 12y ago
    > As long as your < operator works That's not true. sort() can be broken in many different ways. For instance sort([3, 7, 5]) -> [1, 2, 3] The result it sorted and has the correct length, but it's wrong.
    - lmm 12y ago
      The parametricity (edit: thanks imaginenore, I misremembered the name) theorem implies that a generic sort function written in a safe subset of the language could never do that though.
      - Robin_Message 12y ago
        Is that the idea that since the code should neither invent new values, nor duplicate values, it will always end up returning a permutation? It seems like inventing values not being possible is fine, but duplicating a value seems very plausible - what safe subset of Java would ensure that doesn't happen?
        lmm 12y ago
        Maybe http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#linear-checker http://types.cs.washington.edu/checker-framework/current/che... ? (I've used other parts of the checkers framework, but not that one yet)
      - imaginenore 12y ago
        The parameterization theorem doesn't imply such thing. http://en.wikipedia.org/wiki/Smn_theorem http://en.wikipedia.org/wiki/Smn_theorem
        Chinjut 12y ago
        That's different from what is being referred to, which is (very briefly) described at http://en.wikipedia.org/wiki/Parametricity#History http://en.wikipedia.org/wiki/Parametricity#History. Edit: Ah, I didn't realize that there was an edit involved in the post you were referring to. At any rate, things are hopefully now clear to all.
    - fnord123 12y ago
      Terasort handles this by taking a sum of md5sums for each value. The teravalidate program then checks that all the items are in order and that the checksum is the same. It's so unlikely that could generate data that passes teravalidate but not really be correct that it would probably be an important work of computational science in it's own right.
- dagw 12y ago
  Sure, but what is the probability that you generate exactly the type of sequence needed to trigger this bug.
- maxerickson 12y ago
  That was done. It's talked about here: http://svn.python.org/projects/python/trunk/Objects/listsort.txt http://svn.python.org/projects/python/trunk/Objects/listsort... The bug would only be triggered by generating a truly massive array (the implementation mentions that it will work for up to 2^64 elements: http://svn.python.org/projects/python/trunk/Objects/listobject.c http://svn.python.org/projects/python/trunk/Objects/listobje... search for MAX_MERGE_PENDING).
  - e12e 12y ago
    As mentioned by another commenter, the bug is that it's (for python) documented to work for 2^64 elements, but "only" works for 2^49. 2^49 is still pretty big... note that for 64-bit integers, 2^49 integers is 2^(49+3)=2^52 bytes... or 4 petabytes of raw data. Even if you're sorting single bits (one and zero) it's quite a bit of data to chew through. [ed: Hm, that's not quite right. A 64-bit integer is 2^6, so that should be 2^(49+6)=2^55, or 32 petabytes). I think :-) ]
mkesper 12y ago
From the article: The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space. Given the astronomical number of program runs that such a central routine is used in, this leads to a considerable waste of energy.
- tveita 12y ago
  It looks like the Python version that's good for 2^49 items uses 1360 bytes for this array, allocated on the stack. I wouldn't worry about an extra couple of bytes nearly as much as I would worry about changing the behaviour of a function used in an "astronomical number of program", so this looks like a pretty reasonable and conservative choice, at least for an immediate patch.
  - deleted 12y ago
    [deleted]
  - krick 12y ago
    Does it "change behavior"? As far as I understand, the only change is that this test wouldn't crash anymore. Which certainly is "changing the behavior", but allocating more memory is as well. If so, I don't see any reason not to use formally verified version. Not that it is really important, but quite reasonable.
- xamuel 12y ago
  Java: Turning "reasonable data, should fit in RAM" into "Big Data (tm)" since 1995
  - collyw 12y ago
    I thought it was nodejs evangelists that did that.
    - 12y ago
andrewstuart2 12y ago
I'm surprised that modern implementations don't use something like quicksort, since it has linear space requirements (sorts in-place) and good constants on average for its n*log2(n) running time.
- irascible 12y ago
  TimSort is supposed to have better performance on real world datasets.
  - gus_massa 12y ago
    Agree. More info: http://en.wikipedia.org/wiki/Timsort http://en.wikipedia.org/wiki/Timsort The original mail with the proposal is: http://bugs.python.org/file4451/timsort.txt http://bugs.python.org/file4451/timsort.txt
- Arnt 12y ago
  Quicksort has poor worst-case behaviour, so it's easy to carry out a DoS attack on network services that use it. Language maintainers don't like restricting their library to input from friendly users, at least not when there are other algorithms that work reasonably with unfriendly input.
  - jonesetc 12y ago
    Isn't the malicious attack fought by just picking a random pivot?
    - Freaky 12y ago
      There are still inputs that will make it go quadratic, that just obscures it slightly. A proper fix is to fall back on a different sort if it looks like quicksort is doing that: https://en.wikipedia.org/wiki/Introsort https://en.wikipedia.org/wiki/Introsort
      - thaumasiotes 12y ago
ujjwal_wadhawan 12y ago
Spark 1.1 switched default sorting algorithm from quicksort to TimSort as well in both the map and reduce phases- https://databricks.com/blog/2014/10/10/spark-petabyte-sort.html https://databricks.com/blog/2014/10/10/spark-petabyte-sort.h...
thomasahle 12y ago
This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn't seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions. Really shines as an example of how important proof is in computer science.
- stingraycharles 12y ago
  In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions. I am not sure why these kind of testing methods aren't used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive. [1] https://wiki.haskell.org/Introduction_to_QuickCheck2 https://wiki.haskell.org/Introduction_to_QuickCheck2 EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn't making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.
  - im3w1l 12y ago
    It wouldn't catch this bug. The algorithm works for lists of size less than 2^49.
  - jdimov 12y ago
    There is triq[1] for Erlang and excheck[2] for Elixir. [1] https://github.com/krestenkrab/triq https://github.com/krestenkrab/triq [2] https://github.com/parroty/excheck https://github.com/parroty/excheck
  - Osmium 12y ago
    Just FYI for anyone who's interested, but there's a Swift implementation of QuickCheck described in this book: http://www.objc.io/books/ http://www.objc.io/books/ It's very minimal, but the chapter outlines what you'd need to do to make it more complete and get it on par with the Haskell version. There are also a few versions on GitHub too.
inglor 12y ago
This is an excellent use case of formal verification. I can definitely see the merit in using tools like this in my code. They mention KeY http://www.key-project.org/ http://www.key-project.org/ . Is anyone using this here? Are there any good resources on it except for the official site (and this blog post)?
- amund 12y ago
  Hi, I will ask the authors of the blog post and corresponding academic paper about additional KeY resources and follow-up.
  - inglor 12y ago
    Thanks and thanks for the interesting read. I've been looking for real uses of formal verification for a long time. I've played a lot with code contracts in C# and I've played some with languages like Eifel - the advantage of this approach is that it's static and it performs actual proof rather than enforcement. These forms of formal verification could really help with building robust software and if someone makes them easy enough to use I can definitely see them as useful alongside if not instead of unit tests.
- deleted 12y ago
  [deleted]
- iso8859-1 12y ago
  It is in use for undergraduate courses in the universities that develop it, and I used it too. It ships with small training problems. What would you like to know? There are many documents on JML. The prover works for you, you just left click logic expressions in KeY and you can prove large parts by point-and-click. It can also finish proofs for you if it's trivial. Often, you only need to specify the loop invariants. I'd recommend opening up KeY, loading one of the trivial examples first: Contraposition. This will be a quick reminder on the logic concepts like implication, but you pretty much cannot screw it up. Try to understand why the proof tree branches when you choose certain steps. Afterwards, try something else from "Getting started" like the examples that the proof searcher can prove (for example SumAndMax) and exploring the proof tree, and trying out yourself from scratch. The automatic proofs are not always pretty, so it's more for to do the manual work first. KeY will only let you do valid proof steps, so you learn quickly how proofs work.
RubyPinch 12y ago
anyone know the list of bugs for this? https://bugs.openjdk.java.net/browse/JDK-8072909 https://bugs.openjdk.java.net/browse/JDK-8072909 It seems they havn't submitted to any other trackers, which is a bit unfortunate
- vstolz 12y ago
  There is also http://bugs.java.com/view_bug.do?bug_id=8011944 http://bugs.java.com/view_bug.do?bug_id=8011944, where IIUC the suggested "fix" was to use a VM switch to enable the old (and slower) sorting...
bsdetector 12y ago
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?
    - 12y ago
noahl 12y ago
Just a nitpick, but the article makes a mathematical mistake. In the last paragraph of section 1.2, it says For performance reasons, it is crucial to allocate as little memory as possible for runLen, but still enough to store all the runs. *If the invariant is satisfied by all runs, the length of each run grows exponentially (even faster than fibonacci: the length of the current run must be strictly bigger than the sum of the next two runs lengths).* However, fibonacci growth is strictly faster than exponential. In fact, this is why n * log(n) is the lower bound on the number of comparisons a comparison-based sorting algorithm must use: because n! is approximately n * log(n).
- robrenaud 12y ago
  > fibonacci growth is strictly faster than exponential. This is wrong. The easiest intuition for why this is true that I can come up with is that next Fibonacci number is no bigger than double the previous, and so fib(n) <= 2^n.
- anonymoushn 12y ago
  Fibonacci is n(i) = n(i-1) + n(i-2). Factorial is n! = n * n-1 * n-2 * ... * 2 * 1. In the second sentence, you might have wanted "lg(n!) is approximately n lg n". That would be a good reason for needing n lg n comparisons to distinguish between the n! permutations. I have edited this comment as my understanding of the parent comment developed >_>
  - noahl 12y ago
    Thanks for pointing this out! Yes, I meant log_2(n!) is approximately n*log_2(n). I appreciate you spotting the error. :-)
- deleted 12y ago
  [deleted]
- bladedtoys 12y ago
  Fibonacci( n ) = ( P^n - ( -P )^-n ) / sqrt(5) Where P is Golden ratio ( about 1.618 ) So yes it resembles exponential growth but as you can see it is slightly less due to the "- ( -P )^-n" part.
wheaties 12y ago
Wish they'd put that up on Github or Bitbucket. There are so many things to be learned from that. I don't want to just download things or just use a tool (although it's pretty awesome that they made the tool available.)
- vstolz 12y ago
  What are you looking for?
  - wheaties 12y ago
    To watch how change sets are going into the tool. To see what is being done and why as it happens. I find that one of the best ways to learn these things. Especially when it is theory heavy and watching the implementation congele around the theoretical framework.
    - vstolz 12y ago
      Sorry to keep following up, but we'd really like to know what we can improve -- into which tool? Are you talking about the KeY tool, or the various libraries they are now catching up on this issue?
    - emmelaich 12y ago
      Looks like there is a clone on bitbucket, but it hasn't been updated in a while. https://bitbucket.org/adoptopenjdk https://bitbucket.org/adoptopenjdk
bglazer 12y ago
Has anyone used the KeY project in industry? I'd certainly prefer proofs over unit tests. However, I don't understand formal proof systems sufficiently well to know whether these they would work in terms of your typical "app" that makes RPC calls, DB changes, and generally has lots of moving parts and statefulness.
- rwmj 12y ago
  I have tried to use Coq and Frama-C to prove commercial OCaml and C programs, without, it has to be said, any success. I'm waiting for someone to write the brilliant tutorial.
  - dhekir 12y ago
    You're waiting for a tutorial on Coq integrated with Frama-C, or for a tutorial on any of them?
    - rwmj 12y ago
      I'm waiting for a tutorial on how to prove correctness of either OCaml or (especially) C code in real programs.
      - vstolz 12y ago
        It is possible, see e.g. http://ssrg.nicta.com.au/projects/TS/ http://ssrg.nicta.com.au/projects/TS/, though it's not really the tutorial you've been hoping for.
      - dhekir 12y ago
        Research tools are getting closer to what people consider "real" programs, even if they often focus on embedded systems software. CompCert already deals with a quite large subset of C. Frama-C can deal with most if not all syntactic features of C, but then the next challenge is the C standard library, e.g. specifying every useful function (and even "simple" ones such as memcpy can be quite tricky). Afterwards, you have to deal with the glibc, then other high-level libraries, etc... Most of these tools are either still in a mostly-academic setting (where "documentation = conference paper"), or do not have enough funding to pay for the development of more user-friendly features and extensive documentation. But with the ever-increasing security issues receiving media attention lately, we can hope more funding will allow these tools to reach a more mainstream status. By the way, could you give an example of a small program that you would consider "real"? Just to have an idea of its size and complexity.
jordigh 12y ago
Oh, crap. I suppose this also means we have the bug in our GNU Octave implementation: http://hg.savannah.gnu.org/hgweb/octave/file/0486a29d780f/liboctave/util/oct-sort.cc http://hg.savannah.gnu.org/hgweb/octave/file/0486a29d780f/li... Well, time to patch it there too.
ericfrederich 12y ago
Where can I get that PS1 from the shell in the video? It appears to have a green check mark if the previous command returned 0 otherwise some red symbol. Looks cool
- protomyth 12y ago
  for bash http://stackoverflow.com/questions/16715103/bash-prompt-with-last-exit-code http://stackoverflow.com/questions/16715103/bash-prompt-with...
- thedufer 12y ago
  The default oh-my-zsh theme does something similar - first character in the PS1 is `➜`, in grey if the previous command returned 0, red otherwise. It just checks `$?`, I assume.
ezyang 12y ago
Everyone here is talking about Timsort, but you should also check out the materials they've published about the KeY project, which they used to carry out this verification. http://www.key-project.org/~key/eclipse/SED/index.html http://www.key-project.org/~key/eclipse/SED/index.html describes their "symbolic execution debugger", which lets you debug any Java code even if you don't know all the inputs (by simply taking the input as a symbolic value). The screencast is very accessible.
nichochar 12y ago
This is bad-ass. Thanks for taking the time and investigating something that so many overlook yet use every day (myself included)
Animats 12y ago
Nice. As usual, entry and exit conditions aren't that hard to write; it's loop invariants that are hard. /*@ loop_invariant @ (\forall int i; 0<=i && i<stackSize-4; @ runLen[i] > runLen[i+1] + runLen[i+2]) @ && runLen[stackSize-4] > runLen[stackSize-3]) @*/ It's surprising how close their notation is to our Pascal-F verifier from 30 years ago.[1] Formal verification went away in the 1980s because of the dominance of C, where the language doesn't know how big anything is. There were also a lot of diversions into exotic logic systems (I used to refer to this as the "logic of the month club"). The Key system is back to plain old first-order predicate calculus, which is where program verification started in the 1970s. For the invariant, you have to prove three theorems: 1) that the invariant is true the first time the loop is executed, given the entry conditions, 2) that the invariant is true for each iteration after the first if it was true on the previous iteration, and 3) that the exit condition is true given that the invariant is true on the last iteration. You also have to prove loop termination, which you do by showing that a nonnegative integer gets smaller on each iteration. (That, by the way, is how the halting problem is dealt with in practice.) #2 is usually the hardest, because it requires an inductive proof. The others can usually be handled by a simple prover. There's a complete decision procedure by Oppen and Nelson for theorems which contain only integer (really rational) addition, subtraction, multiplication by constants, inequalities, subscripts, and structures. For those, you're guaranteed a proof or a counterexample. But when you have an internal quantifier (the "forall int i") above, proof gets harder. Provers are better now, though. A big practical problem with verification systems is that they usually require a lot of annotation. Somebody has to write all those entry and exit conditions, and it's usually not the original programmer. A practical system has to automate as much of that as possible. In the example shown, someone had to tell the system that a function was "pure" (no side effects, no inputs other than the function arguments). That could be detected automatically. The tools have to make the process much, much easier. Most verification is done by people into theory, not shipping products. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf
tenfingers 12y ago
This is a good example of why formal verification is incredibly useful. I tried to invest some time in learning some of the proof verification languages and tools, but so far I wasn't too successful. It looks like that to formulate a proof, I always have to rewrite the algorithm/problem first in the tool's language, which is often not easy. I could see myself making mistakes in writing the proof just as well as I do when I'm programming. Proof validation is also tricky. Coq isn't fully automatic as I initially was expecting. I actually used "prover9" which is first-order only, but does automatic validation. I guess Coq is really useful when you need to understand the proof and interactive validation can guide you, whereas prover9 could help with automation. The thing is, it's still too much work, even for seemingly simple algorithms, to write a proof in either system in order to improve on the current situation of unit testing (that is: if I wanted to get something with more intrinsic value than a test case). Formally verified languages are nice, but for a gazillion of reasons you still need to verify what's running currently.
- vstolz 12y ago
  With tools like Coq, you may even have the benefit of extracting an implementation from your proof! Some assembly may be required though, and extraction only works to functional languages.
maxerickson 12y ago
Fixed in python: http://bugs.python.org/issue23515 http://bugs.python.org/issue23515
amund 12y ago
The authors have posted a follow-up posting: about KeY - the tool used to prove the bug in TimSort - http://envisage-project.eu/key-deductive-verification-of-software/ http://envisage-project.eu/key-deductive-verification-of-sof...

608 points by amund 12y ago

And I always thought sort functions are always tested with millions of randomly generated sequences and the results are compared with the results of other implementations known to be good.

thomasahle 12y ago
Very often random sequences are very different from sequences encountered in the wild.
TillE 12y ago
As long as your < operator works, you don't really need another sort implementation to compare with. Also, it seems like the bug is only truly present in the Java version due to a slightly different implementation, even though the original Python (and the "fixed" Java) is technically incorrect.
- imaginenore 12y ago
  > As long as your < operator works That's not true. sort() can be broken in many different ways. For instance sort([3, 7, 5]) -> [1, 2, 3] The result it sorted and has the correct length, but it's wrong.
  - lmm 12y ago
    The parametricity (edit: thanks imaginenore, I misremembered the name) theorem implies that a generic sort function written in a safe subset of the language could never do that though.
    - Robin_Message 12y ago
      Is that the idea that since the code should neither invent new values, nor duplicate values, it will always end up returning a permutation? It seems like inventing values not being possible is fine, but duplicating a value seems very plausible - what safe subset of Java would ensure that doesn't happen?
      - lmm 12y ago
        Maybe http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#linear-checker http://types.cs.washington.edu/checker-framework/current/che... ? (I've used other parts of the checkers framework, but not that one yet)
    - imaginenore 12y ago
      The parameterization theorem doesn't imply such thing. http://en.wikipedia.org/wiki/Smn_theorem http://en.wikipedia.org/wiki/Smn_theorem
      - Chinjut 12y ago
        That's different from what is being referred to, which is (very briefly) described at http://en.wikipedia.org/wiki/Parametricity#History http://en.wikipedia.org/wiki/Parametricity#History. Edit: Ah, I didn't realize that there was an edit involved in the post you were referring to. At any rate, things are hopefully now clear to all.
  - fnord123 12y ago
    Terasort handles this by taking a sum of md5sums for each value. The teravalidate program then checks that all the items are in order and that the checksum is the same. It's so unlikely that could generate data that passes teravalidate but not really be correct that it would probably be an important work of computational science in it's own right.
dagw 12y ago
Sure, but what is the probability that you generate exactly the type of sequence needed to trigger this bug.
maxerickson 12y ago
That was done. It's talked about here: http://svn.python.org/projects/python/trunk/Objects/listsort.txt http://svn.python.org/projects/python/trunk/Objects/listsort... The bug would only be triggered by generating a truly massive array (the implementation mentions that it will work for up to 2^64 elements: http://svn.python.org/projects/python/trunk/Objects/listobject.c http://svn.python.org/projects/python/trunk/Objects/listobje... search for MAX_MERGE_PENDING).
- e12e 12y ago
  As mentioned by another commenter, the bug is that it's (for python) documented to work for 2^64 elements, but "only" works for 2^49. 2^49 is still pretty big... note that for 64-bit integers, 2^49 integers is 2^(49+3)=2^52 bytes... or 4 petabytes of raw data. Even if you're sorting single bits (one and zero) it's quite a bit of data to chew through. [ed: Hm, that's not quite right. A 64-bit integer is 2^6, so that should be 2^(49+6)=2^55, or 32 petabytes). I think :-) ]

mkesper 12y ago

From the article: The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space. Given the astronomical number of program runs that such a central routine is used in, this leads to a considerable waste of energy.

tveita 12y ago
It looks like the Python version that's good for 2^49 items uses 1360 bytes for this array, allocated on the stack. I wouldn't worry about an extra couple of bytes nearly as much as I would worry about changing the behaviour of a function used in an "astronomical number of program", so this looks like a pretty reasonable and conservative choice, at least for an immediate patch.
- deleted 12y ago
  [deleted]
- krick 12y ago
  Does it "change behavior"? As far as I understand, the only change is that this test wouldn't crash anymore. Which certainly is "changing the behavior", but allocating more memory is as well. If so, I don't see any reason not to use formally verified version. Not that it is really important, but quite reasonable.
xamuel 12y ago
Java: Turning "reasonable data, should fit in RAM" into "Big Data (tm)" since 1995
- collyw 12y ago
  I thought it was nodejs evangelists that did that.
  - 12y ago

andrewstuart2 12y ago

I'm surprised that modern implementations don't use something like quicksort, since it has linear space requirements (sorts in-place) and good constants on average for its n*log2(n) running time.

irascible 12y ago
TimSort is supposed to have better performance on real world datasets.
- gus_massa 12y ago
  Agree. More info: http://en.wikipedia.org/wiki/Timsort http://en.wikipedia.org/wiki/Timsort The original mail with the proposal is: http://bugs.python.org/file4451/timsort.txt http://bugs.python.org/file4451/timsort.txt
Arnt 12y ago
Quicksort has poor worst-case behaviour, so it's easy to carry out a DoS attack on network services that use it. Language maintainers don't like restricting their library to input from friendly users, at least not when there are other algorithms that work reasonably with unfriendly input.
- jonesetc 12y ago
  Isn't the malicious attack fought by just picking a random pivot?
  - Freaky 12y ago
    There are still inputs that will make it go quadratic, that just obscures it slightly. A proper fix is to fall back on a different sort if it looks like quicksort is doing that: https://en.wikipedia.org/wiki/Introsort https://en.wikipedia.org/wiki/Introsort
    - thaumasiotes 12y ago

ujjwal_wadhawan 12y ago

Spark 1.1 switched default sorting algorithm from quicksort to TimSort as well in both the map and reduce phases- https://databricks.com/blog/2014/10/10/spark-petabyte-sort.html https://databricks.com/blog/2014/10/10/spark-petabyte-sort.h...

thomasahle 12y ago

This is actually really cool. They tried to verify Timsort as implemented in Python and Java using formal methods. When it didn't seem to work, they discovered that there was actually a missing case in both implementations, which could lead to array out of bounds exceptions. Really shines as an example of how important proof is in computer science.

stingraycharles 12y ago
In the Haskell community there is a tool called QuickCheck [1]: it is able to generate inputs based on preconditions, and you provide a function to verify the postconditions. I am not sure why these kind of testing methods aren't used more often in other communities, since it makes it really easy to catch corner cases; in the Haskell world, at least, using QuickCheck is somewhat pervasive. [1] https://wiki.haskell.org/Introduction_to_QuickCheck2 https://wiki.haskell.org/Introduction_to_QuickCheck2 EDIT: I have never done this before, but could anyone explain why I am being downvoted? I wasn't making the claim that this is a substitute for a formal proof, I was merely adding this information to the discussion since it seemed relevant.
- im3w1l 12y ago
  It wouldn't catch this bug. The algorithm works for lists of size less than 2^49.
- jdimov 12y ago
  There is triq[1] for Erlang and excheck[2] for Elixir. [1] https://github.com/krestenkrab/triq https://github.com/krestenkrab/triq [2] https://github.com/parroty/excheck https://github.com/parroty/excheck
- Osmium 12y ago
  Just FYI for anyone who's interested, but there's a Swift implementation of QuickCheck described in this book: http://www.objc.io/books/ http://www.objc.io/books/ It's very minimal, but the chapter outlines what you'd need to do to make it more complete and get it on par with the Haskell version. There are also a few versions on GitHub too.

inglor 12y ago

This is an excellent use case of formal verification. I can definitely see the merit in using tools like this in my code. They mention KeY http://www.key-project.org/ http://www.key-project.org/ . Is anyone using this here? Are there any good resources on it except for the official site (and this blog post)?

amund 12y ago
Hi, I will ask the authors of the blog post and corresponding academic paper about additional KeY resources and follow-up.
- inglor 12y ago
  Thanks and thanks for the interesting read. I've been looking for real uses of formal verification for a long time. I've played a lot with code contracts in C# and I've played some with languages like Eifel - the advantage of this approach is that it's static and it performs actual proof rather than enforcement. These forms of formal verification could really help with building robust software and if someone makes them easy enough to use I can definitely see them as useful alongside if not instead of unit tests.
deleted 12y ago
[deleted]
iso8859-1 12y ago
It is in use for undergraduate courses in the universities that develop it, and I used it too. It ships with small training problems. What would you like to know? There are many documents on JML. The prover works for you, you just left click logic expressions in KeY and you can prove large parts by point-and-click. It can also finish proofs for you if it's trivial. Often, you only need to specify the loop invariants. I'd recommend opening up KeY, loading one of the trivial examples first: Contraposition. This will be a quick reminder on the logic concepts like implication, but you pretty much cannot screw it up. Try to understand why the proof tree branches when you choose certain steps. Afterwards, try something else from "Getting started" like the examples that the proof searcher can prove (for example SumAndMax) and exploring the proof tree, and trying out yourself from scratch. The automatic proofs are not always pretty, so it's more for to do the manual work first. KeY will only let you do valid proof steps, so you learn quickly how proofs work.

RubyPinch 12y ago

anyone know the list of bugs for this? https://bugs.openjdk.java.net/browse/JDK-8072909 https://bugs.openjdk.java.net/browse/JDK-8072909 It seems they havn't submitted to any other trackers, which is a bit unfortunate

vstolz 12y ago
There is also http://bugs.java.com/view_bug.do?bug_id=8011944 http://bugs.java.com/view_bug.do?bug_id=8011944, where IIUC the suggested "fix" was to use a VM switch to enable the old (and slower) sorting...

bsdetector 12y ago

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?
  - 12y ago

noahl 12y ago

Just a nitpick, but the article makes a mathematical mistake. In the last paragraph of section 1.2, it says For performance reasons, it is crucial to allocate as little memory as possible for runLen, but still enough to store all the runs. *If the invariant is satisfied by all runs, the length of each run grows exponentially (even faster than fibonacci: the length of the current run must be strictly bigger than the sum of the next two runs lengths).* However, fibonacci growth is strictly faster than exponential. In fact, this is why n * log(n) is the lower bound on the number of comparisons a comparison-based sorting algorithm must use: because n! is approximately n * log(n).

robrenaud 12y ago
> fibonacci growth is strictly faster than exponential. This is wrong. The easiest intuition for why this is true that I can come up with is that next Fibonacci number is no bigger than double the previous, and so fib(n) <= 2^n.
anonymoushn 12y ago
Fibonacci is n(i) = n(i-1) + n(i-2). Factorial is n! = n * n-1 * n-2 * ... * 2 * 1. In the second sentence, you might have wanted "lg(n!) is approximately n lg n". That would be a good reason for needing n lg n comparisons to distinguish between the n! permutations. I have edited this comment as my understanding of the parent comment developed >_>
- noahl 12y ago
  Thanks for pointing this out! Yes, I meant log_2(n!) is approximately n*log_2(n). I appreciate you spotting the error. :-)
deleted 12y ago
[deleted]
bladedtoys 12y ago
Fibonacci( n ) = ( P^n - ( -P )^-n ) / sqrt(5) Where P is Golden ratio ( about 1.618 ) So yes it resembles exponential growth but as you can see it is slightly less due to the "- ( -P )^-n" part.

wheaties 12y ago

Wish they'd put that up on Github or Bitbucket. There are so many things to be learned from that. I don't want to just download things or just use a tool (although it's pretty awesome that they made the tool available.)

vstolz 12y ago
What are you looking for?
- wheaties 12y ago
  To watch how change sets are going into the tool. To see what is being done and why as it happens. I find that one of the best ways to learn these things. Especially when it is theory heavy and watching the implementation congele around the theoretical framework.
  - vstolz 12y ago
    Sorry to keep following up, but we'd really like to know what we can improve -- into which tool? Are you talking about the KeY tool, or the various libraries they are now catching up on this issue?
  - emmelaich 12y ago
    Looks like there is a clone on bitbucket, but it hasn't been updated in a while. https://bitbucket.org/adoptopenjdk https://bitbucket.org/adoptopenjdk

bglazer 12y ago

Has anyone used the KeY project in industry? I'd certainly prefer proofs over unit tests. However, I don't understand formal proof systems sufficiently well to know whether these they would work in terms of your typical "app" that makes RPC calls, DB changes, and generally has lots of moving parts and statefulness.

rwmj 12y ago
I have tried to use Coq and Frama-C to prove commercial OCaml and C programs, without, it has to be said, any success. I'm waiting for someone to write the brilliant tutorial.
- dhekir 12y ago
  You're waiting for a tutorial on Coq integrated with Frama-C, or for a tutorial on any of them?
  - rwmj 12y ago
    I'm waiting for a tutorial on how to prove correctness of either OCaml or (especially) C code in real programs.
    - vstolz 12y ago
      It is possible, see e.g. http://ssrg.nicta.com.au/projects/TS/ http://ssrg.nicta.com.au/projects/TS/, though it's not really the tutorial you've been hoping for.
    - dhekir 12y ago
      Research tools are getting closer to what people consider "real" programs, even if they often focus on embedded systems software. CompCert already deals with a quite large subset of C. Frama-C can deal with most if not all syntactic features of C, but then the next challenge is the C standard library, e.g. specifying every useful function (and even "simple" ones such as memcpy can be quite tricky). Afterwards, you have to deal with the glibc, then other high-level libraries, etc... Most of these tools are either still in a mostly-academic setting (where "documentation = conference paper"), or do not have enough funding to pay for the development of more user-friendly features and extensive documentation. But with the ever-increasing security issues receiving media attention lately, we can hope more funding will allow these tools to reach a more mainstream status. By the way, could you give an example of a small program that you would consider "real"? Just to have an idea of its size and complexity.

jordigh 12y ago

Oh, crap. I suppose this also means we have the bug in our GNU Octave implementation: http://hg.savannah.gnu.org/hgweb/octave/file/0486a29d780f/liboctave/util/oct-sort.cc http://hg.savannah.gnu.org/hgweb/octave/file/0486a29d780f/li... Well, time to patch it there too.

ericfrederich 12y ago

Where can I get that PS1 from the shell in the video? It appears to have a green check mark if the previous command returned 0 otherwise some red symbol. Looks cool

protomyth 12y ago
for bash http://stackoverflow.com/questions/16715103/bash-prompt-with-last-exit-code http://stackoverflow.com/questions/16715103/bash-prompt-with...
thedufer 12y ago
The default oh-my-zsh theme does something similar - first character in the PS1 is `➜`, in grey if the previous command returned 0, red otherwise. It just checks `$?`, I assume.

ezyang 12y ago

Everyone here is talking about Timsort, but you should also check out the materials they've published about the KeY project, which they used to carry out this verification. http://www.key-project.org/~key/eclipse/SED/index.html http://www.key-project.org/~key/eclipse/SED/index.html describes their "symbolic execution debugger", which lets you debug any Java code even if you don't know all the inputs (by simply taking the input as a symbolic value). The screencast is very accessible.

nichochar 12y ago

This is bad-ass. Thanks for taking the time and investigating something that so many overlook yet use every day (myself included)

Animats 12y ago

Nice. As usual, entry and exit conditions aren't that hard to write; it's loop invariants that are hard. /*@ loop_invariant @ (\forall int i; 0<=i && i<stackSize-4; @ runLen[i] > runLen[i+1] + runLen[i+2]) @ && runLen[stackSize-4] > runLen[stackSize-3]) @*/ It's surprising how close their notation is to our Pascal-F verifier from 30 years ago.[1] Formal verification went away in the 1980s because of the dominance of C, where the language doesn't know how big anything is. There were also a lot of diversions into exotic logic systems (I used to refer to this as the "logic of the month club"). The Key system is back to plain old first-order predicate calculus, which is where program verification started in the 1970s. For the invariant, you have to prove three theorems: 1) that the invariant is true the first time the loop is executed, given the entry conditions, 2) that the invariant is true for each iteration after the first if it was true on the previous iteration, and 3) that the exit condition is true given that the invariant is true on the last iteration. You also have to prove loop termination, which you do by showing that a nonnegative integer gets smaller on each iteration. (That, by the way, is how the halting problem is dealt with in practice.) #2 is usually the hardest, because it requires an inductive proof. The others can usually be handled by a simple prover. There's a complete decision procedure by Oppen and Nelson for theorems which contain only integer (really rational) addition, subtraction, multiplication by constants, inequalities, subscripts, and structures. For those, you're guaranteed a proof or a counterexample. But when you have an internal quantifier (the "forall int i") above, proof gets harder. Provers are better now, though. A big practical problem with verification systems is that they usually require a lot of annotation. Somebody has to write all those entry and exit conditions, and it's usually not the original programmer. A practical system has to automate as much of that as possible. In the example shown, someone had to tell the system that a function was "pure" (no side effects, no inputs other than the function arguments). That could be detected automatically. The tools have to make the process much, much easier. Most verification is done by people into theory, not shipping products. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf

tenfingers 12y ago

This is a good example of why formal verification is incredibly useful. I tried to invest some time in learning some of the proof verification languages and tools, but so far I wasn't too successful. It looks like that to formulate a proof, I always have to rewrite the algorithm/problem first in the tool's language, which is often not easy. I could see myself making mistakes in writing the proof just as well as I do when I'm programming. Proof validation is also tricky. Coq isn't fully automatic as I initially was expecting. I actually used "prover9" which is first-order only, but does automatic validation. I guess Coq is really useful when you need to understand the proof and interactive validation can guide you, whereas prover9 could help with automation. The thing is, it's still too much work, even for seemingly simple algorithms, to write a proof in either system in order to improve on the current situation of unit testing (that is: if I wanted to get something with more intrinsic value than a test case). Formally verified languages are nice, but for a gazillion of reasons you still need to verify what's running currently.

vstolz 12y ago
With tools like Coq, you may even have the benefit of extracting an implementation from your proof! Some assembly may be required though, and extraction only works to functional languages.

maxerickson 12y ago

Fixed in python: http://bugs.python.org/issue23515 http://bugs.python.org/issue23515

amund 12y ago

The authors have posted a follow-up posting: about KeY - the tool used to prove the bug in TimSort - http://envisage-project.eu/key-deductive-verification-of-software/ http://envisage-project.eu/key-deductive-verification-of-sof...