[m-dev.] for review: fix bug with reused choicepoint ids
Fergus Henderson
fjh at cs.mu.OZ.AU
Mon Mar 20 03:10:55 AEDT 2000
On 16-Mar-2000, Warwick Harvey <wharvey at cs.monash.edu.au> wrote:
> Fergus wrote:
> > 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...
>
> This change seemed so simple, but the diff is so long... :-)
>
> I've only reviewed the compiler part so far, but that looks good.
I thought about it fairly carefully and in the process I found a few more
bugs. I also wrote some documentation on how the whole trailing thing hangs
together.
So, here's what follows:
- the new documentation, in human-readable text format
- a relative diff
- an updated full diff
- the new documentation, this time in HTML source format
Since this change is mostly bug fixes, I'll go ahead and commit it shortly,
once I've done a few more tests, unless those tests should happen to uncover
any major problems. If there are any review comments, I'll be happy to
address them with a separate change.
============================================================
new file compiler/notes/trailing.html, formatted via `lynx -dump'
============================================================
_________________________________________________________________
Trail Management
This document describes how the generated code and the runtime system
manage the trail.
It should be read in conjunction with the "Trailing" section of the
language reference manual.
_________________________________________________________________
Purpose of the trail
The trail is a data structure which in Mercury is used for three
things.
* For code using backtrackable destructive update (i.e. code with
modes such as `mdi'/`muo' which use `mostly_unique' insts), the
trail is used to undo backtrackable destructive updates to
arguments when backtracking (or the like) occurs.
* For code using dynamic moding (`any' insts), the trail is used to
undo updates to the representation of variable bindings or to the
constraint store when backtracking (or the like) occurs.
* For code using dynamic scheduling (where constraints are not
checked for satisfiability as soon as they are called, but are
instead delayed, with the variable bindings or constraint store
holding a representation of the delayed constraints), the trail is
also used to check for floundering (attempting to commit to a
solution which there are still outstanding delayed constraints).
_________________________________________________________________
Nature of the trail
The trail is represented as a stack of trail entries. There are two
kinds of trail entries, value trail entries and functions trail
entries.
Value trail entries hold two words, an address and its corresponding
saved value. C code can create a value trail entry before modifying
some data, and then on backtracking the Mercury runtime will reset the
modified word with the saved value.
Function trail entries hold a function pointer and an opaque (`void
*') data pointer. C code can register a function trail entry, and then
in certain circumstances the Mercury runtime will call back the
specified function with its correspoding data, also passing an
MR_trail_reason, which specifies why the function was called.
These circumstances (and their corresponding reasons) are:
* On backtracking, which is further subdivided into
+ ordinary backtracking on failure (MR_undo)
+ when an exception is thrown (MR_exception)
+ when executing a retry command in the debugger (MR_retry)
* At soft commits, e.g. for solutions/2 or if-then-elses with nondet
conditions (MR_solve)
* At hard commits (MR_commit)
In addition to the trail stack itself, which is implemented as an
array of trail entries (stored in the memory zone MR_trail_zone) and a
pointer to the first unused entry (MR_trail_ptr), the trail management
code also maintains the value of two additional variables,
MR_ticket_counter and MR_ticket_high_water, which are used to
implement the "trail ticket" abstraction (see below) and the
MR_current_choicepoint_id() macro (see the "avoiding redundant
trailing" section of the language reference manual).
_________________________________________________________________
Trail operations
The trail is implemented as an ADT which is modified only via certain
operations, which are mostly defined as macros in
runtime/mercury_trail.h. There are two kinds of trail operations:
public operations, which are available for use by the user in `pragma
c_code', and private operations, which are intended for use only by
the Mercury implementation itself.
Public trail operations
The public operations include
* operations to add entries to the trail: MR_trail_value(),
MR_trail_current_value(), and MR_trail_function().
* operations to query the value of MR_ticket_counter:
MR_current_choicepoint_id().
They are documented in the "Trailing" section of the Mercury language
reference manual.
Private trail operations
The private operations are used (indirectly) by the code generator,
which inserts calls to them in the generated code. The private
operations are also directly used by a few other parts of the Mercury
implementation, e.g. the exception handling code (library/exception.m
and the MR_create_exception_handler() macro in
runtime/mercury_stacks.h) and the support for the debugger's retry
command (MR_trace_retry() in trace/mercury_trace_internal.c). For each
private operation that the code generator can generate, there is a
corresponding LLDS or MLDS instruction. The private operations are
documented in runtime/mercury_trail.h, and also in compiler/llds.m,
and are also documented below.
_________________________________________________________________
Trail tickets
At any point where we create a choice point, i.e. a point to which we
may want to backtrack to (including exception handlers, and if
debugging is enabled, all procedure prologues [to handle the debugger
retry command]), or where we are about to start a goal for which we
may want to do a soft or hard commit, the code must allocate a trail
ticket, using the MR_store_ticket() macro. This saves the trail
pointer, and allocates a new ticket id by incrementing
MR_ticket_high_water and assigning that to MR_ticket_counter. Note
that the trail pointer is typically saved on the stack, but the ticket
id is only stored in MR_ticket_counter. If the code needs to save the
ticket id too, then it must call MR_mark_ticket_stack().
Whenever we backtrack, or whenever we do a hard or soft commit, the
code must call MR_reset_ticket(), passing it the trail pointer value
the was saved by MR_store_ticket(), together with the appropriate
MR_trail_reason. This will walk the trail, applying all the trail
entries. In addition, if the ticket will no longer be used, it should
then be pruned or discarded (see below).
Whenever we do a hard or soft commit, the code must "prune" the trail
tickets that we have allocated, using either MR_prune_ticket(), which
prunes the most recently allocated ticket, or MR_prune_tickets_to(),
which prunes all the tickets allocated since the corresponding call to
MR_mark_ticket_stack().
Whenever we backtrack, the code must "discard" the trail tickets that
have allocated since the choice point was created, using either
MR_discard_ticket(), which discards the most recently allocated
ticket, or MR_discard_tickets_to(), which prunes all the tickets
allocated since the corresponding call to MR_mark_ticket_stack().
_________________________________________________________________
Invariants
* MR_trail_ptr:
+ increases when trail entries are created
+ gets reset to its previous value on backtracking
+ does not decrease after commits
+ is non-decreasing during forward execution
* MR_ticket_high_water:
+ increases at each choice point
+ gets reset to its previous value on backtracking
+ does not decrease after commits
+ is non-decreasing during forward execution
* MR_ticket_counter:
+ increases at each choice point
+ gets reset to its previous value on backtracking or after
commits
+ is non-decreasing during commit-free forward execution
+ values are not reused during forward execution
+ any call to a model_det goal will leave it unchanged
(MR_ticket_counter may change during the execution of the
goal, but its value when the goal exits will be the same as
the value it had when the goal was entered, because the goal
must prune away any tickets that it allocates)
+ any call to a model_semi goal which succeeds will likewise
leave it unchanged
+ any call to a goal which fails will leave it unchanged (any
tickets allocated must be discarded or at least pruned before
failing)
_________________________________________________________________
_________________________________________________________________
Last update was $Date$ by $Author$@cs.mu.oz.au.
============================================================
RELATIVE DIFF
============================================================
--- CHANGES6.old Sun Mar 19 19:29:10 2000
+++ CHANGES6 Sun Mar 19 22:51:16 2000
@@ -1,9 +1,21 @@
-Estimated hours taken: 10
-
-Fix a bug where choice point ids were being reused after a commit,
-rather than only after backtracking.
+Estimated hours taken: 20
+Fix several bugs in the trail handling.
+Also improve the documentation of trailing, and add a new macro
+MR_choicepoint_newer() to the public trailing interface.
+
+The bugs which this change fixes are:
+ - choice point ids were being reused after commits,
+ rather than only after backtracking;
+ - for if-then-elses with nondet conditions, the generated code was
+ using MR_commit rather than MR_solve as the MR_untrail_reason;
+ - for semidet disjunctions, when committing to a particular disjunct
+ the generated code was not calling MR_reset_ticket(..., MR_commit)
+ to invoke function trail entries, and was also leaking a trail ticket
+ - the all-solutions predicates in std_util.m were leaking trail
+ tickets (i.e. allocating them but not pruning or discarding them).
+
runtime/mercury_trail.h:
runtime/mercury_regorder.h:
runtime/mercury_regs.h:
@@ -36,16 +48,24 @@
doc/reference_manual.texi:
Document MR_choicepoint_newer().
+ Update the documentation to reflect the fact that exceptions
+ are now a standard part of Mercury.
Clarify the documentation in the "Avoiding Redundant Trailing"
- section. Add a longish example.
+ section, and add a longish example.
+
+compiler/notes/trailing.html:
+ Add some documentation on the trail and how we manage it.
compiler/llds.m:
+compiler/mlds.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).
+ Replace the duplicated documentation in mlds.m with a pointer
+ to llds.m.
compiler/ite_gen.m:
compiler/code_gen.m:
@@ -53,11 +73,15 @@
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/ite_gen.m:
+ When generating the reset_ticket instruction for
+ if-then-elses with nondet conditions, use `solve'
+ rather than `commit' as the reset_trail_reason.
+
+compiler/disj_gen.m:
+ Add code to generate a reset_ticket(..., commit)
+ instruction at the end of every non-last disjunct
+ in semidet disjunctions.
compiler/dupelim.m:
compiler/livemap.m:
@@ -71,4 +95,16 @@
compiler/vn_*.m:
Trivial modifications to handle the changes to the
trailing instructions.
+
+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.
+
+library/std_util.m:
+ Add a new impure predicate `discard_trail_ticket', which calls
+ MR_discard_ticket(), and call it in `builtin_aggregate' and
+ `do_while' to discard the ticket that gets allocated by the
+ call to MR_store_ticket() in `get_registers'.
--- old2/disj_gen.m Thu Mar 16 05:26:48 2000
+++ disj_gen.m Sun Mar 19 22:16:43 2000
@@ -231,16 +231,19 @@
% We can backtrack to the next disjunct from outside,
% so we make sure every variable in the resume set
% is in its stack slot.
- code_info__flush_resume_vars_to_stack(ResumeVarsCode)
+ code_info__flush_resume_vars_to_stack(ResumeVarsCode),
% We hang onto any temporary slots holding saved
% heap pointers and/or tickets, thus ensuring that
% they will still be reserved after the disjunction.
+ { PruneTicketCode = empty }
;
{ ResumeVarsCode = empty },
code_info__maybe_release_hp(MaybeHpSlot),
- code_info__maybe_release_ticket(MaybeTicketSlot),
+ % we're committing to this disjunct
+ code_info__maybe_reset_prune_and_release_ticket(MaybeTicketSlot,
+ commit, PruneTicketCode),
code_info__reset_resume_known(BranchStart)
),
@@ -271,6 +274,7 @@
tree(TraceCode,
tree(GoalCode,
tree(ResumeVarsCode,
+ tree(PruneTicketCode,
tree(SaveCode,
tree(BranchCode,
RestCode))))))))))
--- old2/ite_gen.m Thu Mar 16 05:26:48 2000
+++ ite_gen.m Sun Mar 19 18:18:32 2000
@@ -115,13 +115,15 @@
( { 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_prune_ticket(
- MaybeTicketSlot, commit, PruneTicketCode)
+ % into. Nor can we prune the trail ticket that we allocated,
+ % since the condition may have allocated other trail tickets
+ % since then which have not yet been pruned.
+ code_info__maybe_reset_ticket(
+ MaybeTicketSlot, solve, ResetTicketCode)
;
code_info__maybe_release_hp(MaybeHpSlot),
code_info__maybe_reset_prune_and_release_ticket(
- MaybeTicketSlot, commit, PruneTicketCode)
+ MaybeTicketSlot, commit, ResetTicketCode)
),
code_info__get_instmap(EndCondInstMap),
@@ -175,7 +177,7 @@
tree(CondTraceCode,
tree(CondCode,
tree(ThenNeckCode,
- tree(PruneTicketCode,
+ tree(ResetTicketCode,
tree(ThenTraceCode,
tree(ThenCode,
tree(ThenSaveCode,
--- old2/mlds.m Thu Mar 16 05:26:48 2000
+++ mlds.m Sun Mar 19 19:48:41 2000
@@ -859,7 +859,8 @@
%
% trail management
- % For documentation, see the corresponding LLDS instructions.
+ % For documentation, see the corresponding LLDS instructions
+ % in llds.m.
%
:- type trail_op
---> store_ticket(mlds__lval)
@@ -868,6 +869,7 @@
; prune_ticket
; mark_ticket_stack(mlds__lval)
; prune_tickets_to(mlds__rval)
+% ; discard_tickets_to(mlds__rval) % used only by the library
.
%-----------------------------------------------------------------------------%
--- old/std_util.m Sun Mar 19 19:21:24 2000
+++ std_util.m Sun Mar 19 19:27:39 2000
@@ -628,11 +628,14 @@
% of the accumulator from the solutions heap
% back onto the ordinary heap, and then we can
% reset the solutions heap pointer.
+ % We also need to discard the trail ticket
+ % created by get_registers/3.
% /* Accumulator := MutVar */
impure get_mutvar(Mutvar, Accumulator1),
impure partial_deep_copy(SolutionsHeapPtr, Accumulator1,
Accumulator),
- impure reset_solutions_heap(SolutionsHeapPtr)
+ impure reset_solutions_heap(SolutionsHeapPtr),
+ impure discard_trail_ticket
).
% The code for do_while/4 is essentially the same as the code for
@@ -668,7 +671,8 @@
),
impure get_mutvar(Mutvar, Accumulator1),
impure partial_deep_copy(SolutionsHeapPtr, Accumulator1, Accumulator),
- impure reset_solutions_heap(SolutionsHeapPtr).
+ impure reset_solutions_heap(SolutionsHeapPtr),
+ impure discard_trail_ticket.
:- type heap_ptr ---> heap_ptr(c_pointer).
:- type trail_ptr ---> trail_ptr(c_pointer).
@@ -676,6 +680,9 @@
%
% Save the state of the Mercury heap and trail registers,
% for later use in partial_deep_copy/3 and reset_solutions_heap/1.
+% Note that this allocates a trail ticket;
+% you need to dispose of it properly when you're finished with it,
+% e.g. by calling discard_trail_ticket/0.
%
:- impure pred get_registers(heap_ptr::out, heap_ptr::out, trail_ptr::out)
is det.
@@ -704,6 +711,17 @@
#ifdef MR_USE_TRAIL
/* check for outstanding delayed goals (``floundering'') */
MR_reset_ticket(TrailPtr, MR_solve);
+#endif
+").
+
+%
+% Discard the topmost trail ticket.
+%
+:- impure pred discard_trail_ticket is det.
+:- pragma c_code(discard_trail_ticket, [will_not_call_mercury],
+"
+#ifdef MR_USE_TRAIL
+ MR_discard_ticket();
#endif
").
============================================================
FULL DIFF
============================================================
Estimated hours taken: 20
Fix several bugs in the trail handling.
Also improve the documentation of trailing, and add a new macro
MR_choicepoint_newer() to the public trailing interface.
The bugs which this change fixes are:
- choice point ids were being reused after commits,
rather than only after backtracking;
- for if-then-elses with nondet conditions, the generated code was
using MR_commit rather than MR_solve as the MR_untrail_reason;
- for semidet disjunctions, when committing to a particular disjunct
the generated code was not calling MR_reset_ticket(..., MR_commit)
to invoke function trail entries, and was also leaking a trail ticket
- the all-solutions predicates in std_util.m were leaking trail
tickets (i.e. allocating them but not pruning or discarding them).
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().
Update the documentation to reflect the fact that exceptions
are now a standard part of Mercury.
Clarify the documentation in the "Avoiding Redundant Trailing"
section, and add a longish example.
compiler/notes/trailing.html:
Add some documentation on the trail and how we manage it.
compiler/llds.m:
compiler/mlds.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).
Replace the duplicated documentation in mlds.m with a pointer
to llds.m.
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.
compiler/ite_gen.m:
When generating the reset_ticket instruction for
if-then-elses with nondet conditions, use `solve'
rather than `commit' as the reset_trail_reason.
compiler/disj_gen.m:
Add code to generate a reset_ticket(..., commit)
instruction at the end of every non-last disjunct
in semidet disjunctions.
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.
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.
library/std_util.m:
Add a new impure predicate `discard_trail_ticket', which calls
MR_discard_ticket(), and call it in `builtin_aggregate' and
`do_while' to discard the ticket that gets allocated by the
call to MR_store_ticket() in `get_registers'.
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:08
@@ -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/disj_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/disj_gen.m,v
retrieving revision 1.69
diff -u -d -r1.69 disj_gen.m
--- compiler/disj_gen.m 1999/11/17 01:35:30 1.69
+++ compiler/disj_gen.m 2000/03/19 11:16:43
@@ -231,16 +231,19 @@
% We can backtrack to the next disjunct from outside,
% so we make sure every variable in the resume set
% is in its stack slot.
- code_info__flush_resume_vars_to_stack(ResumeVarsCode)
+ code_info__flush_resume_vars_to_stack(ResumeVarsCode),
% We hang onto any temporary slots holding saved
% heap pointers and/or tickets, thus ensuring that
% they will still be reserved after the disjunction.
+ { PruneTicketCode = empty }
;
{ ResumeVarsCode = empty },
code_info__maybe_release_hp(MaybeHpSlot),
- code_info__maybe_release_ticket(MaybeTicketSlot),
+ % we're committing to this disjunct
+ code_info__maybe_reset_prune_and_release_ticket(MaybeTicketSlot,
+ commit, PruneTicketCode),
code_info__reset_resume_known(BranchStart)
),
@@ -271,6 +274,7 @@
tree(TraceCode,
tree(GoalCode,
tree(ResumeVarsCode,
+ tree(PruneTicketCode,
tree(SaveCode,
tree(BranchCode,
RestCode))))))))))
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:00
@@ -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/19 07:18:32
@@ -111,17 +111,19 @@
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)
+ % into. Nor can we prune the trail ticket that we allocated,
+ % since the condition may have allocated other trail tickets
+ % since then which have not yet been pruned.
+ code_info__maybe_reset_ticket(
+ MaybeTicketSlot, solve, ResetTicketCode)
;
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, ResetTicketCode)
),
code_info__get_instmap(EndCondInstMap),
@@ -175,7 +177,7 @@
tree(CondTraceCode,
tree(CondCode,
tree(ThenNeckCode,
- tree(DiscardTicketCode,
+ tree(ResetTicketCode,
tree(ThenTraceCode,
tree(ThenCode,
tree(ThenSaveCode,
@@ -305,7 +307,7 @@
( { CodeModel = model_det } ->
% the then branch will never be reached
- { DiscardTicketCode = empty },
+ { PruneTicketCode = empty },
{ FailTraceCode = empty },
{ FailCode = empty }
;
@@ -313,8 +315,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 +347,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/18 15:39:18
@@ -767,9 +767,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 +1182,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/mlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mlds.m,v
retrieving revision 1.16
diff -u -d -r1.16 mlds.m
--- compiler/mlds.m 2000/02/23 04:30:54 1.16
+++ compiler/mlds.m 2000/03/19 08:48:41
@@ -859,45 +859,17 @@
%
% trail management
+ % For documentation, see the corresponding LLDS instructions
+ % in llds.m.
%
:- type trail_op
-
---> store_ticket(mlds__lval)
- % Allocate a new "ticket" and store it in the lval.
-
; reset_ticket(mlds__rval, mlds__reset_trail_reason)
- % The rval must specify a ticket allocated with
- % `store_ticket' and not yet invalidated or
- % deallocated.
- % If undo_reason is `undo' or `exception', restore
- % 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' 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'.
-
; discard_ticket
- % Deallocates the most-recently allocated ticket.
-
+ ; prune_ticket
; mark_ticket_stack(mlds__lval)
- % Tell the trail sub-system to store a ticket counter
- % (for later use in discard_tickets_upto)
- % in the specified lval.
-
- ; discard_tickets_to(mlds__rval)
- % 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.
+ ; prune_tickets_to(mlds__rval)
+% ; discard_tickets_to(mlds__rval) % used only by the library
.
%-----------------------------------------------------------------------------%
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:04
@@ -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:06
@@ -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:10
@@ -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:24
@@ -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:32
@@ -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
cvs diff: compiler/notes/trailing.html is a new entry, no comparison available
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/19 07:11:06
@@ -4979,7 +4979,8 @@
@subsection Choice points
A ``choice point'' is a point in the computation to
-which execution might backtrack. The ``current''
+which execution might backtrack when a goal fails or
+throws an exception. The ``current''
choice point is the one that was most recently
encountered; that is also the one to which execution
will branch if the current computation fails.
@@ -5012,7 +5013,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
@@ -5033,14 +5034,13 @@
For more complicated uses of trailing, you can store the address
of a C function on the trail and have the Mercury runtime call your
-function back whenever future execution backtracks to the current choice point,
-or whenever that choice point is pruned, either because execution
-commits to never backtracking over that point, or because an
-exception was thrown, or possibly during garbage collection.
+function back whenever future execution backtracks to the current choice point
+or earlier, or whenever that choice point is pruned, because execution
+commits to never backtracking over that point,
+or whenever that choice point is garbage collected.
-Note that currently Mercury does not support exception handling,
-and the garbage collector in the current Mercury implementation
-does not garbage-collect the trail; these two cases are mentioned
+Note the garbage collector in the current Mercury implementation
+does not garbage-collect the trail; this case is mentioned
only so that we can cater for possible future extensions.
@table @b
@@ -5050,6 +5050,7 @@
typedef enum @{
MR_undo,
MR_exception,
+ MR_retry,
MR_commit,
MR_solve,
MR_gc
@@ -5065,9 +5066,15 @@
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,
+or backtracks past the current choicepoint to some earlier choicepoint,
+then @code{(*@var{untrail_func})(@var{value}, @var{reason})} will be called,
+where @var{reason} will be @samp{MR_undo} if the backtracking was due to
+a goal failing, @samp{MR_exception} if the backtracking was due to
+a goal throwing an exception, or @samp{MR_retry} if the backtracking
+was due to the use of the "retry" command in mdb, the Mercury debugger,
+or any similar user request in a debugger.
+The Mercury implementation 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)}
@@ -5077,15 +5084,15 @@
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.
+MR_gc is currently not used ---
+it is reserved for future use.
@end table
Typically if the @var{untrail_func} is called with @var{reason} being
- at 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}
+ at samp{MR_undo}, @samp{MR_exception}, or @samp{MR_retry}, 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} 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
@@ -5143,23 +5150,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,7 +5187,19 @@
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
The way these functions are generally used is as follows.
@@ -5180,15 +5212,18 @@
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
@@ -5198,6 +5233,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: library/std_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/std_util.m,v
retrieving revision 1.183
diff -u -d -r1.183 std_util.m
--- library/std_util.m 2000/03/13 04:24:15 1.183
+++ library/std_util.m 2000/03/19 08:27:39
@@ -628,11 +628,14 @@
% of the accumulator from the solutions heap
% back onto the ordinary heap, and then we can
% reset the solutions heap pointer.
+ % We also need to discard the trail ticket
+ % created by get_registers/3.
% /* Accumulator := MutVar */
impure get_mutvar(Mutvar, Accumulator1),
impure partial_deep_copy(SolutionsHeapPtr, Accumulator1,
Accumulator),
- impure reset_solutions_heap(SolutionsHeapPtr)
+ impure reset_solutions_heap(SolutionsHeapPtr),
+ impure discard_trail_ticket
).
% The code for do_while/4 is essentially the same as the code for
@@ -668,7 +671,8 @@
),
impure get_mutvar(Mutvar, Accumulator1),
impure partial_deep_copy(SolutionsHeapPtr, Accumulator1, Accumulator),
- impure reset_solutions_heap(SolutionsHeapPtr).
+ impure reset_solutions_heap(SolutionsHeapPtr),
+ impure discard_trail_ticket.
:- type heap_ptr ---> heap_ptr(c_pointer).
:- type trail_ptr ---> trail_ptr(c_pointer).
@@ -676,6 +680,9 @@
%
% Save the state of the Mercury heap and trail registers,
% for later use in partial_deep_copy/3 and reset_solutions_heap/1.
+% Note that this allocates a trail ticket;
+% you need to dispose of it properly when you're finished with it,
+% e.g. by calling discard_trail_ticket/0.
%
:- impure pred get_registers(heap_ptr::out, heap_ptr::out, trail_ptr::out)
is det.
@@ -704,6 +711,17 @@
#ifdef MR_USE_TRAIL
/* check for outstanding delayed goals (``floundering'') */
MR_reset_ticket(TrailPtr, MR_solve);
+#endif
+").
+
+%
+% Discard the topmost trail ticket.
+%
+:- impure pred discard_trail_ticket is det.
+:- pragma c_code(discard_trail_ticket, [will_not_call_mercury],
+"
+#ifdef MR_USE_TRAIL
+ MR_discard_ticket();
#endif
").
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:50
@@ -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;
============================================================
new file compiler/notes/trailing.html
============================================================
<html>
<head>
<title>
Trail Management
</title>
</head>
<body
bgcolor="#ffffff"
text="#000000"
>
<hr>
<!-------------------------->
<h1> Trail Management </h1>
This document describes how the generated code and
the runtime system manage the trail.
<p>
It should be read in conjunction with the
"Trailing" section of the language reference manual.
<p>
<hr>
<!-------------------------->
<h2> Purpose of the trail </h2>
The trail is a data structure which in Mercury is used for three things.
<ul>
<li> For code using backtrackable destructive update (i.e. code with modes
such as `mdi'/`muo' which use `mostly_unique' insts), the trail
is used to undo backtrackable destructive updates to arguments
when backtracking (or the like) occurs.
<li> For code using dynamic moding (`any' insts),
the trail is used to undo updates to the representation
of variable bindings or to the constraint store
when backtracking (or the like) occurs.
<li> For code using dynamic scheduling (where constraints
are not checked for satisfiability as soon as they are called,
but are instead delayed, with the variable bindings
or constraint store holding a representation of the delayed
constraints), the trail is also used to check for floundering
(attempting to commit to a solution which there are still
outstanding delayed constraints).
</ul>
<p>
<hr>
<!-------------------------->
<h2> Nature of the trail </h2>
The trail is represented as a stack of trail entries.
There are two kinds of trail entries, value trail entries
and functions trail entries.
<p>
Value trail entries hold two words, an address and its corresponding
saved value. C code can create a value trail entry before modifying
some data, and then on backtracking the Mercury runtime will reset
the modified word with the saved value.
<p>
Function trail entries hold a function pointer and an opaque (`void *')
data pointer. C code can register a function trail entry, and then in certain
circumstances the Mercury runtime will call back the specified function with
its correspoding data, also passing an MR_trail_reason, which specifies why
the function was called.
<p>
These circumstances (and their corresponding reasons) are:
<ul>
<li> On backtracking, which is further subdivided into
<ul>
<li> ordinary backtracking on failure (MR_undo)
<li> when an exception is thrown (MR_exception)
<li> when executing a retry command in the debugger (MR_retry)
</ul>
<li> At soft commits, e.g. for solutions/2 or if-then-elses with
nondet conditions (MR_solve)
<li> At hard commits (MR_commit)
</ul>
<p>
In addition to the trail stack itself, which is implemented as an array of
trail entries (stored in the memory zone MR_trail_zone) and a pointer to the
first unused entry (MR_trail_ptr), the trail management code also maintains
the value of two additional variables, MR_ticket_counter and
MR_ticket_high_water, which are used to implement the "trail ticket"
abstraction (see below) and the MR_current_choicepoint_id() macro
(see the "avoiding redundant trailing" section of the language reference manual).
<p>
<hr>
<!-------------------------->
<h2> Trail operations </h2>
The trail is implemented as an ADT which is modified only via
certain operations, which are mostly defined as macros in
runtime/mercury_trail.h.
There are two kinds of trail operations: public operations, which are
available for use by the user in `pragma c_code', and private operations,
which are intended for use only by the Mercury implementation itself.
<p>
<h3> Public trail operations </h3>
The public operations include
<ul>
<li> operations to add entries to the trail: MR_trail_value(),
MR_trail_current_value(), and MR_trail_function().
<li> operations to query the value of MR_ticket_counter:
MR_current_choicepoint_id().
</ul>
They are documented in the "Trailing" section of the Mercury language
reference manual.
<p>
<h3> Private trail operations </h3>
The private operations are used (indirectly) by the code generator, which
inserts calls to them in the generated code.
The private operations are also directly used by a few other parts of the
Mercury implementation, e.g. the exception handling code (library/exception.m
and the MR_create_exception_handler() macro in runtime/mercury_stacks.h) and
the support for the debugger's retry command (MR_trace_retry() in
trace/mercury_trace_internal.c).
For each private operation that the code generator can generate,
there is a corresponding LLDS or MLDS instruction.
The private operations are documented in runtime/mercury_trail.h,
and also in compiler/llds.m, and are also documented below.
<p>
<hr>
<!-------------------------->
<h2> Trail tickets </h2>
At any point where we create a choice point, i.e. a point to which we may want
to backtrack to (including exception handlers, and if debugging is enabled,
all procedure prologues [to handle the debugger retry command]), or where we
are about to start a goal for which we may want to do a soft or hard commit,
the code must allocate a trail ticket, using the MR_store_ticket() macro.
This saves the trail pointer, and allocates a new ticket id by incrementing
MR_ticket_high_water and assigning that to MR_ticket_counter. Note that the
trail pointer is typically saved on the stack, but the ticket id is only
stored in MR_ticket_counter. If the code needs to save the ticket id too,
then it must call MR_mark_ticket_stack().
<p>
Whenever we backtrack, or whenever we do a hard or soft commit,
the code must call MR_reset_ticket(), passing it the trail pointer
value the was saved by MR_store_ticket(), together with the appropriate
MR_trail_reason. This will walk the trail, applying all the trail
entries. In addition, if the ticket will no longer be used,
it should then be pruned or discarded (see below).
<p>
Whenever we do a hard or soft commit,
the code must "prune" the trail tickets that we have allocated,
using either MR_prune_ticket(), which prunes the most recently
allocated ticket, or MR_prune_tickets_to(), which prunes all the
tickets allocated since the corresponding call to MR_mark_ticket_stack().
<p>
Whenever we backtrack, the code must "discard" the trail tickets that have
allocated since the choice point was created,
using either MR_discard_ticket(), which discards the most recently
allocated ticket, or MR_discard_tickets_to(), which prunes all the
tickets allocated since the corresponding call to MR_mark_ticket_stack().
<p>
<hr>
<!-------------------------->
<h2> Invariants </h2>
<ul>
<li> MR_trail_ptr:
<ul>
<li> increases when trail entries are created
<li> gets reset to its previous value on backtracking
<li> does not decrease after commits
<li> is non-decreasing during forward execution
</ul>
<li> MR_ticket_high_water:
<ul>
<li> increases at each choice point
<li> gets reset to its previous value on backtracking
<li> does not decrease after commits
<li> is non-decreasing during forward execution
</ul>
<li> MR_ticket_counter:
<ul>
<li> increases at each choice point
<li> gets reset to its previous value on backtracking or after commits
<li> is non-decreasing during commit-free forward execution
<li> values are not reused during forward execution
<li> any call to a model_det goal will leave it unchanged
(MR_ticket_counter may change during the execution of the goal,
but its value when the goal exits will be the same
as the value it had when the goal was entered,
because the goal must prune away any tickets that
it allocates)
<li> any call to a model_semi goal which succeeds will likewise
leave it unchanged
<li> any call to a goal which fails will leave it unchanged
(any tickets allocated must be discarded or at least pruned
before failing)
</ul>
</ul>
<p>
<hr>
<!-------------------------->
<hr>
<!-------------------------->
Last update was $Date$ by $Author: fjh $@cs.mu.oz.au. <br>
</body>
</html>
--
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