Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Collect performance statistics for liquid-fixpoint #539

Open
facundominguez opened this issue Apr 7, 2022 · 4 comments
Open

Collect performance statistics for liquid-fixpoint #539

facundominguez opened this issue Apr 7, 2022 · 4 comments

Comments

@facundominguez
Copy link
Collaborator

facundominguez commented Apr 7, 2022

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).
@Fizzixnerd
Copy link
Contributor

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

@Fizzixnerd
Copy link
Contributor

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
Copy link
Contributor

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.

@facundominguez
Copy link
Collaborator Author

  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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants