!standard 6.1.2(1/5)                             19-10-01    AI12-0334-2/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

The Global and Nonblocking aspects may be defined for nonfirst subtypes,
and referenced via the corresponding attribute. If not specified, the
aspects are inherited from the subtype on which the subtype is based.

For the purposes of checking the conformance to a Global aspect within a
generic unit, the conversion to (or membership test against) a subtype
that is of an access-to-unconstrained type is presumed to dereference
the operand whenever the access subtype is a generic formal subtype, a
parameter subtype of a formal subprogram, or the subtype of a formal
object of mode in out.

The Global and Nonblocking aspects of a subprogram must account for any
global references or potentially blocking operations involved in
evaluating assertion expressions (including preconditions,
postconditions, predicates, and type invariants) that would apply to a
call on that subprogram.

The Global and Nonblocking aspects for a private type or a private
extension must account for evaluation of assertion expressions that
might occur as part of default initialization, finalization, adjustment if
nonlimited, and conversion/membership in the case of a private
extension.

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

Subprograms that make dispatching calls may define their Global
and Nonblocking aspects in terms of their own references and calls
on potentially blocking operations, combined with the Global
and Nonblocking aspects of the particular dispatching operations
they invoke on particular class-wide parameters or globals.
The Global attribute of an object of a class-wide type has a
special syntax that allows an identification of the dispatching
operations invoked on the object.

!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 supposedly nonblocking
subprogram can in fact block if the predicate blocks.

Checking a discriminant or index constraint on an access type implicitly
dereferences the value of the access value. Within a generic, we might
not know whether an access subtype is constrained, so we may need to
assume the worst, namely that the dereference might occur.

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.

As part of a call on a subprogram, we might need to evaluate
various assertion expressions in the form of preconditions, predicates,
postconditions, and/or type invariants, and these might read (or write!) global
variables, or invoke a potentially blocking operation.

Stream and Put_Image attributes internally make dispatching calls on the
stream read/write routines, which can be user written. Nevertheless,
'Image uses a predefined stream and the default implementation of 'Image
should always be effectively Global => null. In general for a subprogram
that internally makes dispatching calls, we probably need a way to
specify its Global aspect in terms of the Global aspects of the
dispatching calls performed on a given classwide object, in combination
with the global references performed directly within the subprogram.

Eventually we might want to allow global variables that are only referenced
in assertion expressions to be identified as "Global => ghost in [out] T"
presuming we have the notion of "ghost" code.

!proposal

(See Summary.)

!wording

Insert before 4.9.1(2/5):

  The Nonblocking aspects (see 9.5) of two entities /statically match/
  if both are static expressions that evaluate to the same value, or if
  their nonblocking expressions come from the same declaration. The
  Global or Global'Class aspects (see 6.1.2) of two entities /statically
  match/ if both consist of a single primitive_global_aspect_definition
  where each is the reserved word NULL, or each is of the form
  "global_mode global_designator" with the same sequence of reserved
  words.

Modify 4.9.1(2/5):

  A subtype statically matches another subtype of the same type if they
  have statically matching constraints, all predicate specifications
  that apply to them come from the same declarations, {Nonblocking and
  Global aspects statically match,} Object_Size (see 13.3) has been
  specified to have a nonconfirming value for either both or neither,
  and the nonconfirming values, if any, are the same, and, for access
  subtypes, either both or neither exclude null. Two anonymous
  access-to-object subtypes statically match if their designated
  subtypes statically match, and either both or neither exclude null,
  and either both or neither are access-to-constant. Two anonymous
  access-to-subprogram subtypes statically match if their designated
  profiles are subtype conformant, and either both or neither exclude
  null.

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] {sub}type (including a formal
  {sub}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.

Add after 6.1.2(14.a/5):

  Syntax

  A dispatching_operation_list is used to identify some or all of
  the dispatching operations of a tagged type T.

    dispatching_operation_list ::=
        ALL
      | /dispatching_/selector_name {, /dispatching_/selector_name}

Add after 6.1.2(15.a/5)
  A /dispatching_/selector_name within a dispatching_operation_list for
  a tagged type T shall resolve to denote a view of one or more
  primitive dispatching operations of T[Redundant:, declared immediately
  within the declarative region in which T is declared].

Modify 6.1.2(17/5):
      [Ed's Note: we are splitting this into multiple paragraphs.]

  The Global aspect for a callable entity defines the global variables
  that might be referenced as part of a call on the entity{, including
  any assertion expressions that might be evaluated as part of the call,
  including preconditions, postconditions, predicates, and type
  invariants}.{

  }The Global aspect for a [composite] {sub}type identifies the
  global variables that might be referenced during default
  initialization, adjustment as part of assignment, [or] finalization of
  an object of the {sub}type{, or conversion to the subtype, including
  the evaluation of any assertion expressions that apply. [Redundant:
  If not specified for {the first subtype of a derived type, the aspect
  defaults to that of the ancestor subtype; if not specified for a
  {nonderived} first subtype the aspect defaults to that of the nearest
  enclosing program unit.] If not specified for a nonfirst subtype S,
  the Global aspect defaults to that of the subtype identified in the
  subtype_indication defining S}. {

  }The Global aspect for an access-to-subprogram object (or {sub}type)
  identifies the global variables that might be referenced when calling
  via the object (or any object of that {sub}type) {including assertion
  expressions that apply}.

  [The Global aspect for any other elementary type is null].

  {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 the same as the Global aspect for its first subtype.}

Add after 6.1.2(38/5):

  AARM Ramification: For a subtype, 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 might not be predefined and thus might have
  a different Global specification than the component types).

Modify 6.1.2(44/5-45/5):

  For a prefix S that statically denotes a subprogram (including a
  formal subprogram), formal object of an anonymous access-to-subprogram
  type, or a {sub}type (including a formal {sub}type), the following
  attribute is defined:

  S'Global
     Identifies the global variable set for each of the [three]
     global_modes, for the given subprogram, object, or {sub}type; a
     reference to this attribute may only appear within a
     global_aspect_definition. {For a subtype to which a
     predicate applies, this includes the global variable sets
     associated with evaluating the predicate.}

Add after 6.1.2(42/5):

  For a prefix X denoting an object of a class-wide type T'Class,
  the following attribute is defined:

  X'Global(dispatching_operation_list)

    X'Global(list) represents the union of the global variable set
    associated with the tagged type T1 identified by the tag of X, and
    the global variable sets of the dispatching operations of T1
    corresponding to the specified dispatching operations of T (or all
    dispatching operations of T if the list is the reserved word ALL); a
    reference to this attribute may only appear within a
    global_aspect_definition. If a /dispatching_/selector_name within
    the list denotes multiple dispatching operations of T, the global
    variable sets of all of the corresponding dispatching operations of
    T1 are included in the union.

Modify 9.5(24/5):

  For a program unit, task entry, formal package, formal subprogram,
  formal object of an anonymous access-to-subprogram type, enumeration
  literal, and for a {sub}type (including a formal {sub}type), the
  following language-defined operational aspect is defined:

Modify 9.5(36/5):

  Unless directly specified, for a formal {sub}type, formal package, or
  formal subprogram, the Nonblocking aspect is that of the actual
  {sub}type, package, or subprogram.

Modify 9.5(47/5):

  S'Nonblocking

     Denotes whether default initialization, finalization, assignment,
     predefined operators, and (in the case of access-to-subprogram
     subtypes) a subprogram designated by a value of {sub}type S are
     considered nonblocking; the type of this attribute is the
     predefined type Boolean. S'Nonblocking represents the nonblocking
     expression of S; evaluation of S'Nonblocking evaluates that
     expression.

Modify 9.5(49/5):

  X'Nonblocking

     Denotes whether the {sub}type of X is considered nonblocking; the
     type of this attribute is the predefined type Boolean.
     X'Nonblocking represents the nonblocking expression of X;
     evaluation of X'Nonblocking evaluates that expression.
     [S'Nonblocking represents the nonblocking expression of S;
     evaluation of S'Nonblocking evaluates that expression.]

Add after 9.5(49.b/5):

  For a prefix X denoting an object of a class-wide type T'Class,
  the following attribute is defined:

  X'Nonblocking(dispatching_operation_list)

    X'Nonblocking(list) represents the AND of the Nonblocking aspect of
    the tagged type T1 identified by the tag of X, and the Nonblocking
    aspects of the dispatching operations of T1 corresponding to the
    specified dispatching operations of T (or all dispatching operations
    of T if the list is the reserved word ALL). If a
    /dispatching_/selector_name within the list denotes multiple
    dispatching operations of T, the Nonblocking aspects of all of the
    corresponding dispatching operations of T1 are ANDed together.

Add after 9.5(65/5):

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

Modify 9.5(68/5):

  Aspect Nonblocking shall be specified for {the first subtype of} a
  derived type only if it fully conforms to the nonblocking expression
  of the ancestor {sub}type or if it is specified to have the Boolean
  literal True. {Aspect Nonblocking shall be specified for a nonfirst
  subtype S only if it fully conforms to the nonblocking expression of the
  subtype identified in the subtype_indication defining S or if it is
  specified to have the Boolean literal True.}

Modify AARM 9.5(88.f/5):

  For checking in P, default initialization, finalization, [or]
  assignment{, or conversion to} [of] a [composite] formal {sub}type F
  is considered to call subprograms that have the nonblocking aspect of
  F'Nonblocking, and this is checked for conformance against that of P
  as described above. [These operations of an elementary formal type are
  considered nonblocking, and thus require no checks.]

Modify 13.1.1(18.1/4):

  If an aspect of a derived type {(or its first subtype)} is inherited
  from an ancestor {(sub)}type  and has the boolean value True, the
  inherited value shall not be overridden to have the value False for
  the derived type {(or its first subtype)}, unless otherwise specified
  in this International Standard. {If an aspect of a nonfirst subtype
  is inherited from the subtype in the subtype_indication that defines
  it, and has the value True, the inherited value shall not be
  overridden to have the value False for the nonfirst subtype, unless
  otherwise specified in this International Standard.}

!discussion

In contrast with the "-1" variant of this AI, in this "-2" variant we
define 'Global and 'Nonblocking as attributes on subtypes rather than
types, and we allow specifying the corresponding aspects. The
alternative of forcing the type Global and Nonblocking aspect
specifications to cover all possible subtypes that might ever be
declared seemed quite limiting, as far as interesting predicates. It
seems clear that some predicates may want to dereference an access
value, or refer to some global variables. Forcing the type declaration
to worry about this seems painful, especially if such global variables
are not visible at the point of the type declaration. Similarly, it
seems painful to require that every time you define an
access-to-unconstrained type, you need to worry about the possibility
that someone might someday define a constrained access subtype.
In most cases we know at compile-time whether such a dereference
will occur. In the case of a generic where we do not know whether
the dereference will occur, we simply assume the worst. Converting
between access subtypes is rare to begin with, and doing so in a generic
is presumably even rarer, so we do not worry about assuming the worst
in this case.

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. Prior to this AI,
                          -- would be legal since scalar
                          -- types didn't block nor access globals.
  begin
      Local := 0; -- Releases the global lock. Also was 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.

=========

We removed the requirement that all elementary types are Global => null,
leaving it to work as for composite types. Note that this requirement
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.

=========

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 nonfirst subtypes incorporate the
Nonblocking and Global characteristics of any applicable predicates.

!appendix

From: Randy Brukardt
Sent: Monday, June 10, 2019  7:45 PM

I didn't review this AI careful, but a couple of comments.

(1) I didn't see anything dealing with the formal subprogram parameter
conversion problem. That seems like a set of amazingly nasty rules, and it
seems completely missing. (That's the hard part IMHO; without that, you
just have a bunch of holes). There's a similar problem caused by in out
formal objects, which also has to be covered.

(2)

...
> Modify 9.5(47/5):
>
>   S'Nonblocking
...
> {For a nonfirst subtype S, S'Nonblocking
>      is False if a predicate that applies to S is potentially blocking.}

"Potentially blocking" is a dynamic concept, not suitable for legality rules
or static definitions of aspect Nonblocking. There's a reason that virtually
the same list of items occurs in the Legality Rules. The problem is the
"during a protected action" case.

We could have defined a static term, but I didn't do it because it would have
been confusing to have "potentially blocking" and "statically potentially
blocking" or some such.

(3) You didn't deal with the 'Put_Image and stream attribute issues; these
need to be addressed as well. (Argubly, we can just ignore the stream
attributes, as they have to be "all", but then many things become
unconditionally "all". This has to be addressed!!).

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

From: Tucker Taft
Sent: Saturday, June 15, 2019  5:50 PM

Here is version 2 of this "fix-up" AI about incorporating the effects of
predicates and friends in Global and Nonblocking aspects. [This was version
/02 of the AI - Editor.]

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

From: Tucker Taft
Sent: Sunday, September 29, 2019  5:55 PM

Here is an update to AI12-0334-2, based on the minutes of the last ARG meeting.
[This is version /03 of the AI - Editor.]

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

From: Randy Brukardt
Sent: Monday, September 30, 2019  9:31 PM

> Here is an update to AI12-0334-2, based on the minutes of the last ARG
> meeting.

I didn't see anything in here as how to fix the definition of the stream
attributes. I suspect that you were planning to use X'Global to define the
Global in terms of the parameter (somehow), but that has to be defined in the AI
-- it's not going to happen by osmosis. (Ergo, we need a redefinition of X'Read
with the appropriate Global applied.) This is probably a good thing anyway,
since the use of X'Global is not obvious and an example is needed (which X'Read
etc. would provide).

I didn't notice any other issues (but I didn't try to figure out how much
violence this does to the assume-the-worst/assume-the-best rules for
Nonblocking, which were constructed assuming that Nonblocking is a type-related
aspect).

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

From: Tucker Taft
Sent: Tuesday, October 1, 2019  1:44 PM

> I didn't see anything in here as how to fix the definition of the
> string attributes. I suspect that you were planning to use X'Global to
> define the Global in terms of the parameter (somehow), but that has to
> be defined in the AI -- it's not going to happen by osmosis. (Ergo, we
> need a redefinition of X'Read with the appropriate Global applied.)
> This is probably a good thing anyway, since the use of X'Global is not
> obvious and an example is needed (which X'Read etc. would provide).

Not sure what you mean by the "fix the definition of the string
attributes".  Perhaps you meant "streaming attributes"?  But even then,
I am not sure what you mean by "fix"?

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

From: Tucker Taft
Sent: Tuesday, October 1, 2019  1:47 PM

I think we also have some issues with the restrictions on Global and
Nonblocking on derived and non first subtypes being overly strict.

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

From: Tucker Taft
Sent: Tuesday, October 1, 2019  2:27 PM

Here is a slight update, mostly just replacing "type" with "subtype" in a
couple of more places.  Randy tells me I am not addressing issues associated
with streaming attributes, but I have lost track of what are the issues!

[This is version /04 of the AI - Editor.]

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

From: Randy Brukardt
Sent: Tuesday, October 1, 2019  2:43 PM

> Not sure what you mean by the "fix the definition of the string 
> attributes".  Perhaps you meant "streaming attributes"?  But even 
> then, I am not sure what you mean by "fix"?

Yes, I meant "stream" (as in my following correction message).

The problem is that the stream attributes don't have any Global or Nonblocking 
aspects, so we need to somehow define what those are. If we don't, they 
default to "all" and "false", and that obviously would be bad for at least 
some uses. (If you're writing to a file, probably it doesn't matter, but if 
you are writing to a buffer, you probably don't want to be forced into "all"
if the buffer is a "null".)

The original problem came from the definition of 'Image, but since we're 
proposing to move that away from streaming, it isn't relevant anymore. But 
it still seems nasty that any streaming forces "all" and "false". I think the
reason you invented the "dispatching" Global was in part for these 
attributes. But then you need to use them. :-)

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

From: Randy Brukardt
Sent: Tuesday, October 1, 2019  2:52 PM

I note that in AI12-0334-1, I had the stream attributes explicitly get 
"in out all" and "false", because it doesn't seem to be well-defined at all. 
So I think it is best that you define what their Global and Nonblocking 
aspects are (if you can do better than "in out all", please do).

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

From: Tucker Taft
Sent: Tuesday, October 1, 2019  3:02 PM

I guess I don't understand why we are defining these at all.  Perhaps what
you are saying is that the *default* implementations need to have specified
Global and Nonblocking.  Clearly if the user defines their own, they can 
pretty much do whatever they want.

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

From: Randy Brukardt
Sent: Tuesday, October 1, 2019  3:25 PM

Stream attributes can be called via dispatching calls, so we need to know what 
to use in that case. And definitely the default implementations need to be 
specified. There's a few words on this topic in an AARM note in AI12-0334-1 
(the counter-part to your AI that I wrote).

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

From: Tucker Taft
Sent: Tuesday, October 1, 2019  3:55 PM

I can understand the situation with default implementations.  I guess there are
default implementations of S'Class'{Read,Write,Input,Output} that make 
dispatching calls on the "appropriate" streaming attribute of the Item 
parameter, so how those work should probably be specified.  But I think when 
the user defines their own streaming subprogram, they have to define their 
own Global aspect -- agreed?


Given that, I propose to add the following after the definition of 
X'Global(dispatching-op-list):


  For the default implementation of a streaming attribute for an
  elementary type (see 13.13.2), the Global aspect is
  Stream'Global(Read) for the Read and Input aspects, and
  Stream'Global(Write) for the Write and Output aspects, where Stream is
  the formal parameter name for the stream parameter.  For the default
  implementation of a streaming attribute for a composite type with
  first subtype S, the Global aspect is S'Global & Stream'Global(Read)
  for the Read and Input aspects, and S'Global & Stream'Global(Write)
  for the Write and Output aspects.
  
    AARM Discussion: We require the Global aspect for a composite
    (first) subtype to include any side-effects associated with
    any non-default streaming attributes of subcomponents, other
    than the usual side effects associated with reading/writing
    the stream itself.  

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

From: Randy Brukardt
Sent: Tuesday, October 1, 2019  4:16 PM

A call on S'{Read,Write,Input,Output} can be a dispatching call (see 3.9.2(1/2) 
- this explicitly defines these as dispatching operations). We need to know the 
Global and Nonblocking aspects for such a dispatching call, and it seems that 
one has to assume an arbitrary user-defined routine could be called from such 
dispatching.
 
Of course, any user-defined routine will have it's own Global/Nonblocking, and 
it's fine for that to be used for statically bound calls (including all 
untagged types). But I don't think that works for dispatching calls.
 
And of course something needs to be said for the class-wide attributes as 
well, but that's a different concern than the one I was discussing.
 
The wording you have is fine as far as it goes, but more needs to be said as 
noted above.

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

From: Tucker Taft
Sent: Tuesday, October 1, 2019  4:32 PM

I've run out of time on this, and I have another commitment this evening.  I'll
try to produce something more before the ARG meeting.

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