6 ms·

Nearly All Binary Searches and Mergesorts Are Broken (2006)

58 points by olalonde 10y ago

Retric 10y ago
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.
- haimez 10y ago
  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.
  - Retric 10y ago
    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.
- forrestthewoods 10y ago
  size_t forever and always
wandering2 10y ago
> 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?
- feral 10y ago
  '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.
  - cmdrfred 10y ago
    > 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?
    - tinco 10y ago
      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.
- mnarayan01 10y ago
  On an idealized machine with arbitrarily large integers I assume.
  - haimez 10y ago
    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.
    - mnarayan01 10y ago
      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.
      - haimez 10y ago
        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.
  - mark-r 10y ago
    This is why I prefer to use Python for my binary searches ;-)
- mshenfield 10y ago
  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.
- Tloewald 10y ago
  A proof is only, at bottom, a convincing argument. Mathmematicians are harder to convince than most people, but they can still miss things.
trav4225 10y ago
Hmm, I always figured it was just assumed that, unless otherwise specified, most well-known implementations fail with sufficiently large numbers.
- taneq 10y ago
  All code running on a machine of finite size will fail (sometimes gracefully, usually not) for sufficiently large input values.
  - tgb 10y ago
    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.
    - Retric 10y ago
      Try to pass in data with zero bits of free memory.
      - mrich 10y ago
        That should still result in a clean error, not some kind of undefined behavior.
      - tgb 10y ago
        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.
- gfody 10y ago
  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.
Animats 10y ago
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 https://news.ycombinator.com/item?id=12146049
- olalonde 10y ago
  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?
  - psyklic 10y ago
    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.
kartickv 10y ago
At least, in a memory-safe language, you'll get an IndexOutOfBoundsException rather than corrupting memory, which can be used as an attack.
Iv 10y ago
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.
kuharich 10y ago
Prior discussions: http://news.ycombinator.com/item?id=621557 http://news.ycombinator.com/item?id=621557 http://news.ycombinator.com/item?id=1130463 http://news.ycombinator.com/item?id=1130463 http://news.ycombinator.com/item?id=3530104 http://news.ycombinator.com/item?id=3530104 https://news.ycombinator.com/item?id=9857392 https://news.ycombinator.com/item?id=9857392 https://news.ycombinator.com/item?id=6799336 https://news.ycombinator.com/item?id=6799336
legulere 10y ago
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);
- abecedarius 10y ago
  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.
tomsmeding 10y ago
> 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
Cpoll 10y ago
> 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.

58 points by olalonde 10y ago

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.

haimez 10y ago
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.
- Retric 10y ago
  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.
forrestthewoods 10y ago
size_t forever and always

wandering2 10y ago

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

feral 10y ago
'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.
- cmdrfred 10y ago
  > 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?
  - tinco 10y ago
    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.
mnarayan01 10y ago
On an idealized machine with arbitrarily large integers I assume.
- haimez 10y ago
  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.
  - mnarayan01 10y ago
    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.
    - haimez 10y ago
      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.
- mark-r 10y ago
  This is why I prefer to use Python for my binary searches ;-)
mshenfield 10y ago
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.
Tloewald 10y ago
A proof is only, at bottom, a convincing argument. Mathmematicians are harder to convince than most people, but they can still miss things.

trav4225 10y ago

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

taneq 10y ago
All code running on a machine of finite size will fail (sometimes gracefully, usually not) for sufficiently large input values.
- tgb 10y ago
  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.
  - Retric 10y ago
    Try to pass in data with zero bits of free memory.
    - mrich 10y ago
      That should still result in a clean error, not some kind of undefined behavior.
    - tgb 10y ago
      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.
gfody 10y ago
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.

Animats 10y ago

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 https://news.ycombinator.com/item?id=12146049

olalonde 10y ago
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?
- psyklic 10y ago
  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.

kartickv 10y ago

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

Iv 10y ago

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.

kuharich 10y ago

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

legulere 10y ago

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);

abecedarius 10y ago
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.

tomsmeding 10y ago

> 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

Cpoll 10y ago

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