CVS difference for ai12s/ai12-0240-1.txt
--- ai12s/ai12-0240-1.txt 2017/11/30 04:18:02 1.3
+++ ai12s/ai12-0240-1.txt 2018/01/25 06:21:14 1.4
@@ -1,4 +1,5 @@
-!standard 3.10(14/3) 17-10-09 AI12-0240-1/01
+!standard H.7(0) 18-01-15 AI12-0240-1/02
+!standard H.8(0)
!class Amendment 17-10-09
!status work item 17-10-09
!status received 17-10-05
@@ -11,20 +12,37 @@
!problem
-When attempting to prove properties about a program, particularly programs
-with multiple threads of control, the enemy is often the unknown "aliasing"
-of names introduced by access types and certain uses of (potentially)
-by-reference parameters. By unknown aliasing of names, we mean the situation
-where two distinct names might refer to the same object, without the compiler
-being aware of that. A rename introduces an alias, but not an "unknown alias,"
-because the compiler is fully aware of such an alias, and hence is not
-something we are worrying about here. On the other hand, if a global variable
-is passed by reference as a parameter to a subprogram that also has visiility
-on the same global, the by-reference parameter and the global are now aliases
-within the subprogram, and the compiler generating code for the subprogram has
-no way of knowing that, hence they are "unknown" aliases. One approach is to
-always assume the worst, but that makes analysis much harder, and in some
-cases infeasible.
+Pointers (access types) are essential to many complex Ada data structures, but
+they also have significant downsides, and can create many kinds of safety and
+security problems. The question is can we create a subset of access-type
+functionality which supports the creation of interesting data structures without
+bringing all of the downsides. The notion of pointer "ownership" has emerged as
+one way to "tame" pointer problems, while preserving flexibility. The goal is
+to allow a pattern of use of pointers that avoids dangling references as well as
+storage leaks, by providing safe, immediate, automatic reclamation of storage
+rather than relying on unchecked deallocation, while also not having to fall
+back on the time and space vagaries of garbage collection. As a side benefit,
+we can also get safer use of pointers in the context of parallelism. This AI
+proposes the use of pointer ownership, as well as some additional rules
+preventing "aliasing" between parameters, and between pa meters and global
+variables, to provide safe, automatic, parallelism-friendly heap storage
+management while allowing the flexible construction of pointer-based data
+structures, such as trees, linked lists, hash tables, etc.
+
+When attempting to prove properties about a program, particularly programs with
+multiple threads of control, the enemy is often the unknown "aliasing" of names
+introduced by access types and certain uses of (potentially) by-reference
+parameters. By unknown aliasing of names, we mean the situation where two
+distinct names might refer to the same object, without the compiler being aware
+of that. A rename introduces an alias, but not an "unknown alias," because the
+compiler is fully aware of such an alias, and hence is not something we are
+worrying about here. On the other hand, if a global variable is passed by
+reference as a parameter to a subprogram that also has visibility on the same
+global, the by-reference parameter and the global are now aliases within the
+subprogram, and the compiler generating code for the subprogram has no way of
+knowing that, hence they are "unknown" aliases. One approach is to always
+assume the worst, but that makes analysis much harder, and in so cases
+infeasible.
Access types also introduce unknown aliasing, and in most cases, an analysis
tool will not be sure whether the aliases exist, and will again have to make
@@ -33,331 +51,806 @@
!proposal
This AI introduces a restriction against parameter aliasing
-(No_Parameter_Aliasing), and an aspect called "Ownership" for access types,
-which together can reduce unknown aliasing to the point that the only
-remaining unknown aliases involve references to elements of the same array
-using dynamic indices. This sort of aliasing is felt to be manageable by most
-analysis tools, as it is restricted to determining the possibility of numeric
-equality between such indices.
+(No_Parameter_Aliasing), and an aspect called "Ownership" for access types and
+composite types, which together provide safe, automatic storage management.
+Furthermore this set of features can reduce potential aliasing to the point that
+the only remaining potential aliases involve names denoting elements or slices
+of the same array using dynamic indices. This sort of aliasing is felt to be
+manageable by most analysis tools, as it is restricted to determining the
+possibility of numeric equality between such indices. Run-time checks are
+defined to deal with this sort of aliasing.
+
+Pointer ownership enables automatic storage reclamation since there is never
+more than one "owning" pointer to a given object, and the pointers are generally
+limited to pointing only at heap objects (never at a stack-allocated object or
+aliased component). This restriction matches that provided by "pool-specific"
+access types, so in this AI we limit the notion of pointer ownership for named
+access types to such types. We could incorporate a restricted set of "general"
+access types as well, but that would require more rules, and in this version we
+choose to go with the simpler, pool-specific-only, approach. We do permit use
+of certain objects of an anonymous access type, but these have restricted use,
+and in any case cannot be used with Unchecked_Deallocation.
+
Access type Ownership:
+
+If a pool-specific access-to-variable type has the value True for the aspect
+Ownership, then certain operations on the access type are restricted, and
+certain operations result in an automatic deallocation of the designated object.
+The Ownership aspect is inherited by derived types, and is non-overridable. On
+a root type, the Ownership aspect defaults to False. We also define the aspect
+on composite types and private types.
+
+The basic rule is that at most one object of such an access-to-variable type
+with Ownership True may be used to refer to a designated object at any time.
+There might be multiple access-to-variable (or access-to-constant) objects that
+designate the same object (or some part of it) at any given time, but at most
+one of them may be dereferenced. All of the others are considered "invalid,"
+because their value has been "borrowed" (see further below).
+
+Conversely, there might be multiple "valid" access-to-constant objects that
+designate a given object, so long as all access-to-variable objects designating
+the object are at that point invalid (or "observed" -- see below). This is the
+usual "single writer, multiple reader" rule for safe access to a shared
+variable.
+
+We say an access-to-variable object is "observed" when its value has been
+"observed", and such an object can only be used for read-only access to the
+designated object.
+
+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
+ some part of the designated object is passed as a potentially by-ref [IN] OUT
+ parameter. Finally, it also covers the case where a subcomponent that is
+ itself an access-to-variable with ownership, is borrowed. The state reverts
+ to unrestricted when the short-lived reference no longer exists.
+
+An access-to-variable object of a named type that is unrestricted or observed is
+considered to be the "owner" of its designated object. There should be exactly
+one owner of every existing object created by an allocator for an access type
+with a True Ownership aspect. While observed, the access object is itself
+read-only. When an object is borrowed, ownership has been temporarily
+transferred to another object, and while in such a state the original access
+object is not usable at all.
+
+Ownership is transitive, in that if a pointer owns a designated object, it
+indirectly owns every object owned by one of its access subcomponents.
+
+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
+ 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)
+
+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
+possibility of exceptions, because pass-by-copy for [in] out composite
+parameters could produce dangling references if a subprogram propagated an
+exception that was then caught. (Ownership aspect is not defined at all for
+scalar types, and we don't allow a private type with Ownership aspect True to be
+of a by-copy type.)
+
+Note that the rules are actually expressed in terms of "names" rather than
+"objects" since objects don't really exist at compile-time. In the rules, we
+distinguish "static" names from "dynamic" names, where static names are those
+made of names denoting stand-alone objects, dereferences of owning/observing
+access objects, and selected components, while "dynamic" names can involve
+indexing or slicing.
+
+!wording
+
+Add the following sections to Annex H:
+
+H.7 The Ownership Aspect
+
+This section describes the Ownership aspect, which can be specified for an
+access type so that there can be either one writable access path to an object
+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]
+
+Static Semantics
+
+The following aspect may be specified for a named access-to-object type, a
+stand-alone object (including a generic formal in-mode object) of an anonymous
+access-to-object type, or a composite type:
+
+Ownership
+
+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
+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
+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
+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 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
+ (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.
+
+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
+of the class.
+
+An access-to-variable type with Ownership aspect True is called an owning access
+type. Similarly, an object of an owning access type is called an owning access
+object. An access-to-constant type with Ownership aspect True is called an
+observing access type. Similarly, an object of an observing access type is
+called an observing access object. Finally, an object that is a part of an
+object with Ownership aspect True, or a part of the dereference of an owning or
+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.]
+
+ 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
+ Ownership aspect True to have a full type that is a by-copy type, so this
+ effectively means that all non-access types with Ownership aspect True are
+ necessarily by-reference types.
+
+ AARM Ramification: An observing access object is never an exclusive owner of
+ its designated object; while it exists it may be dereferenced to produce a
+ constant view, which can be passed around, read in parallel, etc.
+
+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.
+
+Any other name that denotes an object, other than an aggregate or the result of
+a function call (or part thereof), is a dynamic name. Names that denote an
+aggregate or the result of a function call, or part thereof, have their own set
+of rules.
+
+ AARM Reason: We considered specifying that indexed components having static
+ index expressions were also static names, but chose to leave them out, since
+ they can be aliased with names that have dynamic index expressions. So
+ currently a static name and a dynamic name are never "peer" aliases, and it
+ is trivial for the compiler to determine whether two static names denote the
+ same object. On the other hand, determining whether two dynamic names denote
+ 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[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.
+
+ AARM Reason: A renaming can be an implicit borrowing if the renamed object is
+ part of a dereference of an owning access object, so we want to go "through"
+ the renaming, rather than re-dereference the owning access object (which has
+ been implicitly "borrowed" in any case).
+
+Two names with the same root object statically overlap when one is a static name
+and the other denotes the same object, or has a static prefix that denotes the
+same object.
+
+ 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.
+
+A static name that denotes a managed object can be in one of the following
+ownership states:
+
+* unrestricted -- the name may be used as defined elsewhere in this standard,
+ and if it denotes an owning access object, a dereference of the name provides
+ a variable view;
+
+* observed -- the name provides a constant view, and if it denotes an owning
+ access object, it may be used as the prefix of a dereference, but the
+ dereference is similarly a constant view;
+
+* borrowed -- the name is not usable when in this state; the name has
+ temporarily relinquished ownership to a borrower;
+
+If a static name is in the observed or borrowed state, then any other static
+name with the same root object that denotes the same object is in the same
+ownership state.
+
+ AARM Reason: This is a desirable property. We don't want the exact form of a
+ static name to affect its state.
+
+A dynamic name that denotes a managed object can also be in the observed or
+borrowed state, but in addition it can be in a dynamic ownership state where
+run-time checks may be necessary to determine its (run-time) ownership state. If
+a name (static or dynamic) that denotes a managed object has a prefix that is in
+the observed or borrowed state, then the name is similarly in the observed or
+borrowed state (respectively). If a dynamic name that denotes a managed object
+is not in the observed or borrowed state because of this rule, then it is in the
+dynamic ownership state.
+
+ AARM Ramification: In this case we know that any static prefix must be in the
+ unrestricted state rather than observed or borrowed. Run-time checks may be
+ required when using dynamic names that have a dynamic ownership state.
+
+Certain operations are considered to observe, borrow, or move the value of a
+managed object, which might affect whether a name that denotes the object is
+considered to be in the unrestricted, observed, borrowed, or dynamic ownership
+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
+ 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”
+ 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:
+ * 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
+ 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
+ name denotes the source of the assignment.
+
+ AARM Reason: We handle the case of assignment to named owning access types as
+ a special case below under borrowing. Managed objects that do not have
+ Ownership aspect True can be freely copied, since they necessarily have no
+ 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]
+
+ 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
+ access-to-variable, then it is considered borrowing (see below). If the
+ formal is neither composite nor aliased, the parameter is guaranteed to be
+ passed by copy and no long-lived "observer" of the managed object is being
+ created.
+
+At the point where a name denoting a managed object is observed, the state of
+the name becomes observed, and remains so until the end of the scope of the
+observer. While a name that denotes a managed object is in the observed state
+it provides a constant view.
+
+ AARM Reason: We want the managed object to still designate the same object(s)
+ until all the observers go away, so we disallow updating the object.
+
+At the point where a static name that denotes a managed object is observed,
+every static name that denotes the same managed object is observed, and every
+name with that static name as a prefix, is similarly observed.
+
+ AARM Ramification: This applies recursively down the tree of managed objects,
+ meaning that observing a managed object effectively observes 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 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
+ formal object) of a (named or anonymous) access-to-variable type;
+
+ AARM Reason: This supports traversing a data structure with the ability to
+ modify something, without losing a handle on the root of the structure.
+ Unlike subcomponents of a constant, IN parameters and stand-alone constants
+ of an owning access type still provide read/write access. This is to
+ accommodate existing practice in the use of constants of an access type to
+ still be used to update the designated object. Note that as soon as the
+ object becomes a component of a larger constant, we treat everything "owned"
+ by a composite constant as itself being constant. Note that we don't
+ consider this a complete transfer of ownership (i.e. a "move") because we
+ don't want the sole owner to be a constant, since we can't set it to null if
+ we move the value out of the object.
+
+ * A call (or instantiation) where the name denotes an actual parameter that
+ is a managed object other than an owning access object, and the formal
+ 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.
+
+ * Object renaming [aa][ab]where the name is the object_name denoting the
+ renamed object, when the renamed object is not in the observed or borrowed
+ state.
+
+ AARM Reason: We are effectively borrowing the object, because we want to be
+ sure the designated object is not deallocated while the renaming exists. If
+ it has already been borrowed, such a rename would not be permitted. If it
+ has already been observed, then the renaming provides a constant view, but
+ that does not change the ownership state of the object -- it remains
+ "observed."
+
+At the point where a name denoting a managed object is borrowed, the state of
+the name becomes borrowed, and remains so until the end of the scope of the
+borrower. While a name that denotes a managed object is in the borrowed state
+it provides a view that allows neither reading nor updating.
+
+ AARM Reason: We want the name to still designate the same object(s) until the
+ borrower goes away, so we disallow updating via a borrowed name. We also
+ disallow moving, borrowing, observing, and dereference (see below in legality
+ rules). So effectively a name that is borrowed is completely "dead" until
+ the borrowing ends.
+
+At the point where a static name that denotes a managed object is borrowed,
+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.
+
+
+* 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.
+
+ 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.
+
+ AARM Reason: These operations are considered "moves" because they result in a
+ transfer of ownership, and possibly a deallocation of the object designated
+ by the target beforehand, or a setting to null of the source afterward (see
+ dynamic semantics below). Note that this does not include by-reference
+ 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
+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.
+
+ AARM Reason: If the full type might contain an owning component, then it is
+ important that the partial view indicates that. On the other hand, if the
+ partial view has Ownership True, it is OK if the full view is tagged but
+ would not be considered to have Ownership aspect True merely due to its
+ components or parent. We disallow having a full type that is untagged
+ private or derived with Ownership aspect False, because such types might be
+ by-copy types, and we want private types with Ownership aspect True to always
+ be by-reference types, to avoid problems with exceptions propagation leaving
+ dangling references.
+
+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].
+
+ 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
+ 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
+ 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.
+
+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
+the prefix is of a type with Ownership aspect True. [Redundant: A function
+call, aggregate, or allocator of such a type can be assigned to an object of a
+named type (including a parameter), which can then be used as a prefix for
+selecting components or dereferencing.]
+
+ 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
+ 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.
+
+An Access or Unchecked_Access attribute reference shall not be of a type with
+the Ownership aspect True, unless the prefix denotes a managed object, and the
+value is directly used to initialize a stand-alone object of an anonymous access
+type, or an in parameter of an anonymous access type; this is considered
+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
+ 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]
+
+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]
+
+ AARM Reason: [ap][aq][ar][as][at]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
+that anonymous access types are never convertible to (named) pool-specific
+access types (see 4.6).]
+
+ AARM Ramification: A specific type cannot be converted to a class-wide type
+ if the Ownership aspect of the specific type differs from that of the root
+ 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.
+
+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];
+
+ AARM Reason: At its declaration, such an owning access object can be
+ initialized from any owning access object in the unrestricted state. On
+ subsequent assignment statements, such an object can only be set to point to
+ somewhere in the "tree" headed by its prior value. Hence, you can use it to
+ walk exactly one tree -- you can't jump between different trees using the
+ 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.
+
+ AARM Reason: At its declaration, such an observing access object can be
+ initialized from any owning access object in the unrestricted or observed
+ state, but on subsequent assignment statements, it can only be assigned from
+ objects rooted at an observer that lives at least as long as this observer.
+
+For managed objects:
+
+* While the state of a name that denotes a managed object is observed, the name
+ 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.
+
+* 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;
+
+ AARM Reason: The object has been borrowed, and should not even be observed
+ other than via the borrower.
+
+* If the source of a "move" is a name that denotes an object with Ownership
+ aspect True, other than a function call, the name shall be a variable
+ [Redundant: that is not in the observed or borrowed state]; furthermore, there
+ shall be no name that statically overlaps this name that is in the observed or
+ borrowed state;
+
+ 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.
+ 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.
+
+* 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
+ target callable entity (as restricted by the value of its Global aspect and
+ the restrictions imposed by the No_Parameter_Aliasing restriction -- see
+ below) shall not be in the observed or borrowed state. Similarly, any name
+ that denotes a managed object that might be read (but not written) as part of
+ the call, shall not be in the borrowed state.
+
+ AARM Reason: We want to be able to assume that all relevant writable globals
+ are unrestricted when a subprogram starts executing, and all read-only
+ globals are not borrowed.
+
+Dynamic Semantics
+
+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
+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.]
+
+ AARM Reason: If we didn't set it to null, an exception might allow the old
+ value of the variable to be used after handling the exception, which would be
+ bad if the designated object had been deallocated prior to raising the
+ exception.
+
+When a new value is assigned to a variable of a named owning access type, if the
+prior value is non-null and does not match the new value, the object designated
+by the prior value is finalized, and its storage deallocated. If the value being
+assigned matches the prior value of the target, there is no effect. This
+applies to each subcomponent having a named owning access type, in an assignment
+to a composite object.
+
+ AARM Reason: When an owning access object of a named type can legally be
+ assigned, that means there are no borrowers or observers in existence, so it
+ is safe to reclaim the storage. Objects of an anonymous type never truly
+ "own" an object, though they can be the unique borrower. Note that we don't
+ want to rely on the general finalization rule (see below) for handling the
+ left-hand side of an assignment, because we have the extra test that the new
+ and old values differ.
+
+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
+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
+ not complete normally, no copy-back occurs, and we must perform the
+ finalization action to avoid a storage leak.
+
+ 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”
+ 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
+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.]
+
+ AARM Reason: We are attempting to prevent storage leakage via constants that
+ effectively "own" an object created at the time of their initialization, if
+ initialized by a function call, aggregate, or allocator.
+
+For managed objects denoted by a dynamic name, checks are used to ensure that no
+other name that is a potential alias is in a conflicting state. Two names are
+potential aliases when:
+
+* both names statically denote the same entity;
+
+* both names are selected components with the same selector and with prefixes
+ that are potential aliases;
+
+* both names are indexed components, with prefixes that are potential aliases,
+ and corresponding indexing expressions that are both static, if any, have the
+ same value;
+
+* both names are slices, with prefixes that are potential aliases, and the
+ corresponding discrete_ranges are overlapping in the case when both are static
+ ranges;
+
+* one name is a slice whose prefix is a potential alias of the other name;
+
+* one is a slice and the other is an indexed component, with prefixes that are
+ potential aliases, and for the case when both the discrete_range and the
+ indexing expression are static, the value of the indexing expression is within
+ the range;
+
+* both names are dereferences, with prefixes that are potential aliases;
+
+* both are aliased views having the same type, and at least one of them is a
+ dereference of a non-owning access type;
+
+* one denotes an object renaming declaration, and the other denotes the same
+ renaming declaration, or is a potential alias with the object_name denoting
+ the renamed entity.
+
+Two names N1 and N2 potentially overlap if some prefix of N1 is a potential
+alias of N2, or some prefix of N2 is a potential alias of N1. The prefix and
+the name that are potential aliases are called the potentially aliased parts of
+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
+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]
+
+ AARM Ramification: This requires keeping track of what potentially aliased
+ (see above) dynamic names are observed (or borrowed), and doing checks that
+ there are none that overlap with this name or any part of the tree rooted at
+ 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
+ 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?]
+
+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
+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,
+unless both operations are read only, or one operation is read only, and it
+occurs strictly before the second operation where it might be updated.
+
+ AARM Reason: We could allow two updates, if one occurs strictly before the
+ second update, but for now we disallow two updates to the same object within
+ 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:
+
+* The first occurs within an expression, and the result of the expression is an
+ operand to the second;
+
+* The first occurs within the left operand of a short-circuit control form, and
+ the second occurs within the right operand of the same short-circuit control
+ form;
+
+* The first occurs within the condition or selecting_expression of a
+ conditional_expression, and the second occurs within a dependent_expression of
+ the same conditional_expression; or
+
+* The first operation occurs strictly before some other operation, that in turn
+ occurs strictly before the second.
+
+Static Semantics
+
+The following restriction_identifier is language defined:
+
+No_Parameter Aliasing
+
+If the No_Parameter_Aliasing restriction applies to the declaration of a
+callable entity, then the following rules apply on calls to such an entity;
+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
+ 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;
+
+ 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
+ before the second operation, because of the possible side-effect of nulling
+ out an access object as part of passing it as an in-out parameter.
+
+Dynamic Semantics
+
+In a context where the No_Parameter_Aliasing restriction disallows static
+overlap between two names, and the names potentially overlap (see H.7), a check
+is made, after evaluating the potentially conflicting operand(s) but before
+invoking the operation(s), that there is in fact no overlap between the
+potentially aliased parts of the two names. Program_Error is raised if this
+check fails.
+
+
+[end of H.8]
-If an access-to-variable type has the value True for the aspect Ownership,
-then certain operations on the access type are restricted, and certain
-operations result in an automatic deallocation of the designated object.
-
-The basic rule is that at most one object of such an access-to-variable type may
-be used to refer to the designated object at any time. There might be multiple
-access-to-variable (or access-to-constant) objects that designate the same
-object at any given time, but at most one of them may be dereferenced. All of
-the others are considered "invalid." Conversely, there might be multiple
-"valid" access-to-constant objects that designate a given object, so long as all
-access-to-variable objects designating the object are at that point invalid (or
-"read-only-valid" -- see below). This is the usual "single writer, multiple
-reader" rule for safe access to a shared variable.
-
-An access-to-variable object can also become "read-only-valid," which means that
-it can only be used for read-only access to the designated object. Finally, an
-access-to-variable object can become "frozen invalid" which means it is invalid,
-but further it cannot be re-assigned a new value.
-
-An access-to-variable object that is valid or read-only-valid is considered to
-be the "owner" of its designated object. There should be exactly one owner of
-every existing object created by an allocator for an access type with a True
-Ownership aspect. While read-only-valid, the access object is itself considered
-read-only.
-
-Certain operations change which objects are valid, read-only-valid, invalid, or
-frozen invalid, to preserve the above overall objective. In addition, automatic
-deallocation occurs at certain points:
-
-* Default initialization of an access-to-variable object (including a component)
- of a type with a True Ownership aspect:
- # Static semantics: The object starts out as valid but null. The rules
- governing the initial assignment if any are covered below,
- as are assignments from a later assignment statement.
-
-* Creating values
- # Legality rule: The attributes Access and Unchecked_Access shall not be
- used to create a value of an access type with a True Ownership aspect.
-
-* Converting values
- # Legality rule:
- In a type conversion, if the target type is an access type with Ownership
- aspect having the value True:
- + The operand type shall also have the Ownership aspect True;
- + The storage pool of both the operand and target type shall be the
- standard storage pool, or both shall be non-standard storage pools.
- # Dynamic semantics:
- In a type conversion between two types with Ownership aspect True,
- where both have non-standard storage pools, a check is made that the
- Storage_Pool attribute of the two types denote the same object.
- Program_Error is raised if this check fails.
-
-* Assignment to an access-to-variable object:
- # Legality rule: The RHS shall be valid, an allocator, or the literal null.
- If not a null literal or an allocator, the RHS shall be local to the
- nearest enclosing body (or be a parameter thereof).
- The LHS shall not be read-only-valid nor frozen invalid.
- # Static semantics: The LHS becomes valid, and the RHS becomes invalid
- (if not the literal "null" or an allocator).
- [Ownership is transfered to the LHS.]
- # Dynamic semantics: If the LHS is valid and non-null prior to the
- assignment, the object it designates is finalized and deallocated.
-
-* Assignment to an access-to-constant object:
- # Legality rule: The RHS shall be valid or read-only-valid
- (we ignore here cases where the RHS is null or an allocator).
- The RHS shall be local to the nearest enclosing body
- (or be a parameter thereof).
- The accessibility level of the type of the LHS shall be deeper than
- that of the nearest enclosing body.
- # Static semantics: The LHS becomes valid, and the RHS becomes read-only
- valid.
- [Redundant: Ownership of the designated object is not transferred, but the
- access object itself and the designated object are both now effectively
- read-only.]
- The RHS remains read-only-valid until the master of the type of the LHS
- is finalized.
-
-* Assignment to a composite variable with some access object subcomponents
- # Equivalence:
- Legality checks and semantics are those of an equivalent set of individual
- subcomponent assignments, presuming the array subcomponents all use
- static indices (see Arrays section below).
-
-* Assignment to a composite constant with some access object subcomponents
- (as part of initialization, presumably)
- # Legality rule: All access object subcomponents of the RHS shall be
- valid or read-only-valid.
- # Static semantics:
- If the RHS is an aggregate or build-in-place function call, the LHS and
- the RHS are considered a single object for the purposes of these rules.
- and the access subcomponents are considered valid.
- If the RHS is an existing object, the access subcomponents of the
- LHS are read-only-valid, and the access subcomponents of the RHS become
- read-only-valid, and remain so until the finalization of the LHS, at
- which point they are restored to their prior state.
-
-* Dereference
- # Legality rule: The access object shall be valid or read-only-valid
- # Static semantics: A dereference of a read-only-valid access object
- provides a constant view of the designated object (even though the
- access object is of an access-to-variable type).
- A dereference of a valid access-to-variable object provides a
- variable view and takes ownership of the object; in this case
- the access object is frozen invalid as long as the dereference exists.
- [NOTE: This allows the data structured rooted at this object to
- be walked with the pointer to the root restored to validity
- at the end of the lifetime of the dereference; renaming or passing
- as a parameter can be used to extend the lifetime of the dereference
- over the period of exploration of the data structure.]
-
-* Component selection
- # Static semantics: An access object that is a subcomponent
- of a constant view is considered read-only-valid. [Redundant:
- An access object that is a subcomponent of a variable view can be
- valid, read-only-valid, invalid, or frozen invalid according to what
- operations have been applied to it or the enclosing object.]
-
-* Parameter passing, IN parameter
- + If the formal parameter is of an access-to-variable type:
- # Legality rule: The actual shall be valid, the literal null, or an
- allocator.
- # Static semantics: At the point of call,
- the formal becomes valid and the actual becomes
- frozen invalid (if not the literal null or an allocator).
- At the end of the subprogram, the actual becomes valid again;
- if the actual is an allocator the object is reclaimed at this point.
- + If the formal parameter is of an access-to-constant type:
- # Legality rule: The actual shall be valid or read-only-valid
- (we ignore the literal "null" or allocators in this case).
- # Static semantics; At the point of call the actual becomes
- read-only-valid; the formal starts out (and remains throughout
- its existence) read-only-valid.
- At the end of the subprogram, the actual is restored to its prior state.
- + If the formal parameter is a composite object with access subcomponents:
- # Legality rule: All access subcomponents of the actual shall be valid
- or read-only-valid.
- # Static semantics: All access subcomponents of the actual become
- read-only-valid. The access subcomponents of the formal are
- read-only-valid throughout their existence.
- At the end of the subprogram, the access subcomponents of the actual are
- restored to their prior state.
- If the actual is an aggregate, all of the access subcomponents
- are finalized[Redundant:, reclaiming any objects they designate if
- non-null].
-
-* Parameter passing, IN OUT parameter
- + If the formal parameter is of an access-to-variable type:
- # Legality check: The actual shall be valid at the point of call.
- At a return statement or the end of the subprogram, the formal shall
- be valid.
- # Static semantics: At the point of call, the formal becomes valid and
- the actual becomes frozen invalid.
- After the call, the actual becomes valid again.
- + If the formal parameter is of an access-to-constant type: illegal.
- + If the formal parameter is a composite object with access subcomponents:
- # Equivalence: This is equivalent to having a set of IN OUT formal
- parameters, one for each such access subcomponent, with the corresponding
- subcomponent of the actual being passed to the subcomponent of the
- formal.
-
-* Parameter passing, OUT parameter
- + If the formal parameter is of an access-to-variable type:
- # Legality check: At the point of call, the actual shall not be
- read-only-valid.
- At a return statement or the end of the subprogram,
- the formal shall be valid.
- # Static semantics: At the point of call, the actual becomes
- frozen invalid (which it might already be), and the formal starts out
- invalid.
- After the call, the actual becomes valid.
- # Dynamic semantics: Upon return from the subprogram, if the original
- value of the actual was valid, and the final value
- of the formal is not the same as that of the original value of the
- actual, the object designated by the actual is finalized and
- deallocated, prior to copying back from the formal to the actual.
- + If the formal parameter is of an access-to-constant type: illegal.
- + If the formal parameter is a composite object with access subcomponents:
- # Equivalence: This is equivalent to having a set of OUT formal
- parameters, one for each such access subcomponent, with the corresponding
- subcomponent of the actual being passed to the subcomponent of the
- formal.
-
-* Arrays
- # Static semantics: An array as a whole can be valid, read-only-valid,
- or invalid, or the array can be statically partitioned into three
- sets of components, one the valid components, one the read-only-valid
- components, and one the invalid components (the "as a whole" cases
- can be seen as special cases of this more general case, with two of
- the three partitions being empty).
- If other rules would indicate that a statically-indexed component is
- made valid, read-only-valid, or invalid, that one component is affected.
- If other rules would indicate that a dynamically-indexed component
- is made read-only valid, the entire array becomes read-only-valid.
- # Legality rules:
- If a legality rule requires a dynamically-indexed
- array component to be valid or read-only-valid, the array shall
- have no components that violate the requirement.
- If other rules would indicate that a dynamically-indexed
- component is to become valid or invalid, all components of the array
- shall already have that status. [Redundant: Note this implies
- that you cannot transfer ownership from a dynamically indexed
- subcomponent, as that action would necessarily require that it be
- valid before, and invalid afterward. You can make a read-only copy of
- one that is valid or read-only-valid, resulting in the whole array
- becoming read-only-valid. You can also assign into one that is already
- valid, as that preserves the state.]
-
-* Finalization of an object (including a component) being of an access type
- with a True Ownership aspect.
- # Legality check: An access-to-variable object that was valid when
- initialized shall not be read-only-valid when finalized.
- # Dynamic Semantics:
- When an access-to-variable object is finalized, if the object
- is valid, the object it designates (if any) is finalized and
- deallocated.
-
-Control flow:
-
-# Legality Rule: When two control paths converge within a subprogram, such as
- the "then" and "else" part of an "if" statement, or the statements before a
- loop and the end of the body of the loop, the status of an access object shall
- not be valid or read-only valid on one path, while being invalid or frozen
- invalid on the other.
-# Static Semantics: If the status is the same on both paths, the status remains
- that at the join point. If the status on either path is read-only-valid, the
- status is read-only-valid after the join point. Similarly, if the status on
- either path is frozen invalid, the status is frozen invalid after the join
- point.
-
-TBD: Conversion rules? 'Access?
-
-No_Parameter_Aliasing Restriction:
-
-The No_Parameter_Aliasing restriction disallows passing overlapping parts of a
-single variable as a composite or aliased parameter, more than once within the
-same expression or simple statement, unless all are as IN parameters.
-Furthermore, a part of a variable that is global to the called subprogram or
-task entry may not be passed as a parameter if the formal is composite or
-aliased, unless the Global aspect that applies to that subprogram implies that
-it makes no reference to that part of the global variable, or it makes only read
-references to that part of the global variable, and the part is passed as an IN
-parameter. Variables of a private type are presumed composite, for the purpose
-of this rule.
-
-If two parts of the same array are passed as composite or aliased parameters in
-the same expression or simple statement, and at least one is an OUT or IN OUT
-parameter, a check is made that the parts do not overlap. If this check fails,
-Program_Error is raised. A corresponding check is performed if the Global
-aspect of the called subprogram identifies a part of an array, to ensure that an
-overlapping part of that array is not passed as a composite or aliased
-parameter, if either the formal or the global is writable in the called
-subprogram.
-
-If parts of two dereferences of the same type are passed as composite or aliased
-parameters, and at least one of them is an OUT or IN OUT parameter, and the
-parts would overlap if the dereferenced access values were the same, a check is
-made that the access values are not the same. If this check fails,
-Program_Error is raised.
-
-[NOTE: The above is a bit naive, and needs more words to deal with cases like
-slice of dereference of access-to-array, etc. But hopefully you get the idea!
-Also, if all access types have Ownership, the last check should never be
-necessary. Note further than this does not worry about aliasing which occurs
-internal to the subprogram due to dereferencing an access value, as that is
-considered something that can only be dealt with effectively using the Ownership
-aspect.]
-
-[Possible Alternative: Drop the "composite or aliased" part in all the above
-paragraphs. It seems like a minor capability to be allowed to pass the same
-elementary object as both an IN and an [IN] OUT parameter, and this change would
-obviate the need to do the additional subtle Ada 2012 checks for cases where the
-same elementary object appears more than once as an [IN] OUT parameter. Perhaps
-parenthesizing of an IN parameter that is the name of a variable could be used
-to mean the compiler may insert a copy at that point to break aliasing?]
+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
-No_Parameter_Aliasing restriction, is to reduce aliasing to the point where
-programs using pointers and pass-by-reference can nevertheless be fully
-analyzed, in particular for compile-time detection of data races.
+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
+pass-by-reference can nevertheless be fully analyzed, in particular for
+compile-time detection of data races.
The Ownership aspect is a relatively simple idea, where an object is owned by
exactly one pointer at any time. When an object is owned, it can be deallocated
-when the owner is assigned to be null or point at a different object. We want
+when its owner is assigned to be null or point at a different object. We want
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. Most commonly these will probably be
-stand-alone objects of an anonymous access-to-constant type.
+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
+an anonymous access-to-object type, though an IN parameter of a named
+access-to-variable type also acts as a borrower.
+
+Similarly, a long-lived dereference of the root of a data structure (e.g. as
+part of parameter passing) is considered borrowing and may be used to walk a
+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.
+
+As noted we have four states for an access object: unrestricted, observed,
+borrowed, and dynamic. An unrestricted access object is the owner, and provides
+read-write access to the designated object. Assigning a new value to an
+unrestricted access object causes the prior designated object to be deallocated.
+An observed access object is a shared owner, and provides read-only access to
+the designated object. An observed access object cannot itself be set to point
+elsewhere. A borrowed access object is not useful until the borrowers go away.
+
+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
+structure manipulations.
-Similarly, a long-lived dereference of the root of a data structure may be used
-to walk a data structure destructively, while restoring the validity 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 dereference exists.
-
-As noted we have four states for an access object: valid, read-only valid,
-invalid, and frozen invalid. A valid access object is the owner, and provides
-read-write access to the designated object. Assigning a new value to a valid
-access object causes the prior designated object to be deallocated. A
-read-only-valid access object is a shared owner, and provides read-only access
-to the designated object. A read-only-valid access object cannot itself be set
-to point elsewhere. An invalid access object is not useful until it is assigned
-a valid value, or until its validity is restored because all copies have been
-finalized. A frozen invalid access object cannot be copied and cannot be
-assigned a new value, and is used to represent a state of an access object that
-is necessarily transitory due to the existence of another (temporary) owner,
-such as a dereference or a formal parameter.
-
-Tracking validity of stand-alone access objects is pretty straightforward.
-Tracking validity of components is more challenging, and perhaps additional
-rules over and above those given above will be needed. In particular, we have
-proposed rules for dynamically-indexed array components. They will need to be
-studied and used in examples to know whether they are adequate and usable.
-
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
@@ -368,6 +861,119 @@
inspired by the "borrow checker" of the Rust language, and/or the anti-aliasing
rules of the ParaSail language and the SPARK language.
+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
+desired safety properties:
+
+1. For any heap object that was created using an allocator of an owning access
+ type, and not yet deallocated, one of the following is true:
+
+ * There is exactly one name in the unrestricted state denoting an owning
+ access object that designates the heap object; or
+
+ * 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.
+
+1. When such a heap object is deallocated, there are no access objects
+ designating it.
+
+2. Names in the borrowed state provide no access to the designated object.
+
+3. Names in the observed state provide read-only access to the designated
+ 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.
+
+
+!examples
+
+
+Here is an example of swapping two elements of a singly linked list.
+
+
+ type List;
+ type List_Ptr is access List with Ownership;
+
+ type List is record
+ Next : List_Ptr;
+ Data : Data_Type;
+ end record;
+
+ procedure Swap_Last_Two (X : in out List_Ptr) is
+ -- Swap last two elements of list
+ -- (no effect if list has less than two elems)
+ begin
+ if X = null or else X.Next = null then
+ -- List does not have two elements
+ return;
+ else if X.Next.Next = null then
+ -- List has exactly two elements
+ declare
+ Second : List_Ptr := X.Next;
+ -- Second cannot be a constant because it
+ -- will be nulled after a “move”
+ begin
+ -- 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];
+ begin
+ while Walker /= null loop
+ declare
+ Next_Ptr : List_Ptr renames Walker.Next;
+ begin
+ if Next_Ptr /= null
+ and then Next_Ptr.Next /= null
+ and then Next_Ptr.Next.Next = null
+ then
+ -- Found second-to-last element
+ declare
+ Last : List_Ptr := Next_Ptr.Next
+ -- Last cannot be a constant because it
+ -- will be nulled after a “move”
+ begin
+ -- Swap last two
+ Next_Ptr.Next := null; -- not really necessary (already null)
+ Last.Next := Next_Ptr;
+ Next_Ptr := Last;
+ return; -- All done
+ end;
+ end if;
+ end;
+ -- Go to next element
+ -- Note that we need to do this *after* the “borrowing”
+ -- inherent in the renaming of Walker.Next is complete.
+ Walker := Walker.Next;
+ end loop;
+ end;
+ end if;
+ end Swap_Last_Two;
+
!ASIS
[Not sure. It might be necessary to have a query for the new aspects. - Editor.]
@@ -405,7 +1011,7 @@
rules over and above those given above will be needed. In particular, we
have proposed rules for dynamically-indexed array components. They will
need to be studied and used in examples to know whether they are adequate
- and usable.
+ and usable.
I don't think the ARG is the place to develop these sorts of rules. In addition
to the proposed rules, there need to be rules for dealing with this in
@@ -471,7 +1077,7 @@
Sent: Friday, October 6, 2017 10:31 AM
> Interesting, and clearly some work has gone into this. But...
->
+>
> 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.
@@ -489,7 +1095,7 @@
every Ada compiler already does some amount of control flow, merely to provide
helpful warnings. This would be the first time we would make legality depend
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.
@@ -534,10 +1140,10 @@
---
-> You are correct that this would introduce some control-flow based
-> checks, and there are many checks that could take advantage of that.
-> In fact, almost every Ada compiler already does some amount of control
-> flow, merely to provide helpful warnings. This would be the first
+> You are correct that this would introduce some control-flow based
+> checks, and there are many checks that could take advantage of that.
+> In fact, almost every Ada compiler already does some amount of control
+> flow, merely to provide helpful warnings. This would be the first
> time we would make legality depend on that, which is worth considering!
So far as I know, only GNAT uses front-end flow analysis for "helpful
@@ -581,7 +1187,7 @@
You may not buy the rationale, but in my view, safe storage management is a
huge issue, and many languages have adopted full garbage collection, not
because it is a "good thing," but merely because having to deal with storage
-leaks and dangling references is so painful.
+leaks and dangling references is so painful.
I think if Ada had a "mode" in which all storage management was safe and
automatic, and there were no dangling references or storage leaks, and yet
@@ -602,10 +1208,10 @@
From: Randy Brukardt
Sent: Monday, October 9, 2017 9:07 PM
-> You may not buy the rationale, but in my view, safe storage management
-> is a huge issue, and many languages have adopted full garbage
+> You may not buy the rationale, but in my view, safe storage management
+> is a huge issue, and many languages have adopted full garbage
> collection, not because it is a "good thing,"
-> but merely because having to deal with storage leaks and dangling
+> but merely because having to deal with storage leaks and dangling
> references is so painful.
You didn't give that as a rationale! The only thing the AI talks about is
@@ -614,12 +1220,12 @@
I'm surely not against "safe storage management" (that would be like being
against apple pie!), but I don't see how the features in the AI provide
anything safe. (Quite the reverse in fact, unless one assumes things about the
-TBDs known only to the author.)
-
-> I think if Ada had a "mode" in which all storage management was safe
-> and automatic, and there were no dangling references or storage leaks,
-> and yet also no asynchronous garbage collector meaning that real-time
-> guarantees are straightforward, all in the presence of multitasking
+TBDs known only to the author.)
+
+> I think if Ada had a "mode" in which all storage management was safe
+> and automatic, and there were no dangling references or storage leaks,
+> and yet also no asynchronous garbage collector meaning that real-time
+> guarantees are straightforward, all in the presence of multitasking
> and/or parallelism, this would be truly extraordinary.
Yes, it would be truly extraordinary. I'd actually say impossible. :-)
@@ -681,14 +1287,14 @@
From: Raphael Amiard
Sent: Thursday, October 12, 2017 9:11 AM
-> I noted that the !problem seems to concentrate totally on the problems
+> I noted that the !problem seems to concentrate totally on the problems
> of static analysis tools. It starts:
>
> "When attempting to prove properties about a program, ..."
>
-> I'd argue that a large proportion of Ada users aren't planning to do
-> that anytime soon. And arguably, static analysis tools can solve their
-> own problems (as you say is being done with SPARK). So what's the
+> I'd argue that a large proportion of Ada users aren't planning to do
+> that anytime soon. And arguably, static analysis tools can solve their
+> own problems (as you say is being done with SPARK). So what's the
> value of this proposal to the average Ada user?
In my opinion you're drawing a line in the sand that is not so clearly
@@ -696,7 +1302,7 @@
properties about a program, and it is part of the compiler, not of an external
static analysis tool.
-In this instance, the value of this proposal is to solve a class of memory
+In this instance, the value of this proposal is to solve a class of memory
problems in the language directly, instead of relying on static analysis
tools to do it, IMHO.
@@ -708,7 +1314,7 @@
My point, which I may not have made so well, is that the Problem statement/
Proposal explanation ought to spend at least some time on the benefits to
people who aren't using formal static analysis tools. To only talk about proof
-issues leaves a lot of us out.
+issues leaves a lot of us out.
My understanding was that such techniques could be used to make programs that
don't use any tools safe (which Tucker also said in his reply to me). The AI
@@ -717,8 +1323,35 @@
****************************************************************
From: Tucker Taft
-Sent: Friday, October 13, 2017 6:36 AM
+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:
+
+ 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.
+
+[This is version /02 of the AI.]
+
+****************************************************************
+
+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:
+
+ 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):
+
+
+https://docs.google.com/document/d/1pCIzY7ch1Zwa56MUNglzH4M_Ci3L90FvtZh9TBP5
+okg/edit?usp=sharing
-Agreed. The rationale was inadequate.
+P.S. I didn't really read it, but I did verify that the .rtf could be loaded successfully.
***************************************************************
Questions? Ask the ACAA Technical Agent