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

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

!standard 6.1.2(0)          17-09-25 AI12-0079-1/05
!class Amendment 13-06-28
!status work item 13-06-28
!status received 13-06-14
!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 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 ::= Synthesized | primitive_global_aspect_definition | /global_/attribute_reference | global_aspect_definition & /global_/attribute_reference
primitive_global_aspect_definition ::= null | global_mode global_name | global_mode global_designator | (global_mode global_set{, global_mode global_set})
global_mode ::= [ global_mode_qualifier ] basic_global_mode
global_mode_qualifier ::= synchronized | /implementation-defined_/identifier
basic_global_mode ::= in | in out | out
global_set ::= global_name {, global_name} | global_designator
global_designator ::= all | null
global_name ::= /object_/name | /package_/name [ private ] | /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). The following is defined in terms of operations; the rules apply to all of these kinds of entities.
The sets of global variables associated with a Global aspect can be defined explicitly with a primitive_global_aspect_definition or can be defined by combining with the sets specified for other entities by referring to their Global attribute. Alternatively, the Global aspect may be defined using the aspect-specific identifier "Synthesized" which means the implementation will determine in an implementation-defined manner the sets of global variables that might be referenced by uses of the entity.
The global variables associated with any mode can be read as a side effect of an operation. The IN OUT and OUT global_modes together identify the set of global variables that can be updated as a side effect of an operation. The global_mode_qualifier SYNCHRONIZED reduces the set to those objects that are of one of the following sort of types:
* a protected, task, or synchronized tagged type;
* an atomic type;
* a descendant of the language-defined types Suspension_Object or Synchronous_Barrier;
* a record type all of whose components are *sychronized* in this sense.
An implementation-defined global_mode_qualifier may be specified, which reduces the set according to an implementation-defined rule.
The overall set of objects associated with each global_mode include all objects identified for the mode in the primitive_global_aspect_definition (subject to the global_mode_qualifier), if any, plus all objects associated with the given mode for the entities identified by the prefixes of the /global_/attribute_reference's, if any.
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;
* "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; if the reserved word PRIVATE follows the /package_/name, the set is reduced to those variables declared in the private part or body of the package or within a private descendant of the package;
* /access_/subtype_mark identifies the set of (aliased) variables that can be designated by values of the given access-to-variable type;
* ACCESS subtype_mark identifies the set of (aliased) variables that 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 without a global_mode_qualifier, and at most once with any given global_mode_qualifier. Similarly, within a primitive_global_aspect_definition, a given entity shall be named at most once by a global_name.
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).
If an implementation-defined global_mode_qualifier applies to a given set of variables, an implementation-defined rule determines what sort of references to them permitted.
For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the IN OUT mode, of the 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 allowed for an implementation-defined global_mode_qualifier, which would allow "proof in" for SPARK. Similarly, we have allowed for a aspect-specified identifier "Synthesized" to indicate that the implementation will determine the global objects referenced by uses of the entity.
We have allowed reading of "out" mode globals, so long as there is at least one update of the global variable as well.
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's execution to be erroneous.
SPARK does not currently support identifying particular components of a global variable in the Global aspect, but for Ada we plan to allow that. 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.)

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

From: Brad Moore
Sent: Saturday, September 16, 2017  1:13 PM

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

OK, but I now am proposing a more general solution to the more general
problem, at least generalizing this to work for both arrays and containers.

Instead of the array keyword that I suggested earlier, suppose we
extended the global aspect to include the syntax form;

       global => all (name1 .. name2)

The idea here is that this indicates that the only use of globals is via
indexing lookups (via a range of scalar indexes, or container cursors).
The keyword "all" here represents all visible globals. Specific global
names could be used also, with the same index/slicing syntax.

The compiler would do the normal processing for global checks, but if
the only use of globals is via the specified slice of the container or
array, then the global check would pass.

We could say that this implies that the only use of these globals is via
a  loop cursor of a for loop that mentions name1 and name2 to initialize
the loop cursor, so I would think it would be pretty easy for the
compiler to check this.

To do a slice of a container, we just need an iterator that can operate
on a slice of a container.

The existing containers almost already support this, because there
exists Iterate calls that allow you to specify the start of iteration.

eg. For Doubly_Linked_Lists

     for Item in My_List.Iterate (Start => My_Cursor) loop
        ....
     end loop;

If we had an Iterate call that allowed you to specify both the Start and
the Finish cursors, then one could write;

     for Item in My_List.Iterate (Start => My_Start_Cursor, Finish =>
My_End_Cursor) loop
        ....
     end loop;

In fact, I don't know why we don't already have these calls. They would
be more useful than the ones we have today that allow you to only
specify the start cursor, with the end cursor implicitly being
container.Last;

C++ iterators for instance allow one to iterate through a subset of an
array or container. It seems like
useful functionality.

We could either add a default parameter for Finish that defaults to
Last, or add a new call for the Container libraries.

As a simple example of the global syntax, consider a very basic parallel
loop library;
Note I am using Randy's 'global attribute, as I think it is needed also.

generic
    type Loop_Index is range <>;

    with procedure Process (Start, Finish : Loop_Index)
           with Pre    => (Start < Finish),       -- Can we currently
put pre and post on formals?
                  Global => all (Start .. Finish);  --
package Parallel is

    procedure Parallel_Loop
      (From : Loop_Index := Loop_Index'First;
       To   : Loop_Index := Loop_Index'Last);
       with Process'Global and Global => null;

end Parallel;

package body Parallel is

    procedure Parallel_Loop
      (From    : Loop_Index := Loop_Index'First;
       To      : Loop_Index := Loop_Index'Last)
    is
       task type Worker (Start_Index, End_Index : Loop_Index);

       task body Worker is
       begin
          Process (Start_Index, End_Index);
       end Worker;

       Left_End : constant Loop_Index := From + ((To - From + 1) / 2) - 1);

       Left_Worker :  Worker (Start_Index => From,
                              End_Index => Left_End;
       Right_Worker : Worker (Start_Index => Left_End + 1,
                              End_Index => To);
    begin --  Parallel_Loop
       null;
    end Parallel_Loop;

end Parallel;

I could show a similar example for a parallel container iteration,
library call
but thought it best for now to just show a simple array case.

In fact I have a single generic library call that can be used for both
array and container iteration,
and I think the global => all (name1 .. name2) syntax would work for
both cases for different
instantiations of the same generic.

One reason why I think this is important is because for such library
calls, the abstraction is
to only provide parallel chunking over a range of cursor/index.

The client may use this to operate on any number of global references.

For example, calculate the sum of integers from 1 .. N involves 0 arrays.
Increment all the values of an array involves 1 array.
Add Array1 to Array2 involves 2 arrays.
Add Array1, and Array2, to Array 3 arrays.

One library call can be used to handle all these cases. If one were to
pass the globals into the
library call by naming them, then I think you would need an infinite
number of library calls to be written to handle all the possible cases.
Using globals in this manner, one library call can be used to do all
parallel looping problems.

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

Yes, in the example above it seems pretty obvious by inspection in the
package body that there can be no overlap. Hopefully the compiler can be
smart enough to see that also.
We might want to define some sort of aspect or attribute
    (Overlap => False? Covered_Once => True?) that tells the compiler to
add these checks.

In the absence of those checks and with the compiler not being able to
prove that the calls to Process in my example above are non-overlapping,
we might want to allow the programmer to suppress the
global checking on the call from inside the body.

There is still value though to the global all slicing aspect even if the
global checking is suppressed in the body of the library because it can
ensure at least that the clients of the library call are well behaved. If
the library call itself can be  trusted to not call the client with
overlapping ranges, it seems valuable to the client to have the compiler
reject compilations where the client is accessing globals in an unsafe
manner. The global => all(name1 .. name2) on the callback formal subprogram
would provide the check on the clients code.

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

From: Tucker Taft
Sent: Monday, September 25, 2017  4:33 PM

Here is the first piece of my ARG homework.  Mostly I tried to fix up the
syntax according to our discussions in Vienna. [This is version /05
 - Editor.]

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

From: Randy Brukardt
Sent: Monday, October 2, 2017  8:53 PM

> Here is the first piece of my ARG homework.  Mostly I tried to fix up
> the syntax according to our discussions in Vienna.

Thanks for getting this done early. Can I expect the rest of your homework
early, too?? ;-)

A couple of thoughts:

(1) I think you need to soon (if not immediately) address how these are going
to work within generic units and presumably for access-to-subprogram types.
If we plan to use Global aspects for checking in parallel statements *and* we
also want to use the containers there *and* we don't want any significant
incompatibilities in the containers, then we have to have a "reflection"
mechanism for generics.

The mechanism designed for nonblocking provides one model for doing that. This
is likely to be complicated (the Global aspect is not as simple as the boolean
value of Nonblocking), and thus we need to get started on defining it (it isn't
going to work as a last minute thing). Recall we have less than two years to
finish this definition to standardization quality (if we intend to stay on
schedule).

(2) If we intend to use Global aspects for checking in parallel statements, we
need to figure out the details of that checking sooner rather than later. The
checking rules most likely will in part inform how the Global rules need to
work.

(3) I didn't see a solution for global data defined in hidden packages, such
as the System implementation helpers that both Janus/Ada and GNAT have. We
can't start requiring implementors to restructure their entire runtime in
order to meet Global settings.

(4) I didn't see any discussion of the defaults for Global the runtime
packages. I realize the detailed update is going to be a large job in itself,
but I'd like to hear at least about what the defaults will be.

(5) I think I object to the idea of "synthesized" global aspects. (I'm sorry I
didn't think of this during the meeting.)

The basic idea is that global aspects, like many other aspects including Pre,
Post, and Nonblocking, represent contracts between the caller and the callee.
These are enforced on the calls without any knowledge of the implementation,
and similarly are enforced on the body without any knowledge of the calls.

"Synthesized", however, means that the contract depends on the contents of the
body, requiring that a body need be present before any calls can be compiled
and meaning that future maintenance on a body can break calls (a complete
violation of the separation of calls and implementation).

Note that existing cases of body dependencies (generic instances, aspect
Inline) in Ada have two important properties: (1) they're optional, no Ada
compiler needs to implement them (Janus/Ada does not; the primary reason we
implemented generic code sharing was to avoid generic body dependencies); (2)
the code will not change legality regardless of changes in the body.
"Synthesized" will fail (2) and thus be a horrific maintenance hazard
(especially given the cascade effects of contracts).

My long time objection to systems like SPARK is their need to have the
complete program available before they can prove anything. I don't want
to see Ada going down that road.

Synthesizing contracts (Global among them) seems like a ripe area for tools,
and there seems to be no need to include it in the language proper. Moreover,
an implementation could define "Synthesized" if it wanted to
(implementation-defined modifiers are allowed), and that seems preferable to
defining in the language something contract-related that destroys the contract
model!

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

From: Yannick Moy
Sent: Monday, October 2, 2017  11:42 PM

...
>(1) I think you need to soon (if not immediately) address how these are
>going to work within generic units and presumably for access-to-subprogram
>types.

Not sure why you're saying that. Pre/Post also don't work with
access-to-subprogram currently.

...
>(3) I didn't see a solution for global data defined in hidden packages, such
>as the System implementation helpers that both Janus/Ada and GNAT have. We
>can't start requiring implementors to restructure their entire runtime in
>order to meet Global settings.

I think that's the part where package P is meant to represent all data hidden
in P and its private children. Or you have something else in mind?

...
>(5) I think I object to the idea of "synthesized" global aspects. (I'm sorry
>I didn't think of this during the meeting.)

I also do not like it. To me, it looks useless: absence of the aspect already
indicates we know nothing of its reads/writes of global variables.

>My long time objection to systems like SPARK is their need to have the
>complete program available before they can prove anything. I don't want to
>see Ada going down that road.

This is completely wrong. :-)
SPARK is fully modular, except for two things: checking of concurrency, which
is rather a minor point, and generation of Global contracts but *only* when
they are not provided by the user. And even in that second case, you only need
to look at the sub-call graph from a subprogram to generate its Global.

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

From: Randy Brukardt
Sent: Tuesday, October 3, 2017  12:25 AM

>>(1) I think you need to soon (if not immediately) address how these
>>are going to work within generic units and presumably for
>>access-to-subprogram types.

>Not sure why you're saying that. Pre/Post also don't work with
>access-to-subprogram currently.

The generic cases (which is mainly what I'm concerned about) are necessary to
deal with if Global is to work with the containers. And if it doesn't work
with the containers, a significant number of programs couldn't use Global
(including most of the intended uses of Global in parallel blocks and loops).

Pre/Post are dynamic constructs in Ada (as opposed to SPARK), so it doesn't
matter much how they work with access-to-subprogram. Indeed, there is an open
AI to improve that (it's unlikely to stay precisely as it is).

Global, however, is statically enforced in Ada, so it has to be handled
"right" for access-to-subprogram, generics, and any other such cases.
There's no leeeway (something I learned in detail defining Nonblocking).

>>(3) I didn't see a solution for global data defined in hidden
>>packages, such as the System implementation helpers that both Janus/Ada
>>and GNAT have. We can't start requiring implementors to restructure their
>>entire runtime in order to meet Global settings.

>I think that's the part where package P is meant to represent all data
>hidden in P and its private children. Or you have something else in mind?

I'm thinking of unrelated packages that are used to implement some library
package. For instance, Janus/Ada bases all of its I/O packages on a package
called System.Basic_IO. That has some global state. I believe GNAT does
something similar with it's I/O packages; they seem to depend on children of
System and GNAT. It would be amazing if no such package ever needed global
state. (Certainly that will rarely happen if storage pools are considered
state, as they ought to be.)

[Poster's note: I should have mentioned that you don't want to have to name
these unrelated packages in the Global of the package specification; the
user should need to know nothing about them. Especially important for
language-defied packages.]

Forcing implementers to either remove the state or restructure their runtime
to put everything in private packages (which might be very difficult given
visibility issues and the like) seems like the wrong way to go.

It seems like there needs to be some way to refer to state of any/all packages
that might be used to implement a package but aren't visible in that package's
specification.

>> (5) I think I object to the idea of "synthesized" global aspects.
>> (I'm sorry I didn't think of this during the meeting.)

> I also do not like it. To me, it looks useless: absence of the aspect already
> indicates we know nothing of its reads/writes of global variables.

Glad to hear I'm not completely crazy.

>> My long time objection to systems like SPARK is their need to have
>> the complete program available before they can prove anything. I
>> don't want to see Ada going down that road.

> This is completely wrong. :-)
> SPARK is fully modular, except for two things: checking of
> concurrency, which is rather a minor point, and generation of Global
> contracts but *only* when they are not provided by the user. And even in
> that second case, you only need to look at the sub-call graph from a
> subprogram to generate its Global.

I don't want any "except for" in Ada. Period. Good to hear that SPARK has
moved away from complete source code, though.

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

From: Randy Brukardt
Sent: Tuesday, October 3, 2017  1:40 AM

>The generic cases (which is mainly what I'm concerned about) are necessary
>to deal with if Global is to work with the containers. And if it doesn't
>work with the containers, a significant number of programs couldn't use
>Global (including most of the intended uses of Global in parallel blocks and
>loops).

Why would you want to use Global on generic containers? Morally, container's
API reads/writes no globals (except for those like Query_Element and
Update_Element that take a callback in argument, which may have such an
effect). The bounded containers indeed have "Global => null" contracts, while
the regular ones actually allocate memory, so with Tuck's proposal you would
have to mention the corresponding access type. But there is no strong
guarantee here, as the formal parameters of the instance could write or read
a global variable.

A more complex scheme would have a way to describe the formal parameters or
callbacks globals, something like Subp'Global, but that would quickly turn
into a nightmare I'm afraid.

>Global, however, is statically enforced in Ada, so it has to be handled
>"right" for access-to-subprogram, generics, and any other such cases.
>There's no leeeway (something I learned in detail defining Nonblocking).

I don't see why we could not have a situation where the compiler enforces part
of the property, leaving holes to be filled by other tools? That's similar to
the distinction between static checking and dynamic checking. Except here of
course you cannot describe the static analysis performed in these other tools
that complete the compiler.

>I'm thinking of unrelated packages that are used to implement some library
>package. For instance, Janus/Ada bases all of its I/O packages on a package
>called System.Basic_IO. That has some global state. I believe GNAT does
>something similar with it's I/O packages; they seem to depend on children of
>System and GNAT. It would be amazing if no such package ever needed global
>state. (Certainly that will rarely happen if storage pools are considered
>state, as they ought to be.)
>
>Forcing implementers to either remove the state or restructure their runtime
>to put everything in private packages (which might be very difficult given
>visibility issues and the like) seems like the wrong way to go.
>
>It seems like there needs to be some way to refer to state of any/all
>packages that might be used to implement a package but aren't visible in
>that package's specification.

I believe that's what Tuck proposes when he refers to the name of the package.
So in your case, System.Basic_IO would refer to all hidden state in that unit.

>I don't want any "except for" in Ada. Period. Good to hear that SPARK has
>moved away from complete source code, though.

It was never the case, even for the first version of SPARK 83. :-)

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

From: Randy Brukardt
Sent: Tuesday, October 3, 2017  2:28 AM

...
>Why would you want to use Global on generic containers?

Because it's wildly incompatible if you don't. Since Global isn't currently
specified on existing subprograms, all existing instances would fail until
lobal is added. (Formals would have to have to have no global, that is
global => in out null, and that would have to be checked during
instantiation.)

> Morally, container's API reads/writes no globals (except for those
> like Query_Element and Update_Element that take a callback in
> argument, which may have such an effect). The bounded containers
> indeed have "Global => null"
> contracts, while the regular ones actually allocate memory, so with
> Tuck's proposal you would have to mention the corresponding access type.

Yes, that's part of it. Also, the container package itself may have some state
(free chains and a serial number exist in the proposed Janus/Ada
implementations). Perhaps we could ban that from the bounded containers (since
node sharing isn't an option for those), but it is a dead-body issue for me on
the other containers.

> But there is no strong guarantee here, as the formal parameters of the
> instance could write or read a global variable.

There has to be. For the intended use in Ada 2020, preventing race conditions
and other tasking screwups, detecting only some easy cases and letting the
hard ones get through is not an option. This is also a dead-body issue for me;
I'm not remotely interested in parallel statements unless they are safe by
construction (it is easy to write unsafe Ada tasking code, using something
like Brad's Parafin libraries; the language needs no enhancements to do that).
And without parallel statements, we don't need Global at all (there's no other
proposed use for it at this point), and in fact we probably don't need Ada
2020 at all (there's just not enough else of value, and restarting from
nothing is not going to get us anywhere useful by mid-2019).

> A more complex scheme would have a way to describe the formal
> parameters or callbacks globals, something like Subp'Global, but that
> would quickly turn into a nightmare I'm afraid.

That's the only option that is compatible and safe, and thus I want to get
started on it ASAP. If we're not willing to do that, I would like to know
right away so that we can either abandon or redirect our other work into
productive areas (which Global would not be).

Note that it isn't impossible; I worked out all of the details for Nonblocking
(admittedly easier in some ways as a Boolean aspect) and following that pattern
should work fine here (just more complex for the checking). (If we replaced
Global by a boolean aspect -- say "Task_Safe" -- it would be trivial to do;
just do the same as Nonblocking -- but of course that is rather limiting as
parallel statements wouldn't allow any unprotected globals, even if they don't
conflict.)

>> Global, however, is statically enforced in Ada, so it has to be
>> handled "right" for access-to-subprogram, generics, and any other such cases.
>> There's no leeeway (something I learned in detail defining Nonblocking).

> I don't see why we could not have a situation where the compiler
> enforces part of the property, leaving holes to be filled by other
> tools? That's similar to the distinction between static checking and
> dynamic checking. Except here of course you cannot describe the static
> analysis performed in these other tools that complete the compiler.

As noted above, for the intended use in preventing race conditions and other
tasking errors, this is completely unacceptable. If there is a possible race
condition, it *must* be detected either at compile-time or run-time. There's
no grey area there. So putting off part of it to other tools is simply
unacceptable. Some other tool might be able to prove that something Ada doesn't
allow actually is OK, and that could be useful if the "Soft Error"
scheme is adopted, but that's about it.

>>I'm thinking of unrelated packages that are used to implement some
>>library package. For instance, Janus/Ada bases all of its I/O packages
>>on a package called System.Basic_IO. That has some global state. I believe
>>GNAT does something similar with it's I/O packages; they seem to depend on
>>children of System and GNAT. It would be amazing if no such package ever
>>needed global state. (Certainly that will rarely happen if storage pools are
>>considered state, as they ought to be.)
>>
>>Forcing implementers to either remove the state or restructure their
>>runtime to put everything in private packages (which might be very difficult
>>given visibility issues and the like) seems like the wrong way to go.
>>
>>It seems like there needs to be some way to refer to state of any/all
>>packages that might be used to implement a package but aren't visible
>>in that package's specification.

>I believe that's what Tuck proposes when he refers to the name of the
>package. So in your case, System.Basic_IO would refer to all hidden state in
>that unit.

Sure, but no one is going to put System.Basic_IO into the specification of
Ada.Text_IO. It is only referenced from the body. Moreover, the specification
of Ada.Text_IO in the RM has to somehow reference the possibility of state in
these packages (different for every vendor) in the Global aspects that apply
to the Ada.Text_IO package. We're surely not putting Global => System.Basic_IO
into the RM!!

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

From: Yannick Moy
Sent: Tuesday, October 3, 2017  2:53 AM

>Because it's wildly incompatible if you don't. Since Global isn't currently
>specified on existing subprograms, all existing instances would fail until
>Global is added. (Formals would have to have to have no global, that is
>global => in out null, and that would have to be checked during
>instantiation.)

It seems to me that this extremist approach is bound to fail. I see no point
in forcing Global on everything.

>There has to be. For the intended use in Ada 2020, preventing race
>conditions and other tasking screwups, detecting only some easy cases and
>letting the hard ones get through is not an option. This is also a dead-body
>issue for me; I'm not remotely interested in parallel statements unless they
>are safe by construction (it is easy to write unsafe Ada tasking code, using
>something like Brad's Parafin libraries; the language needs no enhancements
>to do that). And without parallel statements, we don't need Global at all
>(there's no other proposed use for it at this point), and in fact we
>probably don't need Ada 2020 at all (there's just not enough else of value,
>and restarting from nothing is not going to get us anywhere useful by
>mid-2019).

I don't see why the compiler would have to check all the boxes here. This will
require analysis techniques beyond what the compiler can do. But I think that
the compiler could do something very valuable, which is to check indeed that
loops can be parallelized based on the Global contracts on the subprograms it
calls. That would leave the verification of Global contracts themselves to
other tools.

>>A more complex scheme would have a way to describe the formal parameters
>>or callbacks globals, something like Subp'Global, but that would quickly
>>turn into a nightmare I'm afraid.

>That's the only option that is compatible and safe, and thus I want to get
>started on it ASAP. If we're not willing to do that, I would like to know
>right away so that we can either abandon or redirect our other work into
>productive areas (which Global would not be).

Based on our experience with users using Global contracts, I'd say it's
unlikely you manage to make something that complex as Subp'Global inside
other contracts be useful to anyone.

>>I don't see why we could not have a situation where the compiler enforces
>>part of the property, leaving holes to be filled by other tools? That's
>>similar to the distinction between static checking and dynamic checking.
>>Except here of course you cannot describe the static analysis performed
>>in these other tools that complete the compiler.
>
>As noted above, for the intended use in preventing race conditions and other
>tasking errors, this is completely unacceptable. If there is a possible race
>condition, it *must* be detected either at compile-time or run-time. There's
>no grey area there. So putting off part of it to other tools is simply
>unacceptable. Some other tool might be able to prove that something Ada
>doesn't allow actually is OK, and that could be useful if the "Soft Error"
>scheme is adopted, but that's about it.

OK if you can pull it, but I doubt it's possible with "just" compilation
techniques, while managing an acceptable complexity in annotations.

Or just settle for something very simple, such as Global=>null that
indicates that no global is read/written, which could be inferred by the
compiler for a subprogram based on the contracts of subprograms it calls (no
need for a global analysis), so would be inferred in particular for generic
instances.

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

From: Randy Brukardt
Sent: Tuesday, October 3, 2017  2:59 PM

>It seems to me that this extremist approach is bound to fail. I see no
>point in forcing Global on everything.

If we don't, then we cannot solve any of the problems that we are trying to
solve. If you are right, then we should abandon work on Global immediately and
switch to something simpler that will work (perhaps a pair of aspects
"Task_Safe" and "Extra_Pure").

>I don't see why the compiler would have to check all the boxes here.
>This will require analysis techniques beyond what the compiler can do.

No. There is no requirement that all things that might be parallelizable be
legal Ada (you can always use an unsafe technique to get that). We just want
to allow what is obviously safe.

>But I think that the compiler could do something very valuable, which is to
>check indeed that loops can be parallelized based on the Global contracts on
>the subprograms it calls. That would leave the verification of Global
>contracts themselves to other tools.

The vast majority of Ada users have no other tools. The language is wildly
incomplete if it cannot be used without depending on "other tools".
Moreover, if some "other tool" can exist that verifies some important
property, then that tool can be part of the Ada compiler. Dependence on
"other tools" for critical functionality is evil.

In any case, Global has to be defined in terms of what it allows. If it is
not, then it has no semantic meaning within the Ada Standard, and that would
make it nonsense to define. (Plus, that is NOT what Tucker is currently
proposing.)

...
>Based on our experience with users using Global contracts, I'd say it's
>unlikely you manage to make something that complex as Subp'Global
>inside other contracts be useful to anyone.

It certainly works for Nonblocking (at least in the context of the containers,
which is the critical case); I fail to see (today!) why it would be different
for Global.

For the intended tasking purpose, the only truly interesting Global contracts
are "in out null" and "synchronized" (everything else would conflict by
definition in a parallel loop). They could be defined by aspects that work
like Nonblocking, and that clearly will work in the context of the containers.
If Global can't be made to work here, then we ought to abandon Global in favor
of something that will work.

...
>OK if you can pull it, but I doubt it's possible with "just"
>compilation techniques, while managing an acceptable complexity in
>annotations.

We don't need perfection, we only need a guarantee that the contract reflects
reality. I fail to see why you think that requires advanced analysis (the
Global contract of a subprogram is the union of all of the contracts of the
subprograms that it calls, plus all of globals that it directly reads or
writes -- hard to see where complex analysis would be needed).

>Or just settle for something very simple, such as Global=>null that indicates
>that no global is read/written, which could be inferred by the compiler for
>a subprogram based on the contracts of subprograms it calls (no need for a
>global analysis), so would be inferred in particular for generic instances.

That's the model of Global in Ada (as opposed to SPARK). All of the contracts
Tucker has are designed to be simply checked by a compiler. And inferring the
contracts for generic instantiations is how Nonblocking works (and I would
like Global to work as well). But we have to have an assume-the-worst model
in the generic body, and some form of reflection. Without that, you have to
have body dependences, which (A) violate the Ada generic contract model,
something we've never done to date; and (B) are a dead body issue for me (as
previously noted) - Janus/Ada has no body dependence mechanism and is never
going to have one.

If there is a problem with the Subp'Global model, it is likely to be with the
needed assume-the-worst rule. In that case, my preference is to abandon Global
(leaving it to SPARK) and instead define two Boolean contracts (which I know
can be defined properly).

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

From: Tucker Taft
Sent: Tuesday, October 3, 2017  3:36 PM

>> Based on our experience with users using Global contracts, I'd say
>> it's unlikely you manage to make something that complex as
>> Subp'Global inside other contracts be useful to anyone.
>
> It certainly works for Nonblocking (at least in the context of the
> containers, which is the critical case); I fail to see (today!) why it
> would be different for Global. ...

We have already proposed using the 'Global attribute for generics in the AI.
The few examples we have looked at seem to make sense.

In our most recent discussion in the SPARK language-design group, we suggested
we drop the explicit "Synthesized" value for the global aspect, and just give
permission for an implementation to synthesize a more precise Global aspect
when it would otherwise default to "in out all."   Clearly if the compiler
cannot synthesize a sufficiently precise Global aspect, there will be safe
programs that are identified as unsafe, so such a program will not be as
portable.  To make such a program portable, the tool that synthesizes the more
precise Global aspect would have to generate the explicit annotations and add
them to the source code, which seems doable.  But for a user who is happy to
have non-portable code, they can leave off the explicit annotations and still
have a modicum of safety.  If the code is given to a compiler that doesn't
have the full machinery, it will be rejected rather than being silently unsafe.

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

From: Randy Brukardt
Sent: Tuesday, October 3, 2017  6:46 PM

...
> We have already proposed using the 'Global attribute for generics in
> the AI.  The few examples we have looked at seem to make sense.

Sorry, missed that. However, I didn't see the needed generic matching rules,
nor the assume-the-best/assume-the-worst rules needed when using this inside
a generic. So I'm not sure how it works in those cases. (Some examples similar
to the ones for Nonblocking probably ought to be constructed to show the
issues that need to be addressed.)

> In our most recent discussion in the SPARK language-design group, we
> suggested we drop the explicit "Synthesized" value for the global
> aspect, and just give permission for an implementation to synthesize a
> more precise Global aspect
> when it would otherwise default to "in out all."   Clearly if
> the compiler cannot synthesize a sufficiently precise Global aspect,
> there will be safe programs that are identified as unsafe, so such a
> program will not be as portable.  To make such a program portable, the
> tool that synthesizes the more precise Global aspect would have to
> generate the explicit annotations and add them to the source code,
> which seems doable.  But for a user who is happy to have non-portable
> code, they can leave off the explicit annotations and still have a
> modicum of safety.  If the code is given to a compiler that doesn't
> have the full machinery, it will be rejected rather than being
> silently unsafe.

I think I like this better than what the AI proposes.

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

From: Tucker Taft
Sent: Tuesday, October 3, 2017  9:38 PM

>> We have already proposed using the 'Global attribute for generics in
>> the AI.  The few examples we have looked at seem to make sense.
>
> Sorry, missed that. However, I didn't see the needed generic matching
> rules, nor the assume-the-best/assume-the-worst rules needed when
> using this inside a generic. So I'm not sure how it works in those
> cases. (Some examples similar to the ones for Nonblocking probably
> ought to be constructed to show the issues that need to be addressed.)

Good point.  We need to specify requirements on actuals when a formal has
a Global specified.  The requirements are pretty simple, as they will be
based on some kind of set inclusion, but of course they need to be spelled
out.

...
> I think I like this better than what the AI proposes.

OK, let's assume we go that direction then.

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

From: Jeff Cousins
Sent: Wednesday, October 4, 2017  3:52 AM

I’m afraid that I haven’t seen Tucker’s original message, please could you
re-send it? [Editor's note: Tucker did so; not shown here.]

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

From: Randy Brukardt
Sent: Thursday, October 5, 2017  12:25 AM

...
> Good point.  We need to specify requirements on actuals when a formal
> has a Global specified.  The requirements are pretty simple, as they
> will be based on some kind of set inclusion, but of course they need
> to be spelled out.

You also need assume-the-best/assume-the-worst rules for the meaning of the
attributes in a generic unit.

Probably these can be quite simple, too: "Subp'Global" acts like "in out all"
in a generic specification, with a recheck on instantiation; "Subp'Global"
acts like "in out null" in a generic body, and specifically a call to Subp is
allowed (while it does not allow other calls) in the scope of a contract
including "Subp'Global".

...

BTW, I forgot to ask if implicit composite "=" is being handled somehow.
Since the default for Global is "all", the default for "=" would have to be
"all" as well. Which is silly, since most "=" are pure (don't use any
globals). That was the biggest mess for Nonblocking, as we ended up defining
Nonblocking for types in order to change the default. (Which required generic
unit changes as well.)

Essentially, everything that was hard for Nonblocking is likely to have a
similar problem for Global. Best that we check that we don't miss anything.

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

From: Tucker Taft
Sent: Thursday, January 25, 2018  4:04 AM

...
> I rather disagree; phone meetings are best for wordsmithing since it
> isn't necessary to diagram on a whiteboard like it is for syntax
> arguments. For Ada 2012, we used phone meetings to finalize almost all
> of the wording, so it's amazing to me to think that it suddenly has
> gotten difficult to do what we've done many times before.

OK, I had a different goal for these phone calls.  We have asked the community
to get all of their proposals in by Jan 15, so I presumed one of the points of
these phone calls was to deal with the final influx of proposals.

> In any case, AI12-0079-1 is nowhere near complete enough for me to be
> able to annotate the containers with them, a job I need to start ASAP.
> For instance, we have no solution in the AI yet to the problem of
> implementation-defined helper packages. We haven't discussed how to
> handle atomic writes in "synchronized" mode (these are easily race
> conditions which shouldn't be allowed in general, lest our goal of
> preventing unsynchronized access be completely undermined). There's
> probably other issues that aren't mentioned in the AI.

I am willing to spend more time on 0079.  I did not realize that the above was
your concern.  Perhaps we can handle this offline.  If you can let me know what
you feel you need to annotate the containers, I'll try to finalize that part of
the wording.  For me it just seemed like there was a general fine tuning needed,
but apparently you feel there are still some big issues, at least when it comes
to annotating the libraries.  So if you can give me a clearer idea of what you
need, I'll focus on that.

> Moreover, you haven't really done much of an update for the last
> couple of meetings. It seems like it isn't progressing, and it is the
> most core thing we are working on.
>
> I was expecting that we would spend a bit of time on the 4 BIs (none
> of which should require much discussion, but maybe some wordsmithing),
> a bit of time on some of the new proposals (to determine whether or
> not we want to pursue them, and find a victim, er, ARG author for the
> AI), and the bulk of the time on AI12-0079-1 and AI12-0119-1 in the
> hopes of getting some of our core work done. [Remember that
> AI12-0119-1 depends on AI12-0079-1.] (We can't finish all of the AIs
> for Ada 2020 in the last week, as I simply couldn't get the all into
> Standard in the two weeks or so of editorial time the schedule
> allows.) And then we would look at anything else as time permits.

Unfortunately, it looks like perhaps we each had our own priorities for the
phone calls.  I appreciate what you are saying, but alas, it wasn't what I
prioritized for this first call.  Perhaps you and I can handle the 0079 issue
ourselves without taking up time for the whole ARG.

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

From: Randy Brukardt
Sent: Thursday, January 25, 2018  6:00 PM

...
> > I rather disagree; phone meetings are best for wordsmithing since it
> > isn't necessary to diagram on a whiteboard like it is for syntax
> > arguments. For Ada 2012, we used phone meetings to finalize almost
> > all of the wording, so it's amazing to me to think that it suddenly
> > has gotten difficult to do what we've done many times before.
>
> OK, I had a different goal for these phone calls.  We have asked the
> community to get all of their proposals in by Jan 15, so I presumed
> one of the points of these phone calls was to deal with the final
> influx of proposals.

True, but at this stage, that mainly is discussing broad outlines of what to do,
whether to do anything at all, and then finding a victim, er author to produce a
real proposal.

After that, I expect we'll work in priority order, which always puts 79 and
119 first. And I've learned over the years that if you don't try to get the
critical work done before doing things that are more fun, the critical work
never does get done.

> > In any case, AI12-0079-1 is nowhere near complete enough for me to
> > be able to annotate the containers with them, a job I need to start ASAP.
> > For instance, we have no solution in the AI yet to the problem of
> > implementation-defined helper packages. We haven't discussed how to
> > handle atomic writes in "synchronized" mode (these are easily race
> > conditions which shouldn't be allowed in general, lest our goal of
> > preventing unsynchronized access be completely undermined). There's
> > probably other issues that aren't mentioned in the AI.
>
> I am willing to spend more time on 0079.  I did not realize that the
> above was your concern.  Perhaps we can handle this offline.  If you
> can let me know what you feel you need to annotate the containers,
> I'll try to finalize that part of the wording.

I'm not completely sure at this stage, as I've never felt the proposal was
solid enough to proceed. Obviously, the containers are generic, so all of the
rules involving combinations and reflecting the Globals of the actuals in
generic specs need to be figured out in detail.

This is rather complex for Nonblocking (which is worked out), and Global is 10
times harder, so the lack of work in that area is concerning.

> For me it just seemed like there was a general fine tuning needed, but
> apparently you feel there are still some big issues, at least when it
> comes to annotating the libraries.  So if you can give me a clearer
> idea of what you need, I'll focus on that.

The other issue for the libraries is clearly what to do about
implementation-defined "helper" packages. We surely have to allow
implementations to have such packages, and they might in some circumstances have
globals in them. It would seem nasty to ban that (other than in Pure packages,
of course). And we surely can't name any such packages in the Standard!

There's also an issue that is not specific to Global, but matters a lot.
Since attribute prefixes have to be unambiguous without context, most of the
names of generic formals can't be directly used in an attribute. That means that
they have to be renamed to a unique name so that they can be used. For instance,
for Vectors:

generic
   type Index_Type is range <>;
   type Element_Type is private;
   with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Vectors
   with Preelaborate, Remote_Types,
        Nonblocking => Equal_Element'Nonblocking,
        Global => Equal_Element'Global and <impl-def stuff??> and <the body of this package> is

   function Equal_Element (Left, Right : Element_Type) return Boolean renames "=";

   ...

The aspects Nonblocking and Global give the default declaration of the aspects
for the contents, and we surely don't want to repeat them on all (approx) 70
subprograms.

However, we've never defined what the freezing point of a package declaration
is, so the place where these aspects are evaluated is not well-defined. So I
don't even know if this formulation is legal. And if it isn't legal, is there
any alternative that IS legal that doesn't require repeating Nonblocking and
Global aspects 70 times.

The third issue is about the actual definition of "synchronized". The purpose of
this setting is to mark task-safe code that still uses global variables. It's
pretty clear that 100% elimination of data races is impossible if any globals
are involved (as soon as there is more than one global, data locks are
impossible to avoid with static rules).

But there definitely is low-hanging fruit that certainly should be detected.
For instance, if A is a global atomic object, then
   A := A + 1;
is a guarenteed data race (assuming any parallel execution). One should be using
one of the routines in the atomic update generic that Bob doesn't think is
important. ;-)

I can think of a number of relatively simple additional rules that would at
least eliminate the worst of these data race conditions (essentially by making
them illegal in "synchronized" code). But I don't know how far we should go.

My fear in this case is that a user will slap "parallel" on an existing loop to
see what happens. And they then get an error about not having Global and
Nonblocking contracts. So they add those, and then get an error about having a
unsynchronized global object (probably with a suggestion to make them protected
or atomic). So they slap "atomic" on the object, the code compiles, and the loop
malfunctions badly because the object is updated without using an atomic update
operation.

I know at least one substantial Ada user who would function this way (I see him
in the mirror every morning ;-), and not detecting bad atomic updates would
greatly reduce the value of all of the other things we've done. (There's a
similar issue for protected objects if someone just provides separate read and
write operations rather than the update operations.)

So I'd like to explore this issue a bit to see what we can do to mitigate it.

[I can write a much longer discussion of this issue, but I have to get AIs
created and mail filed for the meeting, lest we not have a lot of topics that
we're supposed to be able to talk about in place.]

...
> Unfortunately, it looks like perhaps we each had our own priorities
> for the phone calls.  I appreciate what you are saying, but alas, it
> wasn't what I prioritized for this first call.  Perhaps you and I can
> handle the 0079 issue ourselves without taking up time for the whole
> ARG.

I'm just following the plan laid out by Jeff that he's followed at every
previous meeting. I'm pretty sure that hasn't changed for this one. :-)

We do have plans for more calls this winter, so this is hardly the only such
opportunity. If we don't discuss it Monday, I'm sure we'll have a chance in late
February. Experience shows that by the third call, Tucker is hardly touching his
homework :-), so I'm trying to get you to do as much of it now as possible. (And
you've certainly done some of it -- but we put priority indications on AIs for a
reason ... High > Low :-)

Anyway, I've laid out the issues I can think of off-hand above. I also noted
above that I need to do other work today, so looking in detail at the proposals
and AI12-0112-1 had better wait lest the Jan 15th rush not get processed.

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

From: Tucker Taft
Sent: Sunday, February 18, 2018  5:29 PM

...
>>I am willing to spend more time on 0079.  I did not realize 
>>that the above was your concern.  Perhaps we can handle this 
>>offline.  If you can let me know what you feel you need to 
>>annotate the containers, I'll try to finalize that part of 
>>the wording.
>
>I'm not completely sure at this stage, as I've never felt the proposal was
>solid enough to proceed. Obviously, the containers are generic, so all of
>the rules involving combinations and reflecting the Globals of the actuals
>in generic specs need to be figured out in detail.
>
>This is rather complex for Nonblocking (which is worked out), and Global is
>10 times harder, so the lack of work in that area is concerning.

I am not sure what you mean here.  We have the 'Global attribute and permit 
the use of "&" to combine global specifications.  What more do you think we 
need?

>>For me it just seemed like there was a general 
>>fine tuning needed, but apparently you feel there are still 
>>some big issues, at least when it comes to annotating the 
>>libraries.  So if you can give me a clearer idea of what you 
>>need, I'll focus on that.

>The other issue for the libraries is clearly what to do about
>implementation-defined "helper" packages. We surely have to allow
>implementations to have such packages, and they might in some circumstances
>have globals in them. It would seem nasty to ban that (other than in Pure
>packages, of course). And we surely can't name any such packages in the
>Standard!

Private descendants are considered part of the package body from the point 
of "Global => (in out => P private)".  Do we need more than that as a way to
support "helper" packages?

>There's also an issue that is not specific to Global, but matters a lot.
>Since attribute prefixes have to be unambiguous without context, most of the
>names of generic formals can't be directly used in an attribute. That means
>that they have to be renamed to a unique name so that they can be used. For
>instance, for Vectors:
>
>generic
>  type Index_Type is range <>;
>  type Element_Type is private;
>  with function "=" (Left, Right : Element_Type) return Boolean is <>;
>package Ada.Containers.Vectors 
>  with Preelaborate, Remote_Types,
>       Nonblocking => Equal_Element'Nonblocking,
>       Global => Equal_Element'Global and <impl-def stuff??> and <the body of this package> is
>
>  function Equal_Element (Left, Right : Element_Type) return Boolean renames "=";
>
>  ...
>
>The aspects Nonblocking and Global give the default declaration of the
>aspects for the contents, and we surely don't want to repeat them on all
>(approx) 70 subprograms.
>
>However, we've never defined what the freezing point of a package
>declaration is, so the place where these aspects are evaluated is not
>well-defined. So I don't even know if this formulation is legal. And if it
>isn't legal, is there any alternative that IS legal that doesn't require
>repeating Nonblocking and Global aspects 70 times.

Fine, but that seems to be a separate AI.  I think it is safe to assume that
this can be fixed to work the way we want it to for Global and Nonblocking, 
so this shouldn't interfere with you making progress.

>The third issue is about the actual definition of "synchronized". The
>purpose of this setting is to mark task-safe code that still uses global
>variables. It's pretty clear that 100% elimination of data races is
>impossible if any globals are involved (as soon as there is more than one
>global, data locks are impossible to avoid with static rules). ...

There are "data races" and "race conditions."  Frequently these are treated as 
synonyms, but if there is a distinction, it is that "A := A + 1" does not
involve a "data race" if A is atomic, but it is clearly a race condition.  I
don't think we have a prayer of preventing these kinds of race conditions.
Certainly a friendly compiler could recognize some of these simple patterns,
and provide a warning, but I don't see that we can hope for much more than
that.  Again, I think this is a separate AI, or simply out of scope for Ada
standardization.

So I don't find any of the above issues particularly relevant to AI12-0079 and 
its use in annotating language-defined packages.  *However*, I do think we have
a significant issue with respect to access types.  We really want a way to say 
that the side-effects are limited to heap objects "reachable" from a given
parameter.  Saying that a subprogram updates something designated by a given 
access type is pretty useless.

So I plan to spend some time thinking about this problem of access types,
especially in the context of container-like packages that clearly use access
types behind the scenes.  But I don't see that there is much more needed to 
address the issues you identify above.  If you don't agree, please advise!

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

From: Randy Brukardt
Sent: Monday, February 19, 2018  9:45 PM

> I am not sure what you mean here.  We have the 'Global attribute and permit
> the use of "&" to combine global specifications.  What more do you think we
> need?

The assume-the-best and assume-the-worst rules for using the 'Nonblocking
attribute inside a generic turned out to be pretty complex in order to be
usable. And those are just "on-off" type rules!

I'd like to have at least some feeling that we can make the rules for 'Global
attribute inside of a generic usable before using them everywhere and assuming
that implementers can figure it out.

I suppose this is more of a concern for the actual proposal rather that need
in the spec of the containers. But if no one can write a legal body for the 
containers, that would be bad...

...
>> The other issue for the libraries is clearly what to do about
>> implementation-defined "helper" packages. We surely have to allow
>> implementations to have such packages, and they might in some circumstances
>> have globals in them. It would seem nasty to ban that (other than in Pure
>> packages, of course). And we surely can't name any such packages in the
>> Standard!
		
> Private descendants are considered part of the package body from the point
> of "Global => (in out => P private)".  Do we need more than that as a way
> to support "helper" packages?

Traditionally, helper packages are in some implementation-defined subsystem.
The obvious example is IO. In Janus/Ada, we have the helper package defined 
as System.Basic_IO. All of the language-defined packages are defined in terms
of it. (It has a bit of state to support Standard-in/Standard-out.) I believe
GNAT has some such package in the GNAT subsystem.

For containers, I suppose a global non-generic helper could be a private child
of Ada.Containers. (There sadly isn't an Ada.IO subsystem.) But that
*still* isn't a "private descendant" of the generic Ada.Containers.Vectors!
And there is no way to have a non-generic private descendant of a generic
package. [If I was going to use a helper at all, it would definitely be 
non-generic.]

I vaguely remember that one option discussed was just to punt and let
implementers put anything that they wanted as additional dependencies into
Global for impure packages. That would seem to work, especially if we allowed
mentioning packages only referenced from a private with in Global aspects.
(Putting "private" into the context clause would make it clear that the only
reason for mentioning these packages is so that the dependencies can be
visible for checks. I believe that we already allow adding "private withs"
as those are semantically transparent for the purposes of the language-defined
specification.)

...	
>> However, we've never defined what the freezing point of a package
>> declaration is, so the place where these aspects are evaluated is not
>> well-defined. So I don't even know if this formulation is legal. And if it
>> isn't legal, is there any alternative that IS legal that doesn't require
>> repeating Nonblocking and Global aspects 70 times.
>		
> Fine, but that seems to be a separate AI.  I think it is safe to assume
> that this can be fixed to work the way we want it to for Global and
> Nonblocking, so this shouldn't interfere with you making progress.

The reassurance that it can be made to work is important, at least for my
psyche. I don't want to do this overall and then have to start over because
of a bad assumption at the start...

>> The third issue is about the actual definition of "synchronized". The
>> purpose of this setting is to mark task-safe code that still uses global
>> variables. It's pretty clear that 100% elimination of data races is
>> impossible if any globals are involved (as soon as there is more than one
>> global, data locks are impossible to avoid with static rules). ...
		
> There are "data races" and "race conditions."  Frequently these are treated
> as synonyms, but if there is a distinction, it is that "A := A + 1" does not
> involve a "data race" if A is atomic, but it is clearly a race condition.

This seems like hair-splitting. Either way it doesn't work, but only
intermittently.

> I don't think we have a prayer of preventing these kinds of race conditions.
> Certainly a friendly compiler could recognize some of these simple patterns,
> and provide a warning, but I don't see that we can hope for much more than
> that.  Again, I think this is a separate AI, or simply out of scope for Ada
> standardization.

I don't see any good reason to allow writes to atomic objects to be considered
safe unless they are writing a static value, or are using one of a atomic
update operations that Bob doesn't think we need to define. ;-) Anything else
is a guaranteed race condition, so why allow it in the first place? Most of
these sorts of operations should be wrapped into protected objects in order to
be clearly safe. (And even those can be abused, and probably there ought to be
a check for dubious cases as when the same protected object occurs more than
once in a single expression, but that's more like a warning.)

Recall how I'd expect to use the parallelism features (because it's the way I
do all of my Ada programming these days): add parallel to an appropriate loop
and let the compiler tell me what needs to be changed. Ada compilers are ten 
times better at finding issues than I would be -- the big problem I have with
the current tasking model is that it leaves the programmer completely on your
own. I realize that finding every problem statically is probably impractical,
but I don't want to leave anything obvious get through. (If one remembers that
one can only have a single global object in order to be safe, then a proper
set of rules should make it hard to have any undetected problems in that case.
More than one global object is a lost cause; I'd just ban parallelism in that
case, but I don't know how to even do that. :-)

> So I don't find any of the above issues particularly relevant to AI12-0079
> and its use in annotating language-defined packages.  *However*, I do think
> we have a significant issue with respect to access types.  We really want a
> way to say that the side-effects are limited to heap objects "reachable"
> from a given parameter.  Saying that a subprogram updates something designated
> by a given access type is pretty useless.

I don't think there is any other practical option. This just demonstrates why
one should never use access types in visible interfaces. (I think I've been
saying that for 20 years. ;-)

> So I plan to spend some time thinking about this problem of access types,
> especially in the context of container-like packages that clearly use
> access types behind the scenes.  But I don't see that there is much more
> needed to address the issues you identify above.  If you don't agree,
> please advise!

Luckily, we previously agreed to add reading operations that pass the
container. (Which also allows sensible prefix notation using the container
object for reading.) The preconditions then disallow any cases where we are
talking about the implicit container. So I think we're OK reasoning just about
cursor referencing something in the "current" container object,
Which doesn't need to be mentioned in Global.

The old reading operations are a lost cause, but that's OK: don't use them if
you care about the Global reference. BTW, do we have an annotation for "any
object of a type"? That's what those need (it's not designated by some access
type, since there is no visible access definition, and I would be disgusted to
have to declare such a type just for use in Global references).

Not that I would mind if you have some better definition, I'm sure it would be
useful somewhere.

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

From: Tucker Taft
Sent: Monday, February 19, 2018  10:25 PM

> I don't see any good reason to allow writes to atomic objects to be
> considered safe unless they are writing a static value, or are using one of
> a atomic update operations that Bob doesn't think we need to define. ;-) ...

This is an interesting point of view, but I still think it is completely 
unrelated to the Global annotation AI.  I still think this is more of a
"warning" situation than an error.  I don't think we should be in the
business of disallowing use of atomic variables to provide synchronization,
but I could see a compiler warning you about certain uses.

>>... *However*, I do think
>> we have a significant issue with respect to access types.  We really
>> want a way to say that the side-effects are limited to heap objects
>> "reachable" from a given parameter.  Saying that a subprogram updates
>> something designated by a given access type is pretty useless.
>
>I don't think there is any other practical option. This just demonstrates
>why one should never use access types in visible interfaces. (I think I've
>been saying that for 20 years. ;-)

I am not talking about using access types in a visible interface, but rather
trying to define what a given interface does in terms of its reading and
writing of heap-resident data, in a way that it can be checked by the
compiler.

In any case, I have some new ideas how to do this, using a 'Reachable 
attribute.  I'll write this up shortly.

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

From: Randy Brukardt
Sent: Monday, February 19, 2018  11:49 PM

>> I don't see any good reason to allow writes to atomic objects to be
>> considered safe unless they are writing a static value, or are using one of
>> a atomic update operations that Bob doesn't think we need to define. ;-) ...
>		
> This is an interesting point of view, but I still think it is completely
> unrelated to the Global annotation AI.  I still think this is more of a
> "warning" situation than an error.  I don't think we should be in the
> business of disallowing use of atomic variables to provide synchronization,
> but I could see a compiler warning you about certain uses.

We *should* be in the business of disallowing unsafe code by default (for the 
purpose of parallel execution), and that is what Global does here.
Anything should be fine in the Global => all case, because that doesn't
promise any safety. Atomic variables are only usable for synchronization with
xtreme care, and "extreme care" runs counter to the purpose of having safety 
rules in the first place. (You can use any sort of global object with "extreme
care", after all. :-)

But I agree this should be a "suppressible error" (indeed, one could argue that
all of the checks for a parallel loop, etc. should be suppressible). Of course,
that would imply that Bob or someone decides to actually progress that AI...

...
> I am not talking about using access types in a visible interface, but rather
> trying to define what a given interface does in terms of its reading and
> writing of heap-resident data, in a way that it can be checked by the
> compiler.

OIC. You're worried that the static rules would pretty much have to disallow 
doing anything heap-related in the body of a subprogram, since we don't know 
that the heap objects "belong" to the parameter and won't be shared with other
objects. (Such heap objects shouldn't appear in Global at all -- the part I
was worrying about -- since they are of types that are likely private/body and
designate types only defined in the private part or body, and as such
mentioning them is nonsense.) Having to include the "heap" in Global in such a
case would make almost everything Global => all, which isn't useful.

> In any case, I have some new ideas how to do this, using a 'Reachable
> attribute.  I'll write this up shortly.

Sounds good. Hope it isn't too complicated.

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

From: Tucker Taft
Sent: Saturday, February 24, 2018  9:01 PM

> ...
> 
> However, we've never defined what the freezing point of a package 
> declaration is, so the place where these aspects are evaluated is not 
> well-defined. So I don't even know if this formulation is legal. And 
> if it isn't legal, is there any alternative that IS legal that doesn't 
> require repeating Nonblocking and Global aspects 70 times.

Below are two paragraphs I am planning to add to the Global aspect AI.  Do
these address this issue adequately?

----------

Modify 13.1.1(11/3):

  The usage names in an aspect_definition [Redundant: are not resolved
  at the point of the associated declaration, but rather] are resolved
  at the end of the immediately enclosing declaration list{, or in the
  case of the declaration of a library unit, at the end of the visible
  part of the entity}.
  
Modify 13.14(3/5):

  The end of a declarative_part, protected_body, or a declaration of a
  library package or generic library package, causes freezing of each
  entity and profile declared within it{, as well as the entity itself
  in the case of the declaration of a library unit}.

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

From: Randy Brukardt
Sent: Monday, February 26, 2018  9:34 PM

> Below are two paragraphs I am planning to add to the Global aspect AI.  
> Do these address this issue adequately?

So long as they don't stomp on the rules for categorization aspects, we should
be fine.
 
> ----------
> 
> Modify 13.1.1(11/3):
> 
>   The usage names in an aspect_definition [Redundant: are not resolved
>   at the point of the associated declaration, but rather] are resolved
>   at the end of the immediately enclosing declaration list{, or in the
>   case of the declaration of a library unit, at the end of the visible
>   part of the entity}.


Luckily, 13.1.1(32/4) is a "Notwithstanding" rule, so what we say for the 
"normal" case doesn't matter. In particular, 13.1.1(32/4) says:

Notwithstanding what this International Standard says elsewhere, the 
expression of an aspect that can be specified by a library unit pragma is
resolved and evaluated at the point where it occurs in the 
aspect_specification[, rather than the first freezing point of the
associated package].

The redundant remark might be a bit confusing (depending on whether the above
paragraph or the below paragraph is read), but it seems OK. Or we could change
it to "rather than the end of the visible part of the entity".

Humm: do library units that are subprograms or renames have a visible part??
Humm part 2: the index points us to a sentence (in 8.2(5)) that is described
as "redundant" for the definition of visible part. Anyway, that implies that
a subprogram profile is the visible part; for a renames, it appears that
there is no visible part. So, let's rephrase: does the visible part of a
subprogram or rename have a well-defined end?
   
> Modify 13.14(3/5):
> 
>   The end of a declarative_part, protected_body, or a declaration of a
>   library package or generic library package, causes freezing of each
>   entity and profile declared within it{, as well as the entity itself
>   in the case of the declaration of a library unit}.

Looks OK to me.

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

From: Tucker Taft
Sent: Monday, February 26, 2018  10:28 PM

> Humm: do library units that are subprograms or renames have a visible part??

Yes they do.  Look in RM 8.2

> Humm part 2: the index points us to a sentence (in 8.2(5)) that is 
> described as "redundant" for the definition of visible part. Anyway, 
> that implies that a subprogram profile is the visible part; for a 
> renames, it appears that there is no visible part.

The wording might not be precise in its use of "entity" vs. "declaration," but
I think it is clear the intent that the profile in a subprogram renaming is
the visible part.

> So, let's rephrase: does the visible part of a subprogram or rename 
> have a well-defined end?

It seems like it ends at the end of the profile.  Where else would it end?

>> Modify 13.14(3/5):
>> 
>>  The end of a declarative_part, protected_body, or a declaration of a  
>> library package or generic library package, causes freezing of each  
>> entity and profile declared within it{, as well as the entity itself  
>> in the case of the declaration of a library unit}.
> 
> Looks OK to me.

Good.

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

Questions? Ask the ACAA Technical Agent