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,f3d27f1fefd7e554
X-Google-Attributes: gid103376,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local01.nntp.dca.giganews.com!nntp.sun.com!news.sun.com.POSTED!not-for-mail
NNTP-Posting-Date: Mon, 24 Sep 2007 04:03:42 -0500
Newsgroups: comp.lang.ada
Subject: Re: Blocking I/O and Ravenscar
References: <1190408890.068176.182160@n39g2000hsh.googlegroups.com>
 <LU0Ji.97568$Xa3.74710@attbi_s22>
 <1190495840.472000.321860@19g2000hsx.googlegroups.com>
 <vp9df3p4o9u55on11ecse9h179d2rv4b2n@4ax.com>
From: Ole-Hjalmar Kristensen
 <ole-hjalmar.kristensen@substitute_employer_here.com>
Organization: Sun Microsystems
Date: 24 Sep 2007 11:03:42 +0200
Message-ID: <wvbrd4w8sadt.fsf@sun.com>
User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/21.2
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Cache-Post-Path: news1nwk!unknown@khepri42.norway.sun.com
X-Cache: nntpcache 3.0.1 (see http://www.nntpcache.org/)
X-Usenet-Provider: http://www.giganews.com
NNTP-Posting-Host: 192.18.43.225
X-Trace: 
 sv3-Hd8FaIQznbA+TBqSwM+BUlhZWP2N+AGVTyDROLQfFlbidU3xFusXzcUeabp/CcbmCW60BaAcnfpyXY9!CUlaWSxU+RSb0k17u5o+dJzpw4sGl6GbJVGd2mRP+5mSe8dx8W0Jjq1e
X-Complaints-To: abuse@sun.com
X-DMCA-Complaints-To: abuse@sun.com
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.35
Xref: g2news2.google.com comp.lang.ada:2106
Date: 2007-09-24T11:03:42+02:00
List-Id: <comp.lang.ada>

Hmmm. Why not use the rendezvous for implementing CSP communication?
It would seem to be a much closer match than protected objects.

>>>>> "S" == Surfer  <surfer@no.spam.net> writes:

<snip>

    S> There is a very interesting paper about message passing and Ravenscar
    S> here: 

    S> Communicating Ada Tasks (2003)  
    S> http://citeseer.ist.psu.edu/577581.html

    S> Abstract. Ada has proven successful in the area of high integrity sys-
    S> tems development, but its tasking model is hard to reason about. Thus,
    S> Ravenscar has been defined as a restricted subset of the Ada tasking
    S> model, which meets the requirements of producing analysable and de-
    S> terministic code. A central feature of Ravenscar is the use of
    S> protected objects to ensure mutually exclusive access to shared data.
    S> In this paper, we use Ravenscar protected objects to implement CSP
    S> channels in Ada. This allows us to transform the data-oriented
    S> asynchronous tasking model of Ravenscar into the cleaner, and better
    S> understood, message-passing synchronous model of CSP. Thus, formal
    S> proofs and techniques for model-checking CSP specifications can be
    S> applied to Ravenscar programs. In turn, this raises our confidence in
    S> these programs and their reliability. We will formally verify our
    S> implementation of the CSP channel using the Circus model of Ravenscar
    S> protected objects provided in [3].

    S> (You can download a copy from the links in the top right hand corner)

    S> Also a closely related paper here:

    S> Extending Ravenscar with CSP Channels
    S> http://www.springerlink.com/index/j7h8rr665r0x20n9.pdf

-- 
   C++: The power, elegance and simplicity of a hand grenade.