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

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

!standard 13.11.2(3/5)          19-03-06 AI12-0319-1/02
!class Amendment 19-02-22
!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(69/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 each default initialization expression 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 is 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, then the primitive Allocate, Deallocate, and Storage_Size subprograms of that type shall be nonblocking. Additionally, if the pool that supports subpools (see 13.11.4), the primitive Default_Subpool_for_Pool, Allocate_From_Subpool, and Deallocate_Subpool subprogram shall be nonblocking.
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 (if at all). 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 type 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, and storage pool usage). 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.
!ASIS
[Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.]
!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.

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


Questions? Ask the ACAA Technical Agent