Almost the same bug: http://code.google.com/p/guava-libraries/issues/detail?id=61...
Nearly all binary search and merge sort implementations are broken (2006)
21–30 of 70 posts
Re: Nearly all binary search and merge sort implementations are broken (2006)
#22This bug requires either (1) low/mid/high are pointers [edit - I don't think this is valid; IIRC pointer arithmetic is only sane for add/subtract an int from a pointer, not divide a pointer or add two pointers]; or (2) item_count > INT_MAX / 2, which means memory_size >= sizeof(your_array) == sizeof(item) * item_count > INT_MAX / 2, which means either 1-byte or 2-byte array elements, or that your ints are smaller tha…
The author is claiming that nearly all binary search implementations are wrong under those specific conditions, not that binary search implementations are wrong under nearly all conditions.
...bah. I keep forgetting that 64-bit C/C++ compilers are generally LP64 (or even LLP64) instead of ILP64, so "int" being possibly too small is in fact typical.
Still. In the example (Java) implicit down-converting isn't allowed, so this is a result of the spec putting arbitrary limits on array size (must be indexed by nonnegative 'int' values). In C or C++ there is no such limit and I think more modern compilers (llvm) will give a warning on loss of precision, so either you have that warning ignored/disabled/unavailable or you have 32-bit code with a billion-element array. I guess what I'm thinking with this is, with a sane language/compiler, the only way to trigger this should be to fill half of your theoretically-logically-addressable memory with an array with single-byte elements.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#23It 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…
> 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 example, Green Hills Software's INTEGRITY operating system has bounds on the runtime and behavior of system calls formally verified, so one can reasonably guarantee that a malicious user cannot DDOS the system by making system calls with unbounded duration.
There are even entire programming languages designed for the sole purpose of making formal, mathematical verification of programs easier.
A program is a representation of an algorithm.
Yes, which is why you have to prove it correct again, since real programming languages, e.g. C, have limitations not typically present in the original algorithm.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#24Earlier 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…
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?
Re: Nearly all binary search and merge sort implementations are broken (2006)
#25Earlier 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?
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 primarily by the reliability of the hardware.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#26It 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…
You can prove the correctness of a program given a specification of the language you write it in. But is the compiler you use to compile your program correct? Do you know all processor bugs?
What you are talking about is the "trusted computing base". Prove every part of the basesystem your running on, this of course is a HUGE task, but there are people thinking and working on this.
You might injoy this darpa project: http://www.crash-safe.org/papers
The propose there own hardware, OS, languages and compilers. The Hardware Design is by Tom Knight, one of the guys who designed the lisp machine.
Its quite an intressting read.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#27Earlier quoted context omitted.
You can prove the correctness of a program given a specification of the language you write it in. But is the compiler you use to compile your program correct? Do you know all processor bugs?
Computer hardware is not correct. So, you need to step past mathematical perfection and write defensively. Rule 1: you can't trust RAM it lies. That said you can build automated tests that add random memory errors to help find the program that's best able to handle memory errors.
You too might be intressted in the link I posted above. Its about building safe hardware (and software), but I don't think its completly safe to anykind of random bit-flips.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#28I don't understand why I need Javscript enabled to merely read a blog post on blogspots.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#29I'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;
Gimmie a sec; I've got bugger all to do at work. I'll compile it and profile it.
Re: Nearly all binary search and merge sort implementations are broken (2006)
#30I'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.