[m-dev.] Re: semidet predicate with io__state and state variable syntax bug

[Fergus Henderson]

On 24-Mar-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> state.main(STATE_VARIABLE_IO_0_4, STATE_VARIABLE_IO_5) :-
>         ( % conjunction
>                 (if
>                         ( % conjunction
>                                 V_10 = 1 ,
>                                 V_12 = 2 ,
>                                 V_13 = list.[] ,
>                                 V_11 = list.[V_12 | V_13] ,
>                                 V_7 = list.[V_10 | V_11] ,
>                                 V_8 = STATE_VARIABLE_IO_0_4 ,
>                                 state.semidet_io(V_7, V_8, V_9) ,
>                                 V_9 = STATE_VARIABLE_IO_1_6
>                         )
>                 then
			  ...

Short answer:

This is another issue due to the lack of support for definite aliasing
in the mode checker.  But the severity of the problem could be reduced
a lot if the state variable transformation didn't introduce so many
additional unifications.

Long answer:

During the first pass of mode checking, determinism analysis hasn't
run yet, so we only analyze forward-liveness, not liveness after
backtracking, and this code is fine.
For the unification
                                 V_8 = STATE_VARIABLE_IO_0_4 ,
we ought to be keeping track of the fact that V_8 and STATE_VARIABLE_IO_0_4
are aliased, so that when we get to the call to semidet_io, it will clobber
both V_8 and STATE_VARIABLE_IO_0_4.  But we currently don't support definite
aliasing.  So we allow unifications of this kind, provided that one of
the variables is not (forward-)live, i.e. won't be referenced later on in
the clause.

Then we run determinism analysis and figure out that "semidet_io" is semidet.

Then we run the second pass of mode checking, where we check unique modes.
For an if-then-else, we normally mark any variables which are live
(either forward-live or live on backtracking) as "mostly_unique" rather
than "unique" at the start of the if-then-else.  However, this turned
out to be too strict.  In particular, variables which are not modified
by the condition should be left as "unique", not changed to "mostly_unique".

Unfortunately, because of the lack of support for definite aliasing,
the mode annotations that the first pass of mode checking leaves
do not record any change in the inst of V_8, because V_8 was clobbered
via an alias rather than being clobbered directly.

As a result, the check to see if V_8's inst was modified by the condition
says that it was not, and so the unique mode checking pass thinks that
it is safe to leave V_8 as "unique" rather than "mostly_unique" when
mode-analysing the condition of the if-then-else.

For the particular section of code in the compiler which causes the problem,
the code near the XXX at line 354 of unique_modes.m.

DCG expansion does not introduce the additional variable unifications
that cause the aliases which trigger this problem.

-- 
Fergus Henderson                    |  "I have always known that the pursuit
                                    |  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
--------------------------------------------------------------------------