Live data from Hacker News

Rules for Writing Safety Critical Code (2006)

spinroot.com

51–60 of 82 posts

Re: Rules for Writing Safety Critical Code (2006)

#51
post #45

Earlier quoted context omitted.

SpaceX uses VxWorks for their hard real-time requirements: http://blogs.windriver.com/vxworks/2010/12/vxworks-helping-c... They use Linux for non-hard-real-time stuff. Their microcontrollers also do not use Linux. Coincidentally, Tesla uses QNX.

Yes for their microcontrollers they use VxWorks. But Linux is still used for the flight software (i.e. mission control).

VxWorks does not run on microcontrollers.

Re: Rules for Writing Safety Critical Code (2006)

#52
post #21

I work on software that goes to space. I believe we and NASA use the MISRA coding standard, which is effectively this but taken to extremes. If you actually want to create safety critical code I would recommend that you familiarize yourself with the MISRA ruleset and DO-178B.

If anyone is looking into this sort of stuff, you can check out the relatively new DO-178C as well, which adds some more details about tool qualification, formal methods, and model-based development. Signed, your friendly neighbourhood aerospace systems engineer.

Re: Rules for Writing Safety Critical Code (2006)

#53

Earlier quoted context omitted.

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.

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

If I wanted to learn more about open source, reliable microkernels, where would you point me?

Re: Rules for Writing Safety Critical Code (2006)

#54

Earlier quoted context omitted.

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

If I wanted to learn more about open source, reliable microkernels, where would you point me?

seL4 is the big one: https://sel4.systems/

Here's a general reference of open source microkernel operating systems: http://www.microkernel.info/

Here's a general reference for open source real time operating systems: http://www.osrtos.com/

Re: Rules for Writing Safety Critical Code (2006)

#55
Why not just call it "Rules for Writing Code"?

Who would ever, for example, consider checking the return value of some function but then think "ah, this isn't safety critical, I'm just skip writing a quick _if_ statement and then leave this as a place that mysterious bugs can arise"? Same thing with assertions.

Re: Rules for Writing Safety Critical Code (2006)

#56
post #55

Why not just call it "Rules for Writing Code"? Who would ever, for example, consider checking the return value of some function but then think "ah, this isn't safety critical, I'm just skip writing a quick _if_ statement and then leave this as a place that mysterious bugs can arise"? Same thing with assertions.

Because these rules have a cost, and sometimes the cost is not worth it for non-safety critical code. It would be a PITA for general purpose code to avoid all dynamic memory allocation.

Re: Rules for Writing Safety Critical Code (2006)

#57
post #6

An opinionated and needlessly specific list. For example, this Use minimally two assertions per function on average should've been Assert your invariants And this Do not use goto statements is a controversial advice at best, because there are several well-established goto-based patterns that produce a much cleaner code.

I would also say perhaps avoid recursion should be revised to avoid non-tail-call recursion Because the justification to avoid recursion is basically avoid running into the limit of stack, and tail-call recursion uses no stack space at all. Of course you still might end up with situations where the function does not terminate, but simple loops can do that too. In relation to Rule No.2, it is also possible to prove an…

> tail-call recursion uses no stack space at all

Not all compilers optimize tail-call recursion into - effectively - loops. And even those that can might only do so when certain compiler flags are active.

Re: Rules for Writing Safety Critical Code (2006)

#58
post #55

Why not just call it "Rules for Writing Code"? Who would ever, for example, consider checking the return value of some function but then think "ah, this isn't safety critical, I'm just skip writing a quick _if_ statement and then leave this as a place that mysterious bugs can arise"? Same thing with assertions.

Have you met programmers?

Less snarkily, there are billions of lines of production code that don't check return values for malloc(), printf(), and so on because those failures are extremely rare and difficult to handle sensibly.

Banning dynamic allocation would ban large areas of programming language - Lisp, Python, Javascript, and so on.

Re: Rules for Writing Safety Critical Code (2006)

#59
post #56
post #55

Why not just call it "Rules for Writing Code"? Who would ever, for example, consider checking the return value of some function but then think "ah, this isn't safety critical, I'm just skip writing a quick _if_ statement and then leave this as a place that mysterious bugs can arise"? Same thing with assertions.

Because these rules have a cost, and sometimes the cost is not worth it for non-safety critical code. It would be a PITA for general purpose code to avoid all dynamic memory allocation.

With the sole exception of item (3) in that list (pertaining to dynamic allocation), which others carry a cost?

Re: Rules for Writing Safety Critical Code (2006)

#60
post #27
post #21

I work on software that goes to space. I believe we and NASA use the MISRA coding standard, which is effectively this but taken to extremes. If you actually want to create safety critical code I would recommend that you familiarize yourself with the MISRA ruleset and DO-178B.

Space software? Nice! Going to check out MISRA now. FWIW the initial page just reflects the JPL publication "The Power of Ten – Rules for Developing Safety Critical Code" by Gerard Holzmann [0] [0]: http://spinroot.com/gerard/pdf/P10.pdf

Gerard Holzmann is the main author of the formal software verification tool "spin" as well as the owner of spinroot.com. I took a class on formal verification under him at Caltech.
Post reply on HN