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