Optimization
How to optimize GL's symbolic simulations for faster or
larger-scale proofs.
- Using different modes to solve the problem. Some modes vastly
outperform others on particular problems and it is very easy to switch modes,
so this is often a good first thing to try when you run into a performance
problem.
- Decomposing difficult problems into easier subgoals. GL provides some
support for case-splitting hard proofs, and in some cases this kind of
decomposition can tremendously boost performance.
- Using other optimization techniques to make GL's symbolic execution
strategy more efficient.
The scope of theorems GL can handle is directly impacted by its symbolic
execution performance. It is actually quite easy to customize the way certain
terms are interpreted, and this can sometimes provide important speedups.
GL's symbolic interpreter operates much like a basic Lisp interpreter. To
symbolically interpret a function call, GL first eagerly interprets its
arguments to obtain symbolic objects for the actuals. Then GL symbolically
executes the function in one of three ways:
- As a special case, if the actuals evaluate to concrete objects, then GL may
be able to stop symbolically executing and just call the actual ACL2 function
on these arguments.
- For primitive ACL2 functions like +, consp, equal, and
for some defined functions like logand and ash where performance
is important, GL uses hand-written functions called symbolic
counterparts that can operate on symbolic objects. The advanced GL user
can write new custom-symbolic-counterparts to speed up symbolic
execution.
- Otherwise, GL looks up the definition of the function, and recursively
interprets its body in a new environment binding the formals to the symbolic
actuals. The way a function is written can impact its symbolic execution
performance; see redundant-recursion. It is easy to instruct GL to use
more efficient, preferred-definitions for particular functions.
GL symbolically executes functions strictly according to the ACL2 logic and
does not consider guards. An important consequence is that when mbe is
used, GL's interpreter follows the :logic definition instead of the
:exec definition, since it might be unsound to use the :exec version
of a definition without establishing the guard is met. Also, while GL can
symbolically simulate functions that take user-defined stobjs or even the ACL2
state, it does not operate on "real" ACL2::stobjs; instead, it
uses the logical definitions of the relevant stobj operations, which do not
provide the performance benefits of destructive operations. Non-executable
functions cannot be symbolically executed.
In the event that one is performing a very large decomposition proof (e.g.,
the theorem boothmul-decomp-is-boothmul-via-GL in book
centaur/esim/tutorial/boothmul.lisp, one should consider using book
centaur/esim/stv/stv-decomp-proofs.
Subtopics
- Term-level-reasoning
- GL's term-level proof support
- Def-gl-param-thm
- Prove a theorem using GL symbolic simulation with parametrized
case-splitting.
- Case-splitting
- Modes
- GL modes allow you to control major aspects of how GL carries out its
symbolic simulation and how it should solve Boolean formulas that arise during
proofs.
- Memory-management
- Preferred-definitions
- Custom-symbolic-counterparts
- Redundant-recursion
- Alternate-definitions
- Specifying alternative definitions to be used for symbolic
execution.
- Gl-param-thm
- Prove a theorem using GL symbolic simulation with parametrized
case-splitting, without storing the theorem.
