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

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

!standard 6.1.3(0)          19-03-07 AI12-0240-5/02
!class Amendment 19-01-10
!status work item 19-01-10
!status received 19-01-10
!priority Low
!difficulty Hard
!subject Heap object ownership for Abstract Data Types
!summary
We introduce the notion of "ownership" of heap objects to allow us to define the "Global" aspects of the visible operations of an abstract data type, without being concerned with appropriately-managed internal uses of access types. This also simplifies the determination of aliasing between pointer-based names, which enables more sophisticated static analysis. We allow an access object to specify its "Owner" which means that the object it designates is treated as though it is a part of the Owner object, rather than being an independent heap object. We allow a function to specify the Owner of its result (access) object, or in the case of a return object with an access discriminant, the Owner of the access discriminant.
!problem
Assuming that we have some sort of data-race checks (AI12-0267-1), it is important that the Global aspects of abstract data type (ADT) operations introduce as few conflicts as possible. In particular, the Global aspects of the container operations need to imply a minimal use of shared variables. Otherwise, they could not be used safely in any sort of multi-threaded situation.
Currently, the only way to describe the dereferencing of an access object in the context of a Global aspect is by the "X.all", "access T", or "<package_name>" forms of specification. The latter two of these will tend to lump together all objects of the same container type, when in fact two distinct objects of a container type almost certainly share no storage. We believe we need some better way to define the global side effects of ADT operations which reflects the true amount of data sharing, or lack thereof, between objects of an ADT that uses pointers internally.
Beyond concerns about data races, more general concerns about "aliasing" (that is, might two different names actually denote the same object at run time) are also relevant to almost any sort of static analysis. Pointers make the determination of possible aliasing much more difficult. It would be very valuable to adopt some approach to "taming" pointers so that aliasing can be more precisely determined, even in the presence of pointer-based data structures.
!proposal
Handling pointer dereferences has always been a challenge for formal analysis, with approaches such as "separation logic" generally requiring more formalism than would be appropriate even for a skilled programmer. The concept of "pointer ownership" or "object ownership" represents a simpler alternative approach, and reflects a typical way in which most pointers are actually used in the implementation of many ADTs. With "ownership" we are able to treat an independent heap object as though it is actually a subcomponent of some other object, where its "owning" pointer resides. Although there might be other pointers designating the heap object under certain circumstances, these other pointers are recognized as being "secondary" references, which can be managed in a way to reduce the chance that such secondary references are dereferenced after the "owning" pointer is set to null. This sort of ownership makes data race detection and aliasing determination much more straightforward when dealing with pointer-based data structures.
We propose to allow an access object to specify that the object it designates is to be treated as a part of an Owner object. It can specify this with an Owner aspect specification at the point where the object (or component) is declared. Further, a function that has an access result, or a result with an access discriminant, can specify with the Owner aspect the parameter or global with which it shares an owner. If the Owner of a function result is specified as the Result attribute of the function itself, then this indicates a new object is being returned, and the caller takes over ownership by assigning the result of the call.
We also propose to generalize the "X.all" form of Global specification to be usable when X is of a private type, to signify that the subprogram might dereference some subcomponent of X, for the specified mode of access (in, in out, or out). This is particularly useful for specifying the effect of an operation like Text_IO.Put, where the File_Type parameter is of mode IN, but clearly there are side-effects on the underlying internal file object. Hence for Text_IO.Put, you could say "Global => in out File.all" even though File is of a private type. Ownership doesn't really work very well for this, since the fact that File is mode IN would prevent updating anything owned by File.
An object or component that is of an access type can specify the Owner object with the aspect specification "Owner => /object_/name", where in the case of a component, /object_/name denotes the current instance of the enclosing type, or in the case of a stand-alone object, /object_/name denotes some visible object (including itself). In either case, the object_/name must denote an object of a controlled or immutably limited type, or it can designate the object itself (in the stand-alone case), in which case it effectively owns "itself."
Similarly, a function that returns an access object, or returns an object with a single access discriminant, can specify the formal parameter or object global to the function that owns the result, or it can specify that the Owner is the Result attribute of the function, which signifies that the returned value is a "root" access value, and is not owned by any other object at the moment of the function return.
In addition to root access values (more on those a bit later), there are "primary" and "secondary" access objects. Primary access objects are components with a specified Owner, or stand-alone objects that specify themselves as their Owner. Secondary access objects are stand-alone objects that specify some other object as their Owner. A special case for a secondary reference is what we call a "back" reference, an access object that points from an owned object back to one of its owners. The "prev" link in a doubly-linked list, or the "parent" pointer in a multi-way tree, are examples of such "back" references.
As far as the Global aspect is concerned, so long as an access object has an Owner, a dereference of the access object is treated as though it is referencing the Owner. If the Owner is read-only, then the access object can only be used to read the object it designates, except in the case where X.all is specified as mode out or in out in the Global aspect, and X is (or owns) the access object being dereferenced.
If the specified Owner of an access object is a variable, then read/write access is permitted via the access object to the object it designates (presuming of course the access object is itself access-to-variable).
We provide an attribute Y'Move where Y is a primary access object. It returns the original value of Y, and then sets Y to null, to ensure that only a single primary access object designates a given heap object at a time. Before Y'Move, Y.all is owned by Y's Owner. Y'Move effectively breaks this connection by setting Y to null, allowing the designated object to be adopted by a new Owner as part of the "move." Y'Move is one of the ways to create a "root" access value, which is what may then be assigned into another "primary" access object. Allocators and the null literal also produce root access values, as does a call on a function that specifies its Result attribute as its owner (as mentioned above).
Compile-time and run-time checks are proposed to ensure that secondary access objects always designate an object owned by their specified Owner. These checks are not foolproof because an update to a primary access object could invalidate this property. We anticipate in a later revision of Ada (currently being prototyped in the SPARK subset) we could add more rules to prevent this problem, by disallowing modifications to certain primary access objects while a secondary access object exists, but for now we simply declare a dereference of a secondary access object after such an invalidating change as "erroneous."
We have deferred to a future Ada revision automatic storage reclamation when a primary access object is set to null without a Move. We have also deferred to a later revision any attempt to prevent aliasing. Again, aspects of both of these sorts of rules are being prototyped in the SPARK subset. In this version, we presume controlled types will continue to be used to accomplish automatic storage reclamation. We have also kept certain compile-time and run-time checks relatively simple and strict to ease implementation. We could imagine in a future Ada revision, usage patterns might argue for more flexible checks.
!wording
Modify 6.1.1(29/5):
F'Result
Within a postcondition expression for F, denotes the return object of the function call for which the postcondition expression is evaluated. {When specified as the Owner aspect for F, indicates that the function returns a root access value (see 6.1.3).} The type of this attribute is that of the ...
Add after 6.1.2(32/5):
* /object_/name.all where /object_/name denotes an object of an access-to-object type or a composite type, identifies the object(s) designated by any access-to-object-type part(s) of the named object;
Add after 6.1.2(35/5)
In addition, whenever a given object is within a global variable set, all objects owned (see 6.1.3) (directly or indirectly) by the object are within the global variable set.
Add the following subclause:
6.1.3 Object Ownership
This section describes the Owner aspect, which can be used to indicate cases where an object created by an allocator is to be considered /owned/ by another object, meaning that the owner, or some subcomponent of the owner, designates the allocated object, and is the only such object that designates it. [Redundant: For the purposes of identifying Global effects (see 6.1.2) of an operation, reads or updates of the designated object are handled like reads or updates of a subcomponent of the owner object, rather than as reads or updates performed via an access value.]
AARM Language Design Principles:
We distinguish access objects participating in ownership as being "primary" access objects, "secondary" access objects, and "backward" access components. The ownership legality rules and run-time checks, below are designed to accomplish three goals:
1. Ensure that at most one "primary" access object designates a given object at any time.
2. Ensure that a "secondary" access object always designates an object owned (directly or indirectly) by its specified Owner (or if the Owner is itself a secondary access object, by the object designated by the Owner).
3. Ensure that "backward" access components, such as "Prev" or "Parent" pointers, always designate an object that owns (directly or indirectly) their enclosing composite object.
The first goal is relatively easy to accomplish, because we allow a primary access object to be assigned only "root" access values, where a root access value is defined to be an access valut that designates (if nonnull) an object that is not currently designated by any other primary access object. Root access values include things like allocators, the null literal, and the result of the 'Move attribute (see below).
The second goal involves both compile-time checks and run-time checks, but is not bullet proof because we allow primary access objects to be altered while secondary access objects exist. We considered disallowing alterations to primary access objects that might affect the validity of the secondary access objects, but went with a simpler set of checks which we believe will catch the majority of cases.
The third goal is also relatively straightforward to accomplish, though it also relies on run-time checks, and is also subject to some limitations, but again, we believe has the right balance between safety and implementability.
Static Semantics
The following aspect may be specified for an object (including a component) that is of an access-to-object type. It may also be specified for a record type, a record extension, an array type, or an array object of an anonymous array type, presuming it has one or more components of an access-to-object type. Finally, it may be specified for a function with a result that is of an access-to-object type, or is of a type with exactly one access discriminant of an access-to-object type:
Owner
The Owner aspect is an /object_/name, and shall denote the object being declared, the current instance of the type being declared, a component of the type being declared, the current instance of the enclosing type, a discriminant of the enclosing type, a formal parameter of the function being declared, the Result attribute of the function being declared, or a pre-existing object.
The effect of specifying an object as an Owner is determined by the nature of the denoted object:
* if the denoted object is the access object being declared, that object is defined to own the object it designates (if any);
AARM Reason: This is used to create the root pointer of some ownership-based data structure, such as a free list.
* if the denoted object is a current instance of a composite type, an object of the composite type is defined to /own/ the object(s) designated by the access-to-object components to which the aspect applies;
AARM Reason: This is the most common case, where a component that is of an access-to-object type indicates that the object it designates is owned by the enclosing composite object.
* if the denoted object is a component of (the current instance of) the type being declared, the component is considered a /backward access component/, and when nonnull, is presumed to designate an object that owns (directly or indirectly) the object enclosing the component;
AARM Reason: This is used for identifying the "back pointer" in a structure like a doubly-linked list, or a tree with parent pointers in some or all nodes.
* if the denoted object is a discriminant of the enclosing type, the object designated by the component to which the aspect applied is owned by the object designated by the discriminant;
AARM Reason: This case is used to identify via a discriminant the container with which something like a Cursor is associated.
* if the denoted object is a formal parameter of the function being declared, any object designated by the result of the function (or the access discriminant of the result) is owned by the object referenced or designated by the corresponding actual parameter;
AARM Reason: This kind of function is used to "select" an element of a container and return a reference to it, where the element is known to be owned by the container passed as a parameter.
* if the denoted object is the Result attribute of the function being declared, the function returns a /root access value/ (see below) designating an object (if any) that is not owned by any other object;
AARM Reason: This kind of function is used to create and return a new heap object, or to remove a node from one container and return it, making it available for insertion into a different container.
* if the denoted object is a pre-existing object, and the entity being declared is an object or component of an access-to-object type, the denoted object owns the object (if any) designated by the access object being declared; if the entity being declared is an array object (or an array type), any objects designated by components of the object (or components of any object of the type) are owned by the denoted object.
AARM Reason: This case is used when we want to create secondary references, that are known to point somewhere within a pre-existing container (which might be identified by a formal parameter of the enclosing subprogram).
In addition to ownership established by the Owner aspect, any composite object is defined to /own/ its subcomponents, and to own (indirectly) anything that is owned (directly or indirectly) by one of the objects that it owns directly.
Notwithstanding what this International Standard says elsewhere, the dereference of an access-to-variable object with a specified Owner aspect denotes a constant view if the Owner of the access object is a constant (or an access-to-constant) object, except when there is a Global aspect specification of the form "[in] out X.all" where the access-to-variable object being dereferenced is a part of the object denoted by X.
AARM Reason: This special exception is useful for cases like Text_IO or Discrete_Random, where the formal parameter is of mode IN, but clearly the operation is updating the data structure identified by the formal parameter.
An object of an access type with a specified Owner is either a /primary access object/, meaning it holds the sole (primary) reference to the object it designates (if any), or a /secondary access object/, meaning it holds a (secondary) reference to the object it designates (if any), and there is some other (primary) access object designating it as well.
An access object with a specified Owner is a /primary access object/ in the following cases:
* it is a stand-alone object that specifies itself as the Owner;
* it is a component where the current instance of the enclosing type is specified as the Owner;
* it is the return object for a function that specifies its Result attribute as the Owner.
AARM Ramification: At the call site, note that no 'Move is required to turn the return object into a root access value (see below).
Otherwise, an access object with a specified Owner is a /secondary access object/, including the case of the return object for a function that specifies one of its parameters as Owner.
AARM Ramification: The return object is considered a secondary access object both within the return statement, and at the call site, where it represents the result of the call.
The following attribute is defined for a prefix X that denotes a variable of an access-to-object type that is a primary access object:
X'Move
X'Move saves a copy of the value of X, sets X to the null value, and then returns the saved value. The result of X'Move is a /root access value/, which signifies that the object it designates (if any) is not designated by any other primary access object, and it can be assigned to another primary access object, without having two such access objects designating the same object.
The result of an allocator is also a root access value, as is the result of the null literal or the result of a call on a function that specifies its Result attribute as its Owner. The result of a raise_expression is also considered to be a root access value.
AARM Reason: Root access values are the only kinds of values that can be assigned to a primary access object, since they are known to designate "free-floating" objects, not currently owned by any other object.
Legality Rules
When specifying the Owner aspect:
* if the denoted object is the current instance of a composite type, the composite type shall be controlled, or else any partial view, parent, or progenitor of the composite type shall be limited;
AARM Reason: This prevents nonlimited private types from containing primary access objects, unless they are controlled. It also prevents nonlimited extensions from adding components that are primary access objects. The predefined assignment operation (including class-wide assignment) does not do the "right thing" for types with primary access components, so we want only limited types, controlled types, or non-extension visible types to contain them.
* if the denoted object is a component of the type being declared, or a discriminant of the enclosing type, the denoted object shall be of an access-to-object type;
AARM Reason: In these two special cases, the denoted object is not itself an owner, but rather designates the owning object. The first case corresponds to identifying a backward access object, while the second case corresponds to identifying the container with which something like a Cursor is associated.
* if the denoted object is a formal parameter of the function being declared, the formal parameter shall be of a composite type, or be an IN parameter of an access-to-object type;
AARM Reason: We don't allow [IN] OUT parameters of an access type to be specified as Owner of the return object of a function, because the rules for the copy-in-out parameter passing to such formal parameters would get quite complex. On the other hand, [IN] OUT parameters of a composite type that contain a primary access object are always passed by reference, so no special rules are needed for parameter passing in such a case.
* if the denoted object is a pre-existing object, the entity being declared shall be an object (including a component) having an access-to-object type, or shall be an array object or array type [Redundant: whose components are of an access-to-object type].
AARM Reason: This is the way secondary access objects are declared.
In an assignment operation:
* if the target is a primary access object, each basic constituent (see 4.4) of the source of the assignment shall produce a root access value;
* if the target is a composite object with any subcomponents of its nominal type being primary access objects, each basic constituent of the source of the assignment shall be newly constructed (see 4.4).
AARM Reason: The above are the critical legality rules for goal (1) above of the Language Design Principles. These are intended to preserve the unique ownership property for primary access objects. Basically, we are requiring the use of an allocator or 'Move rather than directly copying an existing access object. In the case of composite assignment, we are requiring the use of an aggregate, or a function call that ultimately must originate from an aggregate. In other words, you have to move or "reconstruct" an object when assigning, if ownership is involved.
* if the target is a secondary access object other than a component, each basic constituent name or expression (see 4.4) of the source of the assignment shall be the literal NULL, a raise_expression, or be owned by the object specified as the Owner of the target. For the purposes of this check, a name, expression, or prefix (called a /designator/ below) is /owned by an object/ if one of the following apply:
* the designator statically denotes the object;
* the designator denotes a secondary access object whose Owner specification is an /object_/name that is owned by the object.
* the designator is a dereference (explicit or implicit) of a primary or secondary access object, or a backward access component, and the prefix of the dereference is owned by the object;
* the designator is a selected or indexed name, and its prefix (after any implicit dereference) is owned by the object; or
* the designator denotes a renaming declaration, and the /object_/name of the renaming is owned by the object.
AARM Reason: The above are the critical legality rules for goal (2) above of the Language Design Principles. These are intended to preserve the property that a secondary access object designates an object owned by its specified Owner. As indicated below under Erroneous Execution, these rules are not foolproof since we currently don't limit what changes can be made to primary access objects after a secondary access object is initialized.
Dynamic Semantics
In an assignment operation to a secondary access object, if either the target or a basic constituent of the source is a component that is a secondary access object [Redundant: (meaning a discriminant has been specified as its Owner)], a run-time check is performed if the value being assigned is nonnull, to verify that the /owner object/ is the same (that is, has the same address) for the basic constituent of the source and the target access object; /owner object/ for an access object is defined as follows:
* if the access object is a component that is a secondary access object with a discriminant as its specified Owner, the owner object is the object designated by this discriminant, or if the discriminant is null, a notional object whose address is considered to be System.Null_Address;
AARM Reason: If the Owner is a discriminant, the run-time value of the discriminant designates the "owner object."
* if the access object is a component that is a primary access object or a backward access component, and the enclosing object is denoted by a dereference of an access object (or is a subcomponent thereof), the owner object is that of the access object denoted by the prefix of the dereference;
AARM Reason: If the access object is a component whose Owner is not a discriminant, the owner object of the component is determined by the access object that designates an enclosing composite object.
* otherwise, the owner object is the specified Owner of the access object.
If the owner objects do not have the same address, Program_Error is raised.
AARM Ramification: When assigning to a secondary access object and either the target or the source is a component that is not a primary access object, the owner objects must match exactly.
In an assignment operation to a backward access component B that is a component of a composite object X, a check is made that the new value of B, if nonnull, either:
* designates a composite object that has a component that is a primary access object that designates X; or
* matches the value of the backward access component of the composite object designated by the old value of B (which also requires the old value of B to be nonnull).
If this check fails, Program_Error is raised.
AARM Reason: The above check addresses goal (3) of the Language Design Principles, by ensuring that the backward access component points to an object that points back to it, or is a copy of a backward access component from the priar target of the backward access component (which could happen during a restructuring).
Bounded (Run-Time) Errors
If a controlled type has any subcomponent that is a primary access object, it is a bounded error if the Adjust procedure for the type does not update the value of each such subcomponent that has a nonnull value. The possible consequences are that Program_Error is raised prior to return from the Adjust procedure, or two primary access objects might designate the same object after assignment.
Erroneous Execution
The dereference of a primary access object is erroneous if it designates an object that is also designated by some other primary access object[Redundant:, due to inadequate updates performed by an Adjust procedure as part of an assignment to a controlled object].
AARM Reason: The result of an "inadequate" Adjust procedure does not become erroneous until one of the primary access objects is dereferenced.
The dereference of a secondary access object is erroneous if the object designated by the access object is not owned by the object specified as (or designated by) the Owner of the access object. [Redundant: This can happen as a result of an update to a primary access object that thereby changes the ownership hierarchy.]
AARM Note: Here is an example of how this might occur:
Sec : access Integer := Obj.Prim with Owner => Obj; ... Another_Obj.Prim := Obj.Prim'Move; Sec.all := 42; -- Erroneous, since Sec.all is no longer owned by Obj.
--------- End of 6.1.3 Object Ownership subclause
Add after RM 6.2(7/3):
* a composite type whose current instance is specified as an Owner (see 6.1.3);
Add after RM 11.5(16)
Ownership_Check
Check that in an assignment to or from a secondary access object that is a component, the owner objects match. Also, check that in an assignment to a backward access component, the new value designates an object that owns the enclosing composite object.
!discussion
We originally proposed a more complex model. We have tried to reduce this down to the minimum that still allows the Global aspect to be more precise on abstract data types (ADTs) such as the language-defined Container types. We originally proposed to support some degree of automatic reclamation, deep copying, and automatic streaming of ownership-based access types, as well as anti-aliasing checks. We still think all of that would be useful at some point, but we have decided that for now, we will focus strictly on allowing for reasonable Global aspects on ADT operations.
We provide the Owner aspect, to specify ownership when declaring access objects or components, and to specify ownership relationships established as a result of invoking some function.
We provide the Move attribute and other rules to ensure that two primary access objects never designate the same object. We enforce rules on assignment to secondary access objects to ensure they designate an object owned by their specified Owner, mostly at compile time, but in a special case at run time. We also enforce rules associated with "backward" access components of a given composite object to ensure they always point (backward) to an object that owns the given object.
In earlier versions of this AI we defined "borrower" and "observer" roles for such secondary access objects, and disallowed certain other changes to occur while they existed, but we have concluded that this was probably too elaborate of a design for the Ada 2020 revision, and these additional rules relating to borrowing and observing should be prototyped (in fact, are already being prototyped in the context of the SPARK 2014 language) before being adopted in the Ada standard. So we went with a simpler set of rules, that admittedly have some holes, but which we believe will nevertheless be sufficient to catch typical problems and are compatible with future more elaborate rules.
We require that composite types that are specified as an Owner be passed by reference, to minimize problems that might occur when primary access objects are updated and then an exception is raised. In such a circumstance, if a composite object with a primary access object component had been passed by copy, the exclusive ownership property might be compromised. We also require private types to be limited or controlled if they have any components that are primary access objects, because the predefined assignment does not do the right thing. In the controlled case, we expect the Adjust procedure to update all of the primary access objects, but we do not at this point enforce that as doing so was felt to be too difficult to specify and implement. Instead we make it a bounded error.
We considered allowing [in] out formal parameters of an access type to be used as a way to update actual primary access objects, but the rules became too complex, so we limited updates to primary access objects to assignment operations where the source is known to be a root access value.
!example
For a singly linked list type, we might have declarations like the following in the private part:
type Node; type Node_Ptr is access Node;
type Node is limited record
Elem : Element_Type; Next : Node_Ptr with Owner => Node;
end record;
type List is ... with record Head : Node_Ptr with Owner => List; ... end record;
(Note: List is the visible private type.)
If the implementation wanted to have a free list of nodes, it could declare the following (probably as a component of a protected object):
Free_List : Node_Ptr with Owner => Prot_Obj;
Then moving a Node_Ptr to this object would have the effect of changing the owner to be the global protected object (dereferencing such a pointer would require Global to include this protected object).
With the above Owner specifications, it is possible to walk the linked list in some operation on a List object, without having to mention in the Global aspect for the operation, any of the dereferences involved in the walk, so long as the root of the linked list is covered either as a parameter or as a declared Global.
See below the Hashed_Maps example for an example of a doubly-linked list.
---
Here is a more complete example of a hashed map package:
generic ... package Hashed_Maps is -- Here we show a typical hashed Map, and various operations whose -- Global aspects take advantage of object ownership
type Map is private with ...;
type Cursor is private;
... procedure Insert (Container : in out Map; Key : Key_Type; Element : Element_Type) -- Inserts an element with the given Key into the map with Global => Key_Type'Global & Element_Type'Global; -- We have to allow for global side-effects of copying Key -- and Element, but we don't have to mention dereferencing -- ownership-based pointers that occur within the Container.
function Find (Container : Map; Key : Key_Type) return Cursor -- Returns a cursor identifying the element associated with the Key with Global => null; -- despite internal access value derefs
function Element (Container : Map; Position : Cursor) return Element_Type -- Takes a Cursor and the map and returns the contents of the element -- at that cursor. with Global => Element_Type'Global; -- We have to allow for global side-effects of copying an -- Element, but we don't have to mention dereferencing -- ownership-based pointers that occur within the Container.
type Reference_Type (Element : not null access Element_Type) is private with Implicit_Dereference => Element;
function Reference (Container : aliased in out Map; Key : Key_Type) return Reference_Type -- Returns a reference to the element associated with the given Key -- allowing it to be updated upon return. with Global => null, Owner => Container; -- The object designated by the returned value is owned, -- directly or indirectly, by the Container.
... private type Node; type Node_Ptr is access Node;
type Node is limited record Key : Key_Type; Element : aliased Element_Type; Next : Node_Ptr with Owner => Node; -- This is how we indicate that Next is a primary access object end record;
type Table is array(Natural range <>) of Node_Ptr with Owner => Table; -- This is how we indicate that objects designated by -- the components of a Table are owned by the table.
type Table_Ptr is access Table;
Initial_Size : constant := 19; -- a modest-sized prime number
type Map is new Finalization.Controlled with record Backbone : Table_Ptr := new Table(0 .. Initial_Size - 1) with Owner => Map; -- This is how we indicate that the table designated by -- the Backbone is owned by the enclosing Map object. Count : Natural := 0; end record;
type Map_Const_Ptr is access constant Map; -- Values of this type are used to identify the container -- associated with a given Cursor.
type Cursor (Container : Map_Const_Ptr := null) is record Node : Node_Ptr with Owner => Container; -- This component is a secondary access object -- because it specifies a discriminant as its Owner -- (which means that Container.all is its "owner object"). end record;
type Reference_Type (Element : not null access Element_Type) is null record with Implicit_Dereference => Element;
...
end Hashed_Maps;
package body Hashed_Maps is
... procedure Insert (Container : in out Map; Key : Key_Type; Element : Element_Type) is -- Inserts an element with the given Key into the map Index : Natural := Hash (Key) mod Container.Backbone'Length; First : Node_Ptr renames Container.Backbone (Index); -- rename of primary access object -- known at compile-time to be owned by Container. begin if First /= null then declare Walker : Node_Ptr := First -- secondary access obj, with Owner => Container; -- compile-time check that initializing -- expression "First" is owned by Container. begin while Walker /= null loop if Walker.Key = Key then -- Replace Walker.Element := Element; return; -- All done end if; Walker := Walker.Next; -- compile-time check that Walker.Next -- is owned by Container. end loop; end; end if; -- Insert at head of chain First := new Node'(Key => Key, Element => Element, Next => First'Move); -- Next component is initialized by root access value (First'Move) -- New value of First is also a root access value (an allocator) Container.Count := @ + 1; end Insert;
function Find (Container : Map; Key : Key_Type) return Cursor is -- Returns a cursor identifying the element associated with the Key Index : Natural := Hash (Key) mod Container.Backbone'Length; Waklker : Node_Ptr := Container.Backbone (Index) with Owner => Container; -- Secondary access object; -- compile-time check that initial expression is owned by Container begin while Walker /= null loop if Walker.Key = Key then -- Found it return Cursor '(Container => Container'Unchecked_Access, Node => Walker); -- Run-time check that expression initializing -- the Node component (i.e. Walker) is owned -- by object designated by Container discriminant -- (i.e. Container'Unchecked_Access.all). end if; Walker := Walker.Next; -- Compile-time check that new value of Walker (Walker.Next) is -- owned by Owner of Walker. end loop; return Cursor '(Container => Container'Unchecked_Access, Node => null); end Find;
function Element (Container : Map; Position : Cursor) return Element_Type -- Takes a Cursor and the map and returns the contents of the element -- at that cursor. pragma Assert (Position.Container = Container'Unchecked_Access); -- Make sure the cursor matches the map Node : constant Node_Ptr := Position.Node with Owner => Container; -- Run-time check here to verify that the owner object of -- Position.Node (i.e. Positional.Container.all) -- is the same object as Container (note that we already -- checked this via the explicit Assert above). -- Because Node has an Owner, we can dereference -- it without having to include "access Map" in the Global -- aspect. Referring to Node.all is equivalent to referring -- to some part of Container (its Owner). -- Because the Owner is read-only (it is an IN param), -- Node.all is effectively read-only as well. begin return Node.Element; -- dereference of Node need not be mentioned in Global aspect -- thanks to ownership. end Element;
function Reference (Container : aliased in out Map; Key : Key_Type) return Reference_Type is -- Returns a reference to the element associated with the given Key -- allowing it to be updated upon return. -- The object designated by the returned value is owned, -- directly or indirectly, by the Container. -- NOTE: This creates a default-initialized element indexed by Key -- if such an element doesn't exist (unlike the standard Ada -- Map containers). Hence "Map[Key] := X;" can have the effect -- of expanding the Map if Map[Key] doesn't already exist.
Index : Natural := Hash (Key) mod Container.Backbone'Length; First : Node_Ptr renames Container.Backbone (Index); begin if First /= null then declare Walker : Node_Ptr := First with Owner => Container; begin while Walker /= null loop if Walker.Key = Key then -- Found it return Reference_Type'(Element => Walker.Element'access); end if; Walker := Walker.Next; end loop; end; end if; -- Insert a default-init'ed element at head of chain First := new Node'(Key => Key, Element => <>, Next => First'Move); -- We use 'Move to produce a root access value to initialize -- the Next component in the newly created Node. -- Note that the semantics of 'Move are that the value is -- returned after nulling out the object denoted by the prefix. Container.Count := @ + 1;
-- Return a reference to the default-init'ed element return Reference_Type'(Element => First.Element'access); end Reference; end Hashed_Maps;
---
Here is an example of a doubly-linked list, using a "backward access component" (Prev):
type Node; type Node_Ptr is access Node;
type Node is limited record
Elem : Element_Type; Prev : Node_Ptr; Next : Node_Ptr with Owner => Node;
end record with Owner => Prev; -- This indicates that "Prev" points to an -- object that owns this Node -- i.e. it is -- a "back" pointer, aka a "backward access object"
type List;
type List_Const_Ptr is access constant List;
type Cursor (List : List_Const_Ptr := null) is record Node : Node_Ptr with Owner => List; end record;
type List is limited ... with record Head : Node_Ptr with Owner => List; Tail_Cursor : Cursor (List => List'access); -- points to last element of list, if any ... end record;
...
procedure Insert (Container : in out List; Before : in Cursor; New_Item : in Element_Type) is -- Insert New_Item into list, before the item identified -- by Before. If Before is No_Element, then append to list. pragma Assert (Before.List = Container'Unchecked_Access or else Before.List = null); -- Make sure we have a valid Cursor New_Node : Node_Ptr := new Node'(Elem => New_Item, Prev => null, Next => null) with Owner => New_Node; -- New_Node owns itself at the moment -- We use 'Move below when assigning New_Node to some -- primary access object. It might have been simpler -- to use an allocator directly in the places below where -- we currently use New_Node'Move. begin if Before.Node = null then -- Insert at end if Container.Tail_Cursor.Node = null then -- List is empty; New_Node becomes the first and last element pragma Assert (Container.Head = null); -- Verify existing linkages Container.Head := New_Node'Move; Container.Tail_Cursor.Node := Container.Head; -- Run-time check that Tail_Cursor.List = Container'Access else -- Append to end of list, and update Tail_Cursor declare Tail : constant Node_Ptr := Container.Tail_Cursor.Node with Owner => Container; -- Run-time check that: -- Tail_Cursor.List = Container'Access begin Tail.Next := New_Node'Move; Tail.Next.Prev := Tail; -- Run-time check that Enclosing object of "Prev" -- (i.e. Tail.Next.all) is designated by a primary -- access object (e.g. Next component) contained -- within the composite object designated by its new -- value (i.e. Tail.all). In other words, verifying -- that Tail.Next = Tail.Next (which is True!). Container.Tail_Cursor.Node := Tail.Next; -- Run-time check that Tail_Cursor.List matches -- address of owner object of "Tail.Next," -- which is Container'Address, and it does. end; end if; else -- Add immediately prior to "Before" declare Follower : constant Node_Ptr := Before.Node with Owner => Container; -- Run-time check that Before.List = Container'Access Preceder : constant Node_Ptr := Follower.Prev with Owner => Container; -- Compile-time check that Owner of Preceder -- is same as owner of Follower (i.e. Container) begin if Preceder = null then -- This is a new first element of list pragma Assert (Container.Head = Follower); -- Verify proper existing linkages New_Node.Next := Container.Head'Move; -- Assign the primary access object "Next" of the new -- node, effectively attaching remainder of list to it. Container.Head := New_Node'Move; -- Link the new node as new head of list Follower.Prev := Container.Head; -- Set up new "back" pointer in Follower -- Run-time check that object enclosing Prev -- (Follower.all) is designated by a primary access -- component (Next) of the object designated by the -- new value of Prev (Container.Head.all). -- In other words, check that Container.Head.Next = -- Follower (it does). else -- Inserting into the middle of the list pragma Assert (Preceder.Next = Follower); -- Verify proper existing linkages New_Node.Next := Preceder.Next'Move; -- Assign the primary access object of the new node -- effectively attaching the remainder of list to it. Preceder.Next := New_Node'Move; -- Link the new node into the list Preceder.Next.Prev := Preceder; -- Set up the "back" pointer for new node. -- Run-time check that object enclosing Prev -- (Preceder.Next.all) is designated by a primary access -- component (Next) of the object designated by the new -- value of Prev (Preceder). -- In other words, check that -- Preceder.Next = Preceder.Next. Follower.Prev := Preceder.Next; -- Set up new "back" pointer in Follower -- Run-time check that object enclosing Prev -- (Follower.all) is designated by a primary access -- component (Next) of the object designated by the -- new value of Prev (Preceder.Next.all). -- In other words, check that Preceder.Next.Next = -- Follower (it does). end if; end; end if; end Insert;
As can be seen above, the Move attribute and the various compile-time and run-time checks help to ensure we are preserving the various desirable properties of the doubly-linked list structure. We are not able to have a simple "Tail" pointer in the linked-list header, but instead must put the tail pointer inside a cursor structure, because we want it to follow the rules for a secondary access component, rather than for a primary access component. We could invent yet another kind of aspect to cover this case, but the nested Tail_Cursor seems to be adequate, and allows us to piggy-back on the checks already needed for Cursors.
Implementing Splice is left as an exercise for the reader... ;-)
!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: Tucker Taft
Sent: Thursday, January 10, 2019  3:10 PM

Here is a drastic simplification of the pointer ownership AI [This is version
/01 of this AI - Editor.], focused completely on allowing the Global aspect of
ADTs like the Containers to not have to mention the operations they perform via
access values.  It defines an Owner aspect and an Is_Owner attribute, with the
sole goal of allowing pointed-to objects to be treated like components.  There
is a 4th iteration of AI12-0240 which was not shared, but which might become
interesting in the next version of the standard. Hopefully this one will allow
us to proceed with defining reasonable Global aspects for the Containers,
without burdening implementations with a complex new pointer ownership system.

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

From: Tucker Taft
Sent: Thursday, March 7, 2019  2:32 AM

This AI [Version /02 of this AI - Editor] is a re-boot of the Object Ownership
AI, eliminating the automatic storage reclamation, anti-aliasing checks, and
whole notion of borrowing or observing, which were present in earlier versions.
We have adopted a terminology that goes back to earlier discussions of "primary"
and "secondary" references, herein called "primary access objects" and
"secondary access objects."  We also have the notion of "backward access
components" which are used for "back pointers" in structures like doubly-linked
lists.

Finally there is the notion of "root access values" which are values that
designate an object that is not at the moment owned by any other object, meaning
it is "ripe" to be assigned to a primary access object.  Examples of a root
access value are allocators, the result of calling a function that returns an
allocator, and an attribute reference of the form "X'Move", which saves the
value of a primary access object X, nulls out X, and then returns the saved
value, again ensuring nobody owns the object designated by X'Move.

We have defined compile-time checks and a couple of run-time checks that
together ensure three properties (see the Language Design Principles section of
the AI):

1) No more than one primary access object designates a given heap object;

2) A secondary access object designates an object that is "owned" by the object
   denoted by the "Owner" aspect of the access object;

3) A backward access component designates an object that in turn owns the object
   containing the back pointer.

This seems to be enough to safely define the standard container data structures,
while having all pointer dereferences covered by "ownership" rules, meaning they
don't have to be mentioned in a Global aspect, which was the main goal of this
whole exercise.

I have interspersed in a fair amount of "AARM" rationale, and three extended,
heavily annotated examples.  If you ignore all of that and just look at the
normative parts of the !wording, it isn't too long, but hopefully the AARM
notes, the !proposal, the !discussion, and the !examples will help you
understand how this is designed to work.

Each iteration of this AI has had fewer features, and more complete
container-based examples.  Hopefully we are converging...

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

From: Tucker Taft
Sent: Monday, March 11, 2019  10:21 AM

Here are three slides illustrating AI12-0240-1, object ownership.

https://docs.google.com/presentation/d/1HMpd5p_k3HiiuTr_R0tawhmmKoUGdFWkTyKAlLmtX1g/edit?usp=sharing_eil&amp;ts=5c867cd0

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

Questions? Ask the ACAA Technical Agent