Trailing

[Peter Schachte]

While you're all waiting for /home/mercury* to rise from the dead, here's
something to think about.

-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?

====================================================================

				Trailing in Mercury

Mercury has gotten along without a trail until now, but a trail will
be necessary to implement some desirable Mercury features (eg,
destructive update in mostly unique contexts).  The implementation of
the HAL language on top of Mercury will require Mercury to have a
trail also, so I'm putting forth this proposal.

The constraint grade currently has a sort of trail technology, but I
don't believe this will be adequate, largely because it's not modular
enough.  What I'm proposing is probably more efficient, too.  The
problem is that the Mercury system calls the user's code when a
choicepoint is to be created, and then again when a failure occurs.
Let's call these the setup and backtrack functions.  If there are
several different modules which need to trail entities, the user of
those modules will have to write their own setup and backtrack
functions, which just call all the other modules' setup and backtrack
functions.  This isn't very modular.  Furthermore, it's not very
efficient, as several functions have to be called every time a
choicepoint is created or backtracked into.

A much better approach, I believe, would be for the Mercury system to
provide a function to be called to push an entry on the trail, and not
to do anything special when a choicepoint is created.  For the (I
expect) usual case of a few individual memory locations (words) that
need to be reset to specific values on failure, probably the simple
solution of a stack of address-value pairs is best.  This can be
processed on failure very quickly.  Sometimes, unfortunately, a more
sophisticated form of trailing is necessary.  It may be possible for a
module to recompute the values to be reset more cheaply than a trail
can maintain them (when considering the time and space cost of
trailing).  Sometimes it may be necessary to interface with external
software (eg, a database system) on failure.  For such cases, I
believe the best solution is a stack of function pointer-datum pairs.

The obvious thing to do is to merge the two trails using a tag bit to
distinguish the cases.  However, Zoltan has pointed out that this will
very significantly slow the simple (common) case, so it should be
avoided.  This means there will have to be two trails, which isn't a
big deal.  But it also suggests there will be two trail pointers, and
therefore two new slots in each choicepoint to hold previous values of
those pointers.  I haven't been able to think of a way to avoid this;
I'd appreciate any ideas anyone has on this.  Note that a little
overhead in dealing with the function pointer trail is probably
acceptable.

One further feature is desirable.  It may be sometimes be desirable to
save away more information than necessary once per choicepoint, rather
than saving less once per update.  Eg, if choicepoints are rare and
updates very frequent, it may be best to implement small backtrackable
updatable arrays by copying the entire array each time the array is
changed since a new choicepoint has been created, and then do nothing
until the next choicepoint is created.  To do this we need a very
inexpensive way of determining whether or not a new choicepoint has
been created since the last time the array was copied.  The simplest
way to do this is probably to allow the user to read the current value
of the choicepoint register (cur_fr).

So this suggests the following interface:

	void  MR_trail_value(Word *address, Word value);
		Make sure that when the current execution is
		backtracked over, value is placed in address.
	
	enum {undo,commit} untrail_reason;

	void  MR_trail_function(void (*reset)(Word,untrail_reason),
				Word value);
		Make sure that when the current execution is
		backtracked over, (*reset)(value,undo) is called.
		Also make sure that if the current choicepoint is
		trimmed without being backtracked over (ie, the
		current choice is committed to), then
		(*reset)(value,commit) is called.

	Word *MR_current_choicepoint(void);
		Returns a value indicative of the current
		choicepoint.  If we execute

			oldcp=MR_current_choicepoint();
			... and a long time later ...
			if (oldcp==MR_current_choicepoint()) {A}

		then we can be assured that if the choicepoint current
		at the time of the first call to MR_current_choicepoint()
		has not been backtracked over before the second call,
		then code A will be executed if and only if the
		current choicepoint is the same in both calls.

	void *MR_cut_to_choicepoint(Word cp);
		Assigns cur_fr = cp, but first traverses the function
		trail calling (*reset)(value,commit) for each entry.
		This is the deepest of voodoo, mainly intended for
		Mercury developers to use to make sure that the
		MR_trail_function() protocol is observed.


MR_current_choicepoint() should either be inlined or defined as a
macro.

The reason for the second argument to the MR_trail_function() reset
function is that in some cases it may be desirable to be able to
execute code when a choice is backtracked over *or* when it is
committed to.  For example, in a database system it may be expensive
to maintain a "cursor" referring to choice of a database tuple any
longer than necessary.  If a tuple is committed to, it is desirable to
free it immediately.

I know there are probably not many (any?) predicates in the current
Mercury system or library that can commit to a choice, but they can be
written using the C interface.  It is debatable whether or not the
complication necessary to support this facility is worthwhile.  I'd be
very interested to hear arguments against it, or alternative solutions.

If/when Mercury supports exception handling, the untrail_reason enum
should be extended to include 'exception', and the trail functions for
all the choicepoints that are being "exceptioned over" should be
called with an untrail_reason of exception.  This is essential to
being able to implement what Common Lisp calls 'unwind-protect', a
very useful feature.

Alright, this is much too long already.  Comments/discussion invited.