0000480: regression in cse_detection.m

Mercury Bugs - mercury
View Issue Details

ID	Project	Category	View Status	Date Submitted	Last Update
0000480	mercury	Bug	public	2019-08-05 17:09	2020-04-15 12:58

Reporter	wangp
Assigned To	zs
Priority	normal	Severity	minor	Reproducibility	always
Status	resolved	Resolution	fixed
Platform		OS		OS Version
Product Version
Target Version		Fixed in Version

Summary	0000480: regression in cse_detection.m
Description	The attached test case fails to compile. % mmc -C cse_detection_regression.m cse_detection_regression.m:013: Error: invalid determinism for `to_bool'(in) = cse_detection_regression.m:013: out: cse_detection_regression.m:013: the primary mode of a function cannot be cse_detection_regression.m:013: `nondet'. cse_detection_regression.m:013: In `to_bool'(in) = out: cse_detection_regression.m:013: error: implicit determinism declaration not cse_detection_regression.m:013: satisfied. cse_detection_regression.m:013: Declared `det', inferred `nondet'. cse_detection_regression.m:022: Unification with `maybe.yes(V_8)' can fail. cse_detection_regression.m:024: Disjunction has multiple clauses with cse_detection_regression.m:024: solutions. cse_detection_regression.m:025: Unification with `maybe.no' can fail. For more information, recompile with `-E'. I bisected the problem to this change: commit 2466524308930c380483a90c7d767a74e7c8507b Author: Zoltan Somogyi <zoltan.somogyi@runbox.com> Date: Sun Jun 30 20:16:07 2019 +0200 Fix cse_detection.m's interaction with uniqueness. This fixes github issue 0000064. compiler/cse_detection.m: When pulling a unification X = f(Y1, ..., Yn) out of an arm of a disjunction, switch or if-then-else, require the instantiation state of X to be free of unique or mostly_unique components. Put the requirements on X's inst into a single predicate. Add a mechanism to make debugging similar issues easier.
Tags	No tags attached.
Relationships
Attached Files	cse_detection_regression.m (503) 2019-08-05 17:09 https://bugs.mercurylang.org/file_download.php?file_id=288&type=bug bug480b.m (470) 2019-08-19 13:48 https://bugs.mercurylang.org/file_download.php?file_id=290&type=bug

Notes

It seems that with the current mode analysis system, there can't
really be a simple satisfactory fix for the root cause of this problem.
This is due to the fact that replacing "X = f(Y1, Y2)" with
"X = f(A1, A2), A1 = Y1, A2 = Y2", which is the basic transformation
on which cse is built, makes it lose track of any uniqueness in
X's arguments.

The original change to cse in June to fix github issue 64 was
too conservative in that it avoided making that transformation
not just when it would screw up uniqueness, but in other cases
as well. The original and updated fixes to Mantis bug 480 made
cse less conservative but still conservative enough. However,
Peter's latest test case shows that the current approach will
never be able to draw the line correctly between too conservative
and not conservative enough. This is because it involves uniqueness
in arguments that (a) the cse transformation would screw up, but
(b) the program does not *care* if this uniqueness is screwed up,
because it is only an accidental byproduct of that argument being
a newly constructed term, and the uniqueness of this argument
(the visited field in bug480b.m) is never required by any of its
consumers. Part b is not a local property; it involves at least
all of the rest of the procedure, and in the presence of mode inference,
it may involve the code of the rest of the module as well.

A way to solve this problem would be to downgrade unique insts
to ground insts in situations that do not care about uniqueness.
However, actually doing this would be hard, because it would require
circular interaction between compiler phases. We do cse in stage 45,
determinism analysis in stage 50, and unique mode checking in stage 55.
Each phase depends on the results of the previous phase. We don't *know*
which unique insts are required and which are not, until the end of
stage 55, yet cse would need this info in stage 45.

We *could* get cse to pull unifications out of disjunctions even if
it would screw up uniqueness, but handle github issue 64 by recording
this fact in the proc_info, and then redoing everything from cse onward
if we get any error during unique mode analysis for any procedure
that has been so marked. However, I would not call such a solution "simple",
not least because a procedure may have done N such pulls involving unique args,
and we don't know *which subset* of those N pulls we have to undo (to preserve
uniqueness-correctness), which subset we *must not* undo (to preserve the
expected determinism), and which subset would be fine either way.

I would prefer to leave this issue in its current state with only one change:
a note in NEWS mentioning that due to a bug fix, switches on variables' fields
(as opposed to switches on variables themselves) may not be recognized as such,
and telling people to replace such code with a switch on a variable. This would
get users to do manually what cse used to do before the github 64 fix, the
difference being that they should (would?) not be surprised by any errors
involving uniqueness arising out of such a change.

Since determinism analysis is inherently undecidable, such changes in heuristics
are easily defensible.

We could revisit this decision if/when a constraint based mode analysis
is able to track uniqueness through the extra unifications added by cse.

Date Modified	Username	Field	Change
Issue History

2019-08-05 17:09	wangp	New Issue
2019-08-05 17:09	wangp	File Added: cse_detection_regression.m
2019-08-05 18:29	zs	Assigned To	=> zs
2019-08-05 18:29	zs	Status	new => assigned
2019-08-05 21:11	zs	Note Added: 0001042
2019-08-19 13:48	wangp	File Added: bug480b.m
2019-08-19 13:48	wangp	Note Added: 0001043
2019-08-19 19:07	zs	Note Added: 0001044
2019-08-20 10:35	wangp	Note Added: 0001045
2020-04-15 12:58	zs	Status	assigned => resolved
2020-04-15 12:58	zs	Resolution	open => fixed
2020-04-15 12:58	zs	Note Added: 0001080