Ravenscar References

Ravenscar References

[lyttlec]

Can anyone suggest a good reference on using the ravenscar profile? In
the Ada books I have, it only gets a one or two page mention. A
reference with an extended case study would be great.

Re: Ravenscar References

[Simon Wright]

lyttlec <lyttlec@removegmail.com> writes:

> Can anyone suggest a good reference on using the ravenscar profile? In
> the Ada books I have, it only gets a one or two page mention. A
> reference with an extended case study would be great.

You might find something useful at http://cubesatlab.org -
e.g. http://www.cubesatlab.org:430/PUBLIC/brandon-chapin-HILT-2016.pdf

Re: Ravenscar References

[J-P. Rosen]

Le 16/01/2019 à 18:48, lyttlec a écrit :
> Can anyone suggest a good reference on using the ravenscar profile? In
> the Ada books I have, it only gets a one or two page mention. A
> reference with an extended case study would be great.
> 
Did you get the official report at
http://www.open-std.org/jtc1/sc22/wg9/n424.pdf
?

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Ravenscar References

[Niklas Holsti]

On 19-01-17 07:31 , J-P. Rosen wrote:
> Le 16/01/2019 à 18:48, lyttlec a écrit :
>> Can anyone suggest a good reference on using the ravenscar profile? In
>> the Ada books I have, it only gets a one or two page mention. A
>> reference with an extended case study would be great.
>>
> Did you get the official report at
> http://www.open-std.org/jtc1/sc22/wg9/n424.pdf
> ?

Note that the discussion of pragma Atomic in that document invites risky 
programming. For example, it says "All global objects that are either of 
a protected type or an atomic type may be safely shared, and so no 
static identification [to find risky, unprotected sharing] is required 
for these."

However, as I trust most of us know, while a pragma Atomic ensures that 
any read or write of the object is itself atomic, it does not ensure 
that a read-modify-write update sequence, such as X := X + 1, is atomic 
in its entirety. IMO this means that even atomic shared objects should 
be identified and the safety of their uses checked. And that using a 
protected type, with its fully atomic operations, is preferable, when 
possible.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ravenscar References

[lyttlec]

On 1/16/19 1:15 PM, Simon Wright wrote:
> lyttlec <lyttlec@removegmail.com> writes:
> 
>> Can anyone suggest a good reference on using the ravenscar profile? In
>> the Ada books I have, it only gets a one or two page mention. A
>> reference with an extended case study would be great.
> 
> You might find something useful at http://cubesatlab.org -
> e.g. http://www.cubesatlab.org:430/PUBLIC/brandon-chapin-HILT-2016.pdf
> 

Thanks all for the links. They are a help.
However, I'm looking for something along the lines of porting legacy
code to be ravenscar "safe".
As an illustration, consider making Dmitry A Kazakov's code meet
Ravenscar. I need to port lots of existing more or less standard
components to meet Ravenscar. This is to satisfy some regulatory
authorities.

Re: Ravenscar References

[Jeffrey R. Carter]

On 1/18/19 8:18 PM, lyttlec wrote:
> 
> I need to port lots of existing more or less standard
> components to meet Ravenscar. This is to satisfy some regulatory
> authorities.

I don't know that "port" is a good word for this activity. I once looked at 
implementing Sandén's FMS problem using Ravenscar. Starting from the 
requirements, I first had to find a Ravenscar-suitable design. The standard 
design has a dynamic task per job, and is clearly not possible using Ravenscar. 
An alternative design using a task per workstation had to be used.

 From that choice, Ravenscar drove a proliferation of protected objects and 
helper tasks. Things that were simple in full Ada became much more complex to 
meet the restrictions of the profile.

Presumably you would need to apply a similar process to each of the components 
you need to convert.

-- 
Jeff Carter
"Sir Lancelot saves Sir Gallahad from almost certain temptation."
Monty Python & the Holy Grail
69

Re: Ravenscar References

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1405 bytes --]

"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message 
news:q22a5c$d8o$1@dont-email.me...
> On 1/18/19 8:18 PM, lyttlec wrote:
>>
>> I need to port lots of existing more or less standard
>> components to meet Ravenscar. This is to satisfy some regulatory
>> authorities.
>
> I don't know that "port" is a good word for this activity. I once looked 
> at implementing Sandén's FMS problem using Ravenscar. Starting from the 
> requirements, I first had to find a Ravenscar-suitable design. The 
> standard design has a dynamic task per job, and is clearly not possible 
> using Ravenscar. An alternative design using a task per workstation had to 
> be used.
>
> From that choice, Ravenscar drove a proliferation of protected objects and 
> helper tasks. Things that were simple in full Ada became much more complex 
> to meet the restrictions of the profile.
>
> Presumably you would need to apply a similar process to each of the 
> components you need to convert.

Note that the less strict profile Jorvik, defined in Ada 2020 (and already 
implemented in GNAT) would simplify this process.

I don't think it is possible to "convert" regular Ada code into Ravenscar 
(unless, of course, it doesn't use any tasks ;-). You pretty much have to 
completely rewrite it with Ravenscar in mind. (In this way, it is very much 
like using SPARK.)

                                    Randy.

Re: Ravenscar References

[J-P. Rosen]

Le 22/01/2019 à 00:19, Randy Brukardt a écrit :
> I don't think it is possible to "convert" regular Ada code into Ravenscar 
> (unless, of course, it doesn't use any tasks ;-). You pretty much have to 
> completely rewrite it with Ravenscar in mind. (In this way, it is very much 
> like using SPARK.)

I don't fully agree with that statement; it all depends where you start
from.

I recently helped one of my clients who wanted to move to Ravenscar. The
original structure was all Ada83, communicating with rendezvous.
However, it was already safety critical, therefore based on cyclic,
never ending tasks, and limited communications. It was reasonably easy
to define patterns for matching the existing structure into Ravenscar
patterns.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Ravenscar References

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1155 bytes --]

"J-P. Rosen" <rosen@adalog.fr> wrote in message 
news:q26nhh$nr4$1@dont-email.me...
> Le 22/01/2019 à 00:19, Randy Brukardt a écrit :
>> I don't think it is possible to "convert" regular Ada code into Ravenscar
>> (unless, of course, it doesn't use any tasks ;-). You pretty much have to
>> completely rewrite it with Ravenscar in mind. (In this way, it is very 
>> much
>> like using SPARK.)
>
> I don't fully agree with that statement; it all depends where you start
> from.
>
> I recently helped one of my clients who wanted to move to Ravenscar. The
> original structure was all Ada83, communicating with rendezvous.
> However, it was already safety critical, therefore based on cyclic,
> never ending tasks, and limited communications. It was reasonably easy
> to define patterns for matching the existing structure into Ravenscar
> patterns.

The OP was looking for free resources to do this job for any existing Ada 
code, and that clearly doesn't exist, and it can't exist. I certainly 
believe that it can be done if the code is already quite limited and if you 
hire a Ravenscar expert to help. :-)

                                    Randy.

Re: Ravenscar References

[lyttlec]

I think my situation is similar to yours. The project already had to
meet "life safety" for the 1990s. The architectural changes won't be
trivial, but also won't be overwhelming.
To keep from having to re-invent the wheel for lots of common structures
and components. "Free" isn't a requirement, even though the budget is
limited.
On 1/22/19 5:05 PM, Randy Brukardt wrote:
> "J-P. Rosen" <rosen@adalog.fr> wrote in message 
> news:q26nhh$nr4$1@dont-email.me...
>> Le 22/01/2019 à 00:19, Randy Brukardt a écrit :
>>> I don't think it is possible to "convert" regular Ada code into Ravenscar
>>> (unless, of course, it doesn't use any tasks ;-). You pretty much have to
>>> completely rewrite it with Ravenscar in mind. (In this way, it is very 
>>> much
>>> like using SPARK.)
>>
>> I don't fully agree with that statement; it all depends where you start
>> from.
>>
>> I recently helped one of my clients who wanted to move to Ravenscar. The
>> original structure was all Ada83, communicating with rendezvous.
>> However, it was already safety critical, therefore based on cyclic,
>> never ending tasks, and limited communications. It was reasonably easy
>> to define patterns for matching the existing structure into Ravenscar
>> patterns.
> 
> The OP was looking for free resources to do this job for any existing Ada 
> code, and that clearly doesn't exist, and it can't exist. I certainly 
> believe that it can be done if the code is already quite limited and if you 
> hire a Ravenscar expert to help. :-)
> 
>                                     Randy.
> 
> 

Re: Ravenscar References

[Jorge Real]

El jueves, 17 de enero de 2019, 6:31:34 (UTC+1), J-P. Rosen  escribió:
> Le 16/01/2019 à 18:48, lyttlec a écrit :
> > Can anyone suggest a good reference on using the ravenscar profile? In
> > the Ada books I have, it only gets a one or two page mention. A
> > reference with an extended case study would be great.
> > 
> Did you get the official report at
> http://www.open-std.org/jtc1/sc22/wg9/n424.pdf
> ?

Note there is a revised version of of the Ravenscar guide at
http://www.open-std.org/JTC1/SC22/WG9/n575.pdf

This version of June 2017 is adapted to Ada 2012 TC1.

Cheers,
Jorge.

Re: Ravenscar References

[Niklas Holsti]

On 19-01-29 03:08 , Jorge Real wrote:
> El jueves, 17 de enero de 2019, 6:31:34 (UTC+1), J-P. Rosen  escribió:
>> Le 16/01/2019 à 18:48, lyttlec a écrit :
>>> Can anyone suggest a good reference on using the ravenscar profile? In
>>> the Ada books I have, it only gets a one or two page mention. A
>>> reference with an extended case study would be great.
>>>
>> Did you get the official report at
>> http://www.open-std.org/jtc1/sc22/wg9/n424.pdf
>> ?
>
> Note there is a revised version of of the Ravenscar guide at
> http://www.open-std.org/JTC1/SC22/WG9/n575.pdf
>
> This version of June 2017 is adapted to Ada 2012 TC1.

But, disappointingly, it still contains the (IMO) misleading advice that 
"All global objects that are either of a protected type or an atomic 
type may be safely shared".

IMO atomic-type objects can be safely shared only if care is taken to 
follow a proper lock-free read/write protocol.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Ravenscar References

[Jorge Real]

Niklas, I agree with your observation.

Fortunately, the Ravenscar guide is currently being adapted to ISO formatting so that it eventually becomes searchable in their archive. So there may be an opportunity to correct some typos and to also polish this part of the text. I was proposing other corrections and I have already pointed them to your remark as well.

Cheers,
Jorge.

El martes, 29 de enero de 2019, 20:24:19 (UTC+1), Niklas Holsti  escribió:
> On 19-01-29 03:08 , Jorge Real wrote:
> > El jueves, 17 de enero de 2019, 6:31:34 (UTC+1), J-P. Rosen  escribió:
> >> Le 16/01/2019 à 18:48, lyttlec a écrit :
> >>> Can anyone suggest a good reference on using the ravenscar profile? In
> >>> the Ada books I have, it only gets a one or two page mention. A
> >>> reference with an extended case study would be great.
> >>>
> >> Did you get the official report at
> >> http://www.open-std.org/jtc1/sc22/wg9/n424.pdf
> >> ?
> >
> > Note there is a revised version of of the Ravenscar guide at
> > http://www.open-std.org/JTC1/SC22/WG9/n575.pdf
> >
> > This version of June 2017 is adapted to Ada 2012 TC1.
> 
> But, disappointingly, it still contains the (IMO) misleading advice that 
> "All global objects that are either of a protected type or an atomic 
> type may be safely shared".
> 
> IMO atomic-type objects can be safely shared only if care is taken to 
> follow a proper lock-free read/write protocol.
> 
> -- 
> Niklas Holsti
> Tidorum Ltd
> niklas holsti tidorum fi
>        .      @       .

Re: Ravenscar References

[Jere]

On Tuesday, January 29, 2019 at 2:24:19 PM UTC-5, Niklas Holsti wrote:
> On 19-01-29 03:08 , Jorge Real wrote:
> > El jueves, 17 de enero de 2019, 6:31:34 (UTC+1), J-P. Rosen  escribió:
> >> Le 16/01/2019 à 18:48, lyttlec a écrit :
> >>> Can anyone suggest a good reference on using the ravenscar profile? In
> >>> the Ada books I have, it only gets a one or two page mention. A
> >>> reference with an extended case study would be great.
> >>>
> >> Did you get the official report at
> >> http://www.open-std.org/jtc1/sc22/wg9/n424.pdf
> >> ?
> >
> > Note there is a revised version of of the Ravenscar guide at
> > http://www.open-std.org/JTC1/SC22/WG9/n575.pdf
> >
> > This version of June 2017 is adapted to Ada 2012 TC1.
> 
> But, disappointingly, it still contains the (IMO) misleading advice that 
> "All global objects that are either of a protected type or an atomic 
> type may be safely shared".
> 
> IMO atomic-type objects can be safely shared only if care is taken to 
> follow a proper lock-free read/write protocol.
> 

I got the impression from the entire section there that the author was 
referring to erroneous access from data races, which would make the
statement "technically" correct.  The X := X + 1 case is not 
technically erroneous (not a data race).  It's instead considered
a race condition (which is not technically erroneous).  Atomic
variables don't do anything to protect you from race conditions, 
but they definite make you safe from data races.

That doesn't detract from the meat of your general point that 
protected objects are much more capable of preventing unwanted
code results than atomic variables and that atomic variables
should be used with care.  I just don't think the author was 
intending to go into race conditions and instead focused on 
data races (erroneous access), at least for that section of the
paper.