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

11–20 of 82 posts

Re: Rules for Writing Safety Critical Code (2006)

#11

Post by yitchelle »

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.

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.

Re: Rules for Writing Safety Critical Code (2006)

#12

Post by 4ad »

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.

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.

Re: Rules for Writing Safety Critical Code (2006)

#13

Post by hvidgaard »

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…

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.

Re: Rules for Writing Safety Critical Code (2006)

#14

Post by aetherspawn »

I wrote my capstone project a week ago on rolling out Simulink for automatically generating SC code en masse and minimising hand written code and manual translation.

I referenced the paper mentioned in my literature review

I would not link it here to the world to see as it is just an undergraduate project and my research did not yield a highly quantitive result, but I am applying the technique on a project right now with good success

Re: Rules for Writing Safety Critical Code (2006)

#16

Post by pjmlp »

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.

> but it's still pretty damn ultra-reliable piece of software.

Are you sure?

http://arstechnica.com/security/2016/09/linux-kernel-securit...

http://www.cvedetails.com/product/47/Linux-Linux-Kernel.html...

Re: Rules for Writing Safety Critical Code (2006)

#17

Post by 4ad »

hvidgaard wrote: post #13
kccqzy wrote: post #6

Earlier quoted context omitted.

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…

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.

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.

Re: Rules for Writing Safety Critical Code (2006)

#18

Post by 4ad »

PaulKeeble wrote: post #15

10 Rules isn't going to cut it really, its a lot more detailed than that. Here is the Spark reference manual (a standard for Ada that has been the industrial standard for decades): http://docs.adacore.com/spark2014-docs/html/lrm/

Yeah, the point of these rules (and the 31 JPL rules) is concision. Your programmers will read a 10 page coding standard, and might remember it. Nobody is going to remember hundreds of rules and hundreds of pages. They won't even read it.

In his talks Holzmann always makes the point that a coding standard is a hard sell for most people, and JPL hadn't had any success until they could come up with something simple and concise.

Post reply on HN