Version 1.3 of ai12s/ai12-0410-1.txt

Unformatted version of ai12s/ai12-0410-1.txt version 1.3
Other versions for file ai12s/ai12-0410-1.txt

!standard 9.5(55/5)          21-01-21 AI12-0410-1/02
!standard 13.11(17.1/5)
!standard H.4(23.2/5)
!standard H.4(23.4/5)
!standard H.7(4/5)
!standard H.7(7/5)
!class Amendment 20-12-03
!status Hold 11-1-3 21-01-20
!status work item 20-12-03
!status received 20-12-02
!priority Low
!difficulty Easy
!subject Storage Pool-related side effects
!summary
If the "No_Hidden_Indirect_Globals" restriction is in place, then an allocator or unchecked deallocation for a formal access type or an access type with a user-defined storage pool is considered an update to its storage pool, and the storage pool must be covered by the applicable global aspects.
!problem
There is no way currently to indicate in a generic whether or not an allocator or unchecked deallocation is performed on a formal access type A, even though such operations can have significant side effects on an object, namely the object A'Storage_Pool, which is not an explicit formal parameter. To better understand the possible side effects of a generic, it is important to understand whether there are any uses of the operations of the associated storage pool.
A separate more general issue is whether operations on a user-defined storage pool, or for that matter, on any object of a limited private type, are automatically synchronized thanks to underlying use of a task, a protected object, or one or more atomic variables. We leave that to a separate AI on that topic. We will focus here on how effects on storage pools are to be handled.
!proposal
If the "No_Hidden_Indirect_Globals" restriction is in place, then an allocator or unchecked deallocation for a formal access type or an access type with a user-defined storage pool is considered an update to its storage pool, and the storage pool must be covered by the applicable global aspects. In a separate AI, we will address the issue of whether the operations on a user-defined storage pool can safely be performed concurrently in separate threads, that is, whether the storage pool object is considered to be "synchronized." For the purposes of this AI, we presume that user-defined storage pools, and those of formal access types, are not known to be synchronized objects, and so such an update would not be covered by Global => in out synchronized, and instead would require "Global => in out all." On the other hand, "standard" storage pools are presumed to be synchronized, and further, there is no requirement to cover them at all if the access types are declared in the private part or body of a package.
For precision, a global_object_name may be an attribute reference to the Storage_Pool attribute of an access type. This would also be an Annex H feature. By specifying the storage pool object this way, you don't have to know whether or not the storage pool object of a formal access type is synchronized when writing the Global aspect.
!wording
Insert before 9.5(55/5):
For an access-to-object type that is nonblocking:
* its storage pool shall be a standard storage pool; or
* the Allocate, Deallocate, and Storage_Size operations on its storage pool shall be nonblocking.
Modify H.4(23.2/5):
No_Hidden_Indirect_Globals
When within a context where an applicable global aspect is neither Unspecified nor in out all, any execution within such a context does [neither]{none} of the following:
Modify H.4(23.4/5):
* Read (or return a readable reference to) a variable that is reachable via a sequence of zero or more dereferences of access-to-object values from a global that is not within the applicable global variable set, unless the initial dereference is of a part of a formal parameter or global that is visibly of an access-to-object type[.]{;
* Evaluate an allocator, invoke an instance of Unchecked_Deallocation, or evaluate the Storage_Size attribute, for an access type that is a formal access type, or whose storage pool is not a standard storage pool, unless the storage pool object of the access type is within the applicable global variable set for mode IN OUT for allocation or deallocation, or mode IN or IN OUT for the attribute reference;
* Evaluate an allocator for an access type with a standard storage pool, if the result is assigned to a part of a formal parameter, function result, or global that is visibly of an access type, unless the applicable global variable set for mode IN OUT includes all synchronized objects, or the storage pool object itself.}
Add after H.7(4/5):
An object_name used as a global_name may also be an attribute_reference for the Storage_Pool attribute, so long as the prefix resolves to statically denote an access-to-object subtype, including a formal access type.
Modify H.7(7/5):
The Global aspect for a subtype identifies the global variables that might be referenced during default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. {For a formal access-to-object subtype, or an access-to-object subtype whose storage pool is not a standard storage pool, the Global aspect identifies the global variables (other than the storage pool itself) that might be referenced by a call on Allocate, Deallocate, or Storage_Size for the storage pool type.} ... [the rest is unchanged]
!discussion
As explained in the !problem, side effects on storage pools can be significant. This AI attempts to address this. We only enforce checks on storage pools if the restriction No_Hidden_Indirect_Globals is present, since without that restriction the use of access types is not necessarily reflected at all within global aspects.
We leave to a separate AI the more general issue of whether concurrent allocators on a user-defined storage pool are safe, and more generally, whether concurrent operations on an object of a limited private type can be assumed to be safe.
For standard storage pools, we don't worry about deallocation or Storage_Size, as they are not presumed to have any interesting side effects. We worry about allocation because if we were to write "Global => null" for a function that returns the result of an allocator, it might imply that it returns the same result on each invocation, which is clearly not the case. We don't worry about subprograms whose outputs don't include any parts that are visibly of an access type, to be consistent with the model that such "hidden" access types are presumed to be "well behaved". Clearly such an assumption is not always true, but we choose to follow this assumption consistently for the purposes of the Global aspect. Presuming they are "well behaved" then one would expect, for example, an equality operator over two "compound" objects involving hidden levels of indirection would follow those levels of indirection rather than having the equality depend on the particular values of the internal access values.
!example
type A is access Integer; type B is access Integer; for B'Storage_Pool use My_Cool_Storage_Pool;
function New_A (X : Integer) return A with Global => in out synchronized;
function New_B (Y : Integer) return B with Global => in out all; -- "in out synchronized" would not cover B'Storage_Pool -- since it is (presumably) not a standard storage pool
function Another_New_B (Z : Integer) return B with Global => in out B'Storage_Pool;
!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 Storage_Pools are included in the global as needed (or the code is rejected if not).
!appendix

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


Questions? Ask the ACAA Technical Agent