Use the sharing map for the renaming level maps #4505

danpoe · 2019-04-09T15:59:17Z

Use the sharing map for the renaming level maps current_names in symex_renaming_levelt. The code in this PR has a few issues which I'll fix once we've decided whether to merge it.

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.

danpoe · 2019-04-09T16:02:07Z

Here are some results for the runtime of symex only, with --unwind 1, on several methods from Apache Tika on which symex takes between 5 and 15 sec

Overall with sharing it's 3% faster.

danpoe · 2019-04-09T16:02:39Z

@smowton, @romainbrenguier Would you be able to try this out on your benchmarks too?

tautschnig

Comments (including one blocking one) below; I've started performance experiments, will report on their results later on today.

tautschnig · 2019-04-10T06:02:14Z

src/goto-symex/auto_objects.cpp

-        if(
-          state.get_level2().current_names.find(ssa_expr.get_identifier()) ==
-          state.get_level2().current_names.end())
+        if(!state.get_level2().current_names.has_key(ssa_expr.get_identifier()))


~~Formatting looks messed up?~~ (edit: just a GitHub artifact)

tautschnig · 2019-04-10T06:03:54Z

src/goto-symex/goto_state.cpp

+  {
+    std::pair<ssa_exprt, unsigned> copy = r_opt->get();
+    copy.second = n;
+    level2.current_names.replace(l1_identifier, copy);


std::move(copy)

tautschnig · 2019-04-10T06:04:56Z

src/goto-symex/goto_symex_state.cpp

@@ -776,16 +776,20 @@ ssa_exprt goto_symex_statet::add_object(
  const irep_idt l0_name = ssa.get_identifier();
  const std::size_t l1_index = index_generator(l0_name);

-  // save old L1 name, if any


I'm not sure I appreciate that this comment has been removed.

Put back in

tautschnig · 2019-04-10T06:07:53Z

src/goto-symex/goto_symex_state.h

  {
-    level2.current_names.erase(it);
+    level2.current_names.erase(l1_identifier);
  }


I think this method should either be removed or else be used from drop_l1_name.

The other version is now using erase_if_exists() as suggested by @smowton

tautschnig · 2019-04-10T06:15:10Z

src/util/ssa_expr.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 class ssa_exprt:public symbol_exprt
 {
 public:
+  ssa_exprt() : symbol_exprt("", typet()) {}


This is pretty much a show stopper: why is this needed? Presumably a side effect of how objects are created in a sharing map, but can the sharing map please be fixed instead?

Maybe somewhere between @danpoe and @smowton: can you look into this and see whether we can get away without it?

Sure, I'll take a look

I was meaning to fix this once we have decided whether to merge this PR. Currently the sharing map creates a dummy object (using the default constructor of the stored value type) when for a delta_view_itemt the key is only in one of the maps. We can probably use an optionalt instead.

#4612 @danpoe

#4612 is merged.

tautschnig · 2019-04-10T20:03:52Z

The results for my recent favourite ReachSafety-ECA are: 160 points scored with this patch, 156 points without this patch. Symex steps per second increase from 2978.24 to 2991.21. So that's overall an improvement, albeit not a groundbreaking one.

romainbrenguier · 2019-04-16T17:14:07Z

On my benchmarks the total time went from 106.85 to 99.31

tautschnig · 2019-04-17T08:02:12Z

@danpoe @romainbrenguier Could you rerun your benchmarking now that field-sensitivity is merged? It's possible that the maps now actually get larger, and thus such changes may be more impactful.

smowton · 2019-04-17T09:34:21Z

src/goto-symex/goto_symex_state.h

  }

  /// Drops an L1 name from the local L2 map
  void drop_l1_name(const irep_idt &l1_identifier)
  {
-    level2.current_names.erase(l1_identifier);
+    if(level2.current_names.has_key(l1_identifier))


Now have erase_if_exists

smowton · 2019-04-17T09:35:29Z

src/goto-symex/renaming_level.cpp

-  auto it = current_names.begin();
-  for(const auto &pair : other)
+  current_namest::delta_viewt delta_view;
+  other.get_delta_view(current_names, delta_view, false);


delta_view overestimates the keys that may differ, right? If so couldn't the replace below replace for no good reason?

smowton

Tested this with a long-running Webgoat analysis -- found before the changes it took ~200s, afterwards ~160s.

danpoe · 2019-04-23T15:49:22Z

Here are some results for the runtime of symex only, with --unwind 1, on several methods from Apache Tika, after field-sensitivity was merged:

Overall with sharing it's 3% faster.

Btw, I've also compared old symex vs. field sensitive symex and overall field-sensitive symex was 6.3X faster on the benchmarks.

romainbrenguier · 2019-04-29T11:12:55Z

For my benchmarks it didn't seem to have a positive effect:

Total time went from 73.86s to 77.218s

smowton · 2019-04-30T16:34:02Z

Now that field-sensitivity is in this makes even more of a difference, mostly in skipping the large number of new keys in the renaming map via a sparse delta_viewt. I suspect the benchmarks above aren't really seeing the benefit as they're micro-benchmarks, whereas these effects only really show up once the renaming map gets large.

danpoe · 2019-05-03T09:58:07Z

@smowton Would you be able to re-run the benchmarks on the Webgoat analysis now that field-sensitivity has been merged?

smowton · 2019-05-03T17:07:09Z

Benchmark results for a long-running Webgoat analysis:

Develop: 77s
#4464: 57s
#4464 + #4505: 26s

danpoe · 2019-05-07T09:44:59Z

Thanks everyone for the benchmarking and comments. So in summary on @romainbrenguier's benchmarks it's about 4% slower, on @smowton's benchmark it's about twice as fast, and on my benchmarks it's about 3% faster. So I'd be inclined to merge it once comments have been addressed and CI passes.

smowton · 2019-05-07T16:23:06Z

CI failure is caused by the rebase, as other_m is now a pointer

danpoe added Performance Optimisations do not merge Needs data This PR claims improvements that require further data to substantiate the claims. labels Apr 9, 2019

danpoe requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners April 9, 2019 15:59

tautschnig reviewed Apr 10, 2019

View reviewed changes

tautschnig assigned smowton, danpoe and romainbrenguier Apr 10, 2019

peterschrammel unassigned smowton and romainbrenguier Apr 15, 2019

smowton reviewed Apr 17, 2019

View reviewed changes

smowton approved these changes Apr 17, 2019

View reviewed changes

danpoe assigned romainbrenguier Apr 23, 2019

danpoe force-pushed the feature/use-sharing-map-for-renaming branch from 9edc38c to ba5b977 Compare April 29, 2019 09:44

smowton mentioned this pull request May 3, 2019

Use sharing_mapt to store propagation map #4464

Merged

4 tasks

danpoe force-pushed the feature/use-sharing-map-for-renaming branch from ba5b977 to f37b254 Compare May 7, 2019 16:09

danpoe force-pushed the feature/use-sharing-map-for-renaming branch from f37b254 to c608c50 Compare May 7, 2019 16:30

Use the sharing map for the renaming level maps

60dbcd9

danpoe force-pushed the feature/use-sharing-map-for-renaming branch from c608c50 to 60dbcd9 Compare May 7, 2019 16:35

danpoe merged commit 9dbac2e into diffblue:develop May 7, 2019

danpoe deleted the feature/use-sharing-map-for-renaming branch June 2, 2020 17:08

Use the sharing map for the renaming level maps #4505

Use the sharing map for the renaming level maps #4505

Conversation

danpoe commented Apr 9, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

danpoe commented Apr 9, 2019

Uh oh!

danpoe commented Apr 9, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

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

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!

danpoe May 3, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

tautschnig commented Apr 10, 2019

Uh oh!

romainbrenguier commented Apr 16, 2019

Uh oh!

tautschnig commented Apr 17, 2019

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 left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe commented Apr 23, 2019

Uh oh!

romainbrenguier commented Apr 29, 2019

Uh oh!

smowton commented Apr 30, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

danpoe commented May 3, 2019

Uh oh!

smowton commented May 3, 2019

Uh oh!

danpoe commented May 7, 2019

Uh oh!

smowton commented May 7, 2019

Uh oh!

Uh oh!

danpoe commented Apr 9, 2019 •

edited

Loading

tautschnig Apr 10, 2019 •

edited

Loading

danpoe May 3, 2019 •

edited

Loading

smowton commented Apr 30, 2019 •

edited

Loading