Skip to content

Optimize loop of phi_function #3522

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 8 commits into from
Dec 6, 2018
Merged

Optimize loop of phi_function #3522

merged 8 commits into from
Dec 6, 2018

Conversation

romainbrenguier
Copy link
Contributor

This function was performing unnecessary lookups (even after ranget), we avoid this by introducing a function which goes through both maps and use the fact that they are ordered.

I tested this optimization on 73 methods from tika which where taking between 600ms and 30s with --show-vcc and --verbosity 0, the total time was improved by 20% (from 229s to 185s). Here is a comparison of the execution times
perf_out

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • 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.
  • [na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig
tautschnig requested changes Dec 3, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

The performance improvement is of course desirable, but could the changes please be done in a way so that the diff (when switching on skip-whitespace) is readable?

src/goto-symex/symex_goto.cpp Outdated
/// second one then j is 0, and when the first map has no entry for k then i = 0
static void for_each2(
std::map<irep_idt, std::pair<ssa_exprt, unsigned>> first_map,
std::map<irep_idt, std::pair<ssa_exprt, unsigned>> second_map,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why are these maps passed by value?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes it's a mistake

@romainbrenguier romainbrenguier force-pushed the optimize/phi_function_loop branch from 171afa9 to bafafeb Compare December 3, 2018 21:57
@romainbrenguier
Copy link
Contributor Author

I was passing the maps by copy instead of reference, when correcting that the performance improvement is now of 33%
perf_out

@romainbrenguier romainbrenguier force-pushed the optimize/phi_function_loop branch 6 times, most recently from 9c3ea08 to c796942 Compare December 5, 2018 14:12
@romainbrenguier
Copy link
Contributor Author

@tautschnig this is ready for re-review

allredj
allredj reviewed Dec 5, 2018
View reviewed changes
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: c796942).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93674773

tautschnig
tautschnig approved these changes Dec 5, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

A couple of suggestions left, I think we should be good to go once these are in.

src/goto-symex/symex_goto.cpp Outdated
{
diff_guard=goto_state.guard;
if(all_current_names_range.empty())
return;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Ok, but then you don't need the declaration above either. Could you make the first definition below also be the declaration?

src/goto-symex/symex_goto.cpp Outdated
symex_config.simplify_opt,
target,
l1_identifier,
ssa);
Copy link
Collaborator

Choose a reason for hiding this comment

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

If we pass in ssa anyway, then l1_identifier should be computed from that in the body of merge_names.

src/goto-symex/symex_goto.cpp Outdated
// once the thread is executed)
if(
!ssa.get_level_0().empty() &&
ssa.get_level_0() != std::to_string(dest_state.source.thread_nr))
Copy link
Collaborator

Choose a reason for hiding this comment

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

Would you mind adding an extra commit that avoids this duplicate call to get_level_0()?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

done

@kroening
Copy link
Member

kroening commented Dec 5, 2018

The clang-format commit should be merged into the relevant earlier commits.

@romainbrenguier
Return early if nothing to do in phi_function
1c1ab39
@romainbrenguier
Inline do_simplify
cb52281 
This will allow to more easily extract the code in the loop into a new
function.
@romainbrenguier
Extract function from the loop in phi_function
fd5f0d5 
This simplifies phi_function which was too long.
@romainbrenguier
Document merge_names function
cb35222
@romainbrenguier
Compute goto_count and dest_count before merge_names
7f4aded 
Since these are used several times in the function we can avoid some
lookups by pre-computing it.
We make them parameters to allow later commits to give them without
lookup.
@romainbrenguier
Use a for_each2 function iterating over two maps
235310a 
Inside phi_function we can avoid a lot of lookups if we iterate over the
two maps at the same time, since they are ordered.
@romainbrenguier
Remove unused range
4880553
@romainbrenguier
Avoid duplicate get_level_0 call
bbec003
@romainbrenguier romainbrenguier force-pushed the optimize/phi_function_loop branch from c796942 to bbec003 Compare December 6, 2018 08:34
allredj
allredj reviewed Dec 6, 2018
View reviewed changes
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: bbec003).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93783524

@tautschnig tautschnig merged commit f56ce2e into diffblue:develop Dec 6, 2018
@romainbrenguier romainbrenguier deleted the optimize/phi_function_loop branch December 6, 2018 10:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

Assignees

@romainbrenguier romainbrenguier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@romainbrenguier @kroening @tautschnig @allredj