[m-rev.] for review: resets and statistics for tabling

[Julien Fischer]

On Thu, 8 Jun 2006, Zoltan Somogyi wrote:

> Index: compiler/add_pragma.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/add_pragma.m,v
> retrieving revision 1.33
> diff -u -b -r1.33 add_pragma.m
> --- compiler/add_pragma.m	5 Jun 2006 02:26:06 -0000	1.33
> +++ compiler/add_pragma.m	6 Jun 2006 09:08:06 -0000

...

> @@ -1809,10 +1891,216 @@
>                  ],
>                  module_info_incr_errors(!ModuleInfo),
>                  write_error_pieces(Context, 0, Pieces, !IO)

...

> +table_info_global_var_name(ModuleInfo, SimpleCallId, ProcId) = VarName :-
> +    module_info_get_globals(ModuleInfo, Globals),
> +    globals.get_target(Globals, Target),
> +    expect(unify(Target, target_c), this_file,
> +        "memo table statistics and reset are supported only for C"),
> +    globals.lookup_bool_option(Globals, highlevel_code, HighLevelCode),
> +    module_info_get_name(ModuleInfo, ModuleName),
> +    SimpleCallId = simple_call_id(PredOrFunc, PredSymName, Arity),
> +    (
> +        HighLevelCode = yes,
> +        MaybeModuleName = no,
> +        unqualify_name(PredSymName, PredName),
> +        % We set CodeModel and NoReturnValue to dummy values because we cannot
> +        % do any better right now. The code in that outputs the mlds_proc_label

s/in that/that/

> +        % of an mlds_tabling_ref should use mlds_std_tabling_proc_label to
> +        % set these fields to the same values.

...

> Index: compiler/hlds_pred.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/hlds_pred.m,v
> retrieving revision 1.197
> diff -u -b -r1.197 hlds_pred.m
> --- compiler/hlds_pred.m	20 Apr 2006 05:36:53 -0000	1.197
> +++ compiler/hlds_pred.m	6 Jun 2006 07:01:19 -0000

...

> @@ -1599,6 +1581,10 @@
>      --->    direct(int)
>      ;       indirect(int, int).
>
> +    % This type is differs from the type table_step_kind in

Delete "is".

> +    % library/table_builtin.m in that (a) in gives more information about the
> +    % type of the corresponding argument (if this info is needed and
> +    % available), and (b) it doesn't have to handle dummy steps.
>  :- type table_trie_step
>      --->    table_trie_step_int
>      ;       table_trie_step_char

...

> Index: compiler/mlds.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/mlds.m,v
> retrieving revision 1.132
> diff -u -b -r1.132 mlds.m
> --- compiler/mlds.m	20 Apr 2006 05:36:55 -0000	1.132
> +++ compiler/mlds.m	6 Jun 2006 01:23:28 -0000

> @@ -1875,6 +1879,24 @@
>
>  wrapper_class_name = "mercury_code".
>
> +mlds_std_tabling_proc_label(ProcLabel0) = ProcLabel :-
> +     % We standardize the parts of PredLabel0 that aren't computable from
> +    % the tabling pragma, because the code that creates the reset predicate

Fix the indentation there.

> +    % in table_info_global_var_name in add_pragma.m doesn't have access to
> +    % this information.
> +    ProcLabel0 = mlds_proc_label(PredLabel0, ProcId),
> +    (
> +        PredLabel0 = mlds_user_pred_label(PorF, MaybeModuleName, Name,
> +            Arity, _, _),
> +        PredLabel = mlds_user_pred_label(PorF, MaybeModuleName, Name,
> +            Arity, model_det, no)
> +    ;
> +        PredLabel0 = mlds_special_pred_label(_, _, _, _),
> +        unexpected(this_file,
> +            "mlds_std_tabling_proc_label: mlds_special_pred_label")
> +    ),
> +    ProcLabel = mlds_proc_label(PredLabel, ProcId).
> +
>  flip_initial_case_of_final_part(unqualified(Name)) =
>      unqualified(flip_initial_case(Name)).
>  flip_initial_case_of_final_part(qualified(Qual, Name)) =

...

> Index: doc/reference_manual.texi
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/doc/reference_manual.texi,v
> retrieving revision 1.353
> diff -u -b -r1.353 reference_manual.texi
> --- doc/reference_manual.texi	7 Jun 2006 14:37:37 -0000	1.353
> +++ doc/reference_manual.texi	8 Jun 2006 02:08:27 -0000
> @@ -1,3 +1,4 @@
> + at c vim: expandtab
>  \input texinfo
>  @setfilename mercury_ref.info
>  @settitle The Mercury Language Reference Manual
> @@ -9187,33 +9188,64 @@
>  For some procedures, this recomputation can be very wasteful.
>
>  With tabled evaluation, the implementation keeps a table containing the
> -previously computed results of the specified procedure; at each
> -procedure call, the implementation will search the table to check
> -whether the answer(s) have already been computed and if so, the answers
> -will be returned directly from the tables rather than being recomputed.
> +previously computed results of the specified procedure;
> +this table is sometimes called the memo table
> +(since it ``remembers'' previous answers).
> +At each procedure call, the implementation will search the memo table
> +to check whether the answer(s) have already been computed,
> +and if so, the answers will be returned directly from the memo table
> +rather than being recomputed.
>  This can result in much faster execution, at the cost of additional
>  space to record answers in the table.
>
> -The implementation can optionally also check at runtime for the situation
> +The implementation can also check at runtime for the situation
>  where a procedure calls itself recursively with the same arguments,
>  which would normally result in a infinite loop;
>  if this situation is encountered, it can (at the programmer's option)
>  either throw an exception, or avoid the infinite loop
> -by computing solutions using the ``minimal model'' semantics.
> +by computing solutions using a ``minimal model'' semantics.
> +(Specifically, the minimal model computed by our implementation
> +is the perfect model.)
>
> -The current Mercury implementation thus supports
> +The current Mercury implementation supports
>  three different pragmas for tabling, to cover these three cases:
> - at samp{pragma memo} does no loop checking,
> - at samp{pragma loop_check} checks for loops
> -and throws an exception if a loop is detected,
> -while @samp{pragma minimal_model} computes the ``minimal model'' semantics.
> + at samp{loop_check}, @samp{memo}, and @samp{minimal_model}.
> +The @samp{loop_check} pragma asks only for loop checking.
> +With this pragma, the memo table will map each distinct set of input arguments
> +only to a single boolean saying whether
> +a call with those arguments is currently active or not;
> +the pragma's only effect is to cause the predicate to throw an exception
> +if this boolean says that the current call has the same arguments
> +as one of its ancestors, which indicates an infinite recursive loop.
> +The @samp{memo} pragma asks for both loop checking and memoization.
> +With this pragma, the memo table will map each distinct set of input arguments
> +either to the set of results computed previously for those arguments,
> +or to an indication that the call is still active
> +and thus those results are still being computed.
> +This predicate will thus look for infinite recursive loops
> +(and throw an exception if and when it finds one)
> +but it will also record all its solutions in the memo table,
> +and will avoid recomputing solutions
> +that are already available in the memo table.
> +The @samp{minimal_model} pragma asks for the computation
> +of a ``minimal model'' semantics.
> +These differs from the @samp{memo} pragma in that

s/differs/differ/

> +the detection of what appears to be an infinite recursive loop is not fatal.
> +The implementation will consider the apparently infinitely recursive calls
> +to fail if the call concerned has no way of computing any solutions
> +it hasn't already computed and recorded,
> +and it does have such a way, then it switches the execution to explore
> +those ways before coming back to the apparently infinitely recursive call.
>
>  The syntax for each of these declarations is
>
>  @example
>  :- pragma memo(@var{Name}/@var{Arity}).
> +:- pragma memo(@var{Name}/@var{Arity}, [@var{list of tabling attributes}]).
>  :- pragma loop_check(@var{Name}/@var{Arity}).
> +:- pragma loop_check(@var{Name}/@var{Arity}, [@var{list of tabling attributes}]).
>  :- pragma minimal_model(@var{Name}/@var{Arity}).
> +:- pragma minimal_model(@var{Name}/@var{Arity}, [@var{list of tabling attributes}]).
>  @end example
>
>  @noindent
> @@ -9229,46 +9261,93 @@
>
>  @example
>  :- pragma memo(@var{Name}(in, in, out)).
> +:- pragma memo(@var{Name}(in, in, out), [@var{list of tabling attributes}]).
>  :- pragma loop_check(@var{Name}(in, out)).
> +:- pragma loop_check(@var{Name}(in, out), [@var{list of tabling attributes}]).
>  :- pragma minimal_model(@var{Name}(in, in, out, out)).
> +:- pragma minimal_model(@var{Name}(in, in, out, out), [@var{list of tabling attributes}]).
>  @end example
>
> -We also support two faster variants of @samp{pragma memo}
> -that may be applicable in some circumstances.
> -The implementation of @samp{pragma memo}
> -looks up the value of each input argument in the call table,
> +Because all variants of tabling record the values of input arguments,
> +and all except @samp{loop_check} also record the values of output arguments,
> +you cannot apply any of these pragmas to procedures
> +whose arguments' modes include any unique component.
> +
> +The optional list of attributes allows programmers
> +to control some aspects of the management of the memo table(s)
> +of the procedure(s) affected by the pragma.
> +
> +The @samp{allow_reset} attribute asks the compiler
> +to define a predicate that, when called, resets the memo table.

What is the scope of this predicate?  Presumably local?  This should be
mentioned here (and also that it obeys the usual sub-module visibility
rules).  The same for the generated statistics predicate.

> +The name of this predicate will be ``table_reset_for'',
> +followed by the name of the tabled predicate, followed by its arity,
> +and (if the predicate has more than one mode) by the mode number
> +(the first declared mode is mode 0, the second is mode 1, and so on).
> +These three or four components are separated by underscores.

Add an example of this, e.g. for this

	:- pragma memo(foo/2, [allow_reset]).
	:- pred foo(int, int).
	:- mode foo(in, out) is det.
	:- mode foo(out, in) is nondet.

the compiler constructs:

	:- pred table_reset_for_foo_2_0(io::di, io::uo) is det.
	:- pred table_reset_for_foo_2_1(io:::di, io::uo) is det.

> +The reset predicate takes a di/uo pair of I/O states as arguments.
> +The presence of these I/O state arguments in the reset predicate,
> +and the fact that tabled predicates cannot have unique arguments
> +together imply that a memo table cannot be reset
> +while a call using that memo table is active.

I think that may be a bit limiting.  Consider the following funtion for
computing binomial coefficients:

	:- func bc(int, int) = int.

	bc(N, K) =
	    ( N > K, K > 0 -> bc(N - 1, K - 1) + bc(N - 1, K)
	    ; K = 0 -> 1
	    ; K = N -> 1
	    ; throw("...")
            ).

One of the attractive things about tabling is the ability to turn
straightfoward recursive definitions of functions like the above into dynamic
programming style ones just by the addition of a memo pragma.

Assuming that I wish to reset the memo table after each top-level call to this
function**, I am currently forced to write something like:

	:- func bin_coeff(int, int) = int.

	bin_coeff(N, K) = BC :-
	    some [!IO] (
		create_io_state(!:IO),
		reset_table_for_bc_2(!IO),
		consume_io_state(!.!IO),
            ),
            BC = bc(N, K).

(where create_io_state/1 and consume_io_state/1 are appropriately defined
foreign_procs).

I find this approach a little inconvenient.  What I would really like to have
is an impure_allow_table_reset attribute that generated an impure version of
the table reset predicate.  Then:

	:- func bin_coeff(int, int) = int.

	bin_coeff(N, K) = BC :-
	    promise_pure (
	        impure impure_reset_table_for_bc_2,
		BC = bc(N, K)
	    ).

I like this version better.  It doesn't require me to write foreign_procs and
it also doesn't require that my module import the io module.  While this is
all a matter of convenience it's the same one that sees us supporting
pure/impure mutables and pure/impure initialisers/finalisers.

The alternative to the above is to rely on the programmer to reset the memo
tables manually in a context where the I/O state is available.  That seems
undesirable for library procedures where ideally the user shouldn't need to
know anything of the evaluation method  (it would also require the table reset
predicates to be exported.)

** computing binomial coefficients isn't such a great example for this since
   I probably don't want to throw the computed answers away at all.  There
   are other dynamic programming style problems where keeping the memo tables
   between top-level invocations is not going to be helpful.

On another note: what happens in .par grades if one thread resets the table
while the other thread is using that memo table?

> +The @samp{statistics} attribute asks the compiler
> +to define a predicate that, when called,
> +returns statistics about the memo table.
> +The name of this predicate will be ``table_statistics_for'',
> +followed by the name of the tabled predicate, followed by its arity,
> +and (if the predicate has more than one mode) by the mode number
> +(the first declared mode is mode 0, the second is mode 1, and so on).
> +These three or four components are separated by underscores.
> +The reset predicate takes three arguments.

s/reset/statistics/
s/takes/has/

> +The second and third are a di/uo pair of I/O states as arguments,

Delete "as arguments".

> +while the first is a output argument which contains information

s/a/an/
s/which/that/

Again, I think there ought to be an example of this.

> +about accesses to and modifications of the procedure's memo table,
> +both since the creation of the table,
> +and since the last call to this predicate.
> +The type of this argument is defined in the file table_builtin.m
> +in the Mercury standard library.
> +That module also contains a predicate for printing out this information
> +in a programmer-friendly format.

table_builtin.m is currently excluded from the library reference manual.
You should separate out user and implementation specific code in the
interface of that module (in the usual fashion) and include it in the
library reference.

> +The remaining two attributes, @samp{fast_loose} and @samp{specified},
> +control how arguments are looked up in the memo table.
> +The default implementation
> +looks up the @emph{value} of each input argument,
>  and thus requires time proportional to
> -the number of function symbols in the input arguments
> -to look up the current call in the call table.
> -The @samp{pragma fast_loose_memo} variant
> -looks up only the address of each input argument in the call table,
> +the number of function symbols in the input arguments.
> +This is the only implementation allowed for minimal model tabling,
> +but for predicates tabled with the @samp{loop_check} and @samp{memo} pragmas,
> +programmers can also choose some other tabling methods.
> +
> +The @samp{fast_loose_memo} attribute asks the compiler to generate code
> +that looks up only the @emph{address} of each input argument in the memo table,
>  which means that the time required
> -to look up the current call in the call table
> -is linear only in the number of input arguments.
> +is linear only in the @emph{number} of input arguments, not their @emph{size}.
>  The tradeoff is that @samp{fast_loose_memo} does not recognize
>  calls as duplicates if they involve input arguments that are logically equal
>  but are stored at different locations in memory.
> -The following declarations call for this variant of tabling.
> +The following declaration calls for this variant of tabling.
>
>  @example
> -:- pragma fast_loose_memo(@var{Name}/@var{Arity}).
> -:- pragma fast_loose_memo(@var{Name}(in, in, out)).
> +:- pragma memo(@var{Name}(in, in, in, out),
> +	[allow_reset, statistics, fast_loose]).
>  @end example
>
> -The second variant of @samp{pragma memo} allows programmers to choose
> -individually for each input argument whether that argument
> -should be looked up in the call table by value or by address,
> +The @samp{specified} attribute allows programmers to choose
> +individually, for each input argument, whether that argument
> +should be looked up in the memo table by value or by address,
>  or whether it should be looked up at all:
>
>  @example
> -:- pragma memo(@var{Name}(in, in, in, out),
> -	[value, addr, promise_implied, output]).
> +:- pragma memo(@var{Name}(in, in, in, out), [allow_reset, statistics,
> +	specified([value, addr, promise_implied, output])]).
>  @end example
>
> -The second argument of this form of @samp{pragma memo} should be a list
> -with an element for each argument of the predicate or function concerned
> -(if a function, last element is for the return value).
> -For output arguments, the list element should be @samp{output};
> +The @samp{specified} attribute should have an argument which is a list,
> +and this list should contain one element
> +for each argument of the predicate or function concerned
> +(if a function, the last element is for the return value).
> +For output arguments, the list element should be @samp{output}.
>  For input arguments, the list element may be
>  @samp{value}, @samp{addr} or @samp{promise_implied}.
>  The first calls for tabling the argument by value,
> @@ -9291,29 +9370,30 @@
>  then this declaration can also be specified without giving the argument modes:
>
>  @example
> -:- pragma memo(@var{Name}/@var{Arity},
> -	[value, addr, promise_implied, output]).
> +:- pragma memo(@var{Name}/@var{Arity}, [allow_reset, statistics,
> +	specified([value, addr, promise_implied, output])]).
>  @end example
>
>  Note that a @samp{pragma minimal_model} declaration
>  changes the declarative semantics of the specified predicate or function:
>  instead of using the completion of the clauses as the basis for the semantics,
>  as is normally the case in Mercury,
> -the declarative semantics that is used is the ``minimal model'' semantics.
> +the declarative semantics that is used is a ``minimal model'' semantics,
> +specifically, the perfect model semantics.
>  Anything which is true or false in the completion semantics
> -is also true or false (respectively) in the minimal model semantics,
> -but there are goals for which the minimal model specifies
> +is also true or false (respectively) in the perfect model semantics,
> +but there are goals for which the perfect model specifies
>  that the result is true or false,
>  whereas the completion semantics leaves the result unspecified.
>  For these goals, the usual Mercury semantics requires the
>  implementation to either loop or report an error message,
> -but the minimal model semantics requires a particular answer to be returned.
> -In particular, the minimal model semantics says that
> +but the perfect model semantics requires a particular answer to be returned.
> +In particular, the perfect model semantics says that
>  any call that is not true in @emph{all} models is false.
>
>  Programmers should therefore use a @samp{pragma minimal_model} declaration
>  only in cases where their intended interpretation for a procedure
> -coincides with the minimal model for that procedure.
> +coincides with the perfect model for that procedure.
>  Fortunately, however, this is usually what programmers intend.
>
>  @c XXX give an example
> @@ -9329,15 +9409,13 @@
>  the execution mechanism required by minimal model tabling is quite complicated,
>  requiring the ability to delay goals and then wake them up again.
>  The Mercury implementation uses a technique based on
> -copying relevant parts of the stack to the heap when delaying goals,
> -similar to the one described in
> - at c XXX this citation doesn't come out properly in DVI format
> - at cite{CAT: the copying approach to tabling},
> -by B. Demoen and K. Sagonas.  @xref{[5]}.
> -This ensures that code which does not use tabling
> -does not pay any runtime overheads
> -from the more complicated execution mechanism
> -required by (minimal model) tabling.
> +copying relevant parts of the stack to the heap when delaying goals.
> +It is described in
> + at c XXX this citation may not come out properly in DVI format
> + at cite{Tabling in Mercury: design and implementation}
> +by Z. Somogyi and K. Sagonas,
> +Proceedings of the Eight International Symposium
> +on Practical Aspects of Declarative Languages.

... to be continued.

Julien.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------