liquid-fixpoint icon indicating copy to clipboard operation
liquid-fixpoint copied to clipboard

Collect performance statistics for liquid-fixpoint

Open facundominguez opened this issue 2 years ago • 4 comments

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:

  1. Have one flag to dump them all.
  2. Improve the output to give more context on what they mean.
  3. 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).

facundominguez avatar Apr 07 '22 22:04 facundominguez

I'd like to take a look at this issue.

Fizzixnerd avatar May 04 '22 17:05 Fizzixnerd

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.

Fizzixnerd avatar May 09 '22 16:05 Fizzixnerd

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.

Fizzixnerd avatar May 09 '22 16:05 Fizzixnerd

  1. 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.

facundominguez avatar Jul 26 '22 11:07 facundominguez