liquid-fixpoint
liquid-fixpoint copied to clipboard
Collect performance statistics for liquid-fixpoint
There are some statistics collected currently, and spread on different flags (--elimstats --solverstats --stats
).
There are a few things we could do to make them more useful:
- Have one flag to dump them all.
- Improve the output to give more context on what they mean.
- Add a few more stats:
- how much time is spent in elim, the interpreter ple, and the regular PLE.
- how much time is spent doing calls to the SMT solver on each algorithm (and how many calls).
I'd like to take a look at this issue.
I've added a --profile
flag so far, and used it to control the dumping of profiling stats. After a conversation with @facundominguez , I've decided that the way to go is to just do the most "obvious" thing and wrap calls to the ple and solver in a simple get time, execute action, get time, subtract two times and print, return action result
kind of workflow. This may not catch everything, since Haskell is of course lazy in the inner pure computations still, possibly. But it will at least let us know how much time is being spent talking to the SMT, so I have called this helper function profileIO
.
regarding having one flag to dump them all: note that --stats
actually doesn't run the solver, it only prints the stats. Therefore, a somewhat larger refactor may be required to achieve this goal; it might end up being easy, however.
- Add a few more stats:
- how much time is spent in elim, the interpreter ple, and the regular PLE.
- how much time is spent doing calls to the SMT solver on each algorithm (and how many calls).
I'm considering timestats to solve some of these.