diff: detect floundering in solutions/2 etc.
Fergus Henderson
fjh at cs.mu.oz.au
Sun Oct 12 23:29:56 AEST 1997
Dectect floundering in solutions/2 and nondet if-then-else.
library/std_util.m:
Change the code for builtin_aggregate to (a) check for
floundering and (b) reset the trail properly.
compiler/code_gen.m:
Change the code for if-then-elses with nondet conditions
so that it checks for floundering.
runtime/mercury_trail.h:
compiler/llds.m:
compiler/llds_out.m:
Add new alternative `MR_solve' to MR_untrail_reason.
This is used to for checking for floundering in the
above-mentioned two cases.
extras/clpr/cfloat.m:
extras/trailed_update/var.m:
Handle the MR_solve case.
doc/reference_manual.texi:
Document MR_solve.
NEWS:
Delete the mention of the limitation that we didn't
dectect floundering in solutions/2 and nondet if-then-else.
cvs diff NEWS compiler/code_gen.m compiler/llds.m compiler/llds_out.m doc/reference_manual.texi extras/clpr/cfloat.m extras/trailed_update/var.m library/std_util.m runtime/mercury_trail.h
Index: NEWS
===================================================================
RCS file: /home/staff/zs/imp/mercury/NEWS,v
retrieving revision 1.81
diff -u -r1.81 NEWS
--- NEWS 1997/10/11 15:31:04 1.81
+++ NEWS 1997/10/12 12:56:09
@@ -14,24 +14,20 @@
more flexible. There is a new inst `any' for variables whose value
is unknown but which may have constraints on them.
- The support for `any' insts is not quite complete; in particular, we
+ The support for `any' insts is not 100% complete; in particular, we
do not support passing values of inst `free' where values of inst
`any' are expected, so sometimes you have to explicitly call a predicate
to initialize a free variable to inst `any'. Also the Mercury language
reference manual does not yet contain any documentation on `any' insts.
- Another limitation is that we don't yet do a perfect job of floundering
- detection; floundering in solutions/2 or in if-then-elses with nondet
- conditions may go undetected.
-
The `extras' distribution includes packages for doing constraint
solving on (a) floating point numbers and (b) terms containing
Prolog-style variables. See below.
* The C interface now includes generalized trailing support.
- There is a new set of grades `*.tr' (e.g. `asm_fast.gc.tr') which
- provide support for trailing. This could be used by predicates or
+ The compiler has a new set of grades `*.tr' (e.g. `asm_fast.gc.tr')
+ which provide support for trailing. They could be used by predicates or
functions defined using the C interface to perform such things as
constraint solving, backtrackable destructive update, or even automatic
unwinding of database transactions on backtracking. See the
@@ -135,7 +131,7 @@
Changes to the Mercury compiler:
********************************
-* We've added termination analysis to the compiler.
+* We've added support for termination analysis.
For details, see the "Termination analysis" subsection of the
"Implementation-dependent pragmas" section of the "Pragmas" chapter
Index: compiler/llds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/llds.m,v
retrieving revision 1.210
diff -u -r1.210 llds.m
--- llds.m 1997/08/25 17:48:21 1.210
+++ llds.m 1997/10/12 07:53:10
@@ -185,11 +185,13 @@
% any mutable global state to the state it was in when
% the ticket was obtained with store_ticket();
% invalidates any tickets allocated after this one.
- % If undo_reason is `commit', leave the state
- % unchanged, just discard the trail entries and
- % any associated baggage; invalidates this
- % ticket as well as any tickets allocated after this
- % one.
+ % If undo_reason is `commit' or `solve', leave the state
+ % unchanged, just check that it is safe to commit
+ % to this solution (i.e. that there are no outstanding
+ % delayed goals -- this is the "floundering" check).
+ % Note that we do not discard trail entries after
+ % commits, because that would in general be unsafe.
+ %
% Any invalidated ticket is useless and should
% be deallocated with either `discard_ticket'
% or `discard_tickets_to'.
@@ -256,6 +258,7 @@
:- type reset_trail_reason
---> undo
; commit
+ ; solve
; exception
; gc
.
Index: compiler/llds_out.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/llds_out.m,v
retrieving revision 1.58
diff -u -r1.58 llds_out.m
--- llds_out.m 1997/10/02 00:11:19 1.58
+++ llds_out.m 1997/10/12 07:54:31
@@ -1205,6 +1205,8 @@
io__write_string("MR_undo").
output_reset_trail_reason(commit) -->
io__write_string("MR_commit").
+output_reset_trail_reason(solve) -->
+ io__write_string("MR_solve").
output_reset_trail_reason(exception) -->
io__write_string("MR_exception").
output_reset_trail_reason(gc) -->
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.77
diff -u -r1.77 reference_manual.texi
--- reference_manual.texi 1997/10/10 08:06:11 1.77
+++ reference_manual.texi 1997/10/12 12:44:45
@@ -3191,6 +3191,7 @@
MR_undo,
MR_exception,
MR_commit,
+ MR_solve,
MR_gc
@} MR_untrail_reason;
@@ -3201,12 +3202,20 @@
@end example
@noindent
A call to @samp{MR_trail_function(@var{untrail_func}, @var{value})}
-ensures that
+adds an entry to the function trail.
+The Mercury implementation ensures that
if future execution ever backtracks to current choicepoint,
then @code{(*@var{untrail_func})(@var{value}, MR_undo)} will be called.
It also ensures that if the current choice point is pruned because
execution commits to never backtracking to it,
then @code{(*@var{untrail_func})(@var{value}, MR_commit)} will be called.
+It also ensures that if execution requires that the current goal be
+solvable, then @code{(*@var{untrail_func})(@var{value}, MR_solve)}
+will be called. This happens in calls to @code{solutions/2}, for example.
+(@code{MR_commit} is used for ``hard'' commits, i.e. when we commit
+to a solution and prune away the alternative solutions; @code{MR_solve}
+is used for ``soft'' commits, i.e. when we must commit to a solution
+but do not prune away all the alternatives.)
MR_exception and MR_gc are currently not used ---
they are reserved for future use.
@@ -3217,11 +3226,12 @@
@samp{MR_undo} or @samp{MR_exception}, then it should undo the effects
of the update(s) specified by @var{value}, and the free any resources
associated with that trail entry. If it is called with @var{reason}
-being @samp{MR_commit} then it should not undo the
-effects, instead it should merely free any resources associated with
-the trail entry. If it is called with anything else
-(such as @samp{MR_gc}), then it should probably abort execution
-with an error message.
+being @samp{MR_commit} or @samp{MR_solve}, then it not undo the update(s);
+instead, it may check for floundering (see the next section).
+In the @samp{MR_commit} case it may, in some cases, be possible to
+also free resources associated with the trail entry.
+If it is called with anything else (such as @samp{MR_gc}),
+then it should probably abort execution with an error message.
@node Delayed goals and floundering
@subsubsection Delayed goals and floundering
@@ -3246,10 +3256,12 @@
The check for floundering can be implemented using the function trail,
by simply calling @samp{MR_trail_function()} to add a function trail
entry whenever you create a delayed goal, and putting the appropriate
-check for floundering in the @samp{MR_commit} case of your function.
-(For an example of this, see the @samp{ML_cfloat_untrail_func()}
-function in the file @samp{extras/clpr/cfloat.m} in the Mercury
-distribution.)
+check for floundering in the @samp{MR_commit} and @samp{MR_solve} cases
+of your function.
+(For examples of this, see the @samp{ML_cfloat_untrail_func()}
+function in the file @samp{extras/clpr/cfloat.m} and the
+ at samp{ML_var_untrail_func} function in the file
+ at samp{extras/trailed_update/var.m} in the Mercury distribution.)
If your function does detect floundering, then it should print
an error message and then abort execution.
Index: extras/clpr/cfloat.m
===================================================================
RCS file: /home/staff/zs/imp/clpr/cfloat.m,v
retrieving revision 1.14
diff -u -r1.14 cfloat.m
--- cfloat.m 1997/09/23 16:47:37 1.14
+++ cfloat.m 1997/10/12 13:27:43
@@ -497,16 +497,18 @@
solver_backtrack((Word) trail[i]);
}
trtop = old_trtop;
+ ML_cfloat_current_cp = choicepoint;
break;
}
case MR_commit:
stamp = choicepoint->stamp;
+ /* fall through */
+ case MR_solve:
ML_cfloat_check_floundering(choicepoint->nl_eqn_top);
break;
default:
fatal_error(""cfloat.m: unknown MR_untrail_reason"");
}
- ML_cfloat_current_cp = choicepoint;
}
").
Index: extras/trailed_update/var.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/extras/trailed_update/var.m,v
retrieving revision 1.5
diff -u -r1.5 var.m
--- var.m 1997/10/07 11:47:59 1.5
+++ var.m 1997/10/12 12:22:21
@@ -438,6 +438,7 @@
break;
case MR_commit:
+ case MR_solve:
/*
** Skip past any goals that were created before
** the choice point which we're committing over,
Index: library/std_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/library/std_util.m,v
retrieving revision 1.107
diff -u -r1.107 std_util.m
--- std_util.m 1997/09/30 17:00:42 1.107
+++ std_util.m 1997/10/12 12:50:05
@@ -615,21 +615,33 @@
#define sofar_fv (framevar(3))
#define element_type_info_fv (framevar(4))
#define collection_type_info_fv (framevar(5))
+#ifdef MR_USE_TRAIL
+ #define saved_trail_ticket_fv (framevar(6))
+ #define num_framevars 7
+#else
+ #define num_framevars 6
+#endif
/*
- ** Create a nondet frame with 6 slots and set the failure continuation.
- ** The six frame slots are used to hold heap states and the
+ ** Create a nondet frame and set the failure continuation.
+ ** The frame slots are used to hold heap and trail states and the
** collector pred and the collection, and type infos for copying
** each solution, and for copying the collection back to the heap
** when we're done.
*/
- mkframe(""builtin_aggregate"", 6,
+ mkframe(""builtin_aggregate"", num_framevars,
LABEL(mercury__std_util__builtin_aggregate_4_0_i3));
/* save heap states */
saved_solhp_fv = (Word) solutions_heap_pointer;
mark_hp(saved_hp_fv);
- /* setup the (other) framevars */
+
+#ifdef MR_USE_TRAIL
+ /* save trail state */
+ MR_store_ticket(saved_trail_ticket_fv);
+#endif
+
+ /* save arguments into framevars */
collector_pred_fv = r4;
sofar_fv = r5;
element_type_info_fv = r1;
@@ -651,13 +663,16 @@
/* we found a solution (in r1) */
- /* XXX we should check for delayed non-linear constraints here */
+#ifdef MR_USE_TRAIL
+ /* check for outstanding delayed goals (``floundering'') */
+ MR_reset_ticket(saved_trail_ticket_fv, MR_solve);
+#endif
/* swap heaps so we build on solution heap */
swap_heap_and_solutions_heap();
/*
- ** deep copy solution to the solutions heap, up to the saved_hp
+ ** deep copy solution to the solutions heap, up to the saved_hp.
** Note that we need to save/restore the hp register, if it
** is transient, before/after calling deep_copy().
*/
@@ -694,6 +709,15 @@
/* reset heap */
restore_hp(saved_hp_fv);
+#ifdef MR_USE_TRAIL
+ /*
+ ** Reset the trail. This is necessary to undo any updates performed
+ ** by the called goal before it failed, and to avoid leaking memory
+ ** on the trail.
+ */
+ MR_reset_ticket(saved_trail_ticket_fv, MR_undo);
+#endif
+
/*
** deep_copy() the result to the mercury heap, copying
** everything between where we started on the solutions
@@ -722,6 +746,7 @@
#undef sofar_fv
#undef element_type_info_fv
#undef collection_type_info_fv
+#undef num_framevars
#else
@@ -735,13 +760,24 @@
#define collector_pred_fv (framevar(0))
#define sofar_fv (framevar(1))
+#ifdef MR_USE_TRAIL
+ #define saved_trail_ticket_fv (framevar(2))
+ #define num_framevars 3
+#else
+ #define num_framevars 2
+#endif
/* create a nondet stack frame with two slots, to hold the collector
pred and the collection, and set the failure continuation */
- mkframe(""builtin_aggregate"", 2,
+ mkframe(""builtin_aggregate"", num_framevars,
LABEL(mercury__std_util__builtin_aggregate_4_0_i3));
- /* setup the framevars */
+#ifdef MR_USE_TRAIL
+ /* save trail state */
+ MR_store_ticket(saved_trail_ticket_fv);
+#endif
+
+ /* save our arguments in framevars */
collector_pred_fv = r4;
sofar_fv = r5;
@@ -757,7 +793,10 @@
Define_label(mercury__std_util__builtin_aggregate_4_0_i1);
/* we found a solution (in r1) */
- /* XXX we should check for delayed non-linear constraints here */
+#ifdef MR_USE_TRAIL
+ /* check for outstanding delayed goals (``floundering'') */
+ MR_reset_ticket(saved_trail_ticket_fv, MR_solve);
+#endif
/* setup for calling the collector closure */
r4 = r1; /* put solution to be collected where we need it */
@@ -783,12 +822,22 @@
Define_label(mercury__std_util__builtin_aggregate_4_0_i3);
/* no more solutions */
+#ifdef MR_USE_TRAIL
+ /*
+ ** Reset the trail. This is necessary to undo any updates performed
+ ** by the called goal before it failed, and to avoid leaking memory
+ ** on the trail.
+ */
+ MR_reset_ticket(saved_trail_ticket_fv, MR_undo);
+#endif
+
/* return the collection and discard the frame we made */
builtin_aggregate_output = sofar_fv;
succeed_discard();
#undef collector_pred_fv
#undef sofar_fv
+#undef num_framevars
#endif
Index: runtime/mercury_trail.h
===================================================================
RCS file: /home/staff/zs/imp/mercury/runtime/mercury_trail.h,v
retrieving revision 1.10
diff -u -r1.10 mercury_trail.h
--- mercury_trail.h 1997/09/23 16:47:44 1.10
+++ mercury_trail.h 1997/10/12 07:46:40
@@ -27,7 +27,11 @@
** called when creating a choice point, or before a commit
** MR_reset_ticket()
** called when resuming forward execution after failing (MR_undo),
-** or after a commit (MR_commit)
+** or after a commit (MR_commit), or after a "soft commit"
+** [one that doesn't prune away all the alternative solutions,
+** but which does require us to commit to this goal being solvable]
+** in an if-then-else with a nondet condition, or in solutions/2
+** (MR_solve).
** MR_discard_ticket()
** called when cutting away or failing over the topmost choice point
** MR_mark_ticket_stack()
@@ -96,20 +100,50 @@
** traversed.
*/
typedef enum {
- MR_undo, /* Ordinary backtracking on failure. Function */
- /* trail entries are invoked and value trail */
- /* entries are used to restore memory. Then */
- /* these trail entries are discarded. */
- MR_commit, /* Pruning. Function trail entries are invoked */
- /* and discarded; value trail entries are just */
- /* discarded. */
- MR_exception, /* (reserved for future use) An exception was */
- /* thrown. Behaves as MR_undo, except that */
- /* function trail entries may choose to behave */
- /* differently for exceptions than for failure. */
- MR_gc /* (reserved for future use) Garbage collection. */
- /* The interface between the trail and accurate */
- /* garbage collection is not yet designed. */
+ /*
+ ** MR_undo:
+ ** Ordinary backtracking on failure.
+ ** Function trail entries are invoked and value
+ ** trail entries are used to restore memory.
+ ** Then these trail entries are discarded.
+ */
+ MR_undo,
+
+ /*
+ ** MR_commit:
+ ** A hard (pruning) commit.
+ ** Occurs when nondet/multi goal is called in a cc_nondet/cc_multi
+ ** context, or when a nondet/multi goal has no output variables.
+ ** Function trail entries are invoked.
+ */
+ MR_commit,
+
+ /*
+ ** MR_solve:
+ ** A soft (non-pruning) commit.
+ ** Used for the check for floundering in solutions/2
+ ** and in nondet if-the-elses.
+ ** Function trail entries are invoked.
+ */
+ MR_solve,
+
+ /*
+ ** MR_exception:
+ ** (reserved for future use)
+ ** An exception was thrown.
+ ** Behaves as MR_undo, except that function trail entries may
+ ** choose to behave differently for exceptions than for failure.
+ */
+ MR_exception,
+
+ /*
+ ** MR_gc:
+ ** Reserved for future use.
+ ** The interface between the trail and accurate
+ ** garbage collection is not yet designed.
+ */
+ MR_gc
+
} MR_untrail_reason;
typedef enum {
--
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3 | -- the last words of T. S. Garp.
More information about the developers
mailing list