4 ms·

I want to disagree with you about scaling: most formulas that one might reasonably come up with don't depend in any serious way on the number of bits. So suppos

I want to disagree with you about scaling: most formulas that one might reasonably come up with don't depend in any serious way on the number of bits. So suppose you have a formula that you can test exhaustively with 32-bit floats, and you were to implement it on 64-bit floats. If it fails a couple of times on 32-bit floats, giving it a failure rate of a couple per billion, the same failures are likely to show up in testing with 64-bit floats, a couple per billion. A couple per billion is good enough to be triggered by purely random tests. It's only specifically the exhaustive part that doesn't scale, but that part is not really necessary for this to be useful. Z3's support for floating point theories is really cool, but sometimes the simpler brute-force approach works too! IOW, you could change the message to "Your formula's failure rate is either exactly zero or larger than a few per billion, so random testing is good enough", and I think it would still be good, insufficiently-applied advice.

SomeStupidPoint 9y ago
I'm not sure I understand your point -- For instance, if an algorithm failed only when exactly all three inputs were 0, then it would fail only in 1 per (2^32)^3, despite not being exactly 0 at its failure rate. So exhaustive testing only works if you have a single input, since 2^96 is somewhat harder to exhaustively search, and statistical testing may not be enough, since 1/2^96 << 1/2^32. We can imagine a situation where it fails with each of the values being a number besides 0, making this nontrivial to check for. (For example, if the inputs are normalized somehow before being processed.)
- conistonwater 9y ago
  I wanted to make the point that very few formulas fail on really special inputs in practice.
  - SomeStupidPoint 9y ago
    Thanks for replying. I'm not sure I agree with that, but I'll meet you halfway with those errors rarely matter in practice. (There are only 2^33 people, so getting 2^96 events (or significant portion) is well, impractical. So failure on a single, random one is unlikely to matter.)
  - brucedawson 9y ago
    When rewriting sin() for Xbox 360 I found that the old function gave the wrong result for denormals - off by a factor of two. Since double has an eleven bit exponent that means that roughly one number out of 2,048 would hit this special failure case. For round/ceil/floor a common failure case is the number immediately preceding 0.5. If you're "lucky" then your algorithm fails for lots of numbers ending in 0.5, but if it's just the one number then a random search will never find it. And, an exhaustive search over all of the doubles from 0.0 to 1.0 turns out to cover a really big search space (one quarter of all doubles, roughly).
    - dummyfunny 9y ago
      > "but if it's just the one number then a random search will never find it" Minor, but I think it's not never just very rare. If you're sampling from all floats then the problematic inputs should be possible. I think the distinction people aren't seeing is what are you testing. If it's the sin routine, then I think you're making valid points. But if we're talking about testing for correctness and the overall logic of the program or the abstract expression of the calculation, there are only a limited number of variables. Trying to divide them and vary them under this kind of control seems like a valuable tactic. It might not be sufficient but I've seen way more bugs in shitty if else boolean soups than I have from bits getting flipped. If the output is so sensitive to the value of a certain calculation there should probably be a secondary or checksum. Unless you're doing games where... Framerates.
  - IanCal 9y ago
    The most common ones (for example, when something is 0 or a list is empty) are also typically prioritised in tools like quickcheck.
tikhonj 9y ago
That's a good point—even a few hundred random test cases are usually enough to cover "normal" code. I use QuickCheck for that at work, and it's enough to both find bugs I wouldn't see otherwise and to make me confident in my code when it doesn't find any bugs. (As a bonus, it also tries to "reduce" failing cases, which can really help with debugging.) It's worth tuning your random input generator to produce inputs that commonly cause problems like -0. I can still think of a few situations where exhaustiveness might be worth the effort: - verifying code passed in from the outside (security considerations?) - verifying code generated automatically (ie as part of program synthesis) - verifying very general code you expect to be used in hard-to-predict contexts (ie library routines or compiler optimizations)
- brucedawson 9y ago
  A few hundred random test cases? Double-precision numbers can have 2,048 different exponents. I've seen multiple bugs that only happen with denormals so you need thousands of tests to have any hope of hitting those. If you're going to do random testing then you need to have a huge set of special numbers (denormals, NaNs, infinity, zero, exact powers of two, one more or less than exact powers of two) and you should do millions or billions of random numbers. Then you can start to feel confident.
  - im3w1l 9y ago
    >It's worth tuning your random input generator to produce inputs that commonly cause problems like -0. This would definitely include denormals. As well as +-inf, nan, odd int, even int, negative odd and even int. +-1. Some .5s.
IshKebab 9y ago
Yeah but what about something like hypot or atan2?

SomeStupidPoint 9y ago

I'm not sure I understand your point -- For instance, if an algorithm failed only when exactly all three inputs were 0, then it would fail only in 1 per (2^32)^3, despite not being exactly 0 at its failure rate. So exhaustive testing only works if you have a single input, since 2^96 is somewhat harder to exhaustively search, and statistical testing may not be enough, since 1/2^96 << 1/2^32. We can imagine a situation where it fails with each of the values being a number besides 0, making this nontrivial to check for. (For example, if the inputs are normalized somehow before being processed.)

conistonwater 9y ago
I wanted to make the point that very few formulas fail on really special inputs in practice.
- SomeStupidPoint 9y ago
  Thanks for replying. I'm not sure I agree with that, but I'll meet you halfway with those errors rarely matter in practice. (There are only 2^33 people, so getting 2^96 events (or significant portion) is well, impractical. So failure on a single, random one is unlikely to matter.)
- brucedawson 9y ago
  When rewriting sin() for Xbox 360 I found that the old function gave the wrong result for denormals - off by a factor of two. Since double has an eleven bit exponent that means that roughly one number out of 2,048 would hit this special failure case. For round/ceil/floor a common failure case is the number immediately preceding 0.5. If you're "lucky" then your algorithm fails for lots of numbers ending in 0.5, but if it's just the one number then a random search will never find it. And, an exhaustive search over all of the doubles from 0.0 to 1.0 turns out to cover a really big search space (one quarter of all doubles, roughly).
  - dummyfunny 9y ago
    > "but if it's just the one number then a random search will never find it" Minor, but I think it's not never just very rare. If you're sampling from all floats then the problematic inputs should be possible. I think the distinction people aren't seeing is what are you testing. If it's the sin routine, then I think you're making valid points. But if we're talking about testing for correctness and the overall logic of the program or the abstract expression of the calculation, there are only a limited number of variables. Trying to divide them and vary them under this kind of control seems like a valuable tactic. It might not be sufficient but I've seen way more bugs in shitty if else boolean soups than I have from bits getting flipped. If the output is so sensitive to the value of a certain calculation there should probably be a secondary or checksum. Unless you're doing games where... Framerates.
- IanCal 9y ago
  The most common ones (for example, when something is 0 or a list is empty) are also typically prioritised in tools like quickcheck.

tikhonj 9y ago

That's a good point—even a few hundred random test cases are usually enough to cover "normal" code. I use QuickCheck for that at work, and it's enough to both find bugs I wouldn't see otherwise and to make me confident in my code when it doesn't find any bugs. (As a bonus, it also tries to "reduce" failing cases, which can really help with debugging.) It's worth tuning your random input generator to produce inputs that commonly cause problems like -0. I can still think of a few situations where exhaustiveness might be worth the effort: - verifying code passed in from the outside (security considerations?) - verifying code generated automatically (ie as part of program synthesis) - verifying very general code you expect to be used in hard-to-predict contexts (ie library routines or compiler optimizations)

brucedawson 9y ago
A few hundred random test cases? Double-precision numbers can have 2,048 different exponents. I've seen multiple bugs that only happen with denormals so you need thousands of tests to have any hope of hitting those. If you're going to do random testing then you need to have a huge set of special numbers (denormals, NaNs, infinity, zero, exact powers of two, one more or less than exact powers of two) and you should do millions or billions of random numbers. Then you can start to feel confident.
- im3w1l 9y ago
  >It's worth tuning your random input generator to produce inputs that commonly cause problems like -0. This would definitely include denormals. As well as +-inf, nan, odd int, even int, negative odd and even int. +-1. Some .5s.

IshKebab 9y ago

Yeah but what about something like hypot or atan2?