|
|
|---|
|
|
|
|---|
Ensure the integrity of memoization statistics even upon aborts
Example Forms:
(f-put-global 'protect-memoize-statistics t state) (assign protect-memoize-statistics t) ; same effect as above
By default, if calls of memoized functions are aborted, then statistics reported by memsum for those calls will often be incorrect. Since aborts are relatively rare, this seems a reasonable default, since avoiding such inaccuracy incurs some additional computation time. However, evaluation of either of the forms above will arrange that for functions memoized after such evaluation, the accuracy of the statistics will not be adversely affected by aborts (again, at the expense of some additional computation time).
Once again: evaluation of a form displayed above only affects behavior for future calls of memoize, not for functions already memoized at the time of that form's evaluation (unless the function is subsequently unmemoized and then once again memoized).
To revert to the default state in which performance is preferred to accuracy of memoization statistics after aborts, evaluate either of the following forms.
(f-put-global 'protect-memoize-statistics nil state) (assign protect-memoize-statistics nil) ; same effect as above
The following demo illustrates the effect of assigning to protect-memoize-statistics.
(defun foo (n) (declare (xargs :guard (natp n))) (progn$ (sleep n) n)) ; OPTIONALLY: (assign protect-memoize-statistics t) (memoize 'foo) (clear-memoize-statistics) ; for good measure (memsum) ; should have nothing to report (foo 1) (memsum) ; reports 1 call, 1 second ; Now: submit this and then abort with an interrupt it after about 3 seconds. (foo 15) ; See explanation below. (memsum)
If the ``OPTIONAL'' form above is omitted, we get the default behavior:
the statistics from memsum will show 2 calls of