Re: Are un-validated compilers unsafe?

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

In article <Xnu2xLAvVwI3EwFv@tioman.demon.co.uk>,
  Mark Elson <marke@tioman.demon.co.uk> wrote:

> This question was prompted by the fact that a new space
> project may be using GNAT in conjunction with an
> un-validated RTOS on the grounds that
> the combination is in widespread use and that GNAT is a
> "very good" compiler (also due to the abundance of
> developers as well as users). I
> was somewhat surprised that they could get away with this
> (although their requirement is more reliability than
> safety). Does this mean there is not much motivation for
> vendors to get their compilers validated these days?

There is no magic in validation. The ACVC suite is a useful
test suite, and a formal validation is a useful way of
ensuring that a given compiler passes this suite. Whether
validation is required for a given project is of course
the decision of the project.

In the case of GNAT, we validate mainstream native
compilers, and selected cross-products. The latter are
validated either because we see a very general demand, or
in response to specific customer requirements.

We find three situations with users of cross-GNAT systems
(and there is no particular correlation with size of
project, or reliability requirements).

1. There is no specific validation requirement, and it is
simply not an issue.

2. There is a contract requirement with respect to the
behavior of the compiler on the ACVC suite (and possibly
other test suites), but no requirement for formal
validation.

3. There is a formal requirement for validation (this for
example is the situation for the VxWorks/68K target we
recently validated).

For a given project, you need to decide what you need, and
talk to your vendor. For example, if you are considering
something like an RTEMS/PowerPC combination, then of course
this can be validated, but it will not be a zero-cost
proposition. If you think validation is an important
criterion, then discuss it with us. If a large support
contract is involved, we may be willing to provide
validation as part of this contract. Otherwise we can
quote an add-on price. But check things out carefully to
make sure that you really need this requirement.

> In any case, does the fact that a compiler-OS-processor
> has not been validated mean that it is unsafe (or
> unreliable), i.e. that it is not suitable for use in
> safety-critical applications?

Of course not! There are compilers that are not formally
validated that are considered highly reliable. For example,
the Aonix/CSMART product is I think one that people would
consider to be at the forefront of high reliability tools,
but it is not even possible to validate it, since it is an
Ada subset. Our own GNORT (GNAT No Run-Time) product aimed
at safety critical applications (and in use by customers
for such applications) has similar restrictions.

> I'm guessing, looking
> at a number of software safety requirements, that if you
> don't use a validated combination then the onus is on you
> is to verify down to object code level, i.e. validation
> may save you work.

This is the most worrisome statement in your post. The idea
that validation guarantees, even informally, let alone from
a formal verification process, that you can trust the
compiler 100% and do not need to do your own verification
is seriously flawed.

A validated compiler is simply one that has passed a batch
of tests. It's quite a useful batch of tests, but we would
not rely on the ACVC suite, even for the testing that we
do on a wavefront delivered to a customer. It is entirely
inadequate for such a purpose. Our testing involves running
a very large suite of tests, of which the ACVC is just one
portion (and it is getting to be a smaller portion every
day, as we add new tests to our own internal regression
testing procedures). You will find the same is true for
all other Ada vendors.

Validation does not guarantee *anything* about a compiler
other than that it passed a particular, very incomplete,
set of tests. Why very incomplete? Because for a compiler,
we don't begin to know how to make a complete set of tests,
and we don't begin to know how to verify or validate an
Ada compiler in the sense of rigorous procedures like FAA
certification.

> I've had a look at the EDS site and the choice for
> embedded applications using Ada 95 seems restricted,
> especially wrt. to the RTOS choice. Are
> vendors not bothering to validate their compilers &OSs.

See above

> (or is it something that's done on demand and so
> additions are only likely to occur if a particular
> project can afford the validation). Is obtaining
> validation an expensive exercise anyway?

It depends on the situation

> Do vendors subsidise it if a
> projects chooses to go that route?

It depends on the situation. If you are using a system that
the vendor anticipates selling to others, the answer may be
yes, if not, the answer may be no. I think you may get a
more accurate answer to this question if you ask your
vendor. CLA while it may sometimes be able to answer some
questions is hardly the place to ask about pricing policies
of specific vendors, especially when we don't know what
configuration you are talking about! If indeed you are
considering GNAT, this is something you should discuss
with the sales folks at ACT Europe (sales@act-europe.fr).

> Are there other means by which compiler/OS/target
> combinations get certified

You are looking for something that does not exist, namely
a certification mark that will guarantee a compiler is
safe to use. There are no "other means", because there
are no means at all. Validation of a compiler does NOT
provide this assurance.

> or even proven by common use? Is there a list of such?

The only list that would be meaningful here is references
to existing projects. You should ask your vendor for
references, they may be more significant than any
validation certificate.

> Many thanks for any replies. Sorry for all the questions
- I'm new to
> Ada and safety-critical software.

Your questions are good ones. The choice of the word
validation for Ada compilers was an unfortunate one with
respect to the safety critical community. When that
community talks about validation or certification, they
really mean it! I am afraid that our technology in
compilers just has not reached that stage. We don't even
know how to make useful formal specifications for languages
like Ada (the EEC sponsored effort in this area with Ada 83
resulted in several telephone books full of mathematical
formulae and did not even address the hard parts of the
language like rep clauses and allowed optimizations. The
end result was essentially useless to the Ada community,
although as a research project in learning more about
formal specification techniques it was useful).

We can address the issue of certifying runtimes, and for
that two approaches have been used, as mentioned above.

Aonix provides a subset implementation that uses a very
small, very well defined run-time that can and has been
subjected to standard FAA certification procedures (this
is CSMART, the certified small Ada run time system). A
more recent product (Raven I believe is the name) extends
this to include a small subset (Ravenscar) of the tasking
capability of Ada (CSMART excludes tasking). You should
consult Aonix for further details.

For GNAT, we have a product GNORT that has no run time
at all. Again it is a small subset (the inspiration for
the subset is the SPARK language from Praxis). A nice thing
about this approach is that since there is no run-time,
there is nothing to certify!

Indeed the GNORT approach is an interesting product of the
open source approach. One leading person in the Ada safety
critical vendor community told me once that their company
had considered a zero-byte runtime approach, but one of the
reasons they had rejected it was a commercial one, there
would be nothing to sell :-)

In the case of GNAT, we are basically selling support,
rather than shrink wrapped software, so such commercial
considerations do not apply.

For more details on the GNORT approach, contact
sales@gnat.com or sales@act-europe.fr, or if you have
general technical issues which would be of interest to
the CLA community, then you could post questions here and
I would be happy to answer them (I like to be careful to
stay on the right side of the information/advertising line)

Robert Dewar
Ada Core Technologies

-----------== Posted via Deja News, The Discussion Network ==----------
http://www.dejanews.com/       Search, Read, Discuss, or Start Your Own