!standard 4.6(24.21/4) 20-08-04 AI12-0380-1/07 !standard 6.1.2(0) !standard 13.1.1(17/5) !standard 13.1.1(18/4) !standard H.4(23.2/5) !standard H.4(23.3/5) !standard H.4(23.4/5) !standard H.7(0) !standard H.7.1(0) !class Amendment 20-06-09 !status Amendment 1-2012 20-07-30 !status ARG Approved 8-0-7 20-07-30 !status work item 20-06-09 !status received 20-06-08 !priority Low !difficulty Medium !subject Fixups for Global annotations !summary A variety of wording improvements and clarifications are made. The "use" and "do" parts of Global from H.7 are moved off into their own aspects (Use_Formal and Dispatching) to reduce confusion. !problem We have identified certain issues with the global aspects: 1) The global rules talk about "operations", but not all entities that Global can be applied to are operations, and the connection is vague. Moreover, Ada doesn't even define the term "operations" (it defines some specific sets of operations like "primitive operations" and "predefined operations", but not plain "operations"). 2) A second problem has to do with when parts of a parameter or named global variable are visibly of an access-to-object type. We don't want to limit what can be done with such visible access objects, nor require such effects be included in the global aspects. There is essentially no way a subprogram can know what such access values might designate. The caller might know more, or they might have received such an access value as part of a parameter from their caller. 3) There seems to be no rule restricting conversions between access-to-subprogram types with different global aspects. 4) In H.7, there seems to be no single definition of what is a "formal parameter set." 5) In H.7, the Global aspect of an elementary base subtype should be specified as always NULL. 6) The syntax of the Global aspect uses "," both as a separator between global_aspect_elements and within a single global_set. The syntax disallows the use of ALL or SYNCHRONIZED inside parentheses, which disallows the use of, for example, "IN ALL" inside the parentheses. 7) Combining the use of generic formal parameters and the use of dispatching operations into the Global aspect creates additional complexity, and renders the meaning of "Global => null" to some extent ambiguous, as it is not clear whether the "null" also applies to the use of generic formals. Furthermore, these two kinds of specifications are also relevant to the Nonblocking aspect, so separating them from the Global aspect would make it more natural for them to apply to any aspect that might depend on either the use of generic formals or dispatching calls. Should we try to address these problems? (Yes.) !proposal We propose to address the above problems as follows: 1) 6.1.1(19/5) attempts to explain the use of "operation" in the rules for Global, but it is really terse and fails to clarify the connection between the operations and the entities on which Global is specified. We try to clarify the wording, and also add a reminder in H.7 about this model. 2) To deal with parts of a parameter or a global that are visibly of an access-to-object type, we propose to adopt semantics similar to what we have proposed for generic formal parameters, namely, it is the caller's responsibility to worry about global effects when the called subprogram would have no idea what they might be. Eventually we might allow a subprogram to override the "mode" of the access values that are visible parts of a parameter or global, down from access-to-variable to access-to-constant, or even further down to "never dereferenced," to more precisely indicate how it uses such access-to-object parts, but we leave that capability for a future revision. 3) We propose to limit conversions between access-to-subprogram types where we require the target type has a superset of the global variable sets of the operand type. 4) We propose additional wording to clarify the meaning of "formal parameter set." 5) We propose additional wording to specify the default for the global aspect of a non-derived elementary type to be NULL, in the absence of a predicate. 6) We switch to using ";" to separate global_aspect_elements inside parentheses. We allow ALL and SYNCHRONIZED inside parentheses. 7) We propose to split off the use of generic formals and dispatching operations into their own aspects, in particular "Use_Formal" and "Dispatching" aspects. This also allows us to eliminate the extended_global_aspect_definition and extended_global_aspect_element from the Global aspect syntax. !wording Add after 4.6(24.21/4): If the target type has a Global aspect other than IN OUT ALL or Unspecified, then each mode of the Global aspect of the operand type shall identify a subset of the variables identified by the corresponding mode of the target type Global aspect, or by the IN OUT mode of the target type Global aspect. Replace 6.1.2(3/5) with: global_aspect_definition ::= null | Unspecified | global_mode global_designator | (global_aspect_element{; global_aspect_element}) Replace 6.1.2(4/5) with: global_aspect_element ::= global_mode global_set | global_mode ALL | global_mode SYNCHRONIZED Add after 6.1.2(13/5) [so we can avoid having to repeatedly identify both the Global and the Global'Class aspects] Together, we refer to the Global and Global'Class aspects as /global/ aspects. Replace 6.1.2(19/5): The following is defined in terms of operations; the rules apply to all of the above kinds of entities. with: The following is defined in terms of operations that are performed by or on behalf of an entity. The rules on operations apply to the entity(s) associated with those operations. AARM Discussion: The operations performed by a callable entity are those associated with the body of the entity. For other kinds of entities (such as subtypes, see H.7), we explicitly list the associated operations. Delete 13.1.1(17/5): [AI author's note: this paragraph lists declarative items for which there were no language-defined aspects. This list has become a bit of a maintenance headache, and seems to be written more as an informational list rather than a normative rule. In any case, the key normative intent has now been combined into (18/4) below.] [There are no language-defined aspects that may be specified on a renaming_declaration, a subunit, a package_body, a task_body, a protected_body, an entry_body, or a body_stub other than a subprogram_body_stub.] Modify 13.1.1(18/4): {Unless specified otherwise, a}[A] language-defined aspect shall not be specified in an aspect_specification given on a completion of a [subprogram or generic subprogram]{program unit}. Modify H.4(23.2/5-23.5/5): No_Hidden_Indirect_Globals When within a context where {an}[the] applicable {g}[G]lobal aspect is neither Unspecified nor IN OUT ALL, any execution within such a context does neither of the following: * Update {(or return a writable reference to)} a variable that is reachable via a sequence of zero or more dereferences of access-to-object values {from a parameter of a visibly access-to-constant type}, from a {part of a non-access-type} formal parameter of mode IN (after any OVERRIDING -- see H.7), or from a global that {has mode IN or} is not within the applicable global variable set[, or has mode IN]{, unless the initial dereference is of a part of a formal parameter or global that is visibly of an access-to-variable type}; * Read {(or return a readable reference to)} a variable that is [updatable]{reachable} via a sequence of zero or more dereferences of access-to-object values from a global that is not within the applicable global variable set{, unless the initial dereference is of a part of a formal parameter or global that is visibly of an access-to-object type}. AARM Ramification: The above two rules specify that any {hidden} indirect references are covered by the [G]{g}lobal or formal parameter modes that apply, and {that such references} are *not* subject to alternative paths of access (such as aliasing) that could result in conflicts. {On the other hand, any visible access-to-object parts are allowed to designate objects that are accessible via other means, and side-effects on such objects are permitted if the value is visibly of an access-to-variable type. Such effects do not need to be covered by the applicable global aspect(s), but are rather for the caller to worry about.} For the purposes of the above rules{: * a part of an object is /visibly of an access type/ if the type of the object is declared immediately within the visible part of a package specification, and at the point of declaration of the type the part is visible and of an access type; * a function /returns a writable reference to V/ if it returns a result with a part that is visibly of an access-to-variable type designating V; similarly, a function /returns a readable reference to V/ if it returns a result with a part that is visibly of an access-to-constant type designating V; *} if an applicable global variable set includes a package name, and the collection of some pool-specific access type (see 7.6.1) is implicitly declared in a part of the declarative region of the package included within the global variable set, then all objects allocated from that collection are considered included within the global variable set. Replace H.7(2/5-11/5) with the following [prior content largely moved to H.7.1]: The following additional syntax is provided to override the mode of a formal parameter to reflect indirect effects on variables reachable from the formal parameter by one or more access-value dereferences: extended_global_mode ::= OVERRIDING basic_global_mode Delete H.7(12/5) [moved to H.7.1]. Delete H.7(14/5) [moved to H.7.1]. Delete H.7(16/5-17.a/5) [moved to H.7.1]. Add after H.7(15/5): Redundant[As described in 6.1.2, the following rules are defined in terms of operations that are performed by or on behalf of an entity.] Modify H.7(18/5): The Global aspect for a subtype identifies the global variables that might be referenced by the following operations of the subtype: default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. 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 {composite} first subtype the aspect defaults to that of the enclosing library unit{; if not specified for a nonderived elementary first subtype (or scalar base subtype), the aspect defaults to NULL in the absence of a predicate, and to that of the enclosing library unit otherwise}. If not specified for a nonfirst subtype S, the Global aspect defaults to that of the subtype identified in the subtype_indication defining S. Delete H.7(21/5-22/5) [moved to H.7.1]. Add the following subclause: H.7.1 The Use_Formal and Dispatching Aspects The Use_Formal and Dispatching aspects are provided to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation, enabling more precise checking of conformance with the Nonblocking and global aspects that apply at the point of invocation of the operation. For any declaration within a generic unit for which a global or Nonblocking aspect may be specified, other than a generic_formal_parameter_declaration, the following aspect may be specified to indicate which generic formal parameters are /used/ by the associated entity: Use_Formal The aspect is specified with a formal_parameter_set, with the following form: formal_parameter_set ::= formal_group_designator | formal_parameter_name | (formal_parameter_name{, formal_parameter_name}) formal_group_designator ::= null | all formal_parameter_name ::= /formal_/subtype_mark | /formal_subprogram_/name | /formal_access_to_subprogram_object_/name For any declaration for which a global or Nonblocking aspect may be specified, other than for a library package, a generic library package, or a generic formal, the following aspect may be specified: Dispatching The aspect is specified with a dispatching_operation_set, with the following form: dispatching_operation_set ::= dispatching_operation_specifier | (dispatching_operation_specifier{, dispatching_operation_specifier}) dispatching_operation_specifier ::= /dispatching_operation_/name (/object_/name) Name Resolution A formal_parameter_name in a Use_Formal aspect shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type [Redundant: of an enclosing generic unit or visible formal package]. The /object_/name of a dispatching_operation_specifier shall resolve to statically name an object (including possibly a formal parameter) of a tagged class-wide type T'Class, or of an access type designating a tagged class-wide type T'Class; the /dispatching_operation_/name of the dispatching_operation_specifier shall resolve to statically denote a dispatching operation associated with T. Static Semantics The /formal parameter set/ is identified by a set of formal_parameter_names. Alternatively, the reserved word NULL may be used to indicate none of the generic formal parameters, or ALL to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) might be used within the execution of the operation. If there is no formal parameter set specified for an entity declared within a generic unit, it defaults to ALL. The /dispatching operation set/ is identified by a set of dispatching_operation_specifiers. It indicates that the Nonblocking and global effects of dispatching calls that match one of the specifiers need not be accounted for by the Nonblocking or global aspect, but are instead to be accounted for by the invoker of the operation. A dispatching call matches a dispatching_operation_specifier if the name or prefix of the call statically denotes the same operation(s) as that of the dispatching_operation_specifier, and at least one of the objects controlling the call is denoted by, or designated by, a name that statically names the same object as that denoted by the object_name of the dispatching_operation_specifier. In the absence of any dispatching_operation_specifiers, Nonblocking and global aspects checks are performed at the point of a dispatching call within the operation using the Nonblocking and Global'Class aspects that apply to the named dispatching operation. AARM Ramification: The object "controlling the call" is not necessarily a controlling parameter of the call if the call is a function with a controlling result or has parameters that is such a function. It is one of the objects that provide the dispatching tag used for the call; that could, for example, be a parameter of a function used as a parameter to the call, or an object being assigned to, or a parameter of an enclosing call. Legality Rules Within an operation to which a Use_Formal aspect applies, if the formal parameter set is anything but ALL, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set. When an operation (or instance thereof) to which a Use_Formal aspect applies is invoked, Nonblocking and global aspect checks are performed presuming each generic formal parameter (or corresponding actual parameter) of the formal parameter set is used at least once. Within an operation to which a Dispatching aspect applies, any dispatching call that does not match any dispatching_operation_specifier of the dispatching operation set is checked using the Nonblocking and Global'Class aspect(s) applicable to the called dispatching operation; if there is a match, there is no checking against the Nonblocking or global aspects applicable at the point of call. When an operation to which a Dispatching aspect applies is invoked, Nonblocking and global aspect checks are performed presuming each named dispatching operation is called at least once, with the named object controlling the call, ignoring those dispatching calls that would match a dispatching_operation_specifier applicable at the point of invocation of the operation. !discussion See !problem and !proposal for most of the rationale. The shift of perspective on visible access-to-variable parts was brought about by considerations of "Stable" views and "Implicit_Dereference" types. These both have visible access-to-object parts (discriminants) and in many cases the caller knows what they designate, or at least what is the enclosing container. It is hopeless for the called routine to correctly describe its effects on such objects, without using something like "X.all" which we no longer allow. Nevertheless, in many contexts, the caller knows quite well what object is being updated, and must account for these effects if the caller did not similarly receive the Stable view or Implicit_Dereference object from its caller. Even allowing a subprogram to specify in its Global aspect something like "Param.Disc.all", we would still be stuck with the caller having to know where Param.Disc points. So we are simply saying that if you pass an object with a visible access-to-object part, you need to presume it is going to dereference the corresponding access value. We also talk explicitly about "references" returned by a function. The *intent* is that it is OK if a function returns a reference to an object "reachable" from one of its parameters, so long as it is only a writable reference if the original parameter was [IN] OUT or access-to-variable. If the function "knows" it is returning a reference to an object that is reachable from a Global, the function needs to indicate it is referencing that Global, with the appropriate mode. The finalization of a Constant_Reference is not referencing any new object, so there is no need to say anything. When a Constant_Reference is created, the creator has to fess up whether or not it is a Global or simply a part of something more local, and that use of a Global will be propagated to all of the callers of the creator of the Constant_Reference. !example Here are some examples of the OVERRIDING global mode, and of Dispatching aspects: type T is tagged private with Input => Stream_Input; procedure Display (X : in T; F : in Ada.Text_IO.File_Type := Ada.Text_IO.Current_Input) with Global => overriding in out F; function Stream_Input (Str : not null access Ada.Streams.Root_Stream_Type'Class) return T with Dispatching => Read (Str); -- NOTE: requires allowing object_name to denote an object -- that designates a class-wide object -- (discussed above) procedure Fill (X : out T'Class; Str : aliased in out Ada.Streams.Root_Stream_Type'Class) with Global => in Debug, Dispatching => (T'Input (X), Display (X), Read (Str)); ... procedure Fill (X : out T'Class; Str : aliased in out Ada.Streams.Root_Stream_Type'Class) is begin X := T'Input (Str'Access); if Debug then Display (X); end if; end Fill; Here is an example of how the No_Hidden_Indirect_Globals restriction is enforced: pragma Restrictions (..., No_Hidden_Indirect_Globals, ...); ... package P is type G is private; type Ref (Data : access T) is null record; Glob : G; ... function F (C : aliased in out Container; Pos : Cursor) return Ref with Global => in Glob; ... private type G is record Info : access T; end record; end P; package body P is ... function F (C : aliased in out Container; Pos : Cursor) return Ref is begin return Ref'(Data => Glob.Info); -- Error -- the above returns a writable reference to Glob.Info.all, -- but Glob is of mode IN, and Glob.Info.all is reachable -- from Glob. end F; ... end P; !corrigendum 4.6(24.21/4) @dinsa @xinbull @dinst @xinbull or Unspecified, then each mode of the Global aspect of the operand type shall identify a subset of the variables identified by the corresponding mode of the target type Global aspect, or by the @b mode of the target type Global aspect.> !corrigendum 6.1.2(0) @dinsc Dummy to force a conflict; the wording changes are in the conflict file. !corrigendum 13.1.1(17/5) @ddel There are no language-defined aspects that may be specified on a @fa, a @fa, a @fa, a @fa, a @fa, a @fa, or a @fa other than a @fa. !corrigendum 13.1.1(18/4) @drepl A language-defined aspect shall not be specified in an @fa given on a completion of a subprogram or generic subprogram. @dby Unless specified otherwise, a language-defined aspect shall not be specified in an @fa given on a completion of a program unit. !corrigendum H.4(23) @dinsa @xhang<@xtermDuring the execution of a subprogram by a task, no other task invokes the same subprogram.> @dinss @xhang<@xterm> Find the rest in the conflict file. !corrigendum H.7(0) @dinsc In addition to the entities specified in 6.1.2, the Global aspect may be specified for a subtype (including a formal subtype), formal package, formal subprogram, and formal object of an anonymous access-to-subprogram type. @s8<@i> The following additional syntax is provided to override the mode of a formal parameter to reflect indirect effects on variables reachable from the formal parameter by one or more access-value dereferences: Find the rest in the conflict file. !corrigendum H.7.1(0) @dinsc The Use_Formal and Dispatching aspects are provided to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation, enabling more precise checking of conformance with the Nonblocking and global aspects that apply at the point of invocation of the operation. For any declaration within a generic unit for which a global or Nonblocking aspect may be specified, other than a @fa, the following aspect may be specified to indicate which generic formal parameters are @i by the associated entity: @xhang<@xtermThe aspect is specified with a @fa, with the following form:> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa@hr @ @ |@ @fa@hr @ @ |@ (@fa{, @fa})> @xindent<@fa@fa<@ ::=@ >@b | @b> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @i@fa@hr @ @ |@ @i@fa@hr @ @ |@ @i@fa> For any declaration for which a global or Nonblocking aspect may be specified, other than for a library package, a generic library package, or a generic formal, the following aspect may be specified: @xhang<@xtermThe aspect is specified with a @fa, with the following form:> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa@hr @ @ |@ (@fa{, @fa})> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @i@fa (@i@fa)> @s8<@i> A @fa in a Use_Formal aspect shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type of an enclosing generic unit or visible formal package. The @i@fa of a @fa shall resolve to statically name an object (including possibly a formal parameter) of a tagged class-wide type @i'Class, or of an access type designating a tagged class-wide type @i'Class; the @i@fa of the @fa shall resolve to statically denote a dispatching operation associated with @i. @s8<@i> The @i is identified by a set of @fas. Alternatively, the reserved word @b may be used to indicate none of the generic formal parameters, or @b to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) might be used within the execution of the operation. If there is no formal parameter set specified for an entity declared within a generic unit, it defaults to @b. The @i is identified by a set of @fas. It indicates that the Nonblocking and global effects of dispatching calls that match one of the specifiers need not be accounted for by the Nonblocking or global aspect, but are instead to be accounted for by the invoker of the operation. A dispatching call matches a @fa if the @fa or @fa of the call statically denotes the same operation(s) as that of the @fa, and at least one of the objects controlling the call is denoted by, or designated by, a @fa that statically names the same object as that denoted by the @i@fa of the @fa. In the absence of any @fas, Nonblocking and global aspects checks are performed at the point of a dispatching call within the operation using the Nonblocking and Global'Class aspects that apply to the named dispatching operation. @s8<@i> Within an operation to which a Use_Formal aspect applies, if the formal parameter set is anything but @b, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set. When an operation (or instance thereof) to which a Use_Formal aspect applies is invoked, Nonblocking and global aspect checks are performed presuming each generic formal parameter (or corresponding actual parameter) of the formal parameter set is used at least once. Within an operation to which a Dispatching aspect applies, any dispatching call that does not match any @fa of the dispatching operation set is checked using the Nonblocking and Global'Class aspect(s) applicable to the called dispatching operation; if there is a match, there is no checking against the Nonblocking or global aspects applicable at the point of call. When an operation to which a Dispatching aspect applies is invoked, Nonblocking and global aspect checks are performed presuming each named dispatching operation is called at least once, with the named object controlling the call, ignoring those dispatching calls that would match a @fa applicable at the point of invocation of the operation. !ASIS No ASIS effect. !ACATS test ACATS B-Tests are needed to check that the updated rules are enforced. !appendix From: Randy Brukardt Sent: Thursday, July 2, 2020 10:01 PM I have a number of questions about the syntax for a list of global specifications. This is written as a comma-delimited list inside of parens: with Global => (in all, in out synchronized); with Global => (in all, use null); with Global => (null, use null); with Global => (in all, use Element_Type, Index_Type); As it turns out, none of the above are legal with the grammar as currently defined. Showing just the interesting part: global_aspect_definition ::= | (global_aspect_element{, global_aspect_element}) global_aspect_element ::= global_mode global_set | extended_global_aspect_element global_set ::= global_name {, global_name} extended_global_aspect_element ::= use formal_parameter_set formal_parameter_set ::= formal_group_designator | formal_parameter_name{, formal_parameter_name} A global_aspect_element does not allow any of the keywords null, all, or synchronized. When I asked Tucker about this, he said that the global_set should have included all and synchronized: global_set ::= all | synchronized | global_name {, global_name} He also says that "null" is the absence of anything, and should never appear elsewhere. I find this odd, as it makes the grammar less consistent that it otherwise would be. And to me, the most important thing that you can say about a subprogram is that it has Global => null - the idea that it carries no information seems backwards to me ("in out all" carries no information - it says anything goes). I also think it is likely to be confusing that you can give most, but not all of the standalone global specifications as a list element. Moreover, if one has a package that has a non-null global specification, you would need to specify null on any nested subprograms to get that. Specifying nothing other than some formal parameters must inherit the enclosing package's global specification - there is no other way to modify the inherited specification. That is: with Global => use null would specify using the enclosing package's global specification minus any formal parameter's specification. (When we had a Global attribute, one could get a package's global specification using that attribute to name it, but that is now gone.) The containers have a number of routines that are specified as Global => (null, use null) to ensure that they depend on nothing other than the subprogram's parameters, regardless of what formals or the enclosing package is specified as. This seems to be like it will come up for a few routines (especially property functions) in most generic ADTs; one needs a way to get such a specification. Should we allow "null" to appear as a list element? --- Aside: This grammar is also weird as we have lists of lists all separated by the same separator - a comma. Each list is headed by one or more keywords, so a computer can parse it -- I'm not as convinced about humans. For example, the last Global example given above is *two*, not, three elements: "in all" and "use Element_Type, Index_Type". A human could misparse this, especially in an example where all of the elements have names: with Global => (in Usage_Data, use Element_Type, Index_Type); Does this come from SPARK (in which case we're probably stuck with it) or is this something we can change? I don't think there is anything like this in Ada currently, and it seems to violate the human factors part of our goals. End Aside. In any case, we need to adjust the grammar to allow the keywords all and synchronized. Whether to allow more is TBD. **************************************************************** From: Claire Dross Sent: Friday, July 3, 2020 3:55 AM [...] > > When I asked Tucker about this, he said that the global_set should > have included all and synchronized: > > global_set ::= all | synchronized > | global_name {, global_name} > > He also says that "null" is the absence of anything, and should never > appear elsewhere. I suppose he means after "use" right? Because, AFAICS, Global => null is allowed (and is not the default IIRC). FWIW, it feels natural to me that Global => null really means Global => null, use => null. I also find it pretty clear that Global => use F means Global => null, use => F. As for all and synchronized, I agree that it can make sense to have them in a list of global_aspect_element. > I find this odd, as it makes the grammar less consistent that it > otherwise would be. And to me, the most important thing that you can > say about a subprogram is that it has Global => null - the idea that > it carries no information seems backwards to me ("in out all" carries > no information - it says anything goes). I am not sure I understand you very well. Global => null is allowed by the current wording, no? > Aside: This grammar is also weird as we have lists of lists all > separated by the same separator - a comma. > Each list is headed by one or more keywords, so a computer can parse > it -- I'm not as convinced about humans. > For example, the last Global example given above is *two*, not, three > elements: "in all" and "use Element_Type, Index_Type". A human could > misparse this, especially in an example where all of the elements have > names: > > with Global => (in Usage_Data, use Element_Type, Index_Type); > > Does this come from SPARK (in which case we're probably stuck with it) > or is this something we can change? I don't think there is anything > like this in Ada currently, and it seems to violate the human factors part > of our goals. > End Aside. Nothing to do with SPARK, where we don't even have "use" parts. Also, I don't think that anyone requests the Ada syntax to match the SPARK syntax (as opposed to matching the semantics). Global for Ada and Global for SPARK already do not share the same syntax at all. **************************************************************** From: Tucker Taft Sent: Friday, July 3, 2020 9:21 AM As Claire indicated, this does not have much to do with SPARK at this point, because SPARK has never used "in", "in out", and "out" but rather Input, In_Out, and Output as labels, in a strictly aggregate-like syntax. We pretty early on (probably well before even Ada 2012 was stabilized) presumed we would switch to using reserved words "in" and "out" in the Global syntax when/if we brought it to Ada. SPARK was trying to avoid going beyond the aggregate syntax on its own. So certainly we need to allow "synchronized" and "all" inside parentheses. The question on "null" is separate, as is the issue of separating in and out lists with ',' or using some other approach. SPARK uses extra levels of parentheses. E.g.: with Global => (Input => (X, Y), In_Out => (A, B)) This seemed unnecessary once we used reserved words, but I accept your point that having comma separate groups as well as individual items is unprecedented in Ada. So let's separate these three issues: 1) Allow "synchronized" and "all" inside the parentheses. ==> I think we all agree this was just an oversight, so no controversy here 2) Separate "in", "in out", and "out" groups by something other than a comma. a) Use nested lists, such as: "with Global => (in (X, Y), in out (A, B), use (Key, Element))" b) Require a mode in front of each element, such as: "with Global => (in X, in Y, in out A, in out B, use Key, use Element)" c) Use semicolons, such as: "with Global => (in X, Y; in out A, B; use Key, Element)" d) [current rule] Rely on reserved words as separators: "with Global => (in X, Y, in out A, B, use Key, Element)" 3) Should "null" be allowed "inside" parentheses? a) Yes in all cases, but it is redundant in all cases b) Yes, but only if there is no "in", "in out", or "out" group already there, and it is redundant c) It is *required* if there is no "in", "in out", or "out" group already there, so it is *not* redundant d) [current rule] Never. The only time it can appear is by itself, in "Global => null". In the absence of "in", "in out", or "out" then there is no global access except that which might be performed by a generic formal or a dispatching call. Effectively "Global => null" is equivalent to "Global => ()" -- there is nothing magic about the word "null" other than an absence of anything else (including an absence of "Unspecified"). My thoughts on the above: (1) No debate here (2) Of the above, (a) seems OK but verbose, and (c) seems reasonable given its similarity to parameter specifications, though I am also happy with the status quo (d). (3) I don't like redundancy, as that just becomes another coding style battle, similar to what we have with "in" mode. So to me that argues for (c) or (d), with a personal preference for (d), treating "null" as effectively equivalent to "()". I suspect people are going to be annoyed by having to write "null" explicitly when they have already omitted the various "in", "in out", and "out" groupings. And to some extent, I find it somewhat unhelpful to say "(null, use Key, Element)" since it seems to be saying two potentially contradictory things. But as indicated, I am OK with (c) as it also avoids redundancy. **************************************************************** From: Richard Wai Sent: Friday, July 3, 2020 9:47 AM > 2) Separate "in", "in out", and "out" groups by something other than a > comma. > a) Use nested lists, such as: > "with Global => (in (X, Y), in out (A, B), use (Key, Element))" > b) Require a mode in front of each element, such as: > "with Global => (in X, in Y, in out A, in out B, use Key, use Element)" > c) Use semicolons, such as: > "with Global => (in X, Y; in out A, B; use Key, Element)" > d) [current rule] Rely on reserved words as separators: > "with Global => (in X, Y, in out A, B, use Key, Element)" I'm strongly for (a) in this case. I agree with Randy that there is a serious readability problem with (d). (a) is much easier for human parsing, and it also has the benefit of being similar to how SPARK is currently doing it. > 3) Should "null" be allowed "inside" parentheses? > a) Yes in all cases, but it is redundant in all cases > b) Yes, but only if there is no "in", "in out", or "out" > group already there, and it is redundant > c) It is *required* if there is no "in", "in out", or "out" > group already there, so it is *not* redundant > d) [current rule] Never. The only time it can appear is > by itself, in "Global => null". In the absence of > "in", "in out", or "out" then there is no global access > except that which might be performed by a generic > formal or a dispatching call. Effectively "Global => null" > is equivalent to "Global => ()" -- there is nothing magic > about the word "null" other than an absence of anything > else (including an absence of "Unspecified"). I'd say (d) seems the most reasonable in this group. I expect setting Global => null will be fairly common. It seems that (c) also does something similar, though I am not sure I understand it. **************************************************************** From: Tucker Taft Sent: Friday, July 3, 2020 10:26 AM > I'm strongly for (a) in this case. I agree with Randy that there is a > serious readability problem with (d). (a) is much easier for human > parsing, and it also has the benefit of being similar to how SPARK is > currently doing it. Other than the consistency with SPARK, what makes (a) strongly preferable to (c) in your view? **************************************************************** From: Tucker Taft Sent: Friday, July 3, 2020 10:50 AM Also, if there is just one element in each, would you prefer (or allow): with Global => (in (X), in out (A), use (Key)) or with Global => (in X, in out A, use Key) or with Global => (in X; in out A; use Key) I think the issue of single-element lists argues a bit in favor of using a semicolon as a separator rather than having to decide whether to allow single-element parentheses. **************************************************************** From: Richard Wai Sent: Friday, July 3, 2020 11:05 AM > Other than the consistency with SPARK, what makes (a) strongly > preferable to (c) in your view? > Really I just found it more visually distinct than ';', though (c) was my kind of second favorite. I recognize that there is some consistency with (c) in regards to subprogram parameters, namely Subprog (X, Y: in Integer; A,B: in out Character). But without actually having types in there, I though (c) risked becoming too cluttered/compressed with the A,B,C; presentation. But to be totally honest, the more I look at it, the more (c) looks generally consistent with Ada. I'd still say (a) is more readable all things considered, but I'm also a big fan of consistency. It seems like (c) is growing on me the more I sit with it.. Looking forward to what everyone else has to say! **************************************************************** From: Richard Wai Sent: Friday, July 3, 2020 11:14 AM > I think the issue of single-element lists argues a bit in favor of > using a semicolon as a separator rather than having to decide whether > to allow single-element parentheses. That is a really good point that I didn't consider. I think when it comes to single elements the semicolon clearly wins here, and requiring parenthesis for single elements would be a real pain. Given that there will always be a keyword following a semicolon to create the visual regularity and separation, the semicolon approach probably does solve the readability problem. **************************************************************** From: Jeff Cousins Sent: Friday, July 3, 2020 1:46 PM Re 2), d) looks horrible. In a parameter list, one might have: (X, Y : in In_Type; A, B : in out In_Out_Type) which clearly looks most like c) of the options listed. But a parameter list would also allow (most coding standards would prefer): (X : in In_Type; Y : in In_Type; A : in out In_Out_Type; B : in out In_Out_Type) So maybe the global list syntax should also allow: with Global => (in X; in Y; in out A; in out B; use Key, Element) a hybrid of b) and c). **************************************************************** From: Tucker Taft Sent: Friday, July 3, 2020 2:21 PM This is pretty much what I was hoping to avoid. There seems no real need for flexibility here -- it would just mean we would have to agree on coding standards! ;-) The current rule allows a given global mode only once. I think that is a nice rule... Note that unlike parameter lists, where order might be significant, and you might want to interleave in, in-out, and out parameters, there is no order dependence in the Global aspect, so grouping them together imposes no hardship, and minimizes the number of things left for coding-convention battles. **************************************************************** From: John Barnes Sent: Friday, July 3, 2020 4:31 PM It is not true that Spark never used in, out, and in out in globals. That’s exactly what it did use when the annotations were in Ada comments. It was only when Spark 2005 migrated to Spark 2014 that it couldn’t do that anymore but had to use the revolting Input etc. I fear this topic is looking like rather a mess. Maybe I should ignore it when I rewrite my book! (Hopefully joking) **************************************************************** From: Tucker Taft Sent: Friday, July 3, 2020 4:58 PM Thanks for reminding us! An example of a global annotation in "old" SPARK is: --# global in I; in out J, K; out L; So (2)(c) which uses ";" to separate groups is consistent with that. **************************************************************** From: Randy Brukardt Sent: Friday, July 3, 2020 5:31 PM > I suppose he means after "use" right? He meant in a list of global "elements". Sorry I didn't make that clear. > Because, AFAICS, Global => null > is allowed (and is not the default IIRC). FWIW, it feels natural to me > that Global => null really means Global => null, use => null. If that was the case, I would be much less concerned about this topic. But as it stands, "use all" is the default, so Global => null means Global => (null, use all); Of course, if we made that change, it would be more complex to treat "use" as an Annex H thing, and moreover, many generic units would need "Global => use all" as their overall Global specification rather than "Global => null". But given that would be much more honest, I think I'd be in favor assuming the Annex H issues could be worked out. > I also find it pretty clear that Global => use F means Global => null, use => > F. As for all and synchronized, I agree that it can make sense to have > them in a list of global_aspect_element. > >> I find this odd, as it makes the grammar less consistent that it otherwise >> would be. And to me, the most important thing that you can say about a >> subprogram is that it has Global => null - the idea that it carries no >> information seems backwards to me ("in out all" carries no information - it >> says anything goes). > >I am not sure I understand you very well. Global => null is allowed by >the current wording, no? Yes, but Global => (null, use F) is not allowed by the wording/grammar. I was thinking of the global_element case being rather different than the top-level Global. ... >> Does this come from SPARK (in which case we're probably stuck with it) or is >> this something we can change? I don't think there is anything like this in >> Ada currently, and it seems to violate the human factors part of our goals. >> End Aside. > >Nothing to do with SPARK, where we don't even have "use" parts. Also, >I don't think that anyone requests the Ada syntax to match the SPARK >syntax (as opposed to matching the semantics). Global for Ada and >Global for SPARK already do not share the same syntax at all. OK, thanks. So we can have the best syntax here, all we have to do is agree on what "best" is. Considering I can't even make up my own mind, that's going to be difficult. **************************************************************** From: Randy Brukardt Sent: Friday, July 3, 2020 5:49 PM > So let's separate these three issues: > > 1) Allow "synchronized" and "all" inside the parentheses. > ==> I think we all agree this was just an oversight, so no controversy > here Agreed. I put it into this message mainly so that no one is surprised that it is included in the eventual AI. > 2) Separate "in", "in out", and "out" groups by something other than a comma. > a) Use nested lists, such as: > "with Global => (in (X, Y), in out (A, B), use (Key, Element))" > b) Require a mode in front of each element, such as: > "with Global => (in X, in Y, in out A, in out B, use Key, use Element)" > c) Use semicolons, such as: > "with Global => (in X, Y; in out A, B; use Key, Element)" > d) [current rule] Rely on reserved words as separators: > "with Global => (in X, Y, in out A, B, use Key, Element)" I've convinced myself that every option sucks. :-) (a) and (b) are too wordy, (c) is likely to cause confusion with the ";" that ends the enclosing declaration; and we've already discussed (d). Part of the problem I see here is that the names of globals aren't going to be A, B, and C in practice, they'll be much longer and these specifications are likely to extend over multiple lines. For instance in Trash_Finder (my spam filter), you'd have something like: with Global => (in TF_Params.Trash_Text_List, TF_Params.Spam_Text_List, TF_Params.Delete_Text_List, TF_Params.Virus_Text_List, in out TF_Filter.Filter_Queue, TF_Send.Send_Queue, use message_Type); When the lists have to be broken over multiple lines, one either would want to repeat the keyword or have a different separator (but I can't think of one that works). So I suspect that the best plan is to stick with (d) but do not give restrictions on how people organize these (meaning that (b) would be allowed) and let the world decide what works best for them. I know that's exactly opposite what Tucker wants, but I don't think it is likely that one-size-fits-all here. > 3) Should "null" be allowed "inside" parentheses? > a) Yes in all cases, but it is redundant in all cases > b) Yes, but only if there is no "in", "in out", or "out" > group already there, and it is redundant > c) It is *required* if there is no "in", "in out", or "out" > group already there, so it is *not* redundant > d) [current rule] Never. The only time it can appear is > by itself, in "Global => null". In the absence of > "in", "in out", or "out" then there is no global access > except that which might be performed by a generic > formal or a dispatching call. Effectively "Global => null" > is equivalent to "Global => ()" -- there is nothing magic > about the word "null" other than an absence of anything > else (including an absence of "Unspecified"). I can live with (d) if we also adopt the rule that "null" by itself means "(null, use null)" rather than the "(null, use all)" that it means today. Generally, I want it to be clear when an entity has no side-effects, not just no side-effects other than ones from generic formals. The reason this came up in the first place was my need in the containers to declare that some routines like Length have no side-effects regardless of what the formal parameters are. If Global => null has this effect, then it is obvious and I am satisfied enough, the other syntax is much less common and the meaning can be figured out as needed. **************************************************************** From: Claire Dross Sent: Monday, July 6, 2020 4:43 AM >> Because, AFAICS, Global => null >> is allowed (and is not the default IIRC). FWIW, it feels natural to >> me that Global => null really means Global => null, use => null. > > > If that was the case, I would be much less concerned about this topic. > But as it stands, "use all" is the default, so Global => null means > Global => (null, use all); This looks concerning indeed. I feel pretty strongly that Global => null should stand for Global => null, use null. It seems less confusing. **************************************************************** From: Tucker Taft Sent: Monday, July 6, 2020 6:15 AM The intent is that Global=>null obeys the same rules as pragma Pure, namely no use of global variables. But inside a generic, we certainly allow, and expect, the use of generic formal types, and other generic parameters. Otherwise, why would you make the routine generic? Trying to *avoid* use of generic formals is generally difficult, and so the default is the same as for pragma Pure, where there are no restrictions on generic formals (i.e. "use all"). Specifying "use null" is going to be very rare in my view. Almost any subprogram inside a generic will make use of at least one generic formal parameter. Note that a generic formal object of mode "in out" is a global variable, so that if it is read or updated, then "Global => null" would not be permitted in any case. So Global => null does imply no reading or writing of generic formal in-out objects, so as far as direct use of global variables, Global => null means what it says. It is only the unusual case where a generic formal type has some global side effects that affects the meaning (in the same way it does for pragma Pure), and that is not something you generally worry about when writing a generic unit, and not something you expect to have to worry about when you specify "Global => null" (or pragma Pure). **************************************************************** From: Claire Dross Sent: Tuesday, July 7, 2020 3:00 AM > The intent is that Global=>null obeys the same rules as pragma Pure, namely > no use of global variables. But inside a generic, we certainly allow, and > expect, the use of generic formal types, and other generic parameters. > Otherwise, why would you make the routine generic? Trying to *avoid* use of > generic formals is generally difficult, and so the default is the same as for > pragma Pure, where there are no restrictions on generic formals (i.e. "use > all"). Specifying "use null" is going to be very rare in my view. Almost > any subprogram inside a generic will make use of at least one generic formal > parameter. Is that true? For containers at least it is not the case I think. The "=" parameter is only used in a small number of subprograms (Find and = I think). > Note that a generic formal object of mode "in out" is a global variable, so > that if it is read or updated, then "Global => null" would not be permitted > in any case. So Global => null does imply no reading or writing of generic > formal in-out objects, so as far as direct use of global variables, Global > => null means what it says. It is only the unusual case where a generic > formal type has some global side effects that affects the meaning (in the > same way it does for pragma Pure), and that is not something you generally > worry about when writing a generic unit, and not something you expect to > have to worry about when you specify "Global => null" (or pragma Pure). This is True only if the parameter is not supposed in general to access globals. If you have a generic with a global Store procedure which is supposed to update external state, it does feel strange to me to have Global => null on uses of these packages. What do others think? **************************************************************** From: Arnaud Charlet Sent: Tuesday, July 7, 2020 3:10 AM Clearly without any real user needs and any actual users actually trying to use this feature, it's hard to guess. Also we're talking about a corner case of a corner case (use of "null" inside a "Global" aspect). That being said, I think that as a user I would find it more logical and expected that the Global => null also implies "use null" and I can always specify otherwise if I need something else. In other words, having Global => null means something else than "there are no uses of global variables here" is definitely counter intuitive to me. **************************************************************** From: Tucker Taft Sent: Tuesday, July 7, 2020 7:52 AM Breaking the equivalence between "with Pure" and "with Global => null" will cause a number of problems in my view. For declared-pure generic units, there are no limitations on what uses are made of generic formals (except for generic in out objects, which are not permitted in a declared-pure generic because any instance would necessarily be impure). More generally, if we agree that "use => all" is the default for a generic, this should not be affected by whether the subprogram makes *explicit* references to all, to some, or to no global variables. That is what "Global => null" means -- no explicit reference to a global variable. "Null" means many things in Ada, and in aspects it generally just represents the empty list. It shouldn't be given additional meanings, or generalized to mean that anything not specified is somehow other than simply its default value. **************************************************************** From: Randy Brukardt Sent: Tuesday, July 7, 2020 1:03 PM > Breaking the equivalence between "with Pure" and "with Global => null" will > cause a number of problems in my view. The Pure categorization is a failed feature in my view that is being replaced by Global (which is far more precise and flexible). I don't think it matters very much what the correspondence is. > For declared-pure generic units, there are no limitations on what uses are > made of generic formals (except for generic in out objects, which are not > permitted in a declared-pure generic because any instance would necessarily > be impure). Exactly. A declared-pure generic unit means almost nothing at all, only that you might be able to create a declared-pure instance if everything is exactly right. It has very little relationship to a declared-pure non-generic unit which makes all kinds of guarantees to the user. Trying to make them the same vis-a-vis Global is crazy, since they're not semantically the same. > More generally, if we agree that "use => all" is the default for a generic, > this should not be affected by whether the subprogram makes *explicit* > references to all, to some, or to no global variables. That is what > "Global => null" means -- no explicit reference to a global variable. I agree making this work right is going to be tricky, but I think it makes sense for "use all" to be the *default*, that doesn't necessarily mean that when you write a specification that you always get "use all". > "Null" means many things in Ada, and in aspects it generally just represents > the empty list. It shouldn't be given additional meanings, or generalized > to mean that anything not specified is somehow other than simply its default > value. I'm not sure where you are getting this from. Null generally represents "nothing at all" in Ada: no object (for access value), no body (for procedures), no statements (for statement lists), and so on. It makes sense for it to represent "no global access" for Global; that's certainly the meaning that I use informally and we've used occasionally in language wording. (Not sure if any of that wording remains today.) Using "null" as just a placeholder is unusual and not a usage I would want to use in Ada. When you want to specify that some routine accesses no globals, you mean *ever* and not worrying about generic formals. Note that carefully written code can use formal in parameters and formal scalar types without causing any access to globals - so it's certainly true that there will be many routines that can truly be Global => null. That's especially true for formal scalar types, which might not be Global => null themselves to support predicates -- but it's possible to write a generic body such that such predicates are never used and thus still are Global => null. **************************************************************** From: Claire Dross Sent: Tuesday, July 7, 2020 10:47 AM I am not sure I am understanding correctly. Before AI12-0380-1, No_Hidden_Indirect_Globals could be used to make sure that no globals were updated through access dereference. With the change, I am not sure that I understand how this is done anymore. For example, on the following example: package P is type Priv is private; procedure Hidden_Update (X : Priv); private type Int_Acc is access Integer; type Priv is record V : Int_Acc; end record; procedure Int_Acc_Update (X : Int_Acc); end P; package body P is procedure Hidden_Update (X : Priv) is begin Int_Acc_Update (X.V); end Hidden_Update; procedure Int_Acc_Update (X : Int_Acc) is begin X.all := 10; end Int_Acc_Update; end P; I understand that Int_Acc_Update is now allowed to update its in parameter X because it is visibly an access type (is it?). I understand that Hidden_Update would not be allowed to update directly X, because it is not visibly an access type. I don't see what prevents the call to In_Acc_Update in Hidden_Update though. Could somebody explain it to me? **************************************************************** From: Tucker Taft Sent: Tuesday, July 7, 2020 11:42 AM Here is the change in wording, from AI12-0380-1: ... any execution within such a context does neither of the following: * Update a variable that is reachable via a sequence of zero or more dereferences of access-to-object values from a formal parameter of mode IN (after any OVERRIDING -- see H.7), or from a global that is not within the applicable global variable set, or has mode IN{, unless the initial dereference is of a part of the formal parameter or global that is visibly of an access-to-variable type}; * Read a variable that is updatable via a sequence of zero or more dereferences of access-to-object values from a global that is not within the applicable global variable set{, unless the initial dereference is of a part of the formal parameter or global that is visibly of an access-to-object type}. --- The intent is that you cannot *update* a variable if it is reachable by a mode IN parameter or global, or a global that is not mentioned at all, *unless* it is reachable from a visible access-to-variable parameter or global. Similarly, you cannot *read* a variable if it is reachable from a global to which you have no access, unless it is reachable from a visible access-to-object parameter or global (to which you *do* have access). So in your example, Int_Acc_Update is clearly OK. However, Hidden_Update is violating the rule because it is passing a hidden component of an access-to-variable type to a routine that is allowed to update it, and Hidden_Update only has "in" access to its parameter X of type Priv. So the error is in Hidden_Update, at the point of its call of Int_Acc_Update. **************************************************************** From: Claire Dross Sent: Wednesday, July 8, 2020 2:08 AM Ok, excuse me if I am being dense, but could you tell me the exact rule which is violated at this point? Does it mean that it won't be possible to call any subprogram on a deep part of a private object unless the subprogram has a Global aspect using overriding? Thanks for taking the time to explain this, **************************************************************** From: Tucker Taft Sent: Wednesday, July 8, 2020 9:18 AM > Ok, excuse me if I am being dense, but could you tell me the exact > rule which is violated at this point? The caller has only "IN" mode access on its parameter, but it is passing a part of that parameter that is a visibly access-to-variable value to Int_Acc_Update, and has to presume that the access-to-variable value will be dereferenced and used to update the designated object. If the operation being called had an access-to-constant formal parameter, then that would be fine. > Does it mean that it won't be > possible to call any subprogram on a deep part of a private object > unless the subprogram has a Global aspect using overriding? I am not sure what you mean by "call a subprogram on a deep part of a private object". Can you give an example? The term "deep" is not an Ada term, and I am not familiar enough with the SPARK terminology to know exactly what you mean. The main issue is when you pass a visibly access-to-variable part of something that is of "IN" mode at the call site. **************************************************************** From: Claire Dross Sent: Wednesday, July 8, 2020 10:46 AM > The caller has only "IN" mode access on its parameter, but it is passing a > part of that parameter that is a visibly access-to-variable value to > Int_Acc_Update, and has to presume that the access-to-variable value will > be dereferenced and used to update the designated object. If the operation > being called had an access-to-constant formal parameter, then that would be > fine. Ok, I do understand the intent, the question was more, what part of the wording implies that? If it is only the fact that we are not allowed to update the IN parameter, I think this is not clear that a subprogram call with an in parameter of an access type is assumed to modify its parameter. Maybe there should be some non normative text or something like that? > > Does it mean that it won't be > > possible to call any subprogram on a deep part of a private object > > unless the subprogram has a Global aspect using overriding? > > I am not sure what you mean by "call a subprogram on a deep part of a > private object". Can you give an example? The term "deep" is not an Ada > term, and I am not familiar enough with the SPARK terminology to know > exactly what you mean. The main issue is when you pass a visibly > access-to-variable part of something that is of "IN" mode at the call site. Deep in SPARK means containing an access type. **************************************************************** From: Tucker Taft Sent: Wednesday, July 8, 2020 11:43 AM ... > Ok, I do understand the intent, the question was more, what part of > the wording implies that? If it is only the fact that we are not > allowed to update the IN parameter, I think this is not clear that a > subprogram call with an in parameter of an access type is assumed to > modify its parameter. Maybe there should be some non normative text or > something like that? I agree some additional wording could clarify the intent. ... > Deep in SPARK means containing an access type. One confusion I have with the SPARK terminology is that you tend to blur the distinction between an access value and the object it designates. You did that above when you said a "... call with an in parameter of an access type is assumed to modify its parameter....". It is presumed to modify the object *designated* by its parameter, if it is of an access-to-variable type. Clearly we need to be very careful with our terminology in the Ada RM. SPARK can clearly invent its own terminology if it is felt to be useful, but you need to be very careful when talking to an Ada "lawyer". ;-) I like the term "reachable" as a way to talk more generally about the objects you can reach by dereferencing access values. It would help me if you could use that term as well when talking about objects at one or more levels of indirection from the object in hand. **************************************************************** From: Claire Dross Sent: Thursday, July 9, 2020 2:29 AM > > Ok, I do understand the intent, the question was more, what part of > > the wording implies that? > > I agree some additional wording could clarify the intent. The important part here I think is that such a call would not be considered to modify its parameter without No_Hidden_Indirect_Globals (right?), so I am not sure the current wording is clear enough. ... > > Deep in SPARK means containing an access type. > > One confusion I have with the SPARK terminology is that you tend to blur > the distinction between an access value and the object it designates. Well, this is not surprising since we use ownership in SPARK... > SPARK can clearly invent its own terminology if it is felt to be > useful, but you need to be very careful when talking to an Ada > "lawyer". ;-) I will do my best. We are coming from different backgrounds and Ada terminology is probably as difficult for me as SPARK terminology is for you (possibly worse, because you did come up with a big part of the SPARK semantics for pointers). > I like the term "reachable" as a way to talk more generally about the > objects you can reach by dereferencing access values. It would help me > if you could use that term as well when talking about objects at one or > more levels of indirection from the object in hand. Ok, so let's try again. I say that any call with an actual parameter of mode in which is a part of a private data structure from which a visible access type is reachable will be considered to be an update (unless it is annotated with overriding). This is pretty restrictive, which is why I pointed it out. But I personally think it is better than what we had before. We could also use a distinction closer to what is done in SPARK, and say that the value designated by in parameters of a visible access type are considered to be modified by the call, but not values designated by access subcomponents of a composite type (unless overriding is used to modify their mode to in out). **************************************************************** From: Tucker Taft Sent: Thursday, July 9, 2020 9:49 AM >>> Ok, I do understand the intent, the question was more, what part of >>> the wording implies that? >> >> I agree some additional wording could clarify the intent. >> > > The important part here I think is that such a call would not be > considered to modify its parameter without No_Hidden_Indirect_Globals > (right?), so I am not sure the current wording is clear enough. No_Hidden_Indirect_Globals specifies that the Global aspect includes certain of the effects associated with dereferencing access values, whereas in the core, effects associated with dereferencing access values are ignored, per 6.1.2(29/5): "... In the absence of the No_Hidden_Indirect_Globals restriction (see H.4), this ignores objects reached via a dereference of an access value. ..." I will try to be sure the wording for No_Hidden_Indirect_Globals makes the rules as clear as possible. One area in particular needing more detail is calls between subprograms that are within a package body defining a private type. > ... > >> >> I like the term "reachable" as a way to talk more generally about the >> objects you can reach by dereferencing access values. It would help me >> if you could use that term as well when talking about objects at one or >> more levels of indirection from the object in hand. > > Ok, so let's try again. I say that any call with an actual parameter > of mode in which is a part of a private data structure from which a > visible access type is reachable will be considered to be an update > (unless it is annotated with overriding). It is not only that the access type is visible, it must also be associated with a visible component. > This is pretty restrictive, > which is why I pointed it out. But I personally think it is better > than what we had before. We could also use a distinction closer to > what is done in SPARK, and say that the value designated by in > parameters of a visible access type are considered to be modified by > the call, but not values designated by access subcomponents of a > composite type (unless overriding is used to modify their mode to in > out). I think the intent is already closer to that of SPARK, since it also depends on whether the subcomponent is visible to the caller. I will try to clarify further in the wording. **************************************************************** From: Claire Dross Sent: Friday, July 10, 2020 2:44 AM > > This is pretty restrictive, > > which is why I pointed it out. But I personally think it is better > > than what we had before. We could also use a distinction closer to > > what is done in SPARK, and say that the value designated by in > > parameters of a visible access type are considered to be modified by > > the call, but not values designated by access subcomponents of a > > composite type (unless overriding is used to modify their mode to in > > out). > > I think the intent is already closer to that of SPARK, since it also > depends on whether the subcomponent is visible to the caller. I will > try to clarify further in the wording. I am not convinced. SPARK is not very concerned with visibility as a general rule (unless we reach a SPARK_Mode => Off annotation). The difference in approach really depends on what we think is the most common case. If an in parameter X is of a visible access type, it seems likely that the subprogram will modify it (at least if it is a procedure, it does seem less common with functions), so we do agree here. If X has a partially private type, and its subcomponents of type access are not visible, it seems bad practice to use mode in if we do modify values reachable from the parameter, so here again we agree. The question is for composite types with subcomponents which are visibly access types. What is the most common in this case? Whatever choice we make, users will have to use overridden if their use does not match our choice, so it is really a question of what seems the most likely to occur in practice. Btw, maybe it would be good to separate the AI in two parts? So that we can discuss and vote independently on Private_Globals and other changes? **************************************************************** From: Tucker Taft Sent: Friday, July 10, 2020 10:24 AM ... > I am not convinced. SPARK is not very concerned with visibility as a > general rule (unless we reach a SPARK_Mode => Off annotation). The > difference in approach really depends on what we think is the most > common case. If an in parameter X is of a visible access type, it > seems likely that the subprogram will modify it (at least if it is a > procedure, it does seem less common with functions), so we do agree > here. If X has a partially private type, and its subcomponents of type > access are not visible, it seems bad practice to use mode in if we do > modify values reachable from the parameter, so here again we agree. > The question is for composite types with subcomponents which are > visibly access types. What is the most common in this case? Whatever > choice we make, users will have to use overridden if their use does > not match our choice, so it is really a question of what seems the > most likely to occur in practice. Agreed. We have some specific cases which are influencing what we propose to do in this case, in particular stable views of a container, and reference types. Reference types can be returned from a function, and then used to update the object designated by its access discriminant. So here we definitely have a constant composite object with a visible access-to-variable discriminant, and that is expected to be used to update the designated object. > Btw, maybe it would be good to separate the AI in two parts? So that > we can discuss and vote independently on Private_Globals and other > changes? Yes, I will move Private_Global into a separate AI, as there seems less consensus there. **************************************************************** From: Claire Dross Sent: Friday, July 10, 2020 10:48 AM > Agreed. We have some specific cases which are influencing what we propose > to do in this case, in particular stable views of a container, and reference > types. Reference types can be returned from a function, and then used to > update the object designated by its access discriminant. So here we > definitely have a constant composite object with a visible > access-to-variable discriminant, and that is expected to be used to update > the designated object. Indeed. And how would a usage of this reference type be handled with the current rules? Would the modification be detected? Could you give an example of how it would work? **************************************************************** From: Tucker Taft Sent: Sunday, July 12, 2020 6:47 AM That is certainly the intent. I am working on the AI to be sure that the intent is properly communicated. I'll try to be sure there is an example in the updated AI to illustrate this. **************************************************************** From: Brad Moore Sent: Thursday, July 30, 2020 12:34 PM I agreed to send my set of typographical comments for AI12-380-1, since I was having audio problems during today's teleconference, They are; Problem: "3) There seems {to be} no rule" "4) In H.7, there seems {to be} no single" H.7.1 Ramification "controlling the call", weird characters, and also the ramification ends with a square bracket, but I don't see an opening square bracket. **************************************************************** From: Randy Brukardt Sent: Friday, July 31, 2020 11:19 PM > H.7.1 > Ramification > "controlling the call", weird characters, and also the ramification > ends with a square bracket, but I don't see an opening square bracket. The weird characters are the Windows version of rounded quotes. The square bracket is the end of a number of deleted paragraphs - the opening square bracket is 3 paragraphs above. Digression: There's two occurrences of "controlling the call" with weird characters surrounding it, and the second (the first I found) doesn't have a ending square bracket. It took me a while to realize you were talking about the *first* occurrence. The square brackets around entire paragraphs and even groups of paragraphs have has confused me every time I've read this AI (it looks like some of the text is here twice). Usually we don't show entire deleted paragraphs, especially when they are just getting moved anyway. So I think the best thing is to get rid of all of those entire deleted paragraphs and just leave the English description ("Delete H.7(12/5). [Moved to H.7.1]"). That does possibly make it not completely clear what paragraphs are involved, but there are other places (including in this AI) where text is removed without trying to show the details of that text it is. **************************************************************** From: Tucker Taft Sent: Saturday, August 1, 2020 11:23 AM That is fine with me. I remember various rules that seem to contradict each other about what we want to do when we make wholesale deletions of replacements. I suppose it depends on whether you need to see the old wording for context. **************************************************************** From: Randy Brukardt Sent: Saturday, August 1, 2020 9:57 PM Right, we generally show deleted paragraphs only when there is an important reason for referencing it. The "rules" here are flexible; the main issue is to keep the "instructions" (that is, the "Delete 13.1.1(17/5)" text) consistent. For instance, in this AI there is a deletion of 13.1.1(17/5); I left that text as you have a note explaining why this text was being deleted and that note isn't understandable without seeing the rule in question. **************************************************************** Editor's note, August 21st. It was noticed that the definition of the default behavior when no Dispatching aspect is given didn't include Nonblocking. Tucker proposed the following changes: In the absence of any dispatching_operation_specifiers, {Nonblocking and global aspects checks are performed at the point of a dispatching call within the operation using the Nonblocking and} [all dispatching calls within the operation are presumed to have the effects determined by the set of] Global'Class aspects that apply to the named dispatching operation. ****************************************************************