CVS difference for ai12s/ai12-0240-1.txt

--- ai12s/ai12-0240-1.txt	2018/01/25 07:14:55	1.6
+++ ai12s/ai12-0240-1.txt	2018/03/30 07:55:08	1.7
@@ -1566,4 +1566,77 @@
 currently defined) cannot be an aspect: it has different values for the
 partial and full views.
 
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, March 24, 2018  9:31 AM
+
+I updated a bit this presentation on safe pointers (AI-0240). It could still
+use more pictures, etc., but it might be useful for those still struggling to
+understand this proposal.
+
+https://docs.google.com/presentation/d/1NdZl-Pee6ZyniVtAoqx6i8Fv0KD6nrqLixqX3LXzvkA/edit
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, March 27, 2018  11:48 AM
+
+Randy and I were discussing how to handle cursors, if the rest of the container
+data structure were implemented using these Ownership pointers.  We began to
+discuss some sort of "secondary" pointers or "unchecked" references, but I just
+realized that good old 'Unchecked_Access provides exactly what we need.  The
+pointer inside a cursor would not have Ownership True, would be of a general
+access type, and would be initialized by using 'Unchecked_Access.
+Unchecked_Access already seems to have exactly the right semantics for such 
+pointers, namely it is up to the programmer to worry about dangling references.  
+
+So I don't see any need to add any special notion of "Unchecked_References" to
+AI12-0240.  So long as Unchecked_Access works, I don't think we need a new
+feature to handle the "cursor problem."
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, March 27, 2018  5:37 PM
+
+I don't think this works. Recall (for the rest of you, this was from our
+private discussion) that the primary concern is being able to statically claim
+that a dereference is not a global object because it is "owned" by an object
+that is explicitly passed as a parameter. This is necessary so that the Global
+reference can statically be "null" (or some other very restricted setting) 
+rather than having to be "all" -- "all" necessarily prevents most parallelism
+when checking for safety.
+
+Note that we have to be able to dereference the unchecked reference, as it is 
+not legal to convert the unchecked reference back to the owned pointer (that
+would be a conversion into a pool-specific type, which is generally not
+allowed).
+
+For the owned pointers themselves, there is a fairly simple reachability rule
+which provides the needed safety. The same rule can be used for the unchecked
+pointers used in cursors, so long as the compiler can know that the unchecked
+pointers cannot contain anything other than an owned pointer.
+
+However, proving that the unchecked pointers cannot contain anything other
+than an owned pointer requires analysis of all of the code that could possibly
+create such a pointer. One can probably prove it in very limited circumstances
+(such as when declared in a body), but the possibility of child units having
+visibility into a private part means that separate compilation makes such a
+proof unlikely unless we were to require analysis beyond what is usually
+expected of Ada compilers.
+
+As such, it seems necessary to declare that the type is an unchecked reference
+of an owned pointer, so that we can apply the rules for owned pointers without
+having to engage in complex proofs (perhaps OK for SPARK, not OK for Ada).
+Once that's done, we might as well make that a pool-specific type in order to
+be telling the truth about the capabilities of the type. (Personally, I'd
+rather that all of these things are unchecked references by default, and that
+the owned pointers are marked on the component or object declaration, as that
+would require the least "noise" in the code -- there are only a few owned
+pointer components in a typical program. Unmarked objects and components are
+either "observers" if they have a short lifetime and "unchecked" if they have
+a long lifetime. I don't see the value of having separate types. But that can
+be discussed later.)
+
 ***************************************************************