Use sharing_mapt as container in value_sett #4463

tautschnig · 2019-03-30T14:52:44Z

goto-symex copies a state, which contains a value set, at each branching
point. The paths originating at that branch point typically share most
of the points-to information. Thus the copy is unnecessarily expensive,
and so is the merge at the next join point, which will also result in
one of the value sets to be destroyed. With sharing_mapt, the copy has
constant cost, merging can make use of the delta view, and the cost of
destruction only depends on the size of the delta.

Includes the cleanup-commit from #4462.

Performance evaluation to be done.

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.
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.

allredj

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

tautschnig · 2019-03-30T20:56:45Z

Some stats for SV-COMP's ReachSafety-ECA (which barely uses pointers, i.e., the value set would mostly be near-empty):

goto_statet::goto_statet(goto_symex_statet const&): develop: 1423.62 seconds; this branch: 459.92 seconds
Removing entries from the goto_state list: develop: 587.84 seconds; this branch: 246.81 seconds
value_sett::make_union: develop: 645.59 seconds; this branch: 223.34 seconds
value_sett::assign: develop: 306.79 seconds; this branch: 415.09 seconds

So adding new values to the value set has become more expensive (which is not unexpected), but merging and cloning is a lot cheaper (as intended). @romainbrenguier @smowton would you be able to contribute some benchmarking on Java code, which makes a lot more use of value sets?

martin-cs · 2019-04-01T06:58:35Z

src/pointer-analysis/value_set.h

@@ -297,11 +295,7 @@ class value_sett
  ///
  /// The components of the ID are thus duplicated in the `valuest` key and in
  /// `entryt` fields.
-  #ifdef USE_DSTRING


Are we reaching the point of saying that USE_DSTRING should always be on?

Well, we do still build with USE_DSTRING disabled, but I don't think the regression tests even pass. Though this change might be a step towards making that more likely, as it makes the code more uniform.

Remove value_sett::idt [blocks: #4463]

allredj

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

danpoe

LGTM

danpoe · 2019-04-01T10:43:35Z

src/pointer-analysis/value_set.cpp

+  {
+    entryt replacement = *existing_entry;
+    if(add_to_sets)
+      make_union(replacement.object_map, new_values);


We could check the return value of make_union() and only do the replacement when the object map has changed.

danpoe · 2019-04-01T10:53:53Z

src/pointer-analysis/value_set.cpp

+    if(add_to_sets)
+      make_union(replacement.object_map, new_values);
+    else
+      replacement.object_map = new_values;


We could check whether new_values.read() != existing_entry->object_map.read() before doing the replacement. Not sure about the impact on performance though. We might avoid breaking sharing in some cases but there'd be additional cost for the comparisons.

I think there's a risk this is way too expensive and thus I'd rather not add this change.

Yeah that's ok, we'd probably have to specifically benchmark this. My hunch is that the map comparisons could be cheap on average if it's likely that they differ in size or that we find a mismatch quickly.

romainbrenguier · 2019-04-02T09:10:11Z

Here are the results from my benchmarks, globaly using sharing_mapt was 13% faster and seems to scale better:

owen-mc-diffblue · 2019-04-02T09:41:22Z

src/goto-symex/symex_main.cpp

@@ -676,14 +676,14 @@ void goto_symext::try_filter_value_sets(
  }
  if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty())
  {
-    value_sett::entryt *entry = jump_taken_value_set->get_entry_for_symbol(
+    auto entry = jump_taken_value_set->get_index_of_symbol(


Rename entry to entry_name or entry_index 🍌

owen-mc-diffblue · 2019-04-02T09:41:28Z

src/goto-symex/symex_main.cpp

      symbol_expr->get_identifier(), symbol_type, "", ns);
    jump_taken_value_set->erase_values_from_entry(
      *entry, erase_from_jump_taken_value_set);
  }
  if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty())
  {
-    value_sett::entryt *entry = jump_not_taken_value_set->get_entry_for_symbol(
+    auto entry = jump_not_taken_value_set->get_index_of_symbol(


owen-mc-diffblue · 2019-04-02T09:50:31Z

src/pointer-analysis/value_set.cpp

@@ -491,11 +472,11 @@ void value_sett::get_value_set_rec(
  }
  else if(expr.id()==ID_symbol)
  {
-    const entryt *entry = get_entry_for_symbol(
+    auto entry = get_index_of_symbol(


smowton · 2019-04-02T15:15:49Z

Evaluated this on one of our medium-sized Java applications (a particular WebGoat lesson) -- JBMC execution time down from ~30s to ~15s.

danpoe · 2019-04-02T16:21:40Z

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 was 7% faster, including the changes to update_entry() it was 9% faster.

goto-symex copies a state, which contains a value set, at each branching point. The paths originating at that branch point typically share most of the points-to information. Thus the copy is unnecessarily expensive, and so is the merge at the next join point, which will also result in one of the value sets to be destroyed. With sharing_mapt, the copy has constant cost, merging can make use of the delta view, and the cost of destruction only depends on the size of the delta.

allredj

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

tautschnig added Needs data This PR claims improvements that require further data to substantiate the claims. dependent - do not merge labels Mar 30, 2019

tautschnig self-assigned this Mar 30, 2019

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel and smowton as code owners March 30, 2019 14:52

allredj reviewed Mar 30, 2019

View reviewed changes

tautschnig assigned smowton and romainbrenguier Mar 30, 2019

tautschnig mentioned this pull request Mar 30, 2019

Use sharing_mapt to store propagation map #4464

Merged

4 tasks

martin-cs approved these changes Apr 1, 2019

View reviewed changes

tautschnig added a commit that referenced this pull request Apr 1, 2019

Merge pull request #4462 from tautschnig/remove-value_set-idt

ba576c4

Remove value_sett::idt [blocks: #4463]

tautschnig force-pushed the use-sharing-map-for-value-set branch from 442b500 to 441eb6c Compare April 1, 2019 08:08

tautschnig removed the dependent - do not merge label Apr 1, 2019

tautschnig removed their assignment Apr 1, 2019

smowton approved these changes Apr 1, 2019

View reviewed changes

allredj reviewed Apr 1, 2019

View reviewed changes

danpoe approved these changes Apr 1, 2019

View reviewed changes

owen-mc-diffblue approved these changes Apr 2, 2019

View reviewed changes

tautschnig force-pushed the use-sharing-map-for-value-set branch from 441eb6c to d4b811b Compare April 3, 2019 07:54

tautschnig removed the Needs data This PR claims improvements that require further data to substantiate the claims. label Apr 3, 2019

tautschnig merged commit d583164 into diffblue:develop Apr 3, 2019

tautschnig deleted the use-sharing-map-for-value-set branch April 3, 2019 08:46

allredj reviewed Apr 3, 2019

View reviewed changes

Use sharing_mapt as container in value_sett #4463

Use sharing_mapt as container in value_sett #4463

Uh oh!

Conversation

tautschnig commented Mar 30, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 30, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

danpoe left a comment

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!

romainbrenguier commented Apr 2, 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!

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 Apr 2, 2019

Uh oh!

danpoe commented Apr 2, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!