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

[Fergus Henderson]

On 02-Jan-2003, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Each variable in the goal may have one or more of the following
> properties:
>
> 	bound(X)	X is bound to some term.
> 
> 	X < Y		X was used in the construction of the term to
> 			which Y is bound; < is areflexive, asymmetric
> 			and transitive.
> 
> 	X ~ Y		X is an alias of Y; ~ is symmetric and
> 			transitive.
> 
> 	dead(X)		X may not be referred to in any subsequent
> 			computation.

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.

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

> We use the following definitions and rules:
> 
> 	free(X)		<=>	not bound(X)
> 
> 	shared(X)	<=>	some [Y, Z] (X < Y, X < Z, Y \= Z)
> 
> 	unique(X)	<=>	not shared(X)

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.

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.


> The task of termination analysis for simple conjunctions is ...

Did you mean to say "The task of _mode_ analysis ..."?

> We extend the analysis to cover disjunction and conditional goals (and
> hence negation) thus:
> 
> Disjunction
> (P ; Q)
> 	If P binds any non-local X then Q must bind X also and vice
> 	versa.
> 	If P makes any non-locals X and Y aliases X ~ Y then X ~ Y is a
> 	postcondition of (P ; Q) and similarly for Q.

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

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

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------