OK. I'm beginning to think that I've been asking the wrong question all
along. I have been asking: "is this field immutable". What I should have
been asking is "is this field/whatever immutable *enough*."
Let's see if I can manage to capture the brain-fart of the moment, and then
I think I need to go read some literature.
Region analysis provides a conservative analysis of the lifetime of a value.
In the context of BitC, it is conservative in (at least) two cases:
1. The value escapes beyond the context we wish to analyze
2. Two values flow (through assignment) to the same location,
with the result that it becomes impossible to distinguish their
regions.
The second case is exactly the case that is vexing us in the context of
immutability. Analyzing lifetimes in the presence of this case is a form of
path-sensitive value flow analysis, which is an approach I had not
considered.
We are not concerned here with the flow of the value *per se*. What we are
concerned with is the flow of the *lifetime* of the value.
In particular, consider a procedure with signature: void f(rFoo: deeply
immutable foo)
We have been taking this to mean that /rFoo/ must point to something that
will never change.
But if we assume (for a moment) that /rFoo/ does not escape the call to f(),
then there is another way to look at the contract being expressed here: f()
requires that the value graph targeted by /rFoo/ must be deeply immutable **for
the value lifetime of the binding formed at the call to rFoo**. If the value
of /rFoo/ is not captured, then there is no reason why f() should retain any
say in the mutability of /rFoo/ after f() returns.
This means that if rFoo involves a graph that is threaded through an inner
reference or an on-stack reference somewhere, it isn't really our job to
determine that the entire deep structure is fixed in cement. It is only our
job to ensure that it is fixed in cement for the duration of the call to
/rFoo/.
If /rFoo/ is captured, then we can view this as extending the value lifetime
of the value bound at the call, but the nature of the required determination
remains unchanged - the graph named by the present value of /rFoo/ must
remain unchanged until the last reference to it is lifted.
If we look at matters this way, then we need a kind of analysis that is
qualitatively similar to value flow.
My previous description of the behavior of "pure" seems to remain
consistent: when the rule is "[shallow] pure expands to the box boundary",
all seems to be well. What this means, in effect, is that a pure unboxed
field can only exist within a pure structure, and that a value of pure
aggregate type may not be stored in an impure location.
This also leaves us with "init-only" as a sensible thing to say about a
field.
I wonder if it isn't time to settle for "pure" and "init-only" (and possibly
"deep pure") for the current version of the language, and deal with more
complex cases later as justification emerges. This will tend to push a few
cases in the direction of references, but perhaps not enough that we should
care.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
