CVS difference for ai12s/ai12-0240-2.txt
--- ai12s/ai12-0240-2.txt 2018/06/15 06:09:23 1.1
+++ ai12s/ai12-0240-2.txt 2018/12/12 02:49:40 1.2
@@ -1,4 +1,4 @@
-!standard 3.10.3(0) 18-06-14 AI12-0240-2/01
+!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
@@ -7,7 +7,7 @@
!subject Access ownership for Abstract Data Types
!summary
-A new kind of access type, the owing access type, is defined, which allows a
+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.
!problem
@@ -42,60 +42,91 @@
!proposal
-Add "owned access types" to the language. We define the rules for such access
-types so that an owned access value can belong to at most one object at a
-time. (As a side-effect, if the value belongs to no object, it can be
-automatically reclaimed.)
+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 "unsafe" owned access types, which are unmanaged copies of owned
+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 owner.
+the scope of the appropriate ADT owner.
-====
-
-Detailed outline of the proposal.
-
-3.10.3 Owned Access Types
+!wording
-[Author's notes: This is pseudo-wording: some of it is in the style of
-Ada wording, and some is not.
+[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 AI12-0267-1.]
+data races in parallel statements - see 9.10.1 (from AI12-0267-1 and
+AI12-0298-1).]
-There is a new kind of access type, the *owning* access type.
+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. 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 *Owning* access type is declared by the following aspect:
+The *Fenced* access type is declared by the following aspect:
- Owning => (Primary_Owners => subtype_mark {, subtype_mark}[,
- Secondary_Owners => subtype_mark {, subtype_mark}])
+ Fenced => (subtype_mark {, subtype_mark})
-The subtype_marks specified by the Primary_Owners define the *primary owner
-types*; the other subtype_marks (if any) define *secondary owner types*.
-These are collectively called *owner types*. These subtype_marks shall
+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 primary owner types are typically a public ADT,
- and the secondary owner are (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: This allows multiple node types, as would be needed
- to implement an indefinite list or map container. We allow multiple
- Primary_Owners so that multiple types can share node types if needed.
+ 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.
-An owning access type shall be:
- * declared in a private part or body;
+ 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;
- * the primary owner type and any secondary owner types shall
- have their (full) declaration in the same declaration list as
- the owned access type;
- * the primary owner type and any secondary owner types shall
- be either controlled or immutably limited.
+ * 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
@@ -103,132 +134,204 @@
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.]
-
-No type shall be derived from an owing access type, or any owner type.
-An owing access type shall only match a formal access type which is itself
-an owning access type.
-
- [Author's note: The owner type part is mainly to keep my head from
- exploding trying to figure out the owner relationships in such cases.
- Most likely, it will need to be removed at some point.
-
- The restriction on the owning 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 owning types with the same pool,
- and with the same restrictions).]
-
-An object designated by by an owning access type is a *designated owned
-object* (or *owned object* for short).
-
-Access objects of an owned access type can be of of various kinds:
- * Owner objects are the primary access to the designated owned objects;
- they also control the lifetime of those objects;
- * Reference objects are copies that also designated the owned objects;
- they have no effect on the lifetime of the owned object and have
- no protection against becoming dangling.
-[Author's note: AI12-0240-1 has two additional kinds of access objects, the
-borrower and the observer; it may make sense to add them here to allow
-additional kinds of checked access usages. A borrower is similar to a
-compile-time tampering check, an observer is a short-term use of an
-object -- in both cases, the object can't disappear while they exist.
-We don't need these to implement containers. We have some pieces of
-their definitions below.]
-
-The kind of an access object is defined with an aspect when the access object
-is declared (this includes components, stand-alone objects, parameters, etc.).
-
-For an access object that is of an owing access type, or for a subtype of an
-owning access type, the following aspects are
-defined:
-
- Owing_Kind Can be one of the identifier specific to an aspect Owned,
- Reference, Borrower, or Observer. Specifies that the
- object has the specified kind.
- Owner A boolean aspect, specifying this to True is the same as
- Owning_Kind => Owner.
- Reference A boolean aspect, specifying this to True is the same as
- Owning_Kind => Reference.
- Borrower A boolean aspect, specifying this to True is the same as
- Owning_Kind => Borrower.
- Observer A boolean aspect, specifying this to True is the same as
- Owning_Kind => Observer.
+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.
+
+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 references) don't have to be repeated everywhere.
-My personal preference would be that Borrowers and Owners in particular are
-always explicitly declared on the object -- there should be very few of
-these. There might be more References and Observers.]
+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 Owning_Kind for an object is Owner, the object shall be a component of
-the primary owner type or a secondary owner type, or be a stand-alone object.
+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.
-
-For a parameter or generic formal of a owning access type, the actual object
-shall have the same kind.
-
-[Other rules for Borrower and Observer go here.]
-[Author's note: There are no other restrictions on Reference objects than
-the ones on all objects of owing access types. OTOH, there's no safety,
-either: they have even more possible cases of erroneous execution than regular
-access types.]
+A direct owner type shall be a tagged type. No type shall be derived from a
+direct owner type.
-An owner 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 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 owned access object, the
-source expression shall be only an allocator, another owned access variable
+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 owing access types
+ 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 owned access object first deallocates the existing
-designated object (if any). If the new value comes from some other owned
-access object, that object is set to null.
-
-A deallocator shall be only passed an owned access object.
-
-Inside of a subprogram with one or more parameters of the primary owner type,
-the accessibility of an owned access value (including when stored in a
-reference access object) is that of the parameter (as adjusted for "aliased"
-parameters). Otherwise, the accessibility level is infinite.
+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, an owning access type cannot
+ 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.
-If an owner type is controlled, after the call to Adjust a check is made that
-the owned access component is different in the target object than in the
-original source object. Program_Error is raised if this check fails.
-
- AARM Reason: We want all copies of owner objects to be deep copies (or
- illegal, if the type is limited). This check is a simple way to ensure
- that Adjust does a deep copy.
+[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 access object deallocates the designated owned
-object, if any.
+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 Unchecked_Deallocation of an owner type.
+ and as part of deallocation of a direct owner type.
-An owned access value V *might belong* to an object X if:
- * the type of X is a primary owner type of the type of V; or
- * the designated type of the type of V is a secondary owner type of a
- type D which has an primary owner type which is the type of X;
+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 secondary owner types, as might be needed
- to represent different parts of a data structure.
+ 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
@@ -237,13 +340,13 @@
[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 primary owner type,
+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 checks
+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).]
@@ -260,18 +363,45 @@
object, then the contract needed to cover X is sufficient to cover the
dereference.
-!wording
-
-No wording yet. See the detailed outline above.
+[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.]
!discussion
+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 owned access values. Some of those capabilities could be added
+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
@@ -298,9 +428,8 @@
----
-To allow container operations to use "Global => in out null" (assuming an
-element type that is "Global => in out null"), we need at a minimum for
-allocated nodes:
+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.
@@ -329,10 +458,10 @@
type Node;
type Node_Ptr is access Node
- with Owned => (Primary_Owners => List, Secondary_Owners => Node);
+ with Fenced => (List);
type Node is limited record
Elem : Element_Type;
- Prev : Node_Ptr with Reference;
+ Prev : Node_Ptr with Unmanaged;
Next : Node_Ptr with Owner;
end record;
Questions? Ask the ACAA Technical Agent