5 ms·

You could have condensed your entire post to just "This exception was uncaught". Your last point is just outright ridiculous: > "Rust improves upon this situat

by ajxs 7y ago

You could have condensed your entire post to just "This exception was uncaught". Your last point is just outright ridiculous: > "Rust improves upon this situation by panicking in debug mode and wrapping in release mode, which is better than the Ada behavior in every possible" So... What you're trying to tell us is that Ada recognising an exceptional situation has occurred is bad, and that Rust just ignoring it is a good thing? Righto... An integer overflow occurring in this scenario is an exceptional condition. In this case it was one that the developers did not anticipate. This issue arose because they mistakenly thought it was not possible for this scenario to occur. The mistake here was not anticipating the exception and handling it in a meaningful way, not the raising of an exception. The fact that not raising an exception would have avoided the disaster in this case is entirely incidental. It was still an exceptional circumstance that the developers, testers, designers did not anticipate. The silent wrapping behaviour you describe would have bitten someone eventually, perhaps here, perhaps somewhere else. Possibly with enormous repercussions. > "Normal "unsafe" languages improve this by giving an incorrect value as the result, which in the case of Ariane V would have saved the flight." The normal "unsafe" languages you're referring to ( presumably C ) have a history of very poor error handling. Requiring an extremely high degree of conscientiousness when programming for mission-critical applications. Can you imagine actually programming for what you're describing here? Not only does the computer have to guard against outright failure, but now it has to infer the possibility of an error state from a stream of in-band data in real-time. Righto... Also, just so you know: Signed integer overflow is UNDEFINED BEHAVIOUR in C.

kragen 7y ago
Tainting the dataflow rather than the control flow, like a quiet NaN, would be a better solution in cases like these. It happens that the solution that was chosen was the worst choice possible, but in other cases it wouldn't have been. Probably the fact that the engineers got the case analysis wrong suggests that the methods of reasoning they were using weren't very effective. Modern formal methods might or might not have helped; guaranteeing that a piece of code is statically free of exceptions is not a terribly advanced thing to do, but really you'd like to guarantee that the variable was actually big enough. Having less code to reason about certainly would have helped. C’s choice is clearly unconscionable.
- blub 7y ago
  In hindsight it would have been perhaps better, but I don't think it can be said that having essentially random values in memory is better than having a controlled error handling action being executed. Is there any reference that such a course of action is preferred or beneficial?
  - kragen 7y ago
    We have a lot of experience with floating-point qNaN values since IEEE 488 introduced them in 1985, and more rigorous languages than Ada — such as OCaml, Haskell, and Rust — use a generalized version of the concept for a lot of error handling. I don't think there's an open-and-shut case that error values are "preferred or beneficial" in general with respect to exception handling through nonlocal control-flow transfers; there are reasonable arguments on both sides, and it seems likely that both are viable options in most circumstances, and which is better depends on those circumstances. (For example, lazy evaluation or catastrophic consequences attached to software crashes would seem to me to weigh heavily on the side of using error values, while interactive REPL-style usage would seem to me to weigh on the side of nonlocal control flow, perhaps with Common-Lisp-style restarts.) My point was narrower: in this particular case, using error values analogous to NaNs, rather than shutting down the SRI, would have saved the rocket, without posing the risk of using garbage data that C's semantics pose. In this particular case, they would have been better. It's possible that, in other cases, perhaps even in other places in the SRI firmware, using error values would have been worse than unwinding the stack or shutting down the SRI. But in this case they would have been better. (If you aren't convinced of that narrow point, you should probably read the report from the Lions board of inquiry.)
    - blub 7y ago
      I think I see what you mean. I'm personally interested in generally applicable rules, so the fact that it could have worked in this case doesn't help me decide what to so when designing another system. In the general case, the Ada behavior of detecting and signaling numeric errors seems to be the only robust choice to me. The alternative could only be acceptable if it's proven that the algorithms fail safe in the presence of tainted data.
carlmr 7y ago
> Rust just ignoring it is a good thing? Rust tries to give you zero-cost abstractions where possible. Overflow checks aren't zero-cost, therefore they're disabled in release mode. Otherwise when safety can be done at zero-cost (at runtime) Rust will usually do that. I agree with you though that the exception might have helped in many other situations, especially if a simulation catches it early on. I would still say from gut feeling that ADA makes the safer decision on average.
- Fabien_C 7y ago
  I don't see the point with "zero-cost abstractions", overflow check is not an abstraction. And of course the run-time checks can also be disabled for Ada of course, and usually are for release build.
  - johnisgood 7y ago
    And this is worth noting: > These runtime checks[1] are costly, both in terms of program size and execution time. It may be appropriate to remove them if we can statically ensure they aren't needed at runtime, in other words if we can prove that the condition tested for can never occur. > This is where the analysis done by GNATprove comes in. It can be used to demonstrate statically that none of these errors can ever occur at runtime. Specifically, GNATprove logically interprets the meaning of every instruction in the program. Using this interpretation, GNATprove generates a logical formula called a verification condition for each check that would otherwise be required by the Ada (and hence SPARK) language. [1] overflow check, index check, range check, divide by zero --- So again, I do not see why Rust would shine (as some people suggested) here, Ada/SPARK can statically ensure that your program is correct and eliminate all sorts of runtime errors, including overflow.
    - steveklabnik 7y ago
      The rust compiler also removes bounds checks and such if it can statically prove that they won't occur. You don't have as much tooling to communicate it to the compiler as you do in SPARK just yet. When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.

by ajxs 7y ago

kragen 7y ago

Tainting the dataflow rather than the control flow, like a quiet NaN, would be a better solution in cases like these. It happens that the solution that was chosen was the worst choice possible, but in other cases it wouldn't have been. Probably the fact that the engineers got the case analysis wrong suggests that the methods of reasoning they were using weren't very effective. Modern formal methods might or might not have helped; guaranteeing that a piece of code is statically free of exceptions is not a terribly advanced thing to do, but really you'd like to guarantee that the variable was actually big enough. Having less code to reason about certainly would have helped. C’s choice is clearly unconscionable.

blub 7y ago
In hindsight it would have been perhaps better, but I don't think it can be said that having essentially random values in memory is better than having a controlled error handling action being executed. Is there any reference that such a course of action is preferred or beneficial?
- kragen 7y ago
  We have a lot of experience with floating-point qNaN values since IEEE 488 introduced them in 1985, and more rigorous languages than Ada — such as OCaml, Haskell, and Rust — use a generalized version of the concept for a lot of error handling. I don't think there's an open-and-shut case that error values are "preferred or beneficial" in general with respect to exception handling through nonlocal control-flow transfers; there are reasonable arguments on both sides, and it seems likely that both are viable options in most circumstances, and which is better depends on those circumstances. (For example, lazy evaluation or catastrophic consequences attached to software crashes would seem to me to weigh heavily on the side of using error values, while interactive REPL-style usage would seem to me to weigh on the side of nonlocal control flow, perhaps with Common-Lisp-style restarts.) My point was narrower: in this particular case, using error values analogous to NaNs, rather than shutting down the SRI, would have saved the rocket, without posing the risk of using garbage data that C's semantics pose. In this particular case, they would have been better. It's possible that, in other cases, perhaps even in other places in the SRI firmware, using error values would have been worse than unwinding the stack or shutting down the SRI. But in this case they would have been better. (If you aren't convinced of that narrow point, you should probably read the report from the Lions board of inquiry.)
  - blub 7y ago
    I think I see what you mean. I'm personally interested in generally applicable rules, so the fact that it could have worked in this case doesn't help me decide what to so when designing another system. In the general case, the Ada behavior of detecting and signaling numeric errors seems to be the only robust choice to me. The alternative could only be acceptable if it's proven that the algorithms fail safe in the presence of tainted data.

carlmr 7y ago

> Rust just ignoring it is a good thing? Rust tries to give you zero-cost abstractions where possible. Overflow checks aren't zero-cost, therefore they're disabled in release mode. Otherwise when safety can be done at zero-cost (at runtime) Rust will usually do that. I agree with you though that the exception might have helped in many other situations, especially if a simulation catches it early on. I would still say from gut feeling that ADA makes the safer decision on average.

Fabien_C 7y ago
I don't see the point with "zero-cost abstractions", overflow check is not an abstraction. And of course the run-time checks can also be disabled for Ada of course, and usually are for release build.
- johnisgood 7y ago
  And this is worth noting: > These runtime checks[1] are costly, both in terms of program size and execution time. It may be appropriate to remove them if we can statically ensure they aren't needed at runtime, in other words if we can prove that the condition tested for can never occur. > This is where the analysis done by GNATprove comes in. It can be used to demonstrate statically that none of these errors can ever occur at runtime. Specifically, GNATprove logically interprets the meaning of every instruction in the program. Using this interpretation, GNATprove generates a logical formula called a verification condition for each check that would otherwise be required by the Ada (and hence SPARK) language. [1] overflow check, index check, range check, divide by zero --- So again, I do not see why Rust would shine (as some people suggested) here, Ada/SPARK can statically ensure that your program is correct and eliminate all sorts of runtime errors, including overflow.
  - steveklabnik 7y ago
    The rust compiler also removes bounds checks and such if it can statically prove that they won't occur. You don't have as much tooling to communicate it to the compiler as you do in SPARK just yet. When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.