Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Nearly All Binary Searches and Mergesorts are Broken (2006)

googleresearch.blogspot.co.uk

Post reply on HN
Print view View original

31–40 of 47 posts

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#31

Post by stiff »

crntaylor wrote: post #28
stiff wrote: post #24

Earlier quoted context omitted.

Computers are now complicated enough for Computer Science to have turned to some extent into an empirical science - it is impossible for a single person to have in their head everything that goes in a typical computer, operating system, compiler and so forth, so one is often forced to resort to experiment to find things out, it's no longer a theory where you can just reason things out, maybe it never was one in fact,…

> Imagine mathematicians or computer scientists re-proving real analysis theorems using floating point arithmetic... Mathematicians and computer scientists do prove theorems about floating point arithmetic! For example, the most widely-cited floating point reference contains no fewer than fifteen theorems about floating point: http://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.ht... Or here's a presentation ab…

I know there are theorems about floating point, that's missing the point, what I am saying is that the theories most useful for doing reasoning are often nearly impossible to formulate if you would like to include in them a lot of messy details of something like floating point, just as one example. What happens instead, we reason using nice idealized theories, and then we experiment to asses the gap between theory and reality.

I am completely a fan of theory and proofs, but the point of the quoted comment is that there is an empirical component to software development too, and your original comment seemed to question it.

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#32

Post by skrebbel »

chrismonsanto wrote: post #25
crntaylor wrote: post #17

I don't agree with this statement "It is not sufficient merely to prove a program correct; you have to test it too." It is sufficient to prove a program correct - as long as your proof is not faulty! The problem in this case was not that the program had a bug despite being proved correct. The problem was that the 'proof' was not a proof at all. Machine ints are not mathematical integers. Floats are not real numbers.…

I do agree with the quoted statement. I have a lot of experience with machine-verified proofs (in a language called Coq). Even though Coq guarantees that an accepted proof is correct, you still can't necessarily trust it, because your formal model of the program may be not accurate enough, or your statement of correctness is improperly stated. In this case, it seems like their proof was correct with respect to their…

This hinges on the definition of "program". The OP did not say "algorithm", which is often assumed to be something on paper rather than a piece of working code in $LANGUAGE. I believe that nearly anyone will assume that a "program" is something tangible, something that a computer can run.

So, the OP did not prove the program correct, but he did prove the underlying algorithm correct.

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#33

Post by jadyoyster »

yetanotherphd wrote: post #2

I would guess that nearly all code, period, is vulnerable to integer overflow issues. I don't think it makes sense to worry about this except in very special cases.

How so? From [1] it would seem that Lisps (idiomatic ones at least), Python, Perl, Haskell and Ruby are all free from the possibility of integer overflow. That definitely doesn't sound like "nearly all code".

[1] https://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#34

Post by Jare »

MaulingMonkey wrote: post #15
koverstreet wrote: post #8

Earlier quoted context omitted.

Yup. More annoyingly, for a binary search over an array (i.e. something that can fit in memory) their code is still wrong - they should be using size_t.

On top of that, this 'fix' from the article, even if it were corrected to use size_t instead of unsigned int... In C and C++ (where you don't have the >>> operator), you can do this: 6: mid = ((unsigned int)low + (unsigned int)high)) >> 1; Has the same bug as the original snippet, just in unsigned space. Now, granted, binary searching a >2GB byte array in a 32-bit process is an unlikely use case... but it is technica…

If you have an array >2GB (I understand this isn't possible in Java), you can't attempt to use ints as indices at all, you need size_t everywhere.

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#35

Post by Perseids »

I understand why people actually using these huge data sets see this as a bug but personally I don't agree. Consider how hard programming becomes when you have to take into account integer overflows even for a /single addition/ of array indices. Our mainstream programming languages are build around the assumption that indices don't overflow and I would rather use the binary sort code as argument to support this than to support the argument that bug free code is really hard.

The real lesson in my opinion is to stop using 32 bit integers in big data applications. Which unfortunately doesn't seem trivial in Java.

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#36

Post by Perseids »

jadyoyster wrote: post #33
yetanotherphd wrote: post #2

I would guess that nearly all code, period, is vulnerable to integer overflow issues. I don't think it makes sense to worry about this except in very special cases.

How so? From [1] it would seem that Lisps (idiomatic ones at least), Python, Perl, Haskell and Ruby are all free from the possibility of integer overflow. That definitely doesn't sound like "nearly all code". [1] https://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic

With Haskell I would not be so sure. There is the 'Integer' arbitrary size data type but what is mostly used is 'Int' for efficiency reasons afaik. Compiled as a 64 bit executable this should be a 64 bit integer though.

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#37

Post by rytis »

chattoraj wrote: post #26
crntaylor wrote: post #17

I don't agree with this statement "It is not sufficient merely to prove a program correct; you have to test it too." It is sufficient to prove a program correct - as long as your proof is not faulty! The problem in this case was not that the program had a bug despite being proved correct. The problem was that the 'proof' was not a proof at all. Machine ints are not mathematical integers. Floats are not real numbers.…

>It is sufficient to prove a program correct - as long as your proof is not faulty! This is unquestionable truth. Proof: Proposition A(X): X is true in theory Proposition B : For all X such that A(X), X is true in practice Theoretically, there is no difference between theory and practice. ... (1) Theoretically, statement B is true. [using (1)] ... (2) Therefore, B is true in practice. [using (1) and (2)] QED.

theory is very often contrasted to "practice" [...] a Greek term for "doing", which is opposed to theory because pure theory involves no doing apart from itself. [1]

[1] http://en.wikipedia.org/wiki/Theory

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#38

Post by bproctor »

I don't believe this is necessarily a bug. All code will break under some extremes and nowhere are the requirements specified for what this code is supposed to be able to handle. Without requirements, you can't "prove" it correct (or incorrect for that matter).

Re: Nearly All Binary Searches and Mergesorts are Broken (2006)

#39

Post by dsego »

AndrewBissell wrote: post #4
yetanotherphd wrote: post #2

I would guess that nearly all code, period, is vulnerable to integer overflow issues. I don't think it makes sense to worry about this except in very special cases.

Having an array with more than about 1.2 billion elements is all that it would have taken to break the old binary search, and that's not all that uncommon anymore. Pure JavaScript code isn't vulnerable to integer overflow by virtue of not having any integer types, and I believe errors like this were the reason for leaving them out of the language.

That wasn't the reason, the reason was to make the language simpler, with only one number type.
Post reply on HN