!standard 3.10.3(0) 19-01-10 AI12-0240-5/01 !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. 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, and we allow assertions using an attribute that claims one object Is_Owner of another. !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 "access T" or "" form of specification, which 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. !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. 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, or it can assert this, say in a precondition or postcondition, via a boolean attribute function, X'Is_Owner(Y) which means that the object X is the owner of the object designated by access value Y. It is also possible to simply assert Y'Is_Owner, which is used to say that access value Y designates a heap object that is not owned by any other object (e.g. the result of an allocator), and it owns "itself" if you will. 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." The self-owner assertion Y'Is_Owner may be applied to any access value. It is true for stand-alone access objects that specify themselves as an Owner, and it is true for the result of an allocator. The assertion X'Is_Owner(Y) is defined to be False if X is not specified as an Owner by some component of X or by X itself. The assertion X'Is_Owner(Y) is True if Y = X and Y'Is_Onwer, or if Y equals the value of a component of X whose Owner aspect specifies X, or if there is such a component C of X for which X.C.all'Is_Owner(Y). (This recursion should terminate because there are no cycles for owning pointers, but we expect to permit implementations to treat such assertions as assumptions, in which case it is a bounded error if it is in fact False. Similar rules would apply to Owner aspect specifications for stand-alone access objects.) 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, unless in the following special case: * The Owner object is immutably limited; and * The read/write access is incorporated into a Global or a Modifies aspect of the enclosing subprogram. If its Owner is a variable, then read/write access is permitted by the access object to the object it designates. As a convenience, we provide an attribute Y'Move where Y is a variable of an access type. It returns the original value of Y, and then sets Y to null, to ensure that only a single access value designates a given heap object at a time. If Y has an Owner, then before Y'Move, Y.all is owned by the 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." It is a bounded error if the same heap object is owned (directly) by two different objects. The consequences of the bounded errors is that the single-ownership property is no longer guaranteed, and the Global aspects might misrepresent the true side-effects of a subprogram, which could lead to code with concurrency conflicts not being detected by All_Conflict_Checks. !wording 6.1.3 Object Ownership This section describes the Owner aspect and the Is_Owner attribute. Together these can be used to indicate cases where an object created by an allocator is to be considered /owned/ by another object, such that the owner, or some component of the owner, designates the allocated object, and is the only such object that designates it. For the purposes of identifying Global effects (see 6.1.2) of an operation, reads or updates of such an allocated object are handled like reads or updates of some subcomponent of the owner object, rather than as reads or updates performed via an access value. Static Semantics The following aspect may be specified for a component or stand-alone object that is of an access-to-object type. It may also be specified for an array type, or an array object of an anonymous array type: Owner The Owner aspect is an /object_/name, and shall denote the object being declared, the current instance of the type being declared, the current instance of the enclosing type, or a pre-existing object. In the case where the denoted object is the access object being declared, that object is defined to /own/ any objects it designates. In the case where the denoted object is a current instance of a composite type, any objects of the composite type are defined to /own/ the object(s) designated by the access object(s) to which the aspect applies. 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. For a prefix X that denotes an object, the following attribute is defined: X'Is_Owner X'Is_Owner denotes a function with the following specification: function X'Is_Owner (Arg : any_type := X) return Boolean The actual parameter, if provided, shall be a name that denotes an object of an access-to-object type. If no argument is provided X shall be an object of an access-to-object type. This function evaluates the names of the objects involved and returns True if the object designated by Arg, if not null, is owned by the object X. Otherwise it returns False. For a prefix X that denotes a variable of an access-to-object type for which the Owner aspect has been specified: X'Move X'Move saves a copy of the value of X, sets X to the null value, and then returns the saved value. X'Move is an access value that /owns itself/ [Redundant: meaning it can be assigned to another access object with a specified Owner aspect, without having two such access objects designating the same allocated object.] The result of an allocator also owns itself, as does the result of a call on a function F that returns a value that owns itself. The attribute reference F'Result'Is_Owner is true after a call on such a function F. Legality Rules When the Owner aspect specifies the current instance of a composite type, there shall be no partial view of that composite type that is nonlimited, unless the composite type is a controlled type. AARM Reason: This prevents nonlimited private types from containing owning pointers, unless they are controlled. The predefined assignment operation does not do the "right thing" for types with owning pointer components, so we want only limited types, controlled types, or visible types to contain them. Implementation Permissions For the evaluation of X'Is_Owner(Y), the implementation may check the subcomponents of X which have an Owner aspect specified, and if at least one of them is nonnull, and the type of Y is such that the object it designates could be owned by X, then the implementation may return the value True for the attribute. Bounded Errors It is a bounded error if the attribute X'Is_Owner(Y) is used in an assertion expression and it is not in fact True. The possible effects are that Program_Error is raised, Assertion_Error is raised, or the program proceeds without raising an exception. As a result the Global aspect of some operation might not include all possible effects on global variables, which could allow certain concurrency conflicts not to be detected, depending on the Conflict_Check policy in effect. ... more wording TBD ... !discussion We originally had a much more complex model. We have tried to reduce this down to the bare minimum to allow the Global aspect to be more "reasonable" on abstract data types (ADTs) like the language-defined Container types. We used to provide some amount of automatic reclamation, deep copying, and automatic streaming of ownership-based access types. 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 the Is_Owner attribute to specify ownership relationships established as a result of some operation. The attribute seems necessary to capture the effects of operations that return access values designating "owned" heap objects. We could perhaps use some kind of aspect specification for that, but aspects tend to be pretty static, while operations are generally establishing ownership relationships dynamically. We allow implementations to treat the Is_Owner attribute as more of an assumption than an assertion that needs to be fully evaluated, to reduce implementation burden. We indicate it is a bounded error for an Is_Owner assertion to in fact be incorrect, so that in a future Ada revision we can require implementations to fully evaluate Is_Owner. !example For a linked list container, 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; Prev : Node_Ptr; 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.) The Prev component does NOT specify an Owner; 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): 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 the global protected object (dereferencing such a pointer would require Global to include this protected object). 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 heap-object ownership type Map is private with ...; type Cursor is private; ... procedure Insert (Container : in out Map; Key : Key_Type; Element : Element_Type) with Global => null; -- despite internal access value derefs -- Inserts an element with the given Key into the map function Find (Container : Map; Key : Key_Type) return Cursor with Global => null; -- despite internal access value derefs -- Returns a cursor identifying the element associated with the given key function Element (Container : Map; Position : Cursor) return Element_Type with Global => null; -- despite internal access value derefs -- Takes a Cursor and the map and returns the contents of the element -- at that cursor. 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 with Global => null, Post => Container'Is_Owner (Reference'Result.Element); -- 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. ... 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; end record; type Table is array(Natural range <>) of Node_Ptr with Owner => 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 with Access_Kind => Owner := new Table(0 .. Initial_Size - 1); Count : Natural := 0; end record; type Cursor is record Container : access constant Map; Node : Node_Ptr; 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); begin if First /= null then declare Walker : Node_Ptr := First with Owner => Container; begin while Walker /= null loop if Walker.Key = Key then -- Replace Walker.Element := Element; return; -- All done end if; Walker := Walker.Next; end loop; end; end if; -- Insert at head of chain First := new Node'(Key => Key, Element => <>, Next => First'Move); -- 'Move is not really necessary, but it emphasizes we are -- moving the old First to now be the second element in the -- list. It does require 'Move to null out the prefix -- immediately, and not wait until some random later moment. Container.Count := @ + 1; end Insert; function Find (Container : Map; Key : Key_Type) return Cursor is -- Returns a cursor identifying the element associated with the given key Index : Natural := Hash (Key) mod Container.Backbone'Length; Waklker : Node_Ptr := Container.Backbone (Index) with Owner => Container; begin while Walker /= null loop if Walker.Key = Key then -- Found it return Cursor '(Container => Container'Unchecked_Access, Node => Walker); end if; Walker := Walker.Next; 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 with Owner => Container := Position.Node; -- 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 the 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 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. Index : Natural := Hash (Key) mod Container.Backbone'Length; First : Node_Ptr renames Container.Backbone (Index); pragma Assert (Container'Is_Owner(First)); -- easy to prove 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); -- 'Move is not really necessary, but it emphasizes we are -- moving the old First to now be the second element in the -- list. It does require 'Move to null out the prefix -- immediately, and not wait until some random later moment. Container.Count := @ + 1; -- and return a reference to the default-init'ed element return Reference_Type'(Element => First.Element'Access); end Reference; end Hashed_Maps; !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. ****************************************************************