Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Rules for Writing Safety Critical Code (2006)

spinroot.com

Post reply on HN
Print view View original

31–40 of 82 posts

Re: Rules for Writing Safety Critical Code (2006)

#31

Post by 4ad »

OskarS wrote: post #28
4ad wrote: post #12

Earlier quoted context omitted.

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 t…

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.

No, they don't. The Linux kernel is not a RTOS. Most JPL projects use VxWorks.

Re: Rules for Writing Safety Critical Code (2006)

#32

Post by heisenbit »

kccqzy wrote: post #6
huhtenberg wrote: post #3

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…

And during the maintenance phase someone modifies the code and what was pure tail recursion becomes something else and literally blows up the rocket.

The whole point of these rules is defensive programming. Programming not what is correct but what is robust i.e. if anything breaks it still produces possibly suboptimal but not catastrophic results.

Re: Rules for Writing Safety Critical Code (2006)

#33

Post by lugus35 »

michaelt wrote: post #22

Rules like avoiding recursion and loop upper bounds are partly justified by helping code analyzers to prove executions are bounded. Does anyone have experience performing formal static analysis on code? And if so, are there any open-source examples of the state-of-the-art tools being used on nontrivial problems? I've been looking at this recently, but I've never seen a proof of reasonably standard function like, say,…

Open Source tools are way behind commercial software. Just look at PolySpace Code Prover for example:

https://mathworks.com/products/polyspace-code-prover/

ou PolySpace bug finder :

https://mathworks.com/products/polyspace-bug-finder/

Re: Rules for Writing Safety Critical Code (2006)

#34

Post by pjmlp »

OskarS wrote: post #28
4ad wrote: post #12

Earlier quoted context omitted.

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 t…

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.

No it isn't.

Operating systems like INTEGRITY RTOS are.

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.

Re: Rules for Writing Safety Critical Code (2006)

#35

Post by pjmlp »

nstj wrote: post #27
ti32x wrote: 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

MISRA only goes thus far.

For writing safe code in C, you should also check Frama-C and CERT Secure Coding Standards.

http://frama-c.com/

https://www.securecoding.cert.org/confluence/display/seccode...

Even better, get the algorithms written in a theorem prover which is guaranteed to generate reliable safe C code.

This is approach taken by Microsoft with P Language(Windows USB device driver stack) and F* (new TLS implementation).

Re: Rules for Writing Safety Critical Code (2006)

#36

Post by 4ad »

pja wrote: post #29
4ad wrote: post #17

Earlier quoted context omitted.

Apart from that, TCO destroys information that is valuable for debugging (especially for non-recursive tail calls), exactly what you want to avoid in safety-critical software.

Manual conversion to a loop also destroys the same information, so it’s a wash either way on that front.

You can't convert arbitrary tail calls to a loop. You can only convert recursive tail calls to a loop. The information loss associated with non-recursive tail calls is great. It's true that recursive tail calls lose less information, but it is not true that it's equivalent to the information lost in a loop. In a loop you always have access to {head, current, tail} while in a tail call you might (subject to algorithm and compiler optimization) only have access to {current, head|tail}, depending if the loop goes forwards or backwards.

Re: Rules for Writing Safety Critical Code (2006)

#39

Post by naasking »

bartread wrote: post #24
hvidgaard wrote: post #13

Earlier quoted context omitted.

Recursion is recursion. Tail recursion is optimized away by the compiler except when it isn't (I've seen bugs with this exact setup more than once), but now you have to verify that the compiler actually does this. It's simpler to just avoid it all together unless you want to formally verify the recursion depth.

Exactly. Tail recursion can always be rewritten as a loop. The code might be uglier but at least you have a better idea of how it's going to behave after compilation.

> The code might be uglier but at least you have a better idea of how it's going to behave after compilation.

The fact that it's uglier suggests you'd have less of an idea how it's going to behave than simple tail recursion. That said, I agree with the idea that if you're after tail recursion, an annotation that the compiler checks that ensures the call is properly tail recursive is a good idea.

Re: Rules for Writing Safety Critical Code (2006)

#40

Post by naasking »

huhtenberg wrote: post #8
4ad wrote: post #4

Earlier quoted context omitted.

> 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 re…

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.

Post reply on HN