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

[Ralph Becket]

Fergus Henderson, Friday,  3 January 2003:
> 
> These are properties not just of a variable, but rather of a variable
> and a program point.  A variable may be live at one point in the
> computation and dead at a later point, or free at one point and bound
> at a later point, etc.

Yes - I'm afraid I've been fighting a head-cold for over a week and am
not being as precise as I should.

> I presume these are all definite properties (i.e. X ~ Y means that X
> definitely aliases Y, and X < Y means that Y definitely contains X)?

They may be conservative approximations.  For instance, in a disjunction
we may have X ~ Y from one arm but not from the other.  Conservatively
we take X ~ Y as a result of the disjunction as a whole.

> > 	shared(X)	<=>	some [Y, Z] (X < Y, X < Z, Y \= Z)
> 
> Hmm.  For the purposes of the mode system (e.g. destructive updated),
> uniqueness has to mean definite uniqueness.  It's not safe to
> destructively update something unless there are definitely no other
> references to it.  As a result, shared(X), the negation of unique(X),
> needs to mean *possible* sharing.  But here you define it in terms
> of "<" which apparently means definite containment.

Yes, that should be a rule rather than a definition.  Also, following a
suggestion of Peter Moulder's to make ~ reflexive:

	some [Y, Z] (X < Y, X < Z, not Y ~ Z)  =>  should(X)

> Also, consider this example:
> 
> 	:- mode p(in, in).
> 	p(A,B) :- ...
> 
> At the entry point to p/2, how do you represent the fact that A and B
> might share?  If "<" means definite containment, then neither A < B
> nor B < A hold.  You need some way to represent situations like this.

Agreed.  The solution is to make shared/1 independently assertable and
not contingent on a definition.

> > The task of termination analysis for simple conjunctions is ...
> 
> Did you mean to say "The task of _mode_ analysis ..."?

I need more paracetamol.

> Hmm.  This rule sounds like ~ means possible aliasing, not definite
> aliasing.

Yes.

> > 	If P makes any non-local X shared then X is shared as a
> > 	postcondition of (P ; Q) and similarly for Q.
> 
> You defined sharing not as a base property, but in terms of "<".
> So the rule for disjunction should say how the "<" properties are updated
> (and does not need to explicitly define how the sharing properties are
> updated).
> 
> I suggest that you edit your original post to clarify which properties are
> definite and which are possible (e.g. whether ~ means definite aliasing
> or possible aliasing), and to show how `p(in, in)' is represented.

Will do.  The feedback is much appreciated.

- 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
--------------------------------------------------------------------------