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

Improve timing, add Trace Event Format output #844

Merged
merged 33 commits into from
Oct 7, 2022
Merged

Improve timing, add Trace Event Format output #844

merged 33 commits into from
Oct 7, 2022

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Oct 3, 2022

Changes

  1. Copy CIL's Stats into Goblint as Timing and clean it up. Although as-is CIL barely uses Stats, there's a large number of usages in some CIL plugins, so I decided not to remove it from CIL itself, but just not use it in Goblint. This is similar to what has been done with tracing at some point: CIL still contains Trace, but Goblint contains an improved copy as Tracing.
  2. Rename time to wrap, so it's Timing.wrap instead of Stats.time now.
  3. Fix inconsistent intermediate timing printouts. Previously it was possible that the sum of subtree times of a tree was greater than that tree itself if that tree was still in the middle of timing and hadn't exited cleanly. Now printing also adds all the in-progress times.
  4. Add and improve measured data (all can be individually toggled):
    1. CPU time now includes CPU time of child processes (preprocessor executions). Previously preprocessing time couldn't be accounted for (even if it was wrapped in timing) because waiting for subprocesses exiting suspends Goblint and it doesn't do any work.
    2. Wall time is now measured as well. This rarely makes a difference (especially with preprocessing CPU time accounted for), but there is one case: when jobs is used to run multiple preprocessors in parallel, then wall time (which is what really matters for interactive usage) will be less than CPU time (which is more indicative of actual work done).
    3. Allocated memory is now measured as well. This is an idea I got from the landmarks library.
    4. Call counting existed in CIL already, but was disabled by default and we never used it, but I've recently found it to be quite valuable information. Otherwise if something takes 1s, then it might seem like something very slow is happening, but maybe it just gets executed 10000 times instead of the expected 100.
  5. Rename printstats to dbg.timing.enabled.
  6. Timing is generalized into a functor, which allows multiple simultaneous timing hierarchies. This allows to separately time how long we analyze what functions, for example.
  7. Add Trace Event Format (TEF) output (activated using dbg.timing.tef) for both our normal timings and function analysis times (aka my magic flamegraphs). Documentation for viewing this is included. In TEF additional metadata can be included for timed sections, e.g. parsing timings have their filename attached, so it's easy to find out which files take the longest to parse.

TODO

  • Update bench repo scripts with printstats rename.

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
@sim642 sim642 merged commit 7a083da into master Oct 7, 2022
@sim642 sim642 deleted the timing branch October 7, 2022 08:47
@sim642 sim642 added this to the v2.1.0 milestone Oct 7, 2022
sim642 added a commit to goblint/bench that referenced this pull request Oct 7, 2022
@sim642 sim642 added the hacktoberfest-accepted https://hacktoberfest.digitalocean.com/ label Oct 10, 2022
jerhard pushed a commit to goblint/bench that referenced this pull request Nov 23, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 25, 2022
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2023.

* Add automatic configuration tuning (goblint/analyzer#772).
* Add many library function specifications (goblint/analyzer#865, goblint/analyzer#868, goblint/analyzer#878, goblint/analyzer#884, goblint/analyzer#886).
* Reorganize library stubs (goblint/analyzer#814, goblint/analyzer#845).
* Add Trace Event Format output to timing (goblint/analyzer#844).
* Optimize domains for address and path sets (goblint/analyzer#803, goblint/analyzer#809).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug debugging feature hacktoberfest-accepted https://hacktoberfest.digitalocean.com/ performance time, memory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants