!standard 6.1.2(0) 19-04-02 AI12-0079-1/13 !standard 13.1.1(4/3) !standard 13.1.1(11/3) !standard 13.14(3/5) !class Amendment 13-06-28 !status Amendment 1-2012 18-12-10 !status ARG Approved 11-0-1 18-12-10 !status work item 13-06-28 !status received 13-06-14 !priority High !difficulty Hard !subject Global-in and global-out annotations !summary Annotations are provided to describe the use of global objects by subprograms. !problem Ada 2012 added many kinds of assertions to Ada in order to increase the ability of a programmer to specify contracts for types and subprograms. These contracts are defined to be checked at runtime, but are intended to be potentially checked (at least in part) statically. However, without knowledge of side effects of functions used in the aspects, a tool has to assume the worst about any user-defined functions. For example, that the result of a function can change even when called with the same operands. Other assumptions could cause incorrect programs to be accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution. Both of these results are unacceptable for a feature intended to improve the correctness of programs. The worst-case assumptions pretty much prevent any analysis unless the bodies of any user-defined functions used in the aspects are available. This is bad, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body requires creating pseudo body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again); but the language does not allow these to be "real" body dependencies (any recompilation needed has to occur automatically). Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side effects is needed in the specification of subprograms in order to accomplish that goal. !proposal [Note: the following is mostly a direct quote from the paper "Safe Parallel Programming in Ada with Language Extensions" prepared for HILT 2014.] To encourage convergence with SPARK we are starting from the SPARK Global aspect. However, for Ada, it is necessary to extend this aspect to cover a broader spectrum of usage, since Ada includes access types and other features not allowed in SPARK. The Global aspect in SPARK 2014 is applied to subprogram specifications, and is of the following form: with Global => (Input => ..., In_Out => ..., Output => ...) where "..." is either a single name, or a parenthesized list of names, and Input, In_Out, and Output identify the variables global to the subprogram that are accessed by this subprogram, in read-only, read-write, or write-only mode, respectively. If there are no variables global to the subprogram accessed with a particular parameter mode, then that mode is omitted from the specification. If there are only global inputs, and no outputs or in-outs, then this syntax can be further simplified to: with Global => ... where again "..." is a single name, or a parenthesized list of names. Finally, if there are no global inputs, in-outs, nor outputs, then: with Global => null is used. We need to refine the notion of SPARK's Global aspect, because SPARK does not support access types, and because SPARK relies on an elaborate mechanism for handling the abstract "state" of packages. The refinements we are proposing are the following: 1. Allow the name of an access type A (including "access T") to stand-in for the set of objects described roughly by: [for all X convertible to A => X.all] 2. Allow the name of a package P to stand-in for the set of objects described roughly by: [for all variables X declared in P => X] Also allow this to be qualified with "private" to restrict the set to those objects declared in the private part, the body, or private descendants. 3. Allow the word *synchronized* to be used to represent the set of global variables that are tasks, protected objects, or atomic objects. 4. Allow the word *all* to be used to represent the set of all variables global to the subprogram, including variables designated by access values of types global to the subprogram. 5. Switch to using the normal Ada parameter modes, in, in out, and out rather than Input, In_Out, and Output. Note that references to global constants do not appear in Global annotations. In the absence of a global aspect, a subprogram in a pure package is presumed to reference no global variables (Global => null), while a subprogram in an impure package is presumed to read and write an unspecified set of global variables, including non-synchronized ones (Global => in out all). We also allow a Global aspect on a package, which can be used to establish a default for all subprograms declared within the package specification. The default can be overridden for any particular subprogram by specifying the Global aspect for that subprogram. For dispatching operations, a Global'Class aspect may be specified, which represents an upper bound on the set of up-level variables that any particular overriding of that operation may reference in each of the specified modes. In the absence of a Global'Class aspect, the default for the Global aspect is used for the Global'Class aspect. !wording Add the following section: 6.1.2 The Global and Global'Class Aspects For a program unit, formal package, formal subprogram, formal object of an anonymous access-to-subprogram type, and for 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): Global The syntax for the aspect_definition used to define a Global aspect is as follows: global_aspect_definition ::= primitive_global_aspect_definition | /global_/attribute_reference | global_aspect_definition & /global_/attribute_reference primitive_global_aspect_definition ::= NULL | global_mode global_name | global_mode global_designator | (global_mode global_set{, global_mode global_set}) global_mode ::= [ global_mode_qualifier ] basic_global_mode global_mode_qualifier ::= SYNCHRONIZED | /implementation-defined_/identifier basic_global_mode ::= IN | IN OUT | OUT global_set ::= global_name {, global_name} | global_designator global_designator ::= ALL | NULL global_name ::= /object_/name | /package_/name [ PRIVATE ] | /access_/subtype_mark | ACCESS subtype_mark A /global_/attribute_reference is an attribute_reference with attribute designator "Global". The Global aspect identifies the set of variables (which, for the purposes of this clause includes all task objects) global to a callable entity that are potentially read or updated as part of the execution of a call on the entity. If not specified, 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. For a dispatching subprogram or a tagged type, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1): Global'Class The syntax for the aspect_definition used to define a Global'Class aspect is the same as that defined above for global_aspect_definition. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the nearest enclosing program unit. Name Resolution Rules A global_name that does not have the reserved word ACCESS shall resolve to statically denote an object, a package (including a limited view of a package), or an access-to-variable subtype. The subtype_mark of a global_name that has the reserved word ACCESS shall resolve to denote a subtype (possibly an incomplete type). Static Semantics A global_aspect_definition defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side effect of some operation. The Global'Class aspect associated with a tagged type T (or one of its dispatching operations) represents a restriction on the Global aspect on any descendant of type T (or its corresponding operation). 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 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) identifies the global variables that might be referenced when calling via the object (or any object of that type). The Global aspect for any other elementary type is null. The following is defined in terms of operations; the rules apply to all of the above kinds of entities. The sets of global variables associated with a Global aspect can be defined explicitly with a primitive_global_aspect_definition or can be defined by combining the sets specified for other entities by referring to their Global attribute. The global variables associated with any mode can be read as a side effect of an operation. The IN OUT and OUT global_modes together identify the set of global variables that can be updated as a side effect of an operation. The global_mode_qualifier SYNCHRONIZED reduces the set to those objects that are of one of the following sort of types: * a protected, task, or synchronized tagged type; * an atomic type; * a descendant of the language-defined types Suspension_Object or Synchronous_Barrier; * a record type all of whose components are *sychronized* in this sense; * an array type whose component type is *sychronized* in this sense. An implementation-defined global_mode_qualifier may be specified, which reduces the set according to an implementation-defined rule. The overall set of objects associated with each global_mode includes all objects identified for the mode in the primitive_global_aspect_definition (subject to the global_mode_qualifier), if any, plus all objects associated with the given mode for the entities identified by the prefixes of the /global_/attribute_reference's, if any. A global_set identifies a *global variable set* as follows: * "null" identifies the empty set of global variables; * "all" identifies the set of all global variables; * "global_name{, global_name}" identifies the union of the sets of variables identified by the global_name's in the list, for the following forms of global_name: * /object_/name identifies the specified global variable (or nonpreelaborable constant) * /package_/name identifies the set of all variables declared within the declarative region of the package having the same accessibility level as the package, but not including those within the declarative region of a public child of the package; if the reserved word PRIVATE follows the /package_/name, the set is reduced to those variables declared in the private part or body of the package or within a private descendant of the package; * /access_/subtype_mark identifies the set of (aliased) variables that can be designated by values of the given access-to-variable type; * ACCESS subtype_mark identifies the set of (aliased) objects that can be designated by values of an access-to-variable type with a designated subtype statically matching the given subtype_mark. Legality Rules Within a primitive_global_aspect_definition, a given global_mode shall be specified at most once without a global_mode_qualifier, and at most once with any given global_mode_qualifier. Similarly, within a primitive_global_aspect_definition, a given entity shall be named at most once by a global_name. If an entity has a Global aspect other than IN OUT ALL, then the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the IN, IN OUT, or OUT modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the IN OUT or OUT global_modes. This includes any calls occurring during the execution of the operation, presuming those calls read and update all global variables permitted by their Global aspect (or Global'Class aspect, if a dispatching call). If a variable global to the entity is read that is within the global variable set associated with the OUT global_mode, it shall be updated somewhere within the callable entity (or an entity it calls). If an implementation-defined global_mode_qualifier applies to a given set of variables, an implementation-defined rule determines what sort of references to them are permitted. For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the IN OUT mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of T. A corresponding rule applies to the Global aspect of a tagged type T relative to the Global'Class aspect of any ancestor of T. For a prefix S that statically denotes a subprogram (including a formal subprogram), formal object of an anonymous access-to-subprogram type, or a type (including a formal type): S'Global Identifies the global variable set for each of the three global_modes, for the given subprogram, object, or type; a reference to this attribute may only appear within a global_aspect_definition. Implementation Permissions For a call on a subprogram that has a Global aspect that indicates that there are no references to global variables, the implementation may omit the call: * if the results are not needed after the call; or * simply reuse the results produced by an earlier call on the same subprogram, provided that none of the parameters nor any object accessible via access values from the parameters have any part that is of a type whose full type is an immutably limited type, and the addresses and values of all by-reference actual parameters, the values of all by-copy-in actual parameters, and the values of all objects accessible via access values from the parameters, are the same as they were at the earlier call. Redundant[This permission applies even if the subprogram produces other side effects when called.] AARM Discussion: This permission doesn't really allow a compiler to do anything that it couldn't do anyway (as any optimization that gives the required semantics for program executions that aren't erroneous is always allowed), but we considered it important to make Ada programmers aware that such optimizations are possible. Specifically, an implementation can trust the information given in a Global aspect, as any subprogram that violates it is either illegal or would result in erroneous execution. Specifically, the Global contract can be violated by erroneous execution resulting from dereferencing a dangling reference (see 13.11.2), misuse of unmanaged owned access values (see 3.10.3), by giving an incorrect contract on an interfaced subprogram (see B.1), by specifying the address of a global object for a local object (see 13.3), or by using Unchecked_Conversion (see 13.9) or Address_to_Access_Conversions (see 13.7.2) to create local accesses to global object. Since optimizations like these don't require a special permission, implementations can also use similar optimizations that go beyond the permission above. For instance, if there are two calls with the same parameters on a subprogram whose Global aspect only indicates reading of a global object G, then the second call be omitted and reuse the result of the first call if the compiler can prove (with the help of the Global aspect of any subprograms called) that G is not written to between the calls. End AARM Discussion. Modify 13.1.1(4/3) aspect_definition ::= name | expression | identifier{ | global_aspect_definition} Modify 13.1.1(11/3): The usage names in an aspect_definition [Redundant: are not resolved at the point of the associated declaration, but rather] are resolved at the end of the immediately enclosing declaration list{, or in the case of the declaration of a library unit, at the end of the visible part of the entity}. Modify 13.14(3/5): The end of a declarative_part, protected_body, or a declaration of a library package or generic library package, causes freezing of each entity and profile declared within it{, as well as the entity itself in the case of the declaration of a library unit}. [Author's TBD: annotating the language-defined packages] !discussion Global annotations are critical to being able to perform any sort of modular static analysis. The intent is that all of the global in, in-out, and out annotations proposed can be statically checked. We have allowed for an implementation-defined global_mode_qualifier, which would allow "proof in" for SPARK, as well as something like "synthesized in out all" to indicate that the implementation determines the global variables that are referenced. We have allowed reading of "out" mode globals, so long as there is at least one update of the global variable as well. Note that it is possible to lie about the use of globals of subprograms and other entities that are imported. This is of course impossible to check, but thankfully is covered by B.1(38.1/2). Incorrect annotations on imported subprograms could cause a program's execution to be erroneous. SPARK does not currently support identifying particular components of a global variable in the Global aspect, but for Ada we plan to allow that. This is somewhat inconsistent with what can be specified for parameters, since there is no easy way to identify which components of an in-out parameter are actually updated. It is possible to specify in a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that can be a maintenance issue as the names and numbers of subcomponents changes, and only works for types that have an appropriate "=" operator. It might be useful to have another aspect that indicated which components of an in-out parameter might be modified, with all others presumably being preserved (e.g. Modified => (X.A, X.B)). Note that SPARK has a "Refined_Global" aspect which can be specified on the body of a subprogram, to specify a more restricted set of globals for those callers that have visibility on the body. This could be added at a later point if it was felt to be important. We have adjusted the rules for name resolution within an aspect clause, to cover the case of an aspect that applies to a library unit. For this case, we say that the name resolution happens at the end of the visible part of the entity. We have also made a minor adjustment to 13.14 (freezing rules) to define where a library unit itself is frozen -- namely at the end of the declaration of the library unit. This is important because aspects of a library unit might mention items declared within the library unit declaration. !example package Random is procedure Set_Seed(Seed : Float); with Global => out Random; -- Initialize state of Random package function Next_Random return Float with Global => in out Random; -- Update state of Random package end Random; The Random package presumably has hidden state, which is represented by the name of the package itself in a global_aspect_definition. generic type T is private; with function Hash(X : T) return Hash_Code; package Sets is type Set(Capacity : Positive) is private with Global => T'Global; procedure Insert(S : in out Set; X : T) with Global => in out Hash'Global & T'Global; ... end Sets; Operations within the Sets package reference global variables only indirectly, as a result of using the generic formal parameters T and Hash, and as a result of dereferencing access objects within the representation of a Set. The default initialization, adjustment, and finalization of a Set indirectly uses the corresponding operations of T. !corrigendum 6.1.2(0) @dinsc For a program unit, formal package, formal subprogram, formal object of an anonymous access-to-subprogram type, and for a named access-to-subprogram type or composite type (including a formal type), the following language-defined aspect may be specified with an @fa (see 13.1.1): @xhang<@xtermThe syntax for the @fa used to define a Global aspect is as follows:> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa@hr @ @ |@ @i@fa@hr @ @ |@ @fa & @i@fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @b@hr @ @ |@ @fa @fa@hr @ @ |@ @fa @fa@hr @ @ |@ (@fa @fa{, @fa @fa})> @xindent<@fa@fa<@ ::=@ >[ @fa ] @fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @b@hr @ @ |@ @i@fa> @xindent<@fa@fa<@ ::=@ >@b | @b | @b> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa {, @fa}@hr @ @ |@ @fa> @xindent<@fa@fa<@ ::=@ >@b | @b> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @i@fa@hr @ @ |@ @i@fa [ @b ]@hr @ @ |@ @i@fa@hr @ @ |@ @b @fa> @xindent@fa is an @fa whose @fa is Global.> @xindent @b> for a nongeneric library unit that is declared Pure, and to @fc @b> otherwise.> For a dispatching subprogram or a tagged type, the following language-defined aspect may be specified with an @fa (see 13.1.1): @xhang<@xtermThe syntax for the @fa used to define a Global'Class aspect is the same as that defined above for @fa. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the nearest enclosing program unit.> @s8<@i> A @fa that does not have the reserved word @b shall resolve to statically denote an object, a package (including a limited view of a package), or an access-to-variable subtype. The @fa of a @fa that has the reserved word @b shall resolve to denote a subtype (possibly an incomplete type). @s8<@i> A @fa defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side effect of some operation. The Global'Class aspect associated with a tagged type @i (or one of its dispatching operations) represents a restriction on the Global aspect on any descendant of type @i (or its corresponding operation). 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 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) identifies the global variables that might be referenced when calling via the object (or any object of that type). The Global aspect for any other elementary type is null. The following is defined in terms of operations; the rules apply to all of the above kinds of entities. The sets of global variables associated with a Global aspect can be defined explicitly with a @fa or can be defined by combining the sets specified for other entities by referring to their Global attribute. The global variables associated with any mode can be read as a side effect of an operation. The @b and @b @fas together identify the set of global variables that can be updated as a side effect of an operation. The @fa @b reduces the set to those objects that are of one of the following sort of types: @xbullet @xbullet @xbullet @xbullet in this sense;> @xbullet in this sense.> An implementation-defined @fa may be specified, which reduces the set according to an implementation-defined rule. The overall set of objects associated with each @fa includes all objects identified for the mode in the @fa (subject to the @fa), if any, plus all objects associated with the given mode for the entities identified by the @faes of the @i@fas, if any. A @fa identifies a @i as follows: @xbullet<@b identifies the empty set of global variables;> @xbullet<@b identifies the set of all global variables;> @xbullet<@fa{, @fa} identifies the union of the sets of variables identified by the @fas in the list, for the following forms of @fa:> @xinbull<@i@fa identifies the specified global variable (or nonpreelaborable constant);> @xinbull<@i@fa identifies the set of all variables declared within the declarative region of the package having the same accessibility level as the package, but not including those within the declarative region of a public child of the package; if the reserved word @b follows the @i@fa, the set is reduced to those variables declared in the private part or body of the package or within a private descendant of the package;> @xinbull<@i@fa identifies the set of (aliased) variables that can be designated by values of the given access-to-variable type;> @xinbull<@b @fa identifies the set of (aliased) objects that can be designated by values of an access-to-variable type with a designated subtype statically matching the given @fa.> @s8<@i> Within a @fa, a given @fa shall be specified at most once without a @fa, and at most once with any given @fa. Similarly, within a @fa, a given entity shall be named at most once by a @fa. If an entity has a Global aspect other than @b, then the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the @b, @b, or @b modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the @b or @b @fas. This includes any calls occurring during the execution of the operation, presuming those calls read and update all global variables permitted by their Global aspect (or Global'Class aspect, if a dispatching call). If a variable global to the entity is read that is within the global variable set associated with the @b @fa, it shall be updated somewhere within the callable entity (or an entity it calls). If an implementation-defined @fa applies to a given set of variables, an implementation-defined rule determines what sort of references to them are permitted. For a subprogram that is a dispatching operation of a tagged type @i, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the @b mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of @i. A corresponding rule applies to the Global aspect of a tagged type @i relative to the Global'Class aspect of any ancestor of @i. For a @fa S that statically denotes a subprogram (including a formal subprogram), formal object of an anonymous access-to-subprogram type, or a type (including a formal type), the following attribute is defined: @xhang<@xtermIdentifies the global variable set for each of the three @fas, for the given subprogram, object, or type; a reference to this attribute may only appear within a @fa.> @s8<@i> For a call on a subprogram that has a Global aspect that indicates that there are no references to global variables, the implementation may omit the call: @xbullet @xbullet This permission applies even if the subprogram produces other side effects when called. !corrigendum 13.1.1(4/3) @drepl @xindent<@fa@fa<@ ::=@ @fa | @fa | @fa> @dby @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa@ |@ @fa@ |@ @fa@ |@ @fa@ |@ @fa> !corrigendum 13.1.1(11/3) @drepl The usage names in an @fa are not resolved at the point of the associated declaration, but rather are resolved at the end of the immediately enclosing declaration list. @dby The usage names in an @fa are not resolved at the point of the associated declaration, but rather are resolved at the end of the immediately enclosing declaration list, or in the case of the declaration of a library unit, at the end of the visible part of the entity. !corrigendum 13.14(3/5) @drepl The end of a @fa, @fa, or a declaration of a library package or generic library package, causes @i of each entity and profile declared within it, except for incomplete types. A @fa, @fa, or @fa causes freezing of each entity and profile declared before it within the same @fa that is not an incomplete type; it only causes freezing of an incomplete type if the body is within the immediate scope of the incomplete type. @dby The end of a @fa, @fa, or a declaration of a library package or generic library package, causes @i of each entity and profile declared within it, as well as the entity itself in the case of the declaration of a library unit. A noninstance @fa, @fa, or @fa causes freezing of each entity and profile declared before it within the same @fa. !ASIS ** TBD. !ACATS test ACATS tests should be created to test that the new annotations are correctly enforced. !appendix From: Tucker Taft Sent: Monday, October 6, 2014 10:27 AM The recent paper submitted to HILT by Steve Michell, Miguel Pinho, Brad Moore, and myself, suggests more details about a Global annotation for Ada, based on the SPARK 2014 work. This relates to AI12-0079. Below is the section on this from the final paper. -Tuck ----- One of the strengths of Ada is that it was carefully designed to allow the compiler to detect many problems at compile time, rather than at run time. Programming for parallel execution in particular is an activity that requires care to prevent data races and deadlocks. It is desirable that any new capabilities added to the language to support parallelism also allow the compiler to detect as many such problems as possible, as an aid to the programmer in arriving at a reliable solution without sacrificing performance benefits. A common source of erroneousness in languages that support concurrency and parallelism are data races, which occur when one thread of execution attempts to read or write a variable while another thread of execution is updating that same variable. Such a variable is global in the sense that it is globally accessible from multiple threads of execution. In the current Ada standard, threads of execution are tasks. In this proposal, tasklets are another form of execution threads. Eliminating concurrency and parallelism problems associated with non-protected global variables is an important step towards improving the safety of the language. To that end, we propose the addition of a Global aspect to the language. The main goal in the design of this aspect is to identify which global variables and access-value dereferences a subprogram might read or update. The inspiration for this aspect comes from the SPARK language [24], which has always had global annotations. Earlier versions of SPARK augmented a subset of Ada with annotations added as specially formatted comments, which were used for static analysis by the proof system. With the addition of aspects to Ada in Ada 2012, SPARK 2014 has changed its annotations to use aspects, including the “Global” annotation. To encourage convergence with SPARK we are starting from the SPARK Global aspect. However, for Ada, it is necessary to extend this idea to cover a broader spectrum of usage, since Ada is a more expressive programming environment than SPARK. The Global aspect in SPARK 2014 is applied to subprogram specifications, and is of the following form; with Global =>(Input => ..., In_Out => ..., Output => ...) where “…” is either a single name, or a parenthesized list of names, and Input, In_Out, and Output identify the global variables of the program that are accessed by this subprogram, in read-only, read-write, or write-only mode, respectively. If there are no global variables with a particular parameter mode, then that mode is omitted from the specification. If there are only global inputs, and no outputs or in-outs, then this syntax can be further simplified to: with Global => ... where again "..." is a single name, or a parenthesized list of names. Finally, if there are no global inputs, in-outs, nor outputs, then: with Global => null is used. We needed to refine the notion of SPARK's Global aspect, because SPARK does not support access types, and because SPARK relies on an elaborate mechanism for handling the abstract “state” of packages. The refinements we are proposing are the following: 1. Allow the name of an access type A (including "access T") to stand-in for the set of objects described by: (for all X convertible to A => X.all) 2. Allow the name of a package P to stand-in for the set of objects described by: (for all variables X declared in P => X) 3. Allow the word synchronized to be used to represent the set of global variables that are tasks, protected objects, or atomic objects. Note that references to global constants do not appear in Global annotations. In the absence of a global aspect, the subprogram is presumed to read and write an unspecified set of global variables, including non-synchronized ones. ... If one wants to know whether a subprogram has side-effects, it is important to know about all data that might be read or written. Access types introduce difficulties in determining such side-effects, since the side-effects might result after a dereference of a series of pointers to reach an object to be updated. Our proposal addresses this by allowing the programmer to specify the name of an access type in a Global aspect. This would be essentially equivalent to writing something like; Global => (In_Out => *.all) except we can be more specific about the type of the access values being dereferenced. For example, consider a visible access type declared as; type Acc is access T; and a subprogram that has a value of type Acc in local variable Local, which it then uses to read and update an object via Local.all. It would not be very useful to write: Global => (In_Out => Local.all) since "Local" means nothing to the caller. But it could write: Global => (In_Out => Acc) to indicate that the caller should be aware that a call on this subprogram is updating some object by dereferencing an access value of type Acc. Another problematic case involves specifying in a Global aspect a variable that is declared inside a package body. Directly naming such a variable would not have meaning to the caller of the subprogram, and would violate encapsulation. Similarly, suppose an access type is declared inside the body or private part of package P. In both these cases, we treat the private updatable objects as a part of the overall state of package P. We then simply indicate that the subprogram is updating some or all of the state of package P: Global => (In_Out => P) Now suppose that the objects being updated are all protected or atomic objects. Then the caller doesn't really need to worry about which objects are being read or updated. It is always safe to call the subprogram concurrently. It has some side effects, so you cannot assume it is a "pure" subprogram. In this case, we could describe the effects as: Global => synchronized if it only reads synchronized objects, or: Global => (In_Out => synchronized) if it might update synchronized objects as well. One might be concerned that the number of globals in a subprogram higher in the call structure of a larger program might be unmanageable to specify in a Global aspect. To address this concern we propose a shorthand for the Global aspect: Global => (In_Out => all) where “all” represents all global variables. If the number of non-synchronized globals does get large, then it is likely that the subprogram cannot be used in a parallel context anyway, hence using all is generally adequate. By default, the global aspect is (In_Out => all) for normal subprograms, and null for subprograms in a declared-pure package. **************************************************************** From: Bob Duff Sent: Tuesday, October 14, 2014 5:20 PM > Here is an AI on the Global aspect, based on SPARK and on the HILT > 2014 paper on parallel language extensions for Ada. Looks good. You make it look so simple. So why didn't we already do this? I guess the Devil's in the "!wording". See below for editorial comments and some questions. > !summary > > Annotations are provided to describe the use of global objects by subprograms. ^^^^^^^ variables > !problem > > Ada 2012 added many kinds of assertions to Ada in order to increase > the ability of a programmer to specify contracts for types and > subprograms. These contracts are defined to be checked at runtime, but > are intended to be potentially checked (at least in part) statically. > > However, without knowledge of side-effects of functions used in the > aspects, a tool has to assume the worst about any user-defined > functions. For example, that ^^^^^^^^^ subprograms > the result of a function can change even when called with the same > operands. Other assumptions could cause incorrect programs to be > accepted as correct, and if the assumptions were used to omit "proved" > aspects, to erroneous execution. ^^^^ ^^^^^^^ I think you mean "suppress...checks". If not, please explain. > Both of these results are unacceptable for a feature intended to > improve the correctness of programs. > > The worst-case assumptions pretty much prevent any analysis unless the > bodies of any user-defined functions used in the aspects are > available. This is bad, as it prevents analysis of programs as they > are constructed. If the body is not available, no analysis is > possible. Moreover, analysis depending on a body require creating > pseudo body dependencies (if the body is changed, any analysis > depending on the properties of that body would have to be performed > again); but the language does not allow these to be "real" body > dependencies (any recompilation needed has to occur automatically). I agree, having to look at bodies is "bad", but those don't seem like the main reasons why. To me, the main reason is the usual software engineering one: you want well-defined interfaces, and you want to depend ONLY on those interfaces (i.e. specs). If you prove something about package body X, you want that proof to be valid in the presence of arbitrary changes to bodies called by X. > We need to refine the notion of SPARK's Global aspect, because SPARK > does not support access types, and because SPARK relies on an > elaborate mechanism for handling the abstract “state” of packages. What's your opinion about that elaborate mechanism? I've never understood why it's needed, but I'm told by SPARK folks that it's super-useful. I'd like to understand why, and whether we ought to add such stuff to Ada. >...The > refinements we are proposing are the following: > > 1. Allow the name of an access type A (including "access T") to > stand-in for the set of objects described roughly by: "stand in" (no dash) > (for all X convertible to A => X.all) That's the same thing as the collection of A, right? > 2. Allow the name of a package P to stand-in for the set of objects > described roughly by: > > (for all variables X declared in P => X) Does that include children of P? > !wording > > ** TBD. ;-) ;-) > !discussion > > Global annotations are critical to being able to perform any sort of > modular static analysis. Yeah, that's what I meant by my "software engineering" comment above. > All of the global in, in-out, and out annotations proposed can be > statically checked. > > Note that it is possible to lie about the use of globals of > subprograms and other entities that are imported. This is of course > impossible to check, but thankfully is covered by B.1(38.1/2). > Incorrect annotations on imported subprograms could cause a program to be > erroneous. > > SPARK does not currently support identifying particular components of > a global variable in the Global aspect, but for Ada we plan to allow that. > This is somewhat inconsistent with what can be specified for > parameters, since there is no easy way to identify which components of > an in-out parameter are actually updated. It is possible to specify in > a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that > can be a maintenance issue as the names and numbers of subcomponents > changes, and only works for types that have an appropriate "=" operator. > It might be useful to have another aspect that indicated which > components of an in-out parameter might be updated, with all others > presumably being preserved (e.g. Updated => (X.A, X.B)). Yes, I'm a fan of limited types, and I'd like to be able to say things like that. **************************************************************** From: Tucker Taft Sent: Tuesday, October 14, 2014 9:37 PM ... >> However, without knowledge of side-effects of functions used in the >> aspects, a tool has to assume the worst about any user-defined >> functions. For example, that > ^^^^^^^^^ > subprograms > >> the result of a function can change even when called with the same >> operands. Other assumptions could cause incorrect programs to be >> accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution. > ^^^^ ^^^^^^^ > > I think you mean "suppress...checks". If not, please explain. I didn't actually write the "problem" statement. I think it might be Randy's original wording. >> Both of these results are unacceptable for a feature intended to >> improve the correctness of programs. >> >> The worst-case assumptions pretty much prevent any analysis unless >> the bodies of any user-defined functions used in the aspects are >> available. This is bad, as it prevents analysis of programs as they >> are constructed. If the body is not available, no analysis is >> possible. Moreover, analysis depending on a body require creating >> pseudo body dependencies (if the body is changed, any analysis >> depending on the properties of that body would have to be performed >> again); but the language does not allow these to be "real" body >> dependencies (any recompilation needed has to occur automatically). > > I agree, having to look at bodies is "bad", but those don't seem like > the main reasons why. To me, the main reason is the usual software > engineering one: you want well-defined interfaces, and you want to > depend ONLY on those interfaces (i.e. specs). If you prove something > about package body X, you want that proof to be valid in the presence > of arbitrary changes to bodies called by X. Agreed. Again, this problem statement was from an earlier version of the AI. It seemed adequate to capture the problem, but it could perhaps use some wordsmithing. >> We need to refine the notion of SPARK's Global aspect, because SPARK >> does not support access types, and because SPARK relies on an >> elaborate mechanism for handling the abstract “state” of packages. > > What's your opinion about that elaborate mechanism? I've never > understood why it's needed, but I'm told by SPARK folks that it's > super-useful. I'd like to understand why, and whether we ought to add > such stuff to Ada. The elaborate mechanism is needed if you make heavy use of global variables. I have come to really hate global variables, so for me, it seems to only encourage an evil habit. But when it comes to typical embedded software, I know that it is quite common to have a huge number of global variables representing the state of the environment. These global variables are periodically updated as the result of sensor readings, and they are read whenever needed by algorithms trying to react to the environment. I would hope there are better ways to structure such systems, but I think SPARK is trying to deal with reality as we know it, and many of these systems seem to represent the state using globals. >> ...The >> refinements we are proposing are the following: >> >> 1. Allow the name of an access type A (including "access T") to >> stand-in for the set of objects described roughly by: > > "stand in" (no dash) Good point. >> (for all X convertible to A => X.all) > > That's the same thing as the collection of A, right? Yes for a pool-specific access type, no for a general access type. >> 2. Allow the name of a package P to stand-in for the set of objects >> described roughly by: "stand in" here too. >> >> (for all variables X declared in P => X) > > Does that include children of P? It would presumably need to include the private children of P, but not the public children, as you could name them separately. >> ... >> It might be useful to have another aspect that indicated which >> components of an in-out parameter might be updated, with all others >> presumably being preserved (e.g. Updated => (X.A, X.B)). > > Yes, I'm a fan of limited types, and I'd like to be able to say things > like that. If we adopt something like "Updated" then it might make sense to keep Global at the whole-object level, and use "Updated" to provide more precision for both parameters and globals. **************************************************************** From: Randy Brukardt Sent: Wednesday, November 12, 2014 9:51 PM > > Here is an AI on the Global aspect, based on SPARK and on the HILT > > 2014 paper on parallel language extensions for Ada. > > Looks good. You make it look so simple. So why didn't we already do > this? I guess the Devil's in the "!wording". Mostly FUD, really. You and I spent a lot of hours creating AI05-0186-1, complete with wording. (Perhaps you've forgotten about that.) People were concerned that it was insufficiently mature, so it didn't end up as part of Ada 2012. Also, I think there was a desire to let SPARK 2014 plow this ground first (which only covers part of the problem, of course). Unfortunately, most of the work will have to be redone; hopefully Tucker et. al. will be able to use some of the wording created for AI05-0186-1 so the effort won't totally go to waste. **************************************************************** From: Tucker Taft Sent: Wednesday, June 17, 2015 8:39 AM Here is a first attempt at wording for the Global/Global'Class aspects. [This is version /02 of the AI - Editor.] **************************************************************** From: Randy Brukardt Sent: Thursday, June 18, 2015 12:47 AM > Here is a first attempt at wording for the Global/Global'Class > aspects. ... > If a callable entity has a Global aspect other than (In_Out => all), > then it shall read only those variables global to the entity that are > within the *global variable set* identified by either the Input or > In_Out global_modes, and it shall update only those variables global > to the entity that are within the *global variable set* identified by > either the In_Out or Output global_modes. This includes any calls > within the body of the callable entity, presuming those calls read and > update all global variables permitted by their Global aspect (or > Global'Class aspect, if a dispatching call). I find this rather simplistic, since it seems to require the reader and the compiler to look through a near-infinite set of possible global variables (especially in the call case). Perhaps there is a better way to describe this without requiring that (perhaps some type of matching). I had thought that the term "global" was undefined in Ada, but it actually is defined in 8.1. Who knew? (I've been using it in an English sense forever.) --- As with nonbounded, there doesn't seem anything for formal subprograms. I don't think there is any way to write a container package with these annotations unless there is some way to control the actual subprograms and/or export the same annotations on the routines that call the formal subprograms. The annotations are next to useless if you can't write a generic container using them (and preferably, they'll work with the existing containers). --- There clearly has to be some rules for predefined operations. Most of them should have global => null, but beware of record equality, which can incorporate user-defined "=". I never figured out a good way to handle that (requiring global => null on those as well would have been great, but it's at least 35 years too late for that). --- The entire predefined library needs to be decorated. In the old AI, I proposed doing that by having some defaults for pure library units (which shouldn't have any global state), but we'd still want to manually do it for the containers and possibly other useful packages (probably not for the I/O packages). Perhaps that should be a separate AI or AIs due to the size. Enough comments for tonight. **************************************************************** From: Tucker Taft Sent: Sunday, June 5, 2016 4:26 PM I made some significant updates, to some degree following Randy's approach for Nonblocking. Nonblocking and Global are quite similar in various ways, as they essentially represent side effects of operations. It might be nice if they could somehow share more wording. Biggest change was to add a 'Global attribute for use in generics (similar to Randy's use of the 'Nonblocking attribute), and to define the meaning of 'Global on a composite type, being the globals referenced during the initialization, adjustment, and finalization operations of the type. [Version /03 of this AI was attached - Ed.] **************************************************************** From: Tucker Taft Sent: Monday, June 12, 2017 6:26 PM Sorry to be so late. Hopefully Randy is still in Wisconsin. [This was version /04 of the AI.] I switched over to using in, in out, out. I now require the mode to be specified, even if it is "in", since otherwise the syntax was just too funky. I added "proof in" to support use in assertion expressions, and allowed references to limited views of packages and incomplete views of types, so "limited with" can be of some use. I removed public children from what is covered by Global => in Pkg_Name, but left the visible part, since with a limited view of a package, it wouldn't be possible to refer to individual declarations from the visible part. **************************************************************** From: Randy Brukardt Sent: Monday, June 12, 2017 7:48 PM Generally looks good. Some free association: (1) Not sure why you have "OLD STYLE" and "NEW STYLE" grammars. It just looks confusing. "Old Style" is cheap beer, not something that belongs in an AI. ;-) (2) The "New Style" grammar contains "proof" explicitly like a reserved word. Are you proposing a new reserved word, to fight about unreserved keywords yet again (this seems like a perfect use for such a thing), or something else?? (3) "/object_/name identifies the specified global variable (or non-preelaborable constant, which is ignored for the purposes of the remaining rules)" I'm not sure "ignored" is the right way to put this. I think you're trying to say that the possibility of non-preelaborable constants isn't mentioned in later rules. But that's a bit weird, because many of the later rules talk only about variables, and it would seem easy enough to talk about "objects", at least in the three following rules. Or maybe describe them as a term covering variables and non-preelaborable constants. (4) Minor glitch: You ought to only italicize the defining occurrence of a term, you've got every occurrence of "global variable set" in italics (signified by surrounding by *s). [BTW, wouldn't it be better to call this a "global object set", since some constants are included? Rather than telling people to "ignore" the possibility of a constant being included? Why lie if you don't have to?] **************************************************************** From: Tucker Taft Sent: Tuesday, June 13, 2017 3:54 AM > (1) Not sure why you have "OLD STYLE" and "NEW STYLE" grammars. It > just looks confusing. "Old Style" is cheap beer, not something that > belongs in an AI. ;-) I left it there purely for comparison. Initially I thought I would keep the old style as an option, but ultimately decided to fix all the wording to presume we go with the new style. So better would probably be to put the OLD STYLE stuff in the !discussion or the !proposal. > (2) The "New Style" grammar contains "proof" explicitly like a > reserved word. Are you proposing a new reserved word, to fight about > unreserved keywords yet again (this seems like a perfect use for such > a thing), or something else?? Good question. Perhaps it should just be " IN” from a syntax point of view, where is either “proof” or some implementation-defined identifier. > (3) "/object_/name identifies the specified global variable (or > non-preelaborable constant, which is ignored for the purposes of the > remaining rules)" I'm not sure "ignored" is the right way to put this. > I think you're trying to say that the possibility of non-preelaborable > constants isn't mentioned in later rules. But that's a bit weird, > because many of the later rules talk only about variables, and it > would seem easy enough to talk about "objects", at least in the three > following rules. Or maybe describe them as a term covering variables > and non-preelaborable constants. I tried to do that and it just started getting really complicated. So I punted and chose to allow a name that refers to a non-preelaborable constant, but otherwise ignoring it later. I agree the wording needs work. Perhaps better would be to just allow an implementation-defined extension to the syntax, and not talk about it further. Non-preelaborable constants match pretty closely to what SPARK requires, but it is probably just confusing to give only part of that. > (4) Minor glitch: You ought to only italicize the defining occurrence > of a term, you've got every occurrence of "global variable set" in > italics (signified by surrounding by *s). [BTW, wouldn't it be better > to call this a "global object set", since some constants are included? > Rather than telling people to "ignore" the possibility of a constant > being included? Why lie if you don't have to?] Sorry about that. Yes I began to notice too many “*”s there, but didn’t have time to go back and decide what should be the defining occurrence. **************************************************************** From: Randy Brukardt Sent: Tuesday, June 13, 2017 1:15 PM ... > > (3) "/object_/name identifies the specified global variable (or > > non-preelaborable constant, which is ignored for the purposes of the > > remaining rules)" I'm not sure "ignored" is the right way to put this. ... > I tried to do that and it just started getting really complicated. So > I punted and chose to allow a name that refers to a non-preelaborable > constant, but otherwise ignoring it later. I agree the wording needs > work. Perhaps better would be to just allow an implementation-defined > extension to the syntax, and not talk about it further. > Non-preelaborable constants match pretty closely to what SPARK > requires, but it is probably just confusing to give only part of that. I thought that just generally replacing "variable" by "object" in your wording (except the very first part) would work fine. I do agree that constants that can be modified (as we had a long debate about) ought to be included here, and I don't think there is any need to refer to SPARK to explain that. 3.3 is very clear that not all constants are really constant, and clearly this construct needs to include them. Referring to "variable" in formal Ada definitions is almost always wrong, other than in an actual assignment statement target. **************************************************************** From: Florian Schanda Sent: Thursday, June 15, 2017 2:20 AM > Sorry to be so late. Hopefully Randy is still in Wisconsin. I > switched over to using in, in out, out. I like the new syntax you propose, in a way we've come full circle (SPARK 2005 used exactly these). However in SPARK 2014 we've used Input, In_Out, etc. for reasons of "its more like an aggregate that way" but I was never really happy with that reasoning. At the risk of asking a silly question, does proof in make sense as a parameter mode? Of course Tuck, if Ada adopts your syntax as its Global syntax then we're going to have a bit of fun in SPARK trying to make this backwards/forwards compatible. I suspect the SPARK extension will then just say "you can use Input as synonym for in, and you can't use both in the same global aspect, etc."? **************************************************************** From: Tucker Taft Sent: Thursday, June 15, 2017 3:32 AM > ... > At the risk of asking a silly question, does proof in make sense as a > parameter mode? I presume you mean for a subprogram. If we go that route, it would seem to be similar to having a "ghost" parameter, in which case "ghost in" might be more appropriate than "proof in." Perhaps we should make "ghost" into a reserved word, and allow it on subprograms and types where we currently allow "abstract" or "null," and in object declarations where the word "constant" or "aliased" might appear. > Of course Tuck, if Ada adopts your syntax as its Global syntax then > we're going to have a bit of fun in SPARK trying to make this > backwards/forwards compatible. I suspect the SPARK extension will then > just say "you can use Input as synonym for in, and you can't use both > in the same global aspect, etc.”? You will have to use "Input =>" as equivalent to "in". The "=>" will be the most important discriminator, I think. **************************************************************** From: Florian Schanda Sent: Thursday, June 15, 2017 8:19 AM > You will have to use "Input =>" as equivalent to "in". The "=>" will > be the most important discriminator, I think. There will be some pain to make sure this is not possible: with Global => (Input => X, out X) or: with Global => (Input => X, in Y) Do note that SPARK allows: with Global => X and with Global => (X, Y, Z) It may be worth to allow these as shorthands for the "in". It would also mirror parameters (missing mode = in) and really globals are a kind of parameter ;) Anyways, even with these difficulties I still think the new (yet old) style is better :) **************************************************************** From: Tucker Taft Sent: Thursday, June 15, 2017 8:26 AM ... > There will be some pain to make sure this is not possible: > > with Global => (Input => X, > out X) I think you should have a switch that you pass around when doing parsing to be in one of three states — uncommitted, committed to reserved-word modes, committed to non-reserved-word modes with “=>”. ... > It may be worth to allow these as shorthands for the "in". It would > also mirror parameters (missing mode = in) and really globals are a > kind of parameter ;) I considered this and ultimately rejected it, as being a short-hand that just added complexity and ambiguity to the syntax, and only saved two characters. Yes I know “in” is optional in subprogram parameters, but there is much more context there. Here all we have is a mode and a name, and I think omitting the mode is not helpful. It is just too easy to interpret a missing mode as meaning “all access” (i.e. “in out”) rather than read-only access. **************************************************************** From: Brad Moore Sent: Friday, September 1, 2017 6:46 PM [From a thread in AI12-0119-1 - Editor] "Although SPARK only allows names of stand-alone objects in Global annotations, for Ada we allow any object name, presumably including an indexed component or a slice. We also have proposed in AI12-0079 to allow them on formal subprograms and access-to-subprogram, so I think the cases you mentioned are consistent with the current AI." Thats great, but one thing that isn't in AI12-0079 is to be able to use the array keyword, to indicate any array, or arrays, not just a specific named array. In a library call, such as my parallelism libraries, the library call has no knowledge of which global arrays the clients code might access, so I cannot name these arrays in the specification. It really doesn't matter which global arrays the client accesses, so long as only the specified slice of those arrays is accessed. For example, one client might sum arrays A and B into C, and another client might sum arrays D and E into F. It doesn't matter which arrays are accessed, the library guarantees that the slices wont overlap, which can be viewed as a post condition that the library implementation promises. The global aspect in this case, however forms a precondition that ensures that the client will use the library as it was intended. **************************************************************** From: Tucker Taft Sent: Friday, September 1, 2017 7:50 PM I don’t see the point of solving this problem only for arrays, when there is a general challenge associated with mentioning things in a “Global” annotation that are not normally visible in the spec. SPARK solves this by allowing the programmer to invent a notion of “abstract state,” and then defining what that abstract state comprises in the body. On the other hand, this seems like excessive complexity for Ada, and in some sense harkens back to the days when global variables were used for all kinds of inter-module communication. My own view is that we should be discouraging the use of global variables, and instead rely on Ada’s support for passing slices if we want to give a subprogram access to only a particular slice of an array. Note that even eliminating global annotations completely doesn’t solve the issue of compile-time checking of data races, given that we could pass two different slices of the same array to two different parallel calls. To ensure these two slices don’t overlap, we would probably still need to define run-time checks to ensure there is no overlap, with many compilers (hopefully) being able to eliminate the check at compile-time. **************************************************************** From: Randy Brukardt Sent: Tuesday, September 5, 2017 7:20 PM > I don't see the point of solving this problem only for arrays, when > there is a general challenge associated with mentioning things in a > "Global" annotation that are not normally visible in the spec. Right. This is just part of a much more general problem. > SPARK solves this by allowing > the programmer to invent a notion of "abstract state," and then > defining what that abstract state comprises in the body. > > On the other hand, this seems like excessive complexity for Ada, and > in some sense harkens back to the days when global variables were used > for all kinds of inter-module communication. My own view is that we > should be discouraging the use of global variables, and instead rely > on Ada's support for passing slices if we want to give a subprogram > access to only a particular slice of an array. That doesn't fix anything in the case of generic units, though. I was rather expecting/hoping that you'd use a version of the attribute mechanism that I worked out for Nonblocking for Global as well. In particular, giving a Global aspect on a generic formal requires some form of generic matching: generic type Priv is private; with procedure Do_It (Param : in out Priv) with Global => in out null; package Gen1 is ... In this case, actual subprograms to Do_It have to "match" (in some sense - stronger should be allowed, weaker not allowed) the "in out null" Global aspect. But that is incompatible in interesting cases. generic type Priv is private; with procedure Do_It (Param : in out Priv); package Gen2 is procedure Frobnicate (Param : in out Priv) with Global => Do_It'Global and package Gen2; end Gen2; Here, we're "reflecting" the Global aspect of the generic formal through a outine of the generic package (and also allowing local package state). This keeps compatibility while providing the maximum capability for the routines. We'll need such a mechanism to allow the containers (which can't get incompatible) to be used in checked parallel structures (and any other uses of the Global aspect). Note that these attributes provide a "poor man's" way to name a specific Global state. One can always declare a dummy subprogram: procedure Global_State with Global => ...; and then use that Global setting in other subprograms. procedure Bletch with Global => Global_State'Global and in out Foobar; There does seem to be a need to somehow describe data of private helper packages without naming the packages. That seems important for the Ada runtime, as we don't want to force all of the implementations to internally structure their Ada library the same way. (Case in point: Janus/Ada has a library System.Basic_IO that implements the underlying I/O operations; I believe GNAT has a similar library but of course with a different name. The handles for Stdin, Stdout, and Stderr are found there; those can't change during a run but aren't constant as they are determined dynamically during the program startup.) The SPARK scheme would work for that, but it seems like overkill. > Note that even eliminating global annotations completely doesn't solve > the issue of compile-time checking of data races, given that we could > pass two different slices of the same array to two different parallel > calls. To ensure these two slices don't overlap, we would probably > still need to define run-time checks to ensure there is no overlap, > with many compilers (hopefully) being able to eliminate the check at > compile-time. Yes, that seems reasonable. Perhaps we have to handle race conditions arising from Atomic object misuse the same way? (Updates like Atom := Atom + 1; are not safe as these are separate reads and writes.) **************************************************************** From: Brad Moore Sent: Saturday, September 16, 2017 1:13 PM >> I don't see the point of solving this problem only for arrays, when >> there is a general challenge associated with mentioning things in a >> "Global" annotation that are not normally visible in the spec. > Right. This is just part of a much more general problem. OK, but I now am proposing a more general solution to the more general problem, at least generalizing this to work for both arrays and containers. Instead of the array keyword that I suggested earlier, suppose we extended the global aspect to include the syntax form; global => all (name1 .. name2) The idea here is that this indicates that the only use of globals is via indexing lookups (via a range of scalar indexes, or container cursors). The keyword "all" here represents all visible globals. Specific global names could be used also, with the same index/slicing syntax. The compiler would do the normal processing for global checks, but if the only use of globals is via the specified slice of the container or array, then the global check would pass. We could say that this implies that the only use of these globals is via a loop cursor of a for loop that mentions name1 and name2 to initialize the loop cursor, so I would think it would be pretty easy for the compiler to check this. To do a slice of a container, we just need an iterator that can operate on a slice of a container. The existing containers almost already support this, because there exists Iterate calls that allow you to specify the start of iteration. eg. For Doubly_Linked_Lists for Item in My_List.Iterate (Start => My_Cursor) loop .... end loop; If we had an Iterate call that allowed you to specify both the Start and the Finish cursors, then one could write; for Item in My_List.Iterate (Start => My_Start_Cursor, Finish => My_End_Cursor) loop .... end loop; In fact, I don't know why we don't already have these calls. They would be more useful than the ones we have today that allow you to only specify the start cursor, with the end cursor implicitly being container.Last; C++ iterators for instance allow one to iterate through a subset of an array or container. It seems like useful functionality. We could either add a default parameter for Finish that defaults to Last, or add a new call for the Container libraries. As a simple example of the global syntax, consider a very basic parallel loop library; Note I am using Randy's 'global attribute, as I think it is needed also. generic type Loop_Index is range <>; with procedure Process (Start, Finish : Loop_Index) with Pre => (Start < Finish), -- Can we currently put pre and post on formals? Global => all (Start .. Finish); -- package Parallel is procedure Parallel_Loop (From : Loop_Index := Loop_Index'First; To : Loop_Index := Loop_Index'Last); with Process'Global and Global => null; end Parallel; package body Parallel is procedure Parallel_Loop (From : Loop_Index := Loop_Index'First; To : Loop_Index := Loop_Index'Last) is task type Worker (Start_Index, End_Index : Loop_Index); task body Worker is begin Process (Start_Index, End_Index); end Worker; Left_End : constant Loop_Index := From + ((To - From + 1) / 2) - 1); Left_Worker : Worker (Start_Index => From, End_Index => Left_End; Right_Worker : Worker (Start_Index => Left_End + 1, End_Index => To); begin -- Parallel_Loop null; end Parallel_Loop; end Parallel; I could show a similar example for a parallel container iteration, library call but thought it best for now to just show a simple array case. In fact I have a single generic library call that can be used for both array and container iteration, and I think the global => all (name1 .. name2) syntax would work for both cases for different instantiations of the same generic. One reason why I think this is important is because for such library calls, the abstraction is to only provide parallel chunking over a range of cursor/index. The client may use this to operate on any number of global references. For example, calculate the sum of integers from 1 .. N involves 0 arrays. Increment all the values of an array involves 1 array. Add Array1 to Array2 involves 2 arrays. Add Array1, and Array2, to Array 3 arrays. One library call can be used to handle all these cases. If one were to pass the globals into the library call by naming them, then I think you would need an infinite number of library calls to be written to handle all the possible cases. Using globals in this manner, one library call can be used to do all parallel looping problems. ... >> Note that even eliminating global annotations completely >> doesn't solve the issue of compile-time checking of data >> races, given that we could pass two different slices of the >> same array to two different parallel calls. To ensure these >> two slices don't overlap, we would probably still need to >> define run-time checks to ensure there is no overlap, with >> many compilers (hopefully) being able to eliminate the check >> at compile-time. Yes, in the example above it seems pretty obvious by inspection in the package body that there can be no overlap. Hopefully the compiler can be smart enough to see that also. We might want to define some sort of aspect or attribute (Overlap => False? Covered_Once => True?) that tells the compiler to add these checks. In the absence of those checks and with the compiler not being able to prove that the calls to Process in my example above are non-overlapping, we might want to allow the programmer to suppress the global checking on the call from inside the body. There is still value though to the global all slicing aspect even if the global checking is suppressed in the body of the library because it can ensure at least that the clients of the library call are well behaved. If the library call itself can be trusted to not call the client with overlapping ranges, it seems valuable to the client to have the compiler reject compilations where the client is accessing globals in an unsafe manner. The global => all(name1 .. name2) on the callback formal subprogram would provide the check on the clients code. **************************************************************** From: Tucker Taft Sent: Monday, September 25, 2017 4:33 PM Here is the first piece of my ARG homework. Mostly I tried to fix up the syntax according to our discussions in Vienna. [This is version /05 - Editor.] **************************************************************** From: Randy Brukardt Sent: Monday, October 2, 2017 8:53 PM > Here is the first piece of my ARG homework. Mostly I tried to fix up > the syntax according to our discussions in Vienna. Thanks for getting this done early. Can I expect the rest of your homework early, too?? ;-) A couple of thoughts: (1) I think you need to soon (if not immediately) address how these are going to work within generic units and presumably for access-to-subprogram types. If we plan to use Global aspects for checking in parallel statements *and* we also want to use the containers there *and* we don't want any significant incompatibilities in the containers, then we have to have a "reflection" mechanism for generics. The mechanism designed for nonblocking provides one model for doing that. This is likely to be complicated (the Global aspect is not as simple as the boolean value of Nonblocking), and thus we need to get started on defining it (it isn't going to work as a last minute thing). Recall we have less than two years to finish this definition to standardization quality (if we intend to stay on schedule). (2) If we intend to use Global aspects for checking in parallel statements, we need to figure out the details of that checking sooner rather than later. The checking rules most likely will in part inform how the Global rules need to work. (3) I didn't see a solution for global data defined in hidden packages, such as the System implementation helpers that both Janus/Ada and GNAT have. We can't start requiring implementors to restructure their entire runtime in order to meet Global settings. (4) I didn't see any discussion of the defaults for Global the runtime packages. I realize the detailed update is going to be a large job in itself, but I'd like to hear at least about what the defaults will be. (5) I think I object to the idea of "synthesized" global aspects. (I'm sorry I didn't think of this during the meeting.) The basic idea is that global aspects, like many other aspects including Pre, Post, and Nonblocking, represent contracts between the caller and the callee. These are enforced on the calls without any knowledge of the implementation, and similarly are enforced on the body without any knowledge of the calls. "Synthesized", however, means that the contract depends on the contents of the body, requiring that a body need be present before any calls can be compiled and meaning that future maintenance on a body can break calls (a complete violation of the separation of calls and implementation). Note that existing cases of body dependencies (generic instances, aspect Inline) in Ada have two important properties: (1) they're optional, no Ada compiler needs to implement them (Janus/Ada does not; the primary reason we implemented generic code sharing was to avoid generic body dependencies); (2) the code will not change legality regardless of changes in the body. "Synthesized" will fail (2) and thus be a horrific maintenance hazard (especially given the cascade effects of contracts). My long time objection to systems like SPARK is their need to have the complete program available before they can prove anything. I don't want to see Ada going down that road. Synthesizing contracts (Global among them) seems like a ripe area for tools, and there seems to be no need to include it in the language proper. Moreover, an implementation could define "Synthesized" if it wanted to (implementation-defined modifiers are allowed), and that seems preferable to defining in the language something contract-related that destroys the contract model! **************************************************************** From: Yannick Moy Sent: Monday, October 2, 2017 11:42 PM ... >(1) I think you need to soon (if not immediately) address how these are >going to work within generic units and presumably for access-to-subprogram >types. Not sure why you're saying that. Pre/Post also don't work with access-to-subprogram currently. ... >(3) I didn't see a solution for global data defined in hidden packages, such >as the System implementation helpers that both Janus/Ada and GNAT have. We >can't start requiring implementors to restructure their entire runtime in >order to meet Global settings. I think that's the part where package P is meant to represent all data hidden in P and its private children. Or you have something else in mind? ... >(5) I think I object to the idea of "synthesized" global aspects. (I'm sorry >I didn't think of this during the meeting.) I also do not like it. To me, it looks useless: absence of the aspect already indicates we know nothing of its reads/writes of global variables. >My long time objection to systems like SPARK is their need to have the >complete program available before they can prove anything. I don't want to >see Ada going down that road. This is completely wrong. :-) SPARK is fully modular, except for two things: checking of concurrency, which is rather a minor point, and generation of Global contracts but *only* when they are not provided by the user. And even in that second case, you only need to look at the sub-call graph from a subprogram to generate its Global. **************************************************************** From: Randy Brukardt Sent: Tuesday, October 3, 2017 12:25 AM >>(1) I think you need to soon (if not immediately) address how these >>are going to work within generic units and presumably for >>access-to-subprogram types. >Not sure why you're saying that. Pre/Post also don't work with >access-to-subprogram currently. The generic cases (which is mainly what I'm concerned about) are necessary to deal with if Global is to work with the containers. And if it doesn't work with the containers, a significant number of programs couldn't use Global (including most of the intended uses of Global in parallel blocks and loops). Pre/Post are dynamic constructs in Ada (as opposed to SPARK), so it doesn't matter much how they work with access-to-subprogram. Indeed, there is an open AI to improve that (it's unlikely to stay precisely as it is). Global, however, is statically enforced in Ada, so it has to be handled "right" for access-to-subprogram, generics, and any other such cases. There's no leeeway (something I learned in detail defining Nonblocking). >>(3) I didn't see a solution for global data defined in hidden >>packages, such as the System implementation helpers that both Janus/Ada >>and GNAT have. We can't start requiring implementors to restructure their >>entire runtime in order to meet Global settings. >I think that's the part where package P is meant to represent all data >hidden in P and its private children. Or you have something else in mind? I'm thinking of unrelated packages that are used to implement some library package. For instance, Janus/Ada bases all of its I/O packages on a package called System.Basic_IO. That has some global state. I believe GNAT does something similar with it's I/O packages; they seem to depend on children of System and GNAT. It would be amazing if no such package ever needed global state. (Certainly that will rarely happen if storage pools are considered state, as they ought to be.) [Poster's note: I should have mentioned that you don't want to have to name these unrelated packages in the Global of the package specification; the user should need to know nothing about them. Especially important for language-defied packages.] Forcing implementers to either remove the state or restructure their runtime to put everything in private packages (which might be very difficult given visibility issues and the like) seems like the wrong way to go. It seems like there needs to be some way to refer to state of any/all packages that might be used to implement a package but aren't visible in that package's specification. >> (5) I think I object to the idea of "synthesized" global aspects. >> (I'm sorry I didn't think of this during the meeting.) > I also do not like it. To me, it looks useless: absence of the aspect already > indicates we know nothing of its reads/writes of global variables. Glad to hear I'm not completely crazy. >> My long time objection to systems like SPARK is their need to have >> the complete program available before they can prove anything. I >> don't want to see Ada going down that road. > This is completely wrong. :-) > SPARK is fully modular, except for two things: checking of > concurrency, which is rather a minor point, and generation of Global > contracts but *only* when they are not provided by the user. And even in > that second case, you only need to look at the sub-call graph from a > subprogram to generate its Global. I don't want any "except for" in Ada. Period. Good to hear that SPARK has moved away from complete source code, though. **************************************************************** From: Randy Brukardt Sent: Tuesday, October 3, 2017 1:40 AM >The generic cases (which is mainly what I'm concerned about) are necessary >to deal with if Global is to work with the containers. And if it doesn't >work with the containers, a significant number of programs couldn't use >Global (including most of the intended uses of Global in parallel blocks and >loops). Why would you want to use Global on generic containers? Morally, container's API reads/writes no globals (except for those like Query_Element and Update_Element that take a callback in argument, which may have such an effect). The bounded containers indeed have "Global => null" contracts, while the regular ones actually allocate memory, so with Tuck's proposal you would have to mention the corresponding access type. But there is no strong guarantee here, as the formal parameters of the instance could write or read a global variable. A more complex scheme would have a way to describe the formal parameters or callbacks globals, something like Subp'Global, but that would quickly turn into a nightmare I'm afraid. >Global, however, is statically enforced in Ada, so it has to be handled >"right" for access-to-subprogram, generics, and any other such cases. >There's no leeeway (something I learned in detail defining Nonblocking). I don't see why we could not have a situation where the compiler enforces part of the property, leaving holes to be filled by other tools? That's similar to the distinction between static checking and dynamic checking. Except here of course you cannot describe the static analysis performed in these other tools that complete the compiler. >I'm thinking of unrelated packages that are used to implement some library >package. For instance, Janus/Ada bases all of its I/O packages on a package >called System.Basic_IO. That has some global state. I believe GNAT does >something similar with it's I/O packages; they seem to depend on children of >System and GNAT. It would be amazing if no such package ever needed global >state. (Certainly that will rarely happen if storage pools are considered >state, as they ought to be.) > >Forcing implementers to either remove the state or restructure their runtime >to put everything in private packages (which might be very difficult given >visibility issues and the like) seems like the wrong way to go. > >It seems like there needs to be some way to refer to state of any/all >packages that might be used to implement a package but aren't visible in >that package's specification. I believe that's what Tuck proposes when he refers to the name of the package. So in your case, System.Basic_IO would refer to all hidden state in that unit. >I don't want any "except for" in Ada. Period. Good to hear that SPARK has >moved away from complete source code, though. It was never the case, even for the first version of SPARK 83. :-) **************************************************************** From: Randy Brukardt Sent: Tuesday, October 3, 2017 2:28 AM ... >Why would you want to use Global on generic containers? Because it's wildly incompatible if you don't. Since Global isn't currently specified on existing subprograms, all existing instances would fail until lobal is added. (Formals would have to have to have no global, that is global => in out null, and that would have to be checked during instantiation.) > Morally, container's API reads/writes no globals (except for those > like Query_Element and Update_Element that take a callback in > argument, which may have such an effect). The bounded containers > indeed have "Global => null" > contracts, while the regular ones actually allocate memory, so with > Tuck's proposal you would have to mention the corresponding access type. Yes, that's part of it. Also, the container package itself may have some state (free chains and a serial number exist in the proposed Janus/Ada implementations). Perhaps we could ban that from the bounded containers (since node sharing isn't an option for those), but it is a dead-body issue for me on the other containers. > But there is no strong guarantee here, as the formal parameters of the > instance could write or read a global variable. There has to be. For the intended use in Ada 2020, preventing race conditions and other tasking screwups, detecting only some easy cases and letting the hard ones get through is not an option. This is also a dead-body issue for me; I'm not remotely interested in parallel statements unless they are safe by construction (it is easy to write unsafe Ada tasking code, using something like Brad's Parafin libraries; the language needs no enhancements to do that). And without parallel statements, we don't need Global at all (there's no other proposed use for it at this point), and in fact we probably don't need Ada 2020 at all (there's just not enough else of value, and restarting from nothing is not going to get us anywhere useful by mid-2019). > A more complex scheme would have a way to describe the formal > parameters or callbacks globals, something like Subp'Global, but that > would quickly turn into a nightmare I'm afraid. That's the only option that is compatible and safe, and thus I want to get started on it ASAP. If we're not willing to do that, I would like to know right away so that we can either abandon or redirect our other work into productive areas (which Global would not be). Note that it isn't impossible; I worked out all of the details for Nonblocking (admittedly easier in some ways as a Boolean aspect) and following that pattern should work fine here (just more complex for the checking). (If we replaced Global by a boolean aspect -- say "Task_Safe" -- it would be trivial to do; just do the same as Nonblocking -- but of course that is rather limiting as parallel statements wouldn't allow any unprotected globals, even if they don't conflict.) >> Global, however, is statically enforced in Ada, so it has to be >> handled "right" for access-to-subprogram, generics, and any other such cases. >> There's no leeeway (something I learned in detail defining Nonblocking). > I don't see why we could not have a situation where the compiler > enforces part of the property, leaving holes to be filled by other > tools? That's similar to the distinction between static checking and > dynamic checking. Except here of course you cannot describe the static > analysis performed in these other tools that complete the compiler. As noted above, for the intended use in preventing race conditions and other tasking errors, this is completely unacceptable. If there is a possible race condition, it *must* be detected either at compile-time or run-time. There's no grey area there. So putting off part of it to other tools is simply unacceptable. Some other tool might be able to prove that something Ada doesn't allow actually is OK, and that could be useful if the "Soft Error" scheme is adopted, but that's about it. >>I'm thinking of unrelated packages that are used to implement some >>library package. For instance, Janus/Ada bases all of its I/O packages >>on a package called System.Basic_IO. That has some global state. I believe >>GNAT does something similar with it's I/O packages; they seem to depend on >>children of System and GNAT. It would be amazing if no such package ever >>needed global state. (Certainly that will rarely happen if storage pools are >>considered state, as they ought to be.) >> >>Forcing implementers to either remove the state or restructure their >>runtime to put everything in private packages (which might be very difficult >>given visibility issues and the like) seems like the wrong way to go. >> >>It seems like there needs to be some way to refer to state of any/all >>packages that might be used to implement a package but aren't visible >>in that package's specification. >I believe that's what Tuck proposes when he refers to the name of the >package. So in your case, System.Basic_IO would refer to all hidden state in >that unit. Sure, but no one is going to put System.Basic_IO into the specification of Ada.Text_IO. It is only referenced from the body. Moreover, the specification of Ada.Text_IO in the RM has to somehow reference the possibility of state in these packages (different for every vendor) in the Global aspects that apply to the Ada.Text_IO package. We're surely not putting Global => System.Basic_IO into the RM!! **************************************************************** From: Yannick Moy Sent: Tuesday, October 3, 2017 2:53 AM >Because it's wildly incompatible if you don't. Since Global isn't currently >specified on existing subprograms, all existing instances would fail until >Global is added. (Formals would have to have to have no global, that is >global => in out null, and that would have to be checked during >instantiation.) It seems to me that this extremist approach is bound to fail. I see no point in forcing Global on everything. >There has to be. For the intended use in Ada 2020, preventing race >conditions and other tasking screwups, detecting only some easy cases and >letting the hard ones get through is not an option. This is also a dead-body >issue for me; I'm not remotely interested in parallel statements unless they >are safe by construction (it is easy to write unsafe Ada tasking code, using >something like Brad's Parafin libraries; the language needs no enhancements >to do that). And without parallel statements, we don't need Global at all >(there's no other proposed use for it at this point), and in fact we >probably don't need Ada 2020 at all (there's just not enough else of value, >and restarting from nothing is not going to get us anywhere useful by >mid-2019). I don't see why the compiler would have to check all the boxes here. This will require analysis techniques beyond what the compiler can do. But I think that the compiler could do something very valuable, which is to check indeed that loops can be parallelized based on the Global contracts on the subprograms it calls. That would leave the verification of Global contracts themselves to other tools. >>A more complex scheme would have a way to describe the formal parameters >>or callbacks globals, something like Subp'Global, but that would quickly >>turn into a nightmare I'm afraid. >That's the only option that is compatible and safe, and thus I want to get >started on it ASAP. If we're not willing to do that, I would like to know >right away so that we can either abandon or redirect our other work into >productive areas (which Global would not be). Based on our experience with users using Global contracts, I'd say it's unlikely you manage to make something that complex as Subp'Global inside other contracts be useful to anyone. >>I don't see why we could not have a situation where the compiler enforces >>part of the property, leaving holes to be filled by other tools? That's >>similar to the distinction between static checking and dynamic checking. >>Except here of course you cannot describe the static analysis performed >>in these other tools that complete the compiler. > >As noted above, for the intended use in preventing race conditions and other >tasking errors, this is completely unacceptable. If there is a possible race >condition, it *must* be detected either at compile-time or run-time. There's >no grey area there. So putting off part of it to other tools is simply >unacceptable. Some other tool might be able to prove that something Ada >doesn't allow actually is OK, and that could be useful if the "Soft Error" >scheme is adopted, but that's about it. OK if you can pull it, but I doubt it's possible with "just" compilation techniques, while managing an acceptable complexity in annotations. Or just settle for something very simple, such as Global=>null that indicates that no global is read/written, which could be inferred by the compiler for a subprogram based on the contracts of subprograms it calls (no need for a global analysis), so would be inferred in particular for generic instances. **************************************************************** From: Randy Brukardt Sent: Tuesday, October 3, 2017 2:59 PM >It seems to me that this extremist approach is bound to fail. I see no >point in forcing Global on everything. If we don't, then we cannot solve any of the problems that we are trying to solve. If you are right, then we should abandon work on Global immediately and switch to something simpler that will work (perhaps a pair of aspects "Task_Safe" and "Extra_Pure"). >I don't see why the compiler would have to check all the boxes here. >This will require analysis techniques beyond what the compiler can do. No. There is no requirement that all things that might be parallelizable be legal Ada (you can always use an unsafe technique to get that). We just want to allow what is obviously safe. >But I think that the compiler could do something very valuable, which is to >check indeed that loops can be parallelized based on the Global contracts on >the subprograms it calls. That would leave the verification of Global >contracts themselves to other tools. The vast majority of Ada users have no other tools. The language is wildly incomplete if it cannot be used without depending on "other tools". Moreover, if some "other tool" can exist that verifies some important property, then that tool can be part of the Ada compiler. Dependence on "other tools" for critical functionality is evil. In any case, Global has to be defined in terms of what it allows. If it is not, then it has no semantic meaning within the Ada Standard, and that would make it nonsense to define. (Plus, that is NOT what Tucker is currently proposing.) ... >Based on our experience with users using Global contracts, I'd say it's >unlikely you manage to make something that complex as Subp'Global >inside other contracts be useful to anyone. It certainly works for Nonblocking (at least in the context of the containers, which is the critical case); I fail to see (today!) why it would be different for Global. For the intended tasking purpose, the only truly interesting Global contracts are "in out null" and "synchronized" (everything else would conflict by definition in a parallel loop). They could be defined by aspects that work like Nonblocking, and that clearly will work in the context of the containers. If Global can't be made to work here, then we ought to abandon Global in favor of something that will work. ... >OK if you can pull it, but I doubt it's possible with "just" >compilation techniques, while managing an acceptable complexity in >annotations. We don't need perfection, we only need a guarantee that the contract reflects reality. I fail to see why you think that requires advanced analysis (the Global contract of a subprogram is the union of all of the contracts of the subprograms that it calls, plus all of globals that it directly reads or writes -- hard to see where complex analysis would be needed). >Or just settle for something very simple, such as Global=>null that indicates >that no global is read/written, which could be inferred by the compiler for >a subprogram based on the contracts of subprograms it calls (no need for a >global analysis), so would be inferred in particular for generic instances. That's the model of Global in Ada (as opposed to SPARK). All of the contracts Tucker has are designed to be simply checked by a compiler. And inferring the contracts for generic instantiations is how Nonblocking works (and I would like Global to work as well). But we have to have an assume-the-worst model in the generic body, and some form of reflection. Without that, you have to have body dependences, which (A) violate the Ada generic contract model, something we've never done to date; and (B) are a dead body issue for me (as previously noted) - Janus/Ada has no body dependence mechanism and is never going to have one. If there is a problem with the Subp'Global model, it is likely to be with the needed assume-the-worst rule. In that case, my preference is to abandon Global (leaving it to SPARK) and instead define two Boolean contracts (which I know can be defined properly). **************************************************************** From: Tucker Taft Sent: Tuesday, October 3, 2017 3:36 PM >> Based on our experience with users using Global contracts, I'd say >> it's unlikely you manage to make something that complex as >> Subp'Global inside other contracts be useful to anyone. > > It certainly works for Nonblocking (at least in the context of the > containers, which is the critical case); I fail to see (today!) why it > would be different for Global. ... We have already proposed using the 'Global attribute for generics in the AI. The few examples we have looked at seem to make sense. In our most recent discussion in the SPARK language-design group, we suggested we drop the explicit "Synthesized" value for the global aspect, and just give permission for an implementation to synthesize a more precise Global aspect when it would otherwise default to "in out all." Clearly if the compiler cannot synthesize a sufficiently precise Global aspect, there will be safe programs that are identified as unsafe, so such a program will not be as portable. To make such a program portable, the tool that synthesizes the more precise Global aspect would have to generate the explicit annotations and add them to the source code, which seems doable. But for a user who is happy to have non-portable code, they can leave off the explicit annotations and still have a modicum of safety. If the code is given to a compiler that doesn't have the full machinery, it will be rejected rather than being silently unsafe. **************************************************************** From: Randy Brukardt Sent: Tuesday, October 3, 2017 6:46 PM ... > We have already proposed using the 'Global attribute for generics in > the AI. The few examples we have looked at seem to make sense. Sorry, missed that. However, I didn't see the needed generic matching rules, nor the assume-the-best/assume-the-worst rules needed when using this inside a generic. So I'm not sure how it works in those cases. (Some examples similar to the ones for Nonblocking probably ought to be constructed to show the issues that need to be addressed.) > In our most recent discussion in the SPARK language-design group, we > suggested we drop the explicit "Synthesized" value for the global > aspect, and just give permission for an implementation to synthesize a > more precise Global aspect > when it would otherwise default to "in out all." Clearly if > the compiler cannot synthesize a sufficiently precise Global aspect, > there will be safe programs that are identified as unsafe, so such a > program will not be as portable. To make such a program portable, the > tool that synthesizes the more precise Global aspect would have to > generate the explicit annotations and add them to the source code, > which seems doable. But for a user who is happy to have non-portable > code, they can leave off the explicit annotations and still have a > modicum of safety. If the code is given to a compiler that doesn't > have the full machinery, it will be rejected rather than being > silently unsafe. I think I like this better than what the AI proposes. **************************************************************** From: Tucker Taft Sent: Tuesday, October 3, 2017 9:38 PM >> We have already proposed using the 'Global attribute for generics in >> the AI. The few examples we have looked at seem to make sense. > > Sorry, missed that. However, I didn't see the needed generic matching > rules, nor the assume-the-best/assume-the-worst rules needed when > using this inside a generic. So I'm not sure how it works in those > cases. (Some examples similar to the ones for Nonblocking probably > ought to be constructed to show the issues that need to be addressed.) Good point. We need to specify requirements on actuals when a formal has a Global specified. The requirements are pretty simple, as they will be based on some kind of set inclusion, but of course they need to be spelled out. ... > I think I like this better than what the AI proposes. OK, let's assume we go that direction then. **************************************************************** From: Jeff Cousins Sent: Wednesday, October 4, 2017 3:52 AM I’m afraid that I haven’t seen Tucker’s original message, please could you re-send it? [Editor's note: Tucker did so; not shown here.] **************************************************************** From: Randy Brukardt Sent: Thursday, October 5, 2017 12:25 AM ... > Good point. We need to specify requirements on actuals when a formal > has a Global specified. The requirements are pretty simple, as they > will be based on some kind of set inclusion, but of course they need > to be spelled out. You also need assume-the-best/assume-the-worst rules for the meaning of the attributes in a generic unit. Probably these can be quite simple, too: "Subp'Global" acts like "in out all" in a generic specification, with a recheck on instantiation; "Subp'Global" acts like "in out null" in a generic body, and specifically a call to Subp is allowed (while it does not allow other calls) in the scope of a contract including "Subp'Global". ... BTW, I forgot to ask if implicit composite "=" is being handled somehow. Since the default for Global is "all", the default for "=" would have to be "all" as well. Which is silly, since most "=" are pure (don't use any globals). That was the biggest mess for Nonblocking, as we ended up defining Nonblocking for types in order to change the default. (Which required generic unit changes as well.) Essentially, everything that was hard for Nonblocking is likely to have a similar problem for Global. Best that we check that we don't miss anything. **************************************************************** From: Tucker Taft Sent: Thursday, January 25, 2018 4:04 AM ... > I rather disagree; phone meetings are best for wordsmithing since it > isn't necessary to diagram on a whiteboard like it is for syntax > arguments. For Ada 2012, we used phone meetings to finalize almost all > of the wording, so it's amazing to me to think that it suddenly has > gotten difficult to do what we've done many times before. OK, I had a different goal for these phone calls. We have asked the community to get all of their proposals in by Jan 15, so I presumed one of the points of these phone calls was to deal with the final influx of proposals. > In any case, AI12-0079-1 is nowhere near complete enough for me to be > able to annotate the containers with them, a job I need to start ASAP. > For instance, we have no solution in the AI yet to the problem of > implementation-defined helper packages. We haven't discussed how to > handle atomic writes in "synchronized" mode (these are easily race > conditions which shouldn't be allowed in general, lest our goal of > preventing unsynchronized access be completely undermined). There's > probably other issues that aren't mentioned in the AI. I am willing to spend more time on 0079. I did not realize that the above was your concern. Perhaps we can handle this offline. If you can let me know what you feel you need to annotate the containers, I'll try to finalize that part of the wording. For me it just seemed like there was a general fine tuning needed, but apparently you feel there are still some big issues, at least when it comes to annotating the libraries. So if you can give me a clearer idea of what you need, I'll focus on that. > Moreover, you haven't really done much of an update for the last > couple of meetings. It seems like it isn't progressing, and it is the > most core thing we are working on. > > I was expecting that we would spend a bit of time on the 4 BIs (none > of which should require much discussion, but maybe some wordsmithing), > a bit of time on some of the new proposals (to determine whether or > not we want to pursue them, and find a victim, er, ARG author for the > AI), and the bulk of the time on AI12-0079-1 and AI12-0119-1 in the > hopes of getting some of our core work done. [Remember that > AI12-0119-1 depends on AI12-0079-1.] (We can't finish all of the AIs > for Ada 2020 in the last week, as I simply couldn't get the all into > Standard in the two weeks or so of editorial time the schedule > allows.) And then we would look at anything else as time permits. Unfortunately, it looks like perhaps we each had our own priorities for the phone calls. I appreciate what you are saying, but alas, it wasn't what I prioritized for this first call. Perhaps you and I can handle the 0079 issue ourselves without taking up time for the whole ARG. **************************************************************** From: Randy Brukardt Sent: Thursday, January 25, 2018 6:00 PM ... > > I rather disagree; phone meetings are best for wordsmithing since it > > isn't necessary to diagram on a whiteboard like it is for syntax > > arguments. For Ada 2012, we used phone meetings to finalize almost > > all of the wording, so it's amazing to me to think that it suddenly > > has gotten difficult to do what we've done many times before. > > OK, I had a different goal for these phone calls. We have asked the > community to get all of their proposals in by Jan 15, so I presumed > one of the points of these phone calls was to deal with the final > influx of proposals. True, but at this stage, that mainly is discussing broad outlines of what to do, whether to do anything at all, and then finding a victim, er author to produce a real proposal. After that, I expect we'll work in priority order, which always puts 79 and 119 first. And I've learned over the years that if you don't try to get the critical work done before doing things that are more fun, the critical work never does get done. > > In any case, AI12-0079-1 is nowhere near complete enough for me to > > be able to annotate the containers with them, a job I need to start ASAP. > > For instance, we have no solution in the AI yet to the problem of > > implementation-defined helper packages. We haven't discussed how to > > handle atomic writes in "synchronized" mode (these are easily race > > conditions which shouldn't be allowed in general, lest our goal of > > preventing unsynchronized access be completely undermined). There's > > probably other issues that aren't mentioned in the AI. > > I am willing to spend more time on 0079. I did not realize that the > above was your concern. Perhaps we can handle this offline. If you > can let me know what you feel you need to annotate the containers, > I'll try to finalize that part of the wording. I'm not completely sure at this stage, as I've never felt the proposal was solid enough to proceed. Obviously, the containers are generic, so all of the rules involving combinations and reflecting the Globals of the actuals in generic specs need to be figured out in detail. This is rather complex for Nonblocking (which is worked out), and Global is 10 times harder, so the lack of work in that area is concerning. > For me it just seemed like there was a general fine tuning needed, but > apparently you feel there are still some big issues, at least when it > comes to annotating the libraries. So if you can give me a clearer > idea of what you need, I'll focus on that. The other issue for the libraries is clearly what to do about implementation-defined "helper" packages. We surely have to allow implementations to have such packages, and they might in some circumstances have globals in them. It would seem nasty to ban that (other than in Pure packages, of course). And we surely can't name any such packages in the Standard! There's also an issue that is not specific to Global, but matters a lot. Since attribute prefixes have to be unambiguous without context, most of the names of generic formals can't be directly used in an attribute. That means that they have to be renamed to a unique name so that they can be used. For instance, for Vectors: generic type Index_Type is range <>; type Element_Type is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Vectors with Preelaborate, Remote_Types, Nonblocking => Equal_Element'Nonblocking, Global => Equal_Element'Global and and is function Equal_Element (Left, Right : Element_Type) return Boolean renames "="; ... The aspects Nonblocking and Global give the default declaration of the aspects for the contents, and we surely don't want to repeat them on all (approx) 70 subprograms. However, we've never defined what the freezing point of a package declaration is, so the place where these aspects are evaluated is not well-defined. So I don't even know if this formulation is legal. And if it isn't legal, is there any alternative that IS legal that doesn't require repeating Nonblocking and Global aspects 70 times. The third issue is about the actual definition of "synchronized". The purpose of this setting is to mark task-safe code that still uses global variables. It's pretty clear that 100% elimination of data races is impossible if any globals are involved (as soon as there is more than one global, data locks are impossible to avoid with static rules). But there definitely is low-hanging fruit that certainly should be detected. For instance, if A is a global atomic object, then A := A + 1; is a guarenteed data race (assuming any parallel execution). One should be using one of the routines in the atomic update generic that Bob doesn't think is important. ;-) I can think of a number of relatively simple additional rules that would at least eliminate the worst of these data race conditions (essentially by making them illegal in "synchronized" code). But I don't know how far we should go. My fear in this case is that a user will slap "parallel" on an existing loop to see what happens. And they then get an error about not having Global and Nonblocking contracts. So they add those, and then get an error about having a unsynchronized global object (probably with a suggestion to make them protected or atomic). So they slap "atomic" on the object, the code compiles, and the loop malfunctions badly because the object is updated without using an atomic update operation. I know at least one substantial Ada user who would function this way (I see him in the mirror every morning ;-), and not detecting bad atomic updates would greatly reduce the value of all of the other things we've done. (There's a similar issue for protected objects if someone just provides separate read and write operations rather than the update operations.) So I'd like to explore this issue a bit to see what we can do to mitigate it. [I can write a much longer discussion of this issue, but I have to get AIs created and mail filed for the meeting, lest we not have a lot of topics that we're supposed to be able to talk about in place.] ... > Unfortunately, it looks like perhaps we each had our own priorities > for the phone calls. I appreciate what you are saying, but alas, it > wasn't what I prioritized for this first call. Perhaps you and I can > handle the 0079 issue ourselves without taking up time for the whole > ARG. I'm just following the plan laid out by Jeff that he's followed at every previous meeting. I'm pretty sure that hasn't changed for this one. :-) We do have plans for more calls this winter, so this is hardly the only such opportunity. If we don't discuss it Monday, I'm sure we'll have a chance in late February. Experience shows that by the third call, Tucker is hardly touching his homework :-), so I'm trying to get you to do as much of it now as possible. (And you've certainly done some of it -- but we put priority indications on AIs for a reason ... High > Low :-) Anyway, I've laid out the issues I can think of off-hand above. I also noted above that I need to do other work today, so looking in detail at the proposals and AI12-0112-1 had better wait lest the Jan 15th rush not get processed. **************************************************************** From: Tucker Taft Sent: Sunday, February 18, 2018 5:29 PM ... >>I am willing to spend more time on 0079. I did not realize >>that the above was your concern. Perhaps we can handle this >>offline. If you can let me know what you feel you need to >>annotate the containers, I'll try to finalize that part of >>the wording. > >I'm not completely sure at this stage, as I've never felt the proposal was >solid enough to proceed. Obviously, the containers are generic, so all of >the rules involving combinations and reflecting the Globals of the actuals >in generic specs need to be figured out in detail. > >This is rather complex for Nonblocking (which is worked out), and Global is >10 times harder, so the lack of work in that area is concerning. I am not sure what you mean here. We have the 'Global attribute and permit the use of "&" to combine global specifications. What more do you think we need? >>For me it just seemed like there was a general >>fine tuning needed, but apparently you feel there are still >>some big issues, at least when it comes to annotating the >>libraries. So if you can give me a clearer idea of what you >>need, I'll focus on that. >The other issue for the libraries is clearly what to do about >implementation-defined "helper" packages. We surely have to allow >implementations to have such packages, and they might in some circumstances >have globals in them. It would seem nasty to ban that (other than in Pure >packages, of course). And we surely can't name any such packages in the >Standard! Private descendants are considered part of the package body from the point of "Global => (in out => P private)". Do we need more than that as a way to support "helper" packages? >There's also an issue that is not specific to Global, but matters a lot. >Since attribute prefixes have to be unambiguous without context, most of the >names of generic formals can't be directly used in an attribute. That means >that they have to be renamed to a unique name so that they can be used. For >instance, for Vectors: > >generic > type Index_Type is range <>; > type Element_Type is private; > with function "=" (Left, Right : Element_Type) return Boolean is <>; >package Ada.Containers.Vectors > with Preelaborate, Remote_Types, > Nonblocking => Equal_Element'Nonblocking, > Global => Equal_Element'Global and and is > > function Equal_Element (Left, Right : Element_Type) return Boolean renames "="; > > ... > >The aspects Nonblocking and Global give the default declaration of the >aspects for the contents, and we surely don't want to repeat them on all >(approx) 70 subprograms. > >However, we've never defined what the freezing point of a package >declaration is, so the place where these aspects are evaluated is not >well-defined. So I don't even know if this formulation is legal. And if it >isn't legal, is there any alternative that IS legal that doesn't require >repeating Nonblocking and Global aspects 70 times. Fine, but that seems to be a separate AI. I think it is safe to assume that this can be fixed to work the way we want it to for Global and Nonblocking, so this shouldn't interfere with you making progress. >The third issue is about the actual definition of "synchronized". The >purpose of this setting is to mark task-safe code that still uses global >variables. It's pretty clear that 100% elimination of data races is >impossible if any globals are involved (as soon as there is more than one >global, data locks are impossible to avoid with static rules). ... There are "data races" and "race conditions." Frequently these are treated as synonyms, but if there is a distinction, it is that "A := A + 1" does not involve a "data race" if A is atomic, but it is clearly a race condition. I don't think we have a prayer of preventing these kinds of race conditions. Certainly a friendly compiler could recognize some of these simple patterns, and provide a warning, but I don't see that we can hope for much more than that. Again, I think this is a separate AI, or simply out of scope for Ada standardization. So I don't find any of the above issues particularly relevant to AI12-0079 and its use in annotating language-defined packages. *However*, I do think we have a significant issue with respect to access types. We really want a way to say that the side-effects are limited to heap objects "reachable" from a given parameter. Saying that a subprogram updates something designated by a given access type is pretty useless. So I plan to spend some time thinking about this problem of access types, especially in the context of container-like packages that clearly use access types behind the scenes. But I don't see that there is much more needed to address the issues you identify above. If you don't agree, please advise! **************************************************************** From: Randy Brukardt Sent: Monday, February 19, 2018 9:45 PM > I am not sure what you mean here. We have the 'Global attribute and permit > the use of "&" to combine global specifications. What more do you think we > need? The assume-the-best and assume-the-worst rules for using the 'Nonblocking attribute inside a generic turned out to be pretty complex in order to be usable. And those are just "on-off" type rules! I'd like to have at least some feeling that we can make the rules for 'Global attribute inside of a generic usable before using them everywhere and assuming that implementers can figure it out. I suppose this is more of a concern for the actual proposal rather that need in the spec of the containers. But if no one can write a legal body for the containers, that would be bad... ... >> The other issue for the libraries is clearly what to do about >> implementation-defined "helper" packages. We surely have to allow >> implementations to have such packages, and they might in some circumstances >> have globals in them. It would seem nasty to ban that (other than in Pure >> packages, of course). And we surely can't name any such packages in the >> Standard! > Private descendants are considered part of the package body from the point > of "Global => (in out => P private)". Do we need more than that as a way > to support "helper" packages? Traditionally, helper packages are in some implementation-defined subsystem. The obvious example is IO. In Janus/Ada, we have the helper package defined as System.Basic_IO. All of the language-defined packages are defined in terms of it. (It has a bit of state to support Standard-in/Standard-out.) I believe GNAT has some such package in the GNAT subsystem. For containers, I suppose a global non-generic helper could be a private child of Ada.Containers. (There sadly isn't an Ada.IO subsystem.) But that *still* isn't a "private descendant" of the generic Ada.Containers.Vectors! And there is no way to have a non-generic private descendant of a generic package. [If I was going to use a helper at all, it would definitely be non-generic.] I vaguely remember that one option discussed was just to punt and let implementers put anything that they wanted as additional dependencies into Global for impure packages. That would seem to work, especially if we allowed mentioning packages only referenced from a private with in Global aspects. (Putting "private" into the context clause would make it clear that the only reason for mentioning these packages is so that the dependencies can be visible for checks. I believe that we already allow adding "private withs" as those are semantically transparent for the purposes of the language-defined specification.) ... >> However, we've never defined what the freezing point of a package >> declaration is, so the place where these aspects are evaluated is not >> well-defined. So I don't even know if this formulation is legal. And if it >> isn't legal, is there any alternative that IS legal that doesn't require >> repeating Nonblocking and Global aspects 70 times. > > Fine, but that seems to be a separate AI. I think it is safe to assume > that this can be fixed to work the way we want it to for Global and > Nonblocking, so this shouldn't interfere with you making progress. The reassurance that it can be made to work is important, at least for my psyche. I don't want to do this overall and then have to start over because of a bad assumption at the start... >> The third issue is about the actual definition of "synchronized". The >> purpose of this setting is to mark task-safe code that still uses global >> variables. It's pretty clear that 100% elimination of data races is >> impossible if any globals are involved (as soon as there is more than one >> global, data locks are impossible to avoid with static rules). ... > There are "data races" and "race conditions." Frequently these are treated > as synonyms, but if there is a distinction, it is that "A := A + 1" does not > involve a "data race" if A is atomic, but it is clearly a race condition. This seems like hair-splitting. Either way it doesn't work, but only intermittently. > I don't think we have a prayer of preventing these kinds of race conditions. > Certainly a friendly compiler could recognize some of these simple patterns, > and provide a warning, but I don't see that we can hope for much more than > that. Again, I think this is a separate AI, or simply out of scope for Ada > standardization. I don't see any good reason to allow writes to atomic objects to be considered safe unless they are writing a static value, or are using one of a atomic update operations that Bob doesn't think we need to define. ;-) Anything else is a guaranteed race condition, so why allow it in the first place? Most of these sorts of operations should be wrapped into protected objects in order to be clearly safe. (And even those can be abused, and probably there ought to be a check for dubious cases as when the same protected object occurs more than once in a single expression, but that's more like a warning.) Recall how I'd expect to use the parallelism features (because it's the way I do all of my Ada programming these days): add parallel to an appropriate loop and let the compiler tell me what needs to be changed. Ada compilers are ten times better at finding issues than I would be -- the big problem I have with the current tasking model is that it leaves the programmer completely on your own. I realize that finding every problem statically is probably impractical, but I don't want to leave anything obvious get through. (If one remembers that one can only have a single global object in order to be safe, then a proper set of rules should make it hard to have any undetected problems in that case. More than one global object is a lost cause; I'd just ban parallelism in that case, but I don't know how to even do that. :-) > So I don't find any of the above issues particularly relevant to AI12-0079 > and its use in annotating language-defined packages. *However*, I do think > we have a significant issue with respect to access types. We really want a > way to say that the side-effects are limited to heap objects "reachable" > from a given parameter. Saying that a subprogram updates something designated > by a given access type is pretty useless. I don't think there is any other practical option. This just demonstrates why one should never use access types in visible interfaces. (I think I've been saying that for 20 years. ;-) > So I plan to spend some time thinking about this problem of access types, > especially in the context of container-like packages that clearly use > access types behind the scenes. But I don't see that there is much more > needed to address the issues you identify above. If you don't agree, > please advise! Luckily, we previously agreed to add reading operations that pass the container. (Which also allows sensible prefix notation using the container object for reading.) The preconditions then disallow any cases where we are talking about the implicit container. So I think we're OK reasoning just about cursor referencing something in the "current" container object, Which doesn't need to be mentioned in Global. The old reading operations are a lost cause, but that's OK: don't use them if you care about the Global reference. BTW, do we have an annotation for "any object of a type"? That's what those need (it's not designated by some access type, since there is no visible access definition, and I would be disgusted to have to declare such a type just for use in Global references). Not that I would mind if you have some better definition, I'm sure it would be useful somewhere. **************************************************************** From: Tucker Taft Sent: Monday, February 19, 2018 10:25 PM > I don't see any good reason to allow writes to atomic objects to be > considered safe unless they are writing a static value, or are using one of > a atomic update operations that Bob doesn't think we need to define. ;-) ... This is an interesting point of view, but I still think it is completely unrelated to the Global annotation AI. I still think this is more of a "warning" situation than an error. I don't think we should be in the business of disallowing use of atomic variables to provide synchronization, but I could see a compiler warning you about certain uses. >>... *However*, I do think >> we have a significant issue with respect to access types. We really >> want a way to say that the side-effects are limited to heap objects >> "reachable" from a given parameter. Saying that a subprogram updates >> something designated by a given access type is pretty useless. > >I don't think there is any other practical option. This just demonstrates >why one should never use access types in visible interfaces. (I think I've >been saying that for 20 years. ;-) I am not talking about using access types in a visible interface, but rather trying to define what a given interface does in terms of its reading and writing of heap-resident data, in a way that it can be checked by the compiler. In any case, I have some new ideas how to do this, using a 'Reachable attribute. I'll write this up shortly. **************************************************************** From: Randy Brukardt Sent: Monday, February 19, 2018 11:49 PM >> I don't see any good reason to allow writes to atomic objects to be >> considered safe unless they are writing a static value, or are using one of >> a atomic update operations that Bob doesn't think we need to define. ;-) ... > > This is an interesting point of view, but I still think it is completely > unrelated to the Global annotation AI. I still think this is more of a > "warning" situation than an error. I don't think we should be in the > business of disallowing use of atomic variables to provide synchronization, > but I could see a compiler warning you about certain uses. We *should* be in the business of disallowing unsafe code by default (for the purpose of parallel execution), and that is what Global does here. Anything should be fine in the Global => all case, because that doesn't promise any safety. Atomic variables are only usable for synchronization with xtreme care, and "extreme care" runs counter to the purpose of having safety rules in the first place. (You can use any sort of global object with "extreme care", after all. :-) But I agree this should be a "suppressible error" (indeed, one could argue that all of the checks for a parallel loop, etc. should be suppressible). Of course, that would imply that Bob or someone decides to actually progress that AI... ... > I am not talking about using access types in a visible interface, but rather > trying to define what a given interface does in terms of its reading and > writing of heap-resident data, in a way that it can be checked by the > compiler. OIC. You're worried that the static rules would pretty much have to disallow doing anything heap-related in the body of a subprogram, since we don't know that the heap objects "belong" to the parameter and won't be shared with other objects. (Such heap objects shouldn't appear in Global at all -- the part I was worrying about -- since they are of types that are likely private/body and designate types only defined in the private part or body, and as such mentioning them is nonsense.) Having to include the "heap" in Global in such a case would make almost everything Global => all, which isn't useful. > In any case, I have some new ideas how to do this, using a 'Reachable > attribute. I'll write this up shortly. Sounds good. Hope it isn't too complicated. *************************************************************** From: Tucker Taft Sent: Saturday, February 24, 2018 9:01 PM > ... > > However, we've never defined what the freezing point of a package > declaration is, so the place where these aspects are evaluated is not > well-defined. So I don't even know if this formulation is legal. And > if it isn't legal, is there any alternative that IS legal that doesn't > require repeating Nonblocking and Global aspects 70 times. Below are two paragraphs I am planning to add to the Global aspect AI. Do these address this issue adequately? ---------- Modify 13.1.1(11/3): The usage names in an aspect_definition [Redundant: are not resolved at the point of the associated declaration, but rather] are resolved at the end of the immediately enclosing declaration list{, or in the case of the declaration of a library unit, at the end of the visible part of the entity}. Modify 13.14(3/5): The end of a declarative_part, protected_body, or a declaration of a library package or generic library package, causes freezing of each entity and profile declared within it{, as well as the entity itself in the case of the declaration of a library unit}. **************************************************************** From: Randy Brukardt Sent: Monday, February 26, 2018 9:34 PM > Below are two paragraphs I am planning to add to the Global aspect AI. > Do these address this issue adequately? So long as they don't stomp on the rules for categorization aspects, we should be fine. > ---------- > > Modify 13.1.1(11/3): > > The usage names in an aspect_definition [Redundant: are not resolved > at the point of the associated declaration, but rather] are resolved > at the end of the immediately enclosing declaration list{, or in the > case of the declaration of a library unit, at the end of the visible > part of the entity}. Luckily, 13.1.1(32/4) is a "Notwithstanding" rule, so what we say for the "normal" case doesn't matter. In particular, 13.1.1(32/4) says: Notwithstanding what this International Standard says elsewhere, the expression of an aspect that can be specified by a library unit pragma is resolved and evaluated at the point where it occurs in the aspect_specification[, rather than the first freezing point of the associated package]. The redundant remark might be a bit confusing (depending on whether the above paragraph or the below paragraph is read), but it seems OK. Or we could change it to "rather than the end of the visible part of the entity". Humm: do library units that are subprograms or renames have a visible part?? Humm part 2: the index points us to a sentence (in 8.2(5)) that is described as "redundant" for the definition of visible part. Anyway, that implies that a subprogram profile is the visible part; for a renames, it appears that there is no visible part. So, let's rephrase: does the visible part of a subprogram or rename have a well-defined end? > Modify 13.14(3/5): > > The end of a declarative_part, protected_body, or a declaration of a > library package or generic library package, causes freezing of each > entity and profile declared within it{, as well as the entity itself > in the case of the declaration of a library unit}. Looks OK to me. *************************************************************** From: Tucker Taft Sent: Monday, February 26, 2018 10:28 PM > Humm: do library units that are subprograms or renames have a visible part?? Yes they do. Look in RM 8.2 > Humm part 2: the index points us to a sentence (in 8.2(5)) that is > described as "redundant" for the definition of visible part. Anyway, > that implies that a subprogram profile is the visible part; for a > renames, it appears that there is no visible part. The wording might not be precise in its use of "entity" vs. "declaration," but I think it is clear the intent that the profile in a subprogram renaming is the visible part. > So, let's rephrase: does the visible part of a subprogram or rename > have a well-defined end? It seems like it ends at the end of the profile. Where else would it end? >> Modify 13.14(3/5): >> >> The end of a declarative_part, protected_body, or a declaration of a >> library package or generic library package, causes freezing of each >> entity and profile declared within it{, as well as the entity itself >> in the case of the declaration of a library unit}. > > Looks OK to me. Good. *************************************************************** From: Randy Brukardt Sent: Thursday, March 1, 2018 1:50 AM > I am not talking about using access types in a visible interface, but > rather trying to define what a given interface does in terms of its > reading and writing of heap-resident data, in a way that it can be > checked by the compiler. > > In any case, I have some new ideas how to do this, using a 'Reachable > attribute. I'll write this up shortly. A thought: for the purposes of the containers, we only need to worry about access types declared in private part and/or body of the container package. (These are going to have to depend on the generic formal parameters, so declaring them outside of the generic isn't going to work.) As such, we don't want to have to mention them in the Global aspects anyway. For such hidden access types, they are fine so long as there aren't any conversions to/from types outside of the package (that would be the only way for the access values to point somewhere else). Perhaps we could define an aspect to use on the access types to declare this (with checks on conversions), in which case the storage pool would be presumed to be part of the package body's state (even if it really a global object). (I suppose 'Access of outside objects would also have to be dealt with.) In such a case, a dereference of such a type would also be considered part of the package body's state, which seems to be all we need to make the code legal. Such an aspect would be enough for the containers. It probably would work for lots of other ADTs as well. Thoughts??? *************************************************************** From: Tucker Taft Sent: Thursday, March 1, 2018 4:29 PM Here is a last-minute update to the Global AI. [This is version /06 of the AI - ED.] *************************************************************** From: Randy Brukardt Sent: Thursday, March 1, 2018 6:56 PM > Here is a last-minute update to the Global AI. A couple of questions based on my work on AI12-0112-1, so far: (1) For reading routines that take only a cursor, I had to use a Global aspect to reflect the fact that there is an implicit reference to an (unknown) container. For example, for Element, I have: function Element (Position : Cursor) return Element_Type with Pre => (if Position = No_Element then raise Constraint_Error), Nonblocking => True, Global => Vectors'Global & in access Vector; I intend "access Vector" here to represent any possible Vector object, aliased or not (since, as a tagged type, the implementation of Vectors can always take 'Access of a Vector object). With the "(aliased)" in parens, it's not clear to me whether this is true or not. The wording needs to be clarified a bit. (2) The first part of the above Global aspect is to reuse the "standard" Global for the entire package. Part of that is implementation-defined, so we don't want to duplicate it all over the place. I used "unit'Global" for this purpose, but that is a generic package and the Global attribute isn't defined for that. Not sure if that should be defined or if there is a better way to do this. (One could, I suppose, write the whole thing out once and then copy it for other similar routines -- but that seems like a maintance hazard.) (3) I see the new reachable attribute, but I can't figure out how it should work in the containers case. For the "normal" and indefinite containers (bounded containers are pure and don't have this issue), there are going to be some local access types, most likely using the standard storage pool. That pool is completely global, and the access types (in theory, at least) could have values converted in or out to other similar access types. [In practice that can't happen for these packages, since the types depend on the generic formal parameters, but we can hardly write rules assuming that.] These access types are declared and used only in the package body (or private part) and used to implement the container object. The reachable attribute can't describe them as they are of types not visible to the caller. Ideally, this usage would not require any global beyond specifying that the package body has state. But in order for that to be safe (in general), one needs to be able ensure that there is no "leakage" of access values or designated objects. I don't see anything in the rules that would have this effect; so far as I can tell, the rules prevent (or should prevent) doing any dereferences at all unless the standard storage pool (only describible as "all" or by "access ") is covered by the routines Global access. One could avoid this by declaring a storage pool inside of the container package body, but that couldn't depend on the standard storage pool, and thus it would be a huge amount of work to effectively limit the amount of memory the container should use. What is the intent here?? *************************************************************** From: Randy Brukardt Sent: Thursday, March 1, 2018 8:24 PM > Here is a last-minute update to the Global AI. FYI, your files are still coming with as line endings (note the extra ); this makes it impossible to compare them (it doesn't match typical line endings) and makes a mess if I cut-and-paste part of it. (At least the people who send Unix files with just are readily obvious as those don't display properly in Notepad; I then know to clean them before using.) *************************************************************** From: Tucker Taft Sent: Friday, March 9, 2018 8:06 AM This version [He's talking about version /06 - ED] included a paragraph about when the declaration of a library unit is frozen: Modify 13.14(3/5): The end of a declarative_part, protected_body, or a declaration of a library package or generic library package, causes freezing of each entity and profile declared within it{, as well as the entity itself in the case of the declaration of a library unit}. It did not cover (generic) library subprograms, but we probably care about those as well. For them, we may want to say the end of the *compilation* unit, so as to include any of the "trailing" pragmas (such as pragma Inline). Trailing pragmas are clearly part of the compilation unit, whereas it is a bit less clear whether they are part of the declaration. Hence, to define when the declaration of a library subprogram is frozen, we could leave the above paragraph as is, and add: The end of a compilation unit containing the declaration of a library unit (including any pragmas that apply to it) causes freezing of the library unit. Where the part about the pragmas is probably redundant, but perhaps doesn't hurt to include. ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 8:21 AM [This is version /07 of the AI - Editor.] Here is a very minor update to the Global Annotations AI. I couldn't find any specific things to fix from reading the minutes from our last discussion of the AI. The only substantive thing I did was modify 'Reachable to take into account that a pool-specific access type can only point to things in its associated collection, meaning that if X and Y are of two different pool-specific access types, then X'Reachable does *not* include Y.all. Randy, did I miss something? ************************************************************** From: Randy Brukardt Sent: Thursday, October 18, 2018 2:07 PM > Randy, did I miss something? I remember discussing with you the need to have Global on types reflect the default initialization + Initialize/Adjust/Finalize. And, in particular, for 'Global on generic formal types to have this meaning. Specifically, in the containers, I have Element_Type'Global in the Global for routines like Insert and Delete in order to capture the idea that those routines might create or destroy an object with an Element_Type part. For example, we certainly want Finalize to be able to use some global data (at a minimum for compatibility), but that of course has to be reflected in the Global for routines that might call it. I'll go check my mail on this topic and forward any that seems appropriate (there might have been other issues as well). ************************************************************** From: Randy Brukardt Sent: Thursday, October 18, 2018 2:31 PM ... > I'll go check my mail on this topic and forward any that seems > appropriate (there might have been other issues as well). The only thing I found in mail was this, in March, after the last AI update: Me: >>Aside: I didn't see any definition of what T'Global is for scalar >>types (should be null, I think). This matters in two places: the >>elementary completion of a private type, and passing as a generic >>formal private type. >>In both of those, T'Global is legal on a type that ultimately is not a >>composite type. You: >Good question. I haven't thought about it. Me, now: Probably you should. :-) Note that this mail suggests that you had already dealt with the T'Global issue; that's the problem with relying on memory. ---- I couldn't find anything else, and I didn't want to spend all day looking. ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 3:01 PM OK, here is yet another minor update, where I indicate that the Global aspect for an elementary type is null. [This is version /08 of the AI - Editor.] ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 3:20 PM Other than for an access-to-subprogram type, that is. ************************************************************** From: Randy Brukardt Sent: Thursday, October 18, 2018 7:01 PM ... > The only > substantive thing I did was modify 'Reachable to take into account > that a pool-specific access type can only point to things in its > associated collection, meaning that if X and Y are of two different > pool-specific access types, then X'Reachable does *not* include Y.all. I keep thinking that this AI is so complicated, and 'Reachable doesn't seem necessary for the containers and similar ADTs, if it wouldn't be better to split that concept out into its own AI. We did something like that for the parallel blocks and loops, and that seemed to allow all parts of those split AIs to progress more quickly. In this case, it's even more true since the 'Reachable stuff depends in part on AI12-0240-n, for which we haven't really decided anything yet. And at least AI12-0240-2 includes rules that make it possible to essentially ignore access types used to implement an ADT. I understand the basic concept of the AI pretty well, but the reachable stuff adds a bunch more complication that adds some confusion to the topics that are pretty much tough to understand as it is. Just a thought. (Too late for the agenda, of course.) ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 7:36 PM Your suggestion makes sense. ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 7:54 PM Though without X'Reachable or equivalent, an abstraction that uses a private type with a component of an access type, has no way of describing its global effects other than via "IN OUT ALL." Perhaps we keep X'Reachable, but don't mention the Ownership thing. ************************************************************** From: Randy Brukardt Sent: Thursday, October 18, 2018 8:22 PM 'Reachable doesn't help in that case, assuming the usual case that the access type is itself declared in the private part. Making it visible just to write Global specs doesn't make much sense, especially if the designated type is also in the private part or even are a Taft-amendment type. (Consider a container node.) What does help is the ownership AI (at least my version) that allows such access types to be declared such that the designated objects effectively are part of the private object (which is typically a parameter) for the purposes of Global aspects, regardless of where they actually live. I realize that I'm taking a relatively narrow view here, but it's certain that we have to get this stuff (both AIs 79 and 240) finished so the containers can use them, lest the parallel checking that we've defined turns out to be effectively useless. And many user-defined abstract data types are organized much like the containers (most of mine are, for instance), so many real problems will be fine. I'm less concerned about other program organizations, mainly because we don't have either the time nor the examples to properly evaluate such usage. ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 8:45 PM >> Though without X'Reachable or equivalent, an abstraction that uses a >> private type with a component of an access type, has no way of >> describing its global effects other than via "IN OUT ALL." Perhaps >> we keep X'Reachable, but don't mention the Ownership thing. > > 'Reachable doesn't help in that case, assuming the usual case that the > access type is itself declared in the private part. Making it visible > just to write Global specs doesn't make much sense, especially if the > designated type is also in the private part or even are a Taft-amendment > type. (Consider a container node.) I am not sure you understand what "X" refers to. It is the name of a parameter, typically. X'Reachable then allows the body to update objects reachable from X via following access values. It effectively is equivalent to Global => (in out access T1, in out access T2, ...) where T1, T2, etc. are the access types that are used for subcomponents of the object X (or objects reachable from X), even if X is an object of a private type. So the intent was that X'Reachable was designed exactly for this case of a private type with "hidden" components of non-visible access types. > What does help is the ownership AI (at least my version) that allows > such access types to be declared such that the designated objects > effectively are part of the private object (which is typically a > parameter) for the purposes of Global aspects, regardless of where they > actually live. I certainly agree that ownership helps, but at least with X'Reachable, you can narrow down the effects to aliased objects of a type that can be reached from X. Without something like X'Reachable, and with the access types not externally visible, you will have to say "Global => in out all" if you want the body of the subprogram to compile without complaints about violating its Global annotation. ************************************************************** From: Randy Brukardt Sent: Thursday, October 18, 2018 9:19 PM > I am not sure you understand what "X" refers to. No, I don't; I asked for an example how it would be used in an ADT like the containers and got crickets. I like the engaged Tucker that's here at the moment better. I suppose that only lasts until Tuesday afternoon. :-) > It is the > name of a parameter, typically. X'Reachable then allows the body to > update objects reachable from X via following access values. It > effectively is equivalent to Global => (in out access T1, in out > access T2, ...) where T1, T2, etc. are the access types that are used > for subcomponents of the object X (or objects reachable from X), even > if X is an object of a private type. So the intent was that > X'Reachable was designed exactly for this case of a private type with > "hidden" components of non-visible access types. I don't quite see how that would provide any useful information, as X'Reachable as described here could, in general, reach almost anything aliased. How would the compiler (without peeking into the private part/body) determine that a call of a subprogram with X'Reachable does not conflict with an arbitrary aliased object or storage pool? Specifically, if you have: A : aliased Natural; procedure Foo (X : Priv) with Global => in out X'Reachable; procedure Bar (Val : in out Natural) with Global => in out A; how would the compiler determine that these do or don't overlap? It seemed that they would have to overlap, meaning that it would be only a tiny bit better than "all" (in that any non-aliased, non-by-reference, non-pool global objects couldn't be reached). Seems barely worth it. (And ownership inside of Foo's package doesn't really help, either, because you don't know that outside.) The proposal I made in Ai12-0240-2 allows Foo to use Global => null, which of course allows much more overlap (meaning more safe parallelism). > > What does help is the ownership AI (at least my version) that allows > > such access types to be declared such that the designated objects > > effectively are part of the private object (which is typically a > > parameter) for the purposes of Global aspects, regardless > of where they actually live. > > I certainly agree that ownership helps, but at least with X'Reachable, > you can narrow down the effects to aliased objects of a type that can > be reached from X. Without something like X'Reachable, and with the > access types not externally visible, you will have to say "Global => > in out all" if you want the body of the subprogram to compile without > complaints about violating its Global annotation. Right, but as noted above, that seems to be essentially the same thing unless you are requiring privacy breakage. Perhaps I'm still missing something. (But that fact that I'm having such a hard time groking this idea is one of the reasons for suggesting handling it separately.) ************************************************************** From: Tucker Taft Sent: Thursday, October 18, 2018 10:29 PM ... >No, I don't; I asked for an example how it would be used in an ADT like the >containers and got crickets. I like the engaged Tucker that's here at the >moment better. I suppose that only lasts until Tuesday afternoon. :-) I did include an example in the AI: generic type T is private; with function Hash(X : T) return Hash_Code; package Sets is type Set(Capacity : Positive) is private with Global => T'Global; procedure Insert(S : in out Set; X : T) with Global => in out S'Reachable & Hash'Global & T'Global, Post => S'Reachable(X'Copy'Reachable); ... end Sets; Operations within the Sets package reference global variables only indirectly, as a result of using the generic formal parameters T and Hash, and as a result of dereferencing access objects within the representation of a Set. The default initialization, adjustment, and finalization of a Set indirectly uses the corresponding operations of T. Insert updates the objects reachable from S, as well as those updated by Hash and T's assignment operation, and has a post-condition that indicates it makes the objects reachable from X'Copy reachable from S (in addition to those originally reachable from S). X'Copy is used here to indicate that we are not using X directly, but rather copying X into the data structure that represents S. --- ... >I don't quite see how that would provide any useful information, as >X'Reachable as described here could, in general, reach almost anything >aliased. How would the compiler (without peeking into the private part/body) >determine that a call of a subprogram with X'Reachable does not conflict >with an arbitrary aliased object or storage pool? I guess I was more focused on enforcing the restriction inside the subprogram with the Global annotation. You are right that deciding whether two calls might update overlapping storage is also an important question, as far as parallelism checks, and I agree that X'Reachable doesn't provide much in the absence of Ownership. The other part of the X'Reachable thing was to have X'Reachable defined as part of the postcondition. >Specifically, if you have: > A : aliased Natural; > > procedure Foo (X : Priv) > with Global => in out X'Reachable; > > procedure Bar (Val : in out Natural) > with Global => in out A; If we don't have a postcondition using X'Reachable(...), I agree there is no way to know that Foo doesn't put a pointer to A into X and then update it. If you did have a postcondition using X'Reachable(...) (see "Set" example above), then it might be more reasonable for the caller to know what was added to the set of things reachable by X, and if it didn't include A, we might be OK. But I agree there is a lot of wishful thinking and hand waving going on here! >how would the compiler determine that these do or don't overlap? It seemed >that they would have to overlap, meaning that it would be only a tiny bit >better than "all" (in that any non-aliased, non-by-reference, non-pool >global objects couldn't be reached). Seems barely worth it. (And ownership >inside of Foo's package doesn't really help, either, because you don't know >that outside.) > >The proposal I made in Ai12-0240-2 allows Foo to use Global => null, which >of course allows much more overlap (meaning more safe parallelism). Agreed, that is the goal -- to assume that in the presence of ownership, objects reachable only through "owning" pointers are treated like subcomponents, and need not be mentioned in the Global annotation at all. ... >Right, but as noted above, that seems to be essentially the same thing >unless you are requiring privacy breakage. Perhaps I'm still missing >something. (But that fact that I'm having such a hard time groking this idea >is one of the reasons for suggesting handling it separately.) Fair enough -- it is clear that without some form of ownership, any non-visible use of access types will cause the Global annotation to end up at "in out all." So I agree we should drop the 'Reachable idea, and push for some kind of ownership AI, with the important rule being the one mentioned above, namely that objects reachable only through owning pointers are treated like subcomponents rather than global objects, as far as any global annotation is concerned (as well as far as parameter modes are concerned). Another important rule is that when an owning pointer is a component, the object designated by it is read only if the pointer is a component of a read-only object, even though the owning pointer is probably of an access-to-variable type. This rule is part of AI12-0240-1 (and would certainly be part of the sketchy 0240-3 if it were fleshed out). I don't remember whether you had it in your 0240-2 version. ************************************************************** From: Randy Brukardt Sent: Friday, October 19, 2018 12:39 AM >Fair enough -- it is clear that without some form of ownership, any >non-visible use of access types will cause the Global annotation to end >up at "in out all." So I agree we should drop the 'Reachable idea, and >push for some kind of ownership AI, with the important rule being the >one mentioned above, namely that objects reachable only through owning >pointers are treated like subcomponents rather than global objects, as >far as any global annotation is concerned (as well as far as parameter >modes are concerned). Agreed. Because of cursors, we also need some sort of backdoor unsafe copies of owned access values. (Luckily, the design of the containers prevent doing anything bad with such values, assuming of course that the container is correctly implemented and the checks aren't suppressed -- admittedly, some substantial assumptions.) >Another important rule is that when an owning pointer is a component, >the object designated by it is read only if the pointer is a component >of a read-only object, even though the owning pointer is probably of an >access-to-variable type. This rule is part of AI12-0240-1 (and would >certainly be part of the sketchy 0240-3 if it were fleshed out). I >don't remember whether you had it in your 0240-2 version. No, because it would break 50% of my abstractions. And this ties into the question that I tried to get you to answer about AI12-0240-1 that you never did. Not all constant objects are created equal! Ada specifically allows certain constant objects (those with parts of controlled types and those that are immutably limited) to change without causing erroneousness. (Remember the big fight we had with Erhard about that??) Those objects must be treated as variables for the purposes of Global *and* can be the only constants used as the source of an owned access that is going to be assigned to an owned object. (Since such assignment requires modification of the source.) To take a specific example, a random number generator in Janus/Ada is implemented as a controlled object with a pointer to the actual generator data. (It's controlled only so that it can clean up the allocated data part.) The designated data object is a perfect candidate to be an owned access type, since it really is part of the owning object -- it's separate only to get modification for the contents. Indeed, if that was done, one wouldn't even need to declare the owning object as controlled (although it effectively would be). If one insisted on the rule you give above, then this structure cannot use an owned pointer (given that the generator is an "in" parameter). That seems silly, as there's nothing global being used either way. I could live with having such a rule that applied if the owner was an object of a "really constant" type (I don't write many of those anymore), but otherwise, you're just making trouble for existing code. Redesigning the spec of Ada.Numerics.Random isn't happening, and that's probably true for lots of specs out there. That doesn't mean that programmers won't want to add Global and Nonblocking and the rest to get safe parallelism and the like, and that likely means using Ownership. ************************************************************** From: Tucker Taft Sent: Friday, October 19, 2018 10:10 AM If parameter modes lie, it certainly makes it hard to know what is the net effect of making a call, especially if there are hidden pointers providing read/write access to the object being passed as an IN parameter. Now that we allow "in out" for functions, why not own up to that and change the parameter mode for things like function Random? I suppose we could always assume the worst for objects of a limited private (or inherently limited) type, and perhaps that is the right answer. Even an IN parameter of a limited private type must be assumed to be updated as a side-effect of any call. Eventually we will want a way to be more explicit about what is referenced and what is modified, both to handle these weird lying parameter modes, and to be more precise as far as which components are updated (I suppose the "stable properties" might be of some help here for private types). So I suppose the bottom line for a subprogram with an IN parameter of a limited type, is that the parameter might be updated internally. That means that doing two calls in parallel on a subprogram with IN parameters of a limited type will be considered a potential data race, unless we invent more annotations. And this means that the "transitivity" of read-only access from a composite object to its owning access components would not apply to objects of a limited type. But I think it should definitely apply to composite types that are non limited, or else parameter modes are useless for the purposes of distinguishing read-only from read/write. ************************************************************** From: Randy Brukardt Sent: Friday, October 19, 2018 4:26 PM > If parameter modes lie, it certainly makes it hard to know what is the > net effect of making a call, especially if there are hidden pointers > providing read/write access to the object being passed as an IN > parameter. Now that we allow "in out" > for functions, why not own up to that and change the parameter mode > for things like function Random? Changing the mode breaks calls, because functions, aggregates, and literals cannot be passed to such things. (Functions usually being the most common.) Not sure if that would be a real problem for Random (it sure would make the implementation cheaper), but there is definitely a compatibility concern. > I suppose we could always assume the worst for objects of a limited > private (or inherently limited) type, and perhaps that is the right > answer. Even an IN parameter of a limited private type must be > assumed to be updated as a side-effect of any call. Eventually we > will want a way to be more explicit about what is referenced and what > is modified, both to handle these weird lying parameter modes, and to > be more precise as far as which components are updated (I suppose the > "stable properties" might be of some help here for private types). Yes, since a lot of people have structured their packages similarly to the Ada I/O designs, and those use "in" and "in out" for a vastly different meaning than "read-only" and "read-write". Claw would be a lost cause with such a rule, but that's probably irrelevant, since (A) Claw is already task-safe so long as the Claw objects are disjoint (and we use locking when there are internal conflicts between different objects); (B) no one is going to want to write windows in parallel loop anyway. (There aren't many windows with thousands of distinct visual elements!) > So I suppose the bottom line for a subprogram with an IN parameter of > a limited type, is that the parameter might be updated internally. > That means that doing two calls in parallel on a subprogram with IN > parameters of a limited type will be considered a potential data race, > unless we invent more annotations. Might want to do that (more annotations) in the future, but we're pretty much out of time now. Our Claw design considers any operation on a specific claw object as a data race, and we don't try to prevent data races (those are considered erroneous). The parameter mode is not considered, which is essentially the same as the rules for language-defined units in the intro to Annex A. > And this means that the "transitivity" of read-only access from a > composite object to its owning access components would not apply to > objects of a limited type. But I think it should definitely apply to > composite types that are non limited, or else parameter modes are > useless for the purposes of distinguishing read-only from read/write. Sounds like a plan, but we still have to do something about the source of an owned pointer assignment being any object that is treated as constant by this rule (including everything that actually *is* constant). Since an owned pointer assignment is really a move, the source gets modified as well as the target. And we better not be modifying constants! **************************************************************