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

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

!standard 7.3.2(3/3)          13-10-13 AI12-0079-1/01
!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.
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
** TBD.
!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.
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)).
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;
!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.

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

Questions? Ask the ACAA Technical Agent