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