CVS difference for ai12s/ai12-0240-1.txt
--- ai12s/ai12-0240-1.txt 2018/01/25 06:48:50 1.5
+++ ai12s/ai12-0240-1.txt 2018/01/25 07:14:55 1.6
@@ -1,4 +1,4 @@
-!standard H.7(0) 18-01-16 AI12-0240-1/03
+!standard H.7(0) 18-01-24 AI12-0240-1/04
!standard H.8(0)
!class Amendment 17-10-09
!status work item 17-10-09
@@ -191,10 +191,11 @@
initialization (or default) expression, and otherwise it is the same as that of
the type of the initialization (or default) expression. For an untagged
composite type, the Ownership aspect is nonoverridable in derived types. For a
-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 specificat ns are permitted.
+nonlimited controlled type, the Ownership aspect is False, and only confirming
+specifications are permitted. For other composite types, the Ownership aspect
+is True if there are any visible subcomponents for which the Ownership aspect is
+True if the type is tagged and its parent (if any) has Ownership aspect True,
+and in these cases only confirming specifications 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
@@ -207,6 +208,12 @@
long as Extensions_Visible is False. Not sure if we want to add such an
aspect to Ada.
+ AARM Reason: We do not allow a nonlimited type to be controlled and also have
+ Ownership True, as the Adjust procedure of the controlled type takes over the
+ semantics of assignment, and would defeat the move/borrow/observe semantics
+ defined below. See H.7.1 for a bounded error relating to the Adjust
+ procedure for a controlled types with any subcomponents with Ownership True.
+
The Ownership aspect of an anonymous access-to-object type is determined as
follows:
@@ -425,10 +432,12 @@
parameter is of mode out or in out (or the generic formal object is of mode
in out).
- AARM Reason: We consider this to be "borrowing" of the value of the managed
- object, since either the object is being passed by reference, or a reference
- 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.
+ AARM Reason: We consider this to be "borrowing" of the actual parameter name
+ denoting the managed object, while the formal parameter name comes into use
+ as an unrestricted name for the object. We don't want the actual parameter
+ name used for any other purpose during the execution of the called subprogram
+ or generic instance, since the formal parameter name provides full read/write
+ access to the object.
* 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
@@ -456,11 +465,11 @@
every static name that denotes the same managed object is borrowed, and every
name with that static name as a prefix, is similarly borrowed.
- AARM Ramification: This applies recursively down the tree of managed objects,
- meaning that borrowing a managed object effectively borrows all of the
- objects "owned" by that managed object. Dynamic objects rely on a different
- 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.
+ AARM Ramification: This applies recursively down the tree of managed
+ objects, meaning that borrowing a managed object effectively borrows all of
+ the objects "owned" by that managed object. Dynamic objects rely on a
+ different 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:
@@ -482,7 +491,6 @@
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
@@ -553,9 +561,9 @@
includes the visible part of the package, unless the accessibility level of the
declaration is statically deeper than that of the package.[aq]
- 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.
+ AARM Reason: 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.
In a conversion [Redundant: (explicit or implicit)], the Ownership aspect of the
operand type and that of the target type shall be the same. [Redundant: Note
@@ -577,8 +585,8 @@
* 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[aw][ax], and whose root object is the target
- object itself[ay][az][ba][bb][bc][bd];
+ that is not in the observed state[ar][as], and whose root object is the target
+ object itself;[at]
AARM Reason: At its declaration, such an owning access object can be
initialized from any owning access object in the unrestricted state. On
@@ -588,10 +596,10 @@
same SAOAAT.
* If the type of the target is an anonymous access-to-constant type (an
- observing access type), the source shall be an owning access object denoted by
- a name that is in the observed state, and whose root object is also in the
- observed state and not declared at a statically deeper accessibility level
- than that of the target object.
+observing access type), the source shall be an owning access object denoted by a
+name that is in the observed state, and whose root object is also in the
+observed state and not declared at a statically deeper accessibility level than
+that of the target object.
AARM Reason: At its declaration, such an observing access object can be
initialized from any owning access object in the unrestricted or observed
@@ -607,8 +615,9 @@
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
- the target of an assignment;
+ shall not be moved, borrowed, nor observed (directly or indirectly), and shall
+ not be used as a primary, as a prefix, as an actual parameter, nor as the
+ target of an assignment; [au][av]
AARM Reason: The object has been borrowed, and should not even be observed
other than via the borrower.
@@ -646,7 +655,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 [be]that is of a named owning access type in a move of a
+each subcomponent [aw]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.]
@@ -674,13 +683,13 @@
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[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
-of an owning access type, ensuring that all objects designated indirectly by an
-owning access object are finalized and deallocated when the owning access object
-is finalized.]
+variable is finalized, 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 of an owning
+access type, ensuring that all objects designated indirectly by an owning access
+object are finalized and deallocated when the owning access object is
+finalized.]
AARM Reason: We treat both the copy-in and the copy-back as a "move" for OUT
and IN OUT parameters of a named owning access type, so if a subprogram does
@@ -695,7 +704,7 @@
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 [bj]function call, aggregate, or allocator, then when it is finalized, if
+by a [ax]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.]
@@ -743,12 +752,12 @@
the potentially overlapping names.
For a dynamic name D1 that is in a dynamic ownership state, if an operation
-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.[bp][bq] If this check fails, Program_Error is
-raised.[br][bs]
+requires that[ay], were it static, it not be in an observed[az][ba] (or
+borrowed) state[bb], 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.[bc][bd] If this check fails,
+Program_Error is raised.
AARM Ramification: This requires keeping track of what potentially aliased
(see above) dynamic names are observed (or borrowed), and doing checks that
@@ -769,24 +778,30 @@
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:
+The following attribute is defined for an object X of a named non-limited type
+T[be][bf][bg][bh][bi]:
-X'Copy
+X'Copy[bj]
-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.
+The evaluation of X'Copy when T is a type with Ownership False yields an
+anonymous object initialized by assignment from X; when T is a composite type
+with Ownership True, X'Copy yields an anonymous object initialized from X
+(including adjustment of controlled parts) but with all subcomponents X.S that
+are of a named owning access type (and are not subcomponents of a controlled
+part) being replaced by X.S'Copy; when T is an owning access type, X'Copy raises
+Program_Error if the designated type of T is limited, and otherwise it yields
+null if X is null and if not null, the result of evaluating an allocator of type
+T with the designated object initialized from X.all'Copy. For the purposes of
+other language rules, X'Copy is equivalent to a call on a function that
+"observes" X.
+
+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 that has been successfully replaced by its 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.
+ an exception is propagated by X'Copy, but that no part of X or X.all 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
@@ -802,7 +817,8 @@
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).
+invokes Boolean'Write (Stream, True) followed by D'Output (Stream,
+Item.all).[bk]
S'Write
@@ -815,7 +831,7 @@
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))
+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.
@@ -826,11 +842,21 @@
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.
+The owning access type T in the above is considered to support external
+streaming (see 13.13.2), provided its 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.
+
+Bounded Errors
+
+If a nonlimited controlled type T has a subcomponent of an owning access type,
+it is a bounded error if the Adjust procedure for the type does not replace all
+such subcomponents with null or an access value designating a newly allocated
+object. The possible consequences are that Program_Error is raised immediately
+after invoking Adjust, or the guarantee of an exclusive single updater might be
+violated, and a future dereference of the unreplaced access value could lead to
+erroneous execution.
H.8 The No_Parameter_Aliasing Restriction
@@ -838,7 +864,7 @@
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[bt][bu][bv], if it is
+passing a part of a variable to a subprogram or entry[bl][bm][bn], 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,
@@ -850,7 +876,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[bw] a second such operation only if:
+strictly before[bo] a second such operation only if:
* The first occurs within an expression, and the result of the expression is an
operand to the second;
@@ -877,7 +903,7 @@
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[bx] shall
+* On any call to which the restriction applies, a part of a variable[bp] 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),
@@ -885,7 +911,7 @@
* Within a single expression or simple statement, statically overlapping parts
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
+ operations[bq][br], 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;
@@ -912,7 +938,7 @@
!discussion
-he objective of this pair of features, the Ownership aspect and the
+The 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
@@ -959,6 +985,25 @@
eliminated at compile-time in almost all interesting cases. SPARK would
complain if such a check could not be proved at analysis time.
+We presume that the Adjust procedure of nonlimited controlled types turn every
+assignment into a "deep" copy, potentially making use of the ‘Copy attribute on
+any subcomponents that have Ownership True. Therefore, we do not allow a
+controlled type to itself have Ownership True, even if it has subcomponents with
+Ownership True, so there is no notion of move/observe/borrow with respect to
+controlled types per-se, though objects designating them could still have
+Ownership True. Effectively they are treated like "elementary" types from the
+point of view of most of these rules. However, they still have to abide by the
+No_Parameter_Aliasing rules, which are largely independent of Ownership, except
+in terms of the definition of "overlap."
+
+So in some sense, these Owning access types provide a very low overhead
+"controlled" type. If you still want to write your own Adjust and Finalize
+procedures, then you can explicitly declare a controlled type. If all you want
+is automatic storage management for levels of indirection, then just use an
+access type with Ownership True and the ‘Copy attribute where you want it, and
+let the compiler take care of all of the necessary grunt work of preventing
+dangling references and storage leaks (in a provably safe manner).
+
The work on this topic was started in earnest by an intern at AdaCore,
Georges-Axel Jaloyan, mentored by Yannick Moy. Many of these concepts are
inspired by the "borrow checker" of the Rust language, and/or the anti-aliasing
@@ -1006,6 +1051,7 @@
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.
@@ -1037,11 +1083,10 @@
Second.Next := X;
X := Second;
end;
-
else
-- More than two elements; find second-to-last element
declare
- Walker : access List := X[ca];
+ Walker : access List := X[bs];
begin
while Walker /= null loop
declare
@@ -1074,6 +1119,7 @@
end if;
end Swap_Last_Two;
+
!ASIS
[Not sure. It might be necessary to have a query for the new aspects. - Editor.]
@@ -1425,11 +1471,21 @@
From: Tucker Taft
Sent: Monday, January 15, 2018 10:37 AM
-Here is an update to (well, really a complete re-write of) the AI on safe pointers with automatic storage management. It is available in various formats. We have been working on it in Google Docs, which allows commenting, suggestions, etc. So here is t
he link to that:
+Here is an update to (well, really a complete re-write of) the AI on safe
+pointers with automatic storage management. It is available in various formats.
+We have been working on it in Google Docs, which allows commenting, suggestions,
+etc. So here is the link to that:
https://docs.google.com/document/d/1pCIzY7ch1Zwa56MUNglzH4M_Ci3L90FvtZh9TBP5okg/edit?usp=sharing
-But I realize google-anything can be of concern to some folks. So I have attached a "plain text" version, and will send a "rich text" version separately (my first attempt to send a "rich text" version doesn't seem to have gotten past the various spam fil
ters). The plain text retains some indications of italic and bold fonts, I believe, which isn't particularly helpful, and has a list of the various comments at the end of the file, which is even less useful. At some point I will clean up the plain text v
ersion so it conforms with our normal lexical conventions, but in the mean time, hopefully this is adequate.
+But I realize google-anything can be of concern to some folks. So I have
+attached a "plain text" version, and will send a "rich text" version separately
+(my first attempt to send a "rich text" version doesn't seem to have gotten past
+the various spam filters). The plain text retains some indications of italic
+and bold fonts, I believe, which isn't particularly helpful, and has a list of
+the various comments at the end of the file, which is even less useful. At some
+point I will clean up the plain text version so it conforms with our normal
+lexical conventions, but in the mean time, hopefully this is adequate.
[This is version /02 of the AI.]
@@ -1438,20 +1494,76 @@
From: Randy Brukardt
Sent: Monday, January 15, 2018 10:02 PM
-The .RTF version was ginormous, so the list wouldn't send it. I've put a version into the Grab Bag, but of course Tucker updated the AI since his previous sending, so most likely you want to use one of these versions:
+The .RTF version was ginormous, so the list wouldn't send it. I've put a version
+into the Grab Bag, but of course Tucker updated the AI since his previous
+sending, so most likely you want to use one of these versions:
Text version:
http://www.ada-auth.org/ai-files/grab_bag/AI12-0240-1v7-stt.TXT
Rich Text version:
http://www.ada-auth.org/ai-files/grab_bag/AI12-0240-1v7-stt.rtf
-
-Or you can use the original Google Docs version (although that can change, so it's not useful for a permanent reference):
+Or you can use the original Google Docs version (although that can change, so
+it's not useful for a permanent reference):
https://docs.google.com/document/d/1pCIzY7ch1Zwa56MUNglzH4M_Ci3L90FvtZh9TBP5
okg/edit?usp=sharing
+
+P.S. I didn't really read it, but I did verify that the .rtf could be loaded
+successfully.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, January 24, 2018 10:37 AM
+
+I have new versions of this. I was planning to provide a "pdf" instead of an
+"rtf" plus a ".txt" file.
+
+I have attached a new ".txt" version, and I'll send the PDF directly to Randy.
+[This is version /04 of the AI - ED.]
+
+The major change was a more generalized 'Copy attribute, so it could be used
+more widely to prevent limitations that, for example, come with by-reference
+parameter passing. In addition, I tried to incorporate issues relating to the
+use of controlled types with subcomponents that are owning access objects.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, January 24, 2018 4:58 PM
+
+> I have attached a new ".txt" version, and I'll send the PDF directly
+> to Randy.
+
+You can find both of these in the Grab-Bag, see
+http://www.ada-auth.org/ai-files/grab_bag/AI12-0240-1v8-stt.TXT for the text
+version and http://www.ada-auth.org/ai-files/grab_bag/AI12-0240-1v8-stt.pdf
+for the PDF version.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, January 25, 2018 12:38 AM
+
+I've read little of this AI, but I note that you made the same mistake here
+that you did in container aggregates:
+
+If a type has a partial view, the Ownership aspect may be specified explicitly
+only on the partial view, and if specified True, the full type shall not be an
+elementary type nor an untagged private or derived type with Ownership aspect
+False; furthermore, if the Ownership aspect for the full type would be True if
+not explicitly specified, the Ownership aspect of the partial view shall be
+True, either by inheritance from an ancestor type or by an explicit
+specification.
-P.S. I didn't really read it, but I did verify that the .rtf could be loaded successfully.
+Since an aspect has the same value for all views, the full type will always
+have the same value. So rules like: "derived type with Ownership aspect False"
+can't ever happen and thus are vacuous.
+
+Note that this is the same reason that Preelaborable_Initialization (as
+currently defined) cannot be an aspect: it has different values for the
+partial and full views.
***************************************************************
Questions? Ask the ACAA Technical Agent