Nearly All Binary Searches and Mergesorts Are Broken (2006) | Hacker News Reader

Nearly All Binary Searches and Mergesorts Are Broken (2006)

research.googleblog.com

58 pointsolalonde35 comments

As I was saying over at [1], if you're going to do program proofs, you have to prove absence of overflow. It's the cause of many program bugs.

[1] https://news.ycombinator.com/item?id=12146049

Oh yeah, I actually saw the link in your comment!

At the risk of sounding stupid, I had a question about the following solution:

    int mid = (low + high) >>> 1;

I understand that right shift is like dividing by 2, just like in decimal right shifting the digits is like dividing by 10 (654/10 = 065). But why can we just ignore the low + high overflow issue? Is it because the overflow will be stored in the two's complement bit and right shift doesn't care about what that bit represents? If unsigned ints were used instead, I suppose that trick wouldn't work?

low and high are assumed to be positive and at most 2^31 - 1. So, there is a zeroed high bit in each which, for a signed int, is reserved to indicate negation.

When low and hi are summed together, the high bit of the result might be set. For a signed int, this would be an accidental overflow and would be falsely interpreted as a negative number. However, if you interpret the result as an unsigned int, it would be the correct sum.

The Java logical shift operator >>> does not retain the sign when shifting. So, it will always shift a 0 into the high bit, making the result a positive signed int.

In most C implementations, >> is an arithmetic shift, which would retain the sign in the result. So in C, we would need to cast low and high as unsigned first; otherwise, the high bit will be retained rather than shifted.

Hmm, I always figured it was just assumed that, unless otherwise specified, most well-known implementations fail with sufficiently large numbers.

All code running on a machine of finite size will fail (sometimes gracefully, usually not) for sufficiently large input values.

But the goal is only to work for the finite number of possible inputs allowed by the input types. There's no reason a finite machine has to fail on those.

Try to pass in data with zero bits of free memory.

That should still result in a clean error, not some kind of undefined behavior.

It's not impossible to guarantee that a system has sufficient memory for all possible inputs. Look at high stakes embedded software development. You need more control than you get as an application on a desktop computer but there's nothing inherent about finite state machines that make them vulnerable.

Yep, this is just vintage click-bait.. you can bet more than sorting routines will fail with numbers approaching 2^63. It doesn't matter because if you're running quick sort on a list of 2^64 entries then something else is going wrong before your (l+r)/2 has a chance to overflow.

int in Java and C is 32 bit wide, not 64 bit, this limit is easily reached.

You cannot just assume nobody will use your algorithms with large inputs and act like your data types have unlimited range. Such bugs will typically manifest at important customers and be hard to analyze. Better think about your types beforehand and do add runtime checks!

If you're trying to sort 2^63 items at once, you have other problems.

What is 'sufficiently large'? Could be anything.

A function, especially when part of the standard library, must work correctly for all possible inputs or reject them outright.

Prior discussions: http://news.ycombinator.com/item?id=621557 http://news.ycombinator.com/item?id=1130463 http://news.ycombinator.com/item?id=3530104 https://news.ycombinator.com/item?id=9857392 https://news.ycombinator.com/item?id=6799336

> I was shocked to learn that the binary search program that Bentley proved correct and subsequently tested in Chapter 5 of Programming Pearls contains a bug.

Huh? How did he prove it correct, then?

'Proofs' done by humans are done within a certain context; there's usually a lot that goes unstated, or is left unexamined at the finest level of detail.

Generally that isn't a problem and the 'small' details or assumptions don't 'leak' up to higher levels and do any real damage to the proof.

There's a movement to make proofs formally verified, to try move towards eliminating this issue, but that's hard, because writing out every little detail, specifying every last piece of context & assumption & step is laborious.

> because writing out every like detail, specifying every last piece of context & assumption & step is laborious.

Can code be written and subsequently formally verified that can then help in the process of formally verifying code?

It is not the verification that is laborious, although it can be computationally intensive, it is the specification. It is making sure that whatever it is you are proving is actually exactly and completely what you desire of the function.

In this case the proof did not properly account for the full range of inputs, of at least skipped over the fact that in real hardware the integer domains are finite.

There's a lot of formal verification tools out there though, they do make it easier,easy enough to at least properly verify the correctness of a simple sorting algorithm.

On an idealized machine with arbitrarily large integers I assume.

How else do you "prove" trivial algorithms other than by removing the realities of an actual runtime environment?

I'm pretty sure you're right though. Integers must have been defined as infinite in the proof for it to have been a proof at all.

If you sufficiently specify the runtime environment the proof can still work: Since the array is composed of integers, many C compilers/machine architectures will dictate a maximum size of the array s.t. there can't be overflow.

Touche, and fair enough- although you would expect them to call out that limitation since it's both critical and highly un-general. Bytes are comparable, small, and common enough to at least accommodate an exclusionary statement in the proof.

This is why I prefer to use Python for my binary searches ;-)

One possible scenario is he proved it correct assuming that the ints in the function were mathematical integers(-infinity, ... -1, 0, 1, ..., infinity). In realty all representations of numbers have an upper limit after which the representation will become corrupted or unsupported.

A proof is only, at bottom, a convincing argument. Mathmematicians are harder to convince than most people, but they can still miss things.

At least, in a memory-safe language, you'll get an IndexOutOfBoundsException rather than corrupting memory, which can be used as an attack.

    int mid = (low + high) >>> 1;

I don't get how this fixes anything, the overflow still occurs.

Why not simply

    int mid = (low/2) + (high/2) + (low & high & 1);

More expensive.

Here's another approach: represent the range as a (low, length) pair instead of (low, high). The update becomes either length /= 2 or low += length/2, length -= length/2. IIRC this was what I did when I adapted Bentley's code to C 25 years ago, mainly because of overflow. It never occurred to me to check if standard libraries got it wrong.

All of those proposed solutions still fail on valid arrays that are to large. We changed to 64 bit OS and you now 32 bit indexes just don't cut it.

Not in java (arrays can only be indexed by a signed 32 bit integer) and the C++ solution works exactly the same way with the full 64 bit data types. That much should be obvious, and if you think you might legitimately exceed two billion elements in the array you're sorting- you'd be a fool to rely on someone else's sort implementation.

Java uses shorts in some JavaCard implementations. So, it's clearly just a legacy limitation which will eventually be removed.

As to C++ 2+ billion byte arrays are not uncommon. It's just a few gigs of ram for int[] arrays.

size_t forever and always

> int mid = low + ((high - low) / 2);

Why this instead of the more intuitive `low/2 + high/2` ?

Edit: Nevermind, I get it. The reason is instructive: In the case where high and low are odd numbers, the "more intuitive" way is off by one.

A more interesting version of that bug, I find, and the reason why I almost never used unsigned values in my algorithm is that when you compute indices in a non-trivial way, any intermediate value that is negative will break your program.

> It is not sufficient merely to prove a program correct; you have to test it too.

No, this just indicates that you didn't prove it rigorously enough :p

Reply on news.ycombinator.com