Version 1.3 of ai12s/ai12-0240-2.txt

Unformatted version of ai12s/ai12-0240-2.txt version 1.3
Other versions for file ai12s/ai12-0240-2.txt

!standard 3.10.3(0)          18-12-11 AI12-0240-2/02
!class Amendment 18-06-14
!status work item 18-06-14
!status received 18-06-14
!priority Low
!difficulty Hard
!subject Access ownership for Abstract Data Types
A new kind of access type, the fenced access type, is defined, which allows a more limited form of Global aspect for subprograms in which it is used.
Assuming that we have static tasking checks (AI12-0267-1), it is important that the Global aspects of abstract data types (ADTs) have as little conflicts as possible. In particular, the Global aspects of the containers need to have a very minimum use of global objects; otherwise, they could not be used in parallel blocks and loops when the static checks are on.
Many ADTs (including the normal unbounded containers and the indefinite containers) internally use access types and allocated data. This is necessary to provide memory efficiency and unbounded behavior -- statically sized structures necessarily have a defined bound and have to use the memory needed for the largest possible object.
Moreover, well-defined ADTs hide the implementation from the clients. Thus, the types of allocated objects are unknown to clients.
In normal use, allocated objects for a pool-specific type are considered to belong to the pool that they are allocated from; this typically is a shared global object. General access objects can be part of an associated pool or indeed any object in the entire program that has the correct type. In an ADT where the allocated type is not visible to the client, the only choice often is "in out all".
However, such objects are typically allocated so they belong to a single ADT object. If we could communicate this ownership to the compiler, the objects could be considered to belong to a particular object (typically a parameter to a subprogram, not subject to Global checks) rather than the storage pool that they were allocated from.
Add "fenced access types" to the language. We define the rules for such access types so that a fenced access value can belong to at most one ADT object at a time. A subset of fenced access types - ones with "managed" objects - take this a step further and enforce the ownership relationship with compile-time and run-time rules. As a side-effect, if the managed value belongs to no object, it can be automatically reclaimed.
We allow "unmanaged" fenced access types, which are unmanaged copies of fenced access types. They provide no ownership effects of their own; indeed it is considered erroreous to dereference such an access value if not directly in the scope of the appropriate ADT owner.
[Author's notes: Some of this wording isn't formal enough for the RM and will need to be improved.
We have this in the core, as it will be needed to support Global contracts and language defined containers so that they can pass the core checks for data races in parallel statements - see 9.10.1 (from AI12-0267-1 and AI12-0298-1).]
3.10.3 Fenced Access Types
An \fenced access type\ is a special variety of access type that adds some compile-time and runtime rules that combine to: * reduce erroneous execution by making it possible to eliminate dangling
references and storage leaks; and
* allow allocated objects to be treated as local for the purposes of Global
specifications even when they are allocated from a global pool.
Designated objects of a fenced access type are created and destroyed only via that type; they stay within the "fence" surrounding that type during their entire lifetime.
An fenced access type is declared by giving the aspect Fenced on the type declaration. This aspect includes a list of one or more /ultimate owner types/. Every object allocated for the fenced access type logically belongs to exactly one /ultimate owner object/ of one of the ultimate owner types; the ultimate owner object can be changed during the life of such an allocated object, but there always must be an ultimate owner object.
AARM Discussion: This ultimate owner relationship is purely virtual for a value of an fenced access type; the ultimate owner relationship is managed purely at compile-time. It is not necessary to make any runtime checks or use any extra storage to manage this relationship.
Each object of an fenced access type have a specific kind that specifies how management of the ultimate owner relationship is handled. These kinds can be split into two categories: \managed kinds\ and \unmanaged kinds\. A managed kind of access object is subject to a number of compile-time and runtime rules that prevent various kinds of errors, including dangling references and storage leaks. Allocations and deallocations only are allowed for managed kinds. In contrast, a unmanaged kind of object is only subject to the normal rules for access types; it is useful when separate reference abstractions are needed.
For most purposes, objects allocated for a fenced access type can be considered part of their ultimate owner object, rather than the pool from which they are allocated. This allows Global specifications to treat them as local objects (if, of course, the ultimate owner is local).
The Fenced access type is declared by the following aspect:
Fenced => (subtype_mark {, subtype_mark})
The subtype_marks specified for the aspect define the *ultimate owner types* for the fenced access types. These subtype_marks shall be first subtypes.
AARM Discussion: The ultimate owner types of a fenced access type are typically a public ADT. Other types can be the direct owner of a fenced access type object; these are usually (private) nodes of the data structure. For instance, consider a list container: there is a header structure which is used as the container itself, and individual nodes that make up the chain of elements.
AARM Reason: We allow multiple ultimate owner types so that multiple types can share node types if needed.
A fenced access type shall be:
* be a pool-specific type;
* declared in a private part or body;
* the ultimate owner types shall have their (full) declaration in the same declaration list as the owned access type;
* be either a tagged type or immutably limited.
[Author's note: These restrictions imply that these types are either private or completely hidden; they're only usable within the subsystem. It's not clear whether the private restriction actually helps, because of the possibility of child units that can see all of the declarations. Similarly, requiring the types in the same declaration list may not be necessary; in any case, it's easier to relax restrictions than to have too few. And these restrictions correspond to the typical organization of an ADT. The restrictions on the type are the same as those on direct owner types; they're just repeated here so that useless ultimate owner types can't be declared (every useful ultimate owner will eventually become a direct owner type as well).]
AARM Reason: The restriction to pool-specific types makes most conversions from other access types illegal, even if the designated types are the same.
The global specification of each ultimate owner type shall cover the Allocate and Deallocate operations of the type of the storage pool associated with the fenced access type.
AARM Reason: For clients, the allocation and deallocation of objects of the fenced access type should look like part of the operations for the ultimate owner type. Any global references caused by those operations need to be reflected in the use of the type. Deallocation will automatically happen during the finalization of the type; allocation most likely will occur during initialization of the object.
[Author's note: Is this enough? A deallocation can appear almost anywhere, as they're automatically called by assignment and finalization. OTOH, the 6.1.2 rule is very vague and can be construed to cover virtually anything. (There is an implicit call to Allocate and Deallocate in any explicitly written subprograms.) These obscure cases will almost certainly have to be tested by ACATS tests lest implementers be unaware of them.]
No type shall be derived from a fenced access type. A fenced access type shall only match a formal access type which is itself a fenced access type.
AARM Reason: The restriction on deriving the fenced access type is to eliminate complications caused by having multiple access types in these rules. There's no value to such types (they also have to be fenced types with the same pool, and thus would have the same restrictions).
AARM Ramification: A fenced access type cannot be used to instantiate Unchecked_Deallocation. This is OK, as assigning null into an owner kind object deallocates it automatically, and other kinds are not allowed to do any allocation or deallocation anyway.
The kind of an access object is defined with an aspect when the access object is declared (this includes components, stand-alone objects, and parameters). Redunant[There is no default kind for a fenced access type, the kind always needs to be specified.]
Allocators for a fenced access type are considered to have the Allocator kind.
For an access object that is of an fenced access type, or for a subtype of an fenced access type, the following aspects are defined:
Fencing_Kind Can be one of the identifier specific to an aspect Owner,
Reference, Borrower, or Observer. Specifies that the object has the specified kind.
Owner A boolean aspect, specifying this to True is the same as
Fencing_Kind => Owner.
Unmanaged A boolean aspect, specifying this to True is the same as
Fencing_Kind => Reference.
Borrower A boolean aspect, specifying this to True is the same as
Fencing_Kind => Borrower.
Observer A boolean aspect, specifying this to True is the same as
Fencing_Kind => Observer.
[Author's note: The short-hands are defined to keep object and component declarations from getting too wordy. Similarly, we allow defining subtypes so that common uses (mainly unmanaged objects) don't have to be repeated everywhere. My personal preference would be that Borrowers and Owners in particular are lways explicitly declared on the object -- there should be very few of these. There might be more References and Observers.]
For a parameter or generic formal of a fenced access type, the actual object shall be convertible to the kind of the parameter or formal.
[Author's note: This might follow from the subtype conversion rules below.]
For a subtype conversion to a fenced access type with an Owner kind, the source shall have an Owner or Allocator kind, or be a null literal.
For a subtype conversion to a fenced access type with an Unmanaged kind, the source shall not have an Allocator kind.
AARM Reason: All allocations are done into Owner kind objects.
[Note: Subtype conversion rules for Borrower and Observer go here. These aren't necessary for ADT usage and aren't defined here. We could remove them above for simplification.]
If the Fencing_Kind for an object is Owner, the object shall be a component of a type (called a direct owner type), or be a stand-alone object.
AARM Ramification: The object cannot be a parameter, a generic formal object, etc.
A direct owner type shall be a tagged type. No type shall be derived from a direct owner type.
AARM Reason: We want all direct owner types to be passed by reference, so that the complications of copies during parameter passing can be ignored. This rule applies to the full type, so the partial view of an ADT does ot necessarily have to be either of these.
AARM Implementation Note: Direct owner types could be implemented as a controlled type with compiler-generated Adjust/Finalize routines.
[Author's note: The owner type derivation part is mainly to keep my head from exploding trying to figure out the owner relationships in such cases. It should be OK in generics, as a tagged types can't be derived in a generic body, and the recheck would be good enough for a generic specification. But it might be possible to cover any cases (like formal derived types) that come up from allowing this derivation.]
If a direct owner type is nonlimited, the designated type of the fenced access type of the component shall be nonlimited.
AARM Reason: A non-limited type with limited nodes cannot be assigned usefully; that's because the limited nodes might contain tasks or protected objects that can't be copied. Since we consider this a single object for most rules, we have to ban this combination.
[Other rules for Borrower and Observer go here. These aren't necessary for ADT usage and aren't defined here.]
Langauage Design Principle
An owner kind access object is always the only owner of the owned object; it is never the case that more than one owner designates a single owned object.
AARM Ramification: This means that one cannot define circular structures or structures with multiple references (like a doubly-linked list) solely with owner access objects. It also means that there is a single path that reaches all of the nodes, so we can require deep copies.
For an assignment whose target is (directly) an owner kind access object, the source expression shall be only an allocator, another owner kind access variable (not a constant), or the literal null.
AARM Ramification: Other kinds of access objects for a fenced access types cannot be assigned into an owned access object.
Assigning a new value to an owner kind access object first deallocates the existing designated object (if any). If the new value comes from some other owner kind access object (rather than an allocator or literal null), that object is set to null.
AARM Ramification: We don't allow assigning from a constant as the source will be modified in that case.
[Author's note: We could allow assigning from a constant if its enclosing object is inherently mutable, but that is hard to define as a Legality Rule (inherently mutable is a rule that ignores privacy, which Legality Rules should not).]
Inside of a subprogram with one or more parameters of the ultimate owner type, the accessibility of the designated object of a fenced access value (including when stored in an unmanaged access object) is that of the parameter (as adjusted for "aliased" parameters). Otherwise, the accessibility level is infinite.
AARM Reason: This allows converting one of these access values to an anonymous access type when inside such a subprogram; otherwise, all conversions to other types are banned. This allows creating the anonymous access discriminant of a generalized reference.
AARM Ramification: Except as allowed above, a fenced access type cannot be converted to any other access type. This is regardless of the kind of the access object involved.
[Author's note: We use accessibility to prevent such conversions rather than trying to block them one at a time. There are many approaches to getting 'Access of a part of a designated object of a fenced access value.
For the anonymous access discriminant and anonymous access parameter cases, we want the accessibility of the designated objects to match that of the ultimate owner object - as they are considered "part" of the object rather like coextensions.
I suppose an alternative would be to consider them to directly be coextensions, then all of those rules which are obviously right ;-) could be used. But we wouldn't want the exact storage management rules for coextensions to apply.
End author's note.]
The assignment of a direct owner object of a nonlimited type includes duplication of each owner kind access component C with designated type D by setting the component of the target T to a newly allocated object assigned the designated object of the component of the source S.
T.C := new D'(S.C.all);
Adjust is called (if needed) after this assignment.
AARM Ramification: This is done recursively if the designated objects are themselves direct owner objects.
AARM Discussion: The designated objects can't be limited if the direct object is nonlimited, by rule above. This rule doesn't apply to limited type as those are always built-in-place when assigned, and thus no duplication is needed.
[Note to Tucker: After more thought, I've essentially decided that it is better that the compiler do a deep copy automatically. The owner rules ensure that is possible, and any other rule either requires erroneous execution, or weird exceptions to the normal rules, or other messes. Why not have the compiler do the right thing instead of having errors? Especially as the copy will be cleaned up automatically.]
The finalization of an owner kind access object deallocates the designated object, if any. This occurs after the call to Finalize, if any.
AARM Ramification: This can only happen for stand-alone (local) objects and as part of deallocation of a direct owner type.
A fenced access value V might belong to an object X if:
* a ultimate owner type of the type of V is the type of X; or
* a ultimate owner type of the type of V contains an owner kind access component whose type has an ultimate owner type which is the type of X;
* and so on recursively.
AARM Reason: This allows multiple fenced access types to be used in a single data structure, as might be needed to represent different parts of a data structure.
An owned access value V belongs to an object X if:
* V might belong to X; and
* The designated object of V is reachable from X by following owner access objects (usually components) as needed.
[Note: This is a dynamic definition, we don't expect to check it directly.]
In a subprogram with one or more parameters P of the ultimate owner type, execution is erroneous if a reference access object is dereferenced that does not belong to one of the parameters P.
[Author's note: This rule is annoying, but there is no static way to check it. Luckily, for the containers, such uses of a cursor are already erroneous (the cursor is "invalid"). Moreover, the preconditions for the containers check this property on cursors, so it will always be detected so long as the owner of a node is not changed (Move/Splice is not used).]
Notwithstanding what is said elsewhere, a dereference of an owned access value V (regardless of the kind of object it comes from) is considered covered by the Global contract needed to cover any object X that V might belong to.
AARM Reason: This allows a more restrictive contract than that which normally could be used -- in particular, this rule means that the storage pool of the owning access type is not considered.
AARM Discussion: If X is a parameter, then "Global => null" (that is, anything) is considered to cover the dereference; if X is some global object, then the contract needed to cover X is sufficient to cover the dereference.
[Note to Tucker: I didn't try to change these rules, I need to do other ARG work and this was my best shot anyway. I realize that you don't like this presentation, but I think you understand the idea is to make it clear to the programmer of an ADT what they need to do in order to avoid erroneous execution when giving a Global contract that does not cover the storage pool or designated objects of the nodes of the ADT. Perhaps you will have a far better idea.]
The basic idea is that for the client view and the ADT, any designated objects of the fenced access type are an integrated part of the ADT, and thus share the lifetime, Global status, and other properties with the ultimate owner object (the ADT object). The fact that access types, storage pools, and other minutia are involved is invisible, even through the Global contracts.
We call the overall types "fenced" to separate the concept of overall ownership from the detailed concept of ownership represented by the managed kinds. Moreover, the access type itself is not owned by anything; it is the designated objects of values of the type that have an ownership relationship.
Perhaps there is another name which is more appropriate. We chose "fenced" as the designated objects all live out their lives in an "enclosure"; the objects are created and destroyed for this access type, and there is no other way to create such an object (no conversions into a fenced access type are allowed). It's possible to create a short-lived reference to a part of a fenced object, but otherwise all operations occur inside the fence (that is, via dereferences of fenced objects.
This proposal shares several features with the "access value ownership and parameter aliasing" proposal. The aims of this proposal are much more limited than that proposal, since we are only trying to make it possible to build task-safe ADTs using allocated objects. In particular, we are not trying to prevent dangling references or allow general use of fenced access values. Some of those capabilities could be added to this proposal, but at the cost of substantial additional complication.
Note in particular that the design of the Ada.Containers packages require the possible creation of dangling pointers (inside of cursors). If we tried to eliminate all dangling cursors, we would have to put usage restrictions on cursors which would be highly incompatible with existing usages of the containers.
The Ada.Containers always include an access to the container in each cursor, so it is possible to check that the cursor belongs to the "current" container. Indeed, this check is mandated by all container operations, so erroneous dereference of an unsafe owned access value is essentially impossible unless the owner is changed to a different container object (only a few operations allow that). This latter case is already erroneous by the container rules. Thus, the new possibility of erroneous execution does not change the possibilities of erroneous execution for containers.
One goal of this proposal that is explicitly different than the AI12-0240-1 proposal is that we make an effort here to never have these rules have any consequence to the client of a package. In particular, the semantics of types that contain owned objects is identical to similar declarations that don't include owned objects. We never allow ownership semantics to "leak" out of the package, nor do we require declaration of ownership outside of the ADT.
To allow container operations to use "Global => null" (assuming an element type that is "Global => null"), we need at a minimum for allocated nodes:
Nodes need to be owned by a particular container, the one being operated on.
Nodes need to be able to moved from one container to another. In particular Vector.Move and List.Splice are operations that explicitly change the owner of nodes. Implicitly, we also want to be able to reuse nodes, which can be accomplished by having a global "free" list container, and then using Splice inside of Delete to move the deleted nodes to "free", Insert also using Splice to get nodes from "free". I don't think that eliminating Move and Splice would be a good idea (that would be at a minimum performance incompatible).
We need to be able to convert owned access values (or something contained in them) into an access discriminant to implement Reference/Constant_Reference.
We need to be able to have unchecked references in Cursor values; they have to be able to become dangling without causing some error (the error is using such a cursor).
For a linked list container, we might have declarations like the following in the private part:
type Node; type Node_Ptr is access Node
with Fenced => (List);
type Node is limited record Elem : Element_Type; Prev : Node_Ptr with Unmanaged; Next : Node_Ptr with Owner; end record;
type List is ... with record Head : Node_Ptr with Owner; ... end record;
(Note: List is the visible private type.)
The Prev component is NOT an owner object; it is used only for list traversal and does not have any effect on the lifetime of the objects.
If the implementation wanted to have a free list of nodes, it could declare the following (probably in a protected object; the protected type would have to be listed as a primary owner type):
Free_List : Node_Ptr with Owner := null;
Then assigning a Node_Ptr to this object would have the effect of changing the owner to the global protected object (dereferencing such a pointer would require Global to include this protected object).
[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.


Questions? Ask the ACAA Technical Agent