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!news1.google.com!news.glorb.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!news1.optus.net.au!optus!newsfeeder.syd.optusnet.com.au!news.optusnet.com.au!not-for-mail From: Surfer Newsgroups: comp.lang.ada Subject: Re: Blocking I/O and Ravenscar Date: Mon, 24 Sep 2007 03:33:20 +0930 Message-ID: References: <1190408890.068176.182160@n39g2000hsh.googlegroups.com> <1190495840.472000.321860@19g2000hsx.googlegroups.com> X-Newsreader: Forte Free Agent 2.0/32.652 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit NNTP-Posting-Host: 58.110.86.47 X-Trace: 1190570526 12802 58.110.86.47 X-Original-Bytes: 3455 Xref: g2news2.google.com comp.lang.ada:2099 Date: 2007-09-24T03:33:20+09:30 List-Id: On Sat, 22 Sep 2007 14:17:20 -0700, Maciej Sobczak wrote: >On 22 Wrz, 06:31, "Jeffrey R. Carter" > wrote: > >> > Basically, Ravenscar forbids any blocking operations except waiting on >> > a protected entry or a suspension object. > >> I'm not sure where you got this idea; I don't recall any restrictions on >> blocking by tasks. > >Hm... true, I cannot find anything like this in the profile. > >However, I have found the following: > >"Besides, the compliance to the Ravenscar Profile reduces the >invocation call protocol set to the single asynchronous way." > >That was about communication between nodes in the distributed system, >in "Generating Distributed High Integrity Applications from Their >Architectural Description", which was presented at Reliable Software >Technologies - Ada-Europe 2007 and printed in the proceedings. > >If we conclude that Ravenscar does not prohibit tasks from blocking on >I/O, then the above statement has no foundations and nodes could >safely block on two-way synchronous messages (these would be mapped to >remote subprogram calls with [in] out parameters, which is according >to this paper excluded). > >In short - can I explicitly block on two-way communication in a >Ravenscar-compliant distributed system? > There is a very interesting paper about message passing and Ravenscar here: Communicating Ada Tasks (2003) http://citeseer.ist.psu.edu/577581.html Abstract. Ada has proven successful in the area of high integrity sys- tems development, but its tasking model is hard to reason about. Thus, Ravenscar has been defined as a restricted subset of the Ada tasking model, which meets the requirements of producing analysable and de- terministic code. A central feature of Ravenscar is the use of protected objects to ensure mutually exclusive access to shared data. In this paper, we use Ravenscar protected objects to implement CSP channels in Ada. This allows us to transform the data-oriented asynchronous tasking model of Ravenscar into the cleaner, and better understood, message-passing synchronous model of CSP. Thus, formal proofs and techniques for model-checking CSP specifications can be applied to Ravenscar programs. In turn, this raises our confidence in these programs and their reliability. We will formally verify our implementation of the CSP channel using the Circus model of Ravenscar protected objects provided in [3]. (You can download a copy from the links in the top right hand corner) Also a closely related paper here: Extending Ravenscar with CSP Channels http://www.springerlink.com/index/j7h8rr665r0x20n9.pdf