memory-mgmt-logic

(in-package "ACL2")

(defsection maybe-wash-memory
  :parents (hons)
  :short "Conditionally trigger a @(see hons-wash) and also @(see
  clear-memoize-tables) to reclaim memory.  (CCL only; requires a
  trust tag)"
  :long "<p>@(call maybe-wash-memory) will clear out unused honses and throw
away all currently memoized results, but only if fewer than @('n') bytes of
memory are currently free.  If more than @('n') bytes are free, it does
nothing.</p>

<p>The general idea here is that garbage collection is slow, so you only want
to do it if you are starting to run out of memory.  At the same time, garbage
collection is cheaper if you can do it "in between" computations that are
creating a lot of garbage, where there are fewer live objects.  Moreover, if
you still have a lot of memory still available, then you may prefer to keep
currently memoized results so that you aren't repeating work.</p>

<p>You can use @('maybe-wash-memory') in between computations to trigger
garbage collections in an opportunistic way: if there's ample memory still
available, no GC will be triggered, but if memory is getting scarce, then it's
time to trigger an expensive collection, wiping out the memo tables and
cleaning up honses in the process.</p>

<p>Here's a basic example:</p>

@({
 (include-book "centaur/misc/memory-mgmt" :dir :system) ;; adds ttag
 (value-triple (set-max-mem (* 8 (expt 2 30))))           ;; 8 GB
 ... some memory intensive stuff ...
 (value-triple (maybe-wash-memory (* 3 (expt 2 30))))
 ... more memory intensive stuff ...
 (value-triple (maybe-wash-memory (* 3 (expt 2 30))))
 ... etc ...
})

<p>If the optional @('clear') argument is @('t'), honses will be cleared using
@(see hons-clear) instead of @(see hons-wash).  (This is generally ill
advised.)</p>

<p>This can be a good way to clean up memory in between @(see
gl::def-gl-param-thm) cases, and in other situations.</p>")

(add-macro-alias maybe-wash-memory maybe-wash-memory-fn)

(defxdoc set-max-mem
  :parents (hons-and-memoization)
  :short "An enhanced memory management scheme. (CCL only; requires
  a trust tag)"
  :long "<p>Typical usage:</p>

@({
 (include-book "centaur/misc/memory-mgmt" :dir :system) ;; adds ttag
 (value-triple (set-max-mem (* 4 (expt 2 30))))           ;; 4 GB
})

<p>Logically @(call set-max-mem) just returns @('nil').</p>

<p>Under the hood, loading the @('centaur/misc/memory-mgmt') book adds some
special garbage collection hooks into CCL, and @('set-max-mem') influences the
behavior of these hooks.</p>

<p>Roughly speaking, @(call set-max-mem) means: <b>try</b> to use no more than
@('n') bytes of <b>heap</b> memory.  You should think of this as a soft cap.
Generally the limit will grow by increments of 1 GB as you start to run out of
memory.</p>

<p>Note that this only influences the heap memory.  To avoid swapping death,
you should typically pick an @('n') that leaves space for the stacks and other
processes on your system.  For instance, if your machine has only 8 GB of
physical memory, you may wish to reserve no more than about 6 GB for the
heap.</p>


<h3>Interaction with @(see build::cert.pl)</h3>

<p>The @(see build::cert.pl) build system scans for calls of @('set-max-mem')
and uses them to infer how much memory a book will need.  This information may
be useful for scheduling jobs when carrying out distributed builds on a
cluster.</p>

<p>Note that this parsing is done by a simple Perl script, so you can't just
use an arbitrary Lisp expression here.  Explicitly supported expressions
are:</p>

<ul>
 <li>@('(* n (expt 2 30))')</li>
 <li>@('(expt 2 n)')</li>
</ul>


<h3>Using @('set-max-mem') in Pure ACL2 Books</h3>

<p>To make it possible to embed calls of @(see set-max-mem) into ordinary,
trust-tag free ACL2 code, the logical definition of @('set-max-mem') is found
in the book:</p>

@({
   (include-book "centaur/misc/memory-mgmt-logic" :dir :system)
})

<p>Note that if you load only this @('-logic') book, without also loading the
raw book, then @('set-max-mem') will <b>do nothing</b> except print a message
saying it is doing nothing.</p>")

(add-macro-alias last-chance-wash-memory
  last-chance-wash-memory-fn)