Do not unnecessarily sort guard conjuncts [blocks: #3486] #1998

tautschnig · 2018-04-03T13:50:44Z

They are constructed in a consistent order anyway.

smowton · 2018-04-09T09:06:07Z

src/util/guard.cpp

    if(it1!=op1.end() && *it1==*it2)
      it1=op1.erase(it1);
+    else


I don't think this works? For example, a & b - b would not erase the b, since it1 now has no way of moving except when erasing an element.

Relatedly, for vectors this has worst-case quadratic cost. How about making a utility inplace-set-difference that provides a good place to benchmark this sort of repeated single-element erase vs. std::set_difference followed by swap?

I agree that this would not work with a & b - b, but as the commit message says: we never construct those. My proposal for a full solution is #310: use BDDs. I'm open to all other ideas. But right now it's just computational overhead...

In that case I suggest renaming this remove_prefix_conjuncts, since its behaviour is much more specific than a generic operator-=, and add a doxy comment specifying that's all it can do. Also consider using std::mismatch?

allredj

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

tautschnig · 2019-03-12T10:28:20Z

For the record: on ReachSafety-ECA this increases the number of symex steps per second from 2961.83 to 3580.92 - a speedup of approximately 20%. This is all due to saving approximately 2500 seconds in sort_operands (by not calling it).

Similar savings may be possible when using BDDs, in particular with CUDD. Benchmarking thereof started just now.

tautschnig · 2019-03-12T18:34:48Z

Adding data on BDDs (using CUDD): the operator|= is now, as hoped, basically free (0.5 seconds instead of 440 seconds with develop). Somewhat surprisingly, however, the cost of merge_ireps is now a lot higher. Consequently we only achieve 2608.81 steps per second.

romainbrenguier · 2019-03-13T08:09:07Z

@tautschnig

Adding data on BDDs (using CUDD): the operator|= is now, as hoped, basically free (0.5 seconds instead of 440 seconds with develop). Somewhat surprisingly, however, the cost of merge_ireps is now a lot higher. Consequently we only achieve 2608.81 steps per second.

The guards sometimes become much bigger with BDDs than with exprt. On my benchmarks I also noticed that while the global execution was 30% faster, the execution with --show-vcc --verbosity 0 was slower with BDDs on average. I also noticed merge_ireps taking a long time, in particular in the example I had to disable (grep for "bdd-expected-timeout").

tautschnig · 2019-03-13T08:26:24Z

The above data was all based on profiling information, which I prefer not to exclusively rely on. The optimised, competition-setting runs yield (more == better):

develop: 116 points
this PR: 119 points
BDDs/CUDD: 91 points

This of course is only a single (and somewhat peculiar: basically no pointers, but otherwise heavily stressing goto-symex) category.

tautschnig · 2019-03-13T08:28:59Z

I also noticed merge_ireps taking a long time, in particular in the example I had to disable (grep for "bdd-expected-timeout").

I'll try to do some benchmarking with HASH_CODE enabled at a later time to see whether that helps.

romainbrenguier · 2019-03-13T15:29:31Z

@tautschnig

I'll try to do some benchmarking with HASH_CODE enabled at a later time to see whether that helps.

Oh yes I always use HASH_CODE. For the merging of ireps it seems redundant for BDDs since all nodes that are logically equivalent are already "merged". So maybe the merge and the conversion from BDD to exprt should be done together. I will try some things.

romainbrenguier · 2019-03-14T07:56:50Z

@tautschnig

Adding data on BDDs (using CUDD): the operator|= is now, as hoped, basically free (0.5 seconds instead of 440 seconds with develop). Somewhat surprisingly, however, the cost of merge_ireps is now a lot higher. Consequently we only achieve 2608.81 steps per second.

I'm not sure I understand what these steps represent. Could you explain? If BDDs lead to fewer steps being executed for analyzing the same program, you could have fewer steps per second but still be faster?

tautschnig · 2019-03-14T13:45:44Z

If BDDs lead to fewer steps being executed for analyzing the same program, you could have fewer steps per second but still be faster?

Yes, this is certainly possible, hence me also posting the scores achieved in that category. What I'm looking at in the profiles is:

The number of calls to goto_symext::symex_with_state (that's basically the total number of runs of CBMC).
The number of calls to symex_bmct::symex_step (that's what I consider the total number of symbolic execution steps).
The time spent in symex_bmct::symex_step together with all of the functions that it calls.

For develop and ReachSafety-ECA those numbers were:

4305 calls
48005643 calls
16208.08 seconds

I do agree and emphasise that this is by no means a complete picture. For me this mainly is about having reproducible data that I can key an eye on over time.

tautschnig · 2019-03-25T02:17:24Z

I'll try to do some benchmarking with HASH_CODE enabled at a later time to see whether that helps.

That's now done, scatter plot comparing current develop (y axis) vs BDDs+HASH_CODE (x axis) is shown below. The scores are now almost the same (155 with BDDs, 157 without BDDs).

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: f4a99f0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105613658
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

martin-cs · 2019-03-25T08:22:40Z

There is something significant in that graph to do with the number of time-outs. There is a vertical "smear" near the X axis time-out which suggests that there is a serious scalability difference there so I am surprised the numbers are so similar.

martin-cs

I believe the patch implements what is described in the PR. Whether we want it is a different question. I can see that this is performance critical and I don't think the current behaviour is optimal, even for this design. The "common prefix" comments give me pause for concern because that doesn't describe what I think is going on. Could we simply add (and document) some invariants on the guard expressions always being in (some) sorted order? It feels like that should be do-able, would give the performance benefits of this patch with some extra certainty of what is going on.

( I agree that BDDs are actually the way of solving this in full generality but I do wonder whether what we have is sufficiently restricted that we can solve it with a less heavy-weight solution. Regardless, I think pinning down what is going on here in terms of order with help the BDD case as well. )

tautschnig · 2019-03-25T11:35:56Z

With latest develop (and this PR rebased on top of it) profiling suggest that we save approximately 30% in guard_exprt::operator-= (reducing time spent in there from 1000s to 700s). For the overall result, however, there is no notable difference on ReachSafety-ECA.

martin-cs · 2019-03-25T12:22:24Z

On Mon, 2019-03-25 at 04:35 -0700, Michael Tautschnig wrote: With latest develop (and this PR rebased on top of it) profiling suggest that we save approximately 30% in `guard_exprt::operator-=` (reducing time spent in there from 1000s to 700s). For the overall result, however, there is no notable difference on ReachSafety-ECA.

Do we generate the same results? I can believe that we can save time in guard_exprt but generate more complex guards and thus loose time over-all.

tautschnig · 2019-03-30T16:06:23Z

Do we generate the same results? I can believe that we can save time
in guard_exprt but generate more complex guards and thus loose time
over-all.

As far as I can tell we generate exactly the same results.

Guards are (no longer) generic conjunctions. They are constructed in a consistent order. If a more generic set-up is required, use BDD-backed guards.

codecov · 2021-05-16T21:36:27Z

Codecov Report

Merging #1998 (eabd67c) into develop (f564088) will decrease coverage by 0.08%.
The diff coverage is 82.38%.

@@             Coverage Diff             @@
##           develop    #1998      +/-   ##
===========================================
- Coverage    75.53%   75.45%   -0.09%     
===========================================
  Files         1447     1447              
  Lines       158116   158087      -29     
===========================================
- Hits        119431   119277     -154     
- Misses       38685    38810     +125

Impacted Files	Coverage Δ
src/analyses/guard_expr.cpp	`97.82% <ø> (-0.14%)`	⬇️
src/goto-instrument/accelerate/accelerate.cpp	`34.89% <0.00%> (ø)`
src/goto-instrument/concurrency.cpp	`0.00% <0.00%> (ø)`
src/goto-instrument/nondet_volatile.cpp	`86.55% <ø> (-0.15%)`	⬇️
src/goto-instrument/replace_calls.cpp	`89.55% <0.00%> (+1.31%)`	⬆️
src/goto-programs/goto_convert_class.h	`87.30% <ø> (ø)`
src/goto-programs/goto_convert.cpp	`91.69% <33.33%> (-0.24%)`	⬇️
src/util/simplify_expr_struct.cpp	`74.38% <50.00%> (+0.78%)`	⬆️
src/goto-instrument/goto_program2code.cpp	`69.20% <60.00%> (+0.06%)`	⬆️
src/util/simplify_expr.cpp	`78.14% <65.00%> (-6.93%)`	⬇️
... and 75 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 0ea7f13...eabd67c. Read the comment docs.

tautschnig · 2021-05-18T15:39:05Z

The following two flame graphs demonstrate what made me look into this (observe how goto_symext::merge_gotos seems to be (transitively) spending a lot of time in sort_and_join) and that merge_gotos now no longer is the most expensive part of execute_next_instruction.

That being said, the overall impact is fairly small (total CPU time saved is a few seconds), and this benchmark category of SV-COMP (Reachsafety-Recursive) is the only one where this was notable at all.

I do maintain that this sorting is unnecessary given the way guards are constructed by goto-symex (AFAIK the only user), but I don't think the performance data alone provide a great deal of support for this cleanup.

martin-cs

If the code is redundant and removing it 1. causes no harm, 2. improves things a bit then... why not?

tautschnig requested review from kroening, peterschrammel and smowton as code owners April 3, 2018 13:50

tautschnig self-assigned this Apr 5, 2018

smowton reviewed Apr 9, 2018

View reviewed changes

tautschnig force-pushed the no-sort-guards branch from 1e4fd71 to 6bd4556 Compare March 11, 2019 15:00

tautschnig requested a review from pkesseli as a code owner March 11, 2019 15:00

allredj reviewed Mar 12, 2019

View reviewed changes

tautschnig force-pushed the no-sort-guards branch from 6bd4556 to f4a99f0 Compare March 25, 2019 02:17

tautschnig requested review from chrisr-diffblue, danpoe, martin-cs, owen-mc-diffblue and thk123 as code owners March 25, 2019 02:17

allredj reviewed Mar 25, 2019

View reviewed changes

martin-cs reviewed Mar 25, 2019

View reviewed changes

tautschnig mentioned this pull request Mar 30, 2019

Do not sort operands as part of simplification [blocks: #3486] #1997

Merged

tautschnig changed the title ~~[SV-COMP'18 9/19] Do not unnecessarily sort guard conjuncts~~ [SV-COMP'18 9/19] Do not unnecessarily sort guard conjuncts [blocks: #3486] Mar 30, 2019

tautschnig changed the title ~~[SV-COMP'18 9/19] Do not unnecessarily sort guard conjuncts [blocks: #3486]~~ Do not unnecessarily sort guard conjuncts [blocks: #3486] Mar 30, 2019

tautschnig added the blocker label Mar 30, 2019

Do not unnecessarily sort guard conjuncts

eabd67c

Guards are (no longer) generic conjunctions. They are constructed in a consistent order. If a more generic set-up is required, use BDD-backed guards.

tautschnig force-pushed the no-sort-guards branch from f4a99f0 to eabd67c Compare May 16, 2021 19:53

martin-cs approved these changes May 19, 2021

View reviewed changes

tautschnig merged commit 60abd1e into diffblue:develop May 19, 2021

tautschnig deleted the no-sort-guards branch May 19, 2021 14:35

Do not unnecessarily sort guard conjuncts [blocks: #3486] #1998

Do not unnecessarily sort guard conjuncts [blocks: #3486] #1998

Uh oh!

Conversation

tautschnig commented Apr 3, 2018

Uh oh!

smowton Apr 9, 2018

Choose a reason for hiding this comment

Uh oh!

smowton Apr 9, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Apr 10, 2018

Choose a reason for hiding this comment

Uh oh!

smowton Apr 10, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 12, 2019

Uh oh!

tautschnig commented Mar 12, 2019

Uh oh!

romainbrenguier commented Mar 13, 2019

Uh oh!

tautschnig commented Mar 13, 2019

Uh oh!

tautschnig commented Mar 13, 2019

Uh oh!

romainbrenguier commented Mar 13, 2019

Uh oh!

romainbrenguier commented Mar 14, 2019

Uh oh!

tautschnig commented Mar 14, 2019

Uh oh!

tautschnig commented Mar 25, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Mar 25, 2019

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 25, 2019

Uh oh!

martin-cs commented Mar 25, 2019 via email

Uh oh!

tautschnig commented Mar 30, 2019

Uh oh!

codecov bot commented May 16, 2021

Codecov Report

Uh oh!

tautschnig commented May 18, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!