Safety-critical development in Ada and Eiffel

[donh@syd.csa.com.au (Don Harrison)]

Tucker Taft wrote:

:Don Harrison (donh@syd.csa.com.au) wrote:
:
:: Donovan Baarda wrote:
:
:: :Eiffel is IMHO a better choice for safety-critical applications without
:: :excessive real time requirements. Design by contract obviously (and
:: :measurably?) contributes significantly to program safety. Combining this
:: :with a complete inheritanc heirachy of library classes with all the
:: :contracts defined and inheritable has to make a huge difference.
:
:: I agree on all points. ...
:
:I'm curious what you mean by safety-critical.

Probably the same as you - systems which must function correctly (meet all 
functional requirements including timing constraints) where failure to do so
will incur great cost (loss of life, financial meltdowns etc.)


:In my experience with safety-critical applications, you 
:cannot have any significant amount of out-of-line run-time
:support, 

What, apart from managing concurrency, do you have in mind here?

In terms of the Eiffel concurrency overhead, it would probably be comparable
to that of Ada tasking. Optimisations and sensible design would make that 
acceptable, IMO.


: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.

Both of these issues can be dealt with in Eiffel:

  1) Dynamic storage allocation - The solution here (as in Ada) is to use 
     a pre-allocated memory pool for HRT parts of the system so eliminating 
     the need for dynamic allocation under HRT conditions.

  2) Garbage collection - This can be solved by turning memory allocation and
     deallocation (GC) off after start-up. Most Eiffel implementations already 
     allow you to turn GC off so vendors would just have to add the ability 
     to control allocation as well. It could work as follows:

       - At startup, dynamic storage would be pre-allocated as per 1).
       - Dynamic storage allocation and GC would be turned off.
       - The thread operates under HRT conditions communicating minimally
         with other threads.
       - At shutdown, dynamic storage allocation and GC are turned on again.

     Note that in a concurrent context, such memory control would occur on a 
     per-thread basis so allocation and GC would work as normal on less critical 
     threads.


:One of the important features of Ada in the safety-critical domain
:is that there is a very useful subset that makes little or no use 
:of out-of-line run-time support, and essentially no use of dynamic
:storage allocation.   

What is included in that subset?


:Finally there are available tools (such as the "SPARK" tools from Praxis, 
:Ltd.) which add support for all of the kinds of assertions that
:Eiffel has, including full static analysis and theorem
:proving support of the assertions, ...

Sounds like a step in the right direction, however I guess the assertions are 
not inheritable. If so, they are not as powerful as Eiffel's.

 
[...]
 
:It is not so easy to take a language like Eiffel that is fundamentally 
:oriented toward dynamic storage allocation (and pervasive dynamic binding), ...

Eiffel implementations optimise a high percentage of dynamic calls to static 
ones - 80-90%? Also, since the overhead of the calling mechanism is just part
of the cost of making the call (the total cost includes execution of the body),
the resultant penalty for default dynamic binding is reduced to 5-10% - 
obviously not worth getting excited over, even for HRT systems.


:Ada95 was designed to be able to support programming in a way
:that minimizes dynamic storage allocation, unnecessary dynamic binding, etc.
:while still supporting the object-oriented paradigm and a very strong
:and separately compilable contract between the clients 
:and the implementation(s) of an abstract interface.  The "contract"
:enforced at compile-time by the Ada compiler is much stronger than
:the contract enforced at compile-time by most compilers, since it
:includes strong type distinctions between otherwise equivalent scalar,
:array, and pointer types, plus compiler-enforced parameter modes,
:and the ability to use formal parameter names to verify actual/formal
:parameter association.

Some of these aren't necessary and have been omitted in the design of Eiffel. 
Of the rest, Eiffel effectively delivers the same (or an equivalent) 
functionality or enables you to acheive it through good design. 

A couple of points, however..

1) Eiffel automatically generates interfaces from class texts (a good thing, 
   IMO) but I'm unsure which impementations routinely recompile the "body" 
   of a class after changes that *don't* change the "interface". 
   None should, IMO, as it's technically possible to detect this situation.

2) Eiffel's contracts are stronger, more general, more flexible and more powerful
   than in standard Ada. This doesn't mean Ada's contracting is useless by 
   any means. It's a tribute to the designers of Ada83 that support for 
   predefined contracts was included at the time it was designed. I'm 
   disappointed, of course, that they were omitted from Ada95.

3) Named parameter association is not necessary with systematic, sensible naming.
   I confess to still using them in Ada (through force of habit) but usually 
   find that my formal and actual names are identical. Using named association 
   under such circumstances only serves to clutter the software text.


Don.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison             donh@syd.csa.com.au