Ravenscar and run-time program parameters

Ravenscar and run-time program parameters

[Maciej Sobczak]

As I understand, the Ravenscar profile forbids dynamically created
tasks - all tasks have to be created at the library level.

Consider a system where a (sub)set of tasks forms a task pool.
Depending on the actual deployment, it might make sense to influence
the size of this pool - in other words to influence the number of
tasks that are started within the system.

One obvious way to pass the requested number of tasks is to use
program parameters.

I don't see how this can be implemented within the constraint that all
tasks have to be created at the library level.

On the other hand, having a pool of tasks is often associated with the
pattern where the set of tasks wait on a *single* job queue (or
something conceptually equivalent) - and Max_Entry_Queue_Length=>1
would make such scenario more difficult to implement. I can still
imagine the set of tasks having their own queues, though.

How to parameterize the number of tasks in the Ravenscar-compliant
system?

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

Re: Ravenscar and run-time program parameters

[Jean-Pierre Rosen]

Maciej Sobczak a �crit :
> As I understand, the Ravenscar profile forbids dynamically created
> tasks - all tasks have to be created at the library level.
> [...]
> One obvious way to pass the requested number of tasks is to use
> program parameters.
> 
> I don't see how this can be implemented within the constraint that all
> tasks have to be created at the library level.
Just declare a (global) array of tasks, whose size is computed from the 
parameters.

The issue with Ravenscar is not that the tasks must be library level, it 
is that the number of tasks must be statically known.

One goal of Ravenscar is to be able to predict memory usage, and that 
would be clearly impossible if the number of tasks is not statically known.

Yes, there is a lot of pretty nice things that you can't do under 
Ravenscar constraints. That's the price for safety.
-- 
---------------------------------------------------------
            J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr

Re: Ravenscar and run-time program parameters

[Jeffrey R. Carter]

Jean-Pierre Rosen wrote:
> 
> Yes, there is a lot of pretty nice things that you can't do under 
> Ravenscar constraints. That's the price for safety.

If you've ever looked at the Ravenscar implementation of a simple 
bounded blocking queue between a producer and a consumer task, you know 
that it's much more complex and difficult to get right than using a 
protected object with 2 entries. However, for analysis of the code, the 
Ravenscar version is apparently better. For some SW, that is a price 
worth paying, especially if you use RavenSPARK and can be confident in 
the correctness of the code. But for others, I'd be more confident of 
the correctness of the version with 2 entries.

-- 
Jeff Carter
"Don't knock masturbation. It's sex with someone I love."
Annie Hall
45

Re: Ravenscar and run-time program parameters

[Maciej Sobczak]

On 29 Sie, 18:17, "Jeffrey R. Carter"
<spam.jrcarter....@acm.nospam.org> wrote:

> If you've ever looked at the Ravenscar implementation of a simple
> bounded blocking queue

Could you please give a link, if there is such implementation publicly
available?

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

Re: Ravenscar and run-time program parameters

[Jeffrey R. Carter]

Maciej Sobczak wrote:
> 
> Could you please give a link, if there is such implementation publicly
> available?

One is given at

http://www.sigada.org/ada_letters/jun2004/ravenscar_article.pdf

However, it is incorrect, because Suspend_Until_True is a potentially 
blocking operation and may not be called from a protected operation. You 
may be able to infer a correct implementation from this.

-- 
Jeff Carter
"Propose to an Englishman any principle, or any instrument, however
admirable, and you will observe that the whole effort of the English
mind is directed to find a difficulty, a defect, or an impossibility
in it. If you speak to him of a machine for peeling a potato, he will
pronounce it impossible: if you peel a potato with it before his eyes,
he will declare it useless, because it will not slice a pineapple."
Charles Babbage
92

Re: Ravenscar and run-time program parameters

[Xavier Nicollin]

Hi,

Jeffrey R. Carter wrote:

> One is given at
> 
> http://www.sigada.org/ada_letters/jun2004/ravenscar_article.pdf
> 
> However, it is incorrect, because Suspend_Until_True is a potentially 
> blocking operation and may not be called from a protected operation. You 
> may be able to infer a correct implementation from this.

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). I am missing something?

-- 
Xavier Nicollin

Re: Ravenscar and run-time program parameters

[Maciej Sobczak]

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/

Re: Ravenscar and run-time program parameters

[Colin Paul Gloster]

On 2007-08-29, Jeffrey R. Carter <spam.jrcarter.not@acm.nospam.org>
wrote:

|------------------------------------------------------------------------|
|"If you've ever looked at the Ravenscar implementation of a simple      |
|bounded blocking queue between a producer and a consumer task, you know |
|that it's much more complex and difficult to get right than using a     |
|protected object with 2 entries. However, for analysis of the code, the |
|Ravenscar version is apparently better. For some SW, that is a price    |
|worth paying, especially if you use RavenSPARK and can be confident in  |
|the correctness of the code. But for others, I'd be more confident of   |
|the correctness of the version with 2 entries."                         |
|------------------------------------------------------------------------|

Why would you be more confident that one is good under some
circumstances (simply using RavenSPARK) but be more confident that the
other is good under other circumstances (simply not using RAVENSCAR)?

Regards,
Colin Paul Gloster

Re: Ravenscar and run-time program parameters

[Jeffrey R. Carter]

Colin Paul Gloster wrote:
> 
> Why would you be more confident that one is good under some
> circumstances (simply using RavenSPARK) but be more confident that the
> other is good under other circumstances (simply not using RAVENSCAR)?

I guess I wasn't clear. I was referring to whether or not I'm going to 
invest in the analyses that Ravenscar is intended for. If I do that, 
especially using RavenSPARK, which does additional analyses, then I can 
be confident despite the added complexity. But if I don't consider the 
code worth that extra effort, then I find I'm more likely to be 
confident in the simpler code.

-- 
Jeff Carter
"Propose to an Englishman any principle, or any instrument, however
admirable, and you will observe that the whole effort of the English
mind is directed to find a difficulty, a defect, or an impossibility
in it. If you speak to him of a machine for peeling a potato, he will
pronounce it impossible: if you peel a potato with it before his eyes,
he will declare it useless, because it will not slice a pineapple."
Charles Babbage
92

Re: Ravenscar and run-time program parameters

[Dmitry A. Kazakov]

On Wed, 29 Aug 2007 00:48:23 -0700, Maciej Sobczak wrote:

> As I understand, the Ravenscar profile forbids dynamically created
> tasks - all tasks have to be created at the library level.

I guess you mean no task allocation per new (directly or indirectly). That
is not equivalent to library level tasks. For example:

procedure Main is
   task type Worker;
   type Brigade is array (Positive range <>) of Worker;
   Workers : Brigade (1..Get_No); -- This is not static
begin
   loop
      ...
   end loop;
end Main;

But yes Ravenscar is very limiting for many things. Free cheese is only in
a mouse trap.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ravenscar and run-time program parameters

[brodax]

On 29 Ago, 11:02, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 29 Aug 2007 00:48:23 -0700, Maciej Sobczak wrote:
> > As I understand, the Ravenscar profile forbids dynamically created
> > tasks - all tasks have to be created at the library level.
>
> I guess you mean no task allocation per new (directly or indirectly). That
> is not equivalent to library level tasks. For example:
>
> procedure Main is
>    task type Worker;
>    type Brigade is array (Positive range <>) of Worker;
>    Workers : Brigade (1..Get_No); -- This is not static
> begin
>    loop
>       ...
>    end loop;
> end Main;
>
> But yes Ravenscar is very limiting for many things. Free cheese is only in
> a mouse trap.
>
> --
> Regards,
> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de


Actually you cannot create tasks local to procedures (or other tasks),
but only in the declarative part of a library level package.

The usual approach is declaring all tasks you need and let some of
them suspend on an entry waiting, for example, for an execution mode
change.

If you need to build a Ravenscar compliant system, I would suggest
always thinking in terms of 3 kinds of building blocks: cyclic tasks,
sporadic tasks and entry-less protected objects. Each sporadic task
would suspend on a "private" entry (in the sense it is visible to that
task only), whose barrier is opened by (potentially) several
interrupts or sw invocations (potentially carrying parameters). In
this manner, some Ravenscar constraints (size of entry queue) are
always verified by construction. And the concurrency model is overly
simplified and allows a very precise static timing analysis.

Regards,
Matteo Bordin