[acl2/acl2] 5a5f7c: Change the cl-cache implementation to be a bit mor...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 5a5f7cf1ca026f9604ff84eecce887a2dc56b564
https://github.com/acl2/acl2/commit/5a5f7cf1ca026f9604ff84eecce887a2dc56b564
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2018-01-17 (Wed, 17 Jan 2018)

Changed paths:
M acl2-fns.lisp
M apply-prim.lisp
M apply-raw.lisp
M apply.lisp
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M books/system/tests/apply-timings.lisp
M doc.lisp

Log Message:
-----------
Change the cl-cache implementation to be a bit more efficient, and much more efficient for more than 3 lambdas actively being applied.

The first of the following items, quoting :doc note-8-1, is not new
(it was accomplished with a recent commit).

The following improvements have been made for evaluating calls of the
form (apply$ (lambda ...) ...).

* An optimization had failed to be fully in place, causing such calls
to run slowly. That optimization compiles and caches ``tame
compliant'' lambdas: lambda forms whose [guard]s are verified
by the [tau-system] and that are tame (see [apply$]). The
optimization had been used in the unadvertised use of ``The
Rubric'' prior to the release of ACL2 Version 8.0.
* The optimization above has been improved so that instead of three
cache lines, there is an efficient implementation using 1000
cache lines. That is probably many more than are needed, but
the large size is harmless. The additional cache lines
dramatically improve speed when more than three lambdas are
actively being applied; see [community-books] file
books/system/tests/apply-timings.lisp.
* ACL2 no longer causes an error when the cache is in an inconsistent
state; instead, the cache is suitably reset quietly.

I'm pretty happy with this implementation, which is quite efficient
using circular list structures. Even when only three cache lines are
needed, it is a bit faster; quoting comments in source file
apply-raw.lisp:

; The respective results using our 3-line cache (the one used below, and using
; CCL) were measured at:

; 0.91 seconds realtime, 0.91 seconds runtime
; 2.99 seconds realtime, 3.00 seconds runtime
; 5.73 seconds realtime, 5.73 seconds runtime

; The respective results using our current cache (as of mid-January, 2018,
; using CCL) were measured at:

; 0.69 seconds realtime, 0.69 seconds runtime
; 2.58 seconds realtime, 2.59 seconds runtime
; 4.48 seconds realtime, 4.48 seconds runtime

An additional comment:

; Note by the way that if we reduce 1000 cache lines to 5 cache lines, the
; times are essentially unchanged.

Also, updated tests in books/system/tests/apply-timings.lisp to
reflect the increased capacity.

[GitHub]

Branch: refs/heads/testing