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

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

googleresearch.blogspot.com

Post reply on HN
Print view View original

31–40 of 70 posts

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

#31

Post by 6ren »

DarkShikari wrote: post #8

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.

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

#32

Post by jakubw »

The general lesson that I take away from this bug is humility: It is hard to write even the smallest piece of code correctly, and our whole world runs on big, complex pieces of code.

It surely does if everyone has to write their own binary search implementation when most standard libraries have one and several of them have one that is flexible enough (either due to the language's features or the binary search routine itself) to not just search through a container but through a solution space in an optimization problem. So I'm surprised the author hasn't concluded with the lesson that would be somewhat more practical: It is hard to write even the smallest piece of code correctly, so don't do it and use whatever's in your stack unless you have a good reason not to.

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

#33

Post by ChuckMcM »

redthrowaway wrote: post #29
ChuckMcM wrote: post #11

I'm tempted to solve it with: low/2 + high/2 + (low & high & 1); That side steps the overflow condition completely.

It would sidestep the overflow, but prima facie it appears to be slower than the provided: low + (high - low)/2; Your solution takes, depending on the architecture, between several more and nearly double the trips to the ALU. Gimmie a sec; I've got bugger all to do at work. I'll compile it and profile it.

Would be interested in seeing the profile. Re-ordering it to the following (which the compiler might do too)

  low&high&1 + low>>1 + high>>1
Should compute in a single cycle if the register coloring is working in the pipeline. The >> 1 come out of the barrel shifter stage, the low&high&1 resolves in the load, so you end up with a single sum of three operands. Since its being stored in a separate register that would avoid a write stall in the pipeline as well.

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

#34

Post by abecedarius »

lutorm wrote: 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.

Yes, the binary search I wrote back in the day used size_t and represented the range as (start, length) rather than (start, end). Full range, and no overflow anywhere if you write it the obvious way. Maybe it was a little bit slower, I don't know.

I'd used Bentley as the starting point, so I was surprised when this news first came out and got reported as Bentley's bug. I guess it could be considered so.

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

#35

Post by jberryman »

jrockway wrote: post #16
DarkShikari wrote: post #8

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…

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.…

> But in practice, it's easy to make a simple mistake in implementation and accidentally throw your proof out the window.

But that's not how a proof of correctness works. You have an implementation (of an algorithm, say) and you prove mathematically that it is correct with respect to a formal specification. The implementation and proof aren't separate things.

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

#36

Post by loeg »

lutorm wrote: 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.

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

#37

Post by blackhole »

wtallis wrote: post #25
nazgulnarsil wrote: post #24

Earlier quoted context omitted.

you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?

All proofs start from some assumptions. When you are proving programs, you assume that the hardware is functioning properly. After all, anyone going to the expense of proving their software is correct will also pay for ECC throughout their hardware. Once you've proven your software correct, you can make assurances about the behavior of the software when run on particular hardware, and those assurances will be limited…

Assuming that hardware will work correctly can be an extremely dangerous assumption.

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

#38

Post by jbarham »

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...

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

#39

Post by oconnore »

nazgulnarsil wrote: post #24
DarkShikari wrote: post #23

Earlier quoted context omitted.

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…

you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?

What is your point, exactly?

Do you think testing (likely on a different machine than the target) will catch a 1 in a million hardware error either?

Post reply on HN