2024-12-15 06:29 AEDT

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000018mercuryBugpublic2007-11-08 16:01
Reportermaclarty 
Assigned Tojuliensf 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
Product Version 
Target VersionFixed in Version 
Summary0000018: inconsistent treatment of true goals with no outputs.
DescriptionEven with the --fully-strict option, mmc will optimise away a goal like the following:

    promise_pure(
        impure set_m(I) % m is a mutable.
    ).

However it will not optimise away the following goal under --fully-strict:

    p("hello")

where

p(I) :-
    trace [io(!IO)] (
        io.write(I, !IO)
    ).

(even with --no-inlining)

Either the semantics of --fully-strict needs to be further refined, or the compiler needs to behave the same in both of these cases.
Additional InformationAttached is an example.

With mmc fs --fully-strict the call to p gets optimised away.
With mmc fs --fully-strict --no-inling it doesn't.
TagsNo tags attached.
Attached Files
  • ? file icon fs.m (452 bytes) 2007-10-12 12:57

-Relationships
+Relationships

-Notes

~0000031

juliensf (administrator)

Ian, what exactly are you talking about? The example you attached
doesn't seem to match the description you posted.

Note that just because the compiler can replace goals, doesn't
necessarily mean it will. Also, in order to be able to safely be
able to replace a goal the compiler must be able to prove that it
the goal terminates and does not throw an exception.

If you run your example with --fully-strict --no-inlining and with --enable-termination --analyse-exceptions
you will get the same result as the case with inlining enabled.
(If you look in compiler/goal_form.m you will notice that in the absence
of those two analyses the compiler cannot infer termination/non-exception
throwing across procedure boundaries.)

In any case, the real problem is that the following purity promise is
a lie:

    promise_pure (
        impure set_m(I)
    )

An additional complication in this case, is that trace goals have a
particular semantics w.r.t goal replacement, i.e. they are never replaced
but calls to procedures containing them may be.

~0000032

maclarty (developer)

I think you misunderstood what I was saying.

The documentation currently says that with --fully-strict, the compiler is *not* allowed to replace (semi)pure det goals with no outputs, however the compiler replaces the following with 'true' when the --fully-strict option is given.

    promise_pure (
        impure set_m(I)
    )

The attached example illustrates this (don't you get the output 0 2 when you compile fs.m with --fully-strict?).

Yes, I know the promise_pure is a lie, and I'm not actually using this in any real code. It was just something I came across and I didn't expect this behaviour based on what the reference manual says.

~0000033

juliensf (administrator)

The documentation and the implementation seem to differ on what should be
happening with --fully-strict / --no-fully-strict.

(1) The comments (and code) in compiler/simplify.m mean suggest that if --fully-strict
is enabled then det goals with no outputs should not be replaced by true, and
goals that always fail should not be replaced by false.

(2) The documentation gives a different impression: rather than preventing the compiler
from replacing such goals, --fully-strict and --no-fully-strict just alter the requirements
under which the replacement can occur.

For --no-fully-strict the compiler can replace any semi(pure) det goal with no outputs,
regardless of whether it terminates or throws an exception. (And similarly for the always
fails case.)

For --fully-strict it can only perform that replacement if it can prove that the goal does
terminate and does not throw an exception.

The help message for --no-fully-strict says:

"Allow mmc to optimize away infinite loops or calls to error/1"

That suggest to me that --fully-strict is still allowed to optimise away the goals if
doing so won't change the termination or exception throwing properties of the
program, i.e. doing so won't turn a non-terminating program into a terminating one.
(The reference manual says something.)

It doesn't appear that this is what the compiler does though. There is a bug somewhere here,
I'm just not sure what it is. We should decide what --fully-strict/--no-fully-strict actually
mean before trying to work that out though.

~0000034

maclarty (developer)

Perhaps we should make the semantics of --no-fully-strict simply:
Allow the compiler to improve completeness by replacing infinite loops or calls to error with 'true' or 'false'.

And then change simplify.m so that it doesn't use the --fully-strict option to decide if it can replace terminating (semi)pure det goals with no outputs with 'true' (similarly for failing goals).

The last change I made to the docs tried to get the docs more in line with what the compiler actually does. But I now think we should be fixing the compiler to get it in line with the original docs. The original docs don't say anything about terminating (semi)pure goals that produce no outputs, so simply.m shouldn't be checking the --fully-strict options to decide if it can optimise these away or not (they don't affect completeness anyway).

~0000036

juliensf (administrator)

Actually, looking at it with fresh eyes, the code in simplify.m does the
correct thing, i.e. behaviour (2) in my last note, either --no-fully-strict
is set or the goal must terminate and not throw an exception. (I mistook
the disjunctions for conjunctions last night.)

~0000037

juliensf (administrator)

Incidentally, this means that the warning message at compiler/simplify.m:653
is incorrect because compiling with --fully-strict is not sufficient
to disable the optimisation.

~0000047

juliensf (administrator)

Fixed - see log message for r1.219 of compiler/simplify.m.
+Notes

-Issue History
Date Modified Username Field Change
2007-10-12 12:57 maclarty New Issue
2007-10-12 12:57 maclarty File Added: fs.m
2007-10-18 17:43 juliensf Note Added: 0000031
2007-10-18 17:43 juliensf Status new => acknowledged
2007-10-18 17:46 juliensf Status acknowledged => feedback
2007-10-18 18:21 maclarty Note Added: 0000032
2007-10-19 00:46 juliensf Note Added: 0000033
2007-10-19 09:17 maclarty Note Added: 0000034
2007-10-19 11:28 juliensf Note Added: 0000036
2007-10-19 11:38 juliensf Note Added: 0000037
2007-11-08 16:01 juliensf Status feedback => resolved
2007-11-08 16:01 juliensf Resolution open => fixed
2007-11-08 16:01 juliensf Assigned To => juliensf
2007-11-08 16:01 juliensf Note Added: 0000047
+Issue History