!standard 6.1.2(0) 20-01-13 AI12-0079-2/01 !class Amendment 19-10-05 !status work item 19-10-05 !status received 19-10-05 !priority High !difficulty Hard !subject Global-in and global-out annotations !summary Annotations are provided to describe the use of global objects by subprograms, entries, tasks, and protected units. !problem Here is the original problem statement: 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 troublesome, 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 implicit body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again). 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. --- Additional challenges addressed in this version of the AI: Simplify the proposal, at least in the core, so few if any Global aspects need to be specified by the typical user. Provide a way for more advanced users to impose on themselves stricter requirements should they so choose, but minimize the burden on programmers who want to use the new features of Ada 202X without worrying about Global specifications. Allow more sophisticated implementations, like the SPARK tools, to do additional analysis without requiring the user to specify explicitly all of the Global effects. In so far as possible, achieve compatibility with use of Global in existing SPARK code, so that no significant change in syntax or semantics is required for existing SPARK code to make it Ada 202X compatible. !proposal ** TBD. Similar to AI12-0079-1 and it's later fixups (AI12-0240-6 [overriding], AI12-0303-1, AI12-0310-1, and AI12-0334-2), but with some in the core and some in an annex. !wording Add the following section: 6.1.2 The Global and Global'Class Aspects For a subprogram, an entry, a named access-to-subprogram type, a task unit, a protected unit, or a library package or generic package, 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 ::= NULL | Unspecified | global_group_designator | global_mode global_designator | (global_aspect_element{, global_aspect_element}) | extended_global_aspect_definition -- see H.7 global_aspect_element ::= global_mode global_set | extended_global_aspect_element -- see H.7 global_mode ::= [ OVERRIDING ] basic_global_mode | implementation_defined_mode basic_global_mode ::= IN | IN OUT | OUT global_set ::= global_designator {, global_designator} global_designator ::= global_group_designator | global_name global_group_designator ::= ALL | SYNCHRONIZED | ALIASED global_name ::= /object_/name | /package_/name The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) global to an operation, task unit, or protected unit, that are potentially read or updated as part of the execution of the operation or of the execution of the body of the task or a protected operation of the protected unit. Constants of any type may also be mentioned in a Global aspect. If not specified or otherwise defined below, the aspect defaults to the Global aspect for the enclosing library unit if the entity is declared at library level, and to Unspecified otherwise. If not specified for a library unit, the aspect defaults to Global => NULL for a library unit that is declared Pure, and to Global => Unspecified otherwise. For a dispatching subprogram, 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 dispatching subprogram. Name Resolution Rules A global_name shall resolve to statically denote an object or a package (including a limited view of a package). 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 executing the operation(s) associated with the entity. The Global'Class aspect associated with a dispatching operation of type T represents a restriction on the Global aspect on a corresponding operation of any descendant of type T. The Global aspect for a callable entity defines the global variables that might be referenced as part of a call on the entity, including any assertion expressions that might be evaluated as part of the call, including preconditions, postconditions, predicates, and type invariants. The Global aspect for an access-to-subprogram object (or subtype) identifies the global variables that might be referenced when calling via the object (or any object of that subtype) including assertion expressions that apply. For a predefined operator of an elementary type, or the function representing an enumeration literal, the Global aspect is NULL. For a predefined operator of a composite type, the Global aspect of the operator defaults to that of the enclosing library unit (unless a Global aspect is specified for the type -- see H.7). The following is defined in terms of operations; the rules apply to all of the above kinds of entities. The global variables associated with any global_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 presence of the reserved word OVERRIDING indicates that the specification is overriding the mode of a formal parameter with another mode to reflect the overall effect of an invocation of the callable entity on the state associated with the corresponding actual parameter. An implementation-defined global_mode may be specified, which limits the use of the global objects to which it applies 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 global_aspect_definition. A global_set identifies a global variable set as follows: * ALL identifies the set of all global variables; * ALIASED identifies the set of all aliased variables, which includes any dereference of a value of an access-to-object type; * SYNCHRONIZED identifies the set of all synchronized variables (see 9.10), as well as variables of a composite type all of whose non-discriminant subcomponents are synchronized; * global_name{, global_name} identifies the union of the sets of variables identified by the global_names in the list, for the following forms of global_name: + /object_/name that is not associated with an OVERRIDING mode identifies the specified global variable (or constant); + /object_/name that is associated with an OVERRIDING mode identifies the variable parts associated with the specified formal parameter whose parameter mode is being overridden; + /package_/name identifies the set of all variables declared in the private part or body of the package or of a descendant of the package, or anywhere within a private descendant of the package. Legality Rules Within a global_aspect_definition, a given global_mode shall be specified at most once. Similarly, within a global_aspect_definition, a given entity shall be named at most once by a global_name. If an entity (other than a library package or generic package) has a Global aspect other than Unspecified or IN OUT ALL, then the execution of 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 possible Global effects of calls occurring during the execution of the operation, except for the following excluded calls: * calls to formal subprograms; * calls associated with operations on formal subtypes; * calls through formal objects of an access-to-subprogram type; * calls through access-to-subprogram parameters; * calls on operations with Global aspect Unspecified. The possible Global effects of these excluded calls (other than those that are Unspecified) are taken into account by the caller of the original operation, by presuming they occur at least once during its execution. For calls that are not excluded, the possible Global effects of the call are those permitted by the Global aspect of the associated entity, or by its Global'Class aspect if a dispatching call. AARM Ramification: For a predefined equality operator of a composite type, the possible Global effects includes those of the equality operations called by the operator (which might not be predefined and thus might have a different Global specification than the component types). For the purposes of these checks: * if a formal parameter P of a callable entity C is of an anonymous access-to-object type, no check against the Global aspect occurs within C for the dereference of P, but a check against the Global aspect applies at the point of call of C, presuming that P is dereferenced at least once and then read if of an access-to-constant type or updated if of an access-to-variable type; if the actual parameter is of the form X'Access (explicitly or implicitly), then at the point of call the presumed dereference of P is treated as a read or update of X; if the actual parameter A is of any other form, it is treated as a read or update of A.all; AARM Ramification: An access parameter ACCESS T is treated somewhat like a parameter specified as IN OUT T while access constant T is treated somewhat like IN T. There is no burden to mention the dereference of an access parameter in the Global aspect, as the effects of the dereference are presumed at the call site, just like the effects on "normal" parameters. * if a function returns an object of a type for which the Implicit_Dereference aspect is True (see 4.1.5), or an object of an anonymous access-to-object type, the Global aspect of the function shall reflect the effects of dereferencing the result of the function, if these are over and above reads or updates of parts of aliased formal parameters (or dereferences of access parameters) passed to the function. The effects to be reflected include reading the designated object, and updating the designated object in the case of an access-to-variable result or an Implicit_Dereference result with an access-to-variable access discriminant. A dereference (explicit or implicit) of a function_call on such a function is not further checked at the point of call against any Global or Global'Class aspects that apply to the caller. AARM Reason: The function is in a better position than the caller to enumerate the objects affected by dereferencing the result. Because the access discriminant is often of an anonymous type, there is no other place to declare these effects. In most cases, these effects will already be reflected in the aliased or access parameters passed to the function, so nothing need be added to the Global aspect for these. AARM Ramification: The last sentence is talking specifically about dereferences associated directly with a function_call. Other dereferences (such as those associated with a rename of a call, or an allocated result of a call) are not included — they have to be covered in the Global or Global'Class aspect in the normal way. * if an object of a pool-specific access-to-object type is dereferenced within an operation, and the dereference would violate the restrictions inherent in a Global aspect applicable to the operation, the dereference is nevertheless permitted under the following circumstances: + the pool-specific access type is declared within the private part or body of an enclosing package; + the dereferenced object: * is a part of a formal parameter of the operation whose mode (after any overriding) would allow the operation performed on the dereference; * is a part of a dereference of an object that satisfies these same circumstances; or * is a local object of the operation all of whose assignments are from an object that satisfies these same circumstances. AARM Ramification: This exemption of Global checks for dereferences of pool-specific access-to-object values is intended to allow the typical case where a private type uses multiple objects connected internally with access values to represent a single logical object. Here we allow the operation if the access value is reached from a formal parameter whose parameter mode would have allowed the operation. We give an implementation permission below to extend these exemptions to other dereferences based on additional analysis (such as that provided by newer versions of SPARK). If an implementation-defined global_mode applies to a given set of objects, 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, unless the aspect of that ancestor is Unspecified. 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), 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.1), or by using Unchecked_Conversion (see 13.9) or Address_to_Access_Conversions (see 13.7.2) to create local accesses to global objects. 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 can 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. Implementations may perform additional checks on calls to operations with an Unspecified Global aspect to ensure that they do not violate any limitations associated with the point of call. AARM Discussion: In this sense, Global => Unspecified is not permission to violate the caller's Global restrictions. It is rather that the implementor of the subprogram is presuming other means are being used to ensure safety. Note the No_Unspecified_Globals Restriction (H.4) to prevent the use of Unspecified with the Global aspect in a given partition. Implementations may provide additional (or fewer) exemptions to Global aspect checks on dereferences based on additional analysis of safety. Implementations may extend the syntax or semantics of the Global aspect in an implementation-defined manner. AARM Reason: This is intended to allow preexisting usages from SPARK 2014 to remain acceptable in conforming implementations, as well as to provide flexibility for future enhancements. Note the word "extend" in this permission; we expect that any aspect usage that conforms with the (other) rules of this clause will be accepted by any Ada implementation, regardless of any implementation-defined extensions. NOTES 7 For an example of the use of these aspects and attributes, see the Vector container definition in A.18.2. ---- Add after H.4 (23): No_Unspecified_Globals No library-level entity shall have a Global aspect of Unspecified, either explicitly or by default. No library-level entity shall have a Global'Class aspect of Unspecified, explicitly or by default, if it is used as part of a dispatching call. AARM Ramification: Global'Class need not be specified on an operation if there are no dispatching calls to the operation, or if all of the dispatching calls are covered by dispatching_operation_specifiers for operations with such calls (see H.7). Add the following section: H.7 Extensions to Global and Global'Class Aspects In addition to the entities specified in 6.1.2, the Global aspect may be specified for a subtype (including a formal subtype), formal package, formal subprogram, and formal object of an anonymous access-to-subprogram type. The following additional syntax is provided for specifying Global and Global'Class aspects, to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation: extended_global_aspect_definition ::= USE formal_parameter_designator | DO dispatching_operator_specifier extended_global_aspect_element ::= USE formal_parameter_set | DO dispatching_operation_set formal_parameter_designator ::= formal_group_designator | formal_parameter_name formal_parameter_set ::= formal_group_designator | formal_parameter_name{, formal_parameter_name} formal_group_designator ::= NULL | ALL formal_parameter_name ::= /formal_/subtype_mark | /formal_subprogram_/name | /formal_access_to_subprogram_object_/name dispatching_operation_set ::= dispatching_operation_specifier{, dispatching_operation_specifier} dispatching_operation_specifier ::= /dispatching_operation_/name (/object_/name) Name Resolution Rules A formal_parameter_name shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type. The /object_/name of a dispatching_operation_specifier shall resolve to statically denote an object (including possibly a formal parameter) of a tagged class-wide type T'Class; the /dispatching_operation_/name of the dispatching_operation_specifier shall resolve to statically denote a dispatching operation associated with T. Static Semantics The extended_global_aspect_definition and extended_global_aspect_element can be used to define as part of the Global aspect the *formal parameter set* and the *dispatching operation set* used within an operation. The formal parameter set is identified by a set of formal parameter names after the reserved word USE. Alternatively, the reserved word NULL may be used to indicate none of the generic formal parameters, or ALL to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) might be used within the execution of the operation. If there is no formal parameter set specified for an operation declared within a generic unit, it defaults to USE ALL. The dispatching operation set is identified by a set of dispatching_operation_specifiers after the reserved word DO. It indicates that the Global effects of dispatching calls that *match* one of the specifiers need not be accounted for by other elements of the Global aspect, but are instead to be accounted for by the invoker of the operation. A dispatching call *matches* a dispatching_operation_specifier if the prefix of the call statically denotes the same operation(s) as that of the dispatching_operation_specifier, and at least one of the objects controlling the call is denoted by a name that statically denotes the same object as that denoted by the /object_/name of the dispatching_operation_specifier. In the absence of any dispatching_operation_specifiers, all dispatching calls within the operation are presumed to have the effects determined by the set of Global'Class aspects that apply to the invoked dispatching operation. The Global aspect for a subtype identifies the global variables that might be referenced during default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. If not specified for the first subtype of a derived type, the aspect defaults to that of the ancestor subtype; if not specified for a nonderived first subtype the aspect defaults to that of the enclosing library unit. If not specified for a nonfirst subtype S, the Global aspect defaults to that of the subtype identified in the subtype_indication defining S. The Global'Class aspect may be specified for the first subtype of a tagged type T, indicating an upper bound on the Global aspect of any descendant of T. If not specified, it defaults to Unspecified. Legality Rules For a tagged subtype 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 the first subtype of any ancestor of T. If the formal parameter set is anything but ALL in the Global aspect for an operation declared within a generic unit, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set. Any dispatching call occurring within the operation that does not match a dispatching_operation_specifier is checked using the Global'Class aspect(s) applicable to the dispatching operation; if there is a match, there is no checking against other elements of the Global aspect(s) applicable at the point of call. !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, OUT, USE, and DO annotations proposed can be statically checked. This new version of this AI incorporates changes defined by AI12-0240-6 (overriding), AI12-0303-1 (mutable constants), AI12-0310-1 (package private part), and AI12-0334-2 (subtypes and predicates). In this new version, we have dropped the notion of a Global attribute (i.e. X'Global) in favor of somewhat different defaults, and have incorporated more precise forms of Global aspect elements (USE ... and DO ...) into the High-Integrity Annex H where they need not be supported in initial implementations of the new standard. We have also added a restriction in H.4 to allow users to disallow use of the new Unspecified value for the Global aspect for any library-level entities. We allow Global specifications on packages or generic packages only if they are library units, analogous to the same limitation of where Pure can be specified, to establish a default for library-level entities. More details on the new defaults are detailed below. The overall goal is that a programmer who specifies nothing gets something reasonable. Another goal is that existing SPARK programs use of Global should be acceptable largely as is, except for the slight change in syntax to use reserved words "IN" and "OUT" rather than the non-reserved "Input", "In_Out", and "Output" currently used in the SPARK Global aspect. In any case, a compiler could accept both the old syntax and the new syntax, as they are unambiguously distinguishable at compile time. The most critical new "default" in this new version is that entities not within a declared-pure library unit, or not at library-level, have Unspecified as their default Global aspect. This effectively implies that the caller may assume the best, but no checking is necessarily being performed at the point of call (though implementations are permitted to effectively inline the call to do additional checks). We provide a restriction of No_Unspecified_Globals in Annex H to allow a user to disallow any library-level entities with Global => Unspecified within a partition. Note that for non library-level entities, even if their own Global aspect is Unspecified, they must still honor any Global aspects of lexically enclosing entities, if these entities have an explicit or implicit Global aspect other than Unspecified. For example, a nested subprogram with Global => Unspecified still cannot violate the Global aspect of its enclosing subprogram, so if the enclosing subprogram specifies Global => SYNCHRONIZED, the nested subprogram cannot reference a variable that is global to its enclosing subprogram unless it is synchronized. It *may* reference variables local to its enclosing subprogram with no restrictions. The next critical new "default" is that entities declared within a generic unit are presumed to make use of *all* generic formal parameters associated with any enclosing generic unit, while not worrying about any of the possible Global effects of that usage in their Global aspect. These additional effects are handled at the point of instantiation, rather than at the point of definition of the generic, much in the same way that "purity" of an instantiation is determined by a combination of the "purity" of the generic and the purity of the actual parameters to the generic. In annex H, we provide ways to specify upper bounds on the effects of generic formal parameters, and we provide an ability to limit which generic formal parameters are actually used within an entity defined within a generic unit (USE formal_parameter_name, ...). This allows us to say that all entities declared at library level within a declared-pure library unit default to Global => null, even if they are within a generic unit, because the USE => ALL is implicit for such entities. The final critical new "default" is that private types are presumed to be "Compound" in the sense that any components of a pool-specific access type declared in the same private part are presumed to be "Internal" to the type, and only give access to other elements of the same conceptual Compound object. Visible access types, and general access types (as opposed to pool-specific ones) are never considered to be "Internal" and any dereference of such an access value is presumed to reference some aliased object which might not be part of the current conceptual "Compound" object and must be accounted for in the Global aspect of the operation. We give an implementation permission to allow other special cases of dereferences to be exempted from normal checks, based on additional analysis. We have also included in Annex H an ability to specify that certain dispatching calls might be performed as part of the execution of an entity, allowing the invoker to more precisely deal with the possible effects of such a call, rather than the entity itself having to fall back on the Global'Class effects, which are likely to be very pessimistic, if specified at all. Some overal notes on the above: This version of this AI was based on work done by Tuck and Claire to reach some kind of simpler consensus position on Global. Probably the biggest change that came from that work was the introduction of the notion of Global => Unspecified to better match existing SPARK usage where few if any Global specifications are required. We have coupled that with a restriction No_Unspecified_Globals to accommodate those users who want to impose on themselves a requirement to specify Global, explicitly or implicitly, at least on all library-level entities. A related change was to move concerns about use of generic formals to the point of instantiation, so operations in a "pure" generic unit can be (implicitly or explicitly) simply "Global => null". The additions relative to the consensus report are very few, and are justified based on a strong belief we need to ensure that even if very imprecise, the Global aspect can be presumed to be an *over* approximation of the true set of global effects. This led us to add ALIASED as an option, to cover all dereferences of general access types without going all the way to ALL. We also held on to a way to establish an overall default, but we now limit it to a library unit as a whole, as that is the level at which Pure can be declared, and the default only applies to library-level elements, not to any non library-level declarations. Non library-level entities always default to Global => Unspecified, but we believe that that is not a significant loss in functionality, as these nested entities must still abide by any Global aspect of their enclosing library-level entity. We have exempted certain dereferences of pool-specific access values from being accounted for in the Global aspect. We do not require any special aspect specifications to make use of these exemptions. We only require that the access type be declared in a private part or a body, and that any dereference be reachable from a formal parameter whose parameter mode allows for the operation performed on the dereference. This meets the expressed goal that existing code that "does the right thing" as far as using access types for implementing abstract data types does not need any additional aspect specifications and can still specify a Global aspect of NULL on primitive operations of the abstract data type. We have eliminated the need for a Global attribute (X'Global) and moved all functionality that depended on that into Annex H. We have ensured that the functionality in the Annex is optional in the sense that it only adds precision; it doesn't provide critical functionality for typical use. Certain of the language-defined packages (such as those related to streaming) might use these features to describe their effects more precisely, but implementations that do not support these Annex H features can choose how to reflect the Global effects of these language-defined packages in a way that is appropriate to typical usage patterns. !example ** TBD. !ASIS ** TBD. !ACATS test ACATS tests should be created to test that the new annotations are correctly enforced. !appendix From: Steve Baird Sent: Wednesday, October 2, 2019 1:22 PM AdaCore has reviewed the Global aspect introduced in AI12-079 and subsequently referenced in several other AIs (e.g., AI12-267, AI12-240, AI12-302, AI12-303, AI12-310) and requests that the ARG consider a substantial simplification of the definition of this aspect. Objections to the current proposal that were raised in AdaCore's discussion include: 1) It seems too complex. 2) Compatibility with SPARK seems problematic. 3) It seems to be an immature proposal. Discussion of this request will be an agenda item for the upcoming meeting in Lexington. **************************************************************** From: Jeffrey Cousins Sent: Wednesday, October 2, 2019 1:42 PM Another last minute objection. Do they have any alternative proposal? **************************************************************** From: Tucker Taft Sent: Wednesday, October 2, 2019 2:19 PM The most basic alternative is to eliminate the whole concept. An intermediate suggestion was to revert to something such as "Global => [null | synchronized | all]" **************************************************************** From: Steve Baird Sent: Wednesday, October 2, 2019 2:22 PM > Do they have any alternative proposal? No, but two of the alternatives that have been discussed internally at AdaCore are - completely eliminate the Global aspect and all uses thereof from the Ada 202x language definition; - disallow Global aspect specifications that specify a set of referenced objects other than (roughly speaking) "no objects", "all objects", or "all synchronized objects". **************************************************************** From: Yannick Moy Sent: Wednesday, October 2, 2019 3:47 PM > The most basic alternative is to eliminate the whole concept. An > intermediate suggestion was to revert to something such as > "Global => [null | synchronized | all]" What would be the use of "Global => all"? We suggested either "Global => null" or "Global => synchronized", but I don't see a use for "Global => all"? Unless it is to revert the effect of an enclosing "Global" contract, which I think is more confusing than helping in that case. **************************************************************** From: Richard Wai Sent: Wednesday, October 2, 2019 3:27 PM The idea is that in full Ada, unlike SPARK, accessing global variables is not unusual. We also need to consider existing code. We prefer to avoid changes that break existing code. In SPARK, the default of Global is "null", meaning that no global access are allowed. This would not be an acceptable default for Ada, since it would break a huge amount of existing code, and make new code more complex to reason about. When using SPARK, the goal is to prove that the code will not raise exceptions, so the extra legwork required to describe the data dependencies is part of the cost of getting that proof. However for full Ada, having this requirement is far too extreme. So thus, the default of "all" means that the given entity can access any entity global to it, where as "null" means it is restricted to local entities only. The concept here is to provide a new tool which allows for the specific restriction of global accesses, by restricting them to task-safe objects or local-only objects. **************************************************************** From: Randy Brukardt Sent: Wednesday, October 9, 2019 3:55 PM >What would be the use of "Global => all"? We suggested either "Global => null" >or "Global => synchronized", but I don't see a use for "Global => all"? Unless >it is to revert the effect of an enclosing "Global" contract, which I think is >more confusing than helping in that case. "all" is the default state for most (but not all) existing code. More importantly, we generally allow (for all aspects) a user to confirm that default state. Confirming an aspect always is useful, because it tells readers that the aspect is intended to have a particular value as opposed getting such a value by default. It seems likely that some organizations will require one or more specifications of Global in every compilation unit as part of their recommended programming style, and certainly such organizations will need to be able to write Global => all. Finally, note that "all" is not the default for *all* code; in particular, non-generic Pure packages default to "null". It's possible that some pure packages (those that dereference general access types) will need to use "all" (or some other global specification) on some operations, so being able to specify that will be necessary. **************************************************************** From: Tucker Taft Sent: Wednesday, October 9, 2019 4:03 PM It seems likely that in some packages, you would establish a default of "Synchronized" or "Null," but still have a few routines with side effects that are not thread safe. You would not want to penalize the whole package just because a couple of routines are not thread safe. **************************************************************** From: Yannick Moy Sent: Wednesday, October 9, 2019 11:36 PM I am not convinced by that use case. The need for a package level default is rare enough in my experience that you don't need an escape mechanism. And that's also the only justification for that "Global => all". I'm even less convinced by Randy's explanations that the user may want to positively state that a subprogram can touch any global variables (which is not a proper specification in my opinion). **************************************************************** From: Yannick Moy Sent: Wednesday, October 9, 2019 11:30 PM > The idea is that in full Ada, unlike SPARK, accessing global variables is > not unusual. We also need to consider existing code. We prefer to avoid > changes that break existing code. In SPARK, the default of Global is "null", > meaning that no global access are allowed. This would not be an acceptable > default for Ada, since it would break a huge amount of existing code, and > make new code more complex to reason about. This is not true. There is no default in SPARK. The Global is computed by the tool when not provided explicitly. > When using SPARK, the goal is to prove that the code will not raise > exceptions, so the extra legwork required to describe the data dependencies > is part of the cost of getting that proof. However for full Ada, having this > requirement is far too extreme. I don't know why you say that. Most SPARK users these days don't use Global/Depends at all. Even those who use them do that very little, relying on automatic generation for all the contracts they don't care to specify. > So thus, the default of "all" means that the given entity can access any > entity global to it, where as "null" means it is restricted to local > entities only. The concept here is to provide a new tool which allows for > the specific restriction of global accesses, by restricting them to > task-safe objects or local-only objects. Understood. For me, "all" is the implicit default, which is why I don't see a need to specify it. **************************************************************** From: Richard Wai Sent: Thursday, October 10, 2019 12:43 PM > This is not true. There is no default in SPARK. The Global is computed by > the tool when not provided explicitly. Fair enough, but we can't expect the Ada compiler to synthesize global contracts, so in effect this point is mute. > Understood. For me, "all" is the implicit default, which is why I don't see > a need to specify it. The Ada standard does not usually do implicit (thankfully). These things are usually defined clearly, and that is always better. If an aspect has a default value, there must be a specific value for that default. Also as Tuck mentioned, the enclosing scope might have a Global set to something more restrictive, which a subprogram needs to override. So if the package is Global => synchronized, a subprogram of the package might be Global => all. If there was not "all", it wouldn't be possible to make this override. I understand that you probably don't agree with that idea of overriding, but from a purely Ada perspective, it is orthogonal behaviour. It is similar to, say, the Assertion_Policy pragma. **************************************************************** From: Tucker Taft Sent: Thursday, October 10, 2019 1:31 PM >> It seems likely that in some packages, you would establish a default of >> "Synchronized" or "Null," but still have a few routines with side effects >> that are not thread safe. You would not want to penalize the whole package >> just because a couple of routines are not thread safe. > > I am not convinced by that use case. > The need for a package level default is rare enough in my experience that > you don't need an escape mechanism. I think your SPARK experience might not be as relevant to how we envisage Global being used initially for Ada 202X, since we see Global in the near term being used as an important way to identify thread safety. For thread safety, the natural unit of concern is often the package where a type is defined, rather than the individual subprograms that represent the operations on the type. > And that's also the only justification for that "Global => all". I'm even > less convinced by Randy's explanations that the user may want to positively > state that a subprogram can touch any global variables (which is not a > proper specification in my opinion). It is a fundamental principle of aspects that one can always affirm the default. We have a few "golden" rules in Ada, and this is definitely one of them. Many (but alas, not all) of these "golden" rules are enshrined as "Language Design Principles" in the AARM. The principle associated with being able to express the default is partly captured by AARM 13.1(1.a.1/3): "Confirming the value of an aspect should never change the semantics of the aspect. Thus Size = 8 (for example) means the same thing whether it was specified with a representation item or whether the compiler chose this value by default." Sometimes we violate our own Principles, but when we do, there needs to be some strong overriding reason. **************************************************************** From: Randy Brukardt Sent: Thursday, October 10, 2019 3:28 PM >>It seems likely that in some packages, you would establish a default >>of "Synchronized" or "Null," but still have a few routines with side >>effects that are not thread safe. You would not want to penalize the >>whole package just because a couple of routines are not thread safe. >I am not convinced by that use case. >The need for a package level default is rare enough in my experience >that you don't need an escape mechanism. That's because SPARK doesn't try to contract generic units. The contract for a generic unit depends on the formal parameters, and it can be complex enough that it's impractical to repeat it on all of the contained operations. See the containers definition for an example of what I mean. (Without those complex contracts, all generics would have to be Global => all, which would be deadly to any use of libraries in parallel contexts.) >And that's also the only justification for that "Global => all". I'm >even less convinced by Randy's explanations that the user may want to >positively state that a subprogram can touch any global variables >(which is not a proper specification in my opinion). For SPARK, that may be true. That's why we're considering changing the name of the aspect to avoid any sort of conflict with SPARK. For Ada 202x, however, the primary use of the specification is for parallel safety, and the secondary uses are for optimization (much like pragma Pure, except specifiable everywhere). This is almost completely separate from any use that SPARK has. For instance, for checking parallel loops, we really only need to specify five states (ignoring generic and parameter issues for the moment): "in out all", "in all", "in out synchronized", "in synchronized", and "null" -- and all of the latter ones work with parallel loops while the first does not. More detail buys nothing with a loop since the items are being compared with themselves, so any unsynchronized global writes will always conflict with themselves and thus fail. More detail could help for parallel blocks and in Ada tasks, but it is much less clear whether parallel blocks would be used that much, and whether race checking between Ada tasks is really feasible. The existence or absence of parallel races is a critical part of the specification of a subprogram. It really should be given explicitly, just like constraints and parameter modes and preconditions. Not checking for parallel races is a nonstarter for me. I do not want to leave the field of "safe" parallelism to other languages like Rust, and I certainly do not want to require the use of separate tools to get any sort of safety (we've been saying for decades that Lint is an inadequate way to make C safe, why should the same logic not apply to Ada??). SPARK has to be a tool for a limited number of Ada users with critical needs, not something that is required to make Ada safe. In any case, a basic principle of Ada is that one can always *explicitly* specify something that happens implicitly. It would be madness to have a default of "all" but not be able to specify that. **************************************************************** From: Randy Brukardt Sent: Thursday, October 10, 2019 3:33 PM BTW, as discussed at the meeting, this discussion really ought to be on Ada-Comment so that the entire Ada community can weigh in. Of course, this thread demonstrates the problem, too, as a post about an outside discussion has morphed into a more detailed feature discussion. And it's hard to move existing threads without killing them off. **************************************************************** From: Yannick Moy Sent: Sunday, October 13, 2019 9:27 AM > That's because SPARK doesn't try to contract generic units. The contract for > a generic unit depends on the formal parameters, and it can be complex > enough that it's impractical to repeat it on all of the contained > operations. See the containers definition for an example of what I mean. > (Without those complex contracts, all generics would have to be Global => > all, which would be deadly to any use of libraries in parallel contexts.) Given that the standard containers are not thread-safe, I don't understand your point. What kind of use of standard containers do you envision in parallel contexts? The use of a package-level default is orthogonal IMO to the use of Global on generic units. Yes, for richer Global that take into account the globals of formal subprograms, one would need to be able to refer to these globals using something like Subp'Global. This is most likely a usage that is very specific to the subprograms inside the generic unit, as it depends on calling or not the formal subprogram, so I don't see the use for a package default here. Going beyond that and having contracts like Type'Global is defeating the purpose of specification IMO, by leading to contracts that no-one can understand. > For SPARK, that may be true. That's why we're considering changing the name > of the aspect to avoid any sort of conflict with SPARK. For Ada 202x, > however, the primary use of the specification is for parallel safety, and > the secondary uses are for optimization (much like pragma Pure, except > specifiable everywhere). This is almost completely separate from any use > that SPARK has. If that's true, the new Ada aspect has both a very narrow usage IMO, and will be a source of endless confusion, as we will continue to evolve the Global aspect in SPARK to ensure essentially the same things: detect harmful aliasing in both sequential and parallel contexts (this is already how Global is used in SPARK, which does support Ravenscar and Jorvik profiles!) > For instance, for checking parallel loops, we really only need to specify > five states (ignoring generic and parameter issues for the moment): "in out > all", "in all", "in out synchronized", "in synchronized", and "null" -- and > all of the latter ones work with parallel loops while the first does not. > More detail buys nothing with a loop since the items are being compared with > themselves, so any unsynchronized global writes will always conflict with > themselves and thus fail. Our investigations so far indicate that most real world usage of parallelism in loops are concerned with operating over the same large data structure in chunks, a use that corresponds precisely to your "in out all" above. **************************************************************** From: Tucker Taft Sent: Monday, October 14, 2019 8:01 AM > ... > Our investigations so far indicate that most real world usage of parallelism > in loops are concerned with operating over the same large data structure in > chunks, a use that corresponds precisely to your "in out all" above. So long as the large data structure is indexed by either the chunk parameter or the loop parameter, there is no problem, and no requirement for an "in out all." See 9.10.1(20/5) in latest 202X RM: "This policy includes the restrictions imposed by the Known_Parallel_Conflict_Checks policy, and in addition disallows a parallel construct from reading or updating a variable that is global to the construct, unless it is a synchronized object, or unless the construct is a parallel loop, and the global variable is a part of a component of an array denoted by an indexed component with at least one index expression that statically denotes the loop parameter of the loop_parameter_specification or the chunk parameter of the parallel loop." **************************************************************** From: Tucker Taft Sent: Monday, October 14, 2019 9:24 AM > Given that the standard containers are not thread-safe, I don't understand > your point. What kind of use of standard containers do you envision in > parallel contexts? This issue is addressed by two AIs, AI12-0196-1 which make it clear that there is no conflict between container elements with different indices, and AI12-0111-1, which provides for "stable" containers which are by default used when iterating over a container, allowing the tampering checks to be performed only before and after the whole loop, rather than on each iteration. **************************************************************** From: Randy Brukardt Sent: Tuesday, October 15, 2019 10:28 PM > Given that the standard containers are not thread-safe, I don't understand >your point. What kind of use of standard containers do you envision in parallel >contexts? As Tucker noted, we fixed many of the containers threading issues long ago. In addition to the AIs Tucker mentioned, the containers contract AI makes many of the containers operations (that don't depend on the formal parameters) Global => null, and assuming that the element type is appropriate, allows reading as well. Moreover, *any* generic package has this problem, and it would be a terrible idea to have two features (parallelism and generics) that cannot work together. >The use of a package-level default is orthogonal IMO to the use of Global >on generic units. Certainly true; package-level defaults make sense for many packages. Most OOP ADTs have little or no state, for instance, and thus all of the operations in the package ought to be declared Global => null. Reusable packages also often don't have state. Most language-defined packages can only have synchronized state (since they are supposed to be reentrant). Repeating such a declaration on every individual subprogram would add a lot of clutter (especially if the possibly optional package-level specifications are used). ... >> For instance, for checking parallel loops, we really only need to specify >> five states (ignoring generic and parameter issues for the moment): "in out >> all", "in all", "in out synchronized", "in synchronized", and "null" -- and >> all of the latter ones work with parallel loops while the first does not. >> More detail buys nothing with a loop since the items are being compared with >> themselves, so any unsynchronized global writes will always conflict with >> themselves and thus fail. > Our investigations so far indicate that most real world usage of parallelism >in loops are concerned with operating over the same large data structure in >chunks, a use that corresponds precisely to your "in out all" above. Surely not. If the data structure is passed as a parameter (as in a container), then it doesn't appear in the global at all; the operation will often be global null. If the data structure is only being read (a quite common occurrence), then there is no conflict. Tucker also noted the special cases for writing arrays. Moreover, if Ada is to grow with the future, it has to have facilities to not just do the sorts of parallelism that people are writing today, but also to have abilities to write other sorts of uses in the future. Personally, I can only think of one data structure that I have *ever* written (in 40 years of programming) that could be parallelized by "chunking a large data structure". Most if the structures I've used are trees of some sort that were created directly with unstructured access types -- partitioning them usefully would take more time than you could ever gain. Ideally, it would be possible to parallelize much of that existing code without having to rewrite much of it (for that, SPARK is a non-starter). Such code is far too complex to have any hope of finding conflicts by hand; the compiler has to do it. Certainly, this first version isn't going to work for everyone or in every circumstance (what does?), but if we don't try, we'll be leaving that for other people to do and those will almost certainly not do the careful language design (for readability, correctness, and all of the other motherhood things) of Ada. **************************************************************** From: Yannick Moy Sent: Wednesday, October 16, 2019 12:18 AM > As Tucker noted, we fixed many of the containers threading issues long ago. > In addition to the AIs Tucker mentioned, the containers contract AI makes > many of the containers operations (that don't depend on the formal > parameters) Global => null, and assuming that the element type is > appropriate, allows reading as well. I was talking of updating the containers. This is not thread safe. So you were only talking of reading a container, that's not so compelling to me. >Certainly true; package-level defaults make sense for many packages. Most >OOP ADTs have little or no state, for instance, and thus all of the >operations in the package ought to be declared Global => null. Reusable >packages also often don't have state. Most language-defined packages can >only have synchronized state (since they are supposed to be reentrant). >Repeating such a declaration on every individual subprogram would add a lot >of clutter (especially if the possibly optional package-level specifications >are used). Why not after all, although I would rather the language sticks to the simple version "null/all/synchronized" for these package defaults. Anything more complex seems overengineered/not useful IMO. >>Our investigations so far indicate that most real world usage of parallelism >>in loops are concerned with operating over the same large data structure in >>chunks, a use that corresponds precisely to your "in out all" above. >Surely not. If the data structure is passed as a parameter (as in a >container), then it doesn't appear in the global at all; the operation will >often be global null. sure, but the operation will still be rejected by the "safe parallelism" checking in Ada, that's my point. >If the data structure is only being read (a quite >common occurrence), then there is no conflict. Our limited experience with users wanting parallel speedup is to write to a collection, not only read. >Tucker also noted the special cases for writing arrays. What is that special case? >Moreover, if Ada is to grow with the future, it has to have facilities to >not just do the sorts of parallelism that people are writing today, but also >to have abilities to write other sorts of uses in the future. Personally, I >can only think of one data structure that I have *ever* written (in 40 years >of programming) that could be parallelized by "chunking a large data >structure". Most if the structures I've used are trees of some sort that >were created directly with unstructured access types -- partitioning them >usefully would take more time than you could ever gain. > >Ideally, it would be possible to parallelize much of that existing code >without having to rewrite much of it (for that, SPARK is a non-starter). >Such code is far too complex to have any hope of finding conflicts by hand; >the compiler has to do it. > >Certainly, this first version isn't going to work for everyone or in every >circumstance (what does?), but if we don't try, we'll be leaving that for >other people to do and those will almost certainly not do the careful >language design (for readability, correctness, and all of the other >motherhood things) of Ada. My view is quite the opposite. Unless you carefully plan in the language for practical uses, you're certain to design an unusable feature. The current design of Global (including compound objects, etc) fits that description IMO. **************************************************************** From: Randy Brukardt Sent: Wednesday, October 16, 2019 1:14 AM ... >My view is quite the opposite. Exactly. We can only agree to disagree. There's no point in continuing to talk to someone that isn't willing to consider the future - because it's only the future that is relevant here (Ada 2012 is good enough for the present and probably the next few years as well). >Unless you carefully plan in the language for practical uses, you're >certain to design an unusable feature. If we only worry about existing "practical" uses, we'll be two decades behind by the time of the next revision of Ada. We have to worry about future uses as well. >The current design of Global (including compound objects, etc) fits >that description IMO. For what it's worth, all of the (C and Fortran) examples shown during the OpenMP session would have passed the proposed conflict checks. Pretty much all reduction examples pass the proposed conflict checks. Those cover a large percentage of things that are typically parallelized. As I said, we will have to agree to disagree. **************************************************************** From: Yannick Moy Sent: Wednesday, October 16, 2019 4:13 AM > Exactly. We can only agree to disagree. There's no point in continuing > to talk to someone that isn't willing to consider the future enough said, I was trying to have a technical discussion, not personal attacks. **************************************************************** From: Raphael Amiard Sent: Wednesday, October 16, 2019 5:07 AM >>Understood. For me, "all" is the implicit default, which is why I don't see >>a need to specify it. >The Ada standard does not usually do implicit (thankfully). These things are >usually defined clearly, and that is always better. If an aspect has a >default value, there must be a specific value for that default. I agree with that, it's a bit like "in" mode for parameters. If the default is "all", then the user should still be able to specify it. **************************************************************** From: Arnaud Charlet Sent: Wednesday, October 16, 2019 5:44 AM Makes sense to me too. **************************************************************** From: Raphael Amiard Sent: Wednesday, October 16, 2019 5:54 AM >>Certainly, this first version isn't going to work for everyone or in every >>circumstance (what does?), but if we don't try, we'll be leaving that for >>other people to do and those will almost certainly not do the careful >>language design (for readability, correctness, and all of the other >>motherhood things) of Ada. >My view is quite the opposite. Unless you carefully plan in the language for >practical uses, you're certain to design an unusable feature. The current >design of Global (including compound objects, etc) fits that description IMO. I agree with Yannick. For me this is wishful design at best. "Planning" for the future when you're not sure what the future is, in terms of language design seems like a very bad idea, a good way to put a lot of features that won't be used. If your planning was wrong, this "careful language design" you're talking about will just be dead weight, while those other people will still have to conceive the solution that is actually right for them. For me, one such example in Ada is safety rules wrt. access types in general: Those have proved to be overly restrictive, to the point of making pool specific access types in Ada unusable for a variety of use cases. The result have just been people circumventing the "safety". I predict that's exactly what would happen in that case, if this aspect was to be implemented in a compiler in the first place - which is far from certain at this point, and that's something the ARG should bear in mind. **************************************************************** From: Tucker Taft Sent: Wednesday, October 16, 2019 8:18 AM >>As Tucker noted, we fixed many of the containers threading issues long ago. >>In addition to the AIs Tucker mentioned, the containers contract AI makes >>many of the containers operations (that don't depend on the formal >>parameters) Global => null, and assuming that the element type is >>appropriate, allows reading as well. >I was talking of updating the containers. This is not thread safe. So you >were only talking of reading a container, that's not so compelling to me. You are not limited to reading. As mentioned, "stable" containers are by default used by iterators in 202X (the "Iterator_View" -- see 5.5.2(12/5)), and stable containers allow replacing of existing elements, including in parallel for vectors of "definite" components. The iterators for the language-defined containers explicitly support parallel iteration, since their Iterate functions return "Parallel_Reversible" iterators. Reading is also very important for parallel applications, as any sort of reduction or more complex analysis is frequently a read-only operation on the container. In many cases, a large data structure is read many more times than it is updated. Most "big data" operations are generally reading huge data structures without overwriting them. ... >>Surely not. If the data structure is passed as a parameter (as in a >>container), then it doesn't appear in the global at all; the operation will >>often be global null. >sure, but the operation will still be rejected by the "safe parallelism" >checking in Ada, that's my point. So long as the index is either the loop parameter or the chunk parameter, there is no conflict. >>If the data structure is only being read (a quite >>common occurrence), then there is no conflict. >Our limited experience with users wanting parallel speedup is to write to a >collection, not only read. As mentioned above, you can do both using a parallel iterator. >>Tucker also noted the special cases for writing arrays. >What is that special case? When indexing into an array that is global to a parallel loop, so long as the index is the loop parameter or the chunk parameter, there is no conflict (see 9.10.1(20/5)). **************************************************************** From: Richard Wai Sent: Wednesday, October 16, 2019 10:51 AM > I agree with Yannick. For me this is wishful design at best. "Planning" for > the future when you're not sure what the future is, in terms of language > design seems like a very bad idea, a good way to put a lot of features that > won't be used. If your planning was wrong, this "careful language design" > you're talking about will just be dead weight, while those other people > will still have to conceive the solution that is actually right for them. > For me, one such example in Ada is safety rules wrt. access types in > general: Those have proved to be overly restrictive, to the point of making > pool specific access types in Ada unusable for a variety of use cases. The > result have just been people circumventing the "safety". I strongly disagree with this. Ada often gets flack for these types of things as being "overly restrictive". However in my very practical experience, it has always been a sign of the programmer either not thinking through the problem correctly, or trying to force the style of other languages into Ada. If you follow software engineering principles carefully, show a little discipline, and really think through the problem properly, I have yet to find a case where pool-specific access types (or any access types) stand in the way. And again, if a programmer finds this to be a problem, they are probably approaching the problem poorly. If we don't plan for the future, then what are we going to get? The only other approach I could think of is to be broadly less restrictive, and fall-back into a "programmer knows best" approach. If we do that, we all might as well just use C++. I think the software industry at large really needs to spend some thing reflecting on the prevailing "just let me do whatever I want" attitude. You don't hear electrical engineers complaining about ringing, and how they can't make right-angle traces on PCBs. You don't hear mechanical engineers complaining about thermal expansion. You don't hear structural engineers complain about wind loads. And none of them have stopped innovating because of those things. The rules for access types in Ada are sane and reasonable. And if you accept them for what they are, and they are not C pointers, you will design your software around them, and you'll get rewarded with a very high degree of safety. Ada is about discipline. Ada is about strongly encouraging the programmer to do things with more care. It also allows managers to spot sloppy and unsafe code more easily. Ada is about exact rules. Ada is about planning ahead. Everyone plans for the future. It's simply lazy not to. Yes you can't always get it right, but the benefits of doing so are not predicated on getting it exactly right. **************************************************************** From: Randy Brukardt Sent: Wednesday, October 16, 2019 3:10 PM > enough said, I was trying to have a technical discussion, not personal > attacks. But this is (now) more of a philosophical discussion than a technical discussion. You don't seem to think that safety in this area is achievable, and I not only think that it is, but also that Ada cannot continue with it. Unless we can agree on that point, there is nothing further to talk about, because all of the technical issues stem from that philosophy. In any case, I apologize if you took the above as a personal attack. I was just trying to restate my understanding of your position, and did it badly. **************************************************************** From: Tucker Taft Sent: Tuesday, January 14, 2020 11:41 AM In AI12-0079-2, there is mention of a document describing a simpler consensus proposal for Global developed by Claire and Tuck at AdaCore. Here is the content of that document. Note that in the "overview notes" at the end of the !discussion for AI12-0079-2, an attempt is made to record to what degree the AI goes beyond the consensus document. Most of these additions were alluded to below as "possible extensions" or as extensions to handle "indirect effects." Several AdaCore folks have indicated they are not in favor of any of the additions, or have not had enough time to evaluate them. ----------- Simplified Global Aspect for Ada202X SYNTAX 1 - Global aspects can be supplied on subprograms, tasks, and entries in order to document the set of global objects they access, and how they access them. 2 - These contracts associate a mode, "in", "in out", or "out", to a set of names. Modes in out and out would effectively be the same for the compiler, but they could make a difference for other tools (SPARK, CodePeer...). These names can be: * Global constants * Global variables * A package entity Pack if the contract is located somewhere which does not have visibility over the body of Pack. Here it stands for the private state of Pack. * "all" to state that the subprogram could read or write any global. It may be used to forbid the usage of some subprograms. 3 - Special values of the Global contract can be: * "null" to state that no globals are accessed * "Unspecified" to state that no globals have been supplied for this entity. This would be the default. A restriction No_Unspecified_Globals will be available for projects which choose to require a more precise description of the global effects. * "Synchronized", to state that there are references to an unspecified set of synchronized objects. Because such objects are typically volatile, there is no significant value in being more specific about synchronized objects, as far as "in" vs. "in out". "Synchronized" can be combined in a Global aspect specification with more precise descriptions of the side effects on non-synchronized objects. CHECKS 4 - If a subprogram mentions a global variable, this variable must be in the global contract for the subprogram. If the variable is not visible at the point of the subprogram declaration, the package private state is considered to be mentioned instead. 5 - If a subprogram writes to a global variable, this variable must be in the global contract for the subprogram, and its mode should be either out or in out. If the variable is not visible at the point of the subprogram declaration, the package private state is considered to be written instead. 6 - When a subprogram calls another subprogram: * Names mentioned in the global contract of the callee are considered to be mentioned by the caller. * Names mentioned in the global contract of the callee with modes out or in out are considered to be written by the caller. * If some package private state occurs in the global contract of the called subprogram, and the specification of the caller does have visibility on the body of the package, then the global contract of the caller is expressed in terms of the package private state for the check. 7 - No checks are performed when checking a subprogram with Unspecified as a global annotations, and no checks are associated with the global contract of a callee if the callee has Unspecified as a global. 8 - A subprogram with a synchronized global annotation, can mention any variables which are synchronized, in addition to those stated explicitly in its Global aspect. POSSIBLE EXTENSIONS * Allowing a way to refer to the global contract of a formal parameter of a generic unit in the global contract of generic subprograms or subprograms in generic packages (eg. using Subp'Global). * Having a way to change the default at the package level, at least to put it to null or synchronized. ACKNOWLEDGEMENTS The Global aspect does not in general cover all the global effects of a subprogram. In particular, just like for parameter modes, effects on aliased data, or on data designated through a pointer would not necessarily occur in the Global contract of a subprogram. procedure Write_To_All (X : My_Access_Type) is begin X.all := Some_Value; -- OK end Write_To_All; procedure Write_To_All with Global => (in => X) is begin X.all := Some_Value; -- OK end Write_To_All; Coming up with a good way to handle (some of) these cases would require time and prototyping, so would best be handled through an RFC. As a part of this work on a better handling of indirect effects, it may be necessary to tackle the problem of imprecise parameter modes as well. **************************************************************** From: Randy Brukardt Sent: Wednesday, January 15, 2020 7:03 PM ... >I believe that, to improve user experience, we should use the >under-approximation (ie do not take into account modification under an >access). I wanted to clarify my comments during the meeting on this topic, as I know that many of us have a better understanding of the issues when we read it and can digest it (as opposed to hearing it and having it quickly disappear, not to mention it is hard to understand complex positions from a 30-second summary over a fuzzy audio connection). My primary objection to Claire's document is summarized by this "under-approximation" sentence. The reason is that pretty much every use of Global that I can imagine requires an "over-approximation". (I'm assuming for this argument, like Claire, that an exact result is practically impossible, at least for the full unrestricted Ada language.) The intended use of Global as part of the checking to make parallel operations acceptably safe, for instance, requires that access dereferences be excluded unless provably safe. It's not helpful to detect only a few cases of obvious problems. Without strong checking, "parallel" is an attractive hazard that would make Ada substantially less safe. Similarly, I would like to use this information for optimization of many sorts. Currently, Janus/Ada assumes that every call "kills all", as there is no useful information to the contrary (Pure allows far too much to be useful in this way). Ada contains permissions that go too far and not far enough at once (the permissions don't take all of the parameters into account, and do prevent any optimization even when it is clear that only erroneous execution could change the results). Some of the optimizations in question include removing redundant checks (which of course can't be done if the checked value changes between the checks of interest), removing redundant calls (when the second call has no effect other than wasting time), and the like. Again, any undetected global access makes this sort of thing impossible. It seems to me that much the same situation occurs for verification. A side-effect potentially invalidates much of what is known before a call, and one that it hidden from a verifier is going to mean that invalid assumptions may hold. (Optimization and verification have much the same requirements.) I agree that the "user experience" is important, but if the aspect isn't providing the needed guarantees, then it doesn't matter very much as it won't be used very often. I note in passing that in my recent code, probably 20% of the subprograms could be Global => null, and probably another 40% could be Global => in all, even with the most conservative rule (that is, a dereference is only covered by "all"). These are all opportunities for parallel usage and for optimization (which includes checking code elimination, redundant store elimination, and many more). I've been planning to build something like this with or without language support, but obviously I'd prefer to use something supported by the language (it reduces the chance of missing corner cases and the like). So I would hope that we can find a way to support Global that I (and presumably others) would find useful. One possible way to do so would be to have a configuration mode that determines whether under-specification or over-specification is required for Global. Presumably SPARK would use the under-specified mode, and Janus/Ada would treat anything compiled in the under-specified mode as "unknown" for any implementation-defined uses (optimizations, warnings, etc.) Such a mode would determine how dereferences are handled (either ignored or required to be covered with "all" of the correct mode), and probably ought to have some effect on how library-level "unspecified" is handled as well ("in out all" unless the implementation can prove better). **************************************************************** From: Claire Dross Sent: Thursday, January 16, 2020 8:21 AM > I agree that the "user experience" is important, but if the aspect > isn't providing the needed guarantees, then it doesn't matter very > much as it won't be used very often. All depends on what you call needed guarantees I suppose. We are back to the initial question, what do we want this aspect to be used for. I think that the "complement of to the parameter list" is already interesting. But I understand that you disagree. > I note in passing that in my recent code, probably 20% of the > subprograms could be Global => null, and probably another 40% could be > Global => in all, even with the most conservative rule (that is, a > dereference is only covered by "all"). These are all opportunities for > parallel usage and for optimization (which includes checking code > elimination, redundant store elimination, and many more). Interesting. Do those 20% use pointers at all? If not, maybe a restriction asking for no pointer dereference could reconcile the two views? > I've been planning to build something like this with or without language > support, but obviously I'd prefer to use something supported by the language > (it reduces the chance of missing corner cases and the like). So I would > hope that we can find a way to support Global that I (and presumably others) > would find useful. > > One possible way to do so would be to have a configuration mode that > determines whether under-specification or over-specification is required for > Global. Presumably SPARK would use the under-specified mode, and Janus/Ada > would treat anything compiled in the under-specified mode as "unknown" for > any implementation-defined uses (optimizations, warnings, etc.) Such a mode > would determine how dereferences are handled (either ignored or required to > be covered with "all" of the correct mode), and probably ought to have some > effect on how library-level "unspecified" is handled as well ("in out all" > unless the implementation can prove better). My guess is that with the over-approximation, most (all?) subprograms using pointer dereferences would quickly get "in out all" (or at least "in all"). This is not bringing much information in my opinion... Also remark that, without any proper checking of aliasing, no optimization of anything which does not have Global null would really be safe (even in the absence of pointers). Thus I don't think the over-approximation case would be as valuable as you think: it would hardly ever bring valuable information on programs using pointers, and it would not provide complete safety. Maybe what you really want is something close to Pure which would mean global null? **************************************************************** From: Randy Brukardt Sent: Thursday, January 16, 2020 8:13 PM ... > > I note in passing that in my recent code, probably 20% of the > > subprograms could be Global => null, and probably another 40% could > > be Global => in all, even with the most conservative rule (that is, > > a dereference is only covered by "all"). These are all opportunities > > for parallel usage and for optimization (which includes checking > > code elimination, redundant store elimination, and many more). > > Interesting. Do those 20% use pointers at all? If not, maybe a > restriction asking for no pointer dereference could reconcile the two > views? Probably not, most such routines take a record type and calculate something interesting with the components. But I am assuming that one can use the containers roughly as I annotated them last year (so there might be some pointers in the implementation). You're new here (and don't hang out on comp.lang.ada), so you probably haven't heard my oft-made opinion that a good ADT design for Ada uses no visible access types. (A very brief explanation: this lets the client control memory management explicitly with access types, by using Ada scoping, or by using a container. If you use access types, you end up taking on memory management yourself and that restricts how the client can use your abstraction.) I know many others disagree with this (and I tend to state in an abolutist way which makes a good soundbite but I realize that not every problem is the same), but I try to hold to that for most of my work. Thus, any pointers are hidden in the package and can be often be accounted for with some ownership scheme (or possibly even the simpler compound scheme that Tucker described in AI12-0240-6). Of course, all of these estimates are by eyeballing code, and once a compiler/tool starts checking it, the numbers and possibilities might change. :-) And I've got a lot of compiler code that predates when I knew anything about designing software! ... > > One possible way to do so would be to have a configuration mode that > > determines whether under-specification or over-specification is required for > > Global. Presumably SPARK would use the under-specified mode, and Janus/Ada > > would treat anything compiled in the under-specified mode as "unknown" for > > any implementation-defined uses (optimizations, warnings, etc.) Such a mode > > would determine how dereferences are handled (either ignored or required to > > be covered with "all" of the correct mode), and probably ought to have some > > effect on how library-level "unspecified" is handled as well ("in > > out all" unless the implementation can prove better). > > My guess is that with the over-approximation, most (all?) subprograms > using pointer dereferences would quickly get "in out all" (or at least > "in all"). This is not bringing much information in my opinion... I expect that as well. In the case of uncontrolled access types (especially general access types), there really isn't much information to bring. You could use something like "aliased " if the designated type is visible, but otherwise there is no possible way to describe what it points at. One probably can do better in with an ownership / compound object scheme, but that clearly requires restrictions on the access type. Given that Ada is likely to compete with languages like Rust that are working in this area, it's an area that we need to be looking at. (Whether we can do something standardizable for Ada 202x is of course worth discussing, but it's an area that we need to be working in, IMHO.) But for the sorts of uses I'm primarily thinking about, even "in all" brings a lot of benefits: A parallel loop can call such a routine safely; the information known before a call to an "in all" subprogram is still known afterwards (modulo parameter changes, which are explicitly in the code); and probably with the most benefit, a redundant call can be part of a common subexpression assuming there are no global writes between the calls. (And I want to use the last effect to help verify preconditions and postconditions.) > Also remark that, without any proper checking of aliasing, no optimization of > anything which does not have Global null would really be safe (even in > the absence of pointers). A compiler optimizer can't do anything if it can't rule out aliasing, so I don't quite see the problem. "Assume-the-worst" is pretty much always the watchword for optimization. There are cases that can't be detected (like chapter 13 stuff), but these are explicitly erroneous. And optimization explicitly assumes that the code isn't erroneous (without such an assumption, there is virtually nothing that could be done, since erroneous code can write any memory location at any time). Formally, if execution is erroneous (which means that anything can happen), then any transformation is acceptable (since the result will still be that anything can happen, even if it is different anything). > Thus I don't think the over-approximation case would be as valuable as > you think: it would hardly ever bring valuable information on programs > using pointers, and it would not provide complete safety. Maybe what > you really want is something close to Pure which would mean global > null? As noted above, "in all" is valuable by itself. Additional precision could be useful, but I don't think it is critical (as much of the time, one would still have a conflict as nearby operations tend to work on the same data structure, and if that structure has some global part, they all probably use it). It is necessary, I think, to have some way for "hidden" access types to be "erased" from the picture, since the containers need to be usable in tasks and parallel operations (and *definitely* need to be able to be optimized) -- and we want users to be able to build similar custom data structures if they need to. We did send this stuff back to Tucker, and I do trust Tucker to work his usual magic and find some way to cut this Gordian knot. The notion of splitting the Global stuff into an object part and an access part should help, as I don't think the object part is very controversial and that will allow us to make useful progress. (The new model for generics is definitely easier to work with than the one I came up with.) Part of my reason for discussing this here is to give him some parameters to work in. P.S. Back when we were working on Ada 2005 and Ada 2012, every time I passed through the Indianapolis area there were many billboards proclaiming "Trust Tucker!". I thought that was good advice. I rather regret that I was always on a busy freeway when I saw one of those and never got a picture for the ARG archives. They don't seem to be around anymore, hopefully that doesn't mean anything for the ARG. :-) **************************************************************** From: Yannick Moy Sent: Friday, January 17, 2020 2:17 AM > One probably can do better in with an ownership / compound object scheme, > but that clearly requires restrictions on the access type. Given that Ada is > likely to compete with languages like Rust that are working in this area, > it's an area that we need to be looking at. (Whether we can do something > standardizable for Ada 202x is of course worth discussing, but it's an area > that we need to be working in, IMHO.) Having worked for the past three years (with Tuck in particular) on defining rules for safe analysis of pointers, I think (1) this is an area of much interest for the future of Ada, and (2) it is not reasonable to expect something in a good enough shape by June. Or maybe you're proposing to delay Ada 202X to a later year, but that's not what we agreed on. If you're not convinced that it is complex, have a quick look at the excellent blog posts by Claire about the solution we adopted in SPARK: https://blog.adacore.com/using-pointers-in-spark https://blog.adacore.com/pointer-based-data-structures-in-spark (this is the easy introduction, not the nitty-gritty details) > A compiler optimizer can't do anything if it can't rule out aliasing, so I > don't quite see the problem. "Assume-the-worst" is pretty much always the > watchword for optimization. I don't see optimization being a major reason for investing in safe pointer/aliasing handling. It has not popped up elsewhere AFAIK, not in the Rust world either, unless you have more info here? > It is necessary, I think, to have some way for "hidden" access types to > be "erased" from the picture, since the containers need to be usable in > tasks and parallel operations (and *definitely* need to be able to be > optimized) -- and we want users to be able to build similar custom data > structures if they need to. Reasonably, the only choice we have is to trust their implementation for now. > We did send this stuff back to Tucker, and I do trust Tucker to work his > usual magic and find some way to cut this Gordian knot. The notion of > splitting the Global stuff into an object part and an access part should > help, as I don't think the object part is very controversial and that will > allow us to make useful progress. Being someone who spent a lot of time discussing it with Tuck and others over the past years, I don't understand how you expect a magic solution to pop up by June. By all accounts, it's too late IMO, whatever clever solution is proposed by Tuck or someone else, we won't have the time to properly assess it. **************************************************************** From: Erhard Ploedereder Sent: Friday, January 17, 2020 4:56 AM > I don't see optimization being a major reason for investing in safe > pointer/aliasing handling. It has not popped up elsewhere AFAIK, not > in the Rust world either, unless you have more info here? Well, pretty much all Java compilers do escape analysis, which involves a variant of aliasing analysis, and the resulting optimizations are plenty and important. Admittedly, afaik, they drop everything in the presence of subcalls that potentially create aliases of the local references, but I could be underestimating them. I don't know why Ada compilers haven't started similar analyses for reference types. As to the program analysis world: In almost all of our tools for embedded systems, aliasing analysis for stack pointers is really essential. Not a rough over-estimation, but a more refined analysis as accurate as we can afford to make it time-wise. Heap pointers, on the other hand are rather irrelevant today (way too difficult and hardly used in embedded code except for inroads of simple OOP, when the languae gives you no choice but to use references). Extrapolating a bit to the future: ... except when you can do the analogon of (a global) escape analysis successfully. **************************************************************** From: Tucker Taft Sent: Friday, January 17, 2020 7:26 AM ... >> We did send this stuff back to Tucker, and I do trust Tucker to work his >> usual magic and find some way to cut this Gordian knot. The notion of >> splitting the Global stuff into an object part and an access part should >> help, as I don't think the object part is very controversial and that will >> allow us to make useful progress. > Being someone who spent a lot of time discussing it with Tuck and others > over the past years, I don't understand how you expect a magic solution to > pop up by June. By all accounts, it's too late IMO, whatever clever solution > is proposed by Tuck or someone else, we won't have the time to properly > assess it. Randy and I have discussed something very simple (and quite different from past approaches) which would address at least his concerns -- it was actually suggested by something that Claire said during the ARG meeting. So stay tuned ... **************************************************************** From: Randy Brukardt Sent: Friday, January 17, 2020 6:10 PM >Having worked for the past three years (with Tuck in particular) on defining >rules for safe analysis of pointers, I think (1) this is an area of much >interest for the future of Ada, and (2) it is not reasonable to expect >something in a good enough shape by June. ... As someone who has spent considerable time working with Tucker to refine and improve his proposals from an Ada perspective, I agree with you on the importance, and disagree with you on the possibility. I have a workable proposal for Ada that is fully checked and adds no erroneousness (it's also rather easy to implement in Janus/Ada, can't speak to other compilers). But that solution is unlikely to work for SPARK, and the checks potentially could be rather expensive. I'd hope that the SPARK people here could come up with something, but if they can't, we have to face the question of whether we want to leave *Ada* without a workable solution for another 5-ish years in order to let SPARK catch up. To me, that is likely to cede all of the mindshare to other languages like Rust. We need to have some new things to attract new people to Ada, because if we don't, the customer base will almost certainly gradually dwindle. >>A compiler optimizer can't do anything if it can't rule out aliasing, >>so I don't quite see the problem. "Assume-the-worst" is pretty much >>always the watchword for optimization. >I don't see optimization being a major reason for investing in safe >pointer/aliasing handling. It has not popped up elsewhere AFAIK, not in >the >Rust world either, unless you have more info here? Erhard answered this way better than I would have. I know from past discussions that AdaCore has not been very interested in the possibilities of Ada-aware optimization, while that probably has been my primary driver for the evolution of Janus/Ada. I don't want to sound like I'm asking for features specifically for Janus/Ada, but I don't want to see features in Ada that interfere with the sorts of uses I'm interested in (we need alternatives for no other reason that to push AdaCore; a single dominant implementation is certain to become stale eventually). >>It is necessary, I think, to have some way for "hidden" access types >>to be "erased" from the picture, since the containers need to be >>usable in tasks and parallel operations (and *definitely* need to be >>able to be >>optimized) -- and we want users to be able to build similar custom >>data structures if they need to. >Reasonably, the only choice we have is to trust their implementation >for now. There is two problems with the "trust" model: First, we have to define fairly carefully what the requirements actually are. If we don't do that, no one will even know what lines that they are allowed to color inside of. How can anyone trust my implementation if I don't even know what restrictions I'm supposed to follow? And second, if we have defined such lines, then I don't know how to determine if I (as the implementor of some ADT) actually have implemented something worthy of trust. To me, this requires some form of checking, because it is too hard to determine if the rules (whatever they are) are met. Ada almost never uses "trust" when verification is possible. And in the cases where it does use "trust" (for instance, interfaces), the consequences of breaking the trust are severe (erroneous execution). I think we all would rather have checks rather than new ways to make things erroneous. >>We did send this stuff back to Tucker, and I do trust Tucker to work >>his usual magic and find some way to cut this Gordian knot. The notion >>of splitting the Global stuff into an object part and an access part >>should help, as I don't think the object part is very controversial >>and that will allow us to make useful progress. >Being someone who spent a lot of time discussing it with Tuck and >others over the past years, I don't understand how you expect a magic solution to >pop up by June. Tucker sent me an outline of a solution yesterday which appeared to work (in part because it is based in part on AI12-0240-6, which I know would work). I already have a dynamic checking solution that works within those parameters (it's perhaps too expensive, but I'm hopeful that we can find some additional checks that could reduce the cost). >By all accounts, it's too late IMO, whatever clever solution is >proposed by Tuck or someone else, we won't have the time to properly assess it. We don't have to have every last detail worked out by June, only an scope determination. The ARG has almost a year to complete polishing the Standard after June. Clearly, we'll need a decent amount of detail to get buy in on the scope for this feature, but we can do work (such as wording) after June. In any case, I don't think my dynamic checking solution could work for SPARK. If that means that we simply publish it in an Annex or as a Technical Specification (that is, something that might be added to the Standard in the future), that would be OK with me. (AdaCore's customers and programmers could decide if they want it implemented.) I don't think that we can afford to wait to address these issues. In 5 years, other languages would have all of the mindshare in this area and there would be no way for Ada to get it back. (I think the same applies to parallel operations, even if we don't have an immediate need for them. Other languages already have these features and they'll be more widely understood in the future.) Ada 202x will need some things that will attract new users to Ada. Otherwise, Ada will just gradually lose users as they retire or move to other things. I don't think delta aggregates are going to excite anyone (although existing Ada users will find them handy). **************************************************************** From: Richard Wai Sent: Friday, January 17, 2020 7:02 PM > I'd hope that the SPARK people here could come up with something, but > if they can't, we have to face the question of whether we want to > leave *Ada* without a workable solution for another 5-ish years in > order to let SPARK catch up. To me, that is likely to cede all of the > mindshare to other languages > like Rust. We need to have some new things to attract new people to > Ada, because if we don't, the customer base will almost certainly > gradually dwindle. I think this is a really important point. The ARG should be focused on Ada and only Ada. I don't think it is our concern how hard we make the lives of the SPARK team (sorry). It is great for us to discuss these issues and do what we can to accommodate SPARK where it makes sense, but It is simply wrong for SPARK to control Ada. It should be the other way around. It is equally inappropriate for AdaCore to dictate the ARG's work (as it is for any single party). If I recall correctly, the ARG has been working on this issue for quite some time, and AdaCore has been the primary resistance to most of the working proposals that we've had. I also not that there are plenty of execution contexts (basically 90% of those we work in) where exceptions are not only fine, they are important useful. These same contexts also make run-time checking similarly desirable and useful. SPARK is expensive, and simply not economic for a large number of situations where it provides no additional safety except preventing exceptions. > Erhard answered this way better than I would have. I know from past > discussions that AdaCore has not been very interested in the possibilities > of Ada-aware optimization, while that probably has been my primary driver > for the evolution of Janus/Ada. I don't want to sound like I'm asking for > features specifically for Janus/Ada, but I don't want to see features in > Ada that interfere with the sorts of uses I'm interested in (we need > alternatives for no other reason that to push AdaCore; a single dominant > implementation is certain to become stale eventually). To be totally fair, this has not played out for most languages in existence. The problem are proprietary implementations. And I don't mean this philosophically, I mean it factually: all of the popular languages in use today have unencumbered, free implementations. Full stop. Most of them have one or two implementations, tops. It's honestly a point of strength to have one reference implementation, but the software community, especially the younger of us, expect languages to be free. Period. Maybe some feature implementations we can help work on for FSF GNAT. It's something I'd be consider dedicating some time to. General-purpose languages that are tied to proprietary implementations are almost guaranteed to fail. It's not the 80s anymore. > Ada 202x will need some things that will attract new users to Ada. > Otherwise, Ada will just gradually lose users as they retire or move to > other things. I don't think delta aggregates are going to excite anyone > (although existing Ada users will find them handy). While I agree with this in principle, I strongly believe that Ada already has features that are far ahead of other comparable languages. Rust, the closest "competitor" to Ada, has a lot of problems - and I'd argue that this is mostly due to their single focus on memory safety and not much else. Let's not get caught up with who is the hottest kid on the block this year. In our practical experience, Ada already makes memory problems so rare that Rust doesn't really being anything superior to the table in terms of safety, reliability, or efficiency. More dangerous for Ada than not adding enough features is adding too many features for fickle reasons, especially for trying to win popularity contests or saying "me too". While I agree with you that we can't let SPARK hold back Ada, I'm not convinced that Ada is going to attract any new users on features. At best it will retain existing (probably commercial) users who are considering switching to other languages. If Ada wants to attract new users, it has to do it by being more accessible, and less commercial. If Ada wants to differentiate itself, it should do so by being the sane, mature, carefully designed language that is always has been. If it stops being that, it stops being special. Just my two cents (1.5 c USD) **************************************************************** From: Claire Dross Sent: Friday, January 17, 2020 7:46 PM > Interesting. Do those 20% use pointers at all? If not, maybe a > restriction asking for no pointer dereference could reconcile the two > views? If we want to go this way, maybe we could consider requiring constants containing access-to-variable parts to be listed in the global contract (this could be fair, since in Ada, these constants really are variables). Then checking whether a subprogram is well-behaved (its global contract + parameters is an over-approximation of its effects) could be as simple as checking that its parameters / globals have no access-to-variable/aliased parts (please sanity check me on this, I am not that knowledgeable about the crazy things that can happen in full Ada). When we have ownership types, well-behaved subprograms could use them (provided we manage to make parameter mode consistent on them). **************************************************************** From: Claire Dross Sent: Friday, January 17, 2020 8:57 PM Please, could we avoid adding fuel to the fire here? I think we are all working toward the same goal (making Ada a better language, and if possible more attractive) and I don't think a schism would serve anybody. As for SPARK, I think (I hope?) it may serve to bring people to Ada. This does not mean the ARG *should* take it into account when designing Ada. But it is just another tool of the eco-system, so I think that if something makes its life harder, it can be mentioned as a drawback, just like for any other tool for Ada. **************************************************************** From: Randy Brukardt Sent: Friday, January 17, 2020 9:43 PM > > Interesting. Do those 20% use pointers at all? If not, maybe a > > restriction asking for no pointer dereference could > > reconcile the two views? > > If we want to go this way, maybe we could consider requiring constants > containing access-to-variable parts to be listed in the global > contract (this could be fair, since in Ada, these constants really are > variables). I believe the AI12-0079-1 proposal and its various fixes did that. Not sure if Tucker carried that over into the AI12-0079-2 proposal, but I would hope so. In full Ada, only a few "constants" are really known to be constant. See 3.3(13/3), specifically the part about "inherently mutable". This happens because of the possibility of writable self-pointers being constructed during initialization. The definition of "variable" that had to be included in Global was: The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) global to a callable entity ... (This is 6.1.2(12/5) in the Draft 23 RM: http://www.ada-auth.org/standards/2xaarm/html/AA-6-1-2.html.) Private types have to be included since Legality Rules depend on this definition, and we don't want to break privacy for high-level Legality Rules. (There are only a few rules that break privacy, and most are related to Chapter 13 representation stuff.) This isn't as bad as it sounds, as there aren't that many library-level constants of private types (at least not in my code) -- those would require some sort of constructor which wouldn't be preelaborable. At least in my code, most of the constant globals are numbers and data tables which are none of the things above. > Then checking whether a subprogram is well-behaved (its global contract > + parameters is an over-approximation of its effects) could be as + simple > as checking that its parameters / globals have no > access-to-variable/aliased parts (please sanity check me on this, I am > not that knowledgeable about the crazy things that can happen in full Ada). See above. :-) > When we have ownership types, well-behaved subprograms could use them > (provided we manage to make parameter mode consistent on them). The "overriding" thing for the original Global proposal allowed changing the effective mode only for the purposes of Global. (You can see that in the wording for the draft 23 RM.) That or some equivalent functionality is kinda necessary if we're going to use this on packages like Text_IO and Discrete_Random (we hardly can change the modes at this late date in them). Users write stuff like that, too, probably because they're patterning on package like Text_IO and Discrete_Random. :-) **************************************************************** From: Claire Dross Sent: Saturday, January 18, 2020 4:33 PM ... > This isn't as bad as it sounds, as there aren't that many > library-level constants of private types (at least not in my code) -- > those would require some sort of constructor which wouldn't be > preelaborable. At least in my code, most of the constant globals are > numbers and data tables which are none of the things above. I understand that, but I am not sure I think this is a good idea. I still feel like we are doing to much over-approximation for a compile time verification. When doing a static analysis tool, we are always faced to the difficult challenge of coming up with a correct trade-off between precision and correction. AFAIK, very few people are OK with having a tool emitting a lot of false alarms or require an heavy annotation burden, and so, even if the guarantees offered are important (full functional correctness, absence of RTE...). Unfortunately, this seems to be also true in safety critical domains (from the user feed-back we get on codepeer and spark). And I fear this feature will have too much of both (annotation burden +false alarms) for a limited interest. This is why I am trying to push toward something simple with as little annotation burden and as little false alarms as possible. ... >> When we have ownership types, well-behaved subprograms could use them >> (provided we manage to make parameter mode consistent on them). > The "overriding" thing for the original Global proposal allowed > changing the effective mode only for the purposes of Global. (You can > see that in the wording for the draft 23 RM.) That or some equivalent > functionality is kinda necessary if we're going to use this on > packages like Text_IO and Discrete_Random (we hardly can change the modes > at this late date in them). > Users write stuff like that, too, probably because they're patterning > on package like Text_IO and Discrete_Random. :-) See above... **************************************************************** From: Raphael Amiard Sent: Monday, January 20, 2020 4:56 AM >. Ada 202x will need some things that will attract new users to Ada. >> Otherwise, Ada will just gradually lose users as they retire or move to >> other things. I don't think delta aggregates are going to excite anyone >> (although existing Ada users will find them handy). > While I agree with this in principle, I strongly believe that Ada already > has features that are far ahead of other comparable languages. Rust, the > closest "competitor" to Ada, has a lot of problems - and I'd argue that this > is mostly due to their single focus on memory safety and not much else. > Let's not get caught up with who is the hottest kid on the block this year. > In our practical experience, Ada already makes memory problems so rare that > Rust doesn't really being anything superior to the table in terms of safety, > reliability, or efficiency. This attitude is really concerning to me. I'm seeing it play out everywhere in our community, and it is very strong at the ARG too. I did not yet have the pleasure to meet you in person at an ARG meeting but I have read a lot of your mails and I feel it too: "Our language is superior yet doomed, and other communities have not understood what makes it so great" (I'm making the strokes bold here). Rust has much more going for it than memory safety. Funnily enough, while we're trying to figure out how to do safe parallelism, they've actually had the problem solved since a few years ago (https://blog.rust-lang.org/2015/04/10/Fearless-Concurrency.html). Hint: ownership is not solely about memory. It's about resources, and aliasing of them, and having a sound static model to analyze those. This model is exactly what we're missing to make parallelism safe, hence very related to this AI. Beyond ownership, the trait system, a powerful generic model, and error handling that is much easier to statically analyse than Ada's unchecked exceptions are domains where you could claim that Rust is superior in terms of safety to Ada. There would be a debate, but outright claiming that Rust "only has memory safety" and Ada is "superior in every other way" is an over simplification of reality, to the point of being simply incorrect. > More dangerous for Ada than not adding enough features is adding too many > features for fickle reasons, especially for trying to win popularity > contests or saying "me too". I agree with you here. Actually I think there would be a lot more to do for Ada's popularity at the implementation/ecosystem/tooling/teaching level than at the language level. And even at the language level, reducing inconsistencies and making the language more globally coherent would be *much more valuable* than adding tons of new features: We're not C++. We don't have a large user base to try and keep, our user base is already pretty small, and they're not updating language versions (most of them at least). That means that if we're trying to attract users, they're going to be new users, or old users on new projects. > While I agree with you that we can't let SPARK hold back Ada, ... I'm going to be bold again, but in terms of popularity and appeal to programmers in the large, SPARK is one of the only reasons Ada is interesting to new users. In terms of safety it's a language that is in effect more safe than every other alternatives (including Rust), but yet more usable and production ready than other research-y alternatives. From my point of view it has the unique value proposition that Ada is missing (while still being a great language). **************************************************************** From: Richard Wai Sent: Monday, January 20, 2020 11:14 AM > This attitude is really concerning to me. I'm seeing it play out everywhere > in our community, and it is very strong at the ARG too. I did not yet have > the pleasure to meet you in person at an ARG meeting but I have read a lot > of your mails and I feel it too: > "Our language is superior yet doomed, and other communities have not > understood what makes it so great" (I'm making the strokes bold here). I have never felt Ada was doomed, nor do I think it is broadly superior to everything. What I do think is that Ada is both unique and uniquely proven for general purpose programming - which is most programming. Rust is talking about things - safety and correctness - that Ada has been dealing with since 1983. Unlike Ada, Rust ignores all of the subtle but key ideas of readability, rich abstraction, separate compilation, and data modeling. Ada is not doomed, just as Rust is not proven. Let's please try to see the forest for the trees. > Beyond ownership, the trait system, a powerful generic model, and error > handling that is much easier to statically analyse than Ada's unchecked > exceptions are domains where you could claim that Rust is superior in > terms of safety to Ada. You mean the error handling model where you need to explicitly deal with every possibly return condition on every function, and if you don't deal with every possibility the entire program crashes? Yeah that sounds great for static analysis, but what about the programmer? That's brutal, and frankly the single worst part about programming in Rust, IMO. It's almost as bad as the try-catch approach to exception handling. Good thing we have Ada which handles these problems rationally, and in a way that is very natural and powerful to work with. > There would be a debate, but outright claiming that Rust "only has memory > safety" and Ada is "superior in every other way" is an over simplification > of reality, to the point of being simply incorrect. I'm not coming from a theoretical standpoint here, I'm coming from a purely practical standpoint. And this is an issue that I see as getting dangerously worse lately. I care about using Ada to build real applications - not to research computer science, or to reimplement someone's pet algorithm. Your (and others at AdaCore) fixation on static analysis concerns me. I understand the value of formal methods and static analysis, but I'm not sure your camp appreciates the practical viability (read: economics) in large, non safety-critical, non-embedded domains. For this point, suffice it to say that Rust has a lot of problems stemming from their very "nice on paper" approach, which has been less than nice in practice. Ownership is a neat concept, but used "in real life", it ends up being very restrictive and challenging to get actual work done. I mean actual work as in actual living applications or libraries that do real useful things, not cute little micro-package crates. I'm talking about large applications or frameworks that serve general needs. Rust is struggling with this issue now and the community knows it. Getting practical things to work in that ownership model leads to prevent and egregious use of "unsafe", defeating the entire purpose - take note of the recent Actix-web drama. Ada has tried very hard for very long to avoid falling into that trap - of making the user tempted to always turn off checking and use unsafe approaches, just to get the work done, because it's simply too difficult and time-consuming to do it otherwise. All this talk about Rust and ownership and safety always leaves out Ada's greatest strengths - strengths of structure, discipline, and realistic, rather than idealized rules. Ada is mature and realistic, Rust is not. And yes, it may be one day, but we are not going to compete with that by being less confident in Ada. What I'm saying is - let's not forget about the true strengths of Ada. You need to compare the strengths with the weakness, not in exclusion. > I'm going to be bold again, but in terms of popularity and appeal to > programmers in the large, SPARK is one of the only reasons Ada is > interesting to new users. In terms of safety it's a language that is in > effect more safe than every other alternatives (including Rust), but yet > more usable and production ready than other research-y alternatives. From > my point of view it has the unique value proposition that Ada is missing > (while still being a great language). Respectfully, is it the perspective of AdaCore? Otherwise I don't see how you can talking about what interests new users. Because new AdaCore users /= new Ada users. I should know, we are one of those new users. Unless you're a large corporation - say if you're startup, you're frankly going to be using FSF GNAT, not GNAT Pro. I've seen it time and again. The other userbase AdaCore likely sees is the academic community - which are unsurprisingly interested in theoretical things, so are unsurprisingly excited about SPARK. That's not to say that SPARK is not practical, it is. It's to say that SPARK is especially exciting to the theoretical-minded people. I think suggesting that SPARK is the only thing attracting new users to Ada is frankly hubris. Mainstream uses (like us) crucial to the future of Ada, if not the literal future of Ada. Users that develop mainstream software for mainstream problems - things like web applications, or enterprise business logic. This kind of software is becoming ever more critical, and benefits every more from reliability, safety, and security. But this is software that is very large and very dynamic, and is built by large teams on aggressive schedules. I say this future because if you want Ada to actually grow its user base - that's where the growth needs to happen, since that is where the vast majority of the action is. In these contexts, SPARK is limited to the specific parts where you need especially high performance or especially high safety and security. It is not economical to apply SPARK to very large applications where exceptions are not a concern - but that is somewhere where Ada shines. I argue vehemently that Ada is better at building very large applications than any other language in practical use today. And this is where most problems with software lies - problems that arise from complexity, maintenance, and testing. Problems in keeping separate teams out of eachother's hair. These are all immensely valuable traits. And they are not things that SPARK or Rust do anything about. Static analysis and formal methods do not make software easier to read - but that's actually where software spends most of its time. Look, we love SPARK, it's very cool - but it is not practical as the main language of use for general-purpose software. Ada is. I'm increasingly concerned that the SPARK people, and AdaCore at large, want to make Ada less general-purpose, and more niche than it already is. I think that is a travesty because Ada was always designed to be general-purpose, and was always designed for "programming in the large". And you should know that I will fight tooth-and-nail to make this point heard. **************************************************************** From: Raphael Amiard Sent: Friday, January 31, 2020 7:45 AM I took a very long time to answer that, because a lot of what you write seems exactly like the kind of unsubstantiated claims that I was trying to avoid in the first place. In some places what you write is subjective opinions stated as truth, like "Ada is mature and realistic, Rust is not". In other places, it's simply completely inaccurate, like your vision of the use of Rust today, in "micro"/"cute"/"toy" frameworks, disregarding the heaps of very serious production software that is being written with Rust today. You're perfectly capable of finding this information, should you wish to do so, but just to cite a few examples: - Mozilla Firefox ships with a large portion of code written in Rust nowadays - A large part of Cloudflare's infrastructure is written in Rust - Amazon has an hypervisor used in production written in Rust This extends to your opinions on language design and features, such as error handling. I'll send you an article that I truly love about error handling, http://joeduffyblog.com/2016/02/07/the-error-model/, that I'd highly advise anyone to read. It is highly articulate, documented, argumented, and balanced, making it clear that if there was a silver bullet we would probably have found it some time ago. Your position as you expressed it in the previous message, lacks those qualities. It's black and white and full of contempt. For me, while this is a common way of writing on, for example, comp.lang.ada (which is regrettable in itself) this is definitely not acceptable in a forum where professionals conduct language design. We should at the very least be able to have reasonable and documented positions, and, most importantly, balanced positions, where we acknowledge the complexity of our field and of the drawbacks game that language design is. Please think over this and the tone of your message, in particular with regards to Rust (I'll brush over the SPARK/AdaCore part since it's a very different topic, and you already discussed it a bit with Arnaud). Also please consider that it should be part of your duty as an ARG member to have balanced positions on such topics, and know the pros and cons of various approaches. It might be the case, but if it is, you didn't show it in your message. **************************************************************** From: Randy Brukardt Sent: Friday, January 31, 2020 4:27 PM > I took a very long time to answer that, because a lot of what you write > seems exactly like the kind of unsubstantiated claims that I was trying to > avoid in the first place. Not sure who or what you are responding to since you didn't quote any of it. ... >We should at the very least be able to have reasonable and documented >positions, and, most importantly, balanced positions, where we acknowledge >the complexity of our field and of the drawbacks game that language design >is. That's not the reality of e-mail discussions. Most of us here were "trained" by Robert Dewar to respond quickly to relevant messages, and that necessarily is going to cause positions that aren't as thought out as would be ideal. Moreover, most of us can't spend 4 hours pondering positions and alternatives and researching every topic that comes up, especially given the volume of mail on this list. I've made many points over the years that distracted from the critical topic and that I find embarassing when I reread them while filing mail. (And just as many questions I wish I had asked at the time.) That's the nature of the beast. ****************************************************************