Stack-checking a program... that will execute in orbit
users.softlab.ece.ntua.gr
users.softlab.ece.ntua.gr
The reasoning appears to be "since technique X can cause problems in some circumstances, it can never be used in software for domain Y (usually avionics, space, or similar)".
However, obviously every technique could cause problems in some circumstances. Therefore I conclude it's impossible to ship software into space.
Since software clearly is shipped into space, it seems likely there is some problem with the above argument. My suspect is the "could cause problems? Can't use it!" line of reasoning is oversimplified for the purposes of explanation, and hopefully something better justified is actually occurring.
Checking a programmer's claim that a program will not run out of memory is difficult (sometimes impossible) if you allow heap allocations and arbitrary stack usage. You could allow either, if the programmer supplies a proof that things are OK. But with such a proof in hand, writing the thong so that it can be mechanically checked is "just work" (tedious work, possibly, but for this application, that is not that important). Because of that, why risk that such a proof is flawed (or becomes flawed after a bug fix), if one can just as well prevent the problem?
Of course, the checking code will be buggy, too. That is OK; it will be written by a separate team, and will improve over time, just as the code it checks does.
I guess that, even with these checks, the program will still have some watchdog timer, a way to remotely reset it, and a way to upload new software, just in case it runs wild.
Indeed.
As for the reasoning: couldn't have said it better myself.
This approach provides a good baseline. However, I'd highly recommend empirical testing as well. For example, create a sufficiently large stack, initialize the stack with a known bit pattern and then check the high water mark after fully exercising the program.
Why should recursion be out? You just need to be careful with it. Not having an infinite recursion is basically the same problem as not having an infinite loop.
You'll probably be wondering "what use could that crippled compiler probably have?". Well, most of the people here are carrying code emitted by it in their pocket.
And remember, this is just a hack I did - I wanted to show people the things one can do with objdump. From the article:
"This kind of functionality is usually part of far more mature tools than... quickly-hacked Python scripts. Don't use this to send your spaceship in orbit :-)"
The problem is that the mathematical problem being attacked is undecidable. This script only approximates a solution in the case where function pointers don't exist. Even that would be OK if you knew about the limitation and the script flagged indirect jumps as errors too. It looked like you didn't realize that though, so I thought it had to be mentioned.
When the software can prove X, return True.
When the software can prove !X, return False.
When the software can't do either, return Sorry.
Developing safety-critical code is governed by extensive guidelines (like DO178-B) which dictate lots of things, not just about code (process of development, testing, etc)
Most innovations fail because they do not integrate in the existing chain. Radical change can be accepted if, and only if it has extreme potential (orders of magnitude), because the existing methods are continously improved by small steps as well.
"First of all, you can't use heap - not when you're in orbit. Why? Because quite simply, if you do use heap, and malloc returns null... what do you do? You can't ask the user for help"
This is the OOM problem and is highly dependent upon the kernel you are using. Not bringing the kernel into the discussion means that the discussion is just silly. There is not much of a point to putting the heap in the stack as you said, but hey like the author we are just getting some ideas out there without bringing up the kernel.
The article is just an example of the notions used, and how objdump can be used to enforce them. Linux is used simply for demonstration purposes.
In your average PC with Linux/x86, it is clear that you fear neither stack nor heap error - you just restart the app :-)
Also, for a truly stackless CPU, look at system 370 (and, I guess, most other machines predating Algol)