Re: Ravenscar and run-time program parameters

[Maciej Sobczak <see.my.homepage@gmail.com>]

On 31 Sie, 11:01, Xavier Nicollin
<Xavierno.Spamnicol...@imag.nos.pam.fr> wrote:

> I suppose you are talking about Example 12 (p. 32). I believe (and I hope!)
> it is correct: the two calls to Suspend_Until_True take place in the
> regular procedures (Place_Item and Extract_Item), and not in the protected
> ones (Place and Extract).

When I think about it example a bit more, I conclude that it is kind
of cheating.
The Ravenspark profile was created to establish the practice that
helps with code analysis and verification. Protected object with two
entries was considered too much to be analysable and the trick is
proposed to do exactly the same, just with a bit different spelling:
instead of protected object with many entries one has to use a package
with many blocking procedures - and the blocking is performed on
nothing else than simple boolean barriers (suspension objects are just
this).

I cannot stop myself from asking: what makes is easier to analyze?
Actually, I find this example more *difficult* to analyze, because it
uses the multi-phase approach for performing the single action (try
and then see what happened and then potentially repeat). The fact that
the single action is attempted twice does not make it any easier for
me.
Also, in the second attempt the OK out variable is assigned but never
read after that. Nobody is bothered by this data flow issue?

Am I missing something?

What about another variant: a package with many procedures that block
on private semaphore protected object before doing the requested
action? It's still cheating, but at least the multi-phase operation
and the data flow issue are gone.

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