[m-dev.] for review: fix bug with reused choicepoint ids

Fergus Henderson fjh at cs.mu.OZ.AU
Thu Mar 16 05:26:59 AEDT 2000


This change is an attempt to fix the problem that Warwick reported which
choicepoint ids (as returned from MR_CurrentChoicepointId()) being
reused during forward execution.

I think the basic idea of this fix is OK, but it's quite
likely I have some of the details wrong, and as yet I haven't
tested it.  Still, now would be a good time for any review
comments...

----------

Estimated hours taken: 10

Fix a bug where choice point ids were being reused after a commit,
rather than only after backtracking.

runtime/mercury_trail.h:
runtime/mercury_regorder.h:
runtime/mercury_regs.h:
runtime/mercury_wrapper.c:
runtime/mercury_context.h:
runtime/mercury_engine.h:
	A bunch of changes to add a new virtual register
	`MR_ticket_high_water':
	- in mercury_trail.h, add MR_ticket_high_water_var variable;
	- in mercury_regorder.h, add MR_ticket_high_water macro;
	- in mercury_regs.h, add MR_TICKET_HIGH_WATER_RN macro;
	- in mercury_wrapper.c, change
	  print_register_usage_counts() to handle
	  MR_TICKET_HIGH_WATER_RN.
	- in mercury_context.h and mercury_engine.h,
	  add code to save/restore this new register when
	  appropriate.

runtime/mercury_trail.h:
	- Change MR_store_ticket() so that it does
	  `MR_ticket_counter = ++MR_ticket_high_water'
	  rather than just `MR_ticket_counter++'.
	- Add new macros MR_prune_ticket() and MR_prune_tickets_to(),
	  which only reset MR_ticket_counter, not MR_ticket_high_water.
	- Change the old macros MR_discard_ticket() and MR_discard_tickets_to()
	  so that they reset both MR_ticket_high_water and MR_ticket_counter.
	- Add new macro MR_choicepoint_newer().
	- Enclose macro arguments in parentheses.
	- Some minor changes to the documentation.

doc/reference_manual.texi:
	Document MR_choicepoint_newer().
	Clarify the documentation in the "Avoiding Redundant Trailing"
	section.  Add a longish example.

compiler/llds.m:
	Add new `prune_ticket' and `prune_tickets_to' instructions,
	corresponding to the new macros defined in runtime/mercury_trail.h.
	Comment out the `discard_tickets_to' instruction, since it
	is no longer used in the compiler (the MR_discard_tickets_to()
	macro is only used by library/exception.m and the debugger's
	retry command).

compiler/ite_gen.m:
compiler/code_gen.m:
compiler/code_info.m:
	Change the trail handling code generated after commits
	so that the ticket is pruned rather than discarded.

library/exception.m:
	Change the trail handling code so that when the goal in an
	exception handler succeeds (rather than failing or throwing an
	exception), the trail ticket we created on entry to the
	handler is pruned rather than discarded.

compiler/dupelim.m:
compiler/livemap.m:
compiler/llds_common.m:
compiler/llds_out.m:
compiler/ml_elim_nested.m:
compiler/middle_rec.m:
compiler/opt_debug.m:
compiler/opt_util.m:
compiler/value_number.m:
compiler/vn_*.m:
	Trivial modifications to handle the changes to the
	trailing instructions.

Workspace: /d-drive/home/hg/fjh/mercury
Index: compiler/code_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/code_gen.m,v
retrieving revision 1.74
diff -u -d -r1.74 code_gen.m
--- compiler/code_gen.m	2000/03/13 02:22:57	1.74
+++ compiler/code_gen.m	2000/03/15 10:09:56
@@ -724,17 +724,17 @@
 			TraceSlotInfo = trace_slot_info(_, _, yes(_)),
 			CodeModel \= model_non
 		->
-			DiscardTraceTicketCode = node([
-				discard_ticket - "discard retry ticket"
+			PruneTraceTicketCode = node([
+				prune_ticket - "prune retry ticket"
 			])
 		;
-			DiscardTraceTicketCode = empty
+			PruneTraceTicketCode = empty
 		},
 
 		{ RestoreDeallocCode =
 			tree(RestoreSuccipCode,
 			tree(DeallocCode,
-			     DiscardTraceTicketCode))
+			     PruneTraceTicketCode))
 		},
 
 		code_info__get_maybe_trace_info(MaybeTraceInfo),
Index: compiler/code_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/code_info.m,v
retrieving revision 1.247
diff -u -d -r1.247 code_info.m
--- compiler/code_info.m	2000/02/10 01:59:49	1.247
+++ compiler/code_info.m	2000/03/15 11:05:09
@@ -2489,22 +2489,20 @@
 		{ RestoreCode = empty }
 	;
 		{ MaybeTrailSlots = yes(CounterSlot - TrailPtrSlot) },
-		{ CommitTrailCode = node([
+		{ CommitCode = node([
 			reset_ticket(lval(TrailPtrSlot), commit)
-				- "discard trail entries and restore trail ptr"
+				- "discard trail entries and restore trail ptr",
+			prune_tickets_to(lval(CounterSlot))
+				- "restore ticket counter (but not high water mark)"
 		]) },
-		{ RestoreTrailCode = node([
+		{ RestoreCode = node([
 			reset_ticket(lval(TrailPtrSlot), undo)
-				- "apply trail entries and restore trail ptr"
-		]) },
-		{ RestoreCounterCode = node([
-			discard_tickets_to(lval(CounterSlot))
-				- "restore the ticket counter"
+				- "apply trail entries and restore trail ptr",
+			discard_ticket
+				- "restore ticket counter and high water mark"
 		]) },
 		code_info__release_temp_slot(CounterSlot),
-		code_info__release_temp_slot(TrailPtrSlot),
-		{ CommitCode = tree(CommitTrailCode, RestoreCounterCode) },
-		{ RestoreCode = tree(RestoreTrailCode, RestoreCounterCode) }
+		code_info__release_temp_slot(TrailPtrSlot)
 	).
 
 %---------------------------------------------------------------------------%
@@ -2702,6 +2700,15 @@
 :- pred code_info__release_ticket(lval, code_info, code_info).
 :- mode code_info__release_ticket(in, in, out) is det.
 
+:- pred code_info__reset_and_prune_ticket(lval, reset_trail_reason,
+	code_tree, code_info, code_info).
+:- mode code_info__reset_and_prune_ticket(in, in, out, in, out) is det.
+
+:- pred code_info__reset_prune_and_release_ticket(lval, reset_trail_reason,
+	code_tree, code_info, code_info).
+:- mode code_info__reset_prune_and_release_ticket(in, in, out, in, out)
+	is det.
+
 :- pred code_info__reset_and_discard_ticket(lval, reset_trail_reason,
 	code_tree, code_info, code_info).
 :- mode code_info__reset_and_discard_ticket(in, in, out, in, out) is det.
@@ -2722,6 +2729,15 @@
 :- pred code_info__maybe_release_ticket(maybe(lval), code_info, code_info).
 :- mode code_info__maybe_release_ticket(in, in, out) is det.
 
+:- pred code_info__maybe_reset_and_prune_ticket(maybe(lval),
+	reset_trail_reason, code_tree, code_info, code_info).
+:- mode code_info__maybe_reset_and_prune_ticket(in, in, out, in, out) is det.
+
+:- pred code_info__maybe_reset_prune_and_release_ticket(maybe(lval),
+	reset_trail_reason, code_tree, code_info, code_info).
+:- mode code_info__maybe_reset_prune_and_release_ticket(in, in, out, in, out)
+	is det.
+
 :- pred code_info__maybe_reset_and_discard_ticket(maybe(lval),
 	reset_trail_reason, code_tree, code_info, code_info).
 :- mode code_info__maybe_reset_and_discard_ticket(in, in, out, in, out) is det.
@@ -2803,6 +2819,19 @@
 code_info__release_ticket(TicketSlot) -->
 	code_info__release_temp_slot(TicketSlot).
 
+code_info__reset_and_prune_ticket(TicketSlot, Reason, Code) -->
+	{ Code = node([
+		reset_ticket(lval(TicketSlot), Reason) - "Restore trail",
+		prune_ticket - "Prune ticket stack"
+	]) }.
+
+code_info__reset_prune_and_release_ticket(TicketSlot, Reason, Code) -->
+	{ Code = node([
+		reset_ticket(lval(TicketSlot), Reason) - "Release trail",
+		prune_ticket - "Prune ticket stack"
+	]) },
+	code_info__release_temp_slot(TicketSlot).
+
 code_info__reset_and_discard_ticket(TicketSlot, Reason, Code) -->
 	{ Code = node([
 		reset_ticket(lval(TicketSlot), Reason) - "Restore trail",
@@ -2839,6 +2868,22 @@
 		code_info__release_ticket(TicketSlot)
 	;
 		[]
+	).
+
+code_info__maybe_reset_and_prune_ticket(MaybeTicketSlot, Reason, Code) -->
+	( { MaybeTicketSlot = yes(TicketSlot) } ->
+		code_info__reset_and_prune_ticket(TicketSlot, Reason, Code)
+	;
+		{ Code = empty }
+	).
+
+code_info__maybe_reset_prune_and_release_ticket(MaybeTicketSlot, Reason,
+		Code) -->
+	( { MaybeTicketSlot = yes(TicketSlot) } ->
+		code_info__reset_prune_and_release_ticket(TicketSlot, Reason,
+			Code)
+	;
+		{ Code = empty }
 	).
 
 code_info__maybe_reset_and_discard_ticket(MaybeTicketSlot, Reason, Code) -->
Index: compiler/dupelim.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dupelim.m,v
retrieving revision 1.45
diff -u -d -r1.45 dupelim.m
--- compiler/dupelim.m	2000/01/14 01:10:16	1.45
+++ compiler/dupelim.m	2000/03/15 10:24:01
@@ -342,13 +342,16 @@
 		Instr1 = discard_ticket,
 		Instr = Instr1
 	;
+		Instr1 = prune_ticket,
+		Instr = Instr1
+	;
 		Instr1 = mark_ticket_stack(Lval1),
 		standardize_lval(Lval1, Lval),
 		Instr = mark_ticket_stack(Lval)
 	;
-		Instr1 = discard_tickets_to(Rval1),
+		Instr1 = prune_tickets_to(Rval1),
 		standardize_rval(Rval1, Rval),
-		Instr = discard_tickets_to(Rval)
+		Instr = prune_tickets_to(Rval)
 	;
 		Instr1 = incr_sp(_, _),
 		Instr = Instr1
@@ -627,15 +630,19 @@
 		Instr2 = Instr1,
 		Instr = Instr1
 	;
+		Instr1 = prune_ticket,
+		Instr2 = Instr1,
+		Instr = Instr1
+	;
 		Instr1 = mark_ticket_stack(Lval1),
 		Instr2 = mark_ticket_stack(Lval2),
 		most_specific_lval(Lval1, Lval2, Lval),
 		Instr = mark_ticket_stack(Lval)
 	;
-		Instr1 = discard_tickets_to(Rval1),
-		Instr2 = discard_tickets_to(Rval2),
+		Instr1 = prune_tickets_to(Rval1),
+		Instr2 = prune_tickets_to(Rval2),
 		most_specific_rval(Rval1, Rval2, Rval),
-		Instr = discard_tickets_to(Rval)
+		Instr = prune_tickets_to(Rval)
 	;
 		Instr1 = incr_sp(_, _),
 		Instr2 = Instr1,
Index: compiler/ite_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/ite_gen.m,v
retrieving revision 1.63
diff -u -d -r1.63 ite_gen.m
--- compiler/ite_gen.m	1999/09/20 08:16:48	1.63
+++ compiler/ite_gen.m	2000/03/15 10:59:32
@@ -111,17 +111,17 @@
 	code_info__pickup_zombies(Zombies),
 	code_info__make_vars_forward_dead(Zombies),
 
-		% Discard hp and trail ticket if the condition succeeded
+		% Discard hp and prune trail ticket if the condition succeeded
 	( { CondCodeModel = model_non } ->
 		% We cannot release the stack slots used for the heap pointer
 		% and the trail ticket if the condition can be backtracked
 		% into.
-		code_info__maybe_reset_and_discard_ticket(
-			MaybeTicketSlot, commit, DiscardTicketCode)
+		code_info__maybe_reset_and_prune_ticket(
+			MaybeTicketSlot, commit, PruneTicketCode)
 	;
 		code_info__maybe_release_hp(MaybeHpSlot),
-		code_info__maybe_reset_discard_and_release_ticket(
-			MaybeTicketSlot, commit, DiscardTicketCode)
+		code_info__maybe_reset_prune_and_release_ticket(
+			MaybeTicketSlot, commit, PruneTicketCode)
 	),
 
 	code_info__get_instmap(EndCondInstMap),
@@ -175,7 +175,7 @@
 		tree(CondTraceCode,
 		tree(CondCode,
 		tree(ThenNeckCode,
-		tree(DiscardTicketCode,
+		tree(PruneTicketCode,
 		tree(ThenTraceCode,
 		tree(ThenCode,
 		tree(ThenSaveCode,
@@ -305,7 +305,7 @@
 
 	( { CodeModel = model_det } ->
 			% the then branch will never be reached
-		{ DiscardTicketCode = empty },
+		{ PruneTicketCode = empty },
 		{ FailTraceCode = empty },
 		{ FailCode = empty }
 	;
@@ -313,8 +313,8 @@
 		% The call to reset_ticket(..., commit) here is necessary
 		% in order to properly detect floundering.
 		code_info__maybe_release_hp(MaybeHpSlot),
-		code_info__maybe_reset_discard_and_release_ticket(
-			MaybeTicketSlot, commit, DiscardTicketCode),
+		code_info__maybe_reset_prune_and_release_ticket(
+			MaybeTicketSlot, commit, PruneTicketCode),
 		trace__maybe_generate_negated_event_code(Goal, neg_failure,
 			FailTraceCode),
 		code_info__generate_failure(FailCode),
@@ -345,7 +345,7 @@
 		tree(EnterTraceCode,
 		tree(GoalCode,
 		tree(ThenNeckCode,
-		tree(DiscardTicketCode,
+		tree(PruneTicketCode,
 		tree(FailTraceCode,
 		tree(FailCode,
 		tree(ResumeCode,
Index: compiler/livemap.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/livemap.m,v
retrieving revision 1.46
diff -u -d -r1.46 livemap.m
--- compiler/livemap.m	2000/01/14 01:10:21	1.46
+++ compiler/livemap.m	2000/03/15 10:24:14
@@ -305,6 +305,12 @@
 		Instrs = Instrs0,
 		DontValueNumber = DontValueNumber0
 	;
+		Uinstr0 = prune_ticket,
+		Livevals = Livevals0,
+		Livemap = Livemap0,
+		Instrs = Instrs0,
+		DontValueNumber = DontValueNumber0
+	;
 		Uinstr0 = mark_ticket_stack(Lval),
 		set__delete(Livevals0, Lval, Livevals1),
 		opt_util__lval_access_rvals(Lval, Rvals),
@@ -313,7 +319,7 @@
 		Instrs = Instrs0,
 		DontValueNumber = DontValueNumber0
 	;
-		Uinstr0 = discard_tickets_to(Rval),
+		Uinstr0 = prune_tickets_to(Rval),
 		livemap__make_live_in_rval(Rval, Livevals0, Livevals),
 		Livemap = Livemap0,
 		Instrs = Instrs0,
Index: compiler/llds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/llds.m,v
retrieving revision 1.258
diff -u -d -r1.258 llds.m
--- compiler/llds.m	2000/03/10 13:37:43	1.258
+++ compiler/llds.m	2000/03/15 10:23:34
@@ -314,10 +314,14 @@
 
 	;	store_ticket(lval)
 			% Allocate a new "ticket" and store it in the lval.
+			%
+			% Operational semantics:
+			% 	MR_ticket_counter = ++MR_ticket_high_water;
+			% 	lval = MR_trail_ptr;
 
 	;	reset_ticket(rval, reset_trail_reason)
 			% The rval must specify a ticket allocated with
-			% `store_ticket' and not yet invalidated or
+			% `store_ticket' and not yet invalidated, pruned or
 			% deallocated.
 			% If reset_trail_reason is `undo', `exception', or
 			% `retry', restore any mutable global state to the
@@ -332,24 +336,58 @@
 			% 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'.
+			% Any invalidated ticket which has not yet been
+			% backtracked over should be pruned with
+			% `prune_ticket' or `prune_tickets_to'.
+			% Any invalidated ticket which has been backtracked
+			% over is useless and should be deallocated with
+			% `discard_ticket'.
+			%
+			% Operational semantics:
+			% 	MR_untrail_to(rval, reset_trail_reason);
+
+	;	prune_ticket
+			% Invalidates the most-recently allocated ticket.
+			%
+			% Operational semantics:
+			%	--MR_ticket_counter;
 
 	;	discard_ticket
 			% Deallocates the most-recently allocated ticket.
+			%
+			% Operational semantics:
+			%	MR_ticket_high_water = --MR_ticket_counter;
 
 	;	mark_ticket_stack(lval)
 			% Tell the trail sub-system to store a ticket counter
-			% (for later use in discard_tickets_upto)
+			% (for later use in prune_tickets_to)
 			% in the specified lval.
+			%
+			% Operational semantics:
+			%	lval = MR_ticket_counter;
 
-	;	discard_tickets_to(rval)
+	;	prune_tickets_to(rval)
 			% The rval must be a ticket counter obtained via
 			% `mark_ticket_stack' and not yet invalidated.
+			% Prunes any trail tickets allocated after
+			% the corresponding call to mark_ticket_stack.
+			% Invalidates any later ticket counters.
+			%
+			% Operational semantics:
+			%	MR_ticket_counter = rval;
+
+%	;	discard_tickets_to(rval)	% this is only used in
+						% the hand-written code in
+						% library/exception.m
+			% The rval must be a ticket counter obtained via
+			% `mark_ticket_stack' and not yet invalidated.
 			% Deallocates any trail tickets allocated after
 			% the corresponding call to mark_ticket_stack.
 			% Invalidates any later ticket counters.
+			%
+			% Operational semantics:
+			%	MR_ticket_counter = rval;
+			%	MR_ticket_high_water = MR_ticket_counter;
 
 	;	incr_sp(int, string)
 			% Increment the det stack pointer. The string is
Index: compiler/llds_common.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/llds_common.m,v
retrieving revision 1.29
diff -u -d -r1.29 llds_common.m
--- compiler/llds_common.m	2000/03/10 13:37:44	1.29
+++ compiler/llds_common.m	2000/03/15 10:38:40
@@ -311,11 +311,15 @@
 		Instr = Instr0,
 		Info = Info0
 	;
+		Instr0 = prune_ticket,
+		Instr = Instr0,
+		Info = Info0
+	;
 		Instr0 = mark_ticket_stack(_),
 		Instr = Instr0,
 		Info = Info0
 	;
-		Instr0 = discard_tickets_to(_),
+		Instr0 = prune_tickets_to(_),
 		Instr = Instr0,
 		Info = Info0
 	;
Index: compiler/llds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/llds_out.m,v
retrieving revision 1.136
diff -u -d -r1.136 llds_out.m
--- compiler/llds_out.m	2000/03/10 13:37:44	1.136
+++ compiler/llds_out.m	2000/03/15 16:37:12
@@ -1382,9 +1382,10 @@
 output_instruction_decls(reset_ticket(Rval, _Reason), DeclSet0, DeclSet) -->
 	output_rval_decls(Rval, "", "", 0, _, DeclSet0, DeclSet).
 output_instruction_decls(discard_ticket, DeclSet, DeclSet) --> [].
+output_instruction_decls(prune_ticket, DeclSet, DeclSet) --> [].
 output_instruction_decls(mark_ticket_stack(Lval), DeclSet0, DeclSet) -->
 	output_lval_decls(Lval, "", "", 0, _, DeclSet0, DeclSet).
-output_instruction_decls(discard_tickets_to(Rval), DeclSet0, DeclSet) -->
+output_instruction_decls(prune_tickets_to(Rval), DeclSet0, DeclSet) -->
 	output_rval_decls(Rval, "", "", 0, _, DeclSet0, DeclSet).
 output_instruction_decls(incr_sp(_, _), DeclSet, DeclSet) --> [].
 output_instruction_decls(decr_sp(_), DeclSet, DeclSet) --> [].
@@ -1696,13 +1697,16 @@
 output_instruction(discard_ticket, _) -->
 	io__write_string("\tMR_discard_ticket();\n").
 
+output_instruction(prune_ticket, _) -->
+	io__write_string("\tMR_prune_ticket();\n").
+
 output_instruction(mark_ticket_stack(Lval), _) -->
 	io__write_string("\tMR_mark_ticket_stack("),
 	output_lval_as_word(Lval),
 	io__write_string(");\n").
 
-output_instruction(discard_tickets_to(Rval), _) -->
-	io__write_string("\tMR_discard_tickets_to("),
+output_instruction(prune_tickets_to(Rval), _) -->
+	io__write_string("\tMR_prune_tickets_to("),
 	output_rval_as_type(Rval, word),
 	io__write_string(");\n").
 
Index: compiler/middle_rec.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/middle_rec.m,v
retrieving revision 1.81
diff -u -d -r1.81 middle_rec.m
--- compiler/middle_rec.m	2000/01/14 01:10:31	1.81
+++ compiler/middle_rec.m	2000/03/15 10:25:00
@@ -420,9 +420,10 @@
 middle_rec__find_used_registers_instr(reset_ticket(Rval, _Rsn), Used0, Used) :-
 	middle_rec__find_used_registers_rval(Rval, Used0, Used).
 middle_rec__find_used_registers_instr(discard_ticket, Used, Used).
+middle_rec__find_used_registers_instr(prune_ticket, Used, Used).
 middle_rec__find_used_registers_instr(mark_ticket_stack(Lval), Used0, Used) :-
 	middle_rec__find_used_registers_lval(Lval, Used0, Used).
-middle_rec__find_used_registers_instr(discard_tickets_to(Rval), Used0, Used) :-
+middle_rec__find_used_registers_instr(prune_tickets_to(Rval), Used0, Used) :-
 	middle_rec__find_used_registers_rval(Rval, Used0, Used).
 middle_rec__find_used_registers_instr(incr_sp(_, _), Used, Used).
 middle_rec__find_used_registers_instr(decr_sp(_), Used, Used).
Index: compiler/ml_elim_nested.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/ml_elim_nested.m,v
retrieving revision 1.3
diff -u -d -r1.3 ml_elim_nested.m
--- compiler/ml_elim_nested.m	1999/11/15 10:35:18	1.3
+++ compiler/ml_elim_nested.m	2000/03/15 10:25:19
@@ -767,9 +771,10 @@
 fixup_trail_op(reset_ticket(Rval0, Reason), reset_ticket(Rval, Reason)) -->
 	fixup_rval(Rval0, Rval).
 fixup_trail_op(discard_ticket, discard_ticket) --> [].
+fixup_trail_op(prune_ticket, prune_ticket) --> [].
 fixup_trail_op(mark_ticket_stack(Lval0), mark_ticket_stack(Lval)) -->
 	fixup_lval(Lval0, Lval).
-fixup_trail_op(discard_tickets_to(Rval0), discard_tickets_to(Rval)) -->
+fixup_trail_op(prune_tickets_to(Rval0), prune_tickets_to(Rval)) -->
 	fixup_rval(Rval0, Rval).
 
 :- pred fixup_rvals(list(mlds__rval), list(mlds__rval), elim_info, elim_info).
@@ -1181,9 +1191,10 @@
 trail_op_contains_var(reset_ticket(Rval, _Reason), Name) :-
 	rval_contains_var(Rval, Name).
 trail_op_contains_var(discard_ticket, _Name) :- fail.
+trail_op_contains_var(prune_ticket, _Name) :- fail.
 trail_op_contains_var(mark_ticket_stack(Lval), Name) :-
 	lval_contains_var(Lval, Name).
-trail_op_contains_var(discard_tickets_to(Rval), Name) :-
+trail_op_contains_var(prune_tickets_to(Rval), Name) :-
 	rval_contains_var(Rval, Name).
 
 :- pred rvals_contains_var(list(mlds__rval), mlds__var).
Index: compiler/opt_debug.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/opt_debug.m,v
retrieving revision 1.99
diff -u -d -r1.99 opt_debug.m
--- compiler/opt_debug.m	2000/03/10 13:37:49	1.99
+++ compiler/opt_debug.m	2000/03/15 10:38:40
@@ -337,12 +337,13 @@
 	opt_debug__dump_vn(Vn, Vn_str),
 	string__append_list(["reset_ticket(", Vn_str, ", _)"], Str).
 opt_debug__dump_vninstr(vn_discard_ticket, "discard_ticket").
+opt_debug__dump_vninstr(vn_prune_ticket, "prune_ticket").
 opt_debug__dump_vninstr(vn_mark_ticket_stack(Vnlval), Str) :-
 	opt_debug__dump_vnlval(Vnlval, V_str),
 	string__append_list(["mark_ticket_stack(", V_str, ")"], Str).
-opt_debug__dump_vninstr(vn_discard_tickets_to(Vn), Str) :-
+opt_debug__dump_vninstr(vn_prune_tickets_to(Vn), Str) :-
 	opt_debug__dump_vn(Vn, Vn_str),
-	string__append_list(["discard_tickets_to(", Vn_str, ", _)"], Str).
+	string__append_list(["prune_tickets_to(", Vn_str, ", _)"], Str).
 opt_debug__dump_vninstr(vn_incr_sp(N, _), Str) :-
 	string__int_to_string(N, N_str),
 	string__append_list(["incr_sp(", N_str, ")"], Str).
@@ -990,12 +991,13 @@
 	opt_debug__dump_rval(Rval, R_str),
 	string__append_list(["reset_ticket(", R_str, ", _)"], Str).
 opt_debug__dump_instr(discard_ticket, "discard_ticket").
+opt_debug__dump_instr(prune_ticket, "prune_ticket").
 opt_debug__dump_instr(mark_ticket_stack(Lval), Str) :-
 	opt_debug__dump_lval(Lval, L_str),
 	string__append_list(["mark_ticket_stack(", L_str, ")"], Str).
-opt_debug__dump_instr(discard_tickets_to(Rval), Str) :-
+opt_debug__dump_instr(prune_tickets_to(Rval), Str) :-
 	opt_debug__dump_rval(Rval, R_str),
-	string__append_list(["discard_tickets_to(", R_str, ")"], Str).
+	string__append_list(["prune_tickets_to(", R_str, ")"], Str).
 opt_debug__dump_instr(incr_sp(Size, _), Str) :-
 	string__int_to_string(Size, S_str),
 	string__append_list(["incr_sp(", S_str, ")"], Str).
Index: compiler/opt_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/opt_util.m,v
retrieving revision 1.105
diff -u -d -r1.105 opt_util.m
--- compiler/opt_util.m	2000/01/14 01:10:36	1.105
+++ compiler/opt_util.m	2000/03/15 10:27:56
@@ -877,6 +877,9 @@
 		Uinstr0 = discard_ticket,
 		opt_util__block_refers_stackvars(Instrs0, Need)
 	;
+		Uinstr0 = prune_ticket,
+		opt_util__block_refers_stackvars(Instrs0, Need)
+	;
 		Uinstr0 = mark_ticket_stack(Lval),
 		opt_util__lval_refers_stackvars(Lval, Use),
 		( Use = yes ->
@@ -885,7 +888,7 @@
 			opt_util__block_refers_stackvars(Instrs0, Need)
 		)
 	;
-		Uinstr0 = discard_tickets_to(Rval),
+		Uinstr0 = prune_tickets_to(Rval),
 		opt_util__rval_refers_stackvars(Rval, Use),
 		( Use = yes ->
 			Need = yes
@@ -1019,8 +1022,9 @@
 opt_util__can_instr_branch_away(store_ticket(_), no).
 opt_util__can_instr_branch_away(reset_ticket(_, _), no).
 opt_util__can_instr_branch_away(discard_ticket, no).
+opt_util__can_instr_branch_away(prune_ticket, no).
 opt_util__can_instr_branch_away(mark_ticket_stack(_), no).
-opt_util__can_instr_branch_away(discard_tickets_to(_), no).
+opt_util__can_instr_branch_away(prune_tickets_to(_), no).
 opt_util__can_instr_branch_away(incr_sp(_, _), no).
 opt_util__can_instr_branch_away(decr_sp(_), no).
 opt_util__can_instr_branch_away(init_sync_term(_, _), no).
@@ -1084,8 +1088,9 @@
 opt_util__can_instr_fall_through(store_ticket(_), yes).
 opt_util__can_instr_fall_through(reset_ticket(_, _), yes).
 opt_util__can_instr_fall_through(discard_ticket, yes).
+opt_util__can_instr_fall_through(prune_ticket, yes).
 opt_util__can_instr_fall_through(mark_ticket_stack(_), yes).
-opt_util__can_instr_fall_through(discard_tickets_to(_), yes).
+opt_util__can_instr_fall_through(prune_tickets_to(_), yes).
 opt_util__can_instr_fall_through(incr_sp(_, _), yes).
 opt_util__can_instr_fall_through(decr_sp(_), yes).
 opt_util__can_instr_fall_through(init_sync_term(_, _), yes).
@@ -1129,8 +1134,9 @@
 opt_util__can_use_livevals(store_ticket(_), no).
 opt_util__can_use_livevals(reset_ticket(_, _), no).
 opt_util__can_use_livevals(discard_ticket, no).
+opt_util__can_use_livevals(prune_ticket, no).
 opt_util__can_use_livevals(mark_ticket_stack(_), no).
-opt_util__can_use_livevals(discard_tickets_to(_), no).
+opt_util__can_use_livevals(prune_tickets_to(_), no).
 opt_util__can_use_livevals(incr_sp(_, _), no).
 opt_util__can_use_livevals(decr_sp(_), no).
 opt_util__can_use_livevals(init_sync_term(_, _), no).
@@ -1191,8 +1197,9 @@
 opt_util__instr_labels_2(store_ticket(_), [], []).
 opt_util__instr_labels_2(reset_ticket(_, _), [], []).
 opt_util__instr_labels_2(discard_ticket, [], []).
+opt_util__instr_labels_2(prune_ticket, [], []).
 opt_util__instr_labels_2(mark_ticket_stack(_), [], []).
-opt_util__instr_labels_2(discard_tickets_to(_), [], []).
+opt_util__instr_labels_2(prune_tickets_to(_), [], []).
 opt_util__instr_labels_2(incr_sp(_, _), [], []).
 opt_util__instr_labels_2(decr_sp(_), [], []).
 opt_util__instr_labels_2(init_sync_term(_, _), [], []).
@@ -1249,8 +1256,9 @@
 opt_util__possible_targets(store_ticket(_), []).
 opt_util__possible_targets(reset_ticket(_, _), []).
 opt_util__possible_targets(discard_ticket, []).
+opt_util__possible_targets(prune_ticket, []).
 opt_util__possible_targets(mark_ticket_stack(_), []).
-opt_util__possible_targets(discard_tickets_to(_), []).
+opt_util__possible_targets(prune_tickets_to(_), []).
 opt_util__possible_targets(incr_sp(_, _), []).
 opt_util__possible_targets(decr_sp(_), []).
 opt_util__possible_targets(init_sync_term(_, _), []).
@@ -1297,8 +1305,9 @@
 opt_util__instr_rvals_and_lvals(store_ticket(Lval), [], [Lval]).
 opt_util__instr_rvals_and_lvals(reset_ticket(Rval, _Reason), [Rval], []).
 opt_util__instr_rvals_and_lvals(discard_ticket, [], []).
+opt_util__instr_rvals_and_lvals(prune_ticket, [], []).
 opt_util__instr_rvals_and_lvals(mark_ticket_stack(Lval), [], [Lval]).
-opt_util__instr_rvals_and_lvals(discard_tickets_to(Rval), [Rval], []).
+opt_util__instr_rvals_and_lvals(prune_tickets_to(Rval), [Rval], []).
 opt_util__instr_rvals_and_lvals(incr_sp(_, _), [], []).
 opt_util__instr_rvals_and_lvals(decr_sp(_), [], []).
 opt_util__instr_rvals_and_lvals(init_sync_term(Lval, _), [], [Lval]).
@@ -1439,9 +1448,10 @@
 opt_util__count_temps_instr(reset_ticket(Rval, _Reason), R0, R, F0, F) :-
 	opt_util__count_temps_rval(Rval, R0, R, F0, F).
 opt_util__count_temps_instr(discard_ticket, R, R, F, F).
+opt_util__count_temps_instr(prune_ticket, R, R, F, F).
 opt_util__count_temps_instr(mark_ticket_stack(Lval), R0, R, F0, F) :-
 	opt_util__count_temps_lval(Lval, R0, R, F0, F).
-opt_util__count_temps_instr(discard_tickets_to(Rval), R0, R, F0, F) :-
+opt_util__count_temps_instr(prune_tickets_to(Rval), R0, R, F0, F) :-
 	opt_util__count_temps_rval(Rval, R0, R, F0, F).
 opt_util__count_temps_instr(incr_sp(_, _), R, R, F, F).
 opt_util__count_temps_instr(decr_sp(_), R, R, F, F).
@@ -1871,6 +1881,7 @@
 		Rval = Rval0
 	).
 opt_util__replace_labels_instr(discard_ticket, _, _, discard_ticket).
+opt_util__replace_labels_instr(prune_ticket, _, _, prune_ticket).
 opt_util__replace_labels_instr(mark_ticket_stack(Lval0), ReplMap, ReplData,
 		mark_ticket_stack(Lval)) :-
 	(
@@ -1880,8 +1891,8 @@
 		ReplData = no,
 		Lval = Lval0
 	).
-opt_util__replace_labels_instr(discard_tickets_to(Rval0), ReplMap, ReplData,
-		discard_tickets_to(Rval)) :-
+opt_util__replace_labels_instr(prune_tickets_to(Rval0), ReplMap, ReplData,
+		prune_tickets_to(Rval)) :-
 	(
 		ReplData = yes,
 		opt_util__replace_labels_rval(Rval0, ReplMap, Rval)
Index: compiler/value_number.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/value_number.m,v
retrieving revision 1.102
diff -u -d -r1.102 value_number.m
--- compiler/value_number.m	2000/02/10 04:37:35	1.102
+++ compiler/value_number.m	2000/03/15 10:28:05
@@ -1120,8 +1120,9 @@
 value_number__boundary_instr(store_ticket(_), no).
 value_number__boundary_instr(reset_ticket(_, _), no).
 value_number__boundary_instr(discard_ticket, no).
+value_number__boundary_instr(prune_ticket, no).
 value_number__boundary_instr(mark_ticket_stack(_), no).
-value_number__boundary_instr(discard_tickets_to(_), no).
+value_number__boundary_instr(prune_tickets_to(_), no).
 value_number__boundary_instr(incr_sp(_, _), yes).
 value_number__boundary_instr(decr_sp(_), yes).
 value_number__boundary_instr(init_sync_term(_, _), no).
Index: compiler/vn_block.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_block.m,v
retrieving revision 1.62
diff -u -d -r1.62 vn_block.m
--- compiler/vn_block.m	2000/01/14 01:10:56	1.62
+++ compiler/vn_block.m	2000/03/15 10:54:08
@@ -341,6 +341,12 @@
 	vn_block__new_ctrl_node(vn_discard_ticket, Livemap,
 		Params, VnTables0, VnTables,
 		Liveset0, Liveset, Tuple0, Tuple).
+vn_block__handle_instr(prune_ticket,
+		Livemap, Params, VnTables0, VnTables, Liveset0, Liveset,
+		SeenIncr, SeenIncr, Tuple0, Tuple) :-
+	vn_block__new_ctrl_node(vn_prune_ticket, Livemap,
+		Params, VnTables0, VnTables,
+		Liveset0, Liveset, Tuple0, Tuple).
 vn_block__handle_instr(mark_ticket_stack(Lval),
 		Livemap, Params, VnTables0, VnTables, Liveset0, Liveset,
 		SeenIncr, SeenIncr, Tuple0, Tuple) :-
@@ -348,11 +354,11 @@
 	vn_block__new_ctrl_node(vn_mark_ticket_stack(Vnlval), Livemap,
 		Params, VnTables1, VnTables,
 		Liveset0, Liveset, Tuple0, Tuple).
-vn_block__handle_instr(discard_tickets_to(Rval),
+vn_block__handle_instr(prune_tickets_to(Rval),
 		Livemap, Params, VnTables0, VnTables, Liveset0, Liveset,
 		SeenIncr, SeenIncr, Tuple0, Tuple) :-
 	vn_util__rval_to_vn(Rval, Vn, VnTables0, VnTables1),
-	vn_block__new_ctrl_node(vn_discard_tickets_to(Vn), Livemap,
+	vn_block__new_ctrl_node(vn_prune_tickets_to(Vn), Livemap,
 		Params, VnTables1, VnTables,
 		Liveset0, Liveset, Tuple0, Tuple).
 vn_block__handle_instr(incr_sp(N, Msg),
@@ -508,6 +514,13 @@
 		LabelNo = LabelNo0,
 		Parallels = []
 	;
+		VnInstr = vn_prune_ticket,
+		VnTables = VnTables0,
+		Liveset = Liveset0,
+		FlushEntry = FlushEntry0,
+		LabelNo = LabelNo0,
+		Parallels = []
+	;
 		VnInstr = vn_mark_ticket_stack(Vnlval),
 		( vn_table__search_desired_value(Vnlval, Vn_prime, VnTables0) ->
 			Vn = Vn_prime,
@@ -522,7 +535,7 @@
 		LabelNo = LabelNo0,
 		Parallels = []
 	;
-		VnInstr = vn_discard_tickets_to(_),
+		VnInstr = vn_prune_tickets_to(_),
 		VnTables = VnTables0,
 		Liveset = Liveset0,
 		FlushEntry = FlushEntry0,
@@ -925,8 +938,9 @@
 vn_block__is_ctrl_instr(store_ticket(_), yes).
 vn_block__is_ctrl_instr(reset_ticket(_, _), yes).
 vn_block__is_ctrl_instr(discard_ticket, yes).
+vn_block__is_ctrl_instr(prune_ticket, yes).
 vn_block__is_ctrl_instr(mark_ticket_stack(_), yes).
-vn_block__is_ctrl_instr(discard_tickets_to(_), yes).
+vn_block__is_ctrl_instr(prune_tickets_to(_), yes).
 vn_block__is_ctrl_instr(incr_sp(_, _), yes).
 vn_block__is_ctrl_instr(decr_sp(_), yes).
 vn_block__is_ctrl_instr(init_sync_term(_, _), no).
Index: compiler/vn_cost.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_cost.m,v
retrieving revision 1.40
diff -u -d -r1.40 vn_cost.m
--- compiler/vn_cost.m	2000/01/14 01:10:57	1.40
+++ compiler/vn_cost.m	2000/03/15 10:28:44
@@ -168,11 +168,14 @@
 		Uinstr = discard_ticket,
 		Cost = 0
 	;
+		Uinstr = prune_ticket,
+		Cost = 0
+	;
 		Uinstr = mark_ticket_stack(Lval),
 		vn_cost__lval_cost(Lval, Params, LvalCost),
 		Cost = LvalCost
 	;
-		Uinstr = discard_tickets_to(Rval),
+		Uinstr = prune_tickets_to(Rval),
 		vn_cost__rval_cost(Rval, Params, RvalCost),
 		Cost = RvalCost
 	;
Index: compiler/vn_filter.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_filter.m,v
retrieving revision 1.24
diff -u -d -r1.24 vn_filter.m
--- compiler/vn_filter.m	2000/01/14 01:11:01	1.24
+++ compiler/vn_filter.m	2000/03/15 10:29:07
@@ -150,8 +150,9 @@
 vn_filter__user_instr(store_ticket(_), no).
 vn_filter__user_instr(reset_ticket(Rval, _Reason), yes(Rval)).
 vn_filter__user_instr(discard_ticket, no).
+vn_filter__user_instr(prune_ticket, no).
 vn_filter__user_instr(mark_ticket_stack(_), no).
-vn_filter__user_instr(discard_tickets_to(Rval), yes(Rval)).
+vn_filter__user_instr(prune_tickets_to(Rval), yes(Rval)).
 vn_filter__user_instr(incr_sp(_, _), no).
 vn_filter__user_instr(decr_sp(_), no).
 vn_filter__user_instr(pragma_c(_, _, _, _, _, _), _):-
@@ -216,10 +217,12 @@
 	vn_filter__replace_in_rval(Rval0, Temp, Defn, Rval).
 vn_filter__replace_in_user_instr(discard_ticket, _, _, _) :-
 	error("non-user instruction in vn_filter__replace_in_user_instr").
+vn_filter__replace_in_user_instr(prune_ticket, _, _, _) :-
+	error("non-user instruction in vn_filter__replace_in_user_instr").
 vn_filter__replace_in_user_instr(mark_ticket_stack(_), _, _, _) :-
 	error("non-user instruction in vn_filter__replace_in_user_instr").
-vn_filter__replace_in_user_instr(discard_tickets_to(Rval0), Temp, Defn,
-		discard_tickets_to(Rval)) :-
+vn_filter__replace_in_user_instr(prune_tickets_to(Rval0), Temp, Defn,
+		prune_tickets_to(Rval)) :-
 	vn_filter__replace_in_rval(Rval0, Temp, Defn, Rval).
 vn_filter__replace_in_user_instr(incr_sp(_, _), _, _, _) :-
 	error("non-user instruction in vn_filter__replace_in_user_instr").
@@ -261,8 +264,9 @@
 vn_filter__defining_instr(store_ticket(Lval), yes(Lval)).
 vn_filter__defining_instr(reset_ticket(_, _), no).
 vn_filter__defining_instr(discard_ticket, no).
+vn_filter__defining_instr(prune_ticket, no).
 vn_filter__defining_instr(mark_ticket_stack(Lval), yes(Lval)).
-vn_filter__defining_instr(discard_tickets_to(_), no).
+vn_filter__defining_instr(prune_tickets_to(_), no).
 vn_filter__defining_instr(incr_sp(_, _), no).
 vn_filter__defining_instr(decr_sp(_), no).
 vn_filter__defining_instr(pragma_c(_, _, _, _, _, _), _):-
@@ -324,10 +328,12 @@
 	error("non-def instruction in vn_filter__replace_in_defining_instr").
 vn_filter__replace_in_defining_instr(discard_ticket, _, _, _) :-
 	error("non-def instruction in vn_filter__replace_in_defining_instr").
+vn_filter__replace_in_defining_instr(prune_ticket, _, _, _) :-
+	error("non-def instruction in vn_filter__replace_in_defining_instr").
 vn_filter__replace_in_defining_instr(mark_ticket_stack(Lval0), Temp, Defn,
 		mark_ticket_stack(Lval)) :-
 	vn_filter__replace_in_lval(Lval0, Temp, Defn, Lval).
-vn_filter__replace_in_defining_instr(discard_tickets_to(_), _, _, _) :-
+vn_filter__replace_in_defining_instr(prune_tickets_to(_), _, _, _) :-
 	error("non-def instruction in vn_filter__replace_in_defining_instr").
 vn_filter__replace_in_defining_instr(incr_sp(_, _), _, _, _) :-
 	error("non-def instruction in vn_filter__replace_in_defining_instr").
Index: compiler/vn_flush.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_flush.m,v
retrieving revision 1.51
diff -u -d -r1.51 vn_flush.m
--- compiler/vn_flush.m	2000/01/14 01:11:02	1.51
+++ compiler/vn_flush.m	2000/03/15 10:30:00
@@ -269,6 +269,11 @@
 		Templocs = Templocs0,
 		Instrs = [discard_ticket - ""]
 	;
+		Vn_instr = vn_prune_ticket,
+		VnTables = VnTables0,
+		Templocs = Templocs0,
+		Instrs = [prune_ticket - ""]
+	;
 		Vn_instr = vn_mark_ticket_stack(Vnlval),
 		vn_flush__access_path(Vnlval, [src_ctrl(N)], [], Lval,
 			VnTables0, VnTables1, Templocs0, Templocs, Params,
@@ -279,10 +284,10 @@
 		Instr = mark_ticket_stack(Lval) - "",
 		list__append(FlushInstrs, [Instr], Instrs)
 	;
-		Vn_instr = vn_discard_tickets_to(Vn),
+		Vn_instr = vn_prune_tickets_to(Vn),
 		vn_flush__vn(Vn, [src_ctrl(N)], [], Rval, VnTables0, VnTables,
 			Templocs0, Templocs, Params, FlushInstrs),
-		Instr = discard_tickets_to(Rval) - "",
+		Instr = prune_tickets_to(Rval) - "",
 		list__append(FlushInstrs, [Instr], Instrs)
 	;
 		Vn_instr = vn_incr_sp(Incr, Msg),
Index: compiler/vn_order.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_order.m,v
retrieving revision 1.50
diff -u -d -r1.50 vn_order.m
--- compiler/vn_order.m	2000/01/14 01:11:03	1.50
+++ compiler/vn_order.m	2000/03/15 10:30:11
@@ -385,13 +385,18 @@
 			Predmap1 = Predmap0,
 			VnTables1 = VnTables0
 		;
+			Vn_instr = vn_prune_ticket,
+			Succmap1 = Succmap0,
+			Predmap1 = Predmap0,
+			VnTables1 = VnTables0
+		;
 			Vn_instr = vn_mark_ticket_stack(Vnlval),
 			vn_util__vnlval_access_vns(Vnlval, Vns),
 			vn_order__find_all_links(Vns, node_ctrl(Ctrl),
 				VnTables0, VnTables1,
 				Succmap0, Succmap1, Predmap0, Predmap1)
 		;
-			Vn_instr = vn_discard_tickets_to(Vn),
+			Vn_instr = vn_prune_tickets_to(Vn),
 			vn_order__find_links(Vn, node_ctrl(Ctrl),
 				VnTables0, VnTables1,
 				Succmap0, Succmap1, Predmap0, Predmap1)
Index: compiler/vn_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_type.m,v
retrieving revision 1.43
diff -u -d -r1.43 vn_type.m
--- compiler/vn_type.m	2000/01/14 01:11:05	1.43
+++ compiler/vn_type.m	2000/03/15 10:30:16
@@ -83,8 +83,9 @@
 			;	vn_store_ticket(vnlval)
 			;	vn_reset_ticket(vn, reset_trail_reason)
 			;	vn_discard_ticket
+			;	vn_prune_ticket
 			;	vn_mark_ticket_stack(vnlval)
-			;	vn_discard_tickets_to(vn)
+			;	vn_prune_tickets_to(vn)
 			;	vn_incr_sp(int, string)
 			;	vn_decr_sp(int).
 
Index: compiler/vn_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_util.m,v
retrieving revision 1.68
diff -u -d -r1.68 vn_util.m
--- compiler/vn_util.m	2000/01/14 01:11:06	1.68
+++ compiler/vn_util.m	2000/03/15 10:30:25
@@ -1273,12 +1273,15 @@
 			VnInstr = vn_discard_ticket,
 			VnTables1 = VnTables0
 		;
+			VnInstr = vn_prune_ticket,
+			VnTables1 = VnTables0
+		;
 			VnInstr = vn_mark_ticket_stack(Vnlval),
 			vn_util__vnlval_access_vns(Vnlval, Vns),
 			vn_util__record_use_list(Vns, src_ctrl(Ctrl),
 				VnTables0, VnTables1)
 		;
-			VnInstr = vn_discard_tickets_to(Vn),
+			VnInstr = vn_prune_tickets_to(Vn),
 			vn_util__record_use(Vn, src_ctrl(Ctrl),
 				VnTables0, VnTables1)
 		;
Index: compiler/vn_verify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/vn_verify.m,v
retrieving revision 1.24
diff -u -d -r1.24 vn_verify.m
--- compiler/vn_verify.m	2000/01/14 01:11:11	1.24
+++ compiler/vn_verify.m	2000/03/15 10:30:33
@@ -359,12 +359,16 @@
 		NoDeref = NoDeref0,
 		Tested = Tested0
 	;
+		Instr = prune_ticket,
+		NoDeref = NoDeref0,
+		Tested = Tested0
+	;
 		Instr = mark_ticket_stack(Lval),
 		vn_verify__tags_lval(Lval, NoDeref0),
 		NoDeref = NoDeref0,
 		Tested = Tested0
 	;
-		Instr = discard_tickets_to(Rval),
+		Instr = prune_tickets_to(Rval),
 		vn_verify__tags_rval(Rval, NoDeref0),
 		NoDeref = NoDeref0,
 		Tested = Tested0
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.175
diff -u -d -r1.175 reference_manual.texi
--- doc/reference_manual.texi	2000/03/08 13:16:50	1.175
+++ doc/reference_manual.texi	2000/03/15 05:52:38
@@ -5012,7 +5012,7 @@
 
 Ensures that if future execution backtracks to the
 current choice point, then @var{value} will be placed in @var{address}.
-
+ at sp 1
 @item @bullet{} @code{MR_trail_current_value()}
 Prototype:
 @example
@@ -5143,23 +5143,36 @@
 
 @table @b
 @item @bullet{} @code{MR_ChoicepointId}
- at itemx @bullet{} @code{MR_current_choicepoint_id()}
- at itemx @bullet{} @code{MR_null_choicepoint_id()}
-Prototypes:
+Declaration:
 @example
 typedef @dots{} MR_ChoicepointId;
-MR_ChoicepointId MR_current_choicepoint_id(void);
-MR_ChoicepointId MR_null_choicepoint_id(void);
 @end example
 
 The type @code{MR_ChoicepointId} is an abstract type used
 to hold the identity of a choice point.  Values of this
-type can be compared using C's @samp{==} operator.
+type can be compared using C's @samp{==} operator
+or using @samp{MR_choicepoint_newer()}.
+ at sp 1
+ at item @bullet{} @code{MR_current_choicepoint_id()}
+Prototype:
+ at example
+MR_ChoicepointId MR_current_choicepoint_id(void);
+ at end example
 
 @code{MR_current_choicepoint_id()} returns a value indicating
 the identity of the most recent choice point; that is, the
 point to which execution would backtrack if the current computation
 failed.
+The value remains meaningful if the choicepoint is pruned
+away by a commit, but is not meaningful after backtracking
+past the point where the choicepoint was created (since
+choicepoint ids may be reused after backtracking).
+ at sp 1
+ at item @bullet{} @code{MR_null_choicepoint_id()}
+Prototype:
+ at example
+MR_ChoicepointId MR_null_choicepoint_id(void);
+ at end example
 
 @code{MR_null_choicepoint_id()} returns a ``null'' value that is
 distinct from any value ever returned by @code{MR_current_choicepoint_id}.
@@ -5167,6 +5180,18 @@
 is a macro that is guaranteed to be suitable for use as a
 static initializer, so that it can for example be used to
 provide the initial value of a C global variable.)
+ at sp 1
+ at item @bullet{} @code{MR_choicepoint_newer()}
+Prototype:
+ at example
+bool MR_choicepoint_newer(MR_ChoicepointId, MR_ChoicepointId);
+ at end example
+
+ at code{MR_choicepoint_newer(x, y)} true iff the choicepoint indicated by
+ at samp{x} is newer than (i.e. was created more recently than) the
+choicepoint indicated by @samp{y}.  The null ChoicepointId is considered
+older than any non-null ChoicepointId.  If either of the choice points
+have been backtracked over, the behaviour is undefined.
 
 @end table
 
@@ -5180,16 +5205,19 @@
 When you are about to modify your mutable data structure,
 you can then call @code{MR_current_choicepoint_id()} again and
 compare the result from that call with the value saved in
-the @samp{prev_choicepoint} field in the data structure. 
-If they are different, then you must trail the update,
-and update the prev_choicepoint field with the new value;
+the @samp{prev_choicepoint} field in the data structure
+using @code{MR_choicepoint_newer()}.
+If the current choicepoint is newer, then you must trail the update,
+and update the @samp{prev_choicepoint} field with the new value;
 furthermore, you must also take care that on backtracking the
 previous value of the @samp{prev_choicepoint} field in your data
 structure is restored to its previous value, by trailing that update too.
-But if @code{MR_current_choice_id()} and the @code{prev_choicepoint} field
-are equal, then you can safely perform the update to your data
-structure without trailing it.
+But if @code{MR_current_choice_id()} is not newer than the
+ at code{prev_choicepoint} field, then you can safely perform
+the update to your data structure without trailing it.
 
+For an example, see the sample module below.
+
 Note that there is a cost to this -- you have to include
 an extra field in your data structure for each part of
 the data structure which you might update, you
@@ -5198,6 +5226,80 @@
 then you have an extra field that you need to trail.
 Whether or not the benefits from avoiding redundant trailing
 outweigh these costs will depend on your application.
+
+ at example
+:- module trailing_example.
+:- interface.
+
+:- type int_ref.
+
+    % Create a new int_ref with the specified value.
+:- pred new_int_ref(int_ref::uo, int::in) is det.
+
+    % update_int_ref(Ref0, Ref, OldVal, NewVal):
+    % Ref0 has value OldVal and Ref has value NewVal.
+:- pred update_int_ref(int_ref::mdi, int_ref::muo,
+        int::out, int::in) is det.
+
+:- implementation.
+
+:- type int_ref ---> int_ref(c_pointer).
+
+:- pragma import(new_int_ref(uo, in),
+	"new_int_ref").
+:- pragma import(update_int_ref(mdi, muo, out, in),
+	"update_int_ref").
+
+:- pragma c_header_code("
+typedef Word Mercury_IntRef;
+void new_int_ref(Mercury_IntRef *ref, Integer value);
+void update_int_ref(Mercury_IntRef ref0, Mercury_IntRef *ref,
+    Integer *old_value, Integer new_value);
+").
+
+:- pragma c_code("
+typedef struct @{
+    MR_ChoicepointId prev_choicepoint;
+    Integer data;
+@} C_IntRef;
+
+void
+new_int_ref(Mercury_IntRef *ref, Integer value)
+@{
+    C_IntRef *x = malloc(sizeof(C_IntRef));
+    x->prev_choicepoint = MR_current_choicepoint_id();
+    x->data = value;
+    *ref = (Mercury_IntRef) x;
+@}
+
+void
+update_int_ref(Mercury_IntRef ref0, Mercury_IntRef *ref,
+    Integer *old_value, Integer new_value)
+@{
+    C_IntRef *x = (C_IntRef *) ref0;
+    *old_value = x->data;
+
+    /* check whether we need to trail this update */
+    if (MR_choicepoint_newer(MR_current_choicepoint_id(),
+        x->prev_choicepoint))
+    @{
+        /* trail both x->data and x->prev_choicepoint,
+	   since we're about to update them both*/
+        assert(sizeof(x->data) == sizeof(Word));
+        assert(sizeof(x->prev_choicepoint) == sizeof(Word));
+        MR_trail_current_value((Word *)&x->data);
+        MR_trail_current_value((Word *)&x->prev_choicepoint);
+
+        /* update x->prev_choicepoint to indicate that
+           x->data's previous value has been trailed
+           at this choice point */
+        x->prev_choicepoint = MR_current_choicepoint_id();
+    @}
+    x->data = new_value;
+    *ref = ref0;
+@}
+").
+ at end example
 
 @c @item @code{void MR_untrail_to(MR_TrailEntry *@var{old_trail_ptr}, MR_untrail_reason @var{reason});}
 @c 
Index: library/exception.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/exception.m,v
retrieving revision 1.15
diff -u -d -r1.15 exception.m
--- library/exception.m	2000/03/10 01:21:31	1.15
+++ library/exception.m	2000/03/15 18:12:36
@@ -1075,7 +1075,7 @@
 	** were allocated by MR_create_exception_handler().
 	*/
 #ifdef MR_USE_TRAIL
-	MR_discard_ticket();
+	MR_prune_ticket();
 #endif
 	MR_succeed_discard();
 
@@ -1126,7 +1126,11 @@
 	** back to our caller.
 	*/
 #ifdef MR_USE_TRAIL
-	MR_discard_ticket();
+	if (r1) {
+		MR_prune_ticket();
+	} else {
+		MR_discard_ticket();
+	}
 #endif
 	MR_succeed_discard();
 
Index: runtime/mercury_context.h
===================================================================
RCS file: /home/mercury1/repository/mercury/runtime/mercury_context.h,v
retrieving revision 1.12
diff -u -d -r1.12 mercury_context.h
--- runtime/mercury_context.h	1999/10/27 05:18:07	1.12
+++ runtime/mercury_context.h	2000/03/15 18:04:54
@@ -124,6 +124,8 @@
 		/* saved MR_trail_ptr for this context */
 	MR_ChoicepointId context_ticket_counter;
 		/* saved MR_ticket_counter for this context */
+	MR_ChoicepointId context_ticket_high_water;
+		/* saved MR_ticket_high_water for this context */
 #endif
 
 	Word		*context_hp;
@@ -349,6 +351,8 @@
 		    MR_trail_ptr = load_context_c->context_trail_ptr;	\
 		    MR_ticket_counter =					\
 				load_context_c->context_ticket_counter;	\
+		    MR_ticket_high_water =				\
+			     load_context_c->context_ticket_high_water;	\
 	    	)							\
 		MR_ENGINE(context).detstack_zone =			\
 				load_context_c->detstack_zone;		\
@@ -384,6 +388,8 @@
 		    save_context_c->context_trail_ptr = MR_trail_ptr;	\
 		    save_context_c->context_ticket_counter =		\
 						MR_ticket_counter;	\
+		    save_context_c->context_ticket_high_water =		\
+						MR_ticket_high_water;	\
 		)							\
 		save_context_c->detstack_zone =				\
 				MR_ENGINE(context).detstack_zone;	\
Index: runtime/mercury_engine.h
===================================================================
RCS file: /home/mercury1/repository/mercury/runtime/mercury_engine.h,v
retrieving revision 1.15
diff -u -d -r1.15 mercury_engine.h
--- runtime/mercury_engine.h	2000/02/09 19:32:36	1.15
+++ runtime/mercury_engine.h	2000/03/15 18:06:51
@@ -90,6 +90,7 @@
 		Word *saved_maxfr;
 		MR_IF_USE_TRAIL(Word *saved_trail_ptr;)
 		MR_IF_USE_TRAIL(Word *saved_ticket_counter;)
+		MR_IF_USE_TRAIL(Word *saved_ticket_high_water;)
 
 #if NUM_REAL_REGS > 0
 		Word regs[NUM_REAL_REGS];
@@ -133,6 +134,8 @@
 				MR_trail_ptr);				\
 		MR_IF_USE_TRAIL((setjmp_env)->saved_ticket_counter =	\
 				MR_ticket_counter);			\
+		MR_IF_USE_TRAIL((setjmp_env)->saved_ticket_high_water =	\
+				MR_ticket_high_water);			\
 		if (setjmp((setjmp_env)->env)) {			\
 			MR_ENGINE(e_jmp_buf) = (setjmp_env)->mercury_env; \
 			restore_regs_from_mem((setjmp_env)->regs);	\
@@ -144,6 +147,8 @@
 					(setjmp_env)->saved_trail_ptr);	\
 			MR_IF_USE_TRAIL(MR_ticket_counter = 		\
 				(setjmp_env)->saved_ticket_counter);	\
+			MR_IF_USE_TRAIL(MR_ticket_high_water = 		\
+				(setjmp_env)->saved_ticket_high_water);	\
 			goto longjmp_label;				\
 		}							\
 	    } while (0)
Index: runtime/mercury_regorder.h
===================================================================
RCS file: /home/mercury1/repository/mercury/runtime/mercury_regorder.h,v
retrieving revision 1.12
diff -u -d -r1.12 mercury_regorder.h
--- runtime/mercury_regorder.h	1999/08/09 08:29:52	1.12
+++ runtime/mercury_regorder.h	2000/03/15 10:44:30
@@ -113,6 +113,8 @@
 #define MR_trail_ptr	count_usage(MR_TRAIL_PTR_RN, MR_trail_ptr_var)
 #define MR_ticket_counter	 \
 		count_usage(MR_TICKET_COUNTER_RN, MR_ticket_counter_var)
+#define MR_ticket_high_water	 \
+		count_usage(MR_TICKET_HIGH_WATER_RN, MR_ticket_high_water_var)
 
 /*
 ** the number of "very special" registers, i.e. special registers that can
@@ -259,6 +261,8 @@
 #define MR_trail_ptr	count_usage(MR_TRAIL_PTR_RN, MR_trail_ptr_var)
 #define MR_ticket_counter	 \
 		count_usage(MR_TICKET_COUNTER_RN, MR_ticket_counter_var)
+#define MR_ticket_high_water	 \
+		count_usage(MR_TICKET_HIGH_WATER_RN, MR_ticket_high_water_var)
 #define MR_gen_next	LVALUE_CAST(Integer,	\
 			count_usage(MR_GEN_NEXT_RN, mr(41)))
 #define MR_gen_stack	LVALUE_CAST(struct MR_GeneratorStackFrameStruct *, \
Index: runtime/mercury_regs.h
===================================================================
RCS file: /home/mercury1/repository/mercury/runtime/mercury_regs.h,v
retrieving revision 1.14
diff -u -d -r1.14 mercury_regs.h
--- runtime/mercury_regs.h	1999/10/05 20:21:41	1.14
+++ runtime/mercury_regs.h	2000/03/15 10:45:10
@@ -272,14 +272,15 @@
 #define	MR_MF_RN		(MR_ORD_RN + 4)
 #define MR_TRAIL_PTR_RN		(MR_ORD_RN + 5)
 #define MR_TICKET_COUNTER_RN	(MR_ORD_RN + 6)
-#define	MR_SOL_HP_RN		(MR_ORD_RN + 7)
-#define	MR_MIN_HP_REC		(MR_ORD_RN + 8)
-#define	MR_MIN_SOL_HP_REC	(MR_ORD_RN + 9)
-#define	MR_GLOBAL_HP_RN		(MR_ORD_RN + 10)
-#define	MR_GEN_STACK_RN		(MR_ORD_RN + 11)
-#define	MR_GEN_NEXT_RN		(MR_ORD_RN + 12)
-#define	MR_CUT_STACK_RN		(MR_ORD_RN + 13)
-#define	MR_CUT_NEXT_RN		(MR_ORD_RN + 14)
-#define	MAX_RN			(MR_ORD_RN + 15)
+#define MR_TICKET_HIGH_WATER_RN	(MR_ORD_RN + 7)
+#define	MR_SOL_HP_RN		(MR_ORD_RN + 8)
+#define	MR_MIN_HP_REC		(MR_ORD_RN + 9)
+#define	MR_MIN_SOL_HP_REC	(MR_ORD_RN + 10)
+#define	MR_GLOBAL_HP_RN		(MR_ORD_RN + 11)
+#define	MR_GEN_STACK_RN		(MR_ORD_RN + 12)
+#define	MR_GEN_NEXT_RN		(MR_ORD_RN + 13)
+#define	MR_CUT_STACK_RN		(MR_ORD_RN + 14)
+#define	MR_CUT_NEXT_RN		(MR_ORD_RN + 15)
+#define	MAX_RN			(MR_ORD_RN + 16)
 
 #endif /* not MERCURY_REGS_H */
Index: runtime/mercury_trail.h
===================================================================
RCS file: /home/mercury1/repository/mercury/runtime/mercury_trail.h,v
retrieving revision 1.17
diff -u -d -r1.17 mercury_trail.h
--- runtime/mercury_trail.h	1999/10/08 02:56:20	1.17
+++ runtime/mercury_trail.h	2000/03/15 17:27:18
@@ -40,31 +40,51 @@
 **	  this goal being solvable] in an if-then-else with a nondet condition,
 **	  or in solutions/2 (MR_solve);
 **	- when executing a `retry' command in the debugger (MR_retry).
+** MR_prune_ticket()
+**	called when cutting away the topmost choice point
 ** MR_discard_ticket()
-**	called when cutting away or failing over the topmost choice point
+**	called when failing over the topmost choice point
 ** MR_mark_ticket_stack()
-**	called before a commit, and when entering an execution traced procedure
-** MR_discard_tickets_to()
+**	called before a commit,
+**	when establishing an exception handler,
+**	or when entering an execution traced procedure
+** MR_prune_tickets_to()
 **	called after a commit
+** MR_discard_tickets_to()
+**	called when an exception is thrown,
+**	or when doing a retry in the debugger
 */
 /*---------------------------------------------------------------------------*/
 
 /* void MR_mark_ticket_stack(Word &); */
 #define MR_mark_ticket_stack(save_ticket_counter)		\
 	do {							\
-		save_ticket_counter = MR_ticket_counter;	\
+		(save_ticket_counter) = MR_ticket_counter;	\
+	} while(0)
+
+/* void MR_prune_ticket(void); */
+#define MR_prune_ticket()					\
+	do {							\
+		--MR_ticket_counter;				\
 	} while(0)
 
 /* void MR_discard_ticket(void); */
 #define MR_discard_ticket()					\
 	do {							\
-		--MR_ticket_counter;				\
+		MR_ticket_high_water = --MR_ticket_counter;	\
+	} while(0)
+
+/* void MR_prune_tickets_to(Word); */
+#define MR_prune_tickets_to(save_ticket_counter)		\
+	do {							\
+		MR_ticket_counter = (save_ticket_counter);	\
 	} while(0)
 
 /* void MR_discard_tickets_to(Word); */
 #define MR_discard_tickets_to(save_ticket_counter)		\
 	do {							\
-		MR_ticket_counter = save_ticket_counter;	\
+		MR_ticket_high_water = MR_ticket_counter =	\
+			(save_ticket_counter);			\
 	} while(0)
 
 	/* 
@@ -75,7 +95,7 @@
 #define MR_store_ticket(save_trail_ptr)				\
 	do {							\
 		(save_trail_ptr) = (Word) MR_trail_ptr; 	\
-		++MR_ticket_counter;				\
+		MR_ticket_counter = ++MR_ticket_high_water;	\
 	} while(0)
 
 	/*
@@ -90,10 +110,10 @@
 #define MR_reset_ticket(old, kind)				\
 	do {							\
 		MR_TrailEntry *old_trail_ptr =  		\
-			(MR_TrailEntry *)old;			\
+			(MR_TrailEntry *) (old);		\
 		if (MR_trail_ptr != old_trail_ptr) {		\
 			/* save_transient_registers(); */	\
-			MR_untrail_to(old_trail_ptr, kind);	\
+			MR_untrail_to(old_trail_ptr, (kind));	\
 			/* restore_transient_registers(); */	\
 		}						\
 	} while(0)
@@ -141,7 +161,6 @@
 
 	/*
 	** 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.
@@ -305,15 +324,29 @@
 extern MR_TrailEntry *MR_trail_ptr_var;
 
 /*
-** An integer variable that is incremented whenever we create a choice
+** An integer variable that holds the current choice point identifier;
+** it is allocated a new value whenever we create a choice
 ** point (including semidet choice points, e.g. in an if-then-else)
-** and decremented whenever we remove one.
+** and it is reset whenever a choice point is backtracked over
+** or pruned away.
 **
 ** N.B.  Use `MR_ticket_counter', defined in mercury_regorder.h,
 ** not `MR_ticket_counter_var'.
 */
 extern Unsigned MR_ticket_counter_var;
 
+/*
+** An integer variable that is incremented whenever we create a choice
+** point (including semidet choice points, e.g. in an if-then-else)
+** and decremented or reset whenever we backtrack over one,
+** but which is _not_ decremented or reset when a choice point is
+** pruned away with a commit.
+**
+** N.B.  Use `MR_ticket_high_water', defined in mercury_regorder.h,
+** not `MR_ticket_high_water_var'.
+*/
+extern Unsigned MR_ticket_high_water_var;
+
 /*---------------------------------------------------------------------------*/
 /*
 ** This is the interface that should be used by C code that wants to
@@ -376,8 +409,13 @@
 /*
 ** MR_ChoicepointId MR_current_choicepoint_id(void);
 **
-** Returns a value indicative of the current
-** choicepoint.  If we execute
+** Returns a value indicative of the current choicepoint. 
+** The value remains meaningful if the choicepoint is pruned
+** away by a commit, but is not meaningful after backtracking
+** past the point where the choicepoint was created (since
+** choicepoint ids may be reused after backtracking).
+**
+** If we execute
 ** 
 ** 	oldcp = MR_current_choicepoint_id();
 ** 	... and a long time later ...
@@ -389,13 +427,27 @@
 ** then code A will be executed if and only if the
 ** current choicepoint is the same in both calls.
 */
-#define MR_current_choicepoint_id() ((const MR_ChoicepointId)MR_ticket_counter)
+#define MR_current_choicepoint_id() ((const MR_ChoicepointId) MR_ticket_counter)
 
 /*
 ** MR_ChoicepointId MR_null_choicepoint_id(void);
 **
 ** A macro defining a "null" ChoicepointId.
+** This is suitable for use in static initializers.
 */
 #define MR_null_choicepoint_id() ((const MR_ChoicepointId)0)
+
+/*
+** bool MR_choicepoint_newer(MR_ChoicepointId x, MR_ChoicepointId y);
+**
+** Returns true iff the choicepoint indicated by `x'
+** is newer than (i.e. was created more recently than)
+** the choicepoint indicated by `y'.
+** The null ChoicepointId is considered older than
+** any non-null ChoicepoindId.
+** If either of the choice points have been
+** backtracked over, the behaviour is undefined.
+*/
+#define MR_choicepoint_newer(x, y) ((x) > (y))
 
 #endif /* not MERCURY_TRAIL_H */
Index: runtime/mercury_wrapper.c
===================================================================
RCS file: /home/mercury1/repository/mercury/runtime/mercury_wrapper.c,v
retrieving revision 1.56
diff -u -d -r1.56 mercury_wrapper.c
--- runtime/mercury_wrapper.c	2000/03/10 13:38:17	1.56
+++ runtime/mercury_wrapper.c	2000/03/15 10:46:40
@@ -1022,6 +1022,9 @@
 			case MR_TICKET_COUNTER_RN:
 				printf("MR_ticket_counter");
 				break;
+			case MR_TICKET_HIGH_WATER_RN:
+				printf("MR_ticket_high_water");
+				break;
 			case MR_SOL_HP_RN:
 				printf("MR_sol_hp");
 				break;

-- 
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.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------



More information about the developers mailing list