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

Unformatted version of ai12s/ai12-0079-1.txt version 1.10
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, 2017  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, 2017  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?]

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

From: Tucker Taft
Sent: Tuesday, June 13, 2017  3:54 AM

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

I left it there purely for comparison.  Initially I thought I would keep the
old style as an option, but ultimately decided to fix all the wording to
presume we go with the new style.  So  better would probably be to put the
OLD STYLE stuff in the !discussion or the !proposal.

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

Good question.  Perhaps it should just be "<identifier> IN” from a syntax
point of view, where <identifier> is either “proof” or some
implementation-defined identifier.

> (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.

I tried to do that and it just started getting really complicated.  So I
punted and chose to allow a name that refers to a non-preelaborable constant,
but otherwise ignoring it later.  I agree the wording needs work.  Perhaps
better would be to just allow an implementation-defined extension to the
syntax, and not talk about it further.  Non-preelaborable constants match
pretty closely to what SPARK requires, but it is probably just confusing to
give only part of that.

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

Sorry about that.  Yes I began to notice too many “*”s there, but didn’t have
time to go back and decide what should be the defining occurrence.

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

From: Randy Brukardt
Sent: Tuesday, June 13, 2017  1:15 PM

...
> > (3) "/object_/name identifies the specified global variable (or 
> > non-preelaborable constant, which is ignored for the purposes of the 
> > remaining rules)" I'm not sure "ignored" is the right way to put this.
...
> I tried to do that and it just started getting really complicated.  So 
> I punted and chose to allow a name that refers to a non-preelaborable 
> constant, but otherwise ignoring it later.  I agree the wording needs 
> work.  Perhaps better would be to just allow an implementation-defined 
> extension to the syntax, and not talk about it further.
> Non-preelaborable constants match pretty closely to what SPARK 
> requires, but it is probably just confusing to give only part of that.

I thought that just generally replacing "variable" by "object" in your wording
(except the very first part) would work fine. I do agree that constants that
can be modified (as we had a long debate about) ought to be included here, and
I don't think there is any need to refer to SPARK to explain that. 3.3 is very
clear that not all constants are really constant, and clearly this construct
needs to include them. Referring to "variable" in formal Ada definitions is
almost always wrong, other than in an actual assignment statement target.

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


From: Florian Schanda
Sent: Thursday, June 15, 2017  2:20 AM

> Sorry to be so late.  Hopefully Randy is still in Wisconsin.  I 
> switched over to using in, in out, out.

I like the new syntax you propose, in a way we've come full circle (SPARK 2005
used exactly these). However in SPARK 2014 we've used Input, In_Out, etc. for
reasons of "its more like an aggregate that way" but I was never really happy
with that reasoning.

At the risk of asking a silly question, does proof in make sense as a
parameter mode?

Of course Tuck, if Ada adopts your syntax as its Global syntax then we're
going to have a bit of fun in SPARK trying to make this backwards/forwards
compatible. I suspect the SPARK extension will then just say "you can use
Input as synonym for in, and you can't use both in the same global aspect,
etc."?

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

From: Tucker Taft
Sent: Thursday, June 15, 2017  3:32 AM

> ...
> At the risk of asking a silly question, does proof in make sense as a 
> parameter mode?

I presume you mean for a subprogram.  If we go that route, it would seem to
be similar to having a "ghost" parameter, in which case "ghost in" might be
more appropriate than "proof in."  Perhaps we should make "ghost" into a
reserved word, and allow it on subprograms and types where we currently allow
"abstract" or "null," and in object declarations where the word "constant"
or "aliased" might appear.

> Of course Tuck, if Ada adopts your syntax as its Global syntax then 
> we're going to have a bit of fun in SPARK trying to make this 
> backwards/forwards compatible. I suspect the SPARK extension will then 
> just say "you can use Input as synonym for in, and you can't use both 
> in the same global aspect, etc.”?

You will have to use "Input =>" as equivalent to "in".  The "=>" will be
the most important discriminator, I think.

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

From: Florian Schanda
Sent: Thursday, June 15, 2017  8:19 AM

> You will have to use "Input =>" as equivalent to "in".  The "=>" will 
> be the most important discriminator, I think.

There will be some pain to make sure this is not possible:

with Global => (Input => X,
                out X)

or:

with Global => (Input => X,
                in Y)


Do note that SPARK allows:

with Global => X

and

with Global => (X, Y, Z)

It may be worth to allow these as shorthands for the "in". It would also mirror
parameters (missing mode = in) and really globals are a kind of parameter ;)

Anyways, even with these difficulties I still think the new (yet old) style is
better :)

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

From: Tucker Taft
Sent: Thursday, June 15, 2017  8:26 AM

...
> There will be some pain to make sure this is not possible:
> 
> with Global => (Input => X,
>                out X)

I think you should have a switch that you pass around when doing parsing to be
in one of three states — uncommitted, committed to reserved-word modes,
committed to non-reserved-word modes with “=>”.

...
> It may be worth to allow these as shorthands for the "in". It would 
> also mirror parameters (missing mode = in) and really globals are a 
> kind of parameter ;)

I considered this and ultimately rejected it, as being a short-hand that just
added complexity and ambiguity to the syntax, and only saved two characters.
Yes I know “in” is optional in subprogram parameters, but there is much more
context there.  Here all we have is a mode and a name, and I think omitting
the mode is not helpful.  It is just too easy to interpret a missing mode as
meaning “all access” (i.e. “in out”) rather than read-only access.

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

From: Brad Moore
Sent: Friday, September 1, 2017  6:46 PM

[From a thread in AI12-0119-1 - Editor]

"Although SPARK only allows names of stand-alone objects in Global
annotations, for Ada we allow any object name, presumably including an
indexed component or a slice.  We also have proposed in AI12-0079 to
allow them on formal subprograms and access-to-subprogram, so I think
the cases you mentioned are consistent with the current AI."


Thats great, but one thing that isn't in AI12-0079 is to be able to use the
array keyword, to indicate any array, or arrays, not just a specific named
array.

In a library call, such as my parallelism libraries, the library call has no
knowledge of which global arrays the clients code might access, so I cannot
name these arrays in the specification.

It really doesn't matter which global arrays the client accesses, so long as
only the specified slice of those arrays is accessed. For example, one client 
might sum arrays A and B into C, and another client might sum arrays D and E
into F. It doesn't matter which arrays are accessed, the library guarantees
that the slices wont overlap, which can be viewed as a post condition that the
library implementation promises. The global aspect in this case, however forms
a precondition that ensures that the client will use the library as it was
intended.

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

From: Tucker Taft
Sent: Friday, September 1, 2017  7:50 PM

I don’t see the point of solving this problem only for arrays, when there is a
general challenge associated with mentioning things in a “Global” annotation
that are not normally visible in the spec.  SPARK solves this by allowing the
programmer to invent a notion of “abstract state,” and then defining what that
abstract state comprises in the body.  

On the other hand, this seems like excessive complexity for Ada, and in some
sense harkens back to the days when global variables were used for all kinds
of inter-module communication.  My own view is that we should be discouraging
the use of global variables, and instead rely on Ada’s support for passing
slices if we want to give a subprogram access to only a particular slice of
an array.

Note that even eliminating global annotations completely doesn’t solve the
issue of compile-time checking of data races, given that we could pass two
different slices of the same array to two different parallel calls.  To ensure
these two slices don’t overlap, we would probably still need to define run-time
checks to ensure there is no overlap, with many compilers (hopefully) being
able to eliminate the check at compile-time.

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

From: Randy Brukardt
Sent: Tuesday, September 5, 2017  7:20 PM

> I don't see the point of solving this problem only for arrays, when 
> there is a general challenge associated with mentioning things in a 
> "Global" annotation that are not normally visible in the spec.

Right. This is just part of a much more general problem.

> SPARK solves this by allowing
> the programmer to invent a notion of "abstract state," and then 
> defining what that abstract state comprises in the body.
> 
> On the other hand, this seems like excessive complexity for Ada, and 
> in some sense harkens back to the days when global variables were used 
> for all kinds of inter-module communication.  My own view is that we 
> should be discouraging the use of global variables, and instead rely 
> on Ada's support for passing slices if we want to give a subprogram 
> access to only a particular slice of an array.

That doesn't fix anything in the case of generic units, though. I was rather
expecting/hoping that you'd use a version of the attribute mechanism that I
worked out for Nonblocking for Global as well.

In particular, giving a Global aspect on a generic formal requires some form
of generic matching:

    generic
       type Priv is private;
       with procedure Do_It (Param : in out Priv)
            with Global => in out null;
    package Gen1 is ...

In this case, actual subprograms to Do_It have to "match" (in some sense -
stronger should be allowed, weaker not allowed) the "in out null" Global
aspect. But that is incompatible in interesting cases.

    generic
       type Priv is private;
       with procedure Do_It (Param : in out Priv);
    package Gen2 is
       procedure Frobnicate (Param : in out Priv)
           with Global => Do_It'Global and package Gen2;
    end Gen2;

Here, we're "reflecting" the Global aspect of the generic formal through a
outine of the generic package (and also allowing local package state).
This keeps compatibility while providing the maximum capability for the
routines. We'll need such a mechanism to allow the containers (which can't
get incompatible) to be used in checked parallel structures (and any other
uses of the Global aspect).

Note that these attributes provide a "poor man's" way to name a specific
Global state. One can always declare a dummy subprogram:

    procedure Global_State with Global => ...;

and then use that Global setting in other subprograms.

    procedure Bletch with Global => Global_State'Global and in out Foobar;

There does seem to be a need to somehow describe data of private helper
packages without naming the packages. That seems important for the Ada
runtime, as we don't want to force all of the implementations to internally
structure their Ada library the same way.

(Case in point: Janus/Ada has a library System.Basic_IO that implements the
underlying I/O operations; I believe GNAT has a similar library but of course
with a different name. The handles for Stdin, Stdout, and Stderr are found
there; those can't change during a run but aren't constant as they are
determined dynamically during the program startup.)

The SPARK scheme would work for that, but it seems like overkill.

> Note that even eliminating global annotations completely doesn't solve 
> the issue of compile-time checking of data races, given that we could 
> pass two different slices of the same array to two different parallel 
> calls.  To ensure these two slices don't overlap, we would probably 
> still need to define run-time checks to ensure there is no overlap, 
> with many compilers (hopefully) being able to eliminate the check at 
> compile-time.

Yes, that seems reasonable. Perhaps we have to handle race conditions arising
from Atomic object misuse the same way? (Updates like Atom := Atom + 1; are
not safe as these are separate reads and writes.)

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

Questions? Ask the ACAA Technical Agent