2019-08-26 08:08 AEST

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000480mercuryBugpublic2019-08-20 10:35
Reporterwangp 
Assigned Tozs 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Product Version 
Target VersionFixed in Version 
Summary0000480: regression in cse_detection.m
DescriptionThe 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.
    
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0001042

zs (developer)

Commit 9fab528bba40d614fb5b715a350330a5f346da9f should fix
most occurrences of this bug.

~0001043

wangp (developer)

Attaching a test case. (I previously posted it to the reviews list but it belongs here.)

~0001044

zs (developer)

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.

~0001045

wangp (developer)

Thanks for the explanation. I think leaving it in the current state is acceptable.
+Notes

-Issue History
Date Modified Username Field Change
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
+Issue History