!standard 4.6(24.21/4)                              20-07-24  AI12-0387-1/01
!standard 6.1.1(0)
!standard 13.1.1(17/5)
!standard 13.1.1(18/4)
!standard H.4(23.2/5)
!standard H.4(23.3/5)
!standard H.4(23.4/5)
!standard H.7(0)
!class Amendment 20-06-09
!status work item 20-06-09
!status received 20-06-08
!priority Low
!difficulty Medium
!subject Private_Global aspect
!summary

The Private_Global aspect is introduced.

!problem

We would like to give implementors some freedom in implementing
language-defined package specs, including in the area of usage of global
variables.  Originally we thought we could allow implementors to add "in
out synchronized" as needed, and presumed that there would be
no impact on users of the package.  Alas, that is not so simple if the
user of the package is also interested in using Global aspects, because
as currently defined, any global variable that a called routine uses must be
reflected somehow in the Global aspect of the caller.  This clearly can
create a situation where a very small change deep within an
implementation, to add a cache, for example, or some logging code, could
have ripple effects throughout the implementation, and even worse,
affect many of the existing clients.

!proposal

Ada has a strong separation between spec and body, and it makes sense to
make a similar separation if possible in terms of global variable usage.
Some global variable usage is relevant to the caller, and should not be
hidden within the implementation.  But other global variables are merely
for caching, logging, or other caller-irrelevant purposes, and should
not need to be reflected in the caller-visible Global aspect.

We therefore propose to allow a Private_Global aspect on the body of a
program unit, and on the body of a library unit as a default for program
units completed within the library unit body, to specify global variable
usage that is not relevant to the caller.  The syntax would be identical
as the Global aspect, and the sets of global variables that are allowed
to be read or written by a given program unit would simply be the union
of the Global and Private_Global aspect.  At a subprogram call (or other
invocation of a program unit), only the Global aspect of the invoked
routine would be relevant to the caller, and would have to be covered by
the union of the caller's Global and Private_Global aspects.

Clearly Private_Global aspects should under normal circumstances be
limited to globals that are not visible to the callers, and similarly
should normally be synchronized, but we do not propose to limit that at
this point.  Implementations are permittted to enforce such
restrictions, but for now we require only a simple capability of
separating caller-relevant globals from those that are not of concern to
the caller.  The intent is that if two calls have the same
caller-relevant inputs (i.e. Global variables and in [out] parameters),
then they should return the same result in the caller-relevant outputs
(i.e. Global variables and [in] out parameters). We allow
implementations to detect and complain about such situations  Similarly,
we allow implementations to complain if two calls that would normally
not conflict based strictly on the caller-relevant inputs and outputs
would now conflict if the Private_Global aspects are considered.  As
usual, program execution would be erroneous if an actual data race
occurs.

!wording

Modify H.7(1/5):

  H.7 Extensions to Global and Global'Class Aspects

  In addition to the entities specified in 6.1.2, the Global aspect may
  be specified for a subtype (including a formal subtype), formal
  package, formal subprogram, and formal object of an anonymous
  access-to-subprogram type. {The Private_Global aspect may be
  specified on bodies of program units for which a Global aspect is
  permitted on their specification. Private_Global follows the same
  syntax, name resolution, and legality rules as Global.}

Modify H.7(2/5):

  The following additional syntax is provided for specifying Global{,
  Private_Global,} and Global'Class aspects, to more precisely describe
  the use of generic formal parameters and dispatching calls within the
  execution of an operation:

Add after H.7(19/5):

  If a Private_Global aspect is specified on the body of a program
  unit, then within the body of the unit, the relevant global variable
  sets are each the union of those determined by the Global aspect with
  those determined by the Private_Global aspect. If a Private_Global
  aspect is not specified it defaults to that of the enclosing library
  unit body. If no Private_Global aspect is specified on the enclosing
  library unit body, then it is as though the Private_Global aspect were
  specified as NULL, meaning the subprogram is limited to the sets of
  global variables determined by the Global aspect on the
  specification.

Add after H.7(22/5):

   Implementation Permissions

  An implementation may restrict the use of global variables identified
  by a Private_Global aspect applicable to the body of a program unit,
  if it can determine that the use of such a global variable would
  produce different results in two distinct invocations of the program
  unit, in terms of the IN OUT and OUT formal parameters and visible
  globals, given equivalent inputs in terms of the IN and IN OUT
  parameters and visible globals, where the /visible globals/ are those
  identified by an applicable Global aspect. Similarly, the
  implementation may restrict uses of such global variables if the usage
  could introduce a conflict with other actions occurring in other
  logical threads of control, if such a conflict would not otherwise
  exist. The possible consequences of violating such restrictions are
  implementation defined, and could include a compile-time error or the
  raising of Program_Error at run time.

!discussion

Rather than defining a Bounded Error if Private_Global usage could change
the "visible" results, or introduce a conflict with another logical
thread of control, we give the implementation permission to restrict
such usage, with consequences that match those of Bounded Errors. We
chose this approach because formally defining the circumstances for
the bounded error is not practical given the difficulty of defining
equivalence in inputs and outputs. We leave this area to implementations,
while giving them permission to introduce compile-time or run-time
restrictions that can provide additional safety guarantees.

!example

TBD

!ASIS

No ASIS effect.

!ACATS test

ACATS B-Tests are needed to check that the updated rules are enforced.

!appendix

From: Claire Dross
Sent: Monday, July 6, 2020  4:29 AM

while reading the AI for global processing which was at the agenda of the last 
meeting (but that we did not discuss), I was surprised to see a new 
Private_Global aspect:

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0380-1.txt?rev=1.4&raw=N

I did not see any discussion about it in the list, so I wanted to start it. 
Maybe somebody could give a rationale? For me, it seems to be a way to hide 
Globals under the rug. I understand the argument that it might be fine for 
parallelism as long as these hidden globals are synchronized. However in this
case, why not simply write in out synchronized? Maybe a motivating example 
would help.

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

From: Tucker Taft
Sent: Monday, July 6, 2020  6:31 AM

We have discussed in various AIs and various ARG meetings the desire to allow 
implementors of the language-defined packages to introduce local synchronized 
objects.  However, knowing exactly where this would happen is not something we
want to specify in the standard.  The presumption was that the implementor 
could simply add "in out synchronized" to their implementation at appropriate 
points, and all would be well.

Alas, if a user wants to call a language-defined subprogram, and the 
implementor has added "in out synchronized" when it wasn't there in the Ada 
standard definition, then the user's attempt to write "Global => null" (for 
example) for such a subprogram will fail, since it doesn't account for the 
"hidden" side effects.  Furthermore, if they add "in out synchronized" to 
their routines, then there will be a ripple effect all the way up the call 
hierarchy.

A similar effect occurred in the C++ standard with exception "throw" 
specifications, where the ripple effects became so painful that they 
ultimately removed such "throw" specifications from the language in a recent 
revision.

So we need some way to explicitly say that a particular global side effect 
need not be reflected all the way up the chain of calls.  The simplest 
mechanism was to allow an explicit notion of a "private" global side effect.  
As you can read from the proposed rules, the intent of saying "private" is 
that the caller need not be aware of the effects, and implementations are 
allowed to check that by verifying that the use of the "private" globals has
no effect on the "visible" result.  However, we don't *require* 
implementations to do this sort of check, presuming this is an area where 
additional static analysis would be necessary.

In the context of SPARK, a similar situation is handled by hiding such effects 
in code with SPARK mode off.  Alas, in Ada, we don't have that luxury, so a 
"private" global is similar, saying these effects should not be incorporated 
into the effects that are checked at a call site, but might be of interest 
for other purposes.

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

From: Claire Dross
Sent: Tuesday, July 7, 2020  3:04 AM

> We have discussed in various AIs and various ARG meetings the desire to 
> allow implementors of the language-defined packages to introduce local 
> synchronized objects.  However, knowing exactly where this would happen 
> is not something we want to specify in the standard.  The presumption was 
> that the implementor could simply add "in out synchronized" to their 
> implementation at appropriate points, and all would be well.
>
> Alas, if a user wants to call a language-defined subprogram, and the 
> implementor has added "in out synchronized" when it wasn't there in the 
> Ada standard definition, then the user's attempt to write "Global => null"
> (for example) for such a subprogram will fail, since it doesn't account for
> the "hidden" side effects.  Furthermore, if they add "in out synchronized" 
> to their routines, then there will be a ripple effect all the way up the 
> call hierarchy.

This does not seem convincing to me TBH. The ripple effect, as you called it, 
is well known indeed, and is possibly the main reason people don't want to 
use the Global aspect in SPARK (they let the tool infer it). However, simply
allowing to hide effects seems to remove the interest of the feature. All 
the more since, unlike for SPARK, avoiding this ripple effect in Ada seems 
easy enough. Just add in out synchronized everywhere if you don't care about
these effects and you are done.

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

From: Arnaud Charlet
Sent: Tuesday, July 7, 2020  3:13 AM

Agreed, I don't see any actual user need/request for this capability so let's
postpone this after users have actually used the basic feature and expressed 
the need for more.

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

From: Randy Brukardt
Sent: Tuesday, July 7, 2020  1:36 PM

The ripple effect is a basic effect of any contract, and worrying about that 
isn't much of an argument. But the problem here is portability, especially of
language-defined packages.

Let me explain how we got to this point.

Originally, the language-defined impure packages were supposed to have a 
Global of "synchronized in out private of <my-package>", essentially allowing 
local global synchronized state. There also was a permission for implementers 
to add "synchronized in out <helper-package>" to any such specification. This 
was motivated by the desire to allow implementers to define and use helper 
packages to implement language-defined units.

When the package-level synchronized specifications were dropped (along with 
the package visible specifications), the permission got changes to "in out 
synchronized". For some reason, Tucker decided to drop the visible state 
from the packages.

I pointed out that "in out synchronized" is not compatible with "null", so 
that we'd have a portability problem: if say GNAT used "null" for vectors 
and say Janus/Ada used "in out synchronized" for vectors, then GNAT code 
using Global=> null could not be compiled by Janus/Ada.

So I suggested that all such packages be "in out synchronized" (which would 
directly correspond to the original specification anyway). Tucker objected for
reasons that I still don't really understand and developed the Private_Global 
aspect as an alternative. I believe his view is that most such state is 
benign, in that it really doesn't affect the result values (at most, it might 
change when exceptions are raised or not from erroneous code/bounded error 
code).  

I'd be happy just declaring all such packages to be "in out synchronized", as 
I don't think SPARK and similar static analysis is going to use non-specific 
globals if the body is available anyway, and if the body isn't available one 
needs to assume the worst (which "in out synchronized" would be).

Of course, doing that makes it more important that Global => null really mean 
that, as it will be specified more often.

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

From: Arnaud Charlet
Sent: Tuesday, July 7, 2020  3:19 PM

> I'd be happy just declaring all such packages to be "in out 
> synchronized", as I don't think SPARK and similar static analysis is 
> going to use non-specific globals if the body is available anyway, and 
> if the body isn't available one needs to assume the worst (which "in 
> out synchronized" would be).

Looks good to me, at least until we have real user needs for more.

We've already spent too much time on this feature, we really need to close 
Ada 202x at this stage without inventing new things that nobody will ever use.

Here we're trying to introduce Private_Global basically to solve a theoretical 
concern about portability across Ada implementations, where it's clear that 
there will be exactly zero Ada compilers implementing the Global aspect in the
first place and so we're adding Private_Global and stuff in annex H and lots 
of complex (and probably buggy) annotations in the standar library adding more
on top of these that again, will be ignored by all compiler implementors.

This is really getting out of control so we should really stop there IMO and 
take a deep breath.

> Of course, doing that makes it more important that Global => null 
> really mean that, as it will be specified more often.

Looks good as well.

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

From: Jeff Cousins
Sent: Tuesday, July 7, 2020  3:27 PM

I sympathise with this too.

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

From: Claire Dross
Sent: Wednesday, July 8, 2020  2:17 AM

I completely agree with Arnaud. Let's keep it as simple as it can still 
possibly be. If the intent of the library is to have in out synchronized, 
then just use it, or avoid annotating parts of the library which are not 
too important (ie. use Unspecified).

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

[Editor's note: After this thread, Private_Global was split out into an AI
of it's own - this AI.]

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