Re: Is an RTOS Required for Ada?

["George Romanski" <romanski@aonix.com>]

Robert Dewar wrote in message <7ifapi$lf1$1@nnrp1.deja.com>...
>In article <FCB3LD.2F2@sd.aonix.com>,
>  "George Romanski" <romanski@aonix.com> wrote:
>>
>> If the compiler inserts code for you, then this inserted code
>> must also be verified at level A.   (you will need
>> requirements design, source code tests and all appropriate
>> reviews)
>
>Right! Of course the line between generating code for the source
>you write, and "inserting code" is a very difficult, perhaps
>impossible line to draw.


Agreed
>
>Let's take two extremes. The only inlining that goes on in GNORT
>for example is very simple stuff. For example, if someone writes
>a call to To_Address (XYZ) from System.Storage_Elements, then
>this is inlined, but it also generates no code at all (it is
>basically an unchecked conversion). There is no place in the
>GNORT generated code where you see anything other than
>straightforward code generation that corresponds exactly to
>what you would expect from the source code.

>
>Let's assume on the other hand that a GNORT like compiler
>decides that it would be really nice to implement tasking.
>It does it by including the entire code of the tasking run time
>in your generated program. You can't simply decide that this
>is inlining, though it could be technically achieved by
>inlining. An attempt to say that this code did not need
>independent certification would indeed be completely bogus
>and would be considered cheating!

Agreed
>
>Drawing the precise line between these two extremes would not
>be an easy task. In the case of GNORT itself, we keep the subset
>so simple thatno such bogus insertions of code ever occur. You
>don't typically want fancy language features anyway in a
>safety-critical application!

Let's take an array assignment as an example.
If the arrays do not overlap (slicing is forbidden) then a single decision
may be present (for the loop - assuming the loop is not unrolled)

Providing the assignment is completed the decision would have been
evaluated both true and false.

If the arrays overlap, then a decision may be required to decide
the direction of the indexing, and a decision for the loop.

If the array has a smaller component size than a normal addressed
memory unit (e.g. we can move a word quicker than 4 bytes) then the
loop may move words until it gets to the edges.  This will require
more decisions for the operation.

For Level B code, ALL decisions must be shown to have been taken
in both directions.  ( or the code must be identified and analysed
explicitly).  It may be hard  to write test conditions that evaluate all
inlined
decisions in both directions.

My personal view (there is majority, but no concensus on this at present) is
that
inserted code which includes decisions must be identified and verified, for
level B.  For level A multiple conditions would require additional
verification.

Inserted code that includes no branches will be verified with the
application itself, it must be shown that it has been executed, but
may not require specific tests.

If the language is so restricted that there are no branches in non-user
developed code ( the run-time system which includes code to initialise
the target processor, and any code generator suport routines) then
verification of the application becomes easier.  Of course this must
be balanced with the cost of the user having to write and verify more
code to compensate for the reduced functionality offered by the
subset.


>
>Robert Dewar
>Ada Core Technologies
>
>
>--== Sent via Deja.com http://www.deja.com/ ==--
>---Share what you know. Learn what you don't.---