Live data from Hacker News

Nearly all binary search and merge sort implementations are broken (2006)

googleresearch.blogspot.com

41–50 of 70 posts

Re: Nearly all binary search and merge sort implementations are broken (2006)

#41
post #36
post #9

While true, it seems that if your array is that close to the inherent size limit in indexing by ints, this is at most a temporary fix. How fast does your sorting requirements go from 2^31 to 2^32? It seems that you should be using size_t here, not int.

size_t is actually 32-bit on some 64-bit platforms; you want uint64_t.

If that's true, that's a bug in the platform, not the program. The whole point of size_t is to be however many bits you need to represent the size of things in your address space.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#42
post #5

An interesting article that links back to this one: http://reprog.wordpress.com/2010/04/19/are-you-one-of-the-10... The claim is that even ignoring overflow, only 10% of programmers can correctly implement a binary search. When I tried it, I thought I got it working, but it was later pointed out that I didn't handle empty lists correctly. Programming correctly is hard.

I hope that means "10% get it right first time" and not "only 10% can do it at all, even given a computer and a whole day to do it."

Couldn't resist that challenge (although the thread is nearly 2 years old.) I think mine works, at least it gives the right answer for all my test cases.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#43
post #40

So C, C++, and Java don't have good support for arithmetic. What else is new?

+1, this has nothing to do with binary search and everything to do with the fact that almost any application written in those languages will have bugs that do not show until numbers nearing INT_MAX are used. Another given is that all applications that use recursion is bound to run into stack overflow errors/bugs when used on big data.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#44
post #38

Nice to see that the Go gets it right: func Search(n int, f func(int) bool) int { // Define f(-1) == false and f(n) == true. // Invariant: f(i-1) == false, f(j) == true. i, j := 0, n for i answer is i. return i } http://code.google.com/p/go/source/browse/src/pkg/sort/searc...

I expect at least one of the Go authors was well aware of this very incident (the Java breakage), it was fairly well publicized before Go ever saw the light of day.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#45
post #30

I'm tempted to suggest that the fixed C/C++ version is still not correct with respect to this issue, namely on architectures where INT_MAX == UINT_MAX. (Or really INT_MAX = 65535.)

INT_MAX == UINT_MAX is the only valid failing case, because elsewhere in the standard integer types are restricted to pure binary representations. This means that if UINT_MAX is greater than INT_MAX, it must be at least INT_MAX * 2 + 1.

That can't actually be taken for granted, relevant Usenet discussion begins here:

http://groups.google.com/group/comp.std.c/browse_thread/thre...

Re: Nearly all binary search and merge sort implementations are broken (2006)

#46

Earlier quoted context omitted.

Mathematics sits atop a very small set of trusted axioms. Computer hardware is not so reliable; the parts are made in China as cheaply as possible. So even if you've proven something correct in theory, it doesn't matter because of all the additional variables that the real world introduces. The big insights in computer science look very much like mathematics; the mechanics of a binary search work perfectly in theory.…

Actually most bugs are being introduced in the translation between pseudocode and your working programming language. For instance pseudocode does not deal with 32-bit integers that can overflow. But that's not the fault of the algorithm, or the fault of its proof and it also has nothing to do with the origin of your computer parts. Also, the "mechanics" of binary search work perfectly in practice. I see no evidence t…

Upvoted for the first two paragraphs, but I can't make sense of the second sentence of the third paragraph. The algorithm given in the article works in Python because Python has different overflow behavior than Java, C, or C++. When you say you "see no evidence", it seems like you are saying the implementation given in the article does work in Java etc.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#47
post #31

It is not sufficient merely to prove a program correct; you have to test it too. Moreover, to be really certain that a program is correct, you have to test it for all possible input values, but this is seldom feasible. This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics sho…

How do you prove the proof is correct? And how do you prove that your mathematical representation correctly corresponds to the problem you are modeling? This is why I am bitter and disillusioned about mathematics: it promises certainty, but doesn't deliver. It remains pragmatically useful, like many other tools, but does not deserve the semi-mystical status some confer on it.

The proof is a sequence of extremely easy logical inference rules like if A=>B and A then B. You check the correctness of the proof by verifying that these rules are applied correctly. Obviously though, there is no way to prove that your mathematical model corresponds to reality. That is because mathematics is not concerned with reality.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#48
post #31

It is not sufficient merely to prove a program correct; you have to test it too. Moreover, to be really certain that a program is correct, you have to test it for all possible input values, but this is seldom feasible. This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics sho…

How do you prove the proof is correct? And how do you prove that your mathematical representation correctly corresponds to the problem you are modeling? This is why I am bitter and disillusioned about mathematics: it promises certainty, but doesn't deliver. It remains pragmatically useful, like many other tools, but does not deserve the semi-mystical status some confer on it.

It depends on the scope of the proof. It's sloppy to say "this is proved to be correct". They should say "this is proved to be terminate with output X in a finite time, for input values in the range -Y:Y".

Everything can be proved to be "correct", for some definition of "correct" (i.e. "output undefined, program may not terminate").

Re: Nearly all binary search and merge sort implementations are broken (2006)

#49

Earlier quoted context omitted.

> This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics should be thrown out. > If you've proven a program correct .. You are making a categorical error: One proves algorithms and tests programs. A program is a representation of an algorithm. If the language of implementation…

You are making a categorical error: One proves algorithms and tests programs. You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs. For e…

The programs that can be proven are severely limited in power. For one, the tools to prove correctness of programs can't deal with data other than integers[1].

The way this usually works is that the proof is written and the code is then generated from the proof. That code is then incorporated in something larger, which has not been proven correct. Such is the case with algorithms. You can mathematically prove an algorithm correct. You can even write a proof and generate a program from it. Then you still have to use that algorithm and all the code using it can't be proven correct with current methods. That is why you will still have to test your program.

  There are even entire programming languages designed for
  the sole purpose of making formal, mathematical
  verification of programs easier.
Yes, and their practical usefulness is still severely limited.

[1] Of course, in theory this means they can deal with any data; in practice it means they can't.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#50

Earlier quoted context omitted.

Actually most bugs are being introduced in the translation between pseudocode and your working programming language. For instance pseudocode does not deal with 32-bit integers that can overflow. But that's not the fault of the algorithm, or the fault of its proof and it also has nothing to do with the origin of your computer parts. Also, the "mechanics" of binary search work perfectly in practice. I see no evidence t…

Upvoted for the first two paragraphs, but I can't make sense of the second sentence of the third paragraph. The algorithm given in the article works in Python because Python has different overflow behavior than Java, C, or C++. When you say you "see no evidence", it seems like you are saying the implementation given in the article does work in Java etc.

Technically, the naïve implementation is perfectly fine for C/C++, so long as size_t is at least 268 bits long on your platform. :)
Post reply on HN