From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,4e5770c49b971630 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!m10g2000yqd.googlegroups.com!not-for-mail From: Cyrille Newsgroups: comp.lang.ada Subject: Re: High-Integrity OO and controlled types Date: Mon, 2 May 2011 03:01:29 -0700 (PDT) Organization: http://groups.google.com Message-ID: <94f3a272-d071-4a74-bfbd-8f2b4c2347cf@m10g2000yqd.googlegroups.com> References: <679e3217-98dd-43c1-86f6-2038a029c3ea@b19g2000yqg.googlegroups.com> NNTP-Posting-Host: 194.98.77.125 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1304330489 31649 127.0.0.1 (2 May 2011 10:01:29 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 2 May 2011 10:01:29 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: m10g2000yqd.googlegroups.com; posting-host=194.98.77.125; posting-account=bNhsVwoAAAB6XmNPWgYcbUm6npIwL2C4 User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; fr; rv:1.9.2.16) Gecko/20110319 Firefox/3.6.16 ( .NET CLR 3.5.30729),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:20094 Date: 2011-05-02T03:01:29-07:00 List-Id: > > 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 =A0(for various standards) needs to be developed > and maintained. This is one of the reasons why we minimize =A0our 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.