Re: Safety-critical development in Ada and Eiffel

[abo@minkirri.apana.org.au (Donovan Baarda)]

On Thu, 10 Jul 1997 19:26:17 -0400, 
 Mike Stark <michael.e.stark@gsfc.nasa.gov> wrote:
>Don Harrison wrote:
>> 
>> Tucker Taft wrote:
>> 
><snip> 
>> :and little or no use of dynamic storage allocation after
>> :system startup.
>> :
>> :Eiffel's dependence on dynamic storage allocation and garbage
>> :collection basically rules it out for most (serious) safety-critical
>> :applications, despite all its admittedly nice invariants and assertions.
>> 
[snip heaps of stuff about the evils of dynamic memory allocation in
safety critical applications, and how to get around it in various
languages such as turning off the GC!!]

I can't help but think that the reason dynamic memory allocation got such
a bad rap in the first place was there was no GC in old languages. Turning
it off seems to me like a step backwards.

Absolute control of memory allocation has been seen as necisary in safety
critical systems because you need to be sure that you will never run out
of memory and never write things over each other. 

Dynamic memory allocation made proving this much harder, so the safety
people just banned it, and used the measurable decrease in failures as
proof. Kill dynamic memory in C and it becomes a hell of a lot more
reliable.

However, GC has changed the whole landscape a bit. I wonder if anyone has
tried to formally prove that a GC will ensure you never die from running
out of memory in a program with strictly controlled objects in a
controlled environment?

Programs are so complex today that doing safety analysis right from the
bottom (like where variables are allocated in memory) up for every program
is getting out of the question. At some point there is going to have to be
a heriachical aproach to safety, where low level tools (such as GC) are
proven safe first. Future programs can use these tools, and can have the
safety analysis done at a higher level without worrying about proving the
low level tools all over again.

I'm sure GC would improve safety, but I wouldn't want to try and convince
the safety people. Safety people are by nature, and probably necesity,
conservative people and will take a hell of a lot of convincing before
they will let you do anything the new way, even if it is safer.

I also wouldn't want to try and provide the proof :-)

ABO