Version 1.3 of ai05s/ai05-0186-1.txt

Unformatted version of ai05s/ai05-0186-1.txt version 1.3
Other versions for file ai05s/ai05-0186-1.txt

!standard 13.3.4 (0)          10-01-20 AI05-0186-1/02
!class amendment 09-11-02
!status work item 09-11-02
!status received 09-11-02
!priority Medium
!difficulty Medium
!subject Global-in and global-out annotations
!summary
Annotations are provided to describe the use of global objects by subprograms.
!problem
We're considering adding many kinds of annotations to Ada (see AI05-0145-1 and AI05-0146-1) 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 annotations, a tool has to assume the worst about any user-defined functions. That is, 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" annotations, 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 annotations are available. This is bad, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body require creating pseudo body dependencies (if the body is changed, any analysis depending on that properties of that body would have to be performed again); but the language does not allow these to be "real" body dependencies (any recompilation needed has to occur automatically).
Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side-effects is needed in the specification of subprograms in order to accomplish that goal.
!proposal
Add global in and global out annotations to Ada, for subprograms and access-to-subprogram types. Add global_init in and global_init out annotations for packages and types.
The global_init annotations cover default initialization/adjustment/finalization for types; and cover operations that occur as part of the elaboration for packages.
!wording
Semi-formal description (presumably in Section 13.3.4):
Add to the aspect syntax given in AI05-0184-1:
Aspect_Mark [in|out] => Annotation_List
Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
Annotation_Item ::= object_name | access_subtype_mark |
NULL | OTHERS [IN packagename]
The names in these items resolve with the same visibility as other aspect expressions (that usually is the end of the visible part). The names must resolve without context.
Aspects Global and Global_Init are defined.
Static Semantics
A read or write of an object O is covered by an annotation in an Annotation_List if:
* O statically denotes a part of an object named in the Annotation_List;
* The annotation OTHERS without a package name occurs in the list;
* The annotation OTHERS with a package name P occurs in the list, and O denotes part of an object declared in P, or O denotes a part of an object produced by a dereference of an object of an access type declared in P; or
* O denotes a part of an object produced by a dereference of an object of an access type named in the Annotation_List.
AARM Ramification: "others" by itself allows anything to be read or written.
An annotation A1 is compatible with another annotation A2 if:
* A1 contains NULL; or
* A2 contains the annotation OTHERS without a package name; or
* All of the following must be true: -- Each object_name in A1 is covered by an annotation in A2; -- Each access_subtype_name in A1 is found in A2; and -- For each OTHERS annotation with a package name P, there is
a OTHERS annotation in A2 that statically denotes P.
AARM Ramification: This is not symeterical.
Legality Rules
An annotation_list can be given if and only if the aspect is Global or Global_Init.
The aspect Global shall be given only on subprograms and on access-to-subprogram types. The aspect Global_Init shall be given only on types, packages, and generic packages.
The Annotation_Item NULL has to be the only item in an Annotation_List if it is given.
An object_name given in an Annotation_List shall statically denote some object.
If a subprogram contains a Global in annotation, then:
* Every object that is read by the subprogram body shall either be accessible from the function call, be a constant object of an elementary type, or be covered by the Global in annotation.
* The subprogram corresponding to each dispatching call in the subprogram body which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call of a dereference of an access value shall have a compatible Global in annotation; the subprogram corresponding to every other call in the subprogram body shall have a compatible Global in annotation.
* The type of every stand-alone object declared by the subprogram shall have a compatible Global_Init in annotation.
* Every nested package and package instantiation declared by the subprogram shall have a compatible Global_Init in annotation.
* The type of each assignment_statement shall have a compatible Global_Init in annotation.
* The Allocate routine associated with the storage pool for the type of each allocator in the subprogram body shall have a compatible Global in annotation.
* For each attribute A'Storage_Size in the subprogram body where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
[I can't find any way to share these rules amongst the various kinds of entities. The first rule is slightly different for each kind of thing, depending on the accessibility or other rule needed.
AARM Ramification: Local objects, elementary constant objects (declared anywhere) and the parameters of the call do not need to appear in a Global in annotation. Note that this is referring to constant objects, not just constant views of an object. End Ramification.
AARM Discussion: We don't need a rule for Deallocate calls in Unchecked_Deallocation, as it is a call and does not have annotations defined. Thus the above rule will always fail and thus we don't care about the annotations on Deallocate.
Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and "read" by "written" everywhere).
[Editor's note: I don't want to duplicate the rules, they're complex enough as it is.]
For an attribute P'Access of access-to-subprogram type S that has a Global in annotation, subprogram P shall have a compatible Global in annotation. Similarly, for a type S that has a Global out annotation, subprogram P shall have a compatible Global out annotation.
Global'Class annotations shall be given only on primitive subprograms of a tagged type Redundant[; they provide annotations for dispatching calls]. The Global in annotation of a subprogram shall be compatible with the Global'Class in annotation of the subprogram; similarly Global out annotation of a subprogram shall be compatible with the Global'Class in annotation of the subprogram.
AARM Ramification: The Global'Class annotations have to allow the same or more than the Global annotations, as they apply to all overriding subprograms as well.
For each primitive subprogram P of a tagged type that overrides another primitive subprogram PP of the type:
* If PP has a Global'Class in annotation, the annotation shall be compatible with the Global'Class in annotation for P. The Global in annotation for P shall be compatible with the Global'Class in annotation for PP.
* If PP has a Global'Class out annotation, the annotation shall be compatible with the Global'Class out annotation for P. The Global out annotation for P shall be compatible with the Global'Class out annotation for PP.
If a type includes a Global_init in annotation:
* If the full type is composite, the type of each component shall have a compatible Global_init in annotation.
* If the full type is controlled, the associated Initialize and Finalize routines shall have compatible Global in annotations.
* If the full type is controlled and not limited, the associated Adjust routine shall have a compatible Global in annotation.
* If the full type is composite, for each default expression E for a component of the type:
* every object that is read by E shall be a constant object of an elementary type, or be covered by the Global_init in annotation; and
* the subprogram corresponding to each dispatching call in E which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call in E of a dereference of an access value shall have a compatible Global in annotation; the subprogram corresponding to every other call in E shall have a compatible Global in annotation; and
* the Allocate routine associated with the storage pool for the type of each allocator in E shall have a compatible Global in annotation.
* For each attribute A'Storage_Size in E where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* If the full type is a task type, the body shall conform to the rules for a subprogram body (given previously).
[We do not need to worry about assignment, stand-alone objects, and instances here, none of those are possible inside of types, other than task bodies, which we handle by requiring the rules of a subprogram body to be checked.]
AARM Note: Adjust really doesn't belong here, but it seems to be overkill to have a special kind of annotation just for it (and composition means that trying to define it directly would be a mess - composition happens automatically for the above rules). In practice, Adjust and Finalize are usually very similar in design, and are likely to depend on the same set of globals, so this isn't much of a limitation.
Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and "read" by "written" everywhere).
If a package or generic package includes a Global_init in annotation:
* For each expression or call E in every declarative_item (but not including those in nested units) and the sequence of statements of the package body:
* every object that is read by E shall be declared in the package, a constant object of an elementary type, or be covered by the Global_init in annotation; and
* the subprogram corresponding to each dispatching call in E which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call in E of a dereference of an access value shall have a compatible Global in annotation; the subprogram corresponding to every other call in E shall have a compatible Global in annotation; and
* the Allocate routine associated with the storage pool for the type of each allocator in E shall have a compatible Global in annotation.
* For each attribute A'Storage_Size in E where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* The type of every stand-alone object declared by the package shall have a compatible Global_Init in annotation.
* Every nested package and package instantiation declared by the package shall have a compatible Global_Init in annotation.
* The type of each assignment_statement in the sequence_of_statements of the package body shall have a compatible Global_Init in annotation.
Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and "read" by "written" everywhere).
[Generic rules; these apply to the entire Legality Rules section]
In addition to the places where Legality Rules normally apply, these rules also apply in the private part of an instance of a generic unit.
For the purposes of enforcing these rules in a generic body, the Global_Init annotations for a formal type are assumed to be (others); the Global annotations for formal subprograms and formal access types are assumed to be (others); the Global annotations on the storage pool operations for formal access types are assumed to be (others).
[This last paragraph is not talking about inside of instances; rechecking is done there with the actual annotations. This is the assume-the-worst rule needed in generic bodies.]
---
[Define the default annotations. Effectively, all annotations default to "others" because all of the rules above treat absense of an annotation like "others", unless we say otherwise. - Editor.]
Add to 3.5:
Elementary types of the language have implied annotations of Global_Init in => (null), Global_Init out => (null).
Add to 4.5:
Unless otherwise specified, the predefined operators of the language that have at operands of an elementary type all have implied annotations of Global in => (null), Global out => (null).
Add after 4.5.2:
The predefined equality and ordering operators for discrete array types have implied annotations of Global in => (null), Global out => (null).
AARM Ramification: The global rule means that equality and ordering operators for elementary types also have such annotations. Composition of equality for composite types means that they cannot have implied null annotations; that would be seriously incompatible. User-defined equality operators can have annotations, of course.
Add after 4.5.3:
If C is an elementary type, the predefined concatenation operators have implied annotations of Global in => (null), Global out => (null).
[We could go further, but it gets messy, as any controlled component may drag Adjustment into the equation.]
Add after A(2)
Static Semantics
Each subprogram that is declared pure or is declared in a language-defined package or generic package that is declared pure has implied annotations of Global in => (null), Global out => (null) unless the subprogram has one or more parameters of an access type.
AARM Compatibility Note: This could be imcompatible if a composite object passed as a parameter to such a subprogram has an access component. This does not seem likely for the language defined packages.
[Editor's note: I'm not sure the exception is actually needed, but I didn't check.
Here the list of such packages approved as of this writing; I don't intend to put the list into the AARM as it would require constant maintenance. I'm ignoring Wide_ and Wide_Wide_ versions of packages for this list, as well as bounded and unbounded string versions.
Ada Ada.Assertions Ada.Characters Ada.Characters.Handling Ada.Characters.Latin_1 Ada.Characters.Conversions Ada.Containers -- No subprograms Ada.Containers.Generic_Array_Sort Ada.Containers.Generic_Constrained_Array_Sort Ada.Containers.Generic_Sort Ada.Decimal Ada.Dispatching Ada.IO_Exceptions -- No subprograms Ada.Numerics Ada.Numerics.Generic_Complex_Types Ada.Numerics.Generic_Complex_Elementary_Functions Ada.Numerics.Generic_Elementary_Functions Ada.Numerics.Generic_Real_Arrays Ada.Numerics.Generic_Complex_Arrays Ada.Streams Ada.Strings Ada.Strings.Equal_Case_Insensitive Ada.Strings.Hash Ada.Strings.Hash_Case_Insensitive Ada.Strings.Less_Case_Insensitive Ada.Strings.Maps Ada.Strings.Maps.Constants Ada.Strings.UTF_encoding Ada.Unchecked_Conversion Interfaces Interfaces.C Interfaces.Fortran Standard -- covered by the rules for predefined operators. System System.Storage_Elements
I'm assuming that we adopt AI-142-4 and/or AI-139-2, both of which require the bounded containers to be preelaborable (so that the accessors and iterators work). We would like to explicitly provide annotations for the bounded containers as appropriate (I suspect unbounded is nasty because of the access types involved).
I suspect that we need to exclude the generic sorts, as the annotations of element types or the formal subprograms come into play for these, and we don't want to restrict them. Not sure of the best way to do that.
We probably also want to exclude the generic real and complex array packages; adding these annotations would prevent sparse matrix representations. I don't think we want to go that far (although they'd be hard to implement within the restrictions of Pure).
End really long Editor's note. Probably should move some of this to !discussion after we make decisions.]
** Wording TBD:
I don't quite see how to take into account (or if we have to) the storage pool of an access type.
The intended rules are:
For pool-specific types, only the storage pool can be accessed by a dereference. For general access types, any aliased object of the designated type (and the storage pool) can be accessed by a dereference.
The current wording "covers" dereferences by naming their access type. The above rules would seem necessary for tools depending on these annotations, but doesn't seem necessary for the rules defining the annotations themselves. I handled calls to Allocate and Storage_Size explicitly. This latter set of rules doesn't handle implicitly called Allocate/Deallocate calls in assignement statements, but that could be handled explicitly as well if the approach is OK.
If there is a problem with this strategy, it is that there isn't any way to localize access types to a particular pool (when that is known but the type isn't visible). You would have to use a package name for a local access type (usually youself). For instance, all of the operations of Ada.Containers.Vectors would need Global in => (others in Vectors) because of the (presumably) local access type declared to implement the unbounded-ness.
I don't think there is enough benefit to further complications here (especially as the containers example, the pool isn't visible either, so I can't imagine any other annotation that would work), but I am willing to be convinced otherwise.
An alternative approach would be to wrap up the entire set of items in Global in/out annotations for each access type (that would be disjoint with access-to-subprograms use for the same thing). That would include all of the Global annotations for the subprograms of the storage pool, an annotation for the storage pool object, and ??? for general access object ["others" is the only current thing, which would be nasty]. That would be easier for tools to use, I suspect, but harder to write and less specific. Which doesn't seem to be an improvement to me.
---
I hate the duplication of rules here. I tried and tried to find some way to eliminate the duplication for expressions and calls (for which most of the rules applied. But I continually got stuck by the fact that there are essentially 4 parameters: the expression E; the accessibility/locality of objects to exclude (that is, the definition of what is local is different for subprograms [we need to include the parameters], packages [we need to exclude anything outside of the package, even though at the same accessibility level, as packages are invisible to accessibility], and types [locals only for tasks,and nothing special needed]; the kind of annotation (either "in" or "out"); and which annotation it is (Global or Global_Init). It's just too much to do in any understandable way. And I couldn't find a way to factor out the accessibility without getting overlapping rules. Maybe someone else has a better idea.
** End Wording TBD.
!discussion
The global in and global out annotations are intended to be descriptive. That is, the annotations describe the behavior of the subprogram body, initialization/finalization of a type, or elaboration of a package. As such, these annotations are checked. There is no benefit to be gained from lying about side-effects; such incorrect information could easily lead to incorrect code being generated (if the compiler uses the annotations). Moreover, if it is impractical to specify the correct annotations, it makes sense to specify none at all.
All of the global in and global out annotations proposed can be statically checked. It is possible to imagine annotations that cannot be statically checked, but these are assumptions as opposed to descriptive. Assumptions are a different set of annotations.
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.
---
The keywords in the syntax are necessary in order that the special syntax of this list can be recognized immediately. Otherwise, a massive amount of lookahead is needed to parse this (as the list would start the same way as the expression used for more typical aspects). We take advantage of the fact that Ada already has "in" and "out" keywords to make this syntax distinctive but still sensible.
---
These annotations can be used by the compiler to guide code generation as well as for static analysis. In that case, rules similar to those for Pure subprograms should be applied -- it is OK to assume that the annotations are correct, but if the subprogram is called, then the compiler must use the actual side-effects, not any assumed because of annotations.
[I didn't try to word this. - Randy]
---
It might make the most sense to define these in Annex H (High-Integrity Systems), rather than in Section 13. The most important thing is to define the syntax so that implementations can implement it and the checking (even if they are not doing semantic analysis now). The information is valuable to have in programs for future analysis when improved tools are available. The legality rules ensure that the information is accurate.
---
We have two kinds of global annotations, one for callable entities (Global) and one for the initialization/elaboration of entities. We need both as there is a (small) overlap for access-to-subprogram types, which is both a type and an callable entity.
Global_Init annotations can be given on private types; if so, they are enforced on the full type as well.
---
The definition of preelaborable has legality rules depending on a runtime concept (elaboration). We tried to avoid that mistake with this set of rules.
That requires making composition of annotations explicit. The definition of the Global_Init annotations for types requires this. Once we have this, applying the rules just requires talking about the type of stand-alone objects and of assignment_statements; they include the annotations of any components by definition.
---
The rules are complicated by the need to include all implicit calls. That is done by folding Initialize/Finalize/Adjust into Global_Init (along with default initialization), and explicitly talking about the operations of storage pools.
!example
** TBD **
!ACATS test
!appendix

From: Randy Brukardt
Sent (privately): Wednesday, March 18, 2009  4:30 PM

As I understand it (mainly from an old message of John's about "exposing your
globals"), Global_In is a list of names of globals touched by the body of a
subprogram. It also ought to include two special names: "null" (for explicitly
stating that no globals are harmed by this subprogram :-); and "private" (for
globals that aren't visible at the point of the annotation). By default, all
subprograms have

    Global_In => private,

which says that they touch globals but we aren't going to say which ones.

Presumably, Global_Out are a similar list of globals written by a subprogram.

Do I have it so far?

Now, the problem with the SPARK definition is that it doesn't take into account
things like storage pools and tasks, which we'll have to do.

For the storage pool problem, I think that declaring any collections read would
be sufficient, and that could easily be done by mentioning the name of the
access type in the annotation. (Directly naming the pool has two problems: the
pool may not be visible while the access type is, and secondly, the default pool
does not have a name.)

I'm going to ignore tasks for now (not really relevant to my questions).

I do think that the compiler needs to check that this listing is correct. (And I
think that is fairly easy: any object whose accessibility is outside of that of
the subprogram call "shall be listed" in the Global_In annotation unless the
Global_In annotation includes "private". ["Subprogram call" allows
accessing/modifying the parameters.] That would of course include anything
listed in the Global_In annotation of any called routines. Language-defined
operators other than "=" for tagged types would be defined to have Global_In =>
null.) Having this information incorrect would lead to all kinds of bad
assumptions by the compiler and by the reader. And you can always use Global_In
=> private if you don't want to say - just don't lie.

I note that this gets the effect of the "strict" annotation that I was lobbying
for, but in a way which is much harder to argue with. ("Global_In => null" means
"I don't have a side effect other than as declared in the spec", and the
compiler and reader can depend on that.) We don't get the elaboration benefit (I
would have allowed early calls on strict functions, because so long as their
parameters are frozen, they are safe), but that is no big deal.


But I am wondering about accesses to sub-parts of parameters. My "strict"
definition would have banned that, because it would allow depending on
side-effects. The way I wrote the description above would also ban that, but I
worry that people would be annoyed. This problem comes from my recognition that
the Claw Is_Valid routine is not strict, even though it only depends on reading
its parameter. For example:

     type A_Window is private;

     function Is_Valid (A : A_Window) return Boolean
     when Global_In => ???;

  private

     type Data is record
        Valid : Boolean := False;
        Handle : HWnd := Null_HWnd;
        ...
     end record;
     type Data_Access is access all Data;

     type A_Window is record
         My_Data : Data_Access;
         ...
     end record;

The problem here is that the user of the GUI application can manually close a
window, at which point Valid gets set to False and the Handle gets set to
Null_HWnd (among other things, of course).

Is_Valid only reads its parameter, but the portion that is pointed at can be
modified asynchronously by another task. So it would be wrong for an analyzer to
depend on the value of Is_Valid not changing. (This is a huge challenge when
programming with Claw.)

So, does this mean that type Data_Access must be included in the Global_In list?
(In this particular case, since the type is defined in the private part, the
Global_In list would have to be "private").

****************************************************************

From: Tucker Taft
Sent (privately): Wednesday, March 18, 2009  5:31 PM

...
> Do I have it so far?

I hadn't thought about it too much in detail yet.  As you know SPARK has
something like this.

The notion of "private" doesn't sound too useful.  I would suggest allowing the
names of packages as well as objects, where the name of a package means some
presumably non-visible "state" in the package (spec or body).  I suspect we
would need to parenthesize the list if there is more than one item, to avoid
creating a syntactic mess, with "null" substituting for the syntactically
illegal "()".

>
> Now, the problem with the SPARK definition is that it doesn't take
> into account things like storage pools and tasks, which we'll have to do.
>
> For the storage pool problem, I think that declaring any collections
> read would be sufficient, and that could easily be done by mentioning
> the name of the access type in the annotation. (Directly naming the
> pool has two
> problems: the pool may not be visible while the access type is, and
> secondly, the default pool does not have a name.)

Yes, an access type would seem reasonable as a stand-in for the collection it
represents.  And a package name would cover any non-visible *pool-specific*
access types declared within it.

If you are going through a non-visible *general* access type, then I think we
would want some notation for that if the access type is private, but the
designated type is not.  E.g. "all aliased T" might be a legal entry in the
list, and perhaps simply "all aliased" if the type is itself non-visible.

Alternatively, it might be appropriate in some cases to identify the particular
pointed-to object referenced/updated, e.g. Global_In => (X.all, Y.T.all),
Global_Out => (X.A, Y.B.all); Saying an entire access collection is affected is
too imprecise for some kinds of analysis.  And if the access type is a general
access type, then you are effectively "killing" all aliased objects of the
designated type (or types covered by it).

> I'm going to ignore tasks for now (not really relevant to my questions).

I don't see tasks as a big special case.  A task has state just like other
objects.  The slightly weird thing is that you can change the state of a task
even though you have it as an "IN" parameter.  Probably one way to think about
it is that every task has its own "collection", and the stack of the task is
allocated out of that collection, and the task object is really just a pointer
to that.  A call on an entry of a task passes an implicit dereference of that
pointer to the accept statement.

> I do think that the compiler needs to check that this listing is correct.
> (And I think that is fairly easy: any object whose accessibility is
> outside of that of the subprogram call "shall be listed" in the
> Global_In annotation unless the Global_In annotation includes "private". ["Subprogram call"
> allows accessing/modifying the parameters.] That would of course
> include anything listed in the Global_In annotation of any called routines.
> Language-defined operators other than "=" for tagged types would be
> defined to have Global_In => null.) Having this information incorrect
> would lead to all kinds of bad assumptions by the compiler and by the
> reader. And you can always use Global_In => private if you don't want to say - just don't lie.

Yes, I would agree with all of this.  But I would also try to define the
semantics so that if you manage to lie (e.g. by referencing imported
subprograms), the world doesn't implode. Instead it is like pragma Pure, the
compiler is allowed to avoid calling a subprogram again if it concludes
everything it takes as input is unchanged, and use the prior results of the
call.  It isn't allowed to assume that if it actually *makes* the call, it will
always get the same answer.

Something similar would be said about Global_Out, which would permit reusing
cached values after a call rather than reloading them from memory if they
supposedly wouldn't be affected by the call, but if you actually go to the
trouble of *reloading* the value from memory, you shouldn't presume this newly
loaded value is identical to the old one, and use the newly reloaded value to,
say, index into an array without rechecking against the bounds.

> I note that this gets the effect of the "strict" annotation that I was
> lobbying for, but in a way which is much harder to argue with.
> ("Global_In => null" means "I don't have a side effect other than as
> declared in the spec", and the compiler and reader can depend on
> that.) We don't get the elaboration benefit (I would have allowed
> early calls on strict functions, because so long as their parameters
> are frozen, they are safe), but that is no big deal.
>
>
> But I am wondering about accesses to sub-parts of parameters. My "strict"
> definition would have banned that, because it would allow depending on
> side-effects.

I don't really understand this last sentence.  I'm not sure what is a "sub-part"
and I'm not sure what you mean about "depending on side-effects."  I think I
understand what you mean in your example below, but I don't understand this
introductory sentence.

> ... The way I wrote the description above would also ban that, but
> I worry that people would be annoyed. This problem comes from my
> recognition that the Claw Is_Valid routine is not strict, even though
> it only depends on reading its parameter. For example:
>
>      type A_Window is private;
>
>      function Is_Valid (A : A_Window) return Boolean
>      when Global_In => ???;
>
>   private
>
>      type Data is record
>         Valid : Boolean := False;
>         Handle : HWnd := Null_HWnd;
>         ...
>      end record;
>      type Data_Access is access all Data;
>
>      type A_Window is record
>          My_Data : Data_Access;
>          ...
>      end record;
>
> The problem here is that the user of the GUI application can manually
> close a window, at which point Valid gets set to False and the Handle
> gets set to Null_HWnd (among other things, of course).
>
> Is_Valid only reads its parameter, but the portion that is pointed at
> can be modified asynchronously by another task. So it would be wrong
> for an analyzer to depend on the value of Is_Valid not changing. (This
> is a huge challenge when programming with Claw.)
>
> So, does this mean that type Data_Access must be included in the
> Global_In list? (In this particular case, since the type is defined in
> the private part, the Global_In list would have to be "private").
>
> Thanks in advance for your answer.

If you read something you get through an access value, then you will need to
account for it somehow, as "blah.all", the name of an access type, the name of a
package, or something like "all aliased [T]".

I think you are also talking about issues that have to multi-threading here.  If
the asynchronous event can happen at "any" time, then I would say you should
really declare the "Valid" field as volatile, in which case we would probably
want some way of stating that the result of a function is volatile and hence
essentially unpredictable.

If the aynchronous update can only happen during to some kind of
potentially-blocking or signaling operation, then it should be handled the
normal way things are handled at potential task signaling/blocking points, where
some appropriate part of the universe might be affected by the actions of other
tasks.

****************************************************************

From: Randy Brukardt
Sent (privately): Wednesday, March 18, 2009  5:59 PM

...
> The notion of "private" doesn't sound too useful.  I would suggest
> allowing the names of packages as well as objects, where the name of a
> package means some presumably non-visible "state" in the package (spec
> or body).  I suspect we would need to parenthesize the list if there
> is more than one item, to avoid creating a syntactic mess, with "null"
> substituting for the syntactically illegal "()".

Well, it surely isn't useful for analysis, but it seems necessary to have a
default that says, yup, we have some side effects and we aren't going to say
which ones. Because we surely can't require this annotation on all subprograms,
but we do have to know what to do if such a subprogram is called from inside of
one that does have an annotation.

If there is a better way to express the default of "anything goes, assume the
worst", I'm happy to see it.

...
> > I do think that the compiler needs to check that this listing is correct.
> > (And I think that is fairly easy: any object whose accessibility is
> > outside of that of the subprogram call "shall be listed" in the
> > Global_In annotation unless the Global_In annotation includes "private".
> > ["Subprogram call" allows accessing/modifying the parameters.] That
> > would of course  include anything listed in the Global_In annotation
> > of any called routines.
> > Language-defined operators other than "=" for tagged types would be
> > defined to have Global_In => null.) Having this information
> > incorrect would lead to all kinds of bad assumptions by the compiler
> > and by the reader. And you can always use Global_In => private if
> > you don't want to say - just don't lie.
>
> Yes, I would agree with all of this.  But I would also try to define
> the semantics so that if you manage to lie (e.g. by referencing
> imported subprograms), the world doesn't implode.
> Instead it is like pragma Pure, the compiler is allowed to avoid
> calling a subprogram again if it concludes everything it takes as
> input is unchanged, and use the prior results of the call.  It isn't
> allowed to assume that if it actually
> *makes* the call, it will always get the same answer.

Well, for static analysis, either you have the truth or the world implodes. :-)
And that's also true for legality rules - if you depend on an incorrect
annotation when enforcing a legality rule (or more accurately not enforcing),
it's pretty much garbage in, garbage out. Probably would want to define that as
a bounded error if at all possible (either you get an error or the code works at
runtime).

But I agree that we pretty much have to leave the Duff door open: lying in
annotations on an imported subprogram can't be banned or detected.

I do agree that uses in optimizations and code selection should follow rules
like you give here.

> Something similar would be said about Global_Out, which would permit
> reusing cached values after a call rather than reloading them from
> memory if they supposedly wouldn't be affected by the call, but if you
> actually go to the trouble of *reloading* the value from memory, you
> shouldn't presume this newly loaded value is identical to the old one,
> and use the newly reloaded value to, say, index into an array without
> rechecking against the bounds.

Right. I'm not personally as interested in Global_Out, at least not right this
minute, but I can see how it would be useful.

...
> > But I am wondering about accesses to sub-parts of parameters. My "strict"
> > definition would have banned that, because it would allow depending
> > on side-effects.
>
> I don't really understand this last sentence.  I'm not sure what is a
> "sub-part" and I'm not sure what you mean about "depending on
> side-effects."  I think I understand what you mean in your example
> below, but I don't understand this introductory sentence.

I mean cases like the example below. In other words, ignore the above if it is
too confusing.

> > ... The way I wrote the description above would also ban that, but I
> > worry that people would be annoyed. This problem comes from my
> > recognition that the Claw Is_Valid routine is not strict, even
> > though it only depends on reading its parameter. For example:
> >
> >      type A_Window is private;
> >
> >      function Is_Valid (A : A_Window) return Boolean
> >      when Global_In => ???;
> >
> >   private
> >
> >      type Data is record
> >         Valid : Boolean := False;
> >         Handle : HWnd := Null_HWnd;
> >         ...
> >      end record;
> >      type Data_Access is access all Data;
> >
> >      type A_Window is record
> >          My_Data : Data_Access;
> >          ...
> >      end record;
> >
> > The problem here is that the user of the GUI application can
> > manually close a window, at which point Valid gets set to False and
> > the Handle gets set to Null_HWnd (among other things, of course).
> >
> > Is_Valid only reads its parameter, but the portion that is pointed
> > at can be modified asynchronously by another task. So it would be
> > wrong for an analyzer to depend on the value of Is_Valid not
> > changing. (This is a huge challenge when programming with Claw.)
> >
> > So, does this mean that type Data_Access must be included in the
> > Global_In list? (In this particular case, since the type is defined
> > in the private part, the Global_In list would have to be "private").
> >
> > Thanks in advance for your answer.
>
> If you read something you get through an access value, then you will
> need to account for it somehow, as "blah.all", the name of an access
> type, the name of a package, or something like "all aliased [T]".

Right. I suspect some people will not like that much (you have even argued wrt
to constants that such accessed parts are logically part of the passed object).
But in this case, they are *not* logically part of the passed object.

> I think you are also talking about issues that have to multi-threading
> here.  If the asynchronous event can happen at "any" time, then I
> would say you should really declare the "Valid" field as volatile, in
> which case we would probably want some way of stating that the result
> of a function is volatile and hence essentially unpredictable.
>
> If the aynchronous update can only happen during to some kind of
> potentially-blocking or signaling operation, then it should be handled
> the normal way things are handled at potential task signaling/blocking
> points, where some appropriate part of the universe might be affected
> by the actions of other tasks.

Claw uses locks so that the state can't change inside of a Claw-defined routine.
If a state change needs to happen, it is delayed until the lock is available,
meaning after the current routine is finished. But we don't lock things that
only read scalar components (and don't have dependencies), because those can't
be in an inconsistent state: the Valid component can only be True or False.

I suppose that they really ought to be declared volatile, but given the nasty
impact on code generation, and that we only care that Valid is not some value
other than True or False (which can't happen with any of the Ada compilers we've
used), we never did that.

In any case, the pool or object has to be identified somehow in Global_In. That
eliminates my concern.

It does seem that a real proposal would be valuable here. If I had it, I could
point to it rather than duplicating a lot of that in AI-144's discussion.

****************************************************************

(Partial) Minutes of the Amendment subcommittee of the ARG conference call of
December 10, 2009

Attendees: Bob Duff, Tucker Taft, Randy Brukardt, Steve Baird, Gary Dismukes, Ed Schonberg

AI05-0186-1/01

Bob says that this is essential if you ever want to do any analysis of programs
without all of the source code available.

Bob comments that the write up talks about function too much, it should say
subprogram more. Tucker notes that this is mainly an issue in !problem. Randy
notes that the motivating case has to do with functions, so it just talks about
that there.

Bob wonders if we should talk about variables rather than constants. He doesn't
want to annotate reads of global constants. Not all constants are really
constants, however. Calling an entry of tasks if side-effect, even if the task
is a constant. He is not sure what the right answer is (we could except
elementary constants from the rules without problems).

Elementary Operators would have null annotations. Randy notes that composition
of equality means that we have to exclude composite operators, as they might
contain user-defined parts (even array "=" has that problem).

Bob wonders about annotations of the existing predefined packages. In an ideal
world, they would all have them, but that is a heck of a lot of work. Bob notes
that most of the pure packages could use global in/out => null. But access
parameters could cause problems, global in => null is stronger than Pure.

We would want all of the pure packages (like Generic_Elementary_Functions) to
have annotations. We'd like that for the containers, too, but they are mostly
preelaborable.

Randy notes that we'll all have to pitch in on this AI if we want to get it done
on time. Bob will investigate how these annotations could be used on the
unbounded vectors packages.

Ed doesn't like the idea too much. He thinks it is going halfway. If you don't
do data flow it is too imperfect.

Others disagree. You have explicitly include side effects of anything that you
call. That is the same as SPARK. No one thinks SPARK is "too imperfect".

Ed suggests that we might want this on task bodies. That could be used to
prevent/declare unsynchronized access. That seems useful.

Randy notes that in'Class and out'Class would be useful for dispatching calls.
We also would like to have this on access-to-subprogram types.

Bob leaves the call at this point.

We start wondering about the elaboration of entities. Calls that occur in
initialization are definitely included.

Steve notes that you need to worry about default initialization. That's at least
in the spec. It's the body that is hidden that is a problem.

What about instantiating a generic? You would like annotations for things that
happen in the body elaboration there.

That means we have to put aspect specs on bodys. Tucker already had an action
item to do that from St. Pete. He doesn't remember that, and asks for the
minutes draft.

Aspect specs need to be somewhere around the "is" - putting them at the very end
makes no sense. Tucker thinks before the "is". Ed thinks after the "is" makes
more sense. The current end is the ';' the end being the "is" makes more sense.
Gary thinks that would read OK.

Initialize procedures also need their side effects included.

Steve wonders about user-defined storage pools, those too ought be included.

Lots more wording to add, especially for implicit calls.

Access_subtype_name really ought to be Access_subtype_mark. For general access,
it would mean everything aliased covered by the designated type, plus the
storage pool. For all access types, also include the side effects of any
allocate/deallocate routines. (What about function Storage_Size?)

Is this privacy-preserving? In that case, a private type would need an
annotation for default initialization and finalization. But you can't really
have one without the other. Well, you could if you don't use the default
initialization. Tucker says that you ought to be responsible for them anyway. So
only a single annotation is needed for a private type.

Steve would like this to preserve the separation of static and dynamic
semantics. That is the intent - he notes that Pure does not do that. That means
the wording shouldn't talk about what happens at elaboration.

****************************************************************

Questions? Ask the ACAA Technical Agent