Re: Is an RTOS Required for Ada?

[Robert Dewar <robert_dewar@my-deja.com>]

In article <FCCLAJ.Esq@sd.aonix.com>,
  "George Romanski" <romanski@aonix.com> wrote:

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

That seems a reasonable working approximation. Certainly GNAT
does not begin to come close to this line (really it does not
do much insertion in this sense at all, and certainly nothing
that involves complex decisions, I agree with George that this
would usually cross the line).

But the line is still murky.

After all, what if the decision was not generated by inserting
code, but directly by the compiler's code generator. In this
case there *is* no source code to identify in this case, but
certainly you have to check all paths if your certification
discipline involves this. A lot of directly generated code
involves such decisions. As an example, consider:

   A,B,C : Integer;
   A := B / C;

on the 8086. You cannot simply generate a DIV instruction
since there is a bug which causes 16#8000# (largest negative
number) / 1 to divide trap. So either this has to be fixed
up in the divide trap handler, or you have to check this case
specially, generating a decision point in the code.

Second, especially in modern predicated architectures,
conditional jumps tend to disappear anyway as a result of
if conversions. Should there be a principle that every
predicated instruction must be executed with and without
the predicate being True. Sounds reasonable, but I don't
know if testing standards have caught up with this.

Third, there are lots of cases that involve no predication,
and no explicit testing, but they do strange things to avoid
jumps. For example, consider the following computation of
MAX (EAX, EBX) on a 386:

                     -- EAX < EBX   EAX >= EBX

    CMP   EAX. EBX   -- CF = 1        CF = 0
    SBB   EDX, EDX   -- all 1 bits    all 0 bits
    MOV   ECX, EDX
    NOT   ECX        -- all 0 bits    all 1 bits
    AND   EDX, EBX   --   EBX            0
    AND   ECX, EAX   --    0            EAX
    OR    EDX, ECX   --    MAX (EAX, EBX)

No predication, no jumps, but one would sure like to check
this code in "both directions", yet this is not easy to codify
either in terms of directly generated code or in terms of
inlined inserted code.

Note that a clever compiler might generate the above sequence
from code that looked like:

      if A >= B then
         C := A;
      else
         C := B;
      end if;

so a decision point in the source has disappeared in the
generated code. Of course if the source code had written
MAX, then we don't have an obvious decision point in the
source, but depending on the machine we might see:

   1. A single MAX instruction (Power)
   2. The above hairy sequence (x86)
   3. A converted if, using predication, with no jumps (Merced)
   4. An explicit test and jumps (Sparc)

So decision points in the source may not correspond to decision
points in the object in any obvious way.

I give this example just to remind us that, unlike the
formalists view of precise mathematical verification, the
real world of safety-critical verification is a more pragmatic
one. The FAA rules (and other similar verification protocols)
do not guarantee 100% correctness in a formal sense, but they
have been found to be effective in practice, and we refine the
practice based on experience as we go along.

That there is not yet a consensus on some of these issues is
not surprising, this is a very tricky area, and one in which
common sense is not necesarily the best guide :-)


Sent via Deja.com http://www.deja.com/
Share what you know. Learn what you don't.