5 ms·

That ... feels like it defeats the purpose of designating a special, certified library for safety-critical code.

by SilasX 2y ago

estebank 2y ago
Its not so much about ensuring the best tool chain is used, but rather about setting the lowest bound of quality. By being slow moving it avoids the potential for temporary regressions. It is also ass-covering by demonstrating you followed "industry standard procedure". If you do something different, even if it is quantifiably better, it might make for a stressful deposition explaining why the worse but standard approach wasn't used instead.
AlotOfReading 2y ago
Would it make you feel better if I told you that these kinds of offerings usually also don't offer modern validation tools like sanitizers? They expect people to just wing it with whatever the proprietary IDE happens to give them. A big part of the job of safety critical development is knowing the difference between box checking best practices/regulations and building actually safe systems so you can do both.
- yjftsjthsd-h 2y ago
  I would assume the solution is to run your code through multiple compilers/toolchains - in dev, CI can run the certified compiler to make sure your code stays compatible with it, but also through modern clang/gcc with every linter and static analysis tool you can think of. Then for the "official" prod builds you use the certified compiler. Automated testing should probably use both, and even compare the behavior of binaries from each chain to look out for bugs that only exist in one. That way you get most of the benefits of both worlds (not all, since you can only write code that all compilers can handle).
  - steveklabnik 2y ago
    It isn’t. The idea is to quantify the risk. A buggy toolchain is okay if the bugs are known and you can demonstrate how you’re mitigating them. All software has bugs, you cannot rely on the idea of bug free software to ensure safety, you must have a process that is robust in the face of problems.
    - yjftsjthsd-h 2y ago
      Sure, but if you can do something to reduce the number of bugs it seems like you should still do that?
      - steveklabnik 2y ago
        I don’t disagree that in general, reducing the number of bugs is a good goal, but there’s always a limit to how far you go. It’s not like every line is formally proven, for example. Just because you can use a specific technique doesn’t mean that you must. But also I don’t work directly in these industries and so maybe my impression of this aspect of their processes is incorrect.
        tialaramex 2y ago
        I actually think far more of these safety of life standards should require formal proof. IMNSHO the standards were set so low so that C++ could clamber over the low bar, and it's a happy consequence in some sense that Rust has no trouble clearing it, but the bar should be raised considerably instead. Software crucial to the safe operation of an airliner ought to be proven correct, not just slapped together in any of the general purpose languages, including Rust and then subject to a bit more process than for a web app.
        adrianN 2y ago
        That would explode the costs for marginal safety improvements. I think the same effort spent on better requirement engineering would yield more payoff.
  - AlotOfReading 2y ago
    That's a common partial solution, but it's not complete. For example, it essentially requires you to be able to observe all safety-relevant behaviors of the code in both compilers. This is a much more comprehensive degree of validation than almost any system actually achieves. You also run into issues where the behaviors you're observing (e.g. low bits in floating point results) depend on intimate details of codegen that aren't identical between compilers. The complete solution depends on the application and the integrity level. It's not one size fits all, but rather about producing documentation showing you've considered various failure modes and developed mitigations for them (or otherwise accept the risk). Sometimes that's binary analysis of the compiled output to ensure it meets some formal model, sometimes that's a formally proven, decent compiler like concert, and so on. An additional wrinkle is that the business model for high integrity compilers can also be a huge obstacle here. Some charge seats by how many people have modified the code that's running through the compiler. These aren't cheap licenses either, so companies have a large incentive not to use methodologies that require many eyes making all bugs shallow. There are also issues running these compilers in CI. They might require online license verification on every file, for example, or not allow ephemeral licensing at all.
darthrupert 2y ago
If the compiler crashes, no safety-breaking code was generated.

That ... feels like it defeats the purpose of designating a special, certified library for safety-critical code.

by SilasX 2y ago

That ... feels like it defeats the purpose of designating a special, certified library for safety-critical code.

Its not so much about ensuring the best tool chain is used, but rather about setting the lowest bound of quality. By being slow moving it avoids the potential for temporary regressions. It is also ass-covering by demonstrating you followed "industry standard procedure". If you do something different, even if it is quantifiably better, it might make for a stressful deposition explaining why the worse but standard approach wasn't used instead.

AlotOfReading 2y ago

Would it make you feel better if I told you that these kinds of offerings usually also don't offer modern validation tools like sanitizers? They expect people to just wing it with whatever the proprietary IDE happens to give them. A big part of the job of safety critical development is knowing the difference between box checking best practices/regulations and building actually safe systems so you can do both.

yjftsjthsd-h 2y ago
I would assume the solution is to run your code through multiple compilers/toolchains - in dev, CI can run the certified compiler to make sure your code stays compatible with it, but also through modern clang/gcc with every linter and static analysis tool you can think of. Then for the "official" prod builds you use the certified compiler. Automated testing should probably use both, and even compare the behavior of binaries from each chain to look out for bugs that only exist in one. That way you get most of the benefits of both worlds (not all, since you can only write code that all compilers can handle).
- steveklabnik 2y ago
  It isn’t. The idea is to quantify the risk. A buggy toolchain is okay if the bugs are known and you can demonstrate how you’re mitigating them. All software has bugs, you cannot rely on the idea of bug free software to ensure safety, you must have a process that is robust in the face of problems.
  - yjftsjthsd-h 2y ago
    Sure, but if you can do something to reduce the number of bugs it seems like you should still do that?
    - steveklabnik 2y ago
      I don’t disagree that in general, reducing the number of bugs is a good goal, but there’s always a limit to how far you go. It’s not like every line is formally proven, for example. Just because you can use a specific technique doesn’t mean that you must. But also I don’t work directly in these industries and so maybe my impression of this aspect of their processes is incorrect.
      - tialaramex 2y ago
        I actually think far more of these safety of life standards should require formal proof. IMNSHO the standards were set so low so that C++ could clamber over the low bar, and it's a happy consequence in some sense that Rust has no trouble clearing it, but the bar should be raised considerably instead. Software crucial to the safe operation of an airliner ought to be proven correct, not just slapped together in any of the general purpose languages, including Rust and then subject to a bit more process than for a web app.
        adrianN 2y ago
        That would explode the costs for marginal safety improvements. I think the same effort spent on better requirement engineering would yield more payoff.
- AlotOfReading 2y ago
  That's a common partial solution, but it's not complete. For example, it essentially requires you to be able to observe all safety-relevant behaviors of the code in both compilers. This is a much more comprehensive degree of validation than almost any system actually achieves. You also run into issues where the behaviors you're observing (e.g. low bits in floating point results) depend on intimate details of codegen that aren't identical between compilers. The complete solution depends on the application and the integrity level. It's not one size fits all, but rather about producing documentation showing you've considered various failure modes and developed mitigations for them (or otherwise accept the risk). Sometimes that's binary analysis of the compiled output to ensure it meets some formal model, sometimes that's a formally proven, decent compiler like concert, and so on. An additional wrinkle is that the business model for high integrity compilers can also be a huge obstacle here. Some charge seats by how many people have modified the code that's running through the compiler. These aren't cheap licenses either, so companies have a large incentive not to use methodologies that require many eyes making all bugs shallow. There are also issues running these compilers in CI. They might require online license verification on every file, for example, or not allow ephemeral licensing at all.

darthrupert 2y ago

If the compiler crashes, no safety-breaking code was generated.