CVS difference for ai12s/ai12-0079-1.txt

Differences between 1.10 and version 1.11
Log of other versions for file ai12s/ai12-0079-1.txt

--- ai12s/ai12-0079-1.txt	2017/09/07 02:53:23	1.10
+++ ai12s/ai12-0079-1.txt	2017/10/03 01:58:22	1.11
@@ -1,4 +1,4 @@
-!standard 6.1.2(0)                                  17-06-12    AI12-0079-1/04
+!standard 6.1.2(0)                                  17-09-25    AI12-0079-1/05
 !class Amendment 13-06-28
 !status work item 13-06-28
 !status received 13-06-14
@@ -127,7 +127,7 @@
 For a program unit, for a formal package, formal subprogram, formal
 object of an anonymous access-to-subprogram type, and for a named
 access-to-subprogram type or composite type (including a formal type),
-the following language-defined representation aspect may be specified
+the following language-defined aspect may be specified
 with an aspect_specification (see 13.1.1):
 
 Global
@@ -136,40 +136,35 @@
    is as follows:
 
     global_aspect_definition ::=
-        primitive_global_aspect_definition
+        Synthesized
+      | primitive_global_aspect_definition
       | /global_/attribute_reference
       | global_aspect_definition & /global_/attribute_reference
 
-OLD STYLE:
     primitive_global_aspect_definition ::=
-        global_set | (global_mode => global_set{, global_mode => global_set})
-
-    global_mode ::= Input | In_Out | Output | Proof_In
-
-    global_set ::=
-         global_name
-       | (global_name{, global_name})
-       | ALL | SYNCHRONIZED | NULL
-
-NEW STYLE:
-    primitive_global_aspect_definition ::=
          NULL
        | global_mode global_name
        | global_mode global_designator
        | (global_mode global_set{, global_mode global_set})
 
-    global_mode ::= in | in out | out | proof in
+    global_mode ::= [ global_mode_qualifier ] basic_global_mode
 
+    global_mode_qualifier ::=
+         SYNCHRONIZED
+       | /implementation-defined_/identifier
+
+    basic_global_mode ::= IN | IN OUT | OUT
+
     global_set ::=
          global_name {, global_name}
        | global_designator
 
-    global_designator ::= ALL | SYNCHRONIZED | NULL
+    global_designator ::= ALL | NULL
 
-------
-
     global_name ::=
-        /object_/name | /package_/name | /access_/subtype_mark
+        /object_/name
+      | /package_/name [ PRIVATE ]
+      | /access_/subtype_mark
       | ACCESS subtype_mark
 
    A /global_/attribute_reference is an attribute_reference with attribute
@@ -222,19 +217,36 @@
 assignment, or finalization of an object of the type. The Global aspect
 for an access-to-subprogram object (or type) identifies the global
 variables that might be referenced when calling via the object (or any
-object of that type).  In the following we talk in terms of operations;
+object of that type).  The following is defined in terms of operations;
 the rules apply to all of these kinds of entities.
 
 The sets of global variables associated with a Global aspect can be
 defined explicitly with a primitive_global_aspect_definition or can be
 defined by combining with the sets specified for other entities by
-referring to their Global attribute. The global variables associated
-with any mode can be read as a side
+referring to their Global attribute. Alternatively, the Global aspect may
+be defined using the aspect-specific identifier "Synthesized" which means
+the implementation will determine in an implementation-defined manner
+the sets of global variables that might be referenced by uses of the entity.
+
+The global variables associated with any mode can be read as a side
 effect of an operation.  The IN OUT and OUT global_modes together
 identify the set of global variables that can be updated as a side
-effect of an operation.  The overall set of objects associated with
+effect of an operation.  The global_mode_qualifier SYNCHRONIZED reduces
+the set to those objects that are of one of the following sort of types:
+
+  * a protected, task, or synchronized tagged type;
+  * an atomic type;
+  * a descendant of the language-defined types Suspension_Object
+    or Synchronous_Barrier;
+  * a record type all of whose components are *sychronized* in this sense.
+
+An implementation-defined global_mode_qualifier may be specified, which
+reduces the set according to an implementation-defined rule.
+
+The overall set of objects associated with
 each global_mode include all objects identified for the mode in the
-primitive_global_aspect_definition, if any, plus all objects
+primitive_global_aspect_definition (subject to the global_mode_qualifier),
+if any, plus all objects
 associated with the given mode for the entities identified by the
 prefixes of the /global_/attribute_reference's, if any.
 
@@ -242,9 +254,6 @@
 
    * "null" identifies the empty set of global variables;
    * "all" identifies the set of all global variables;
-   * "synchronized" identifies the set of all global variables that are
-     either of a protected type, a task type, an atomic type, or a record
-     or array all of whose components are "synchronized" in this sense;
    * "global_name{, global_name}" identifies the union of the
      sets of variables identified by the global_name's in the list.
    * for the four forms of global_name:
@@ -254,7 +263,10 @@
      * /package_/name identifies the set of all variables declared within
        the declarative region of the package having the same accessibility
        level as the package, but not including those within the declarative
-       region of a public child of the package;
+       region of a public child of the package; if the reserved word PRIVATE
+       follows the /package_/name, the set is reduced to those variables
+       declared in the private part or body of the package or within a
+       private descendant of the package;
      * /access_/subtype_mark identifies the set of (aliased) variables that
        can be designated by values of the given access-to-variable type;
      * ACCESS subtype_mark identifies the set of (aliased) variables that
@@ -264,28 +276,29 @@
     Legality Rules
 
 Within a primitive_global_aspect_definition, a given global_mode shall
-be specified at most once. Similarly, within a
+be specified at most once without a global_mode_qualifier, and at most
+once with any given global_mode_qualifier. Similarly, within a
 primitive_global_aspect_definition, a given entity shall be named at
-most once by a global_name, and the reserved words ALL and SYNCHRONIZED
-shall appear at most once.
+most once by a global_name.
 
 If an entity has a Global aspect other than IN OUT ALL, then the
 associated operation(s) shall read only those variables global to the
-entity that are within the *global variable set* associated with the IN,
+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*
+variables global to the entity that are within the global variable set
 associated with either the IN OUT or OUT global_modes. This includes any
 calls occurring during the execution of the operation, presuming those
 calls read and update all global variables permitted by their Global
-aspect (or Global'Class aspect, if a dispatching call). If a variable
-global to the entity is read that is within the *global variable set*
-associated with the OUT global_mode, it shall be updated somewhere
-within the callable entity (or an entity it calls). The variables global
-to the entity that are within the *global variable set* associated with
-the PROOF IN global_mode shall be read only within an assertion
-expression of the callable entity, or another entity
-that it calls.
+aspect (or Global'Class aspect, if a dispatching call).
 
+If a variable global to the entity is read that is within the global variable
+set associated with the OUT global_mode, it shall be updated somewhere
+within the callable entity (or an entity it calls).
+
+If an implementation-defined global_mode_qualifier applies to a given
+set of variables, an implementation-defined rule determines what sort
+of references to them 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
@@ -318,7 +331,10 @@
 All of the global in, in-out, and out annotations proposed can be
 statically checked.
 
-We have provided a proof-in mode for use within assertion expressions.
+We have allowed for an implementation-defined global_mode_qualifier, which
+would allow "proof in" for SPARK.  Similarly, we have allowed for
+a aspect-specified identifier "Synthesized" to indicate that the implementation
+will determine the global objects referenced by uses of the entity.
 
 We have allowed reading of "out" mode globals, so long as there is at least
 one update of the global variable as well.
@@ -326,7 +342,7 @@
 Note that it is possible to lie about the use of globals of subprograms
 and other entities that are imported. This is of course impossible to
 check, but thankfully is covered by B.1(38.1/2). Incorrect annotations
-on imported subprograms could cause a program to be erroneous.
+on imported subprograms could cause a program's execution to be erroneous.
 
 SPARK does not currently support identifying particular components of a
 global variable in the Global aspect, but for Ada we plan to allow that.
@@ -345,7 +361,6 @@
 for those callers that have visibility on the body.  This could be added
 at a later point if it was felt to be important.
 
-
 !example
 
    package Random is
@@ -918,8 +933,8 @@
 From: Tucker Taft
 Sent: Tuesday, June 13, 2017  3:54 AM
 
-> (1) Not sure why you have "OLD STYLE" and "NEW STYLE" grammars. It 
-> just looks confusing. "Old Style" is cheap beer, not something that 
+> (1) Not sure why you have "OLD STYLE" and "NEW STYLE" grammars. It
+> just looks confusing. "Old Style" is cheap beer, not something that
 > belongs in an AI. ;-)
 
 I left it there purely for comparison.  Initially I thought I would keep the
@@ -927,9 +942,9 @@
 presume we go with the new style.  So  better would probably be to put the
 OLD STYLE stuff in the !discussion or the !proposal.
 
-> (2) The "New Style" grammar contains "proof" explicitly like a 
-> reserved word. Are you proposing a new reserved word, to fight about 
-> unreserved keywords yet again (this seems like a perfect use for such 
+> (2) The "New Style" grammar contains "proof" explicitly like a
+> reserved word. Are you proposing a new reserved word, to fight about
+> unreserved keywords yet again (this seems like a perfect use for such
 > a thing), or something else??
 
 Good question.  Perhaps it should just be "<identifier> IN” from a syntax
@@ -938,12 +953,12 @@
 
 > (3) "/object_/name identifies the specified global variable (or
 > non-preelaborable constant, which is ignored for the purposes of the
-> remaining rules)" I'm not sure "ignored" is the right way to put this. 
-> I think you're trying to say that the possibility of non-preelaborable 
-> constants isn't mentioned in later rules. But that's a bit weird, 
-> because many of the later rules talk only about variables, and it 
-> would seem easy enough to talk about "objects", at least in the three 
-> following rules. Or maybe describe them as a term covering variables 
+> remaining rules)" I'm not sure "ignored" is the right way to put this.
+> I think you're trying to say that the possibility of non-preelaborable
+> constants isn't mentioned in later rules. But that's a bit weird,
+> because many of the later rules talk only about variables, and it
+> would seem easy enough to talk about "objects", at least in the three
+> following rules. Or maybe describe them as a term covering variables
 > and non-preelaborable constants.
 
 I tried to do that and it just started getting really complicated.  So I
@@ -954,11 +969,11 @@
 pretty closely to what SPARK requires, but it is probably just confusing to
 give only part of that.
 
-> (4) Minor glitch: You ought to only italicize the defining occurrence 
-> of a term, you've got every occurrence of "global variable set" in 
-> italics (signified by surrounding by *s). [BTW, wouldn't it be better 
-> to call this a "global object set", since some constants are included? 
-> Rather than telling people to "ignore" the possibility of a constant 
+> (4) Minor glitch: You ought to only italicize the defining occurrence
+> of a term, you've got every occurrence of "global variable set" in
+> italics (signified by surrounding by *s). [BTW, wouldn't it be better
+> to call this a "global object set", since some constants are included?
+> Rather than telling people to "ignore" the possibility of a constant
 > being included? Why lie if you don't have to?]
 
 Sorry about that.  Yes I began to notice too many “*”s there, but didn’t have
@@ -970,16 +985,16 @@
 Sent: Tuesday, June 13, 2017  1:15 PM
 
 ...
-> > (3) "/object_/name identifies the specified global variable (or 
-> > non-preelaborable constant, which is ignored for the purposes of the 
+> > (3) "/object_/name identifies the specified global variable (or
+> > non-preelaborable constant, which is ignored for the purposes of the
 > > remaining rules)" I'm not sure "ignored" is the right way to put this.
 ...
-> I tried to do that and it just started getting really complicated.  So 
-> I punted and chose to allow a name that refers to a non-preelaborable 
-> constant, but otherwise ignoring it later.  I agree the wording needs 
-> work.  Perhaps better would be to just allow an implementation-defined 
+> I tried to do that and it just started getting really complicated.  So
+> I punted and chose to allow a name that refers to a non-preelaborable
+> constant, but otherwise ignoring it later.  I agree the wording needs
+> work.  Perhaps better would be to just allow an implementation-defined
 > extension to the syntax, and not talk about it further.
-> Non-preelaborable constants match pretty closely to what SPARK 
+> Non-preelaborable constants match pretty closely to what SPARK
 > requires, but it is probably just confusing to give only part of that.
 
 I thought that just generally replacing "variable" by "object" in your wording
@@ -996,7 +1011,7 @@
 From: Florian Schanda
 Sent: Thursday, June 15, 2017  2:20 AM
 
-> Sorry to be so late.  Hopefully Randy is still in Wisconsin.  I 
+> Sorry to be so late.  Hopefully Randy is still in Wisconsin.  I
 > switched over to using in, in out, out.
 
 I like the new syntax you propose, in a way we've come full circle (SPARK 2005
@@ -1019,7 +1034,7 @@
 Sent: Thursday, June 15, 2017  3:32 AM
 
 > ...
-> At the risk of asking a silly question, does proof in make sense as a 
+> At the risk of asking a silly question, does proof in make sense as a
 > parameter mode?
 
 I presume you mean for a subprogram.  If we go that route, it would seem to
@@ -1029,10 +1044,10 @@
 "abstract" or "null," and in object declarations where the word "constant"
 or "aliased" might appear.
 
-> Of course Tuck, if Ada adopts your syntax as its Global syntax then 
-> we're going to have a bit of fun in SPARK trying to make this 
-> backwards/forwards compatible. I suspect the SPARK extension will then 
-> just say "you can use Input as synonym for in, and you can't use both 
+> Of course Tuck, if Ada adopts your syntax as its Global syntax then
+> we're going to have a bit of fun in SPARK trying to make this
+> backwards/forwards compatible. I suspect the SPARK extension will then
+> just say "you can use Input as synonym for in, and you can't use both
 > in the same global aspect, etc.”?
 
 You will have to use "Input =>" as equivalent to "in".  The "=>" will be
@@ -1043,7 +1058,7 @@
 From: Florian Schanda
 Sent: Thursday, June 15, 2017  8:19 AM
 
-> You will have to use "Input =>" as equivalent to "in".  The "=>" will 
+> You will have to use "Input =>" as equivalent to "in".  The "=>" will
 > be the most important discriminator, I think.
 
 There will be some pain to make sure this is not possible:
@@ -1078,7 +1093,7 @@
 
 ...
 > There will be some pain to make sure this is not possible:
-> 
+>
 > with Global => (Input => X,
 >                out X)
 
@@ -1087,8 +1102,8 @@
 committed to non-reserved-word modes with “=>”.
 
 ...
-> It may be worth to allow these as shorthands for the "in". It would 
-> also mirror parameters (missing mode = in) and really globals are a 
+> It may be worth to allow these as shorthands for the "in". It would
+> also mirror parameters (missing mode = in) and really globals are a
 > kind of parameter ;)
 
 I considered this and ultimately rejected it, as being a short-hand that just
@@ -1121,7 +1136,7 @@
 name these arrays in the specification.
 
 It really doesn't matter which global arrays the client accesses, so long as
-only the specified slice of those arrays is accessed. For example, one client 
+only the specified slice of those arrays is accessed. For example, one client
 might sum arrays A and B into C, and another client might sum arrays D and E
 into F. It doesn't matter which arrays are accessed, the library guarantees
 that the slices wont overlap, which can be viewed as a post condition that the
@@ -1138,7 +1153,7 @@
 general challenge associated with mentioning things in a “Global” annotation
 that are not normally visible in the spec.  SPARK solves this by allowing the
 programmer to invent a notion of “abstract state,” and then defining what that
-abstract state comprises in the body.  
+abstract state comprises in the body.
 
 On the other hand, this seems like excessive complexity for Ada, and in some
 sense harkens back to the days when global variables were used for all kinds
@@ -1159,21 +1174,21 @@
 From: Randy Brukardt
 Sent: Tuesday, September 5, 2017  7:20 PM
 
-> I don't see the point of solving this problem only for arrays, when 
-> there is a general challenge associated with mentioning things in a 
+> I don't see the point of solving this problem only for arrays, when
+> there is a general challenge associated with mentioning things in a
 > "Global" annotation that are not normally visible in the spec.
 
 Right. This is just part of a much more general problem.
 
 > SPARK solves this by allowing
-> the programmer to invent a notion of "abstract state," and then 
+> the programmer to invent a notion of "abstract state," and then
 > defining what that abstract state comprises in the body.
-> 
-> On the other hand, this seems like excessive complexity for Ada, and 
-> in some sense harkens back to the days when global variables were used 
-> for all kinds of inter-module communication.  My own view is that we 
-> should be discouraging the use of global variables, and instead rely 
-> on Ada's support for passing slices if we want to give a subprogram 
+>
+> On the other hand, this seems like excessive complexity for Ada, and
+> in some sense harkens back to the days when global variables were used
+> for all kinds of inter-module communication.  My own view is that we
+> should be discouraging the use of global variables, and instead rely
+> on Ada's support for passing slices if we want to give a subprogram
 > access to only a particular slice of an array.
 
 That doesn't fix anything in the case of generic units, though. I was rather
@@ -1230,16 +1245,265 @@
 
 The SPARK scheme would work for that, but it seems like overkill.
 
-> Note that even eliminating global annotations completely doesn't solve 
-> the issue of compile-time checking of data races, given that we could 
-> pass two different slices of the same array to two different parallel 
-> calls.  To ensure these two slices don't overlap, we would probably 
-> still need to define run-time checks to ensure there is no overlap, 
-> with many compilers (hopefully) being able to eliminate the check at 
+> Note that even eliminating global annotations completely doesn't solve
+> the issue of compile-time checking of data races, given that we could
+> pass two different slices of the same array to two different parallel
+> calls.  To ensure these two slices don't overlap, we would probably
+> still need to define run-time checks to ensure there is no overlap,
+> with many compilers (hopefully) being able to eliminate the check at
 > compile-time.
 
 Yes, that seems reasonable. Perhaps we have to handle race conditions arising
 from Atomic object misuse the same way? (Updates like Atom := Atom + 1; are
 not safe as these are separate reads and writes.)
+
+****************************************************************
+
+From: Brad Moore
+Sent: Saturday, September 16, 2017  1:13 PM
+
+>> I don't see the point of solving this problem only for arrays, when
+>> there is a general challenge associated with mentioning things in a
+>> "Global" annotation that are not normally visible in the spec.
+> Right. This is just part of a much more general problem.
+
+OK, but I now am proposing a more general solution to the more general
+problem, at least generalizing this to work for both arrays and containers.
+
+Instead of the array keyword that I suggested earlier, suppose we
+extended the global aspect to include the syntax form;
+
+       global => all (name1 .. name2)
+
+The idea here is that this indicates that the only use of globals is via
+indexing lookups (via a range of scalar indexes, or container cursors).
+The keyword "all" here represents all visible globals. Specific global
+names could be used also, with the same index/slicing syntax.
+
+The compiler would do the normal processing for global checks, but if
+the only use of globals is via the specified slice of the container or
+array, then the global check would pass.
+
+We could say that this implies that the only use of these globals is via
+a  loop cursor of a for loop that mentions name1 and name2 to initialize
+the loop cursor, so I would think it would be pretty easy for the
+compiler to check this.
+
+To do a slice of a container, we just need an iterator that can operate
+on a slice of a container.
+
+The existing containers almost already support this, because there
+exists Iterate calls that allow you to specify the start of iteration.
+
+eg. For Doubly_Linked_Lists
+
+     for Item in My_List.Iterate (Start => My_Cursor) loop
+        ....
+     end loop;
+
+If we had an Iterate call that allowed you to specify both the Start and
+the Finish cursors, then one could write;
+
+     for Item in My_List.Iterate (Start => My_Start_Cursor, Finish =>
+My_End_Cursor) loop
+        ....
+     end loop;
+
+In fact, I don't know why we don't already have these calls. They would
+be more useful than the ones we have today that allow you to only
+specify the start cursor, with the end cursor implicitly being
+container.Last;
+
+C++ iterators for instance allow one to iterate through a subset of an
+array or container. It seems like
+useful functionality.
+
+We could either add a default parameter for Finish that defaults to
+Last, or add a new call for the Container libraries.
+
+As a simple example of the global syntax, consider a very basic parallel
+loop library;
+Note I am using Randy's 'global attribute, as I think it is needed also.
+
+generic
+    type Loop_Index is range <>;
+
+    with procedure Process (Start, Finish : Loop_Index)
+           with Pre    => (Start < Finish),       -- Can we currently
+put pre and post on formals?
+                  Global => all (Start .. Finish);  --
+package Parallel is
+
+    procedure Parallel_Loop
+      (From : Loop_Index := Loop_Index'First;
+       To   : Loop_Index := Loop_Index'Last);
+       with Process'Global and Global => null;
+
+end Parallel;
+
+package body Parallel is
+
+    procedure Parallel_Loop
+      (From    : Loop_Index := Loop_Index'First;
+       To      : Loop_Index := Loop_Index'Last)
+    is
+       task type Worker (Start_Index, End_Index : Loop_Index);
+
+       task body Worker is
+       begin
+          Process (Start_Index, End_Index);
+       end Worker;
+
+       Left_End : constant Loop_Index := From + ((To - From + 1) / 2) - 1);
+
+       Left_Worker :  Worker (Start_Index => From,
+                              End_Index => Left_End;
+       Right_Worker : Worker (Start_Index => Left_End + 1,
+                              End_Index => To);
+    begin --  Parallel_Loop
+       null;
+    end Parallel_Loop;
+
+end Parallel;
+
+I could show a similar example for a parallel container iteration,
+library call
+but thought it best for now to just show a simple array case.
+
+In fact I have a single generic library call that can be used for both
+array and container iteration,
+and I think the global => all (name1 .. name2) syntax would work for
+both cases for different
+instantiations of the same generic.
+
+One reason why I think this is important is because for such library
+calls, the abstraction is
+to only provide parallel chunking over a range of cursor/index.
+
+The client may use this to operate on any number of global references.
+
+For example, calculate the sum of integers from 1 .. N involves 0 arrays.
+Increment all the values of an array involves 1 array.
+Add Array1 to Array2 involves 2 arrays.
+Add Array1, and Array2, to Array 3 arrays.
+
+One library call can be used to handle all these cases. If one were to
+pass the globals into the
+library call by naming them, then I think you would need an infinite
+number of library calls to be written to handle all the possible cases.
+Using globals in this manner, one library call can be used to do all
+parallel looping problems.
+
+...
+>> Note that even eliminating global annotations completely
+>> doesn't solve the issue of compile-time checking of data
+>> races, given that we could pass two different slices of the
+>> same array to two different parallel calls.  To ensure these
+>> two slices don't overlap, we would probably still need to
+>> define run-time checks to ensure there is no overlap, with
+>> many compilers (hopefully) being able to eliminate the check
+>> at compile-time.
+
+Yes, in the example above it seems pretty obvious by inspection in the
+package body that there can be no overlap. Hopefully the compiler can be
+smart enough to see that also.
+We might want to define some sort of aspect or attribute
+    (Overlap => False? Covered_Once => True?) that tells the compiler to
+add these checks.
+
+In the absence of those checks and with the compiler not being able to
+prove that the calls to Process in my example above are non-overlapping,
+we might want to allow the programmer to suppress the
+global checking on the call from inside the body.
+
+There is still value though to the global all slicing aspect even if the
+global checking is suppressed in the body of the library because it can
+ensure at least that the clients of the library call are well behaved. If
+the library call itself can be  trusted to not call the client with
+overlapping ranges, it seems valuable to the client to have the compiler
+reject compilations where the client is accessing globals in an unsafe
+manner. The global => all(name1 .. name2) on the callback formal subprogram
+would provide the check on the clients code.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, September 25, 2017  4:33 PM
+
+Here is the first piece of my ARG homework.  Mostly I tried to fix up the
+syntax according to our discussions in Vienna.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, October 2, 2017  8:53 PM
+
+> Here is the first piece of my ARG homework.  Mostly I tried to fix up 
+> the syntax according to our discussions in Vienna.
+
+Thanks for getting this done early. Can I expect the rest of your homework
+early, too?? ;-)
+
+A couple of thoughts:
+
+(1) I think you need to soon (if not immediately) address how these are going
+to work within generic units and presumably for access-to-subprogram types.
+If we plan to use Global aspects for checking in parallel statements *and* we
+also want to use the containers there *and* we don't want any significant
+incompatibilities in the containers, then we have to have a "reflection"
+mechanism for generics.
+
+The mechanism designed for nonblocking provides one model for doing that. This
+is likely to be complicated (the Global aspect is not as simple as the boolean
+value of Nonblocking), and thus we need to get started on defining it (it isn't
+going to work as a last minute thing). Recall we have less than two years to
+finish this definition to standardization quality (if we intend to stay on
+schedule).
+
+(2) If we intend to use Global aspects for checking in parallel statements, we
+need to figure out the details of that checking sooner rather than later. The
+checking rules most likely will in part inform how the Global rules need to
+work.
+
+(3) I didn't see a solution for global data defined in hidden packages, such
+as the System implementation helpers that both Janus/Ada and GNAT have. We
+can't start requiring implementors to restructure their entire runtime in
+order to meet Global settings.
+
+(4) I didn't see any discussion of the defaults for Global the runtime
+packages. I realize the detailed update is going to be a large job in itself,
+but I'd like to hear at least about what the defaults will be.
+
+(5) I think I object to the idea of "synthesized" global aspects. (I'm sorry I
+didn't think of this during the meeting.)
+
+The basic idea is that global aspects, like many other aspects including Pre,
+Post, and Nonblocking, represent contracts between the caller and the callee.
+These are enforced on the calls without any knowledge of the implementation,
+and similarly are enforced on the body without any knowledge of the calls.
+
+"Synthesized", however, means that the contract depends on the contents of the
+body, requiring that a body need be present before any calls can be compiled
+and meaning that future maintenance on a body can break calls (a complete
+violation of the separation of calls and implementation).
+
+Note that existing cases of body dependencies (generic instances, aspect
+Inline) in Ada have two important properties: (1) they're optional, no Ada
+compiler needs to implement them (Janus/Ada does not; the primary reason we
+implemented generic code sharing was to avoid generic body dependencies); (2)
+the code will not change legality regardless of changes in the body.
+"Synthesized" will fail (2) and thus be a horrific maintenance hazard
+(especially given the cascade effects of contracts).
+
+My long time objection to systems like SPARK is their need to have the
+complete program available before they can prove anything. I don't want
+to see Ada going down that road.
+
+Synthesizing contracts (Global among them) seems like a ripe area for tools,
+and there seems to be no need to include it in the language proper. Moreover,
+an implementation could define "Synthesized" if it wanted to
+(implementation-defined modifiers are allowed), and that seems preferable to
+defining in the language something contract-related that destroys the contract
+model!
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent