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

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

--- ai12s/ai12-0079-1.txt	2018/03/30 07:55:07	1.17
+++ ai12s/ai12-0079-1.txt	2018/10/18 23:53:42	1.18
@@ -1,4 +1,4 @@
-!standard 6.1.2(0)                                  18-03-01    AI12-0079-1/06
+!standard 6.1.2(0)                                  18-10-18    AI12-0079-1/07
 !class Amendment 13-06-28
 !status work item 13-06-28
 !status received 13-06-14
@@ -83,7 +83,7 @@
 1.	Allow the name of an access type A (including "access T") to
 stand-in for the set of objects described roughly by:
 
-    (for all X convertible to A => X.all)
+    [for all X convertible to A => X.all]
 
 Also allow within a Global or Global'Class aspect
 a reference to the set of pointed-to objects reachable from
@@ -99,7 +99,7 @@
 2.	Allow the name of a package P to stand-in for the set of objects
 described roughly by:
 
-    (for all variables X declared in P => X)
+    [for all variables X declared in P => X]
 
 Also allow this to be qualified with "private" to restrict the set to those
 objects declared in the private part, the body, or private descendants.
@@ -136,15 +136,17 @@
 
 Add after 6.1.1(30.3/5) -- at the end of static semantics:
 
-  Given an access type T that has Ownership aspect False (see H.7), an
-  aliased object is /reachable/ from an access object X of type T if
-  that object satisfies the constraints of the designated subtype of T
-  and any constraints that apply to X, or is reachable from an object
-  that is part of some object that is itself reachable from X.
-  Reachability from access objects of a type with Ownership aspect True
-  is defined in H.7. An aliased object is /reachable/ from a composite
-  object if the object is reachable from some subcomponent of the
-  composite object.
+  Given an access-to-object type T that has Ownership aspect False (see
+  H.7), an aliased object is /reachable/ from an access object X of type
+  T if the aliased object satisfies the constraints of the designated
+  subtype of T and any constraints that apply to X, and, when T is a
+  pool-specific access type, the aliased object might be part of the
+  collection (see 7.6.1) associated with T. In addition, an aliased
+  object is reachable from X if it is reachable from a part of an object
+  that is itself reachable from X. Reachability from access objects of a
+  type with Ownership aspect True is defined in H.7. An aliased object is
+  /reachable/ from a composite object if the aliased object is reachable
+  from some subcomponent of the composite object.
     AARM Reason: Reachability is defined in terms of types rather than
     individual objects, in the absence of "ownership."  See H.7 (AI-0240)
     for the rules that apply when ownership is True.
@@ -165,6 +167,9 @@
 
    X'Reachable (global_set) returns True if at least one object in the set
    identified by the global_set is reachable from X.
+     AARM Rationale: This allows a postcondition to indicate what additional
+     objects might become reachable from X as a result of invoking the
+     subprogram.
 
 Add the following section:
 
@@ -211,7 +216,7 @@
       | /package_/name [ PRIVATE ]
       | /access_/subtype_mark
       | ACCESS subtype_mark
-      | /object_\name'Reachable
+      | /object_/name'Reachable
 
    A /global_/attribute_reference is an attribute_reference with attribute
    designator "Global."
@@ -2359,10 +2364,10 @@
 Sent: Sunday, February 18, 2018  5:29 PM
 
 ...
->>I am willing to spend more time on 0079.  I did not realize 
->>that the above was your concern.  Perhaps we can handle this 
->>offline.  If you can let me know what you feel you need to 
->>annotate the containers, I'll try to finalize that part of 
+>>I am willing to spend more time on 0079.  I did not realize
+>>that the above was your concern.  Perhaps we can handle this
+>>offline.  If you can let me know what you feel you need to
+>>annotate the containers, I'll try to finalize that part of
 >>the wording.
 >
 >I'm not completely sure at this stage, as I've never felt the proposal was
@@ -2373,14 +2378,14 @@
 >This is rather complex for Nonblocking (which is worked out), and Global is
 >10 times harder, so the lack of work in that area is concerning.
 
-I am not sure what you mean here.  We have the 'Global attribute and permit 
-the use of "&" to combine global specifications.  What more do you think we 
+I am not sure what you mean here.  We have the 'Global attribute and permit
+the use of "&" to combine global specifications.  What more do you think we
 need?
 
->>For me it just seemed like there was a general 
->>fine tuning needed, but apparently you feel there are still 
->>some big issues, at least when it comes to annotating the 
->>libraries.  So if you can give me a clearer idea of what you 
+>>For me it just seemed like there was a general
+>>fine tuning needed, but apparently you feel there are still
+>>some big issues, at least when it comes to annotating the
+>>libraries.  So if you can give me a clearer idea of what you
 >>need, I'll focus on that.
 
 >The other issue for the libraries is clearly what to do about
@@ -2390,7 +2395,7 @@
 >packages, of course). And we surely can't name any such packages in the
 >Standard!
 
-Private descendants are considered part of the package body from the point 
+Private descendants are considered part of the package body from the point
 of "Global => (in out => P private)".  Do we need more than that as a way to
 support "helper" packages?
 
@@ -2404,7 +2409,7 @@
 >  type Index_Type is range <>;
 >  type Element_Type is private;
 >  with function "=" (Left, Right : Element_Type) return Boolean is <>;
->package Ada.Containers.Vectors 
+>package Ada.Containers.Vectors
 >  with Preelaborate, Remote_Types,
 >       Nonblocking => Equal_Element'Nonblocking,
 >       Global => Equal_Element'Global and <impl-def stuff??> and <the body of this package> is
@@ -2424,7 +2429,7 @@
 >repeating Nonblocking and Global aspects 70 times.
 
 Fine, but that seems to be a separate AI.  I think it is safe to assume that
-this can be fixed to work the way we want it to for Global and Nonblocking, 
+this can be fixed to work the way we want it to for Global and Nonblocking,
 so this shouldn't interfere with you making progress.
 
 >The third issue is about the actual definition of "synchronized". The
@@ -2433,7 +2438,7 @@
 >impossible if any globals are involved (as soon as there is more than one
 >global, data locks are impossible to avoid with static rules). ...
 
-There are "data races" and "race conditions."  Frequently these are treated as 
+There are "data races" and "race conditions."  Frequently these are treated as
 synonyms, but if there is a distinction, it is that "A := A + 1" does not
 involve a "data race" if A is atomic, but it is clearly a race condition.  I
 don't think we have a prayer of preventing these kinds of race conditions.
@@ -2442,16 +2447,16 @@
 that.  Again, I think this is a separate AI, or simply out of scope for Ada
 standardization.
 
-So I don't find any of the above issues particularly relevant to AI12-0079 and 
+So I don't find any of the above issues particularly relevant to AI12-0079 and
 its use in annotating language-defined packages.  *However*, I do think we have
-a significant issue with respect to access types.  We really want a way to say 
+a significant issue with respect to access types.  We really want a way to say
 that the side-effects are limited to heap objects "reachable" from a given
-parameter.  Saying that a subprogram updates something designated by a given 
+parameter.  Saying that a subprogram updates something designated by a given
 access type is pretty useless.
 
 So I plan to spend some time thinking about this problem of access types,
 especially in the context of container-like packages that clearly use access
-types behind the scenes.  But I don't see that there is much more needed to 
+types behind the scenes.  But I don't see that there is much more needed to
 address the issues you identify above.  If you don't agree, please advise!
 
 ****************************************************************
@@ -2472,7 +2477,7 @@
 that implementers can figure it out.
 
 I suppose this is more of a concern for the actual proposal rather that need
-in the spec of the containers. But if no one can write a legal body for the 
+in the spec of the containers. But if no one can write a legal body for the
 containers, that would be bad...
 
 ...
@@ -2482,13 +2487,13 @@
 >> have globals in them. It would seem nasty to ban that (other than in Pure
 >> packages, of course). And we surely can't name any such packages in the
 >> Standard!
-		
+
 > Private descendants are considered part of the package body from the point
 > of "Global => (in out => P private)".  Do we need more than that as a way
 > to support "helper" packages?
 
 Traditionally, helper packages are in some implementation-defined subsystem.
-The obvious example is IO. In Janus/Ada, we have the helper package defined 
+The obvious example is IO. In Janus/Ada, we have the helper package defined
 as System.Basic_IO. All of the language-defined packages are defined in terms
 of it. (It has a bit of state to support Standard-in/Standard-out.) I believe
 GNAT has some such package in the GNAT subsystem.
@@ -2497,7 +2502,7 @@
 of Ada.Containers. (There sadly isn't an Ada.IO subsystem.) But that
 *still* isn't a "private descendant" of the generic Ada.Containers.Vectors!
 And there is no way to have a non-generic private descendant of a generic
-package. [If I was going to use a helper at all, it would definitely be 
+package. [If I was going to use a helper at all, it would definitely be
 non-generic.]
 
 I vaguely remember that one option discussed was just to punt and let
@@ -2510,13 +2515,13 @@
 as those are semantically transparent for the purposes of the language-defined
 specification.)
 
-...	
+...
 >> However, we've never defined what the freezing point of a package
 >> declaration is, so the place where these aspects are evaluated is not
 >> well-defined. So I don't even know if this formulation is legal. And if it
 >> isn't legal, is there any alternative that IS legal that doesn't require
 >> repeating Nonblocking and Global aspects 70 times.
->		
+>
 > Fine, but that seems to be a separate AI.  I think it is safe to assume
 > that this can be fixed to work the way we want it to for Global and
 > Nonblocking, so this shouldn't interfere with you making progress.
@@ -2530,7 +2535,7 @@
 >> variables. It's pretty clear that 100% elimination of data races is
 >> impossible if any globals are involved (as soon as there is more than one
 >> global, data locks are impossible to avoid with static rules). ...
-		
+
 > There are "data races" and "race conditions."  Frequently these are treated
 > as synonyms, but if there is a distinction, it is that "A := A + 1" does not
 > involve a "data race" if A is atomic, but it is clearly a race condition.
@@ -2555,7 +2560,7 @@
 
 Recall how I'd expect to use the parallelism features (because it's the way I
 do all of my Ada programming these days): add parallel to an appropriate loop
-and let the compiler tell me what needs to be changed. Ada compilers are ten 
+and let the compiler tell me what needs to be changed. Ada compilers are ten
 times better at finding issues than I would be -- the big problem I have with
 the current tasking model is that it leaves the programmer completely on your
 own. I realize that finding every problem statically is probably impractical,
@@ -2607,7 +2612,7 @@
 > considered safe unless they are writing a static value, or are using one of
 > a atomic update operations that Bob doesn't think we need to define. ;-) ...
 
-This is an interesting point of view, but I still think it is completely 
+This is an interesting point of view, but I still think it is completely
 unrelated to the Global annotation AI.  I still think this is more of a
 "warning" situation than an error.  I don't think we should be in the
 business of disallowing use of atomic variables to provide synchronization,
@@ -2628,7 +2633,7 @@
 writing of heap-resident data, in a way that it can be checked by the
 compiler.
 
-In any case, I have some new ideas how to do this, using a 'Reachable 
+In any case, I have some new ideas how to do this, using a 'Reachable
 attribute.  I'll write this up shortly.
 
 ****************************************************************
@@ -2639,18 +2644,18 @@
 >> I don't see any good reason to allow writes to atomic objects to be
 >> considered safe unless they are writing a static value, or are using one of
 >> a atomic update operations that Bob doesn't think we need to define. ;-) ...
->		
+>
 > This is an interesting point of view, but I still think it is completely
 > unrelated to the Global annotation AI.  I still think this is more of a
 > "warning" situation than an error.  I don't think we should be in the
 > business of disallowing use of atomic variables to provide synchronization,
 > but I could see a compiler warning you about certain uses.
 
-We *should* be in the business of disallowing unsafe code by default (for the 
+We *should* be in the business of disallowing unsafe code by default (for the
 purpose of parallel execution), and that is what Global does here.
 Anything should be fine in the Global => all case, because that doesn't
 promise any safety. Atomic variables are only usable for synchronization with
-xtreme care, and "extreme care" runs counter to the purpose of having safety 
+xtreme care, and "extreme care" runs counter to the purpose of having safety
 rules in the first place. (You can use any sort of global object with "extreme
 care", after all. :-)
 
@@ -2664,8 +2669,8 @@
 > writing of heap-resident data, in a way that it can be checked by the
 > compiler.
 
-OIC. You're worried that the static rules would pretty much have to disallow 
-doing anything heap-related in the body of a subprogram, since we don't know 
+OIC. You're worried that the static rules would pretty much have to disallow
+doing anything heap-related in the body of a subprogram, since we don't know
 that the heap objects "belong" to the parameter and won't be shared with other
 objects. (Such heap objects shouldn't appear in Global at all -- the part I
 was worrying about -- since they are of types that are likely private/body and
@@ -2684,11 +2689,11 @@
 Sent: Saturday, February 24, 2018  9:01 PM
 
 > ...
-> 
-> However, we've never defined what the freezing point of a package 
-> declaration is, so the place where these aspects are evaluated is not 
-> well-defined. So I don't even know if this formulation is legal. And 
-> if it isn't legal, is there any alternative that IS legal that doesn't 
+>
+> However, we've never defined what the freezing point of a package
+> declaration is, so the place where these aspects are evaluated is not
+> well-defined. So I don't even know if this formulation is legal. And
+> if it isn't legal, is there any alternative that IS legal that doesn't
 > require repeating Nonblocking and Global aspects 70 times.
 
 Below are two paragraphs I am planning to add to the Global aspect AI.  Do
@@ -2703,7 +2708,7 @@
   at the end of the immediately enclosing declaration list{, or in the
   case of the declaration of a library unit, at the end of the visible
   part of the entity}.
-  
+
 Modify 13.14(3/5):
 
   The end of a declarative_part, protected_body, or a declaration of a
@@ -2716,16 +2721,16 @@
 From: Randy Brukardt
 Sent: Monday, February 26, 2018  9:34 PM
 
-> Below are two paragraphs I am planning to add to the Global aspect AI.  
+> Below are two paragraphs I am planning to add to the Global aspect AI.
 > Do these address this issue adequately?
 
 So long as they don't stomp on the rules for categorization aspects, we should
 be fine.
- 
+
 > ----------
-> 
+>
 > Modify 13.1.1(11/3):
-> 
+>
 >   The usage names in an aspect_definition [Redundant: are not resolved
 >   at the point of the associated declaration, but rather] are resolved
 >   at the end of the immediately enclosing declaration list{, or in the
@@ -2733,12 +2738,12 @@
 >   part of the entity}.
 
 
-Luckily, 13.1.1(32/4) is a "Notwithstanding" rule, so what we say for the 
+Luckily, 13.1.1(32/4) is a "Notwithstanding" rule, so what we say for the
 "normal" case doesn't matter. In particular, 13.1.1(32/4) says:
 
-Notwithstanding what this International Standard says elsewhere, the 
+Notwithstanding what this International Standard says elsewhere, the
 expression of an aspect that can be specified by a library unit pragma is
-resolved and evaluated at the point where it occurs in the 
+resolved and evaluated at the point where it occurs in the
 aspect_specification[, rather than the first freezing point of the
 associated package].
 
@@ -2752,9 +2757,9 @@
 a subprogram profile is the visible part; for a renames, it appears that
 there is no visible part. So, let's rephrase: does the visible part of a
 subprogram or rename have a well-defined end?
-   
+
 > Modify 13.14(3/5):
-> 
+>
 >   The end of a declarative_part, protected_body, or a declaration of a
 >   library package or generic library package, causes freezing of each
 >   entity and profile declared within it{, as well as the entity itself
@@ -2771,27 +2776,27 @@
 
 Yes they do.  Look in RM 8.2
 
-> Humm part 2: the index points us to a sentence (in 8.2(5)) that is 
-> described as "redundant" for the definition of visible part. Anyway, 
-> that implies that a subprogram profile is the visible part; for a 
+> Humm part 2: the index points us to a sentence (in 8.2(5)) that is
+> described as "redundant" for the definition of visible part. Anyway,
+> that implies that a subprogram profile is the visible part; for a
 > renames, it appears that there is no visible part.
 
 The wording might not be precise in its use of "entity" vs. "declaration," but
 I think it is clear the intent that the profile in a subprogram renaming is
 the visible part.
 
-> So, let's rephrase: does the visible part of a subprogram or rename 
+> So, let's rephrase: does the visible part of a subprogram or rename
 > have a well-defined end?
 
 It seems like it ends at the end of the profile.  Where else would it end?
 
 >> Modify 13.14(3/5):
->> 
->>  The end of a declarative_part, protected_body, or a declaration of a  
->> library package or generic library package, causes freezing of each  
->> entity and profile declared within it{, as well as the entity itself  
+>>
+>>  The end of a declarative_part, protected_body, or a declaration of a
+>> library package or generic library package, causes freezing of each
+>> entity and profile declared within it{, as well as the entity itself
 >> in the case of the declaration of a library unit}.
-> 
+>
 > Looks OK to me.
 
 Good.
@@ -2801,12 +2806,12 @@
 From: Randy Brukardt
 Sent: Thursday, March  1, 2018  1:50 AM
 
-> I am not talking about using access types in a visible interface, but 
-> rather trying to define what a given interface does in terms of its 
-> reading and writing of heap-resident data, in a way that it can be 
+> I am not talking about using access types in a visible interface, but
+> rather trying to define what a given interface does in terms of its
+> reading and writing of heap-resident data, in a way that it can be
 > checked by the compiler.
 >
-> In any case, I have some new ideas how to do this, using a 'Reachable 
+> In any case, I have some new ideas how to do this, using a 'Reachable
 > attribute.  I'll write this up shortly.
 
 A thought: for the purposes of the containers, we only need to worry about
@@ -2864,8 +2869,8 @@
 me whether this is true or not. The wording needs to be clarified a bit.
 
 (2) The first part of the above Global aspect is to reuse the "standard"
-Global for the entire package. Part of that is implementation-defined, so we 
-don't want to duplicate it all over the place. I used "unit'Global" for this 
+Global for the entire package. Part of that is implementation-defined, so we
+don't want to duplicate it all over the place. I used "unit'Global" for this
 purpose, but that is a generic package and the Global attribute isn't defined
 for that. Not sure if that should be defined or if there is a better way to do
 this. (One could, I suppose, write the whole thing out once and then copy it
@@ -2886,7 +2891,7 @@
 part) and used to implement the container object. The reachable attribute
 can't describe them as they are of types not visible to the caller.
 
-Ideally, this usage would not require any global beyond specifying that the 
+Ideally, this usage would not require any global beyond specifying that the
 package body has state. But in order for that to be safe (in general), one
 needs to be able ensure that there is no "leakage" of access values or
 designated objects. I don't see anything in the rules that would have this
@@ -2909,7 +2914,7 @@
 
 > Here is a last-minute update to the Global AI.
 
-FYI, your files are still coming with <CR><CR><LF> as line endings (note the 
+FYI, your files are still coming with <CR><CR><LF> as line endings (note the
 extra <CR>); this makes it impossible to compare them (it doesn't match
 typical line endings) and makes a mess if I cut-and-paste part of it. (At
 least the people who send Unix files with just <LF> are readily obvious as
@@ -2929,15 +2934,15 @@
   The end of a declarative_part, protected_body, or a declaration of a
   library package or generic library package, causes freezing of each
   entity and profile declared within it{, as well as the entity itself
-  in the case of the declaration of a library unit}.  
+  in the case of the declaration of a library unit}.
 
-It did not cover (generic) library subprograms, but we probably care about 
+It did not cover (generic) library subprograms, but we probably care about
 those as well.  For them, we may want to say the end of the *compilation*
 unit, so as to include any of the "trailing" pragmas (such as pragma Inline).
 Trailing pragmas are clearly part of the compilation unit, whereas it is a bit
 less clear whether they are part of the declaration.
 
-Hence, to define when the declaration of a library subprogram is frozen, we 
+Hence, to define when the declaration of a library subprogram is frozen, we
 could leave the above paragraph as is, and add:
 
   The end of a compilation unit containing the declaration of a library unit
@@ -2946,5 +2951,19 @@
 
 Where the part about the pragmas is probably redundant, but perhaps doesn't
 hurt to include.
+
+**************************************************************
+
+From: Tucker Taft
+Sent: Thursday, October 18, 2018  8:21 AM
+
+[This is version /07 of the AI - Editor.]
+
+Here is a very minor update to the Global Annotations AI.  I couldn't find any
+specific things to fix from reading the minutes from our last discussion of the
+AI.  The only substantive thing I did was modify 'Reachable to take into account
+that a pool-specific access type can only point to things in its associated
+collection, meaning that if X and Y are of two different pool-specific access
+types, then X'Reachable does *not* include Y.all.   Randy, did I miss something?
 
 **************************************************************

Questions? Ask the ACAA Technical Agent