5 ms·

> An opinionated and needlessly specific list Not really. Gerard Holzmann is in charge of software at NASA/JPL. Each rule comes from experience with a mission

by 4ad 10y ago

> An opinionated and needlessly specific list Not really. Gerard Holzmann is in charge of software at NASA/JPL. Each rule comes from experience with a mission loss that would have been prevented if people had implemented that rule. They also help static analysers become more accurate. These rules are specific to ultra-reliable embedded software, flight software or software for life-critical equipment. They are not really relevant for most normal programming.

adrianN 10y ago
That doesn't mean that the rules are perfect. There haven't been that many mission losses to have a large corpus of data and finding a root cause of an accident might not lead to the best rules. "The rocket wouldn't have blown up if you asserted this here" doesn't mean that adding a large number assertions necessarily leads to better code.
- erikbye 10y ago
  A lot of wisdom comes from simulations as well.
huhtenberg 10y ago
Sure and this list likely worked well in the NASA/JBL context. The point being is it needlessly specific as a generic advice. At the risk of stating the obvious, a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel, which may not be flying every space probe, but it's still pretty damn ultra-reliable piece of software.
- yitchelle 10y ago
  An ultra reliable software comes down to knowing its behaviour fully in its released form. If the code has 100s of gotos and their paths are mapped out and its ramifications of the paths are clearly understood for all scenarios, then it is still reliable as its full behaviour is understood and is safe.
- 4ad 10y ago
  Talk about missing the point and the whole context around mission-critical software. > a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel There are many ways to do error cleanup that do not involve goto, and there are many bad ways to use goto. A static analyser can't decide if you do "good goto" or "bad goto", but it's easy to ban goto outright and avoid all the "bad gotos". You pay the price in terms of programmer work (he has to do something different), but you gain better static analysis and eliminate a full class of bugs. This tradeoff makes sense for JPL and other people who do mission-critical of life-critical software. It might not make sense for the Linux kernel or most C software. Mission-critical is not the place where you want to rely on programmers to do their work correctly (goto fail anyone?). You rely on specific methodology, standards, and static analysis.
  - OskarS 10y ago
    The Linux kernel is not mission critical? Many of those mission critical systems probably run off of a Linux kernel, you know. I think the point is that while it is potentially a good rule for mission critical code, it is not essential. There are other ways as well.
    - 4ad 10y ago
      No, they don't. The Linux kernel is not a RTOS. Most JPL projects use VxWorks.
    - pjmlp 10y ago
      No it isn't. Operating systems like INTEGRITY RTOS are. http://www.ghs.com/products/rtos/integrity.html http://www.ghs.com/products/rtos/integrity.html Which is why GNU/Linux gets packed into his own little sandbox running on top of INTEGRITY.
      - kristoffer 10y ago
        Well, SpaceX claims to be running their flight software on Linux so it is critical to their missions at least :)
- pjmlp 10y ago
  > but it's still pretty damn ultra-reliable piece of software. Are you sure? http://arstechnica.com/security/2016/09/linux-kernel-security-needs-fixing/ http://arstechnica.com/security/2016/09/linux-kernel-securit... http://www.cvedetails.com/product/47/Linux-Linux-Kernel.html?vendor_id=33 http://www.cvedetails.com/product/47/Linux-Linux-Kernel.html...
- naasking 10y ago
  > [Linux is] still pretty damn ultra-reliable piece of software. It's really not. I don't think you have a good sense of how reliable the systems in this space really are. Firmwares and other ultra-reliable systems typically use microkernels, and there are billions of units of verified L4 microkernels out there. Linux can't even dream of approaching this level of reliability.
  - unethical_ban 10y ago
    If I wanted to learn more about open source, reliable microkernels, where would you point me?
    - naasking 10y ago
      seL4 is the big one: https://sel4.systems/ https://sel4.systems/ Here's a general reference of open source microkernel operating systems: http://www.microkernel.info/ http://www.microkernel.info/ Here's a general reference for open source real time operating systems: http://www.osrtos.com/ http://www.osrtos.com/
      - JoachimSchipper 10y ago
        seL4 is really sexy, but I don't think it's anywhere near the most-used one?
        nickpsecurity 10y ago
        OKL4 if we're going with the phone example. They stopped open-sourcing it by version 4.0 but someone should be able to dig up OKL4 3.0 somewhere.

by 4ad 10y ago

adrianN 10y ago

That doesn't mean that the rules are perfect. There haven't been that many mission losses to have a large corpus of data and finding a root cause of an accident might not lead to the best rules. "The rocket wouldn't have blown up if you asserted this here" doesn't mean that adding a large number assertions necessarily leads to better code.

erikbye 10y ago
A lot of wisdom comes from simulations as well.

huhtenberg 10y ago

Sure and this list likely worked well in the NASA/JBL context. The point being is it needlessly specific as a generic advice. At the risk of stating the obvious, a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel, which may not be flying every space probe, but it's still pretty damn ultra-reliable piece of software.

yitchelle 10y ago
An ultra reliable software comes down to knowing its behaviour fully in its released form. If the code has 100s of gotos and their paths are mapped out and its ramifications of the paths are clearly understood for all scenarios, then it is still reliable as its full behaviour is understood and is safe.
4ad 10y ago
Talk about missing the point and the whole context around mission-critical software. > a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel There are many ways to do error cleanup that do not involve goto, and there are many bad ways to use goto. A static analyser can't decide if you do "good goto" or "bad goto", but it's easy to ban goto outright and avoid all the "bad gotos". You pay the price in terms of programmer work (he has to do something different), but you gain better static analysis and eliminate a full class of bugs. This tradeoff makes sense for JPL and other people who do mission-critical of life-critical software. It might not make sense for the Linux kernel or most C software. Mission-critical is not the place where you want to rely on programmers to do their work correctly (goto fail anyone?). You rely on specific methodology, standards, and static analysis.
- OskarS 10y ago
  The Linux kernel is not mission critical? Many of those mission critical systems probably run off of a Linux kernel, you know. I think the point is that while it is potentially a good rule for mission critical code, it is not essential. There are other ways as well.
  - 4ad 10y ago
    No, they don't. The Linux kernel is not a RTOS. Most JPL projects use VxWorks.
  - pjmlp 10y ago
    No it isn't. Operating systems like INTEGRITY RTOS are. http://www.ghs.com/products/rtos/integrity.html http://www.ghs.com/products/rtos/integrity.html Which is why GNU/Linux gets packed into his own little sandbox running on top of INTEGRITY.
    - kristoffer 10y ago
      Well, SpaceX claims to be running their flight software on Linux so it is critical to their missions at least :)
pjmlp 10y ago
> but it's still pretty damn ultra-reliable piece of software. Are you sure? http://arstechnica.com/security/2016/09/linux-kernel-security-needs-fixing/ http://arstechnica.com/security/2016/09/linux-kernel-securit... http://www.cvedetails.com/product/47/Linux-Linux-Kernel.html?vendor_id=33 http://www.cvedetails.com/product/47/Linux-Linux-Kernel.html...
naasking 10y ago
> [Linux is] still pretty damn ultra-reliable piece of software. It's really not. I don't think you have a good sense of how reliable the systems in this space really are. Firmwares and other ultra-reliable systems typically use microkernels, and there are billions of units of verified L4 microkernels out there. Linux can't even dream of approaching this level of reliability.
- unethical_ban 10y ago
  If I wanted to learn more about open source, reliable microkernels, where would you point me?
  - naasking 10y ago
    seL4 is the big one: https://sel4.systems/ https://sel4.systems/ Here's a general reference of open source microkernel operating systems: http://www.microkernel.info/ http://www.microkernel.info/ Here's a general reference for open source real time operating systems: http://www.osrtos.com/ http://www.osrtos.com/
    - JoachimSchipper 10y ago
      seL4 is really sexy, but I don't think it's anywhere near the most-used one?
      - nickpsecurity 10y ago
        OKL4 if we're going with the phone example. They stopped open-sourcing it by version 4.0 but someone should be able to dig up OKL4 3.0 somewhere.