Version 1.3 of ai12s/ai12-0334-1.txt

Unformatted version of ai12s/ai12-0334-1.txt version 1.3
Other versions for file ai12s/ai12-0334-1.txt

!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

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


Questions? Ask the ACAA Technical Agent