Stone age programming for space age hardware?
A few days ago, I watched a presentation by Gerard Holzmann on the development methodology and programming techniques used at JPL for writing the software for the next Mars mission. I found the talk entertaining and learned a few things. http://www.infoq.com/presentations/Scrub-Spin Among the arsenal of methods they use to ensure correctness is model checking for the algorithms used as well as rather restrictive coding standards. Well, model checking sounds good, real formal oomph. But the coding itself? For one thing, they're using C. On top of that, the coding standards prohibit dynamic memory allocation, recursion, and loops without explicit bounds; see [*] for more details. I was dumbfounded, although I have known all this. I have no personal experience with either embedded or real time software, but I've been aware that C still is the most popular language for that purpose and that coding standards are very restrictive. The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine. I have a hunch that the real restrictions of this kind of software are not concerned with fixed memory, iterations, whatever, but rather with guaranteed bounds. If that is indeed the case, how feasible would it be to prove relevant properties for systems programmed in Haskell? Michael [*] http://spinroot.com/gerard/pdf/Power_of_Ten.pdf -- Michael Schuerig mailto:michael@schuerig.de http://www.schuerig.de/michael/
On 07/06/2010, at 3:05 AM, Michael Schuerig wrote:
I have a hunch that the real restrictions of this kind of software are not concerned with fixed memory, iterations, whatever, but rather with guaranteed bounds. If that is indeed the case, how feasible would it be to prove relevant properties for systems programmed in Haskell?
For full Haskell that includes laziness and general recursion: not very. Proving properties about the values returned by functions is one thing, but giving good guaranteed upper bounds to the time and space used by an arbitrary program can be very difficult. See for example: J ̈orgen Gustavsson and David Sands, Possibilities and limitations of call-by-need space improvement, ICFP 2001: Proc. of the International Conference on Functional Programming, ACM, 2001, pp. 265–276. Adam Bakewell and Colin Runciman, A model for comparing the space usage of lazy evaluators, PPDP 2000: Proc. of the International Conference on Principles and Practice of Declarative Pro- gramming, ACM, 2000, pp. 151–162. Hans-Wolfgang Loidl. Granularity in Large-Scale Parallel Functional Programming. PhD Thesis. Department of Computing Science, University of Glasgow, March 1998. I expect future solutions for this domain will look more like the Hume (family of) languages [1]. They give several language levels, and can give stronger bounds for programs using less language features. [1] http://www-fp.cs.st-andrews.ac.uk/hume/index.shtml
Hi,
The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine.
for some safety critical applications that require certification, SCADE with the underlying Lustre language is used. It has formal semantics and some properties can be checked with automatic verification (up to linear arithmetic). The Lustre dataflow programs are then transformed to C (or Ada), by compiling to automata and representing those in C. This transformation is realized in Ocaml afaik. I think these kind of transformations, maybe specifying an embedded DSL instead of using a language like Lustre resulting in C with static bounds etc. could be a way to use Haskell. But anything using dynamic memory allocation, GC etc. is dangerous for real-time bounds. These programs also often run on old "outdated", but reliable HW for which mainly C compilers exist. The used standards only allow a certain set of programming languages (or subsets of these languages) and you even have to use "proved and tested" compilers and tools.
I have a hunch that the real restrictions of this kind of software are not concerned with fixed memory, iterations, whatever, but rather with guaranteed bounds. If that is indeed the case, how feasible would it be to prove relevant properties for systems programmed in Haskell?
I think proving the correct transformation of some input language to static C using Haskell is possible. Functional languages like Haskell or Ocaml in the case of SCADE are well suited to this, due to lack of loops, side effects etc. I think "atom" is such a DSL embedded into Haskell that can generate code for real-time systems. regards Matthias
Michael Schuerig wrote:
I was dumbfounded, although I have known all this. I have no personal experience with either embedded or real time software, but I've been aware that C still is the most popular language for that purpose and that coding standards are very restrictive.
The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine.
I have absolutely no experience with real time system, but if I were tasked to write with these coding standards, I would refuse and instead create a small DSL in Haskell that compiles to the requested subset of C. After all, the question is this: why use C if you don't actually use C? The reason is probably that designing/writing a proper DSL is considered too error prone, but with today's theorem provers, this should no longer be the case. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
On Tuesday 08 June 2010, Heinrich Apfelmus wrote:
Michael Schuerig wrote:
I was dumbfounded, although I have known all this. I have no personal experience with either embedded or real time software, but I've been aware that C still is the most popular language for that purpose and that coding standards are very restrictive.
The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine.
I have absolutely no experience with real time system, but if I were tasked to write with these coding standards, I would refuse and instead create a small DSL in Haskell that compiles to the requested subset of C.
That suggestion is similar to the approach taken by "verifiable" languages, as Matthias describes it in a parallel reply. Now, the interesting question is, whether it is possible to define a DSL that's expressive enough and still can be translated to a very restrictive subset of C. I wouldn't expect the on-board functionality of a space probe or rover to be trivial. I think it would count as cheating if you compile down a DSL to C code that only takes a fixed chunk of memory, but then itself manages blocks of that memory dynamically.
After all, the question is this: why use C if you don't actually use C? The reason is probably that designing/writing a proper DSL is considered too error prone, but with today's theorem provers, this should no longer be the case.
As I understood Holzmann in his talk, use of C is a kind of cultural heritage at JPL. BTW, thanks for your recent video on GADTs. Michael -- Michael Schuerig mailto:michael@schuerig.de http://www.schuerig.de/michael/
On Jun 8, 2010, at 14:22 , Michael Schuerig wrote:
On Tuesday 08 June 2010, Heinrich Apfelmus wrote:
I have absolutely no experience with real time system, but if I were tasked to write with these coding standards, I would refuse and instead create a small DSL in Haskell that compiles to the requested subset of C.
Now, the interesting question is, whether it is possible to define a DSL that's expressive enough and still can be translated to a very restrictive subset of C. I wouldn't expect the on-board functionality of a space probe or rover to be trivial.
Hm. Atom? -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
Michael Schuerig wrote:
Heinrich Apfelmus wrote:
I have absolutely no experience with real time system, but if I were tasked to write with these coding standards, I would refuse and instead create a small DSL in Haskell that compiles to the requested subset of C.
That suggestion is similar to the approach taken by "verifiable" languages, as Matthias describes it in a parallel reply.
Now, the interesting question is, whether it is possible to define a DSL that's expressive enough and still can be translated to a very restrictive subset of C. I wouldn't expect the on-board functionality of a space probe or rover to be trivial.
I think it would count as cheating if you compile down a DSL to C code that only takes a fixed chunk of memory, but then itself manages blocks of that memory dynamically.
Ah, I had in mind that the embedded DSL represents the target subset of C verbatim, very much in the spirit of Lennart Augustsson's reimplementation of BASIC http://tinyurl.com/augustss-BASIC http://hackage.haskell.org/cgi-bin/hackage-scripts/package/BASIC In other words, I'm thinking of a direct copy of the target language in Haskell. This way, you can use the type system to reject programs that don't adhere to the coding standards, which would be the main point of this embedding. But you get a huge benefit on top of that: Haskell now serves as a macro language and you can implement many abstractions that are not directly available in the target language, like custom control structures ("foreach") or exceptions (to organize these abundant checks for error conditions). Of course, the main goal of the NASA restrictions is to make the code so simple that it has no obvious deficiencies, but what better way is there to do that than finding and expressing - even small-scale - abstractions? (The foreach statement seems to be a convincing example.)
As I understood Holzmann in his talk, use of C is a kind of cultural heritage at JPL.
Ah well, the shackles of habit... In the matter of program design, I am unconvinced of any cultural heritage that is not based on the mathematical clarity of Edsger W. Dijkstra. ;)
BTW, thanks for your recent video on GADTs.
My pleasure. :) I'm already planning another video experiment. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
That's interesting, writing a DSL that compiles to C. I've actually inerviewed Gerard Holzamann twice, the first time when he received the ACM Software System Award in 2002 [1] and in 2008 after he moved to JPL [2]. What they use to test distributed software is the Process Meta Language (Promela) which models communication between distributed processes. Now Spin checks all possible models for deadlock, liveness etc. You can also use asserts to test conditions, just as in C. It also uses LTL (linear temporal logic) to formulate statements like, "will the railroad crossing always eventually open" and such. Two articles about Spin are [3] and [4]. Unfortunately, all four are in Dutch, but, hey, surely somebody here must be able to read that language <g>. The articles on Spin contain listings in Promela. Now, what Gerard Holzmann told me in the interview, is that NASA is very conservative in it's use of software tools. They don't use C++, just C, and a well defined version of the GNU C compiler at that. The coding standards, which even prohibit the use of C pointers, are aimed to keep everything as simple as possible. Just imagine hundreds of people working over many years to produce code where any error, how trivial it may be, will occur millions of miles away, cost hundreds of millions of dollars, and could damage the reputation of the company and its future funding. Now, if you can use a DSL to make embedded software absolutely failsafe, that would certainly grab NASA's attention. But again, they are very conservative, it seems... [1] http://muitovar.com/pub/pdf/holzmann.pdf [2] http://muitovar.com/pub/pdf/acmaw.pdf [3] http://muitovar.com/pub/pdf/spin1.pdf [4] http://muitovar.com/pub/pdf/spin2.pdf On Tue, 2010-06-08 at 18:27 +0200, Heinrich Apfelmus wrote:
Michael Schuerig wrote:
I was dumbfounded, although I have known all this. I have no personal experience with either embedded or real time software, but I've been aware that C still is the most popular language for that purpose and that coding standards are very restrictive.
The real reason behind my surprise was, that I was wondering how more modern languages could make inroads into such an environment. Haskell without recursion and dynamic memory allocation? Hard to imagine.
I have absolutely no experience with real time system, but if I were tasked to write with these coding standards, I would refuse and instead create a small DSL in Haskell that compiles to the requested subset of C.
After all, the question is this: why use C if you don't actually use C? The reason is probably that designing/writing a proper DSL is considered too error prone, but with today's theorem provers, this should no longer be the case.
Regards, Heinrich Apfelmus
On Tuesday 08 June 2010, Hans van Thiel wrote:
Now, what Gerard Holzmann told me in the interview, is that NASA is very conservative in it's use of software tools. They don't use C++, just C, and a well defined version of the GNU C compiler at that. The coding standards, which even prohibit the use of C pointers, are aimed to keep everything as simple as possible. Just imagine hundreds of people working over many years to produce code where any error, how trivial it may be, will occur millions of miles away, cost hundreds of millions of dollars, and could damage the reputation of the company and its future funding.
Perhaps it's just my lack of imagination that was driving my original question. I'm just having a hard time imagining how to write reasonably interesting algorithms that way. As I wrote, they might "cheat". It's entirely possible to implement dynamic memory on top of fixed-size arrays and use indexes instead of pointers. Of course, I have no idea if that's what they do. Michael -- Michael Schuerig mailto:michael@schuerig.de http://www.schuerig.de/michael/
Perhaps it's just my lack of imagination that was driving my original question. I'm just having a hard time imagining how to write reasonably interesting algorithms that way.
Very likely they have very specific functionality and hopefully a precise specification about what to do if the memory bounds are reached (at least some "failsafe" mode etc.) Many of these programs are very simple, but deliberately so.
As I wrote, they might "cheat". It's entirely possible to implement dynamic memory on top of fixed-size arrays and use indexes instead of pointers. Of course, I have no idea if that's what they do.
I think it is very likely done that way. I know this kind of programming from Java-smartcards. These support a subset of Java and allow the creation of objects only when installing a program on the card. There is no garbage collection, objects are persistent, i.e. creating new objects at runtime would fill up the available (very low) memory. "Dynamic" creation is done by reusing one "freed" object of the statically allocated ones or returning an error if no free object is available. Systems in high security or safety applications and those with properties like very low memory, very slow CPUs etc. often have requirements that makes direct usage of languages like Haskell very difficult or impossible. They are programmed in a way that makes their behavior as deterministic as possible, often also from the temporal view. If you have dynamic data structures with non-O(1) access it is also not possible to guarantee RT bounds. regards Matthias
participants (6)
-
Ben Lippmeier -
Brandon S. Allbery KF8NH -
Hans van Thiel -
Heinrich Apfelmus -
Matthias Guedemann -
Michael Schuerig