This directory illustrates performance benefits of using different
memory models for different tasks, and it shows that the use of
attachable stobjs has minimal impact on performance.

File mem-test.sh runs file mem-test.lsp in ACL2, to generate timing
output that was saved to file mem-test-output-8.6.txt.  Specifically,
that file was generated by running the following bash shell command on
a 2019 Intel-based Mac, where, acl2-8.6 invoked ACL2 Version 8.6 built
on CCL Version 1.12.2 (v1.12.2-32-g768239e4) DarwinX8664.

(export ACL2=acl2-8.6 ; ./mem-test.sh) > mem-test-output-8.6.txt

NOTE: mem-test.sh runs only on CCL (it uses ccl:heap-utilization and
parses its output).  It invokes file mem-test.lsp, which is NOT a
certifiable book.

In mem-test-output-8.6.txt, times are measured using ACL2's TIME$
utility, which reports both realtime and runtime, and these correspond
to the `Real` and `Run` columns respectively.  (It's a bit surprising
perhaps to find runtimes that exceed corresponding realtimes; perhaps
the Mac is taking advantage of more than one of its eight cores (with
hyperthreading) during the runs.)

The rows are based on doing 100,000 writes with the memory model
obtained after invoking the following ACL2 commands

;;; "symmetric"
(time$ (include-book "centaur/bigmems/bigmem/bigmem" :dir :system))

;;; "asymmetric"
(include-book "centaur/bigmems/bigmem-asymmetric/bigmem-asymmetric" :dir :system)

;;; "attached"
(include-book "centaur/bigmems/bigmem-asymmetric/bigmem-asymmetric" :dir :system)
(attach-stobj bigmem::mem bigmem-asymmetric::mem)
(time$ (include-book "centaur/bigmems/bigmem/bigmem" :dir :system))

Here are key observations supported by the successful use of those
commands and the generated output, mem-test-output-8.6.txt.

(1) One can use community book "centaur/bigmems/bigmem/bigmem" with
execution performed by either of two memory models, without
recertifying any books.

- "symmetric", the memory model defined in the "bigmem" book; or

- "attached", the memory model defined in the "bigmem-asymmetric"
  book.

(2) These two memory models have very different performance
characteristics, dependent on whether one is writing to "low" memory
or "high" memory.  The "low" and "high" writes are writes of byte 1
made to 100,000 random addresses from a range of 2^30 contiguous
addresses: these start at address 0 for "low" writes and at address
6*2^30 for "high" writes.

(3) There are only small performance penalties for using "attached"
instead of "asymmetric".  This is a small price to pay for allowing
the user to choose which memory model to use while using a single
book, "bigmem", for logical reasoning.  Allowing the user to choose a
memory model is significant because, as illustrated by the benchmark,
the best performing implementation of a stobj may depend on the
application.
