Skip to content

Use std::forward_list instead of std::map in irept by default #4731

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

Merged
merged 1 commit into from
Nov 14, 2020

Conversation

tautschnig
Copy link
Collaborator

This reduces the size of an irept by 5 pointers (i.e., 40 bytes on
64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can
perform 3819.81 symex_step calls per second, compared to 2752.28 calls
per second with the std::map configuration. The performance improvements
are spread across various irept-related operations.

This is a repeat of #4458 and re-introduces what #4729 just reverted. It must only be merged after #4724 is in.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig self-assigned this May 30, 2019
@tautschnig tautschnig changed the title Use std::forward_list instead of std::map in irept by default [depends-on: #4724] Use std::forward_list instead of std::map in irept by default May 31, 2019
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 4ea27a0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113878030

@tautschnig
Copy link
Collaborator Author

This would need a timeout limit increase for the CodeBuild job to pass.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 61b0bc3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114067829

@kroening kroening removed their assignment Jun 3, 2019
@smowton
Copy link
Contributor

smowton commented Aug 13, 2019

Shall we do this then?

@codecov
Copy link

codecov bot commented Nov 10, 2020

Codecov Report

Merging #4731 (235dde8) into develop (a503f5c) will increase coverage by 0.00%.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #4731   +/-   ##
========================================
  Coverage    69.31%   69.32%           
========================================
  Files         1241     1242    +1     
  Lines       100381   100418   +37     
========================================
+ Hits         69580    69615   +35     
- Misses       30801    30803    +2     
Flag Coverage Δ
cproversmt2 43.09% <ø> (+0.01%) ⬆️
regression 66.22% <ø> (+<0.01%) ⬆️
unit 32.26% <ø> (+0.02%) ⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/util/irep.cpp 97.41% <ø> (-0.03%) ⬇️
src/util/irep.h 95.38% <ø> (ø)
src/util/irep_hash_container.cpp 63.88% <ø> (ø)
src/util/irep_serialization.cpp 92.39% <ø> (ø)
src/util/lispirep.cpp 70.00% <ø> (+0.76%) ⬆️
src/util/merge_irep.cpp 33.33% <ø> (ø)
src/util/type.h 100.00% <ø> (ø)
.../strings/string_constraint_generator_constants.cpp 63.33% <0.00%> (-2.19%) ⬇️
... and 9 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update a503f5c...235dde8. Read the comment docs.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds reasonable.

@tautschnig
Copy link
Collaborator Author

@peterschrammel (or anyone else with direct access to CodeBuild logs): am I right to assume that the "cbmc" CodeBuild job just times out? I believe this is down to it running with -D_GLIBCXX_DEBUG, which makes the tests take 2 hours of wall clock time on my machine (compared to 400 seconds in a Release build).

@peterschrammel
Copy link
Member

Yes, it times out.

Screenshot 2020-11-12 at 10 47 47

@tautschnig
Copy link
Collaborator Author

Yes, it times out.

Screenshot 2020-11-12 at 10 47 47

Thank you @peterschrammel! How long does this build job take without the changes in this PR, i.e., on about any other PR? I am not too surprised that -D_GLIBCXX_DEBUG adds a lot of overhead here, but at the same time I don't want to go ahead and merge this PR just to make the job then fail on all other PRs as well (even when it's not longer marked "Required").

@peterschrammel
Copy link
Member

peterschrammel commented Nov 13, 2020

You should actually have access. Ping me if you forgot your credentials.

Screenshot 2020-11-13 at 10 03 15

This reduces the size of an irept by 5 pointers (i.e., 40 bytes on
64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can
perform 3819.81 symex_step calls per second, compared to 2752.28 calls
per second with the std::map configuration. The performance improvements
are spread across various `irept`-related operations.
@tautschnig tautschnig merged commit 57c5505 into diffblue:develop Nov 14, 2020
@tautschnig tautschnig deleted the forward-list branch November 14, 2020 02:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants