Performance improvement and cleanup of local bitvector analysis #6528

tautschnig · 2021-12-15T11:59:52Z

Please review commit-by-commit. The commit messages include performance evaluation data.

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.

kroening · 2021-12-15T12:11:08Z

Commit message: "enqueuing successor nodes" -> "dequeuing successor nodes"

By using a set instead of a stack as work queue we reduce the number of visits to each node in two ways: 1) The work queue will not contain duplicate nodes. 2) When dequeuing successor nodes, back edges will be given preference over forward ones. Once the later (in program order) node is visited, more information is already merged into the abstract state. On a goto function with 160822 instruction, this reduces processing time (just the local bitvector analysis) from 1700 seconds down to 72 seconds. The number of invocations of `local_bitvector_analysist::merge` previously was 32815499 (204 times the number of nodes), and is now 997083 (6 times the number of nodes).

This avoids a jump. On a goto function of 160822 instructions, the total time required by local bitvector analysis decreases from 72 seconds to 65 seconds (averaged over three runs, the difference between the slowest and longest run is below 0.2 seconds).

The correct type is std::size_t in all cases. Use `auto` where the type can be inferred, and the typedef'd name where it's `local_cfgt`'s business to choose the type.

tautschnig · 2021-12-15T12:37:06Z

Commit message: "enqueuing successor nodes" -> "dequeuing successor nodes"

Err, of course, thank you!

codecov · 2021-12-15T13:14:11Z

Codecov Report

Merging #6528 (8834dc5) into develop (5f33908) will increase coverage by 0.00%.
The diff coverage is 96.42%.

@@           Coverage Diff            @@
##           develop    #6528   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1578     1578           
  Lines       180910   180919    +9     
========================================
+ Hits        137467   137476    +9     
  Misses       43443    43443

Impacted Files	Coverage Δ
src/analyses/local_bitvector_analysis.h	`90.19% <ø> (ø)`
src/analyses/local_bitvector_analysis.cpp	`73.98% <88.88%> (-0.15%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`95.11% <100.00%> (+0.07%)`	⬆️

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 eeddb3f...8834dc5. Read the comment docs.

martin-cs

20x speed-up due to a change in data-structure! I love it! Classic computer science. Would it be possible to have another PR that s/stack/set/ in local_may_aliast too?

martin-cs · 2021-12-15T14:20:31Z

src/analyses/local_bitvector_analysis.cpp

@@ -242,8 +242,8 @@ void local_bitvector_analysist::build()
  if(cfg.nodes.empty())
    return;

-  work_queuet work_queue;


This one has a friend who would also like to become a set:

cbmc/src/analyses/local_may_alias.h

Line 61 in eeddb3f

typedef std::stack<local_cfgt::node_nrt> work_queuet;

Good call, I'll do so in a follow-up PR.

kroening · 2021-12-15T12:07:08Z

src/analyses/local_bitvector_analysis.cpp

-    if(a[i].merge(b[i]))
-      result=true;
-  }
+    result |= a[i].merge(b[i]);


I would add a comment that the bitwise or is used instead of the logical or to prevent the short-circuit semantics.

kroening · 2021-12-15T12:08:39Z

src/analyses/local_bitvector_analysis.cpp

-  work_queuet work_queue;
-  work_queue.push(0);
+  std::set<local_cfgt::node_nrt> work_queue;
+  work_queue.insert(0);



Queues are usually ordered (especially in the UK). Is the set really helping performance, and if so, I'd rename it to "work_set".

remi-delmas-3000

Can this result in a different fixed point being reached ? What are the implications for the precision of the analysis ? Are there any iteration strategies that can result in more precise results ? In any acceptable perf tradeoff that favors precision might more useful for users of this class.

martin-cs · 2021-12-15T21:09:35Z

Can this result in a different fixed point being reached ?

In the general case, yes. In this specific analysis, I think not because it is so simple and does not do any of the obvious "exploration order matters" things like interprocedural analysis.

What are the implications for the precision of the analysis ?

I don't think there are any. I would be interested in being proven wrong. It should be possible to easily test for significant differences by: 1. Patching the "remove from set" to remove a random element. 2. Ask @tautschnig to run the analysis a bunch of times with different random seeds and see what happens.

Are there any iteration strategies that can result in more precise results ?

Given a program, there is a best order. It is not clear (and I think somewhere I have examples to show) that there is not one order which works for all programs.

In any acceptable perf tradeoff that favors precision might more useful for users of this class.

I think in this specific case it doesn't matter, plus, this is supposed to be a very light-weight analysis. If you want to experiment, `ai_historyt` has control over the order of exploration, via: https://github.com/diffblue/cbmc/blob/47c1c7e70cb17e3315ebacde99ef5b1f4a69eb91/src/analyses/ai_history.h#L123 Some of the existing implementation are ... to put it bluntly, kinda crude: https://github.com/diffblue/cbmc/blob/47c1c7e70cb17e3315ebacde99ef5b1f4a69eb91/src/analyses/ai_history.h#L199 So this could be improved. If you want to do something more sophisticated then a new `ai_historyt` or inheriting from `ai_baset` and changing how `fixpoint()` works: https://github.com/diffblue/cbmc/blob/47c1c7e70cb17e3315ebacde99ef5b1f4a69eb91/src/analyses/ai.cpp#L224 HTH Cheers, - Martin

tautschnig requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners December 15, 2021 11:59

tautschnig force-pushed the bitvector-analysis branch from 08d2339 to c25f97b Compare December 15, 2021 12:06

tautschnig added 3 commits December 15, 2021 12:36

Local bitvector analysis: cleanup improver use of unsigned

8834dc5

The correct type is std::size_t in all cases. Use `auto` where the type can be inferred, and the typedef'd name where it's `local_cfgt`'s business to choose the type.

tautschnig force-pushed the bitvector-analysis branch from c25f97b to 8834dc5 Compare December 15, 2021 12:36

martin-cs approved these changes Dec 15, 2021

View reviewed changes

tautschnig merged commit 73fbad9 into diffblue:develop Dec 15, 2021

tautschnig deleted the bitvector-analysis branch December 15, 2021 15:11

kroening reviewed Dec 15, 2021

View reviewed changes

remi-delmas-3000 reviewed Dec 15, 2021

View reviewed changes

martin-cs mentioned this pull request Dec 15, 2021

A new abstract interpreter for performing function-local analysis #6529

Draft

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Performance improvement and cleanup of local bitvector analysis #6528

Performance improvement and cleanup of local bitvector analysis #6528

Uh oh!

tautschnig commented Dec 15, 2021

Uh oh!

kroening commented Dec 15, 2021

Uh oh!

tautschnig commented Dec 15, 2021

Uh oh!

codecov bot commented Dec 15, 2021 •

edited

Loading

Uh oh!

martin-cs left a comment

Uh oh!

martin-cs Dec 15, 2021

Uh oh!

tautschnig Dec 15, 2021

Uh oh!

kroening Dec 15, 2021

Uh oh!

kroening Dec 15, 2021

Uh oh!

remi-delmas-3000 left a comment

Uh oh!

martin-cs commented Dec 15, 2021 via email

Uh oh!

Uh oh!

Performance improvement and cleanup of local bitvector analysis #6528

Performance improvement and cleanup of local bitvector analysis #6528

Uh oh!

Conversation

tautschnig commented Dec 15, 2021

Uh oh!

kroening commented Dec 15, 2021

Uh oh!

tautschnig commented Dec 15, 2021

Uh oh!

codecov bot commented Dec 15, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs Dec 15, 2021

Choose a reason for hiding this comment

Uh oh!

tautschnig Dec 15, 2021

Choose a reason for hiding this comment

Uh oh!

kroening Dec 15, 2021

Choose a reason for hiding this comment

Uh oh!

kroening Dec 15, 2021

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Dec 15, 2021 via email

Uh oh!

Uh oh!

codecov bot commented Dec 15, 2021 •

edited

Loading