| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000018 | mercury | Bug | public | 2007-10-12 12:57 | 2007-11-08 16:01 | ||||
| Reporter | maclarty | ||||||||
| Assigned To | juliensf | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | resolved | Resolution | fixed | ||||||
| Product Version | |||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0000018: inconsistent treatment of true goals with no outputs. | ||||||||
| Description | Even 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 Information | Attached 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
juliensf (administrator) 2007-10-18 17:43 |
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. |
|
2007-10-18 18:21 |
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. |
|
juliensf (administrator) 2007-10-19 00:46 |
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. |
|
2007-10-19 09:17 |
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). |
|
juliensf (administrator) 2007-10-19 11:28 |
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.) |
|
juliensf (administrator) 2007-10-19 11:38 |
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. |
|
juliensf (administrator) 2007-11-08 16:01 |
Fixed - see log message for r1.219 of compiler/simplify.m. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2007-10-12 12:57 |
|
New Issue | |
| 2007-10-12 12:57 |
|
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 |
|
Note Added: 0000032 | |
| 2007-10-19 00:46 | juliensf | Note Added: 0000033 | |
| 2007-10-19 09:17 |
|
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 |