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

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

!standard 9.5(47/5)          19-03-19 AI12-0319-1/04
!standard 9.5(68/5)
!standard 13.11(15)
!standard 13.11(17)
!standard 13.11(18/4)
!standard 13.11.2(3/5)
!class Amendment 19-02-22
!status Amendment 1-2012 19-03-11
!status ARG Approved 6-0-4 19-03-11
!status work item 19-02-22
!status received 19-02-22
!priority Low
!difficulty Medium
!subject Nonblocking for Unchecked_Deallocation is wrong
!summary
Add the ability for the Nonblocking attribute to be used to specify whether a type's initialization, finalization, and assignments allow blocking.
Add the Nonblocking attribute for an object, so it can be used to describe the storage pool of an access type.
Correct the definition of Unchecked_Deallocation using these new capabilities.
!problem
Unchecked_Deallocation has Nonblocking => True. However, it can be instantiated with a type whose Finalize routine blocks. This allows blocking in a nonblocking subprogram. Similarly, if the Deallocate routine for the storage pool of the access type blocks, we also would be allowing blocking in a nonblocking subprogram.
!proposal
The original problem led to determining that the definition of Nonblocking did not allow specifying whether object default initialization, finalization, or assignment allows blocking, nor whether object allocation, deallocation, and use of the Storage_Size attribute allow blocking.
We therefore extend existing mechanisms (the Nonblocking attributes) to ensure that we have sufficient contracts to describe those things in generic bodies with appropriate "assume-the-worst" rules.
We also add a rule requiring that the language-defined primitive operations of a controlled type and of a storage pool are nonblocking if the type is nonblocking.
We then use these new contracts to properly define Unchecked_Deallocation.
In discussing this, we also noticed that we need requirements on the standard pool(s). Such pools should be nonblocking so that they can be used within protected types. It was not intended by Ada 95 for an allocator to be potentially blocking, and we don't want to implicitly make such a change now.
Much of this wording is modifying previously approved Ada 2020 wording; the paragraph numbers are as found in Draft 18 of the Standard.
!wording
Modify 9.5(47/5): [Static Semantics, the definition of S'Nonblocking]
Denotes whether {default initialization, finalization, assignment, }predefined operators{, and} ([and] in the case of access-to-subprogram subtypes) a subprogram designated by a value of type S are considered nonblocking; the type of this attribute is the predefined type Boolean. S'Nonblocking represents the nonblocking expression of S; evaluation of S'Nonblocking evaluates that expression.
Add after 9.5(47/5):
For a prefix X that denotes an object:
X'Nonblocking
Denotes whether the type of X is considered nonblocking; the type of this attribute is the predefined type Boolean. X'Nonblocking represents the nonblocking expression of X; evaluation of X'Nonblocking evaluates that expression.
AARM To Be Honest: In the case when the prefix represents the Storage_Pool of some type, this is the specific type of the associated pool object, if known.
[Author's note: This is explaining how this works for S'Storage_Pool'Nonblocking. I don't think the type of the pool of an access type is well-defined; there's no requirement (elsewhere) to keep the static type of the pool object along with the access type. From the perspective of the access type, the pool object could be considered to be class-wide (Root_Storage_Pool'Class). It didn't seem worth spelling this out somewhere.]
Add after 9.5(68/5): [Legality Rules]
For a composite type that is nonblocking:
* All component subtypes shall be nonblocking;
* For a record type or extension, every call in the default_expression of a component (including discriminants) shall call an operation that is nonblocking;
* For a controlled type, the Initialize, Finalize, and Adjust (if any) subprograms shall be nonblocking.
AARM Ramification: Default initialization, finalization, and assignment of elementary types are always nonblocking, so we don't need any rules for those.
Add after AARM 9.5(82.e/5): [About assume-the-worst checking in generic bodies]
AARM To Be Honest: For checking in P, default initialization, finalization, and assignment of a composite formal type F is considered to call subprograms that have the nonblocking aspect of F'Nonblocking, and this is checked for conformance against that of P as described above. These operations of an elementary formal type are considered nonblocking, and thus require no checks.
Similarly, for checking in P, the implicit calls associated with an allocator of an access type A or a use of attribute A'Storage_Size are considered to call subprograms that have the nonblocking aspect of A'Storage_Pool'Nonblocking, and this is checked for conformance against that of P as described above. End To Be Honest.
[Author's note: We don't need to include instances of Unchecked_Deallocation in the above note, because that is an actual explicit call with an explicit Nonblocking aspect.]
---
Add to 13.11(15):
If the nominal subtype of the name specified for Storage_Pool is nonblocking (see 9.5), then the primitive Allocate, Deallocate, and Storage_Size subprograms of that type shall be nonblocking. Additionally, if the pool that is one that supports subpools (see 13.11.4), the primitive Default_Subpool_for_Pool, Allocate_From_Subpool, and Deallocate_Subpool subprograms shall be nonblocking.
AARM Reason: We need to be able to describe in contracts (especially for generic units) whether the operations of a storage pool allow blocking, and we do that with the nonblocking status of the type. We make the check when the pool is specified so we can avoid adding a special check to the declaration of a pool type - we want pool types to follow the same rules as any other type.
Add after 13.11(17):
The type(s) of the standard pool(s), and the primitive Allocate, Deallocate, and Storage_Size subprograms for the standard pool(s) are nonblocking.
AARM Reason: We need to specify that the type is nonblocking so that an instance of Unchecked_Deallocation is nonblocking if the object type is nonblocking (as the type is used in the contract). Ada 95 did not declare standard allocation/deallocation as potentially blocking, so these things can be used in protected types, and we want that to remain true (with static checking).
Add to the end of 13.11(18/4):
The type of P, and the primitive Allocate, Deallocate, and Storage_Size subprograms of P are nonblocking.
[This is talking about the implementation-defined pool used when Storage_Size is specified.]
---
Replace 13.11.2(3/5) with:
generic type Object(<>) is limited private; type Name is access Object; procedure Ada.Unchecked_Deallocation(X : in out Name) with Preelaborate, Nonblocking => Object'Nonblocking and Name'Storage_Pool'Nonblocking, Convention => Intrinsic;
!discussion
Note that Nonblocking is not used for elementary types. The finalization of elementary types has no effect; assignment of elementary types is trivial; and default initialization is always of a static value (or uninitialized). Thus, these things are always nonblocking for elementary types.
We have to ignore Nonblocking for elementary subtypes as whether a subtype is elementary is view-dependent (private types are always composite types); but the aspect Nonblocking is type-related (so the private view and full view have the same value).
We only need new rules in the case of checking generic bodies. In all other cases, we have rules about including implicit calls when checking Nonblocking, and that makes the needed checks (for all of default initialization, controlled finalization, controlled assignment, and storage pool usage via allocators and the Storage_Size attribute). In a generic specification, those checks are made by the legality recheck that occurs on instantiation based on the properties of the actual types.
We make the check on the subprograms for a storage pool when the pool is used, so that we don't need to invent a special rule for storage pool type declarations that would only be enforced for such types.
Note that the contract for Unchecked_Deallocate_Subpool always allows blocking. Unlike Unchecked_Deallocation, Unchecked_Deallocate_Subpool uses dispatching calls rather than generic parameters for deallocation, so neither the designated type(s) nor the pool type are known when it is called. So those cannot be described in the contract.
!corrigendum 9.5(17/3)
Insert after the paragraph:
In addition to the places where Legality Rules normally apply (see 12.3), these rules also apply in the private part of an instance of a generic unit.
the new paragraphs:
Just to force a conflict; the updated text will be found in the conflict file.
!corrigendum 13.11(15)
Replace the paragraph:
Storage_Size or Storage_Pool may be specified for a nonderived access-to-object type via an attribute_definition_clause; the name in a Storage_Pool clause shall denote a variable.
by:
Storage_Size or Storage_Pool may be specified for a nonderived access-to-object type via an attribute_definition_clause; the name in a Storage_Pool clause shall denote a variable. If the nominal subtype of the name specified for Storage_Pool is nonblocking (see 9.5), then the primitive Allocate, Deallocate, and Storage_Size subprograms of that type shall be nonblocking. Additionally, if the pool that is one that supports subpools (see 13.11.4), the primitive Default_Subpool_for_Pool, Allocate_From_Subpool, and Deallocate_Subpool subprograms shall be nonblocking.
!corrigendum 13.11(17)
Insert after the paragraph:
If Storage_Pool is not specified for a type defined by an access_to_object_definition, then the implementation chooses a standard storage pool for it in an implementation-defined manner. In this case, the exception Storage_Error is raised by an allocator if there is not enough storage. It is implementation defined whether or not the implementation provides user-accessible names for the standard pool type(s).
the new paragraph:
The type(s) of the standard pool(s), and the primitive Allocate, Deallocate, and Storage_Size subprograms for the standard pool(s) are nonblocking.
!corrigendum 13.11(18)
Replace the paragraph:
If Storage_Size is specified for an access type T, an implementation-defined pool P is used for the type. The Storage_Size of P is at least that requested, and the storage for P is reclaimed when the master containing the declaration of the access type is left. If the implementation cannot satisfy the request, Storage_Error is raised at the freezing point of type T. The storage pool P is used only for allocators returning type T or other access types specified to use T'Storage_Pool. Storage_Error is raised by an allocator returning such a type if the storage space of P is exhausted (additional memory is not allocated).
by:
If Storage_Size is specified for an access type T, an implementation-defined pool P is used for the type. The Storage_Size of P is at least that requested, and the storage for P is reclaimed when the master containing the declaration of the access type is left. If the implementation cannot satisfy the request, Storage_Error is raised at the freezing point of type T. The storage pool P is used only for allocators returning type T or other access types specified to use T'Storage_Pool. Storage_Error is raised by an allocator returning such a type if the storage space of P is exhausted (additional memory is not allocated). The type of P, and the primitive Allocate, Deallocate, and Storage_Size subprograms of P are nonblocking.
!corrigendum 13.11.2(3/3)
Replace the paragraph:
generic type Object(<>) is limited private; type Name is access Object; procedure Ada.Unchecked_Deallocation(X : in out Name) with Convention => Intrinsic; pragma Preelaborate(Ada.Unchecked_Deallocation);
by:
generic type Object(<>) is limited private; type Name is access Object; procedure Ada.Unchecked_Deallocation(X : in out Name) with Preelaborate, Nonblocking => Object'Nonblocking and Name'Storage_Pool'Nonblocking, Convention => Intrinsic;
!ASIS
None needed; only the definition and use of some properties have changed.
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix

From: Randy Brukardt
Sent: Friday, February 22, 2019  8:06 PM

> The automatic rule only applies to *non-generic* Pure 
> packages. I forget precisely why, ...

I remember now: the Nonblocking has to depend on the generic formals (if any),
lest we introduce an incompatibility. But that's not an issue for some formals
(elementary types, in particular, which are always nonblocking).

Unchecked_Conversion is a special case, in that the nonblocking of the actuals 
doesn't matter as the (virtual) body won't execute any of the operations that 
would require them to be followed.

Anyway, as with a lot of these things, it's more complex than it appears on 
the surface.

All of this is discussed (somewhat in code) in the !discussion of AI12-0241-1:

  Non-generic units that are pure are automatically nonblocking as specified in
  9.5 (these are noted below). Other units should explicitly have aspect
  Nonblocking specified if nonblocking is desired.

And Unchecked_Deallocation is wrong: if the type Object allows blocking, then 
Unchecked_Deallocation should, too. Thus, it should be:

generic
   type Object(<>) is limited private;
   type Name   is access  Object;
procedure Ada.Unchecked_Deallocation(X : in out Name)
   with Preelaborate, Nonblocking => Object'Nonblocking, Convention => Intrinsic;

That's because Unchecked_Deallocation finalizes an object, and if the Finalize 
routine is blocking, then the previous definition would have allowed a 
blocking operation in a nonblocking subprogram. (Which obviously would be 
silly.) Moreover, the *body* of Unchecked_Deallocation would be illegal if 
written in Ada, and since that probably isn't in Ada anyway, probably no one 
would have noticed it. But allowing blocking in a nonblocking subprogram is 
bad in any case. Must fix.

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

From: Randy Brukardt
Sent: Monday, March 11, 2019  2:24 PM

Steve asked how the assume-the-worst rule for Nonblocking works in a generic 
body for the storage pool of a formal access type. I wasn't able to give an 
immediate answer (other than an assurance that it was considered). Here's 
the real answer:

The intent is that the storage pool of a formal access type needs to be 
reflected in the contract of the generic. For instance:

   generic
       type Element is private;
       type Ptr is access Element;
   package Gen
       with Element'Nonblocking and Ptr'Storage_Pool'Nonblocking is

       procedure Save_It (E : in Element);

       ...
   end Gen;

   package body Gen is

       procedure Save_It (E : in Element) is
       begin
	     ... new Element'(E); 
       end Save_It;

       ...

   end Gen;

Save_It inherits the Nonblocking contract from the enclosing unit, so it also 
has a contract of Element'Nonblocking and Ptr'Storage_Pool'Nonblocking.

The allocator makes implicit calls to Finalize of Element (which is covered by 
Element'Nonblocking), and Allocate of the pool of Ptr (which is covered by 
Ptr'Storage_Pool'Nonblocking), so all is well.

The wording has always made it clear that implicit calls are handled the same 
way as explicit calls. For the assume-the-worst rules, I have two To Be Honest
notes which explain that the contract of Finalize (and Initialize [and default
init] and Adjust) is type'Nonblocking, and the contract of Allocate (and 
Storage_Size) is Ptr'Storage_Pool'Nonblocking. The assume-the-worst rules 
require that either the contract of the enclosing subprogram is statically 
False or that it contains the contract of any call that it contains. (Of 
course, if the needed contract is itself static (that is, doesn't depend on a 
formal type), then we just use the normal static check. See the rules for 
details.)

If Save_It had been declared

     procedure Save_It (E : in Element) with Nonblocking;

then the allocator makes the subprogram body illegal, because neither of the 
conditions of the assume-the-worst rule are satisfied (the contract is not 
statically False, and it does not contain Element'Nonblocking nor 
Ptr'Storage_Pool'Nonblocking).

So I'm pretty certain this is covered. There is a some handwaving about the 
desired contract (we want to use the most specific one possible, but defining
that precisely is difficult), but the rules do the right thing presuming you 
have the contract.

We probably will need some ACATS tests on this, and the containers will use 
some of it as well, so I expect compilers will do the right thing eventually
(might take a few iterations to get it right).

P.S. There are similar issues surrounding Global in these same cases. It 
definitely handles finalization properly, not sure about default 
initialization, and it probably needs some fixes for pools. That's a separate 
AI for some other time.

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

From: Tucker Taft
Sent: Monday, March 11, 2019  2:51 PM

> ...
> 
> The intent is that the storage pool of a formal access type needs to 
> be reflected in the contract of the generic. For instance:
> 
>   generic
>       type Element is private;
>       type Ptr is access Element;
>   package Gen
>       with Element'Nonblocking and Ptr'Storage_Pool'Nonblocking is

I suspect you mean:

     with Nonblocking => Element'Nonblocking and Ptr'Storage_Pool'Nonblocking ...

Otherwise, looks good.

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


Questions? Ask the ACAA Technical Agent