Use std::forward_list instead of std::map in irept by default [blocks: #3486] #4458

tautschnig · 2019-03-29T22:29:38Z

This reduces the size of an irept by 5 pointers (i.e., 40 bytes on
64-bit systems).

Also make typet constructor compatible with the STL shipped with GCC 5.

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 · 2019-03-30T09:07:34Z

Can you split? The constructor seems obvious and trivial, whereas the change to list will require us to do a lot of consulting & benchmarking.

tautschnig · 2019-03-30T10:06:15Z

@kroening The constructor change is now in #4460.

tautschnig · 2019-03-30T10:38:56Z

Just for the record: on ReachSafety-ECA with this change we can perform 3819.81 symex_step calls per second, compared to 2752.28 calls per second with develop. I'll now try to figure out what exactly makes so much of a difference.

tautschnig · 2019-03-30T10:56:01Z

It seems that just about any irept-related operation is cheaper (creating fresh irepts of course, but also irept::operator==).

Ensure typet constructor is always compatible with GCC 5's STL [blocks: #4458]

danpoe · 2019-05-09T11:43:28Z

On a set of methods from Apache Tika, symex was overall 21% faster with the changes in this PR (20.8s vs 26.4s).

smowton · 2019-05-09T15:47:45Z

On my large Webgoat run I find running time is practically identical, but the memory usage is down around 30%.

martin-cs · 2019-05-09T17:21:07Z

Although I responded with a 👍 I didn't actually provide meaningfu l comments to what @martin-cs said:

No worries -- I ignored your responses for a month! :-\

> I think we're going to need some large scale benchmarking before we > can make this change. Yes, all proposals or efforts most welcome.

Am a bit short on time but will try when I have some.

> My guess is that there is a clear bias on which of the entries of > the map are most used. Does it make sense to sort them / use a list > that pivots them to the front? We might as well want to measure the median size of the map: I'd suspect it would be 1 or 2 (expressions carry a type and maybe a source location).

Yes; that would be the thing to do before thinking of any optimisations.

romainbrenguier · 2019-05-10T11:09:52Z

Here are the results on my benchmark:

overall forward lists were about 10% faster

martin-cs · 2019-05-10T13:25:25Z

That's starting to look quite convincing isn't it?

tautschnig · 2019-05-11T13:05:04Z

No known regressions (including external feedback), just needs final approval from at least one of @chrisr-diffblue @forejtv @peterschrammel @thk123.

allredj

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

allredj

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

irep.h provides std::map if, and only if, NAMED_SUB_IS_FORWARD_LIST is not set. Also cleanup include guards (pushing them to be the outermost preprocessor directives) and indentation of includes.

This reduces the size of an irept by 5 pointers (i.e., 40 bytes on 64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can perform 3819.81 symex_step calls per second, compared to 2752.28 calls per second with the std::map configuration. The performance improvements are spread across various `irept`-related operations.

allredj

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

tautschnig added Needs data This PR claims improvements that require further data to substantiate the claims. blocker labels Mar 29, 2019

tautschnig mentioned this pull request Mar 29, 2019

Patch set for SV-COMP'19 [depends-on: #2000, #3462] #3486

Closed

13 tasks

tautschnig self-assigned this Mar 29, 2019

tautschnig force-pushed the forward-list branch from 6a00fc5 to c8f04da Compare March 29, 2019 23:43

tautschnig changed the title ~~Use std::forward_list instead of std::map in irept by default~~ Use std::forward_list instead of std::map in irept by default [depends-on: #4460] Mar 30, 2019

tautschnig marked this pull request as ready for review March 30, 2019 10:56

tautschnig requested review from kroening, peterschrammel, pkesseli and smowton as code owners March 30, 2019 10:56

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

smowton approved these changes Mar 30, 2019

View reviewed changes

tautschnig added a commit that referenced this pull request Mar 30, 2019

Merge pull request #4460 from tautschnig/constructor-fix

d460249

Ensure typet constructor is always compatible with GCC 5's STL [blocks: #4458]

tautschnig force-pushed the forward-list branch from c8f04da to ff3ab02 Compare March 30, 2019 12:38

tautschnig removed the dependent - do not merge label Mar 30, 2019

tautschnig assigned kroening and unassigned tautschnig Mar 30, 2019

tautschnig changed the title ~~Use std::forward_list instead of std::map in irept by default [depends-on: #4460]~~ Use std::forward_list instead of std::map in irept by default [blocks: #3486] Mar 30, 2019

tautschnig force-pushed the forward-list branch 2 times, most recently from 512e9c9 to d0f270e Compare March 30, 2019 15:58

tautschnig requested review from chrisr-diffblue, forejtv and thk123 as code owners March 30, 2019 15:58

tautschnig force-pushed the forward-list branch from d0f270e to 8abf058 Compare March 30, 2019 16:08

tautschnig assigned peterschrammel, forejtv, danpoe, romainbrenguier and chrisr-diffblue May 8, 2019

tautschnig assigned thk123 and chrisr-diffblue and unassigned smowton, danpoe, chrisr-diffblue and romainbrenguier May 11, 2019

tautschnig force-pushed the forward-list branch from dbaeda0 to 754dbfc Compare May 16, 2019 08:47

allredj reviewed May 16, 2019

View reviewed changes

tautschnig force-pushed the forward-list branch from 754dbfc to cfcc7e8 Compare May 16, 2019 13:25

allredj reviewed May 16, 2019

View reviewed changes

tautschnig added 2 commits May 19, 2019 17:03

Add missing std::map include

71eaad6

irep.h provides std::map if, and only if, NAMED_SUB_IS_FORWARD_LIST is not set. Also cleanup include guards (pushing them to be the outermost preprocessor directives) and indentation of includes.

tautschnig force-pushed the forward-list branch from cfcc7e8 to 2b9849a Compare May 19, 2019 17:03

allredj reviewed May 19, 2019

View reviewed changes

peterschrammel approved these changes May 28, 2019

View reviewed changes

tautschnig merged commit c4ffbee into diffblue:develop May 28, 2019

tautschnig deleted the forward-list branch May 28, 2019 15:02

This was referenced May 29, 2019

Revert "Use std::forward_list instead of std::map in irept by default" #4729

Merged

Use std::forward_list instead of std::map in irept by default #4731

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use std::forward_list instead of std::map in irept by default [blocks: #3486] #4458

Use std::forward_list instead of std::map in irept by default [blocks: #3486] #4458

tautschnig commented Mar 29, 2019

kroening commented Mar 30, 2019

tautschnig commented Mar 30, 2019

tautschnig commented Mar 30, 2019

tautschnig commented Mar 30, 2019

danpoe commented May 9, 2019

smowton commented May 9, 2019

martin-cs commented May 9, 2019 via email

romainbrenguier commented May 10, 2019

martin-cs commented May 10, 2019

tautschnig commented May 11, 2019

allredj left a comment

allredj left a comment

allredj left a comment

Use std::forward_list instead of std::map in irept by default [blocks: #3486] #4458

Use std::forward_list instead of std::map in irept by default [blocks: #3486] #4458

Conversation

tautschnig commented Mar 29, 2019

kroening commented Mar 30, 2019

tautschnig commented Mar 30, 2019

tautschnig commented Mar 30, 2019

tautschnig commented Mar 30, 2019

danpoe commented May 9, 2019

smowton commented May 9, 2019

martin-cs commented May 9, 2019 via email

romainbrenguier commented May 10, 2019

martin-cs commented May 10, 2019

tautschnig commented May 11, 2019

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment