Version 1.3 of ai12s/ai12-0334-2.txt
!standard 6.1.2(1/5) 19-09-29 AI12-0334-2/03
!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 type{, or conversion to the subtype, including the
evaluation of any assertion expressions that apply. [Redundant: If
not specified for a 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 type)
identifies the global variables that might be referenced when calling
via the object (or any object of that 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(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 might not be predefined and thus might have
a different Global specification than the component types).
Modify 6.1.2(41/5-42/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. {For a nonfirst subtype S, S'Nonblocking
is False if a predicate that applies to S is potentially blocking.}
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; --
return True;
end Seize;
function Release return Boolean
with Nonblocking => False, Global => synchronized in out Lock is
begin
Lock.Release; --
return True;
end Release;
type Wild is range 0 .. 255
with Nonblocking,
Global => null,
Dynamic_Predicate => (if Wild > 200 then Seize else Release);
--
procedure P
with Nonblocking, Global => null is
Local : Wild := 255; --
--
--
begin
Local := 0; --
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; --
private
type Priv is range 0 .. 99; --
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).
****************************************************************
Questions? Ask the ACAA Technical Agent