Re: Blocking I/O and Ravenscar

[Surfer <surfer@no.spam.net>]

On Sat, 22 Sep 2007 14:17:20 -0700, Maciej Sobczak
<see.my.homepage@gmail.com> wrote:

>On 22 Wrz, 06:31, "Jeffrey R. Carter"
><spam.jrcarter....@acm.nospam.org> 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