Live data from Hacker News

Rules for Writing Safety Critical Code (2006)

spinroot.com

61–70 of 82 posts

Re: Rules for Writing Safety Critical Code (2006)

#61

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

For an open source analyzer library you might look at IKOS (https://ti.arc.nasa.gov/opensource/ikos/).

Re: Rules for Writing Safety Critical Code (2006)

#62
post #27

Earlier quoted context omitted.

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.

As an anecdote, spin was used in Plan 9 to validate the kernel scheduler and the IL network protocol. It was also used to validate a very early version of the Go scheduler.

Re: Rules for Writing Safety Critical Code (2006)

#63
post #27

Earlier quoted context omitted.

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.

Gerard is an ACM Fellow and a member of the NAE, and has been a leader in reliable software for NASA since he came to JPL from Bell Labs.

Re: Rules for Writing Safety Critical Code (2006)

#64
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.

1) Some languages have tail call optimization and sometimes recursion is the clearest way to express an idea.

2) Requiring a fixed upper bound when iterating a collection of objects is a direct contradiction of the ZOI rule[0]. Most programs should not place arbitrary boundaries on the number of objects they'll operate on. This is better adapted to systems with relatively fixed databases and a predictably low volume of operator and sensor input (i.e. flight management computers, train control systems) more than internet services.

7) "For this reason, most coding guidelines for safety critical software also forbid the use of all ansi standard headers like string.h, stdlib.h, stdio.h" should speak for itself.

9) Is pretty C/C++ specific.

[0] https://en.wikipedia.org/wiki/Zero_one_infinity_rule

Re: Rules for Writing Safety Critical Code (2006)

#65
post #51

Earlier quoted context omitted.

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.

Don't know your definition of microcontroller but VxWorks runs on e.g. Cortex-M3/4, MIPS, 68K, SH, SparcV8, PowerPC thus including some devices I could microcontrollers. But there is no clear cut definition of microcontroller, microprocessor, SoC, whatnot.

Re: Rules for Writing Safety Critical Code (2006)

#66

Earlier quoted context omitted.

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.

Quite often, when time you suggest using a loop rather than a tail call, people pop up to tell you that the code is neater as a tail call. So I'm assuming the comment about ugliness is a way of heading off these people ;)

I'm happy to argue that in C, it's never neater to write a loop as a tail call. Tail calls aren't guaranteed to compile into a goto, so it can be difficult to say whether it's going to end up with a call or a goto - even on a case-by-case basis. And if you write a tail call expecting a goto, and you get a call, obviously you can't just give up and go home - you'll need to rewrite it as a loop, just like you could have done in the first place. This does not strike me as less ugly than just writing that loop.

I know people like to do things the roundabout way, by writing one thing, certain that the compiler will do something else, and then saying this code is more clear rather than less so - but I've never quite understood why. A better rule of thumb to my mind is that if you want something particular to happen: write the code that way.

(I'm not denying an annotation would help - because then at least you'd know statically when you need to rewrite your code as a loop, rather than having to wait until something bad happens. Though... maybe if nothing bad ever happens... it's fine after all...? Sheesh. Ask a philosopher. Too much for me!)

Re: Rules for Writing Safety Critical Code (2006)

#67
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.

I'm writing a quick program that's supposed to compute something and print out the answer. I don't check the return value of printf(). Why not?

1. printf almost never fails. If it does, I'm just going to re-run the program. If that doesn't work, I'll reboot and then re-run. On average, I waste less time with that approach than with checking the return value of printf.

2. If printf fails, what am I going to do? Print out an error message? But that might fail, too. Log something? That could also fail. Should I check the return values of those attempts, too?

But safety-critical code is usually not calling printf - it may not have a conventional output device at all. (It should have some mechanism for alerting the operator if there are failures, though.)

Re: Rules for Writing Safety Critical Code (2006)

#69
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.

1) Some languages have tail call optimization and sometimes recursion is the clearest way to express an idea. 2) Requiring a fixed upper bound when iterating a collection of objects is a direct contradiction of the ZOI rule[0]. Most programs should not place arbitrary boundaries on the number of objects they'll operate on. This is better adapted to systems with relatively fixed databases and a predictably low volume…

> Most programs should not place arbitrary boundaries on the number of objects they'll operate on

I think this can be argued both ways. The classic stateless pipe programs, sure, they can take as many lines as you want. User-facing programs? It can be worth imposing fairly small limits just so you don't have to worry about pathological behavior and security risks. (What happens if someone pastes a million lines of text into a small box, etc)

Re: Rules for Writing Safety Critical Code (2006)

#70

Earlier quoted context omitted.

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/

seL4 is really sexy, but I don't think it's anywhere near the most-used one?
Post reply on HN