Blocking I/O and Ravenscar

Blocking I/O and Ravenscar

[Maciej Sobczak]

Basically, Ravenscar forbids any blocking operations except waiting on
a protected entry or a suspension object.

How can I perform a blocking I/O without breaking this restriction?

Let's say I would like to read a byte from a socket.
An entry with the simple barrier Is_Ready can do the job in terms of
the interface, but implementation-wise it only pushes the problem away
- who will set the Is_Ready flag after the byte is actually read from
the blocking physical device and put in the buffer? A separate task?
It would need to be non-Ravenscar - there seems to be a chicken&egg
problem here.

--
Maciej Sobczak
http://www.msobczak.com/

Re: Blocking I/O and Ravenscar

[Jeffrey R. Carter]

Maciej Sobczak wrote:
> Basically, Ravenscar forbids any blocking operations except waiting on
> a protected entry or a suspension object.
> 
> How can I perform a blocking I/O without breaking this restriction?
> 
> Let's say I would like to read a byte from a socket.
> An entry with the simple barrier Is_Ready can do the job in terms of
> the interface, but implementation-wise it only pushes the problem away
> - who will set the Is_Ready flag after the byte is actually read from
> the blocking physical device and put in the buffer? A separate task?
> It would need to be non-Ravenscar - there seems to be a chicken&egg
> problem here.

I'm not sure where you got this idea; I don't recall any restrictions on 
blocking by tasks.

-- 
Jeff Carter
"English bed-wetting types."
Monty Python & the Holy Grail
15

Re: Blocking I/O and Ravenscar

[Maciej Sobczak]

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?

--
Maciej Sobczak
http://www.msobczak.com/

Re: Blocking I/O and Ravenscar

[Surfer]

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

Re: Blocking I/O and Ravenscar

[Surfer]

On Mon, 24 Sep 2007 03:33:20 +0930, Surfer <surfer@no.spam.net> wrote:

>
>There is a very interesting paper about message passing and Ravenscar
>here: 
>
>Communicating Ada Tasks (2003)  
>http://citeseer.ist.psu.edu/577581.html
>
<snip>
>
>Also a closely related paper here:
>
>Extending Ravenscar with CSP Channels
>http://www.springerlink.com/index/j7h8rr665r0x20n9.pdf
>

Actually while having another look at these papers, I noticed that  
"Communicating Ada Tasks" uses three protected objects per channel but
"Extending Ravenscar with CSP Channels" uses only two protected
objects per channel.

That seems to be a considerable improvement. 

Re: Blocking I/O and Ravenscar

[Maciej Sobczak]

Thank you for the links, I will surely read these papers.

--
Maciej Sobczak
http://www.msobczak.com/

Re: Blocking I/O and Ravenscar

[Ole-Hjalmar Kristensen]

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.

Re: Blocking I/O and Ravenscar

[Surfer]

On 24 Sep 2007 11:03:42 +0200, Ole-Hjalmar Kristensen
<ole-hjalmar.kristensen@substitute_employer_here.com> wrote:

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

Its because the authors are considering the Ravenscar profile which
requires zero entries per task. That means that no Ada rendezvous are
possible.

However, implementation of CSP communication within the Ravenscar
profile, allows CSP rendezvous to be used in place of Ada rendezvous.

According to the paper[1]:

"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."

The authors also write:

"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."

So they seem to consider the CSP tasking model to be easier to reason
about than those of either Ada or Ravenscar.


[1]  Communicating Ada Tasks (2003)  
http://citeseer.ist.psu.edu/577581.html

[2] Extending Ravenscar with CSP Channels
http://www.springerlink.com/index/j7h8rr665r0x20n9.pdf