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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,eb0daafec4ae827a
X-Google-Attributes: gid103376,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news1.google.com!news.glorb.com!news-in.ntli.net!newsrout1-win.ntli.net!ntli.net!news.highwinds-media.com!xara.net!gxn.net!194.159.246.34.MISMATCH!peer-uk.news.demon.net!kibo.news.demon.net!news.demon.co.uk!demon!not-for-mail
From: Simon Wright <simon.j.wright@mac.com>
Newsgroups: comp.lang.ada
Subject: Re: High-integrity networking
Date: Wed, 10 Oct 2007 20:40:17 +0100
Organization: Pushface
Message-ID: <m2przm7o7y.fsf@mac.com>
References: <1191845623.383675.190820@d55g2000hsg.googlegroups.com>
 <l3sog357n18c6onk58a3sbru4sn1tn606d@4ax.com>
NNTP-Posting-Host: pogner.demon.co.uk
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
X-Trace: news.demon.co.uk 1192045222 28871 62.49.19.209 (10 Oct 2007 19:40:22
 GMT)
X-Complaints-To: abuse@demon.net
NNTP-Posting-Date: Wed, 10 Oct 2007 19:40:22 +0000 (UTC)
Cancel-Lock: sha1:+UxrDrymSzks3K4MdJz5OdlBiJk=
User-Agent: Gnus/5.11 (Gnus v5.11) Emacs/22.1 (darwin)
Xref: g2news2.google.com comp.lang.ada:2423
Date: 2007-10-10T20:40:17+01:00
List-Id: <comp.lang.ada>

Peter Morris <no@spam.please.net> writes:

> Issues with using Ravenscar and the Ada Distributed Systems Annex for
> High-Integrity Systems
> http://www.acm.org/sigada/ada_letters/march2001/103-audsley_1.pdf
>
> It identified the following problem:
>
> "It is clear that in order to facilitate distributed
> high-integrity real-time programming, the run-time
> support for distributed programming itself should conform
> to the Ravenscar profile. We have illustrated in this paper
> that this support requires greater expressive power than that
> afforded by Ravenscar. The result is greater complexity in
> the run-time – the code is almost certainly less analyzable,
> and definitely harder to produce and read."

Not clear from the last sentence whether it's the run-time or the user
code that's harder to analyse, produce or read. (Presumably that's not
true of Ravenscar itself, or no one would use it? It would be a hard
sell to management ...)

> I don't know if anyone has solved this problem.

Could a solution be analogous to the SPARK technique of telling the
Analyser that certain elements can be assumed to behave as specified
without needing proof? Could a multi-partition program use different
profiles for different parts?

Of course, that depends on what problem you are trying to solve; using
Ravenscar makes it easier to argue for correctness, not using
Ravenscar probably doesn't make an argiment impossible.