Re: Blocking I/O and Ravenscar

[Ole-Hjalmar Kristensen <ole-hjalmar.kristensen@substitute_employer_here.com>]

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.