Note-7-0-memoize
ACL2 Version 7.0 Notes on Changes to Memoization Implementation
See memoize for a user-level introduction to function
memoization. Here we summarize technical changes made in Version 7.0 of ACL2
to the implementation of function memoization; most ACL2 users should have no
need to read further in this topic. We thank Jared Davis for helpful
conversations.
The function memoize-init now resets the table *memo-max-sizes*,
which is used when creating memo tables and pons tables. This change may be
irrelevant, since generally memoize-init is only called at startup. But it
seemed appropriate to reset it along with all other globals involved in the
memoization implementation.
Lisp variable *print-pretty* is no longer globally set to t by
certain memoization code. Probably this change will not generally be
observable.
The utility clear-memoize-statistics now resets data for the pons
summary, but implementation function clear-memo-tables no longer does
so (it only calls clear-memoize-tables).
Avoided some recklessness in computing statistics related to ponsing
(specifically, replaced very-unsafe-incf by macro safe-incf-pons,
which is a wrapper for safe-incf).
Clear-memo-tables no longer takes &rest arguments, since it is
merely a wrapper for clear-memoize-tables, which does not (and did
not) take &rest arguments.
For the utility pons-summary, we no longer use our-syntax-nice;
so far example, *print-case* is not bound to :downcase.
Function internal-real-ticks (formerly internal-real-time) now
uses logand in its implementation, which should improve performance.
It also replaces, for non-static-hons implementations, the call
(get-internal-real-time) by (the mfixnum (get-internal-real-time)),
which can also help performance.
More principled, consistent use is made of our-syntax for suitable
printing.
Added ``TO DO'' comments near the top of source file
memoize-raw.lisp. Thanks to Jared Davis for suggesting some of
these.
We improved many comments in source file memoize-raw.lisp.
We did some renaming, including the following (note that
this is probably not a complete list):
- number-of-arguments -> mf-len-inputs
- number-of-return-values -> mf-len-outputs
- *compute-array* -> *callers-array*
- maybe-count-pons-calls -> incf-pons-calls
- maybe-count-pons-misses -> incf-pons-misses
- print-alist -> mf-print-alist
- shorten -> mf-shorten
- outside-p -> outside-caller-p
- ofni -> mf-make-symbol
- ofnum -> mf-num-to-string
- internal-real-time -> internal-real-ticks
- dcls -> mf-dcls
- hl-without-interrupts -> without-interrupts [which already existed]
- *ma-initial-max-symbol-to-fixnum* -> *initial-max-symbol-to-fixnum*
- REPLACEMENT:
*initial-max-memoize-fns* -> *initial-2max-memoize-fns*
We eliminated some dead code, including the following functions (probably
not a complete list): our-syntax-brief, ofnm, uses-state,
global-restore-memoize, prine-alist, set-gc-threshold,
our-gctime, and short-symbol-name, and all variants of format
functions with names starting with "of" except for ofni (now
mf-make-symbol) and ofnum (now mf-num-to-string). Also, we
moved memoize-here-come to community book
books/centaur/memoize/old/profile-raw.lsp. Regarding
our-syntax-brief: there had been one call, in print-call-stack, but
that call did not seem appropriate so we deleted it.
The variable *count-pons-calls* was deleted. It had been set to
t and was only used during macroexpansion of incf-pons-calls and
incf-pons-misses (formerly maybe-count-pons-calls and
maybe-count-pons-misses), where that macroexpansion was done at ACL2
build time — hence user setting of *count-pons-calls* had no
effect.
We eliminated a needless error check that prevented loading
memoize-raw.lisp without #+hons, since we don't currently ever
expect to try to do that.
Miscellaneous additional code cleanup has been done. Here is a (probably
very incomplete) list.
- Float-ticks/second-init uses a default rather than duplicating the
default's code, and has improved treatment of errors.
- Removed unused :before field of memoize-info-ht-entry
record.
- The implementations of number-of-arguments and
number-of-return-values (now called mf-len-inputs and
mf-len-outputs, respectively) have been made cleaner, in particular,
starting with an empty *number-of-arguments-and-values-ht*.
- New macros such as ma-index provide some abstraction, to give the
illusion that *memoize-call-array* is two-dimensional.
- We broke up some definitions, in particular substantially shortening
memoize-fn by moving parts of it into new functions
memoize-fn-inner-body, memoize-fn-outer-body, and
memoize-fn-def. A benefit: it is easy to see the definition that is
actually created when memoizing, by tracing memoize-fn-def.
- Added raw Lisp interface function mf-note-arity for informing
memoize-fn of input and output arities.
- Coerce-index asserts that an index is in range rather than treating
an out-of-range index as a symbol.
- We renamed some variables to make them clearer. In particular, it is
whether a variable stores time or ticks.
- We now make complete and correct (we hope) the use of suitable fixnum
and mfixnum declarations, many of which had been missing or
incorrect.
- Both memoize and unmemoize are now safe for control-c and
unexpected errors.
- We no longer set ccl::*save-definitions* or
ccl::*fasl-save-definitions* to t. This may improve performance,
but it may require explicitly calling mf-note-arity, as is now done in
books/centaur/aig/bddify.lisp. However, this removes CCL-only behavior;
in particular, we removed dependence on #+Clozure in
books/centaur/aig/bddify.lisp for profiling count-branches-to.
- We use #+ccl instead of #+Clozure, for consistency with most of
the rest of ACL2.
- We no longer set ccl::*save-source-locations* or
ccl::*record-source-file* to t, as there is no clear advantage to
doing so, and in fact there is a comment near the end of source file
acl2.lisp suggesting that there could be slowdown from setting (at least)
the first of these variables to t.
- We slightly modified internal-real-time to improve its
performance (see comments there).
- We fixed a performance bug in function addr-for (parenthesis error
was needlessly putting us in the ``large-case'').
- Fixed a typo: declaim of fixnum type for *initial-max-memoize-fns*
had instead been for nonexistent variable
*initial-2max-memoize-fns*.
- In memoize-fn, we removed support for :condition to be a
function symbol, which was at best confused.
- The table *never-memoize-ht* is now populated mostly automatically,
by initialize-never-memoize-ht.
- Slight optimization: the form (update-attached-fn-called
,*attached-fn-temp*), which had been in the definition of memoize-fn
but now is in memoize-fn-inner-body, is conditioned on
,*attached-fn-temp*.
