Merge pull request #248 from ragerdl/master

3 CLs
Function memoization has been extensively updated, in particular fixing two soundness bugs.  Also, enhancements and bug fixes have been made for gc-verbose.

This is the first and probably largest step towards updating the
memoization code, which is all that remains in order for ACl2(h) to
become the default ACL2 build.  The major remaining step is for J to
review memoize-raw.lisp.

Quoting :doc note-7-0:

  Gc-verbose now takes an optional second argument, which is only
  relevant when the host Lisp is CCL, where that argument specifies
  verbosity for EGC.

  (ACL2(h) only) Fixed a soundness bug related to function memoization.
  For a proof of nil exploiting this bug in Version 6.5, see the
  comment about ``pons-addr-of-argument'' in Community Books file
  system/doc/acl2-doc.lisp, form (defxdoc note-7-0 ...).

  (ACL2(h) only) Fixed a soundness bug due to the fact that function
  never-memoize-fn returned nil in the logic but returned t in raw
  Lisp. For a proof of nil exploiting this bug in Version 6.5, see
  the comment about ``never-memoize-fn'' in Community Books file
  system/doc/acl2-doc.lisp, form (defxdoc note-7-0 ...).

  (GCL only) The utility [gc-verbose] was broken, but has been fixed.

  (CCL only) Control-d now quits ACL2 in raw Lisp just as it has done
  for a long time in the loop and, for ACL2(h), even in raw Lisp.

  Several changes been made to function memoization (see [memoize]).
  Here is a list of changes visible at the user level; for
  implementation details, see [note-7-0-memoize].

    * It is now legal to call [memoize] on functions with special raw-Lisp
      code (such as [len]) provided the value of the :inline keyword
      argument is nil.
    * Bug fix: Fixed bug that was making [memsum] attribute the count of
      making of hash tables to ``Heap bytes allocated'' instead of to
      ``Number of calls to mht.''
    * Memoize keyword :trace is no longer supported, as the [trace$]
      utility provides much more flexibility.
    * Bug fix: Fixed a bug in handling of the :commutative argument of
      [memoize] that could cause a hard Lisp error. For a book that
      exhibits this bug, see the comment about ``:commutative'' in
      Community Books file system/doc/acl2-doc.lisp, in the form
      (defxdoc note-7-0 ...).
    * When [memoize] is called with keyword argument :commutative having
      value t, the benefit of that argument can apply to rational
      number arguments even when not using static honsing. Moreover,
      now only one argument needs to be a rational or to be
      ``static'' according to the implementation (technically: to
      have an hl-staticp value).
    * Bug fix: Calls of [memoize] with keyword argument :commutative t were
      sometimes inappropriately treated as redundant
      [redundant-events]. This has been fixed. Here is a simple
      example of what formerly went wrong.

          (defn f (x y) (equal x y))
          (memoize 'f :commutative t)
          (unmemoize 'f)
          (memoize 'f :commutative t) ; was redundant, so did not memoize

    * (For those who memoized directly in raw Lisp) Memoize-fn now requires
      its first argument to be a defined (fboundp) function symbol.
      (It seemed odd and needlessly arcane to allow memoize-fn to
      define an undefined function.)
    * (For those who memoized directly in raw Lisp) Memoize-fn now causes
      an error when it fails.
    * Bug fix: It had been possible to lose a memoization setting of :aokp
      t when many functions were memoized. For an example, see the
      comment about ``rememoize-all'' in Community Books file
      system/doc/acl2-doc.lisp, in the form (defxdoc note-7-0 ...).
    * We eliminated undocumented utilities memoize-on and memoize-off,
      which were not used as far as we know.
    * When a memoized function call fails to satisfy the specified
      condition, that call is no longer counted as a ``hit'', at
      least by default. This can be changed with raw Lisp variable,
      *condition-nil-as-hit*.
    * The utility [memsum] had reported one more pons call and (CCL only)
      one more byte than was correct, and could perhaps report one
      call when there were actually zero. That has all been fixed.
    * Bug fix: Some sorting of results based on ``self'' time and ``other
      functions'' time had been wrong. (Technical remark: the problem
      wa that the implementation confused ``ticks'' with ``time''.)
      This has been fixed.
    * Statistics reporting (see [memsum]) often has a more uniform look. It
      is now done with a right margin of 79 instead of 70. For
      [memsum], thanks to a suggestion from Warren Hunt, the defun
      formerly printed to start each entry is now omitted, and after
      the name is printed at the start, a newline is printed before
      the ``hits'' or ``hits/calls'' information is printed. A
      related change: when *report-hits* and *report-calls* are both
      nil, ``calls'' is no longer printed. Other cosmetic changes
      were also made to [memsum] output.
    * For ACL2(hp), we changed the obervations printed about memoization
      when executing [set-waterfall-parallelism] --- for the better,
      we think.
    * On Mac OS (Darwin), the physical memory is now accurately computed
      (using shell command ``sysctl hw.memsize'', which works in some
      versions of Mac OS, maybe all recent ones; tested on 10.6 and
      10.7). Before, the physical memmory value had been assumed to
      be 2^32 bytes. The physical memory value is used in CCL for
      triggering garbage collections. (Technical remark: this is
      implemented in function start-sol-gc.)
    * Bug fix: in the pons summary, misses had been reported instead of
      hits on the ``hits/calls'' line.
    * Fixed [memsum] so that package names are printed with the symbols.
      Also, printing is done with respect to the current package, not
      the "ACL2" package.

Quoting :doc note-7-0-memoize (a new topic), which is about
lower-level changes:

  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 defintions, 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*.
Brought doc.lisp up-to-date with books/system/doc/acl2-doc.lisp.
Changed (loop for i integer ...) to (loop for i of-type integer ...); CCL was OK with the former, but not LispWorks.