Version 1.8 of ai12s/ai12-0079-1.txt

Unformatted version of ai12s/ai12-0079-1.txt version 1.8
Other versions for file ai12s/ai12-0079-1.txt

!standard 6.1.2(0)          17-06-12 AI12-0079-1/04
!class Amendment 13-06-28
!status work item 13-06-28
!status received 13-06-14
!priority High
!difficulty Hard
!subject Global-in and global-out annotations
!summary
Annotations are provided to describe the use of global objects by subprograms.
!problem
Ada 2012 added many kinds of assertions to Ada in order to increase the ability of a programmer to specify contracts for types and subprograms. These contracts are defined to be checked at runtime, but are intended to be potentially checked (at least in part) statically.
However, without knowledge of side-effects of functions used in the aspects, a tool has to assume the worst about any user-defined functions. For example, that the result of a function can change even when called with the same operands. Other assumptions could cause incorrect programs to be accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution. Both of these results are unacceptable for a feature intended to improve the correctness of programs.
The worst-case assumptions pretty much prevent any analysis unless the bodies of any user-defined functions used in the aspects are available. This is bad, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body require creating pseudo body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again); but the language does not allow these to be "real" body dependencies (any recompilation needed has to occur automatically).
Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side-effects is needed in the specification of subprograms in order to accomplish that goal.
!proposal
[Note: the following is mostly a direct quote from the paper "Safe Parallel Programming in Ada with Language Extensions" prepared for HILT 2014.]
To encourage convergence with SPARK we are starting from the SPARK Global aspect. However, for Ada, it is necessary to extend this aspect to cover a broader spectrum of usage, since Ada includes access types and other features not allowed in SPARK.
The Global aspect in SPARK 2014 is applied to subprogram specifications, and is of the following form:
with Global => (Input => ...,
In_Out => ..., Output => ...)
where "..." is either a single name, or a parenthesized list of names, and Input, In_Out, and Output identify the variables global to the subprogram that are accessed by this subprogram, in read-only, read-write, or write-only mode, respectively. If there are no variables global to the subprogram accessed with a particular parameter mode, then that mode is omitted from the specification. If there are only global inputs, and no outputs or in-outs, then this syntax can be further simplified to:
with Global => ...
where again "..." is a single name, or a parenthesized list of names.
Finally, if there are no global inputs, in-outs, nor outputs, then:
with Global => null
is used.
We need to refine the notion of SPARK's Global aspect, because SPARK does not support access types, and because SPARK relies on an elaborate mechanism for handling the abstract "state" of packages. The refinements we are proposing are the following:
1. Allow the name of an access type A (including "access T") to stand-in for the set of objects described roughly by:
(for all X convertible to A => X.all)
2. Allow the name of a package P to stand-in for the set of objects described roughly by:
(for all variables X declared in P => X)
3. Allow the word synchronized to be used to represent the set of global variables that are tasks, protected objects, or atomic objects.
4. Allow the word all to be used to represent the set of all variables global to the subprogram, including variables designated by access values of types global to the subprogram.
5. Switch to using the normal Ada parameter modes, in, in out, and out rather than Input, In_Out, and Output.
Note that references to global constants do not appear in Global annotations. In the absence of a global aspect, a subprogram in a pure package is presumed to reference no global variables (Global => null), while a subprogram in an impure package is presumed to read and write an unspecified set of global variables, including non-synchronized ones (Global => in out all).
We also allow a Global aspect on a package, which can be used to establish a default for all subprograms declared within the package specification. The default can be overridden for any particular subprogram by specifying the Global aspect for that subprogram.
For dispatching operations, a Global'Class aspect may be specified, which represents an upper bound on the set of up-level variables that any particular overriding of that operation may reference in each of the specified modes. In the absence of a Global'Class aspect, the default for the Global aspect is used for the Global'Class aspect.
!wording
Add the following section:
6.1.2 The Global and Global'Class Aspects
For a program unit, 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 with an aspect_specification (see 13.1.1):
Global
The syntax for the aspect_definition used to define a Global aspect is as follows:
global_aspect_definition ::= primitive_global_aspect_definition | /global_/attribute_reference | global_aspect_definition & /global_/attribute_reference
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_set ::= global_name {, global_name} | global_designator
global_designator ::= all | synchronized | null
------
global_name ::= /object_/name | /package_/name | /access_/subtype_mark | access subtype_mark
A /global_/attribute_reference is an attribute_reference with attribute designator "Global."
The Global aspect identifies the set of variables global to a callable entity that are potentially read or updated as part of the execution of a call on the entity. If not specified, the aspect defaults to the Global aspect for the nearest enclosing program unit. If not specified for a library unit, the aspect defaults to "Global => null" for a non-generic library unit that is declared Pure, and to "Global => in out all" otherwise.
For a dispatching subprogram or a tagged type, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
Global'Class
The syntax for the aspect_definition used to define a Global'Class aspect is the same as that defined above for global_aspect_definition. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the nearest enclosing program unit.
Name Resolution Rules
A global_name that does not have the reserved word ACCESS shall resolve to statically denote a variable (or non-preelaborable constant), a package (including a limited view of a package), or an access-to-variable subtype. The subtype_mark of a global_name that has the reserved word ACCESS shall resolve to denote a subtype (possibly an incomplete type).
Static Semantics
A global_aspect_definition defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side-effect of some operation. The Global'Class aspect associated with a tagged type T (or one of its dispatching operations) represents a restriction on the Global aspect on any descendant of type T (or its corresponding operation).
The Global aspect for a callable entity defines the global variables that might be referenced as part of a call on the entity. The Global aspect for a composite type identifies the global variables that might be referenced during default initialization, adjustment as part of assignment, or finalization of an object of the type. The Global aspect for an access-to-subprogram object (or type) identifies the global variables that might be referenced when calling via the object (or any object of that type). In the following we talk 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 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 each global_mode include all objects identified for the mode in the primitive_global_aspect_definition, if any, plus all objects associated with the given mode for the entities identified by the prefixes of the /global_/attribute_reference's, if any.
A global_set identifies a global variable set as follows:
* "null" identifies the empty set of global variables;
* "all" identifies the set of all global variables;
* "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:
* /object_/name identifies the specified global variable (or non-preelaborable constant, which is ignored for the purposes of the remaining rules)
* /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;
* /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 can be designated by values of an access-to-variable type with a designated subtype statically matching the given subtype_mark.
Legality Rules
Within a primitive_global_aspect_definition, a given global_mode shall be specified at most once. 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.
If an entity has a Global aspect other than IN OUT ALL, then the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the IN, IN OUT, or OUT modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the IN OUT or OUT global_modes. This includes any calls occurring during the execution of the operation, presuming those calls read and update all global variables permitted by their Global aspect (or Global'Class aspect, if a dispatching call). If a variable global to the entity is read that is within the global variable set associated with the OUT global_mode, it shall be updated somewhere within the callable entity (or an entity it calls). 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.
For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the IN OUT mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of T. A corresponding rule applies to the Global aspect of a tagged type T relative to the Global'Class aspect of any ancestor of T.
For a prefix S that statically denotes a subprogram (including a formal subprogram), formal object of an anonymous access-to-subprogram type, or a type (including a formal type):
S'Global Identifies the global variable set for each of the three
global_modes, for the given subprogram, object, or type; a reference to this attribute may only appear within a global_aspect_definition.
Modify 13.1.1(4/3)
aspect_definition ::= name | expression | identifier{ | global_aspect_definition}
[Author's TBD: annotating the language-defined packages]
!discussion
Global annotations are critical to being able to perform any sort of modular static analysis.
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 reading of "out" mode globals, so long as there is at least one update of the global variable as well.
Note that it is possible to lie about the use of globals of subprograms and other entities that are imported. This is of course impossible to check, but thankfully is covered by B.1(38.1/2). Incorrect annotations on imported subprograms could cause a program to be erroneous.
SPARK does not currently support identifying particular components of a global variable in the Global aspect, but for Ada we plan to allow that. This is somewhat inconsistent with what can be specified for parameters, since there is no easy way to identify which components of an in-out parameter are actually updated. It is possible to specify in a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that can be a maintenance issue as the names and numbers of subcomponents changes, and only works for types that have an appropriate "=" operator. It might be useful to have another aspect that indicated which components of an in-out parameter might be modified, with all others presumably being preserved (e.g. Modified => (X.A, X.B)).
Note that SPARK has a "Refined_Global" aspect which can be specified on the body of a subprogram, to specify a more restricted set of globals for those callers that have visibility on the body. This could be added at a later point if it was felt to be important.
!example
package Random is procedure Set_Seed(Seed : Float); with Global => out Random; -- Initialize state of Random package
function Next_Random return Float with Global => in out Random; -- Update state of Random package end Random;
The Random package presumably has hidden state, which is represented by the name of the package itself in a global_aspect_definition.
generic type T is private; with function Hash(X : T) return Hash_Code; package Sets is type Set(Capacity : Positive) is private with Global => T'Global;
procedure Insert(S : in out Set; X : T) with Global => Hash'Global & T'Global;
... end Sets;
The Sets package only updates global variables via its formal parameters. The default initialization, adjustment, and finalization of a Set indirectly uses the corresponding operations of T. Insert uses Hash and T's assignment operation.
!ASIS
** TBD.
!ACATS test
ACATS tests should be created to test that the new annotations are correctly enforced.
!appendix

From: Tucker Taft
Sent: Monday, October 6, 2014  10:27 AM

The recent paper submitted to HILT by Steve Michell, Miguel Pinho, Brad Moore,
and myself, suggests more details about a Global annotation for Ada, based on
the SPARK 2014 work. This relates to AI12-0079.  Below is the section on this
from the final paper.

-Tuck
-----

One of the strengths of Ada is that it was carefully designed to allow the
compiler to detect many problems at compile time, rather than at run time.
Programming for parallel execution in particular is an activity that requires
care to prevent data races and deadlocks. It is desirable that any new
capabilities added to the language to support parallelism also allow the
compiler to detect as many such problems as possible, as an aid to the
programmer in arriving at a reliable solution without sacrificing performance
benefits.

A common source of erroneousness in languages that support concurrency and
parallelism are data races, which occur when one thread of execution attempts to
read or write a variable while another thread of execution is updating that same
variable. Such a variable is global in the sense that it is globally accessible
from multiple threads of execution. In the current Ada standard, threads of
execution are tasks. In this proposal, tasklets are another form of execution
threads.

Eliminating concurrency and parallelism problems associated with non-protected
global variables is an important step towards improving the safety of the
language. To that end, we propose the addition of a Global aspect to the
language.  The main goal in the design of this aspect is to identify which
global variables and access-value dereferences a subprogram might read or
update.

The inspiration for this aspect comes from the SPARK language [24], which has
always had global annotations. Earlier versions of SPARK augmented a subset of
Ada with annotations added as specially formatted comments, which were used for
static analysis by the proof system. With the addition of aspects to Ada in Ada
2012, SPARK 2014 has changed its annotations to use aspects, including the
“Global” annotation. To encourage convergence with SPARK we are starting from
the SPARK Global aspect. However, for Ada, it is necessary to extend this idea
to cover a broader spectrum of usage, since Ada is a more expressive programming
environment than SPARK. The Global aspect in SPARK 2014 is applied to subprogram
specifications, and is of the following form;

with Global =>(Input => ...,
                In_Out => ..., Output => ...)

where “…” is either a single name, or a parenthesized list of names, and Input,
In_Out, and Output identify the global variables of the program that are
accessed by this subprogram, in read-only, read-write, or write-only mode,
respectively. If there are no global variables with a particular parameter mode,
then that mode is omitted from the specification. If there are only global
inputs, and no outputs or in-outs, then this syntax can be further simplified
to:

with Global => ...

where again "..." is a single name, or a parenthesized list of names.
Finally, if there are no global inputs, in-outs, nor outputs, then:
with Global => null
is used.

We needed to refine the notion of SPARK's Global aspect, because SPARK does not
support access types, and because SPARK relies on an elaborate mechanism for
handling the abstract “state” of packages.  The refinements we are proposing are
the following:

1.	Allow the name of an access type A (including "access T") to stand-in
	for the set of objects described by:
(for all X convertible to A => X.all)

2.	Allow the name of a package P to stand-in for the set of objects
	described by:
(for all variables X declared in P => X)

3.	Allow the word synchronized to be used to represent the set of global
	variables that are tasks, protected objects, or atomic objects.

Note that references to global constants do not appear in Global annotations. In
the absence of a global aspect, the subprogram is presumed to read and write an
unspecified set of global variables, including non-synchronized ones.

...

If one wants to know whether a subprogram has side-effects, it is important to
know about all data that might be read or written. Access types introduce
difficulties in determining such side-effects, since the side-effects might
result after a dereference of a series of pointers to reach an object to be
updated.  Our proposal addresses this by allowing the programmer to specify the
name of an access type in a Global aspect. This would be essentially equivalent
to writing something like;

Global => (In_Out => *.all)

except we can be more specific about the type of the access values being
dereferenced. For example, consider a visible access type declared as;

type Acc is access T;

and a subprogram that has a value of type Acc in local variable Local, which it
then uses to read and update an object via Local.all.  It would not be very
useful to write:

Global => (In_Out => Local.all)

since "Local" means nothing to the caller.  But it could write:

Global => (In_Out => Acc)

to indicate that the caller should be aware that a call on this subprogram is
updating some object by dereferencing an access value of type Acc. Another
problematic case involves specifying in a Global aspect a variable that is
declared inside a package body.  Directly naming such a variable would not have
meaning to the caller of the subprogram, and would violate encapsulation.
Similarly, suppose an access type is declared inside the body or private part of
package P. In both these cases, we treat the private updatable objects as a part
of the overall state of package P.  We then simply indicate that the subprogram
is updating some or all of the state of package P:

Global => (In_Out => P)

Now suppose that the objects being updated are all protected or atomic objects.
Then the caller doesn't really need to worry about which objects are being read
or updated.  It is always safe to call the subprogram concurrently.  It has some
side effects, so you cannot assume it is a "pure" subprogram. In this case, we
could describe the effects as:

Global => synchronized

if it only reads synchronized objects, or:

Global => (In_Out => synchronized)

if it might update synchronized objects as well.

One might be concerned that the number of globals in a subprogram higher in the
call structure of a larger program might be unmanageable to specify in a Global
aspect. To address this concern we propose a shorthand for the Global aspect:

Global => (In_Out => all)

where “all” represents all global variables. If the number of non-synchronized
globals does get large, then it is likely that the subprogram cannot be used in
a parallel context anyway, hence using all is generally adequate.  By default,
the global aspect is (In_Out => all) for normal subprograms, and null for
subprograms in a declared-pure package.

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

From: Bob Duff
Sent: Tuesday, October 14, 2014  5:20 PM

> Here is an AI on the Global aspect, based on SPARK and on the HILT
> 2014 paper on parallel language extensions for Ada.

Looks good.  You make it look so simple.  So why didn't we already do this?
I guess the Devil's in the "!wording".

See below for editorial comments and some questions.

> !summary
>
> Annotations are provided to describe the use of global objects by subprograms.
                                                         ^^^^^^^

variables

> !problem
>
> Ada 2012 added many kinds of assertions to Ada in order to increase
> the ability of a programmer to specify contracts for types and
> subprograms. These contracts are defined to be checked at runtime, but
> are intended to be potentially checked (at least in part) statically.
>
> However, without knowledge of side-effects of functions used in the
> aspects, a tool has to assume the worst about any user-defined
> functions. For example, that
                                                        ^^^^^^^^^ subprograms

> the result of a function can change even when called with the same
> operands. Other assumptions could cause incorrect programs to be
> accepted as correct, and if the assumptions were used to omit "proved"
> aspects, to erroneous execution.
                           ^^^^          ^^^^^^^

I think you mean "suppress...checks".  If not, please explain.

> Both of these results are unacceptable for a feature intended to
> improve the correctness of programs.
>
> The worst-case assumptions pretty much prevent any analysis unless the
> bodies of any user-defined functions used in the aspects are
> available. This is bad, as it prevents analysis of programs as they
> are constructed. If the body is not available, no analysis is
> possible. Moreover, analysis depending on a body require creating
> pseudo body dependencies (if the body is changed, any analysis
> depending on the properties of that body would have to be performed
> again); but the language does not allow these to be "real" body
> dependencies (any recompilation needed has to occur automatically).

I agree, having to look at bodies is "bad", but those don't seem like the main
reasons why.  To me, the main reason is the usual software engineering one: you
want well-defined interfaces, and you want to depend ONLY on those interfaces
(i.e. specs).  If you prove something about package body X, you want that proof
to be valid in the presence of arbitrary changes to bodies called by X.

> We need to refine the notion of SPARK's Global aspect, because SPARK
> does not support access types, and because SPARK relies on an
> elaborate mechanism for handling the abstract “state” of packages.

What's your opinion about that elaborate mechanism?  I've never understood why
it's needed, but I'm told by SPARK folks that it's super-useful.  I'd like to
understand why, and whether we ought to add such stuff to Ada.

>...The
> refinements we are proposing are the following:
>
> 1.	Allow the name of an access type A (including "access T") to
> stand-in for the set of objects described roughly by:

"stand in" (no dash)

>    (for all X convertible to A => X.all)

That's the same thing as the collection of A, right?

> 2.	Allow the name of a package P to stand-in for the set of objects
> described roughly by:
>
>    (for all variables X declared in P => X)

Does that include children of P?

> !wording
>
> ** TBD.

;-)  ;-)

> !discussion
>
> Global annotations are critical to being able to perform any sort of
> modular static analysis.

Yeah, that's what I meant by my "software engineering" comment above.

> All of the global in, in-out, and out annotations proposed can be
> statically checked.
>
> Note that it is possible to lie about the use of globals of
> subprograms and other entities that are imported. This is of course
> impossible to check, but thankfully is covered by B.1(38.1/2).
> Incorrect annotations on imported subprograms could cause a program to be
> erroneous.
>
> SPARK does not currently support identifying particular components of
> a global variable in the Global aspect, but for Ada we plan to allow that.
> This is somewhat inconsistent with what can be specified for
> parameters, since there is no easy way to identify which components of
> an in-out parameter are actually updated. It is possible to specify in
> a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that
> can be a maintenance issue as the names and numbers of subcomponents
> changes, and only works for types that have an appropriate "=" operator.
> It might be useful to have another aspect that indicated which
> components of an in-out parameter might be updated, with all others
> presumably being preserved (e.g. Updated => (X.A, X.B)).

Yes, I'm a fan of limited types, and I'd like to be able to say things like
that.

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

From: Tucker Taft
Sent: Tuesday, October 14, 2014  9:37 PM

...
>> However, without knowledge of side-effects of functions used in the
>> aspects, a tool has to assume the worst about any user-defined
>> functions. For example, that
>                                                          ^^^^^^^^^
> subprograms
>
>> the result of a function can change even when called with the same
>> operands. Other assumptions could cause incorrect programs to be
>> accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution.
>                             ^^^^          ^^^^^^^
>
> I think you mean "suppress...checks".  If not, please explain.

I didn't actually write the "problem" statement.  I think it might be Randy's original wording.


>> Both of these results are unacceptable for a feature intended to
>> improve the correctness of programs.
>>
>> The worst-case assumptions pretty much prevent any analysis unless
>> the bodies of any user-defined functions used in the aspects are
>> available. This is bad, as it prevents analysis of programs as they
>> are constructed. If the body is not available, no analysis is
>> possible. Moreover, analysis depending on a body require creating
>> pseudo body dependencies (if the body is changed, any analysis
>> depending on the properties of that body would have to be performed
>> again); but the language does not allow these to be "real" body
>> dependencies (any recompilation needed has to occur automatically).
>
> I agree, having to look at bodies is "bad", but those don't seem like
> the main reasons why.  To me, the main reason is the usual software
> engineering one: you want well-defined interfaces, and you want to
> depend ONLY on those interfaces (i.e. specs).  If you prove something
> about package body X, you want that proof to be valid in the presence
> of arbitrary changes to bodies called by X.

Agreed.  Again, this problem statement was from an earlier version of the AI.
It seemed adequate to capture the problem, but it could perhaps use some
wordsmithing.

>> We need to refine the notion of SPARK's Global aspect, because SPARK
>> does not support access types, and because SPARK relies on an
>> elaborate mechanism for handling the abstract “state” of packages.
>
> What's your opinion about that elaborate mechanism?  I've never
> understood why it's needed, but I'm told by SPARK folks that it's
> super-useful.  I'd like to understand why, and whether we ought to add
> such stuff to Ada.

The elaborate mechanism is needed if you make heavy use of global variables.
I have come to really hate global variables, so for me, it seems to only
encourage an evil habit.  But when it comes to typical embedded software, I
know that it is quite common to have a huge number of global variables
representing the state of the environment.  These global variables are
periodically updated as the result of sensor readings, and they are read
whenever needed by algorithms trying to react to the environment.  I would
hope there are better ways to structure such systems, but I think SPARK is
trying to deal with reality as we know it, and many of these systems seem
to represent the state using globals.

>> ...The
>> refinements we are proposing are the following:
>>
>> 1.	Allow the name of an access type A (including "access T") to
>> stand-in for the set of objects described roughly by:
>
> "stand in" (no dash)

Good point.

>>     (for all X convertible to A => X.all)
>
> That's the same thing as the collection of A, right?

Yes for a pool-specific access type, no for a general access type.

>> 2.	Allow the name of a package P to stand-in for the set of objects
>> described roughly by:

"stand in" here too.

>>
>>     (for all variables X declared in P => X)
>
> Does that include children of P?

It would presumably need to include the private children of P, but not the
public children, as you could name them separately.

>> ...
>> It might be useful to have another aspect that indicated which
>> components of an in-out parameter might be updated, with all others
>> presumably being preserved (e.g. Updated => (X.A, X.B)).
>
> Yes, I'm a fan of limited types, and I'd like to be able to say things
> like that.

If we adopt something like "Updated" then it might make sense to keep Global
at the whole-object level, and use "Updated" to provide more precision for both
parameters and globals.

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

From: Randy Brukardt
Sent: Wednesday, November 12, 2014  9:51 PM

> > Here is an AI on the Global aspect, based on SPARK and on the HILT
> > 2014 paper on parallel language extensions for Ada.
>
> Looks good.  You make it look so simple.  So why didn't we already do
> this?  I guess the Devil's in the "!wording".

Mostly FUD, really. You and I spent a lot of hours creating AI05-0186-1,
complete with wording. (Perhaps you've forgotten about that.) People were
concerned that it was insufficiently mature, so it didn't end up as part of
Ada 2012.

Also, I think there was a desire to let SPARK 2014 plow this ground first
(which only covers part of the problem, of course).

Unfortunately, most of the work will have to be redone; hopefully Tucker et.
al. will be able to use some of the wording created for AI05-0186-1 so the
effort won't totally go to waste.

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

From: Tucker Taft
Sent: Wednesday, June 17, 2015  8:39 AM

Here is a first attempt at wording for the Global/Global'Class aspects.
[This is version /02 of the AI - Editor.]

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

From: Randy Brukardt
Sent: Thursday, June 18, 2015 12:47 AM

> Here is a first attempt at wording for the Global/Global'Class
> aspects.
...
> If a callable entity has a Global aspect other than (In_Out => all),
> then it shall read only those variables global to the entity that are
> within the *global variable set* identified by either the Input or
> In_Out global_modes, and it shall update only those variables global
> to the entity that are within the *global variable set* identified by
> either the In_Out or Output global_modes. This includes any calls
> within the body of the callable entity, presuming those calls read and
> update all global variables permitted by their Global aspect (or
> Global'Class aspect, if a dispatching call).

I find this rather simplistic, since it seems to require the reader and the
compiler to look through a near-infinite set of possible global variables
(especially in the call case). Perhaps there is a better way to describe this
without requiring that (perhaps some type of matching).

I had thought that the term "global" was undefined in Ada, but it actually is
defined in 8.1. Who knew? (I've been using it in an English sense forever.)

---

As with nonbounded, there doesn't seem anything for formal subprograms. I don't
think there is any way to write a container package with these annotations
unless there is some way to control the actual subprograms and/or export the
same annotations on the routines that call the formal subprograms. The
annotations are next to useless if you can't write a generic container using
them (and preferably, they'll work with the existing containers).

---

There clearly has to be some rules for predefined operations. Most of them
should have global => null, but beware of record equality, which can incorporate
user-defined "=". I never figured out a good way to handle that (requiring
global => null on those as well would have been great, but it's at least 35
years too late for that).

---

The entire predefined library needs to be decorated. In the old AI, I proposed
doing that by having some defaults for pure library units (which shouldn't have
any global state), but we'd still want to manually do it for the containers and
possibly other useful packages (probably not for the I/O packages). Perhaps that
should be a separate AI or AIs due to the size.

Enough comments for tonight.

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

From: Tucker Taft
Sent: Sunday, June 5, 2016  4:26 PM

I made some significant updates, to some degree following Randy's approach for
Nonblocking.  Nonblocking and Global are quite similar in various ways, as they
essentially represent side effects of operations.  It might be nice if they
could somehow share more wording.  Biggest change was to add a 'Global attribute
for use in generics (similar to Randy's use of the 'Nonblocking attribute), and
to define the meaning of 'Global on a composite type, being the globals
referenced during the initialization, adjustment, and finalization operations of
the type.

[Version /03 of this AI was attached - Ed.]

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

From: Tucker Taft
Sent: Monday, June 12, 2016  6:26 PM

Sorry to be so late.  Hopefully Randy is still in Wisconsin.  [This was version
/04 of the AI.] I switched over to using in, in out, out.   I now require the
mode to be specified, even if it is "in", since otherwise the syntax was just
too funky.  I added "proof in" to support use in assertion expressions, and
allowed references to limited views of packages and incomplete views of types,
so "limited with" can be of some use.  I removed public children from what is
covered by Global => in Pkg_Name, but left the visible part, since with a
limited view of a package, it wouldn't be possible to refer to individual
declarations from the visible part.

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

From: Randy Brukardt
Sent: Monday, June 12, 2016  7:48 PM

Generally looks good. Some free association:

(1) Not sure why you have "OLD STYLE" and "NEW STYLE" grammars. It just looks
confusing. "Old Style" is cheap beer, not something that belongs in an AI. ;-)

(2) The "New Style" grammar contains "proof" explicitly like a reserved word.
Are you proposing a new reserved word, to fight about unreserved keywords yet
again (this seems like a perfect use for such a thing), or something else??

(3) "/object_/name identifies the specified global variable (or
non-preelaborable constant, which is ignored for the purposes of the
remaining rules)" I'm not sure "ignored" is the right way to put this. I think
you're trying to say that the possibility of non-preelaborable constants isn't
mentioned in later rules. But that's a bit weird, because many of the later
rules talk only about variables, and it would seem easy enough to talk about
"objects", at least in the three following rules. Or maybe describe them as a
term covering variables and non-preelaborable constants.

(4) Minor glitch: You ought to only italicize the defining occurrence of a term,
you've got every occurrence of "global variable set" in italics (signified by
surrounding by *s). [BTW, wouldn't it be better to call this a "global object
set", since some constants are included? Rather than telling people to "ignore"
the possibility of a constant being included? Why lie if you don't have to?]

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

Questions? Ask the ACAA Technical Agent