[m-dev.] Thinking about mode analysis and uniqueness

[Ralph Becket]

Hi Nancy,

Nancy Mazur, Monday,  6 January 2003:
> 
> Hi Ralph, 
> 
> You might have a look at the reuse branch. 

You're right - I'll look into it.  Does your analysis handle partial
instantiation?  I wasn't (and aren't) interested in that option; also,
I'm primarily interested in working with mode declarations supplied by
the programmer, both of which should make the analysis simpler.

> * Ralph Becket <rafe at cs.mu.OZ.AU> [2003-01-06 04:08]:
> > Inference:
> > 
> > 	(sX, X ~ Y) => sY
> > 	(dX, X ~ Y) => dY
> > 
> > 	(X < Y, sY) => sX
> > 	(dX, X < Y) => dY
> 
> I'm not sure this is correct... 
> 
> Your definition X < Y: 
> || X < Y X is possibly used in the construction bound to Y.  < is a
> ||       partial order.
> 
> So this reflects situations like: Y = f(X, ... ) 
> If so, then the 'deadness' of X doesn't tell anything about the deadness
> of Y... 

The rule (dX, X < Y) => dY says that live values cannot include dead
components.

The rule (dX, X ~ Y) => dY says that we must assume that a possible
alias of a dead variable is also dead (since we may have updated the
value bound to that variable.)

Both of these rules seem reasonable to me.  I agree that I am placing
stronger constraints on bindings than are required by the language
definition, but I would argue that this is a conservative approximation
and is hence safe.

> The other way around; 
> 	X = f(Y,...)
> If X is dead, this indeed implies all the Y's being dead...

I don't agree at all.  X being dead simply means that there can be no
further references to X (and, if X is unique, that we may destructively
update the value bound to X.)  Put another way, X being dead only
affects the top-level functor, not the arguments of that functor.

> but I don't see
> how this rule will ever get applied. Because in most situations, you are
> interested in proving that all the arguments are dead, in order to
> conclude that X is fully dead. And even then, you have to be sure that
> the outermost constructor is not shared. 

My analysis hopefully allows us to detect when a particular cell may be
reused.  I don't see why that requires showing that the arguments to the
functor in question are also dead: if they're boxed then overwriting the
parent functor cell can do no harm; if they're not boxed then there
shouldn't be any references to those addresses.

> I don't know if I'm making myself clear here, but the thing is, I don't
> understand the point of this rule ;-)

I don't think I understand your point.  Can you give me an example where
you think my analysis gets it wrong?

> > 
> > I will use the notation Precondition | Goal | Postcondition
> > or just Goal | Postcondition where Precondition is not of interest
> > or just Precondition | Goal where Postcondition is not of interest.
> > 
> > We treat goals as operators on states of variables and write P(S) to
> > denote the state resulting from successfully executing P starting in
> > state S.
> > 
> > The Postcondition lists those properties that are explicitly affected
> > by successfully executing the goal.  All others that do not follow are
> > unaffected (so we don't have to write endless frame axioms.)
> > 
> > Aliasing, X = Y
> > 
> > 	lX, fX, lY, bY  |  X = Y  |  bX, X ~ Y
> > 
> > Test for equality, X = Y
> > 
> > 	lX, bX, lY, bY  |  X = Y  |
> > 
> > Construction, X = f(Y, ...)
> > 
> > 	lX, fX, lY, bY, ...  |  X = f(Y, ...)  |  bX, Y < X
> > 
> > Deconstruction, X = f(Y, ...)
> > 
> > 	lX, bX, lY, fY, ...  |  X = f(Y, ...)  |  bY, Y < X, ...
> > 
> > 	We may also have postcondition uY for some uY depending upon the
> > 	inst of X at this point.
> 
> I don't know how finegrained you are planning to go (and I'm not sure
> anymore what the goal of this mode-analysis was in the first place),

The point is to identify safe cells for reuse in the context of nested
unique values.

> but 
> uY will only be the case if X is fully unique.

No, I can have a uniquely referenced value f(Y, Z) which has the unique
reference for Y and a shared reference for Z.

> Are you planning to make
> a difference between uX, and the uniqueness of the outermost functor of
> X? 

Yes, uniqueness only refers to the top-level functor of a variable in
this analysis.  Thanks for pointing out an omission in my description!

> Anyway, I have the feeling that you really ought to check the
> reuse-branch I've been working on. If the only difference is the degree
> of detail of the analysis, then it's not difficult to modify the level
> op detail by simplifying the domains we use. 

Given that I've been thinking about this far less than you have, I'd be
surprised if that wasn't the case!

> I wonder how the precision of the overall process will be. I have a
> strong feeling that everything will be shared at some point. 

Why?  I've tried to come up with reasonably precise definitions of when
a variable is the unique reference to a particular functor and when that
variable dies (and hence whether or not that functor's cell may be
safely overwritten.)

I can't see how the analysis would go wrong; tomorrow morning I'll try
going through some examples and see what happens.  I'll post the
results.

> > Disjunction, (P ; Q), starting with state S
> > 
> > 	If PrecondP | P then S must entail PrecondP.
> > 	If PrecondQ | Q then S must entail PrecondQ.
> > 	If X is a nonlocal and P | bX then we must also have Q | bX
> > 	and vice versa.
> > 	For any nonlocals X and Y we must have
> > 		if P | dX    then (P ; Q) | dX    (and similarly for Q),
> 
> I disagree. It's not because P leaves a variable dead, that the whole
> disjunction makes it dead. What if Q contains some non-deterministic
> call depending on X. In that case, even if X is not used 'after' (P; Q),
> it is unsafe to call it dead, as it still may be used upon backtracking. 

You've caught me out - I haven't addressed mostly deadness and so forth.
The analysis presented here is an approximation to the real thing, which
I haven't fully worked out; I'm hoping the audience will allow me a
little leeway for now while the basic idea is discussed.  However, I
will say that since unique values can't be passed out of
non-deterministic contexts, it's not obvious to me that there's a
problem.

> > 		if P | sX    then (P ; Q) | sX    (and similarly for Q),
> > 		if P | X < Y then (P ; Q) | s < Y (and similarly for Q),
> > 		if P | X ~ Y then (P ; Q) | s ~ Y (and similarly for Q).
> 
> Hmmm. What if P | sX and Q | X < Y ? What is the result? 
> (P ; Q) | sX sY  ? How does the information get lost here? 

Yes.  The analysis isn't 100% accurate, but I don't think that's an
issue.  I think this analysis will work for 90+% of the key cases and is
simple enough to be efficiently implementable.

> I think you should be more specific on how the 'least upper bound' of
> the different elements in your domain is... because it is the least
> upper bound that you are computing here... 

I'm sorry - it may be because I've had a couple of beers, but I'm not
clear what you mean here!  Can you rephrase the suggestion?

> > Negation, not P
> > 
> > 	Handled as ( if P then false else true ).
> > 
> > Conditional goals, ( if P then Q else R ), starting with state S
> > 
> > 	If X is a nonlocal then we may not have P | bX.
> > 
> > 	Otherwise handled as (P, Q ; R).
> > 
> > Initial state
> > 
> > 	The initial properties of each argument variable are taken from
> > 	the argument mode (with initally free variables also being
> > 	unique) and local variables are initially free and unique.
> > 
> > Variable Death
> > 
> > 	If at any point we have uX and for all Y s.t. X ~ Y we have that
> > 	Y does not appear anywhere in the subsequent computation, then
> > 	we infer that X is dead, hence dX.
> 
> "anywhere in the subsequent computation" may be a bit harder then you
> think if you want to take non-deterministic procedure calls into
> account... 

But I don't, really.  I'm pretty much only concerned with explicitly
declared unique values, which rules out non-deterministic contexts.

> > Reuse criterion
> > 
> > 	A variable X's cell may be destructively updated (reused) if we
> > 	have (uX, dX).
> > 
> > I'll hold off posting thoughts on efficient implementation until I see
> > what holes people can find in the above.
> 
> I'll repeat myself ;-) But this analysis is the goal of the liveness
> analysis we're doing in the context of CTGC. The precision of this
> analysis is finer-grained then what you specify here. 

How much more complex is your analysis?
How much more effective is it?

I really don't want to reinvent the wheel, but I was under the
impression that your analysis was far more general and costly than what
I have in mind.

> So, my questions would be: 
> - what is the exact purpose of all these inferences? 

To provide "cheap" local analysis for nested unique values in order to
support destructive update thereof.  I'm primarily interested in cases
where the uniqueness of the headvars is known.

> - can't the liveness information we collect be simply used for your
>   purposes? Or is the analysis too complex/time consuming? 

For the first part, I'll have to go look at your code.
For the second part, I don't know - how costly is your analysis?

> The thing is, that the analysis we've implemented infers for each
> variable that is ever deconstructed whether it becomes dead or not. If
> it's not dead, the analysis will still say to what it is aliased. And if
> the aliases die, then at some point the whole structure may die. 

Agreed.  I belive I cover this case.

> Other, a finer grained question... 
> I guess you don't need a fixpoint computation, because every argument
> of a procedure call that is bound is automatically set to shared? 

Yes, I'm not particularly interested in inter-procedural inference.

> For the moment I have no further remarks... but I think we should talk
> ;-) Or else one of us will do some work in double here... 

Definitely!  I should go and re-read your papers.  Or have you a
disseration I could look at?

The plus-side of my analysis is that it should be relatively cheap
(there's an equivalence class and a partial order involved, but I reckon
the average equivalence class will have but two or three members and the
average depth of any tree in the partial order will similarly be two or
three.)

Cheers,

- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------