Boffins zapped '2,000 bugs' from Curiosity's 2 MILLION lines of code
With a $2.5bn price tag, a 350-million mile journey and 2 million lines of C and some C++ code, the only bugs NASA wants its Curiosity rover to find are those possibly beneath the Martian surface. And it may not be a particularly glamorous job, but software analysis outfit Coverity was the company tasked with "ensuring that …
This topic is closed for new posts.
Re: I wonder...
They use a combination of Tarot cards, tea leaves, and a level 3 summoning grid.
Re: I wonder...
"..how many lines of code are in the Coverity software, and what do they use to search for errors in that."
Thats the problem with proving software - how do you know the tests or the proof is correct? In theory you could end up in an infinite regression of testing - prove the software, prove the proof, prove the proof of the proof etc etc. I guess at some point you just have to draw a line and say "its as good as its humanly possible to get".
Re: I wonder...
boltar says: "Thats the problem with proving software - how do you know the tests or the proof is correct? In theory you could end up in an infinite regression of testing - prove the software, prove the proof, prove the proof of the proof etc etc. I guess at some point you just have to draw a line and say "its as good as its humanly possible to get"."
It is actually not as bad as that. Proof systems usually have a very small set of primitive rules and combining forms that are verified by hand, and then all proofs are build up from this set of primitive rules and combining forms. This means that errors in the code that generates the proofs can not generate faulty proofs (at least not without triggering run-time errors). Basically, the worst a programming error in the proof generator can cause is failure to produce any proof, but faulty proofs can not be made. Assuming, of course, that the small kernel of primitive rules is correct, but great effort has been made to ensure this.
When proving behaviour about programs, a much larger problem is whether the formal specification of the programming language actually corresponds to the behaviour of running programs: The compiler may not conform to the specified standard. Hence, you often verify the generated machine code instead of the source code. That way, you don't have to trust the compiler and you don't need a formal language specification for the high-level language. What you need instead is a formal specification of the machine language, but that is often easier to make. A problem is, though, that the machine language does not have information about the types of values (are they integers or pointers, and pointers to what?). So you sometimes make the compiler generate typed assembly language. The types can be checked by the proof system and help verification of the correctness of the code relative to a specification. Obviously, few "standard" compilers generate typed assembly language that can be verified this way.
Problem lines of code
Rover.PrimaryTarget = "Conner, John";
Rover.AI = new AI("Terminate");
Re: Problem lines of code -- original lines
No, those were the corrected lines. The original lines were:
Rover.PrimaryTarget = "Appleseed, John";
Rover.AI = new AI("Germinate");
They had been intended as a stub for testing, but some bright spark figured that they were just what a (nearly) barren planet needed and left them in without authorization.
Re: Problem lines of code -- original lines
Imagines a Dalek meeting Curiosity.
"YOU WILL BE INSEMINATED!!!"
Re: Problem lines of code -- original lines
You do know all Daleks are gay, right?
Proof
http://www.youtube.com/watch?v=ZfxyvrW-lUs
Why C
While there is a lot of "religion" in choice of programming language, I find C a particularly bad choice for writing zero-defect software: There is not enough information in the types to catch even simple mistakes (such as writing x=y instead of x==y) at compile time, memory deallocation is unchecked and unsafe, lots of behaviour is specified as "implementation dependent" or "undefined" in the standard, and so on.
As a result, you have to throw a lot of complex analysis after the program just to catch errors that in most other languages would have given a compile-time error message or which could not even occur in these languages. And to make the analysis tractable, programmers are forced to use only the simplest parts of the language, as the more complex parts are too difficult to analyse. Of course, this allows Stanford researchers to write a few scientific papers and Coverisity to earn a few bucks. But that seems like a very costly solution.
I don't suggest using one of the newer mainstream languages, because while they have better type systems, they are not suited for small computers running real-time software. But there are plenty of languages designed for ease of verification and control of resources. Some of these even have compilers that are verified to generate correct code, which I don't think any (full) C compiler is.
Re: Why C
Agreed but I am about 100% sure they would have used a safe subset (knocking out impl. dep. behaviour & more) + a whole lot of other procedures & doubtless other static checkers. Their figure of 1 bug per 1000 lines suggests that strongly. Also they probably define a bug more stringently than normal software dev process would.
Odd claims like checking for null pointer dereferences, erm, you can statically do that I'm pretty sure, with suitable restrictions, much like const propagation I guess.
I'd very much like current software dev processes - which are horrible - to grow up and become a boring engineering job. Yes, boring. Less 'excitement' for me, fewer 'thrills' for the user. Less crunch time, more having-a-life. Also would winnow the actual able guys & gals from egoists and bullshitters and plain bad.
(this article does read suspiciously like an advert, no?)
Re: Why C
I agree. They should have used assembly language. That way, what you see is what you get.
Re: Why C
Well, as they are running on the Wind River VxWorks RTOS, it could be that the choice of <insert your favourite language here> is not supported. I have not programmed in VXWorks, but looking at the design spec's for Curiosity, I would imagine that getting as close to the hardware interface as possible is a requirement. Would <insert your favourite language here> support real time control of the the devices?
Also, JPL programs in C as a language of choice. I have worked with them (briefly) and although I was not working in C, it quickly became apparent that all their examples and code base was in C. Well, actually, some of the examples were in (shudder) FORTRAN.
Mine's the one with the card deck and manual hole punch in the pocket.
Re: Writing zero-defect software
I for one would like to hear more about this magical language that allow me to build software with zero defects.
Re: Why C
JPL's C Coding Standard is available online (http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf) and makes good reading for any C programmer, really.
Re: Writing zero-defect software
Any language allows you to build software with zero defects. I if you fail to take advantage of the opportunity, then that is your fault.
Re: Writing zero-defect software
Here's the guideline for ESA's Galileo System (a monstrous "industrial policy" effort gone badly wrong, but that's another problem)
Galileo Software Standard (GSWS) defines 5 different software development assurance levels (SW-DAL), which determine the situations in which software that has passed a given DAL can be used:
Level A: Software whose anomalous behaviour would cause or contribute to a failure resulting in a catastrophic event.
Level B: Software whose anomalous behaviour would cause or contribute to a failure resulting in a critical event.
Level C: Software whose anomalous behaviour would cause or contribute to a failure resulting in a major event.
Level D: Software whose anomalous behaviour would cause or contribute to a failure resulting in a minor event.
Level E: Software whose anomalous behaviour would cause or contribute to a failure resulting in a negligible event.
Programming languages allowed according to [GSWS-SWENG-1180]:
Ada, Assembler, C: any DAL
C++: Allowed only for DAL D and E (except if you can get a waiver)
Java: Allowed only for DAL E (except if you can get a waiver)
So yeah, C is nice. Though the GSWS also says, no dynamic memory allocation and other casualness. Also, independent validation and verification by a second team if above DAL D etc. It's a telephone book of requirements..
Re: Why C
That standard's comments are quite common for embedded and (AFAIK) high reliability stuff, I should have remembered the no-alloc rules and no-side effects rules, at the very least. I'll go through the rest.
Thanks (and to Destroy All Monsters) for some actually informative posts.
Re: Why C
I'd agree with certain elements of such software not being written in C, but i'm mystified by some of your comments....
"There is not enough information in the types"
I'm not sure what you're trying to say here - I certainly can't parse it. Short of explicitly casting pointers to things to stupid values, C is perfectly well aware of what types things are.
"to catch even simple mistakes (such as writing x=y instead of x==y) at compile time"
If y is assignable to x, then how do you know that 'x = y' is not the intention. If y is not assignable / convertible to x then an error will (or can) be produced with any half decent / current standards compliant C (or, indeed, C++) compiler. This assignment versus equality problem is common to many languages, but is impossible to classify as an error (because it's not, if the types are assignable/convertable) - this is part of the reason that every C compiler i've used, within the last 10 years at least - many long before that - warns about it.
"lots of behaviour is specified as "implementation dependent" or "undefined" in the standard, and so on."
They mostly tell you what not to do. This is useful. It is perfectly possible to write well-defined C programs - alas in the wrong hands (and even the right ones) it's all to easy to write ones that aren't. C is not alone in that, just jolly good at it...
Re: Why C
I love the fact that the reviewers included K&R ...yes, that K&R. To say nothing of Doug McIlroy. It would be like me calling Steve Jobs for a homework essay on ego. Brilliant.
Re: Why C
>makes good reading for any C programmer
Not just C programmers. A lot of the rules in the JPL Coding Standard are worth following in any imperative language. Also it is written in an admirably down to earth style.
Re: Why C
I think the main reason is that C is easier to statically analyze, and this seems to be a method of bug finding they rely on heavily.
Re: Why C
You *might* like to check the MISRA coding rules.
They were developed for *automotive* applications like engine management units brake and gear change systems.
IE *lots* of meatsack testing it and if it fails someone *will* end up going "squish".
Dynamic memory allocation is *explicitly* ruled out as "unsafe" (at any speed).
Re: Why C
JPL's *other* core area is mission planning and orbital planning.
Some of the apps they use for this are highly numerical and have been under development for a *long* time.
C is easier to statically analyze,
choke.. arf, arf, arf, arf, arf......
C is 'easier to statically analyze' because by definition the compiler is unwilling to prevent whole classes of static faults, thus leaving [whole classes of static faults] available for a seperate static analysis program to detect.
Re: Why C
May I draw your attention to "Structured programming" by Linger, Mills & Witt.
It describes the underlying tools used by the teams that built the the software for the Shuttle (and whose work *defined* what the term CMM5 means).
AFAIK most of their key innovations were in *procedure* rather than actual software tools, although their change management system could give cradle-to-grave histories on every line of code in the source (not sure if this is SOP for *all* modern CMS's these days).
*sticking* to the process when deadlines loom is another matter.
I'd also recommend Harlan Mills "Software Productivity" for a very neat way to establish how many bugs are *likely* to be left in a program. Implementing it however may be quite tricky (but I bet it would make a hell of a product).
Re: Why C
Forgive my ignorance on this subject, but aren't a lot of operating systems and compliers written in C? If that's the case then using another language whose complier is written in C would be worse, since then you would have to debug both code and complier.
Some deadline!
"... ensuring that every software defect is found and fixed before launch."
Just for a moment I thought you said "... before lunch."
advertising?
Well I'm interested. Anyone else use coverity? All the static analysis tools I've used fail to find anything terribly complex. A tool that could spot data consistency errors across threads would be nice.
Also, the language debate appears to be winding down so... C++ is the best language ever because recursive template FFT implementations are the fastest.
Re: advertising?
You should have a look at spinroot.com who do spin. Its old and reliable but not easy to use because you dont' start from your code but have to make a model manually.
Cheap eastern labour at CERN.
"The cost [...] has been evaluated, taking into account realistic labor prices in different countries. The total cost is X (with a western equivalent value of Y)" [where Y>X]
source: LHCb calorimeters : Technical Design Report
ISBN: 9290831693 http://cdsweb.cern.ch/record/494264
Well, well, well.
Talk all the shit you want about us poor dumb Americans. We landed a nuclear powered rover on another planet, despite a buggy system. So suck it.
Re: Well, well, well.
Suck it?
Err thanks but no thanks my American cousin. I prefer my daily semen intake to be free of Cafinee, Fat & Prozac.
Paris cos she likes a good sloppy slurp so she does!
"Mein Führer, I can walk!"
"We landed a nuclear powered rover on another planet, despite a buggy system!!"
You shall now picture Dr. Strangelove rolling his wheelchair speedily after the departing rover into the sunset, possibly to Yakety Sax or a song by Vera Lynn.
Helldesk
"after all, there's no service desk on Mars"
No, but the call centre is there.
...to catch even simple mistakes (such as writing x=y instead of x==y) at compile time...
Wouldn't the missing 'if' or equivalent clause be a dead giveaway? Sorry, haven't programmed in C this millenium, but...
Re: ...to catch even simple mistakes (such as writing x=y instead of x==y) at compile time...
I have to tell you the sad truth...
if (x=y) {
}
is a reasonable statement in C.
Re: ...to catch even simple mistakes (such as writing x=y instead of x==y) at compile time...
Yes, but is probably not what you want. So set the compiler to warn about such things, and further set the compiler to treat all warnings as errors. If you really, really want that construct as written, then put in a pragma or some other thing so for that line, the compiler does not treat that as a warning. Your program will compile, and there will be a rather obvious sentinel to the next poor sod who has to maintain your wonderfulness that you did something a little unconventional (because we all know that real C programmers can't be arsed to write comments explaining that they're doing something unconventional, now could we?)
Coverity ad
I wonder what there spin would have been if it had crashed into the sun ?
interesting that they trust their software sooooo much, they had to wait till the tested code was switched off before claiming victory.
Re: Coverity ad
> I wonder what there spin would have been if it had crashed into the sun?
"Our software mines ENORMOUS AMOUNTS OF DELTA-V out of the VACUUM!"
I don't know about you guys, but I'm pretty sure my last 1000 lines of code have more than one defect...
"Warning 1 of 682..."
I for one would welcome....
"it's not unusual to find approximately 1 defect for every thousand lines of code ", given the some of the developers I have to work with, 1 defect per 1000 lines of code would be a red letter day.
Anonymous because ....do I really need to spell it out?
Re: I for one would welcome....
I'm thinking that the easiest way of reducing the bug-introduction rate would be to put more statements on each line.
Not just Coverity
Other reports listed a whole collection of static analysis tools used, most of the major vendors, plus some NASA homegrown tools. Sourcing articles from Coverity press releases by any chance?
This topic is closed for new posts.
