[m-dev.] diff: documentation for trailing interface

[Peter Schachte]

On Fri, 19 Sep 1997, Fergus Henderson wrote:

> doc/reference_manual.texi:
> 	Document the trailing interface.
> 	Document the `mdi', `muo', and `mui' modes.
> 
> NEWS:
> 	Point to the documentation for trailing.

>Trailing is a means
> +of having side-effects such as destructive updates to data structures
> +undone on backtracking.

Not to be pedantic, but I think this sentence would be more readable with a
couple of commas:

	Trailing is a means of having side-effects, such as destructive
	updates to data structures, undone on backtracking.


>The basic idea is that during forward
> +execution, whenever you perform a destructive modification to
> +a data structure that may still be live on backtracking
> +you should record whatever information is necessary on
> +a stack-like data structure called the ``trail''.

s/backtracking/backtracking,/
s/necessary/necessary to restore it/

> +A "choice point" is a point in the computation to
> +which execution might backtrack.  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.

`Encountered' is not very well defined.  Could you say `created' instead?
Neither is actually correct, because after a failure, the choicepoint you
would fail back to on failure will not be the most recent one `created' *or*
`encountered.'  If you want to be accurate, maybe you could say

	The "current" choice point is the one that was most recently created
	but not yet failed back into or committed to.  This is also ....

But then, of course, you'd need to define `failed back into' and `committed
to'. 

> +Note that if the Mercury compiler determines that it will never
> +need to backtrack to a particular choice point, then it will
> +"prune" away that choice point.  If a choice point is pruned,

s/"prune"/``prune''/

> +the trail entries for those updates will be discarded;
> +any updates occurring after that choice point will not be undone.

s/occurring after that choice point/made since that choice point was created/

> +Execution may subsequently backtrack to a @emph{prior} choice point,
> +but if so, the values updated will not be live at that point, so
> +there is no need to undo the updates.

An explaination of why this is true would be helpful.

> +
> +For example:
> +
> + at example
> +:- mode q(out) is nondet.
> +:- mode r(in) is det.
> +
> +p :-
> +	q(X), r(X), fail.
> + at end example
> +
> +Here any choice points created in @code{q/1} will be pruned away
> +before the call to @code{r/1}.

Again, an explaination of why this is correct would be helpful.

> At the call to @code{fail},
> +execution will backtrack; any updates performed inside @code{q/1}
> +will not be undone, but that should be OK, since the variable
> + at samp{X} will no longer be live.

But q/1 has no inputs to destructively modify.  It *generates* X, so it
doesn't make sense for it to *modify* X.

It might be better if the example was:

	:- mode q(out) is nondet.
	:- mode r(mdi,muo) is det.
	:- mode s(in) is det.

	p :-
		q(X), r(X, Y), s(Y), fail.

though this example still doesn't make much sense as Mercury code.

> + at node Function trailing
> + at subsubsection Function trailing
> +
> +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 because the garbage collector determined
> +that the value being trailed is no longer accessible.

Note that your description of the MR_gc reason here is not in keeping with
the latest thinking (I've heard) on this.  In fact, the garbage collector
really has no way of knowing what value or values will be reset by a
function trail entry, so it has no way of knowing whether or not it's
live.  The idea was that the trail function would be called with reason
MR_gc when GC was *starting*.  The trail function would then be required to
register addresses that would be reset on failure and the values they'd be
reset to.  This would allow the garbage collector to update trail entries to
refer to the new, moved, addresses of heap contents.  Or soemthing like
that. 

> +A call to @samp{MR_trail_function(@var{untrail_func}, @var{value})}
> +ensures that
> +if future execution ever backtracks to current choicepoint,
> +then @code{(*@var{untrail_func})(@var{value}, MR_undo)} will called.

s/will/will be/

> +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}
> +being @samp{MR_commit} or @samp{MR_gc}, then it should not undo the
> +effects, instead it should merely free any resources associated with
> +the trail entry.

I don't think it's a good idea to encourage users to free resources when
reason is MR_gc.  I think it's probably better to encourage them to print a
message an abort if reason is anything but MR_undo, MR_exception, or
MR_commit.

> + at node Delayed goals and floundering
> + at subsubsection Delayed goals and floundering
> +
> +Another use for the function trail is check for floundering
> +in the presence of delayed goals.
> +
> +Often, when implementating certain kinds of constraint solvers, it may
> +not be possible to actually solve all of the constraints at the time
> +they are added.  Instead, it may be necessary to simply delay their
> +execution until a later time, in the hope the constraints may become
> +solvable when more information is available.  If you do implement a
> +constraint solver with these properties, then at certain points in
> +the computation --- for example, after executing a negated goal --- it
> +is important for the system to check that their are no outstanding
> +delayed goals which might cause failure, before execution commits
> +to this execution path.

I think this would be clearer if you add here:  

	If there are such delayed goals, then the computation is said
	to ``flounder.''

>  If this check was omitted, then it could
> +lead to unsound behavior,  such as a negation failing even though
> +logically speaking it ought to have succeeded.
> +
> +The check for floundering can be implemented using the function trail,
> +by simply calling @samp{MR_trail_function()} to add a function trail
> +entry whenever you create a delayed goal, and putting the appropriate
> +check for floundering in the @samp{MR_commit} case of your function.

I think you should explain here what the trail function should do in
the case of floundering.

> +(For an example of this, see the @samp{ML_cfloat_untrail_func()}
> +function in the file @samp{extras/clpr/cfloat.m} in the Mercury
> +distribution.)
> +
> + at node Avoiding redundant trailing
> + at subsubsection Avoiding redundant trailing
> +
> +If a mutable data structure is updated multiple times, and each update
> +is recorded on the trail using the functions described above, then
> +some of this trailing may be redundant.  It is generally not necessary
> +to record enough information to recover the original state of the
> +data structure for @emph{every} update on the trail; instead, it is
> +enough to record the original state of each updated data structure
> +just once for each choice point, rather than once for each update.

s/choice point,/choice point created after the data structure is allocated,/

> +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.
> +But if they are equal, then you can avoid trailing the
> +update.

i/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.  Mercury's value trail provides an easy way to
accomplish that./

> +
> +Note that there is a cost to this -- you have to include

s/--/---/


-Peter Schachte      URL:  http://www.cs.mu.oz.au/~pets/
pets at cs.mu.OZ.AU     PGP:  finger pets at 128.250.37.150 for key
    Do insects spend hours demammaling their programs?