irept: use single map for all named sub-nodes #3470

kroening · 2018-11-26T23:06:56Z

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

This is probably a very good idea, with two requests:

The version number of goto binaries needs to be incremented.
We need to do benchmarking, most likely this is a major improvement (it's just the operator== that's of concern).

smowton · 2018-11-27T10:00:16Z

The hash-container change suggests we'll always include comments in a particular irep's hashcode? In that case surely unordered_map will break as hash-code equality and operator== will disagree?

kroening · 2018-11-27T11:39:27Z

@smowton Was still getting there; they now agree.

kroening · 2018-11-27T11:50:58Z

One more BTW @tautschnig : The goto-binary format is tolerant of this change (forwards and backwards), i.e., no need to tweak the version number for this.

src/util/irep_serialization.cpp

@kroening

Thanks @kroening for helping me understand!

tautschnig · 2018-11-27T13:16:44Z

I will take care of benchmarking once CI passes.

allredj

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

tautschnig

With this change there is a desirable reduction in memory consumption, but also approximately 20% slowdown across all benchmarks. This additional time is spent in irept::number_of_non_comments. The two dominating causes of invoking this are 1) computing a hash - to be optimised away via HASH_CODE, and 2) sorting operands in expression simplification - see #1997 for removing it.

Overall I think we should work to enable this optimisation, but we have more work to do to avoid a performance regression.

kroening · 2018-12-05T12:56:04Z

@tautschnig Many thanks -- I've just done a tweak that should reduce the cost of counting for the case of hashing. May I ask you to do another run?

tautschnig · 2018-12-05T13:09:33Z

May I ask you to do another run?

Running.

tautschnig · 2018-12-05T14:01:32Z

That's the quantile plot for ReachSafety-BitVectors - it seems the new version is back en par with develop.

tautschnig · 2018-12-05T14:05:32Z

src/goto-programs/show_goto_functions_json.cpp

 {
  json_arrayt json_functions;
-  const json_irept no_comments_irep_converter(false);
+  const json_irept no_comments_irep_converter;


Does this still do what the name promises? If so, how?

removed these changes

src/util/irep.cpp

tautschnig · 2018-12-05T14:13:31Z

src/util/irep.cpp

+      // must be the same
+      INVARIANT(it1 != get_named_sub().end(), "not at end of get_named_sub()");
+      INVARIANT(
+        it2 != i.get_named_sub().end(), "not at end of i.get_named_sub()");


This should basically be the same code as irept::operator== but does extra checks and just overall looks a bit different. Maybe we can avoid this?

could use compare() for both, but seems to be an unrelated change

src/util/json_irep.cpp

tautschnig · 2018-12-05T14:18:06Z

src/util/json_irep.cpp

 #include <algorithm>

 /// To convert to JSON from an irep structure by recursively generating JSON
 /// for the different sub trees.


This comment should actually go with the class, not with the constructor.

src/util/json_irep.h

src/util/xml_irep.cpp

unit/util/irep.cpp

allredj

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

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 6024861).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93968598
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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: df4dee0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93969059
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: 31ab10a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93970956

allredj

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

allredj

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

tautschnig · 2018-12-20T09:48:42Z

I am attaching the results for develop vs this branch on SV-COMP's ReachSafety-ECA category, which is the category where we spend the most time actually running symbolic execution (before handing the formula to the SAT solver). The difference is very small, but overall in favour of the proposed change. Some tasks are slower, some finish quicker. The total memory consumption is lower, as expected.

kroening added enhancement work in progress labels Nov 26, 2018

kroening requested review from chrisr-diffblue, peterschrammel, pkesseli, smowton and tautschnig as code owners November 26, 2018 23:06

tautschnig previously requested changes Nov 26, 2018

View reviewed changes

kroening force-pushed the irep-with-single-map branch from 980ca13 to ba355e2 Compare November 26, 2018 23:59

kroening force-pushed the irep-with-single-map branch from ba355e2 to 95d4cac Compare November 27, 2018 11:38

kroening force-pushed the irep-with-single-map branch 2 times, most recently from ecb76e2 to cfcc3ef Compare November 27, 2018 11:46

tautschnig reviewed Nov 27, 2018

View reviewed changes

src/util/irep_serialization.cpp Show resolved Hide resolved

tautschnig added the Needs data This PR claims improvements that require further data to substantiate the claims. label Nov 27, 2018

kroening force-pushed the irep-with-single-map branch 5 times, most recently from 2d0273b to ced9234 Compare November 29, 2018 10:43

allredj reviewed Nov 29, 2018

View reviewed changes

tautschnig self-assigned this Dec 1, 2018

tautschnig requested changes Dec 5, 2018

View reviewed changes

kroening force-pushed the irep-with-single-map branch from ced9234 to d202f7c Compare December 5, 2018 12:55

tautschnig reviewed Dec 5, 2018

View reviewed changes

allredj reviewed Dec 5, 2018

View reviewed changes

kroening force-pushed the irep-with-single-map branch 2 times, most recently from 6024861 to df4dee0 Compare December 7, 2018 08:24

kroening removed Needs data This PR claims improvements that require further data to substantiate the claims. work in progress labels Dec 7, 2018

kroening force-pushed the irep-with-single-map branch from df4dee0 to 31ab10a Compare December 7, 2018 08:51

allredj reviewed Dec 7, 2018

View reviewed changes

tautschnig force-pushed the irep-with-single-map branch from 31ab10a to 6933585 Compare December 19, 2018 10:04

allredj reviewed Dec 19, 2018

View reviewed changes

irept: use single map for all named sub-nodes

48c40db

tautschnig force-pushed the irep-with-single-map branch from 6933585 to 48c40db Compare December 19, 2018 22:39

allredj reviewed Dec 19, 2018

View reviewed changes

tautschnig approved these changes Dec 20, 2018

View reviewed changes

tautschnig merged commit 0ebc228 into develop Dec 20, 2018

tautschnig deleted the irep-with-single-map branch December 20, 2018 09:50

irept: use single map for all named sub-nodes #3470

irept: use single map for all named sub-nodes #3470

Uh oh!

Conversation

kroening commented Nov 26, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Nov 27, 2018

Uh oh!

kroening commented Nov 27, 2018

Uh oh!

kroening commented Nov 27, 2018

Uh oh!

Uh oh!

tautschnig commented Nov 27, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Dec 5, 2018

Uh oh!

tautschnig commented Dec 5, 2018

Uh oh!

tautschnig commented Dec 5, 2018

Uh oh!

tautschnig Dec 5, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Dec 7, 2018

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

tautschnig Dec 5, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Dec 7, 2018

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Dec 5, 2018

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

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!

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 Dec 20, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants