Re: High-Integrity OO and controlled types

[Cyrille <comar@eu.adacore.com>]

> > This is surprising to me. I don't see anything in controlled types
> > that would require "extensive run-time support".
>
> Admittedly, we could provide more info here. "Extensive runtime
> support" is, in fact, only one aspect of it. Let me first say why
> "runtime support" is an issue: that's because in a HI context, the Ada
> runtime needs to be certified along with the application and thus
> certification material  (for various standards) needs to be developed
> and maintained. This is one of the reasons why we minimize  our HI
> runtime footprint. There are other reasons: source to object tracea

(this message was posted too fast...)

so I was saying "source to object" traceability (as required for
do-178b level A) becomes more difficult. And finally, this feature is
not that useful in very critical part of a system. The most common use
of controlled types is for dynamic memory management. something that
is usually avoided in the most critical part of the system. If you
really need to use dynamic memory management, then demonstrating the
correctness of the allocation strategy is not particularly easy in
such a context. It's probably simpler to wait for a fully certified GC
system to appear and used that instead...


> > There is another angle to this question: the Ravenscar profile does
> > not exclude controlled types. If GNAT's so-called Ravenscar profile
> > does exclude them, then it looks that it does not support some
> > formally valid Ravenscar programs, even some very trivial ones. Am I
> > missing something?

right. HI profiles come with additional restrictions. Note that
Ravenscar is just a restriction of the tasking model. So many
different profiles can claim to be "Ravenscar" compliant. For some of
our ports we provide 2 different ones: one less restricted than the
other.