!standard 6.1.2(1/5)                                  19-06-10  AI12-0334-1/04
!standard 6.1.2(12/5)
!standard 6.1.2(17/5)
!standard 9.5(65/5)
!class Amendment 19-06-03
!status work item 19-06-03
!status received 19-06-03
!priority Low
!difficulty Medium
!subject Predicates and Global/Nonblocking
!summary

If a type is nonblocking, the predicates that apply to any subtype of that
type also must be nonblocking. Similarly, the Global specification that
applies to a type also applies to any predicates of subtypes of that type.

Predefined operators of elementary types are always Global => null; predefined
operators of composite types inherit the Global specification from their type 
(not the surrounding package).

!problem

A predicate expression can include references to Global objects and
potentially block. However, there is currently no way to indicate that
the predicate of a type has blocking behavior or global reference.
This means that a nonblocking type used in a nonblocking subprogram
can in fact block if the predicate blocks.

Predefined operators are automatically declared along with generic formal types. 
Therefore, we need to be able to determine their Global specification from that 
of the formal type. The current rules do not tie the Global specification to that
of the type.

!proposal

(See Summary.)

!wording

Modify 6.1.2(1/5):

For a program unit, formal package, formal subprogram, formal object of an 
anonymous access-to-subprogram type, and for {any}[a named access-to-subprogram 
type or composite] type (including a formal type), the following 
language-defined aspect may be specified with an aspect_specification (see 
13.1.1):

Modify 6.1.2(12/5):

The Global aspect identifies the set of variables (which, for the purposes of 
this clause includes all constants with some part being immutably limited, or 
of a controlled type, private type, or private extension) global to a callable
entity that are potentially read or updated as part of the execution of a call
on the entity. Constants of any type may also be mentioned in a Global aspect.
If not specified {or otherwise defined below}, the aspect defaults to the 
Global aspect for the nearest enclosing program unit. If not specified for a 
library unit, the aspect defaults to Global => null for a nongeneric library 
unit that is declared Pure, and to Global => in out all otherwise.

[Editor's note: The "if not specified" wording here was a lie with the old rules,
for which elementary types were always Global => null, and it still would be lie
with the proposed rules.]

Modify 6.1.2(17/5): [Note that we split this into three paragraphs.]

The Global aspect for a callable entity defines the global variables that might 
be referenced as part of a call on the entity.{

The Global aspect for any type identifies the global variables that might be 
referenced when evaluating any predicate that applies to a subtype of the type. 
It also identifies the global variables that might be referenced when 
evaluating any stream-oriented attribute (Read, Write, Input, or Output) or the
Put_Image attribute of the type. In addition, the}[The] Global 
aspect for a composite type identifies the global variables that might be 
referenced during default initialization, adjustment as part of assignment, or 
finalization of an object of the type. The Global aspect for an 
access-to-subprogram object (or type) {also} identifies the global variables 
that might be referenced when calling via the object (or any object of that 
type). The Global aspect for {an access-to-object type also 
identifies the global variables that might be referenced when evaluating any
constraint that applies to a subtype of the type}[any other elementary type 
is null].

   {AARM Discussion: A constraint, even one that has dynamic parts, is 
   effectively a constant and does not need to be included in a Global
   specification. However, evaluating a constraint on an access-to-object
   type includes an implicit dereference (since the constraint applies to
   the designated object), and that dereference needs to be included in the
   Global specification for the type.}

{For a predefined operator of an elementary type, the Global aspect is null.
For a predefined operator of a composite type, the Global aspect of the 
operator is same as the Global aspect for the type.}

{For the predefined attributes Image, Put_Image, Read, Write, Input, and Output
(and the class-wide versions of those), the Global aspect is "in out all".}

   {AARM Discussion: The Global'Class for dispatching operations stream 
   operations is "in out all", since we have no way to tell the actual details,
   and we have to allow arbitrary I/O operations and the like in streams.
   Thus, these attributes, which are built on dispatching calls on stream
   operations also have to be "in out all". Image is built on Put_Image,
   so it gets the same problem.}

Add after 6.1.2(37/5):

AARM Ramification: For a type, this includes operations included in 
initialization, adjustment, finalization, and predicate evaluation of
both the type and all of its subcomponents.For a predefined equality operator
of a composite type, this includes the equality operations called by the 
operator (which may not be predefined and thus may have a different Global
specification than the component types).


Add after 9.5(65/5):

For a type for which aspect Nonblocking is True, any predicate expression that 
applies to any subtype of the type shall only contain constructs that are
allowed immediately within a nonblocking program unit.

Add after AARM 9.5(88.g/5):

Additionally, for checking in P, the evaluation of a predicate that applies to
a subtype of a type T is considered to call a subprogram that has the 
nonblocking aspect of T'Nonblocking, and this is checked for conformance against
that of P as described above.

!discussion

An example of the problem in a predicate could be:

   Lock : Some_Protected_Lock_Type;

   function Seize return Boolean 
      with Nonblocking => False, Global => synchronized in out Lock is
   begin
      Lock.Seize; -- Entry call.
      return True;
   end Seize;

   function Release return Boolean
      with Nonblocking => False, Global => synchronized in out Lock is
   begin
      Lock.Release; -- Entry call.
      return True;
   end Release;

   type Wild is range 0 .. 255 
      with Nonblocking,
           Global => null,
           Dynamic_Predicate => (if Wild > 200 then Seize else Release);
         -- Illegal by this AI.

   procedure P 
      with Nonblocking, Global => null is
      Local : Wild := 255; -- Seizes the global lock. But legal
                           -- since scalar types don't block nor 
                           -- access globals.
   begin
       Local := 0; -- Releases the global lock. Also legal.
   end P;

If the declaration of Wild wasn't illegal, then P would be legal even
though the predicate would access a global object and potentially block.
   
=========

The nonblocking rule restricts the predicates that can be applied to 
nonblocking types. This seems OK, since a blocking predicate is unusual to 
begin with.

The Global rule would be incompatible, as the definition was that all
elementary types are Global => null. We removed this requirement, leaving
it work as for composite types. Note that this specification was a bad idea
anyway, as it would lead to a conflict between a private type (which is 
composite) and it's elementary full type.

That is:

      package Foo
         with Global => in out all is

         type Priv is private; -- Global "in out all"

      private

         type Priv is range 0 .. 99; -- Global "null"!!??!!

      end Foo;

To avoid this case, we need to allow elementary types to have arbitrary Global
specifications. (Note that a similar rule is used for Nonblocking.) Having
done that, there is no incompatibility.

=========

In discussing this, we realized that constraints on access-to-object types 
include an implicit dereference and thus any such constraints have to be
covered in the type's Global. Constraints themselves are evaluated only
once and are constants for the purposes of Global, so we only need to worry
about access constraints.

=========

The alternative approach of enforcing the nonblocking and global rules when
a predicate is evaluated doesn't work for generic formal types, where the
details of any predicate that might apply are unknown.

!ASIS

No ASIS impact.

!ACATS test

ACATS B-Tests are needed to check that predicates enforce the Nonblocking
and Global for the type.

!appendix

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