[m-dev.] Thinking about mode analysis and uniqueness
Ralph Becket
rafe at cs.mu.OZ.AU
Fri Jan 3 11:37:07 AEDT 2003
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
--------------------------------------------------------------------------
More information about the developers
mailing list