On 07/06/2011 7:52 AM, Marijn Haverbeke wrote:
Sure. But how many of them are potentially *interfering* with other aliases
in the same scope (under type-based and conservative root-based analysis)?
A lot. As I explained in my first email to this thread, type-based
alias analysis is just not very helpful in our current type system.
Sure. You explained this on friday, and we spent friday working out
details of how to manage the corner cases.
There are two separate induction hypotheses to maintain:
- Every alias is outlived by its referent.
- An aliased memory cell can't be written-to by any other path
visible from the current scope.
These two relate. That is, the referent-outlives-alias rule is only
possible to prove insofar as you can prove the no-alias-interference
rule (because, as you observed, someone could mutate the referent
through some other path).
You thought you had proved the first in isolation with your patch
yesterday, for the most part. What patrick and I were discussing on
friday was how to prove the second, which we though to be a presequisite
for the first holding together. So when you told me yesterday that you
could get away with just proving the first in isolation, this is why I
was skeptical. We were quite aware of the "variant changes underfoot"
problem, and wanted to prohibit it (I think I stated it in my first
email to this thread). I still think we have to prove the second in
order to support the first.
To enforce the second, we believe it suffices to show any of the following:
- Non-type-overlap between referent and any other alias in
scope at present.
- Non-pointer-equivalence between referent address and any other
alias in scope at present.
- Sub-cases:
- Referent is uniquely owned (local, interior-of-local, or
unique-pointer-from-local, ad infinitum) and other referent
is either in-a-shared-box or uniquely-owned from a different
path.
- Special cases patrick suggested: referent is the contents of
a *single level* of "immutable box held by a uniquely-owned
path", and we prove disjointness of that box address from all
other visible aliases either by static disjointness (as in
cases above) or, in the limit, by a shallow runtime test
against any ambiguous aliases currently in scope. This is
strictly to permit writing functions that by & so that they
can work on boxed or unboxed varieties of the same type.
This also requires us to consider the LHS of an assignment to an upvar,
and the LHS of any assignment to a variable outside the scope of an alt,
as a short-lived alias. It might well be wise, for conservativeness
sake, to generalize this to all LHS-of-assignment. IOW consider each
assignment operator as a "call" to a function copy[T](&mutable T, &T)
and ensure that the 2 aliases formed by that rule aren't breaking any of
the rules above.
(The receive operator |> probably goes in the same camp, and all the op=
operators, possibly a few more..)
-Graydon
_______________________________________________
Rust-dev mailing list
[email protected]
https://mail.mozilla.org/listinfo/rust-dev
