Making robust software: the “Mars Code” talk (2012) | Hacker News Reader

Making robust software: the “Mars Code” talk (2012)

verticalsysadmin.com

102 pointsvog43 comments

Dr Holzmann's "The Power of 10: Rules for Developing Safety-Critical Code" was published in June 2006 issue of IEEE Computer Society "Computer" magazine. It is a small standard, easy to understand and remember; mechanically verifiable; and measurably effective. http://spinroot.com/gerard/pdf/P10.pdf

The only one odd here for me is the ban on de-referencing more than one level.

Even a simple linked list implementation uses double pointers to reset parent nodes.. Does anyone have insight into the risk in static analysis? Seems like it would be handled by whatever logic was handling normal pointer derefs.

Seems like the only argument is the one against function pointers, which is a pretty amazing thing to ban but at least provides logic WRT static analysis.

> "The color coding green/yellow/red had a psychological effect. The software developers worked really hard to make all the buttons go green."

There is a possible risk element of Cargo Cult'ing here. I would hope that all programmers understood why the buttons weren't green. It sounds like they would have, having been certified, and in an environment that lives and breathes code safety, but it is always worth being aware that metrics like that can have hidden consequences.

I wonder how much easier it would be to write the software in a language other than C/C++. Ada has a pretty mature toolchain for security critical software development. Where I work we still use C++, but mostly for political reasons. Rust also seems more suited for security critical engineering.

At that level of reliability, language matters surprisingly little since everything is heavily tested, reviewed, hand verified, etc... Language safety is a cheap high-value solution, but might not make sense when coupled with other more expensive safety solutions (imagine wearing a simple seatbelt with a complete safety harness, they aren't additive). C/C++ have other benefits: minimal abstraction, lots of trained up talent.

If there are no bugs, you're right. However, every bug that does ship becomes harder to debug, and so does every bug you fight with during development. The impact of bugs becomes more severe and less predictable on average (dangling reference or buffer overflow can affect pretty much anything.)

The more accurate analogy is seatbelts' utility in a car fitted with various collision avoidance devices all the way up to fully autonomous driving. I say you'd still want the seatbelt for when collision does occur after all.

Again, the assurances you get from a seatbelt are dwarfed by the safety harness, they aren't additive. That is, you are going to have to check everything very carefully anyways, anything that allows you to be less careful then isn't very useful, and can actually be counterproductive. Continuing the analogy, the cheap seatbelt kills you when combined with a fancy safety harness/ejection system; it isn't helping, and it can actually hurt.

I agree that the resulting quality doesn't really depend on language choice. I just wonder about the development cost. For example, a lot of time can be spent reviewing code and checking that no unsafe constructs are used. A safe language makes that unnecessary. Some of those checks can be automated, but in my experience there is still a lot of manual checking going on.

I think that the main advantage of C/C++ is the number of people who speak it. But my guess is that the time to train a competent programmer in a safe language can be easily saved in improved productivity.

What safer languages you would recommend?

He mentionned Ada and Rust in his initial comment.

The main advantage of C (and, to a lesser, but still very significant degree, C++) in this field -- besides the number of people who speak it -- is the availability of a great deal of mature, well-tested compilers, static analysis tools and so on.

We have about 40 years of experience writing C compilers today (and we still screw it up sometimes; C++ is... well, I mean, we have about 30 years of experience writing C++ compilers, but those are still in the "mostly right" state). Many subtleties of the language are well understood and many problems have had idiomatic, well-known, widely-used solutions for decades now.

Ada would be a good choice for such projects but for the relative flimsiness of its ecosystem. It's a great language, but its development is fairly underfunded, and back when all this stuff was happening, its future was very uncertain (it still is, I guess).

And when I say "fairly underfunded" and with a "very uncertain" future, you should understand that I mean "it used to be funded by the DoD, but with various levels of commitment" and "only a few companies, most of them government contractors, and maybe a few state institutions along with a small, but enthusiastic community were pushing for it".

Its fame on HN and Reddit may not indicate it, but Rust fares even worse in this regard. Ten years from now, Rust may not even exist anymore.

It's not only about technical merit. Projects like these would benefit a lot from being written in Ada (and Rust, too, I guess -- it's a great language), provided that there were such a well-developed ecosystem around either of them. But there isn't. E.g. when choosing their static analysis tools, these guys settled for the top 5 solutions. Top 5! They evaluated a bunch of programs and settled for the best 5. I don't think there are 5 static analysis solutions for Rust in total (and I'm pretty sure there are only two or three for Ada that have been maintained after 1999 or so).

I'd point out that C only got to this stage of tooling maturity by being around a while -- it's not like less than a year after its first "stable" release it was in that state (which is the current age of the Rust stable releases). If Rust manages enough staying power to be here in 20/30/40 years, who knows. Every grizzled and battle-hardened language ecosystem needs to start out young and a bit wild-west-ish before it can gain legitimacy and rock solid tooling.

Exactly! There's nothing really wrong with Rust -- it's a good language -- but people in this space (and in the embedded world in general, myself included) are skeptical of it simply because reliability is not only something that's inherent to a design, but also something that a) has to be a quality of an implementation, not just of the principles behind it, and b) something that has to be proven in practice, both for the principles and for the implementation.

Edit: for what it's worth, I do think it's on the right track on both accounts!

Excellent response. My default recommendation is Ada + SPARK but I can easily recommend a C subset + tooling for those reasons. Especially on the compiler issue as it's known that Ada compilers aren't what they advertise themselves to be. The static analysis observation I'm not as sure about. A combo of SPARK, safe concurrency, the monitor concept w/ restarts or failovers, and one analysis tool should cover about anything they want. There's a quality vs quantity effect in Ada vs C static analysis where I can't be sure which wins here.

The ecosystem is really weak, though. There's no doubt about that. I don't see that changing regardless of whether Ada stays around. It's why I'm excited about Rust's mainstream adoption where it might get where Ada is or exceed it as tooling improves. It's one of few times mainstream goes for The Right Thing over Worse is Better. Eiffel, esp SCOOP model, being another good example that has significant momentum. The CompSci people are doing amazing things with SCOOP extensions right now that could be implemented in an Ada successor.

So, still potential at least. Plus, at least our tooling for C is now good enough to emulate Ada's safety with the right people doing the work. Plus, we only have to buy 5 tools now. Much improvement over old days. ;)

> It's why I'm excited about Rust's mainstream adoption where it might get where Ada is or exceed it as tooling improves.

Me too! We had a great chance with Ada and we kindda wasted it. Rust is literally a second chance. This is pretty rare in tech.

C is the most widely used and deployed language in the world and it has a very long tenure. I would trust it much more with billions of dollars at stake than a less proven language like Rust. And as a C programmer, it's really not a bad language, and it makes sense for this application.

Exactly. Rust is great for deployments which can't afford such rigorous testing processes; for NASA however any abstraction above the bare minimum is just another risk.

I wonder: why this publicly funded code isn't available for download on GitHub or NASA website. Is this because Russians and Chinese can "steal" it and send another Curiosity to Mars?

It probably contains lots of proprietary code to interface with the hardware.

Hardware was also funded by tax payers.

No, hardware is produced by big companies like Lockheed Martin. They adapt their proprietary solutions for NASA.

Most of which was originally developed to fulfil some government tender; space flight is not exactly the paragon of commercial innovation.

Not a complete answer, but certain kinds of NASA tech undoubtedly has military applications.

https://en.wikipedia.org/wiki/International_Traffic_in_Arms_...

I think your question is valid nonetheless, especially for the USPS, Dept. of Education, etc.

This. I work at a space research lab and we can't even let many of our employees view mission code; let alone the public. Violating export controls in any way could cost us our funding

And still:

The second was a software bug which led to a wrong file being deleted as part of regular housekeeping activities. The fix was straightforward and was applied and the MSL continues its investigation of life on Mars. (end of the article)

There's also some similar talks/presentations on various topics related to software development for spacecrafts from the yearly Flight Software Workshop at APL: http://flightsoftware.jhuapl.edu/

Very good read. Thanks for submitting it. I like that there's significant overlap in the list in the summary and the list I produced of examples of techniques for improving software quality:

http://pastebin.com/xZ6m4T8Z

Further validates those aspects of my list. I'll keep recommending them. Most tools and the rule list are available but I see no link for scrub on his website. Is it not going to be freely distributed or just not ready for public release? More tools for code review that are field-proven is A Good Thing to have.

Yay! Glad you enjoyed it.

For those interested in the "Static Source Code Analysis" section, "Semil" is a typo for "Semmle" [1]

[1]: https://semmle.com/customers/code-exploration-at-nasa/

> For example, coding standard says every "switch" statement has to have a "default" case. grep "switch", grep "default", and you get wildly different numbers! Standards were not being followed.

Are they implying that MSL is the first time they used automated code checks?

When you can't use recursion, what data structures/algorithms do you use in place of the common data structures that often use recursion? I'm thinking of stuff like trees and quicksort. Do they even need these things?

Loops. A recursive algorithm can be transformed into an iterative looping algorithm that uses a fixed stack of memory.

There's probably no change in the algorithms. They just use non-recursive versions.

What's the gain? If you turn your recursive algorithm into an iterative one with a stack, you are sill subject to all the same problems.

They probably don't use trees and quicksort at all.

  > What's the gain?

You can prove that you won't have a stack overflow. You can calculate the maximum depth of the stack at compile time, not runtime.

Can't you also just pass a bit through the recursion that contains its depth, and halt the recursion if that number gets too high?

Yes, but that depends on making sure you get the programming logic correct, whereas with banning recursion outright, it can be tested automatically.

Well, you can either prove that you won't have a stack overflow at the original program, or you can not guarantee that your new code will run out of stack space.

If you can calculate the size of the stack at compile time, you don't need to manually manage it.

I think that recursion can always be converted to iterative equivalents.

Typically you don't use dynamic allocation, making trees much more tedious to implement. The usual data structure is a stack allocated constant size array.

But if you really have to use recursion, you can always simulate it with a loop and an explicit stack. This way it's also easy to bound the stack size.

Anyone else than me (as a C programmer) that felt like: "Nice, most things mentioned are how I prefer to do it anyway"?

> For example, coding standard says every "case" statement has to have a "default" switch. grep "case", grep "default", and you get wildly different numbers!

I hope that's an error in the document. I assume they meant "$(grep -r 'switch (' . | wc -l) != $(grep -r 'default:' . | wc -l)".

It's a summary of the talk at https://vimeo.com/84991949 , where Holzmann just mentions the use of grep verbally, not giving the exact commands to run.

Article author here. I'm a sysadmin so my programming mind may have translated "switch" (C) to "case" (bash). Fixed. Thanks for the catch!

Reply on news.ycombinator.com