CVS difference for ai12s/ai12-0240-1.txt
--- ai12s/ai12-0240-1.txt 2018/01/25 06:21:14 1.4
+++ ai12s/ai12-0240-1.txt 2018/01/25 06:48:50 1.5
@@ -1,4 +1,4 @@
-!standard H.7(0) 18-01-15 AI12-0240-1/02
+!standard H.7(0) 18-01-16 AI12-0240-1/03
!standard H.8(0)
!class Amendment 17-10-09
!status work item 17-10-09
@@ -100,12 +100,15 @@
To summarize the possible states of an access-to-variable object of a type with
pointer ownership (changing "valid" to "unrestricted" below):
+
1. "unrestricted" -- may be dereferenced and used to update the designated
object.
+
2. "observed" -- value has been "observed," meaning that other
access-to-constant objects or IN formal parameters may exist that give
read-only access to all or part of the designated object, or part of some
object directly or indirectly owned by the designated object.
+
3. "borrowed" -- value has been "borrowed," meaning that the value has been
copied into a short-lived access-to-variable object, such as an IN parameter,
possibly of an anonymous access type. "Borrowed" also covers the case where
@@ -127,12 +130,19 @@
To simplify the rules, we introduce the notion of managed objects, which come in
two varieties:
+
1. Ownership Objects -- Objects of a type with Ownership aspect True:
- 1. Owning access objects -- access-to-variable objects with Ownership aspect True
- 2. Observing access objects -- access-to-constant objects with Ownership aspect True
+
+ 1. Owning access objects -- access-to-variable objects with Ownership aspect
+ True
+
+ 2. Observing access objects -- access-to-constant objects with Ownership
+ aspect True
+
3. Composite Ownership Objects
+
2. Other Managed Objects -- Any part of a non-Ownership object designated by an
-owning (1.a above) or observing access object (1b. above)
+ owning (1.a above) or observing access object (1b. above)
We require pass-by-reference for all types with Ownership aspect True, unless
they are visibly an access type. This is important to properly deal with the
@@ -149,6 +159,7 @@
access objects, and selected components, while "dynamic" names can involve
indexing or slicing.
+
!wording
Add the following sections to Annex H:
@@ -160,7 +171,7 @@
designated by an object of such an access type, or one or more read-only access
paths via such access objects, but never both. Furthermore, objects designated
by such access objects are automatically finalized and deallocated when the last
-access path is removed.[a][b]
+access path is removed.[a][b][c]
Static Semantics
@@ -172,9 +183,9 @@
The Ownership aspect is of type Boolean, and shall be specified by a static
expression. The Ownership aspect for a named general access type is
-False[c][d], and only confirming specifications are permitted. The Ownership
+False[d][e], and only confirming specifications are permitted. The Ownership
aspect is nonoverridable for a pool-specific access type, and if not specified
-for a root pool-specific access type, the value is False. [e][f] If not
+for a root pool-specific access type, the value is False. [f][g] If not
specified for a stand-alone object (or generic formal in-mode object) of an
anonymous access-to-object type, the value is False if there is no
initialization (or default) expression, and otherwise it is the same as that of
@@ -183,23 +194,28 @@
composite type, the Ownership aspect is True if there are any visible
subcomponents for which the Ownership aspect is True or if the type is tagged
and its parent (if any) has Ownership aspect True, and in these cases only
-confirming specifications are permitted.
+confirming specificat ns are permitted.
AARM Ramification: We do not require that all descendants of a tagged type
with Ownership aspect False also have Ownership False, but we disallow
(implicit or explicit) conversion between types with differing Ownership,
preventing inheritance of dispatching operations across such an Ownership
- aspect change. SPARK Note: We could probably allow inheriting dispatching
- operations in SPARK, even if Ownership differs between a parent type and its
- descendant, so long as Extensions_Visible is False. Not sure if we want to
- add such an aspect to Ada.
+ aspect change.
+ SPARK Note: We could probably allow inheriting dispatching operations in
+ SPARK, even if Ownership differs between a parent type and its descendant, so
+ long as Extensions_Visible is False. Not sure if we want to add such an
+ aspect to Ada.
+
The Ownership aspect of an anonymous access-to-object type is determined as
follows:
+
* If it is the type of a stand-alone object (including a generic formal in-mode
object), it is the same as that of the object;
+
* If it is the type of a formal parameter or result of a callable entity to
which the Restriction No_Parameter_Aliasing applies, it is True;
+
* Otherwise, it is False.
The Ownership aspect of a class-wide type is the same as that of the root type
@@ -214,9 +230,11 @@
observing access object, is called a managed object.
[Redundant: Any composite type with Ownership aspect True is a by-reference type
-(see 6.2).] [Ed. note: This additional rule for 6.2, where by-reference types
-are defined, is given below.]
+(see 6.2).]
+[Ed. note: This additional rule for 6.2, where by-reference types are defined,
+is given below.]
+
AARM Reason: Forcing by-reference parameter passing for such composite types
simplifies the rules significantly, and avoids the possibility of dangling
references upon exception propagation. Later we disallow private types with
@@ -230,10 +248,14 @@
A name denoting an object can either be a static name or a dynamic name. The
following are static names:
+
* a name that statically denotes an object (see 4.9);
+
* a selected component with prefix being a static name;
+
* a dereference (implicit or explicit), with prefix being a static name denoting
an object of an access type with Ownership aspect True;
+
* a name that denotes an object renaming declaration, if the object_name
denoting the renamed entity is a static name.
@@ -251,10 +273,12 @@
the same or overlapping objects might require a run-time check on the values
of array indices, or on the values of pointers of a non owning/observing
type.
+
+A static or dynamic name has a root object[h][i] defined as follows:
-A static or dynamic name has a root object[g][h] defined as follows:
* if the name has a prefix that statically denotes an object, it is the object
statically denoted by that prefix;
+
* otherwise, the name has a prefix that denotes an object renaming declaration,
in which case the root object is the renamed object.
@@ -269,8 +293,8 @@
AARM Reason: We will need this term later, and this seems like the best place
to introduce it. Note that static names/prefixes never involve indexing or
- slicing, so “overlap” is easy to define. They denote the same “whole”
- object, or one denotes a component or an object “owned” by the other.
+ slicing, so "overlap" is easy to define. They denote the same "whole"
+ object, or one denotes a component or an object "owned" by the other.
A static name that denotes a managed object can be in one of the following
ownership states:
@@ -312,29 +336,35 @@
state after the operation.
For names that denote managed objects:
+
* The default ownership state of such a name is determined as follows:
- * If it denotes a constant[i][j][k][l][m], other than an in parameter of an
+
+ * If it denotes a constant[j][k][l][m][n], other than an in parameter of an
owning access type, its default state is observed;
+
AARM Reason: Constant-ness is transitive for components that are owning
- access objects, so access-to-constant to the root means that nothing "below”
+ access objects, so access-to-constant to the root means that nothing "below"
that pointer can be written.
* If it is a dynamic name that denotes a variable, its default ownership
state is dynamic;
+
* Otherwise, its default ownership state is unrestricted.
-* The following operations observe[n] a name that denotes a managed object:
+
+* The following operations observe[o] a name that denotes a managed object:
+
* An assignment operation where the target is an access-to-constant object of
an anonymous type, and the name denotes an owning access object as the
source of the assignment, if the assignment is part of the initialization
- of a stand-alone object[o] or the parameter association for a formal
+ of a stand-alone object[p] or the parameter association for a formal
parameter or generic formal object of mode in;
AARM Reason: This supports traversing a data structure in read-only fashion,
while preserving the handle on the root of the structure.
* An assignment operation that is used to initialize a constant object
- [p][q](including a generic formal object of mode in) of a named type with
- Ownership aspect True but that is not an owning access type,[r] where the
+ [q][r](including a generic formal object of mode in) of a named type with
+ Ownership aspect True but that is not an owning access type,[s] where the
name denotes the source of the assignment.
AARM Reason: We handle the case of assignment to named owning access types as
@@ -343,7 +373,7 @@
nested owning access objects.
* A call where the name denotes an actual parameter, and the formal parameter
- is of mode in and composite or aliased;[s][t]
+ is of mode in and composite or aliased;[t][u]
AARM Reason: Unless the parameter is an owning access object, we treat this
as observing. If it is an owning access object, and the formal is
@@ -371,10 +401,11 @@
that "own" this object that are in the borrowed state.
* The following operations borrow a name that denotes a managed object:
+
* An assignment operation that is used to initialize an owning access object,
where the (borrowed) name denotes the source of the assignment and the
target is a stand-alone variable of an anonymous access-to-variable type,
- or is a constant [u][v][w][x][y][z](including an in parameter or a generic
+ or is a constant [v][w][x][y][z][aa](including an in parameter or a generic
formal object) of a (named or anonymous) access-to-variable type;
AARM Reason: This supports traversing a data structure with the ability to
@@ -399,7 +430,7 @@
to the parameter is being held at the call site for the copy back, and in
either case, we don't want the object to be deallocated.
- * Object renaming [aa][ab]where the name is the object_name denoting the
+ * Object renaming [ab][ac]where the name is the object_name denoting the
renamed object, when the renamed object is not in the observed or borrowed
state.
@@ -431,18 +462,18 @@
rule that will check (at run-time if necessary) that there are no objects
that "own" this object that are in the observed or borrowed state.
-
* The following operations are considered move operations:
+
* An assignment operation, where the target is a variable or return object
- [ac][ad][ae](see 6.5) of a named type[af] with Ownership aspect True,
- including an OUT or IN OUT formal parameter [ag]of an owning access type.
+ [ad][ae][af](see 6.5) of a named type[ag] with Ownership aspect True,
+ including an OUT or IN OUT formal parameter [ah]of an owning access type.
AARM Ramification: This includes both the copy in and the copy back of such a
formal parameter from its actual parameter, and an assignment to/from such a
formal inside the subprogram.
- * An assignment operation where the target is part of an aggregate[ah][ai],
- having a named type with Ownership aspect True.
+ * An assignment operation where the target is part of an
+ aggregate[ai][aj][ak], having a named type with Ownership aspect True.
AARM Reason: These operations are considered "moves" because they result in a
transfer of ownership, and possibly a deallocation of the object designated
@@ -451,6 +482,7 @@
parameter passing, which is what is used for all composite/private types with
Ownership aspect True.
+
Legality Rules
If a type has a partial view, the Ownership aspect may be specified explicitly
@@ -473,19 +505,19 @@
The source of an assignment operation to an object of an anonymous
access-to-object type with Ownership True (including a parameter) shall neither
-be[aj][ak] an allocator nor a function call[al].
+be[al][am] an allocator nor a function call[an].
AARM Reason: This could lead to a storage leak, since we do not finalize and
reclaim the object designated by such an access object when its scope ends --
we assume there is still some other access object that designates it. An
allocator or function call must first be assigned to an (owning) access
- object of a named type, and then it can be “walked” using an object of an
+ object of a named type, and then it can be "walked" using an object of an
anonymous type. Note that we want any allocators to be of a named
pool-specific type so their storage is allocated from a pool that is being
- used for “managed” objects, so you would end up having, in any case, to put
+ used for "managed" objects, so you would end up having, in any case, to put
an explicit type qualification around the allocator to specify the named
pool-specific type. So requiring the target to be an access object of a
- named (pool-specific) type doesn’t seem like a big burden.
+ named (pool-specific) type doesn't seem like a big burden.
The prefix of a name shall not denote denote a function call, or a qualified
expression whose operand is a function call, an aggregate, or an allocator, if
@@ -497,7 +529,7 @@
AARM Reason: Again, this is to avoid storage leaks, from constructs like
F(A).X, where it is not clear when we could deallocate the storage of the
object designated by F(A). We could relax this by requiring the compiler to
- deallocate these objects at the “right” time, but that would require worrying
+ deallocate these objects at the "right" time, but that would require worrying
about observes and borrows, etc. Also, allowing names whose prefix is a
function call or qualified expression with allocator or aggregate as an
operand would complicate other rules, so we make them illegal.
@@ -509,19 +541,19 @@
observing the prefix if the anonymous access type is access-to-constant, and
borrowing otherwise.
- AARM Reason: We allow taking ‘Access of aliased “managed” objects to
+ AARM Reason: We allow taking ‘Access of aliased "managed" objects to
initialize an object of an anonymous access type to support use of pointers
in programs where dynamic allocation is not permitted. The same rules for
- borrowing and observing apply, but no “move” operations are permitted, nor
- any deallocations.[am][an]
+ borrowing and observing apply, but no "move" operations are permitted, nor
+ any deallocations.[ao][ap]
A declaration that observes or borrows a managed object shall not occur within
the private part or private descendant of a package, nor within a package body,
if the root of the name of the managed object denotes an object whose scope
includes the visible part of the package, unless the accessibility level of the
-declaration is statically deeper than that of the package.[ao]
+declaration is statically deeper than that of the package.[aq]
- AARM Reason: [ap][aq][ar][as][at]We disallow borrowing in "private" an object
+ AARM Reason: [ar][as][at][au][av]We disallow borrowing in "private" an object
that is visible, since the compiler needs to "know" whether an object has
been observed or borrowed, everywhere within the scope of the object.
@@ -535,16 +567,18 @@
type of the class. Similarly, a type cannot inherit a dispatching operation
from its parent type if the parent has a different value for its Ownership
aspect, since the implicit conversion associated with calling an inherited
- subprogram would violate this rule. SPARK Note: We could perhaps relax this
- in the context of the Extensions_Visible attribute being True.
+ subprogram would violate this rule.
+
+ SPARK Note: We could perhaps relax this in the context of the
+ Extensions_Visible attribute being True.
For an assignment statement where the target is a stand-alone object of an
anonymous access-to-object type with Ownership aspect True:
* If the type of the target is an anonymous access-to-variable type (an owning
access type), the source shall be an owning access object denoted by a name
- that is not in the observed state[au][av], and whose root object is the target
- object itself[aw][ax][ay][az][ba][bb];
+ that is not in the observed state[aw][ax], and whose root object is the target
+ object itself[ay][az][ba][bb][bc][bd];
AARM Reason: At its declaration, such an owning access object can be
initialized from any owning access object in the unrestricted state. On
@@ -570,7 +604,7 @@
shall not be moved nor borrowed and shall not be used as the target of an
assignment;
- AARM Reason: Observed objects and everything “owned” by them are read only.
+ AARM Reason: Observed objects and everything "owned" by them are read only.
* While the state of a name that denotes a managed object is borrowed, the name
shall not be used as a primary, as a prefix, as an actual parameter, nor as
@@ -587,14 +621,14 @@
AARM Reason: After a move, we set the source to be null if it is an object
other than an anonymous return object, aggregate, or allocator, and
- effectively “destroy” everything bearing a name that overlaps the source.
+ effectively "destroy" everything bearing a name that overlaps the source.
Note that the only case where a (non-anonymous) owning access object can be a
constant and not be in the observed state, is when it is an in parameter. So
the first part really only disallows moving the value of an in parameter.
You *can* borrow the value of an in parameter, by passing it further along as
an in parameter, or assigning it to an object of an anonymous owning
- access-to-variable type. The second part is more important -- you can’t move
- something if anything “beneath” it is in the borrowed or observed state.
+ access-to-variable type. The second part is more important -- you can't move
+ something if anything "beneath" it is in the borrowed or observed state.
* At the point of a call, any name that denotes a managed object that might be
written (other than via a formal parameter) as part of the invocation of the
@@ -612,7 +646,7 @@
When the value of a variable of a named owning access type is moved to another
object, the value of the owning access variable is set to null. This applies to
-each subcomponent [bc]that is of a named owning access type in a move of a
+each subcomponent [be]that is of a named owning access type in a move of a
composite object. [Redundant: This includes the case of moving an actual
parameter to a formal parameter of a named owning access type that is of mode
out or in out, as well as the copy back.]
@@ -640,7 +674,7 @@
Similarly, if a variable of a named owning access type (including a component)
is non-null when it is finalized (other than when it is the target of an
assignment, which is covered by the above rule), the object designated by the
-variable is finalized[bd][be][bf][bg], and its storage is deallocated. This
+variable is finalized[bf][bg][bh][bi], and its storage is deallocated. This
applies as well to formal parameters of mode out and in out that are of a named
owning access type, when the subprogram does not complete normally. [Redundant:
This rule applies recursively to subcomponents of the designated object that are
@@ -656,12 +690,12 @@
AARM Ramification: The finalization that normally precedes an assignment,
according to 7.6, is handled differently, as described for the assignment
case (the finalization only happens if the value is changing). On the other
- hand, the finalization that happens to the subcomponents of the “old”
+ hand, the finalization that happens to the subcomponents of the "old"
designated object prior to it being reclaimed, *is* intended to be covered by
this rule, so we get reclamation of the entire tree of objects.
Finally, if a constant of a named type with Ownership aspect True is initialized
-by a [bh]function call, aggregate, or allocator, then when it is finalized, if
+by a [bj]function call, aggregate, or allocator, then when it is finalized, if
the constant is not itself part of a return object or aggregate, each part of
the constant that is of a named owning access type is finalized as above.
[Redundant: This includes in parameters initialized by such an expression.]
@@ -709,12 +743,12 @@
the potentially overlapping names.
For a dynamic name D1 that is in a dynamic ownership state, if an operation
-requires that[bi], were it static, it not be in an observed[bj][bk] [bl][bm](or
+requires that[bk], were it static, it not be in an observed[bl][bm] [bn][bo](or
borrowed) state, then for every other dynamic name D2 that is in the observed
(or borrowed) state and potentially overlaps with D1, a check is made that the
potentially aliased parts of the names do not in fact denote overlapping parts
-of the same object.[bn][bo] If this check fails, Program_Error is
-raised.[bp][bq]
+of the same object.[bp][bq] If this check fails, Program_Error is
+raised.[br][bs]
AARM Ramification: This requires keeping track of what potentially aliased
(see above) dynamic names are observed (or borrowed), and doing checks that
@@ -722,23 +756,89 @@
this name. Note that this can be as simple as comparing the addresses of the
shared prefixes.
- AARM Reason: We don’t just talk about “overlap” of the denoted objects, but
+ AARM Reason: We don't just talk about "overlap" of the denoted objects, but
instead talk about overlap between the potentially aliased parts of the two
names. That is necessary because we are interested in a more general notion
- of “overlap” between names that treats designated objects as overlapping with
- the object containing the pointer to them. [Ed. question: Note that we are
- relying here (and later) on the meaning of (physical) “overlap” that is
- already used in various parts of the standard (e.g. A(3/4) and 13.3(73.6/3)).
- Should we actually define it “officially” somewhere -- perhaps as part of
- defining attribute function Overlaps_Storage?]
+ of "overlap" between names that treats designated objects as overlapping with
+ the object containing the pointer to them.
+
+[Ed. question: Note that we are relying here (and later) on the meaning of
+(physical) "overlap" that is already used in various parts of the standard (e.g.
+A(3/4) and 13.3(73.6/3)). Should we actually define it "officially" somewhere
+-- perhaps as part of defining attribute function Overlaps_Storage?]
+
+H.7.1 Operations of Owning Access Types
+The following attribute is defined for an object X of a named access-to-variable
+type T with Ownership aspect True:
+
+X'Copy
+
+The evaluation of X'Copy yields null if X is null; otherwise it yields the
+result of evaluating an allocator of type T with the designated object
+initialized from a copy of X.all (adjusted as appropriate -- see 7.6), but with
+each subcomponent X.all.S that is itself of a named owning access type replaced
+with X.all.S'Copy. If the designated type of T is limited, Program_Error is
+raised, and no copying or allocation is performed. If the evaluation of X'Copy
+propagates an exception, any object that has been newly allocated and adjusted
+is finalized, including any owning access subcomponent X.all.S that has been
+successfully replaced by X.all.S'Copy.
+
+ AARM Ramification: The intent is that no newly allocated storage is lost if
+ an exception is propagated by X'Copy, but that no part of X itself is
+ finalized or deallocated as a side-effect of such an exception.
+
+The stream-oriented attributes (see 13.13.2) for every subtype S of a named
+access-to-variable type T with designated type D and Ownership aspect True, have
+the following semantics:
+
+ AARM Ramification: Essentially the access objects "disappear" in the
+ streaming representation, and all you have are the non-access type elements
+ of the "tree," plus some Boolean "existence" flags to indicate whether an
+ access object was null.
+
+S'Output
+
+If the designated type D does not have an available Output attribute,
+Program_Error is raised. Otherwise, S'Output (Stream, Item), where Item is of
+type T, invokes Boolean'Write (Stream, False) if Item is null, and otherwise
+invokes Boolean'Write (Stream, True) followed by D'Output (Stream, Item.all).
+
+S'Write
+
+S'Write (Stream, Item) is equivalent to S'Output (Stream, Item).
+
+S'Input
+
+If the designated type D does not have an available Input attribute,
+Program_Error is raised. Otherwise, S'Input (Stream) invokes
+Boolean'Input(Stream). If this returns False, S'Input returns null. If
+Boolean'Input returns True, an allocator of the form:
+
+ new D'(D'Input (Stream))
+
+is evaluated and returned by S'Input. If the evaluation of D'Input propagates
+an exception, S'Input propagates the exception, and no storage is allocated.
+
+S'Read
+
+S'Read (Stream, Item), where Item is of type T, invokes S'Input (Stream) and
+assigns (moves) the result to Item. If S'Input propagates an exception, S'Read
+propagates the exception.
+
+The above attributes are considered to support external streaming (see 13.13.2),
+provided the the designated type D supports external streaming. For the
+purposes of this determination, a set of mutually recursive owning access types
+do not by themselves prevent an enclosing type from supporting external
+streaming.
+
H.8 The No_Parameter_Aliasing Restriction
[TBD: Talk about aliasing between parallel tasklets, or have a separate
No_Data_Races restriction?]
This section describes the No_Parameter_Aliasing restriction, which disallows
-passing a part of a variable to a subprogram or entry[br][bs][bt], if it is
+passing a part of a variable to a subprogram or entry[bt][bu][bv], if it is
potentially referenced as a global by the callable entity, unless both access
paths are read only. Furthermore, it disallows operating on overlapping parts
of a single variable twice within the same expression or simple statement,
@@ -750,7 +850,7 @@
a single expression or simple statement, given the likelihood for error.
An operation that occurs within an expression or simple statement occurs
-strictly before[bu] a second such operation only if:
+strictly before[bw] a second such operation only if:
* The first occurs within an expression, and the result of the expression is an
operand to the second;
@@ -777,17 +877,18 @@
these rules also apply if the restriction applies at the point of a call or
other operation:
-* On any call to which the restriction applies, a part of a variable[bv] shall
+* On any call to which the restriction applies, a part of a variable[bx] shall
not be passed as a parameter if a statically overlapping part (see H.7) of the
variable can be referenced as a global during the invocation of the called
entity (as limited by its (explicit or default) Global aspect -- see 6.1.2),
unless both access paths are read only;
* Within a single expression or simple statement, statically overlapping parts
- of a single variable shall not be passed twice as operands to operations[bw],
- unless both are read only operands, one is a read-only scalar operand that is
- not an aliased parameter, or one is a read-only operand to an operation that
- occurs strictly before the operation where it an updatable operand;
+ of a single variable shall not be passed twice as operands to
+ operations[by][bz], unless both are read only operands, one is a read-only
+ scalar operand that is not an aliased parameter, or one is a read-only operand
+ to an operation that occurs strictly before the operation where it an
+ updatable operand;
AARM Reason: We allow non-aliased scalar operands because they are certain to
be passed by copy; we disallow access-type operands if not used strictly
@@ -803,17 +904,15 @@
potentially aliased parts of the two names. Program_Error is raised if this
check fails.
-
[end of H.8]
-
Add after 6.2(7/3):
* a composite type with Ownership aspect True (see H.7);
!discussion
-The objective of this pair of features, the Ownership aspect and the
+he objective of this pair of features, the Ownership aspect and the
No_Parameter_Aliasing restriction, is to allow pointers to heap objects to be
used safely and efficiently without fear of dangling references or storage
leaks, and to reduce aliasing to the point where programs using pointers and
@@ -826,7 +925,7 @@
to allow read-only copies to be used to walk a data structure, so we allow
access-to-constant copies so long as they are of a type that goes away before
the original object is finalized. We also allow access-to-variable copies which
-are considered “borrowers.” Most commonly these will be stand-alone objects of
+are considered "borrowers." Most commonly these will be stand-alone objects of
an anonymous access-to-object type, though an IN parameter of a named
access-to-variable type also acts as a borrower.
@@ -835,7 +934,7 @@
data structure destructively, while restoring the ownership state of the access
object designating the root after the dereference goes away. To change what is
the root object itself requires a direct assignment to the owner of the root,
-which cannot occur while the “borrower” exists.
+which cannot occur while the "borrower" exists.
As noted we have four states for an access object: unrestricted, observed,
borrowed, and dynamic. An unrestricted access object is the owner, and provides
@@ -848,9 +947,13 @@
Tracking the state of stand-alone access objects is pretty straightforward.
Tracking the state of components is more challenging. We have given the rules
in terms of static and dynamic names, and their prefixes. We believe these
-rules are now sound and sufficiently flexible to permit “normal” kinds of data
+rules are now sound and sufficiently flexible to permit "normal" kinds of data
structure manipulations.
+We have provided "deep" copying and streaming attributes, so that arbitrarily
+complex data structures built using owning access types can be easily copied or
+streamed, without additional work by the programer.
+
For the No_Parameter_Aliasing rules, we fall back on run-time checks to prevent
aliasing when necessary for "dynamic" names. Hopefully such checks can be
eliminated at compile-time in almost all interesting cases. SPARK would
@@ -864,7 +967,6 @@
Eventually we will extend this to cover checking for data races between
potentially concurrent actions.
-
Safety Properties
The rules that make up the above proposal are intended to ensure the following
@@ -879,18 +981,16 @@
* There are one or more names in the observed state denoting access objects
that designate the heap object.
-There may be any number of names in the borrowed state denoting access objects
-designating the heap object, but these give no access while in this state.
-
-TBD: What about dynamic names in the dynamic ownership state?
-
* When an operation observes or borrows using a dynamic name, that name
enters the observed or borrowed state throughout the scope of the observer
or borrower; during that period run-time checks are used to check any other
- dynamic name that is potentially overlapping with the first dynamic name,
- to see if it does in fact overlap, and if so, to preclude it from all
- operations, if it overlaps a borrowed name, or from updating operations, if
- it overlaps an observed name.
+ dynamic name in the dynamic ownership state that is potentially overlapping
+ with the first dynamic name, to see if it does in fact overlap, and if so,
+ to preclude it from all operations, if it overlaps a borrowed name, or from
+ updating operations, if it overlaps an observed name.
+
+There may be any number of names in the borrowed state denoting access objects
+designating the heap object, but these give no access while in this state.
1. When such a heap object is deallocated, there are no access objects
designating it.
@@ -901,16 +1001,15 @@
object, and any name that denotes a subcomponent of the designated object
that is of an owning access type, is also in the observed state.
-4. Only names in the unrestricted state provide read-write access to the
- designated object.
+4. Only static names in the unrestricted state provide read-write access to the
+ designated object, or dynamic names in the dynamic ownership state where they
+ have been checked to ensure they do not overlap with a dynamic name in the
+ observed or borrowed state.
-
!examples
-
Here is an example of swapping two elements of a singly linked list.
-
type List;
type List_Ptr is access List with Ownership;
@@ -931,17 +1030,18 @@
declare
Second : List_Ptr := X.Next;
-- Second cannot be a constant because it
- -- will be nulled after a “move”
+ -- will be nulled after a "move"
begin
- -- Swap them (via “move”s)
+ -- Swap them (via "move"s)
X.Next := null; -- not really necessary (already null)
Second.Next := X;
X := Second;
end;
+
else
-- More than two elements; find second-to-last element
declare
- Walker : access List := X[bx];
+ Walker : access List := X[ca];
begin
while Walker /= null loop
declare
@@ -955,7 +1055,7 @@
declare
Last : List_Ptr := Next_Ptr.Next
-- Last cannot be a constant because it
- -- will be nulled after a “move”
+ -- will be nulled after a "move"
begin
-- Swap last two
Next_Ptr.Next := null; -- not really necessary (already null)
@@ -966,7 +1066,7 @@
end if;
end;
-- Go to next element
- -- Note that we need to do this *after* the “borrowing”
+ -- Note that we need to do this *after* the "borrowing"
-- inherent in the renaming of Walker.Next is complete.
Walker := Walker.Next;
end loop;
@@ -1056,7 +1156,7 @@
Interesting, and clearly some work has gone into this. But...
-It says “The Ownership aspect is a relatively simple idea” but it looks quite
+It says "The Ownership aspect is a relatively simple idea" but it looks quite
complicated to me, most of it is more like what I would expect a static
analysis tool to do than a compiler. E.g. it has a section on control flow -
if we were to require flow analysis of a compiler, then there are more useful
@@ -1065,7 +1165,7 @@
a function return a value.
It seems to have an Ada 83 view of access types, i.e. that they only point to
-objects allocated on the heap. Randy’s reply elaborates on this.
+objects allocated on the heap. Randy's reply elaborates on this.
Also, access types are currently classified as being elementary types, I think
that would have to be revised if they have to carry around hidden state
@@ -1078,7 +1178,7 @@
> Interesting, and clearly some work has gone into this. But...
>
-> It says “The Ownership aspect is a relatively simple idea” but it looks
+> It says "The Ownership aspect is a relatively simple idea" but it looks
> quite complicated to me, most of it is more like what I would expect a
> static analysis tool to do than a compiler.
@@ -1097,7 +1197,7 @@
on that, which is worth considering!
> It seems to have an Ada 83 view of access types, i.e. that they only point
-> to objects allocated on the heap. Randy’s reply elaborates on this.
+> to objects allocated on the heap. Randy's reply elaborates on this.
This is a good point. The TBD "conversion" rules were meant to cover that, in
particular a value of such an "owning" access type would only be allowed to
Questions? Ask the ACAA Technical Agent