diff: documentation for trailing interface

[Fergus Henderson]

doc/reference_manual.texi:
	Document the trailing interface.
	Document the `mdi', `muo', and `mui' modes.

NEWS:
	Point to the documentation for trailing.

Could someone please review this change?

cvs diff NEWS doc/reference_manual.texi
Index: NEWS
===================================================================
RCS file: /home/staff/zs/imp/mercury/NEWS,v
retrieving revision 1.72
diff -u -r1.72 NEWS
--- NEWS	1997/09/11 07:08:11	1.72
+++ NEWS	1997/09/19 06:45:17
@@ -36,10 +36,11 @@
   There is a new set of grades `*.tr' (e.g. `asm_fast.gc.tr') which
   provide support for trailing.  This could be used by predicates or
   functions defined using the C interface to perform such things as
-  constraint solving, backtrackable destructive update, and automatic
-  unwinding of database transactions on backtracking.  See the declarations
-  and comments at the end of runtime/mercury_trail.h for documentation
-  of the interface.
+  constraint solving, backtrackable destructive update, or even automatic
+  unwinding of database transactions on backtracking.  See the
+  documentation in the "Trailing" section of the Mercury language
+  reference manual (it's at the end of the "C interface" section,
+  which is in the chapter on "Pragmas").
 
 * We've added support for backtrackable destructive update on arrays.
 
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.68
diff -u -r1.68 reference_manual.texi
--- reference_manual.texi	1997/09/19 01:02:26	1.68
+++ reference_manual.texi	1997/09/19 06:53:27
@@ -1381,6 +1381,20 @@
 forward execution are counted - it is OK for @samp{mostly_unique} or
 @samp{mostly_dead} values to be needed again on backtracking.
 
+Mercury defines some standard modes for manipulating ``mostly unique''
+values, just as it does for unique values:
+
+ at example
+% mostly unique output
+:- mode muo :: free -> unique.
+
+% mostly unique input
+:- mode mui :: unique -> unique.
+
+% mostly destructive input
+:- mode mdi :: unique -> dead.
+ at end example
+
 @node Limitations of the current implementation
 @section Limitations of the current implementation
 
@@ -1389,6 +1403,8 @@
 modes in which anything but the top level of a variable is unique.
 If you do, you will get unique mode errors when you try
 to get a unique field of a unique data structure.
+It is also not possible to use unique-input modes;
+only destructive-input and unique-output modes work.
 
 The Mercury compiler does not (yet) reuse @samp{dead}
 values.  The only destructive update in the current implementation occurs
@@ -1396,14 +1412,6 @@
 implement structure reuse and compile-time garbage collection
 in the very near future.
 
-Reusing @samp{mostly_dead} values would require keeping a trail, which
-might negatively impact on the performance of code which didn't use
-backtrackable destructive update.  Furthermore, it wouldn't have such a
-big impact as reuse of @samp{dead} values; it really pays off only for
-large structures or arrays.  As a result, implementing reuse of
- at samp{mostly_dead} values is a much lower priority on our
-implementation schedule.
-
 @node Determinism
 @chapter Determinism
 
@@ -2681,6 +2689,7 @@
                                         structures in Mercury code.
 * Memory management::                   Caveats about passing dynamically
                                         allocated memory to or from C.
+* Trailing::                   		Undoing side-effects on backtracking.
 @end menu
 
 The Mercury distribution includes a number of examples of the
@@ -3020,6 +3029,271 @@
 for use when interfacing with other languages that can work for all
 methods of memory management, but more implementation experience is
 needed before we can formulate such an interface.
+
+ at node Trailing
+ at subsection Trailing
+
+In certain compilation grades (see the ``Compilation model options''
+section of the Mercury User's Guide), the University of Melbourne
+Mercury implementation supports trailing.  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''.  Then, if
+a computation fails, and execution backtracks to before those
+those updates were performed, the Mercury runtime engine will
+traverse the trail back to the most recent choice point,
+undoing all those updates.
+
+The interface used is a set of C functions (which are actually
+implemented as macros) and types.  Typically these will be
+called from C code within @samp{pragma c_code} declarations
+in Mercury code.
+
+For examples of the use of this interface, see the modules
+ at file{extras/trailed_update/tr_array.m} and
+ at file{extras/clpr/cfloat.m} in the Mercury distribution.
+
+ at menu
+* Choice points::
+* Value trailing::
+* Function trailing::
+* Delayed goals and floundering::
+* Avoiding redundant trailing::
+ at end menu
+
+ at node Choice points
+ at subsubsection Choice points
+
+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.
+
+When you trail an update, the Mercury engine will ensure that if
+execution ever backtracks to the choice point that was current
+at the time of trailing, then the update will be undone.
+
+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,
+the trail entries for those updates will be discarded;
+any updates occurring after that choice point will not be undone.
+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.
+
+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}.  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.
+
+ at node Value trailing
+ at subsubsection Value trailing
+
+The simplest form of trailing is value trailing.
+This allows you to trail updates to memory and have
+the Mercury runtime engine automatically undo them
+on backtracking.
+
+ at table @b
+ at item @bullet{} @code{MR_trail_value()}
+Prototype:
+ at example
+void MR_trail_value(Word *@var{address}, Word @var{value});
+ at end example
+
+Ensures that if future execution backtracks to the
+current choice point, then @var{value} will be placed in @var{address}.
+
+ at item @bullet{} @code{MR_trail_current_value()}
+Prototype:
+ at example
+void MR_trail_current_value(Word *@var{address});
+ at end example
+
+Ensures that if future execution backtracks to the
+current choice point, the value currently in @var{address}
+will be restored.
+
+ at samp{MR_trail_current_value(@var{address})} is equivalent to
+ at samp{MR_trail_value(@var{address}, *@var{address})}.
+
+ at end table
+
+ 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 currently Mercury does not support exception handling,
+and (as with most logic programming implementations) the garbage
+collector in the current Mercury implementation does not garbage-collect
+the trail; these two cases are mentioned only so that we can cater
+for possible future extensions.
+
+ at table @b
+ at item @bullet{} @code{MR_trail_function()}
+Prototype:
+ at example
+typedef enum @{
+        MR_undo,
+        MR_exception,
+        MR_commit,
+        MR_gc
+@} MR_untrail_reason;
+
+void MR_trail_function(
+        void (*@var{untrail_func})(Word, MR_untrail_reason),
+        Word @var{value}
+);
+ at end example
+ at noindent
+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.
+It also ensures that if the current choice point is pruned because
+execution commits to never backtracking to it,
+then @code{(*@var{untrail_func})(@var{value}, MR_commit)} will be called.
+
+MR_exception and MR_gc are currently not used ---
+they are reserved for future use.
+
+ at 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}
+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.
+
+ 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.  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.
+(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.
+
+The functions described below provide a means to avoid
+redundant trailing.
+
+ at table @b
+ at item @bullet{} @code{MR_ChoicepointId}
+ at itemx @bullet{} @code{MR_current_choicepoint_id()}
+ at itemx @bullet{} @code{MR_null_choicepoint_id()}
+Prototypes:
+ at example
+typedef ... MR_ChoicepointId;
+MR_ChoicepointId MR_current_choicepoint_id(void);
+MR_ChoicepointId MR_null_choicepoint_id(void);
+ at 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.
+
+ at 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.
+
+ at code{MR_null_choicepoint_id()} returns a "null" value that is
+distinct from any value ever returned by @code{MR_current_choicepoint_id}.
+(Note that @code{MR_null_choicepoint_id()}
+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 end table
+
+The way these functions are generally used is as follows.
+When you create a mutable data structure, you should call
+ at code{MR_current_choicepoint_id()} and save the value it returns
+as a @samp{prev_choicepoint} field in your data structure.
+(If your mutable data structure
+is a C global variable, then you can use MR_null_choicepoint_id()
+for the initial value of this @samp{prev_choicepoint} field.)
+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.
+
+Note that there is a cost to this -- you have to include
+an extra field in your data structure for each part of
+the data structure which you might update, and you
+need to perform a test for each update to decide whether
+or not to trail it.  Whether or not the benefits from
+avoiding redundant trailing outweigh these costs
+will depend on your application.
+
+ at c @item @code{void MR_untrail_to(MR_TrailEntry *@var{old_trail_ptr}, MR_untrail_reason @var{reason});}
+ at c 
+ at c Apply all the trail entries between @samp{MR_trail_ptr} and
+ at c @var{old_trail_ptr}, using the specified @var{reason}.
+ at c 
+ at c This function is called by the Mercury engine after backtracking,
+ at c after a commit, or after catching an exception.
+ at c There is probably little need for user code to call this function,
+ at c but it might be needed if you're doing certain low-level things
+ at c such as implementing your own exception handling.
 
 @node Inlining
 @section Inlining

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