merge_irept: insert once and then const_cast to edit in place #4155

tautschnig · 2019-02-11T13:25:49Z

This avoids multiple lookups in the hash set, each of which requires a number of
operator== and hash() calls. The use of const_cast is acceptable, because we do
not actually change the object in a way that would affect ordering (objects will
continue to have the same hash value and still compare equal).

We furthermore ensure that operator== can use pointer equality when submitting
an already-shared irept to merge_irept. On SV-COMP/ReachSafety-ECA this reduces
the number of recursive operator== invocations from 5,814,764,546 (generated by
4,241,423,614 invocations) to 2,232,563,047 (generated from 4,326,016,698
invocations). That is, despite ~100M additional invocations (because the
performance improvement permits more symbolic execution runs) around 3.6B
recursive calls are avoided.

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.

smowton · 2019-02-11T13:51:44Z

src/util/merge_irep.cpp

  irep_storet::const_iterator entry=irep_store.find(irep);
  if(entry!=irep_store.end())
    return *entry;

+  bool same_irep = true;
  irept new_irep(irep.id());


How about starting with new_irep = irep (cheap refcounted copy), then selectively overwriting sub / named_sub? That way we only make a CoW break if merged does some merging and we actually update either sub or named_sub, whereas at present we'll build and then discard new_irep in that case.

Alternatively if you take my suggestion above then new_irep will just be irept &new_irep = *irep_store.insert(irep).first

I've got a follow-up change that will avoid discarding new_irep (well, in fact it will never build new_irep in the first place), but I wanted to benchmark these independently (as they optimise on different aspects, this here reduces the number of operator== calls, while the other will reduce the number of detach calls). Let's look into this on that other PR (yet to come).

smowton · 2019-02-11T13:53:26Z

src/util/merge_irep.cpp

@@ -145,18 +145,26 @@ void merge_irept::operator()(irept &irep)

 const irept &merge_irept::merged(const irept &irep)
 {
+  if(irep.get_sub().empty() && irep.get_named_sub().empty())


How about we start with an unconditional insert regardless of get_sub() or get_named_sub(), then alter it in place if any of the child merges do anything?

Let's assume irept A was previously inserted into the store. Now we have an irept B. If the unconditional insert of B is unsuccessful (because A==B), then each of the child merges would result in a detach, meaning that sharing between A and its stored copy is now broken. At the end, B would now be the shared copy of the store, and so it would continue every time you call this method. We would actually not have any sharing at all anymore.

Huh? If the insert is unsuccessful then only read-only operations are performed (operator== and hash), after which a reference to A is returned. You then return that, like the find call currently immediately below the new insert

Ah, sorry, I didn't get that you still wanted to return immediately. Let me try to see how that would perform.

Constness of the inserted element gets in the way I'm afraid: the store is a std::unordered_set, so elements once inserted cannot be modified in place.

Personally I'd say this is an ideal case for use of const_cast, since we're making changes that don't affect its ==-ness or its hash code. Also it's surely worth it to avoid the find then insert that we get for ireps not currently in the store?

I've got an implementation that does what you proposed, but this now highlights how broken our use of parametert is: sometimes two parametert with different ID_C_identifier should be considered distinct (when using them to assign to arguments), while otherwise we would want them to be the same (while type checking declarations vs definitions). I'll see what I can do...

Although the parametert business should still be cleaned up, it was actually me being stupid. I should have benchmarking results in a few hours.

smowton · 2019-02-11T13:54:58Z

Also is the description accurate? It looks like the number of stores will be the same, but we'll save a find in the case where the irep has no sub or named-sub?

tautschnig · 2019-02-11T13:58:30Z

Re description: indeed, it should say irept::dt instead of just irept.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: de358fe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100454419
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

This avoids multiple lookups in the hash set, each of which requires a number of operator== and hash() calls. The use of const_cast is acceptable, because we do not actually change the object in a way that would affect ordering (objects will continue to have the same hash value and still compare equal). We furthermore ensure that operator== can use pointer equality when submitting an already-shared irept to merge_irept. On SV-COMP/ReachSafety-ECA this reduces the number of recursive operator== invocations from 5,814,764,546 (generated by 4,241,423,614 invocations) to 2,232,563,047 (generated from 4,326,016,698 invocations). That is, despite ~100M additional invocations (because the performance improvement permits more symbolic execution runs) around 3.6B recursive calls are avoided.

tautschnig · 2019-02-12T12:57:20Z

@smowton Done, finally ready for re-review. The results are quite a bit better!

smowton · 2019-02-12T13:42:20Z

Update the description with them?

tautschnig · 2019-02-12T13:45:09Z

Update the description with them?

That was done already - my initial attempt saved 1.1B calls, now we're saving 3.6B calls.

smowton

Nice :D

allredj

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

tautschnig added the Performance Optimisations label Feb 11, 2019

tautschnig requested review from kroening, peterschrammel, pkesseli and smowton as code owners February 11, 2019 13:25

smowton reviewed Feb 11, 2019

View reviewed changes

tautschnig force-pushed the merge-irept-skip-same branch from de358fe to d394c49 Compare February 11, 2019 14:42

allredj reviewed Feb 11, 2019

View reviewed changes

tautschnig force-pushed the merge-irept-skip-same branch 2 times, most recently from 6dbc155 to fd7c02d Compare February 12, 2019 12:52

tautschnig force-pushed the merge-irept-skip-same branch from fd7c02d to 3b95d0a Compare February 12, 2019 12:53

tautschnig changed the title ~~merge_irept: do not store fresh irept unless necessary~~ merge_irept: insert once and then const_cast to edit in place Feb 12, 2019

smowton approved these changes Feb 12, 2019

View reviewed changes

tautschnig self-assigned this Feb 12, 2019

tautschnig merged commit 2f1514e into diffblue:develop Feb 12, 2019

tautschnig deleted the merge-irept-skip-same branch February 12, 2019 16:37

allredj reviewed Feb 12, 2019

View reviewed changes

merge_irept: insert once and then const_cast to edit in place #4155

merge_irept: insert once and then const_cast to edit in place #4155

Uh oh!

Conversation

tautschnig commented Feb 11, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Feb 11, 2019

Uh oh!

tautschnig commented Feb 11, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 12, 2019

Uh oh!

smowton commented Feb 12, 2019

Uh oh!

tautschnig commented Feb 12, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented Feb 11, 2019 •

edited

Loading