!standard 6.1.2(1/5) 19-06-15 AI12-0334-2/02 !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 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(26/5): The Nonblocking aspect may be specified for all entities for which it is defined, except for {nonfirst subtypes,} protected operations{,} and task entries. In particular, Nonblocking may be specified for generic formal parameters. 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 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.] !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.] ****************************************************************