[m-rev.] Bugfix: solver type scheduling

[Ralph Becket]

I haven't included the diff because, apart from four characters, it is
identical to the last one.  This change bootchecks and passes all the
tests that we are currently passing (i.e. all but three or four, mainly
caused by out-of-date .exp files).

Estimated hours taken: 80
Branches: main

[This is a fix to a recently backed-out change which caused a problem
when building library/bitmap.m; this change bootchecks successfully.
The hard-to-find problem with the original change turned out to be
mode_info_add_goals_live_vars(Goals1, !ModeInfo),
which should have been
mode_info_add_goals_live_vars(InitGoals, !ModeInfo),
in modes.modecheck_conj_list_3.]

This change allows the compiler to identify a minimal set of solver type
variables for which it needs to insert initialisation calls in order to
achieve a deterministic schedule if one exists.

The problem before was that given

	:- func f(t)        = t.
	:- mode f(in(any))  = out(any) is det.
	:- mode f(out(any)) = in(any)  is semidet.

and the goal

	X = f(Tmp),
	Tmp = f(Y)

in a situation where X, Tmp and Y are free, the compiler did not
know which variable(s) to initialise, so it simply initialised variables
optimistically.  This led to the following (inefficient) semidet
schedule where an (efficient) det schedule would be expected:

	init(Tmp),
	X = f(Tmp),	% using f(in(any)) = out(any) is det.
	Tmp = f(Y),	% using f(out(any)) = in(any) is semidet.

The new analysis kicks in when ordinary scheduling fails to schedule all
the goals in a conjunction.  It identifies the right variable(s) to
initialise by exploiting the following observations:
- a det var/var unification must be an assignment;
- a det var/functor unification must be a construction;
- a det call must be to a det proc and use no implied modes.
(A conservative approach is taken to handling if-then-else goals,
negations, disjunctions and so forth.) The analysis therefore does not
need to know what order the goals will be scheduled in, just whether or
not a deterministic schedule should exist.

Using this analysis the compiler works out that Y is the right variable
to initialise, giving

	init(Y),
	Tmp = f(Y),	% using f(in(any)) = out(any) is det.
	X = f(Tmp)	% using f(in(any)) = out(any) is det.

which is deterministic, as one would expect.

There is one problem concerning impure goals.  Say we have

	X = f(Tmp),
	Tmp = f(Y),
	impure p(...)

Mode analysis will delay the first two unifications, then attempt to
schedule the impure goal, and consequently flag an impurity error since
p(...) cannot be reordered with respect to the other goals (why? p(...)
may be a solver "ask" goal and f/1 may be a solver "tell" goal.)

One workaround is to use the following idiom:

	some [_DummyVariable] (
		X = f(Tmp),
		Tmp = f(Y)
	),
	impure p(...)

which causes the conjunction inside the quantifier to be scheduled
properly.  (We would not want to wrap each subgoal in a `some [_] (...)'
wrapper because that may remove useful reordering opportunities.)

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------