Version 1.13 of ai12s/ai12-0038-1.txt

Unformatted version of ai12s/ai12-0038-1.txt version 1.13
Other versions for file ai12s/ai12-0038-1.txt

!standard E.2.1(7/1)          15-01-27 AI12-0038-1/07
!class binding interpretation 12-11-28
!status Corrigendum 2015 12-12-31
!status work item 13-01-04
!status ARG Approved 5-0-4 12-12-09
!status work item 12-11-28
!status received 12-06-23
!priority Low
!difficulty Medium
!subject Shared_Passive package restrictions
!summary
Shared_Passive restrictions have to be adjusted because declared-pure packages now allow the declarations of access types.
[Editor's note: These changes were included in the draft Standard when they were initially approved. We're no longer certain that they are correct, so they have much more risk of change.]
!question
Shared passive packages are allowed to depend on declared-pure packages. In Ada 2005, access type declarations were allowed in declared-pure packages, but the implications of this were not accounted for in the restrictions on shared passive packages. Should we add new restrictions directly on shared passive packages to account for this change? (Yes)
!recommendation
Shared passive packages shall not reference within a library-level declaration a type from a declared-pure package that contains a part that is of an access type. Note that this applies even if the type from the declared-pure package is a private type, and hence breaks the normal rules of privacy.
!wording
Modify E.2.1(7/1):
* it shall not contain a library-level declaration of an access type that designates a class-wide type, {nor a type with a part that is of a} task type[,] or protected type with entry_declarations{;
* it shall not contain a library-level declaration that contains a name that denotes a type declared within a declared-pure package, if that type has a part that is of an access type; for the purposes of this rule, the parts considered include those of the full views of any private types or private extensions}.
AARM Reason: This rule breaks privacy by looking into the full views of private types. Avoiding privacy breakage here would have required disallowing the use in a shared passive package of any private type declared in a declared-pure package, which would have been severely incompatible.
!discussion
The change to the existing bullet of E.2.1(7/1) is recognizing that tasks and protected objects with entries are bad news in an access collection (aka heap) within a shared-passive partition, whether they are whole objects or parts of other objects.
The new bullet following E.2.1(7/1) is intended to bolster E.2.1(8) to ensure that no access value of a "pure" access type could be embedded within an object of a shared-passive package, since it might point "back" into the data area of some particular active partition.
Shared passive packages are not allowed to declare access-to-class-wide types, but there is nothing preventing them from referencing an access-to-class-wide type declared in a declared-pure package. Furthermore, there is nothing preventing them using a type that has a part that is of an access type declared in a declared-pure package. The special shared-passive accessibility rules (E.2.1(8)) prevent creating values of an access type declared within the shared-passive package itself, that designate objects that might not be within the semantic closure of the shared-passive package. But these special accessibility rules don't apply to types declared in declared-pure packages, and hence values of such types might include references to such shorter-lived objects.
!examples
Here is an example to help illustrate the purpose of the original E.2.1(8) rule:
package P1 is X : aliased Integer; end P1;
package P2 is pragma Shared_Passive(P2); type Acc is access all Integer; end P2;
with P1, P2; package P3 is Z : P2.Acc := P1.X'access; -- legal? (No.) end P3;
P2 does not depend semantically on P1, so the above is illegal. However, if we were to add a "with P1" in P2's context clause, then it would be legal, provided, of course, that P2 could legally depend on P1. That is only possible if P1 is itself a shared-passive package, since it cannot be "Pure" given that it has a variable. (Note that we could make X an aliased constant, and make "Acc" an "access constant" type, and then P1 could be a Pure package.)
This rule makes sense because unless P2 depends on P1, there is no guarantee that P1 will live as long as P2. We don't want a value of type P2.Acc designating an object in a package that doesn't live as long as P2. For shared-passive packages, it is semantic dependence that determines relative longevity.
Here is the problem that the new paragraph after E.2.1(7/1) is intended to address:
package P0 is pragma Pure(P0); type Trouble is private; function Make_Trouble(Z : access Integer) return Trouble; private type Pure_Acc is access all Integer; for Pure_Acc'Storage_Size use 0; type Trouble is record PA : Pure_Acc; end record;
function Make_Trouble(Z : access Integer) return Trouble is (Trouble'(PA => Pure_Acc(Z))); end P0;
package P1 is X : aliased Integer; end P1;
with P0; package P2 is pragma Shared_Passive(P2); type Rec is record Troub : P0.Trouble; -- legal? (No.) end record; end P2;
with P1, P2; package P3 is Z : P2.Rec := (Troub => P0.Make_Trouble(X'access)); -- not allowed end P3;
Here we have used a type from the pure package P0 within a library-level type declaration in shared-passive package P2, and that type has a part that is of an access type. In P3 we set a value of that type to designate an object in P1. Just because P0 was originally declared in a pure package doesn't change the story. We definitely don't want any type defined in P2 to have a value that contains a pointer to an object in a package that doesn't live as long as P2. So with this new paragraph we simply disallow a shared-passive package using such a type, even though it requires us to break normal privacy rules.
We originally tried to augment the special accessibility rule, but that was inadequate, because accessibility of components is not re-checked on composite assignment, and so we felt we had to prevent the declaration or use of composite types in shared-passive pacakges that might carry pointers to shorter-lived objects.
!corrigendum E.2.1(7/1)
Replace the paragraph:
by:
!ACATS test
An ACATS B-Test should be created to check that the new rule is actually enforced; the example in discussion could be used as a basis.
!ASIS
No ASIS impact.
!appendix

From: Tucker Taft
Sent: Thursday, November 29, 2012  8:49 AM

I was tasked with splitting off an AI from AI12-0031, to deal with issues associated
with shared-passive packages and their interaction with declared-pure packages.
The basic problem is that in Ada 2005 we starting allowing access types to be declared
in declared-pure packages, but didn't adjust the rules for shared-passive packages to
account for that change.

So here is a proposed new AI that tries to do that.

[This is version /01 of this AI.]

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

From: Randy Brukardt
Sent: Thursday, November 29, 2012  1:27 PM

...
> So here is a proposed new AI that tries to do that.

I fear the Mayans are right about an impending apocalypse, as the point when Tucker is
among the first to finish most of his homework is roughly as likely as me winning the
Powerball lottery. :-)

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

From: Randy Brukardt
Sent: Thursday, November 29, 2012  8:12 PM

The first sentence of the !discussion says:

The accessibility rule of E.2.3(8) is intended to prevent pointers being created in a
shared-passive package that poing "back" into the data area of some particular active
partition.

"poing" is a new term for Ada, even informally. :-) I presume you mean "pointing", right?

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

From: Randy Brukardt
Sent: Thursday, November 29, 2012  8:15 PM

Upon further reflection, you probably meant "point" (no "ing").

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

From: Tucker Taft
Sent: Thursday, November 29, 2012  8:16 PM

> "poing" is a new term for Ada, even informally. :-) I presume you mean
> "pointing", right?

Oops.  I meant "point".

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

From: Randy Brukardt
Sent: Monday, December 31, 2012  6:08 PM

For AI12-0038-1, we approved the following wording:

it shall not contain a library-level declaration of an access type that
designates a class-wide type, task type, or protected type with
entry_declarations{; further, it shall not contain a library-level declaration
that includes a name that denotes a subtype with a part having an access type
that is declared within a declared-pure package}.

So far so good. Then, the first draft of the minutes on the meeting go on to
say:

A non-limited private type that has stream attributes and an access component
could be legal in a declared-pure package (as the type would then have external
streaming). If the package also declares a function that is passed an access
value and returns that type could cause trouble by storing the parameter value
into the component and then returning that to be stored in an object of the
shared-passive partition. No solution is obvious: a solution would seem to
require making referencing any non-limited private types illegal which seems way
over the top. We're going to ignore this problem.

Say what?? Did we really decide this? (Probably, as 4 people abstained,
presumably because of this hole.)

The problem here is that we can't get away with completely ignoring this "hole".
If we ignore it, we're saying that compilers have to make it work. But that
makes no sense; if we're going to require it to work in some (obscure) case,
then we surely don't need E.2.1(7-8) to prevent it in most cases. Even if we
can't figure out an appropriate rule, we need to let compilers off the hook
somehow.

Specifically, we either need a Legality Rule, some sort of run-time check, or it
has to be erroneous.

A Legality Rule would be easy if we could break privacy, but we can't.
Probably the best solution would to attack the function that is required to
cause a problem (as it has to return the type, and take a parameter with a part
of an access type). But there probably are more forms of this (for instance, a
procedure with an out parameter of the type), so such a solution is likely to be
fragile.

I suppose we could have a To-Be-Honest AARM note that implementations need to
break privacy to make the check described by the wording given above. (That
seems to be OK since Mr. Private is retired. ;-) I would hope that is a last
resort, however.

A run-time check might happen here anyway (we're talking about passing an access
parameter in most of the scenarios), but adding overhead for this is not
appealing. And figuring out the interactions of E.2.1(8) and the algorithms
described for AI12-0016-1 sound like torture.

There is some argument for making it erroneous; I suspect that there are other
ways to get an access value of some other partition (via chapter 13 means, at
least), and those are probably going to be erroneous (at least we hope so!). A
small expansion isn't going to be a major problem.

Another option would be to make assigning a non-limited private type that has
part of an access type declared in a declared-pure package a bounded error
inside of a shared-passive package. Either it works (no one will want to
implement that) or it raises Program_Error. This check (being at runtime) can
break privacy, but in actual fact, it would always be detected at compile-time.
(And presumably would have an associated warning.) [Since the package is
preelaborated, a dangerous value can only be introduced by a later assignment,
as no constructor functions are allowed -- I think.] Or perhaps just do this for
the declaration of such an object at library-level in a shared passive package.

Should we reopen this AI to get *some* solution to this problem?? (I have no
idea what to write in the AI to explain why we're ignoring this hole.) Is there
any better ideas of a solution?

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

From: Brad Moore
Sent: Friday, January  4, 2013  2:43 PM

...
> A Legality Rule would be easy if we could break privacy, but we can't.
> Probably the best solution would to attack the function that is
> required to cause a problem (as it has to return the type, and take a
> parameter with a part of an access type). But there probably are more
> forms of this (for instance, a procedure with an out parameter of the
> type), so such a solution is likely to be fragile.

There seems to be a myriad of ways to do this sort of thing other than returning
a type that has an access component. Consider:

private with Ada.Streams;

package Pure_P is
   pragma Pure;

   type T is private with Preelaborable_Initialization;

   type Access_T is access all T with Storage_Size => 0;

   procedure Add (X : in out T;
                  Val : Integer;
                  Next : access T);  -- Anonymous Access

   procedure Add2 (X : in out T;
                  Val : Integer;
                  Next : Access_T);  -- Access Type

   procedure Add3 (X : in out T;
                   Val : Integer;
                   Next : aliased in out T);  -- Aliased

   function Value (X : T) return Integer;

private

   type Array_Of_Access_T is array (1 .. 10) of Access_T;
   type Array_Of_Anon_Access_T is array (1 .. 10) of access T;

   type T is record
      Val : Integer := 0;
      Count : Integer := 0;
      Count2 : Integer := 0;
      List : Array_Of_Anon_Access_T;
      List2 : Array_Of_Access_T;
   end record;

   procedure Read
     (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
      Item : out T);
   for T'Read use Read;

   procedure Write
     (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
      Item : T);
   for T'Write use Write;

end Pure_P;

package body Pure_P is

   procedure Add
     (X : in out T;
      Val : Integer;
      Next : access T)
   is
   begin
      X.Count := X.Count + 1;
      X.List (X.Count) := Next;
      Next.Val := Val;
   end Add;


   procedure Add2
     (X : in out T;
      Val : Integer;
      Next : Access_T)
   is
   begin
      X.Count2 := X.Count2 + 1;
      X.List2 (X.Count2) := Next;
      Next.Val := Val;
   end Add2;

   procedure Add3 (X : in out T;
                   Val : Integer;
                   Next : aliased in out T) is
   begin
      X.Count2 := X.Count2 + 1;
      X.List2 (X.Count2) := Next'Unchecked_Access;
      Next.Val := Val;
   end Add3;

   procedure Read
     (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
      Item : out T) is
   begin
      Integer'Read (Stream, Item.Count);
      for I in 1 .. Item.Count loop
         ...
      end loop;

      Integer'Read (Stream, Item.Count2);
      for I in 1 .. Item.Count2 loop
         ...
      end loop;

   end Read;

   function Value (X : T) return Integer is
   begin
      return X.Val;
   end Value;

   procedure Write
     (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
      Item : T) is
   begin
      Integer'Write (Stream, Item.Count);
      for I in 1 .. Item.Count loop
         ...
      end loop;

      Integer'Write (Stream, Item.Count2);
      for I in 1 .. Item.Count2 loop
         ...
      end loop;
   end Write;

end Pure_P;

with Pure_P;
package Normal_P is
   X, Y : aliased Pure_P.T;
end Normal_P;

with Pure_P;

package Passive_P is
   pragma Shared_Passive;
   X : Pure_P.T;
end Passive_P;

with Normal_P;
with Pure_P;
with Passive_P;
procedure Main is
   X, Y : aliased Pure_P.T;
begin
   Pure_P.Add (X    => Normal_P.X,
               Val  => 1,
               Next => Normal_P.Y'Access);  -- Store anonymous access to Normal variables in Shared package

   Pure_P.Add2 (X    => Passive_P.X,
               Val  => 1,
               Next => X'Unchecked_Access);  -- Store named access to local variables in Shared package

   Pure_P.Add3 (X    => Passive_P.X,
                Val  => 1,
                Next => Y);                   -- Store access to aliased variable in Shared package
end Main;

The proposed wording of this AI breaks privacy in these examples.

Could a solution to prevent privacy breaking involve a new aspect similar to the
way Preelaborable_Initialization works that says that the full view of a
private type does not contain parts that involve access types?

Perhaps No_Access_Components as in...

package Pure_P is
   pragma Pure;

   type T is private with Preelaborable_Initialization, No_Access_Components;

   ...

private

   ...
end Pure_P;

Then the wording for Shared Passive units could be tweaked to only allow non
limited private types that have this aspect.

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

From: Tucker Taft
Sent: Friday, January  4, 2013  3:10 PM

We don't need to protect against examples using Unchecked_Access.

I would say make it a bounded error if there is no use of Unchecked_Access.

If Unchecked_Access is used, then as usual execution can become erroneous if the
designated object disappears and someone dereferences the access value stored in
the passive partition.

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

From: Randy Brukardt
Sent: Friday, January  4, 2013  7:03 PM

> We don't need to protect against examples using Unchecked_Access.

Right. The "original" rule that prevents these problems is an accessibility
check, and the whole point of 'Unchecked_Access is to turn off accessibility
checks.

> I would say make it a bounded error if there is no use of
> Unchecked_Access.

The advantage of a Bounded Error is that it is a runtime check, and thus can
break privacy (or more accurately, privacy is not considered). The question is,
exactly what is checked?

The rule I suggested was that the *assignment* of an object that has an access
part declared in a pure unit is a bounded error. I suppose that would also have
to cover reference parameter passing (I forgot about this in my original
message; I was thinking assignment covered all parameter passing, which is
wrong). But the idea is that the check is on the assignment or parameter passing
of an object declared in a shared passive package.

I don't see how it could be on the access value or object passed in, unless we
want to insist on full run-time accessibility checking in this case. (In which
case, I don't think it needs to be a bounded error, it just has to be checked at
run-time.) But that seems like it would have distributed overhead.

> If Unchecked_Access is used, then as usual execution can become
> erroneous if the designated object disappears and someone dereferences
> the access value stored in the passive partition.

Right.

But in any case my original question was whether we need to reopen the AI to
determine a solution. If we do that, then there is plenty more time for the AI
author (that would be Tucker) to figure out a solution (we don't have to have it
now).

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

From: Tucker Taft
Sent: Sunday, June  9, 2013  3:23 PM

I came up with a possible simple fix for this one.  I propose that whenever a
reference is made to an access type declared in a declared-pure package is used
within a library-level declaration of a shared-passive package, that it
effectively "inherits" the special accessibility rule of access types declared
in shared-passive packages.  I didn't work out all of the implications, but I
think this is approximately right... [This is version /03 of the AI.]

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

From: Tucker Taft
Sent: Monday, October 13, 2014  1:23 PM

Here is an update to AI12-0038, which relates to how accessibility works in
shared-passive packages, and in particular as it relates to using access types
declared in a pure package.  I mostly just added a couple of examples.

[This is version /05 of the AI - Editor.]

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

From: Tucker Taft
Sent: Monday, January 26, 2015  2:21 PM

Here is an update to AI12-0038, now version 6, relating to shared-passive
package use of access types from declared-pure packages. It is pretty nasty, in
that it breaks privacy. But that was the approach chosen by consensus at the
last ARG meeting because the alternatives seemed worse.

[This is version /06 of the AI - Editor.]

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

From: Bob Duff
Sent: Monday, January 26, 2015  3:34 PM

> Here is an update to AI12-0038, now version 6, relating to
> shared-passive package use of access types from declared-pure packages.  It is pretty nasty, in that it breaks privacy.

I agree it's nasty to break privacy.

>   But that was the approach chosen by consensus at the last ARG
> meeting because the alternatives seemed worse.

I agree that it's acceptable to break privacy in this case.

Is this the first time we have a legality rule that breaks privacy?

>    * it shall not contain a library-level declaration that contains a name
>      that denotes a type declared within a declared-pure package, if that
>      type has a part that is of an access type}.

Shouldn't this wording say explicitly that we're breaking privacy?
Normally, compile-time rules are understood to refer to visible views of things, but here we intend to refer to the full view(s).
Something like, "For the purposes of this rule, we refer to the full view of any private types or private extensions."?
Or, "For the purposes of this rule, the 'parts' include those of the full views of any private types or private extensions."?

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

From: Randy Brukardt
Sent: Monday, January 26, 2015  3:51 PM

...
> Is this the first time we have a legality rule that breaks privacy?

I believe so. I don't think it would have politically flown in the past.
(Not sure it will now, either, but there's more chance.)

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

From: Robert Dewar
Sent: Monday, January 26, 2015  3:57 PM

Aren't rep clauses like size clauses examples of legality rules that break
privacy?

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

From: Randy Brukardt
Sent: Monday, January 26, 2015  4:09 PM

How so? You can't have a size clause on a partial view, and you can't give it on
a type that includes a partial view. The runtime effects of a size clause don't
effect legality (and of course, there is no privacy in dynamic semantics).

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

From: Randy Brukardt
Sent: Monday, January 26, 2015  4:29 PM

As soon as I pressed 'send', I realized that you meant used as a client rather
than within a single package (which is what I was thinking about for some silly
reason). Specifically, the size of some type Priv is only defined within the
private part (because of the rules I was thinking about previously), so in some
type where it is used, a Size clause has to take into account the size that it
can't know without looking in the private part.

And you're right that 13.1(12/3) is formally a Legality Rule, and it surely
breaks privacy for the previous reasons.

However, I always think of representation stuff as part of the dynamic domain,
so privacy breaking goes with the territory. (My understanding is that was
precisely how it was handled in the Rational compiler.) So the fact that some of
the rules are actually Legality Rules is a bit surprising, as they feel like
something else altogether.

This proposed rule, however, is clearly and solely within the static semantics
domain, where we've never previously tolerated privacy breaking. Once we adopt
this rule, we'll have broken the dam and we'll never again consider privacy
breaking an automatic disqualification for a rule (although I hope we don't
start adding such rules lightly).

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

From: Tucker Taft
Sent: Monday, January 26, 2015  4:32 PM

> How so? You can't have a size clause on a partial view, and you can't
> give it on a type that includes a partial view. The runtime effects of
> a size clause don't effect legality (and of course, there is no
> privacy in dynamic semantics).

You can put a size clause on a record that contains a component of a private
type.  The success of that size clause depends on the size of the private type.
So yes, representation clauses can effectively break privacy.  We also allow
some categorization pragmas to break privacy, I believe, and certainly
Restrictions pragmas break privacy.

But this one feels a little nastier, since it is more of a pure semantic issue.

I suppose if we really felt bad, we could add another category such as
"Shared_Pure" which would ensure that any private types declared therein do not
contain access types. Shared_Pure could presumably only depend on other
Shared_Pure, and Shared_Passive could only depend on Shared_Pure.  But this all
seems a bit of overkill given how few users we have of the distribution annex.
In 20-15 hindsight <grin>, we should have probably had a different category such
as Shared_Pure rather than trying to make "Pure" mean something special both as
far as distribution and as far as being side-effect free.

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

From: Tucker Taft
Sent: Monday, January 26, 2015  4:34 PM

>>     * it shall not contain a library-level declaration that contains a name
>>       that denotes a type declared within a declared-pure package, if that
>>       type has a part that is of an access type}.
>
> Shouldn't this wording say explicitly that we're breaking privacy?

You are probably right.  We have often struggled with the meaning of "part" in static semantics, and we should probably be more explicit, especially in this very special case.

> Normally, compile-time rules are understood to refer to visible views
> of things, but here we intend to refer to the full view(s).
> Something like, "For the purposes of this rule, we refer to the full
> view of any private types or private extensions."?
> Or, "For the purposes of this rule, the 'parts' include those of the
> full views of any private types or private extensions."?

(recursively)

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

From: Randy Brukardt
Sent: Monday, January 26, 2015  6:40 PM

...
> >    * it shall not contain a library-level declaration that contains a name
> >      that denotes a type declared within a declared-pure package, if that
> >      type has a part that is of an access type}.
>
> Shouldn't this wording say explicitly that we're breaking privacy?
> Normally, compile-time rules are understood to refer to visible views
> of things, but here we intend to refer to the full view(s).

Bob's right. Remember that we adopted a blanket rule about the meaning of
Legality Rules that says that "view of" is always implied. (3.1(7.1/3), from
AI05-0080-1.) That was done particularly so we didn't have to rewrite every
Legality Rule where there might be a question. Here we need to hit any readers
over the head that this is privacy breaking - the normal case does not apply.

> Something like, "For the purposes of this rule, we refer to the full
> view of any private types or private extensions."?
> Or, "For the purposes of this rule, the 'parts' include those of the
> full views of any private types or private extensions."?

Perhaps "For the purposes of this rule, the parts are those of the full views of
any private types or private extensions."??

And then "AARM reason: This rule breaks privacy by looking into the full views
of private types. Avoiding privacy breakage here would have required disallowing
the use in a shared passive package of any private type declared in a
declared-pure package, which would have been severely incompatible."

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

From: Randy Brukardt
Sent: Monday, January 26, 2015  6:52 PM

...
> I suppose if we really felt bad, we could add another category such as
> "Shared_Pure" which would ensure that any private types declared
> therein do not contain access types.
> Shared_Pure could presumably only depend on other Shared_Pure, and
> Shared_Passive could only depend on Shared_Pure.  But this all seems a
> bit of overkill given how few users we have of the distribution annex.

Besides which it would still be incompatible for those users because we'd have
to ban any use of a private type that originates in a declared-pure package
(unless the declared-pure package was compiled in Ada 95 mode). Maybe OK if the
number is small enough, but I'm dubious.

>  In 20-15
> hindsight <grin>, we should have probably had a different category
> such as Shared_Pure rather than trying to make "Pure" mean something
> special both as far as distribution and as far as being side-effect
> free.

That really was a mistake of Ada 2005, as the Ada 95 Pure worked for both. But
the problem is that we tried to put lipstick on a pig to make Pure packages more
useful for the side-effect free case. The trouble is that requiring everything
side-effect free in a single package (with nothing else included) is
unrealistic. On top of which, the Pure restrictions aren't enough to use them in
parallel applications nor to use them in proof rules, so we'll have to have
something different for those anyway.

Probably should have left Pure packages alone (and mainly for distribution) and
invented an aspect (say, Global => null :-) for side-effect free subprograms
that can work for parallel and proof applications. But, as you say, hindsight is
20-20 (or maybe 20-15 in this case).

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

Questions? Ask the ACAA Technical Agent