Version 1.2 of ai12s/ai12-0369-1.txt

Unformatted version of ai12s/ai12-0369-1.txt version 1.2
Other versions for file ai12s/ai12-0369-1.txt

!standard D.7(1.3/5)          20-03-12 AI12-0369-1/02
!standard D.7(10.12/5)
!class Amendment 20-03-06
!status Amendment 1-2012 20-03-11
!status ARG Approved 14-0-0 20-03-11
!status work item 20-03-06
!status received 20-02-24
!priority Low
!difficulty Easy
!subject Relaxing barrier restrictions
!summary
Use "statically names" rather than "statically denotes" in the definition of the restrictions Pure_Barriers and Simple_Barriers.
!problem
A predicate of a protected type cannot access its components.
An idiom (which is commonly used in SPARK) to add a predicate to the components of a protected type is to wrap the components in a record and then add the predicate to the record type.
Thus, the illegal:
protected type T with Dynamic_Predicate => (Count /= 0) or not Flag is entry E; private Flag : Boolean := False; Count : Natural := 0; end T;
protected body T is entry E when Flag is begin ...; end E; end T;
can be replaced by:
type Rec is record Flag : Boolean := False; Count : Natural := 0; end record with Dynamic_Predicate => (Count /= 0) or not Flag;
protected type T is entry E; private Data : Rec; end T;
protected body T is entry E when Data.Flag is begin ... end E; end T;
Unfortunately, the barrier in the above is not allowed by restrictions Simple_Barriers or Pure_Barriers. This means this idiom cannot be used with the Ravenscar or Jorvik profiles - which are also commonly used by SPARK users.
!proposal
(See Summary.)
!wording
Replace D.7(1.3/5):
- a name that statically denotes a scalar component of the
immediately enclosing protected unit;
with:
- a name that statically names (see 4.9) a scalar subcomponent
of the immediately enclosing protected unit;
Replace D.7(10.12/5):
- The Boolean expression in each entry barrier is either a static expression
or a name that statically denotes a component of the enclosing protected object.
with:
- The Boolean expression in each entry barrier is either a static expression
or a name that statically names (see 4.9) a subcomponent of the enclosing protected object.
!discussion
We already have the term "statically names" (originally defined for the Old attribute, now used for a number of other rules - see AI12-0368-1), which allows any prefix that does not require any dynamic evaluation or checking. This is exactly what we want (it also allows other cases, such as statically indexed array components). So we just revise the existing wording to use this term.
!corrigendum D.7(2)
Insert before the paragraph:
The following restriction_identifiers are language-defined:
the new paragraphs:
The actual text is in the conflict file.
!corrigendum D.7(10.8/2)
Replace the paragraph:
The Boolean expression in an entry barrier shall be either a static Boolean expression or a Boolean component of the enclosing protected object.
by:
The Boolean expression in each entry barrier is either a static expression or a name that statically names (see 4.9) a subcomponent of the enclosing protected object.
!ASIS
None needed.
!ACATS test
The Pure_Barriers test(s) should cover that case; an existing Simple_Barriers test should be update (or if one doesn't exist, a complete test should be constructed). Both a B-Test and a C-Test should exist for each restriction.
!appendix

From: Steve Baird
Sent: Friday, February 21, 2020  3:15 PM

[Not sending to Ada-Comment because this issue is a low-level detail.]

A use-case has come up in internal discussions at AdaCore that (IMO) suggests 
that a small change to the definition of "pure-barrier-eligible" given in 
AI12-0290 would be appropriate.

The issue has to do with allowing a name denoting a scalar subcomponent (not 
just a component) of the immediately enclosing protected object, provided that
    - the name does not denote a component that depends on a
      discriminant; and
    - no prefix of the name denotes an array.

[The idea is that there are no checks of any kind associated with the 
evaluation of the name, even checks whose success is statically "obvious".]

In the following example, the barrier expression is (currently) not
pure-barrier-eligible:

    type Rec is record
       Flag  : Boolean;
       ... <other stuff> ...
    end record;

    protected type T is
       entry E;
    private
       Data : Rec;
    end T;

    protected body T is
       entry E when Data.Flag is
       begin
          ...
       end E;
    end T;

This proposal is about modifying the definition of pure-barrier-eligible 
(slightly) to change this.

What is the motivation? Why does anyone care about being able to use this sort 
of construct when the Pure_Barriers restriction is in effect?

Lots of folks (notably SPARK) want to be able to use the Pure_Barriers 
restriction (which is part of the Jorvik profile), so this reduces to the 
question of why anyone cares about being able to use this sort of construct in 
any context.

In the above example, why couldn't the user declare Flag as a component of 
type T?

This has to do with the use of predicates.

A predicate for a protected type cannot name a component.

The following example is illegal (which is a good thing that nobody is 
considering changing):

    protected type T
       with Dynamic_Predicate => (Count /= 0) or not Flag
    is
       entry E;
    private
       Flag  : Boolean := False;
       Count : Natural :;
    end T;

    protected body T is
       entry E when Flag is
       begin
          ...;
       end E;
    end T;

An idiom used to get this effect (which is important in SPARK) is to declare 
the protected type with only a single component; that component's type is a 
record which includes the multiple components we "really" want and is subject 
to the desired predicate.

So the above example would be written instead as

    type Rec is record
       Flag  : Boolean := False;
       Count : Natural := 0;
    end record with
       Dynamic_Predicate => (Count /= 0) or not Flag;

    protected type T is
       entry E;
    private
       Data : Rec;
    end T;

    protected body T is
       entry E when Data.Flag is
       begin
          null;
       end E;
    end T;

which is fine until you try to compile it with a Jorvik profile in effect, at 
which point the Data.Flag barrier is rejected.

A brief digression:
    As it happens, SPARK statically enforces subtype predicates in
    some cases where Ada defines no dynamic checks, notably an assignment
    to a subcomponent of an object of a predicate-bearing subtype. If
    anyone is interested in the details, see 
    docs.adacore.com/live/wave/spark2014/html/spark2014_rm/declarations-and-types.html#subtype-predicates

    In the context of non-SPARK Ada, assertions of the form "Data in Rec"
    might need to be added to protected operations of type T to get any
    desired dynamic checking.
[end of digression]

For the sake of specificity, I propose the following wording change:

    Replace the bulleted-list item D.7 (1.3/5)
      - a name that statically denotes a scalar component of the
        immediately enclosing protected unit;
    with
      - a name that denotes a scalar subcomponent of the
        immediately enclosing protected unit which does not
        depend on a discriminant, and which is not part of an
        array.

Obviously this may be subject to further wordsmithing.

Opinions?

****************************************************************

From: Randy Brukardt
Sent: Friday, February 21, 2020  3:26 PM

> A use-case has come up in internal discussions at AdaCore that (IMO) 
> suggests that a small change to the definition of 
> "pure-barrier-eligible" given in AI12-0290 would be appropriate.
> 
> The issue has to do with allowing a name denoting a scalar 
> subcomponent (not just a component) of the immediately enclosing 
> protected object, provided that
>     - the name does not denote a component that depends on a
>       discriminant; and
>     - no prefix of the name denotes an array.
> 
> [The idea is that there are no checks of any kind associated with the 
> evaluation of the name, even checks whose success is statically 
> "obvious".]

This is (approximately) the purpose of the term "statically name" as defined 
in 6.1.1 (paragraphs 24.2-24.5). Would it be possible to use that 
terminology??

...
> For the sake of specificity, I propose the following wording change:
> 
>     Replace the bulleted-list item D.7 (1.3/5)
>       - a name that statically denotes a scalar component of the
>         immediately enclosing protected unit;
>     with
>       - a name that denotes a scalar subcomponent of the
>         immediately enclosing protected unit which does not
>         depend on a discriminant, and which is not part of an
>         array.
> 
> Obviously this may be subject to further wordsmithing.

How about:

     Replace the bulleted-list item D.7 (1.3/5)
       - a name that statically denotes a scalar component of the
         immediately enclosing protected unit;
     with
       - a name that statically names (see 6.1.1) a scalar component 
         of the immediately enclosing protected unit;

Let's not define the same thing twice!!


****************************************************************

From: Tucker Taft
Sent: Friday, February 21, 2020  3:29 PM

> ...
> For the sake of specificity, I propose the following wording change:
> 
>   Replace the bulleted-list item D.7 (1.3/5)
>     - a name that statically denotes a scalar component of the
>       immediately enclosing protected unit;
>   with
>     - a name that denotes a scalar subcomponent of the
>       immediately enclosing protected unit which does not
>       depend on a discriminant, and which is not part of an
>       array.
> 
> Obviously this may be subject to further wordsmithing.
> 
> Opinions?

Go for it.

****************************************************************

From: Randy Brukardt
Sent: Friday, February 21, 2020  3:30 PM

...
> How about:
> 
>      Replace the bulleted-list item D.7 (1.3/5)
>        - a name that statically denotes a scalar component of the
>          immediately enclosing protected unit;
>      with
>        - a name that statically names (see 6.1.1) a scalar component 
>          of the immediately enclosing protected unit;

Probably should talk about a "subcomponent" here rather than a "component".
Still, the change is so obviously better (why would anyone want more 
restrictions than necessary?) that there doesn't really need to be any 
discussion about it (stick it into the presentation AI or an editorial review 
AI).

****************************************************************

From: Tucker Taft
Sent: Friday, February 21, 2020  3:32 PM

>> [The idea is that there are no checks of any kind associated with the 
>> evaluation of the name, even checks whose success is statically 
>> "obvious".]
> 
> This is (approximately) the purpose of the term "statically name" as 
> defined in 6.1.1 (paragraphs 24.2-24.5). Would it be possible to use 
> that terminology??

Good suggestion.  This will allow statically-indexed array components, which 
is a reasonable further relaxation.

> ...
> How about:
> 
>     Replace the bulleted-list item D.7 (1.3/5)
>       - a name that statically denotes a scalar component of the
>         immediately enclosing protected unit;
>     with
>       - a name that statically names (see 6.1.1) a scalar component 
>         of the immediately enclosing protected unit;

I think you need to say "a scalar *sub*component".

****************************************************************

From: Pat Rogers
Sent: Friday, February 21, 2020  4:45 PM

> [Not sending to Ada-Comment because this issue is a low-level detail.]
> 
> A use-case has come up in internal discussions at AdaCore that (IMO) 
> suggests that a small change to the definition of 
> "pure-barrier-eligible" given in AI12-0290 would be appropriate.
> 
> The issue has to do with allowing a name denoting a scalar 
> subcomponent (not just a component) of the immediately enclosing 
> protected object, provided that
>     - the name does not denote a component that depends on a
>       discriminant; and
>     - no prefix of the name denotes an array.
> ...
> 
> Obviously this may be subject to further wordsmithing.
> 
> Opinions?

Looks good to me!

****************************************************************

From: Steve Baird
Sent: Friday, February 21, 2020  5:20 PM

> How about:
> 
>       Replace the bulleted-list item D.7 (1.3/5)
>         - a name that statically denotes a scalar component of the
>           immediately enclosing protected unit;
>       with
>         - a name that statically names (see 6.1.1) a scalar component
>           of the immediately enclosing protected unit;


and then later

> Probably should talk about a "subcomponent" here rather than a "component".

I agree, this is better than my proposed wording. I like it.

> Still, the change is so obviously better (why would anyone want more 
> restrictions than necessary?) that there doesn't really need to be any 
> discussion about it (stick it into the presentation AI or an editorial 
> review AI)

That reasoning sounds suspiciously slippery, but I agree with your conclusion.

The resolution you suggest is fine with me if nobody objects. If someone sees 
a problem with this then please speak up and we'll do things differently.

****************************************************************

From: Tullio Vardanega
Sent: Saturday, February 22, 2020  8:05 AM

I am fine with the outcome of this brief burst.

****************************************************************

From: Tucker Taft
Sent: Saturday, February 22, 2020  10:28 AM

> ...
> 
> So the above example would be written instead as
> 
>   type Rec is record
>      Flag  : Boolean := False;
>      Count : Natural := 0;
>   end record with
>      Dynamic_Predicate => (Count /= 0) or not Flag;

I think this example should probably be:

      Dynamic_Predicate => (Count /= 0) = Flag;

based on other examples we have discussed.  Otherwise Flag is undetermined
(with the first predicate, if Count /= 0, Flag can have any value).

****************************************************************

From: Tucker Taft
Sent: Saturday, February 22, 2020  10:29 AM

An interesting question is whether an analogous relaxation would be 
appropriate for Ravenscar.  That is, should we change D.7(10.12/5) as follows:

Simple_Barriers 

    The Boolean expression in each entry barrier is either a static expression 
    or a name that statically [denotes a component]{names a subcomponent} of 
    the enclosing protected object.

With this change, the Dynamic_Predicate-on-a-record-component trick could work 
with Ravenscar as well.

One side comment on the Dynamic_Predicate trick.  If you make all of the 
components of the record into discriminants (with defaults) then the only 
alterations permitted would be whole-record assignments, which would mean 
there is never an intermediate moment when the predicate wouldn't hold.  
That is, change:

  type Rec is record
     Flag  : Boolean := False;
     Count : Natural := 0;
  end record with
     Dynamic_Predicate => (Count /= 0) or not Flag;

to:

  type Rec
     (Flag  : Boolean := False;
      Count : Natural := 0) is null record
    with
      Dynamic_Predicate => (Count /= 0) = Flag;
         -- incorporates minor fix-up to condition ;-)

and you can ensure that you can never change one without changing the other.

****************************************************************

From: Tullio Vardanega
Sent: Monday, February 24, 2020  7:57 AM

>I think this example should probably be:
>
>      Dynamic_Predicate => (Count /= 0) = Flag;
>
>based on other examples we have discussed.  Otherwise Flag is undetermined 
>(with the first predicate, if Count /= 0, Flag can have any value).

Nice catch.

****************************************************************

From: Tullio Vardanega
Sent: Monday, February 24, 2020  7:59 AM

>An interesting question is whether an analogous relaxation would be 
>appropriate for Ravenscar.  That is, should we change D.7(10.12/5) as follows:
...

Yes, that relaxation should also apply to the Ravenscar profile.

****************************************************************

From: Steve Baird
Sent: Monday, February 24, 2020  12:54 PM

> I think this example should probably be:
> 
>        Dynamic_Predicate => (Count /= 0) = Flag;
> 
> based on other examples we have discussed.  Otherwise Flag is undetermined 
> (with the first predicate, if Count /= 0, Flag can have any value).

It doesn't really matter because this is just an example, but FWIW I intended 
it as I originally wrote it - I did not want Flag to be redundant.

****************************************************************

From: Tucker Taft
Sent: Monday, February 24, 2020  12:58 PM

Got it.

****************************************************************



Questions? Ask the ACAA Technical Agent