Memory regression test [blocks: #2035] #1971

tautschnig · 2018-03-25T12:44:38Z

This is a first proof of concept that should help spotting differences in heap memory usage. CPU performance benchmarking does not necessarily provide sufficient insight as discussed in #1855 and #1860.

chrisr-diffblue · 2018-03-26T09:57:05Z

scripts/memory-test/memory.py

+        data_seq.append(
+                snapshot(data['snapshots'][rd], rd == peak_index))
+
+    diff = color_diff(


While colour diff output is pretty and a neat feature, could we make it fallback gracefully to non-colourised output when, e.g. the output terminal doesn't support colour (rare these days) or the output is piped to a file?

Done, I think. (Colorama knows how to do this, and I've now hacked that into the ColorFallback code as well.)

chrisr-diffblue · 2018-03-26T10:01:01Z

.travis.yml

    - stage: Test different OS/CXX/Flags
      os: linux
      compiler: gcc
-      cache: ccache
      env:


What is the reason for disabling ccache here? You changed this config to be a Debug build, but you can still use ccache with that if you increase the ccache size to 2G just for this configuration.

Is that ok to do? Surely happy to do that, I was actually hoping for your input on that ;-)

Yeah, I'd much rather have ccache enabled and bump it's size just for this config than not have it enabled (it'll make saving the cache back a bit slower, but you'll more than win that back with the build time improvements :-) )

chrisr-diffblue · 2018-03-26T10:08:31Z

.travis.yml

-        - ccache -z
-        - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Debug'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'


Do you want/need Debug here, or would RelWithDebInfo be a closer representative of the memory performance of a release build?

Probably true - will use that!

tautschnig · 2018-03-26T19:17:49Z

This appears to work reliably now. Reviews would be appreciated.

chrisr-diffblue

Looks good to me!

tautschnig · 2018-03-27T11:07:48Z

Just one heads-up: it seems this regression test is now stable when run on an unmodified code-base. The memory-profile matching is fuzzy, but might not yet be sufficiently fuzzy to accept all negligible differences. I will have to work on this once it is merged and spuriously failing PRs arise.

forejtv · 2018-04-13T07:50:13Z

@tautschnig I am not too excited about having a subdirectory with an alternative license. Where does the script come from? Any chance we could use it under the standard CBMC license?

chrisr-diffblue · 2018-04-13T11:20:05Z

I haven't gone to look what other licenses we have inside the CBMC repo, but if we're going to have mixed license like this, is there an argument for putting all the files that are separately licensed under their own directory hierarchy - e.g a 'contrib' or 'external' directory at the top level of the CBMC repo? Or treat these files like mini-sat, where they get downloaded rather than imported into the repo? I'm not personally hugely concerned either way, but it would make things clearer if all the 'non CBMC license' stuff was more obviously separated.

tautschnig · 2018-04-13T11:43:38Z

As far as I'm aware we have got:

scripts/cpplint.py: Copyright Google Inc; BSD 3-clause license
src/big-int/*: Copyright Dirk Zoller; public domain
src/miniz/*: Copyright RAD Game Tools, Valve Software, Rich Geldreich, Tenacious Software LLC; MIT license
src/nonstd/optional.hpp: Copyright Martin Moene; MIT license
src/util/sorted_vector.h: Copyright Martin Holzherr; MIT-like license (Remove utilities that never got used #2019 proposes to remove this file)
unit/testing-utils/catch.hpp: Copyright Two Blue Cubes Ltd; Boost Software License (almost the same as MIT)

Just import the minimum required for our future use from https://github.com/MathieuTurcotte/msparser at 8ce7336d9b55366. This code is MIT licensed (license information included).

This tool will enable memory regression tests by comparing heap memory profiles generated using valgrind's Massif tool (or any other tool that can generate compatible output).

The CMake build configuration is now set to RelWithDebInfo to obtain usable function call names in the heap trace. As this yields different and larger binaries, ccache's cache size is increased to 2G for this stage.

tautschnig · 2018-04-18T00:56:54Z

Back to reviewers: not sure what the status on licenses is, otherwise this has now seen the following improvements: 1) The memory regression test is non-fatal to make sure its somewhat experimental nature doesn't cause inadvertent blocking. 2) The diff script now is fuzzy in its matching so that the the varying number of snapshots that massif generates does not cause havoc each time. 3) I have experimented with Google perftools and heaptrack and have neither found either of them more deterministic nor more insightful; on the contrary, massif still produces the most reliable memory profiles.

NathanJPhillips

Don't know enough about memory profiling, Python or Yaml to contribute a useful review however I approve of the efforts to introduce memory profiling to CBMC.

NathanJPhillips · 2018-04-30T16:45:49Z

.travis.yml

-        - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
+        - ccache --max-size=2G
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=RelWithDebInfo'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'


Have these two changes accidentally escaped here from other work?

No, they are intentional; the commit message tries to call them out, but it might not be sufficiently clear?

I can confirm that this was an intentional change that @tautschnig and I
discussed in an earlier part of this PR.

martin-cs

I'm not going to comment on the licensing issues but massif is my tool of choice for heap profiling CPROVER and having a regular, automated run of it would be A Good Thing.

peterschrammel

Putting the MIT-licensed test utility scripts into a separate directory is ok.

TGWDB · 2021-05-19T08:05:00Z

Closing this this is very out of date and apparently untouched. The blocker appears to no longer be true. Please reopen and redo for new CI system if you believe this is erroneous.

tautschnig requested review from forejtv, peterschrammel and thk123 as code owners March 25, 2018 12:44

tautschnig requested review from NathanJPhillips, martin-cs and chrisr-diffblue March 25, 2018 12:44

tautschnig added the do not merge label Mar 25, 2018

tautschnig self-assigned this Mar 25, 2018

tautschnig force-pushed the memory-regression-test branch 4 times, most recently from 9d6ecda to b3b98a6 Compare March 26, 2018 09:11

chrisr-diffblue reviewed Mar 26, 2018

View reviewed changes

tautschnig force-pushed the memory-regression-test branch 2 times, most recently from 2688772 to 27e794f Compare March 26, 2018 11:10

tautschnig removed the do not merge label Mar 26, 2018

tautschnig force-pushed the memory-regression-test branch 4 times, most recently from 8e8a19b to edcf5c2 Compare March 26, 2018 18:14

tautschnig assigned thk123, peterschrammel and forejtv and unassigned tautschnig Mar 26, 2018

chrisr-diffblue approved these changes Mar 27, 2018

View reviewed changes

tautschnig mentioned this pull request Mar 27, 2018

Restore irept sharing #1855

Closed

tautschnig mentioned this pull request Apr 9, 2018

irept: Use singly-linked lists with SUB_IS_LIST [depends on: #3606] #2035

Merged

tautschnig assigned tautschnig and unassigned thk123, peterschrammel and forejtv Apr 15, 2018

tautschnig force-pushed the memory-regression-test branch 4 times, most recently from 651b607 to 1d90a73 Compare April 17, 2018 22:51

tautschnig added 2 commits April 17, 2018 23:51

Import Massif parser from MathieuTurcotte/msparser

da287d1

Just import the minimum required for our future use from https://github.com/MathieuTurcotte/msparser at 8ce7336d9b55366. This code is MIT licensed (license information included).

memory.py: Compute a diff over Massif heap memory profiles

a02caa4

This tool will enable memory regression tests by comparing heap memory profiles generated using valgrind's Massif tool (or any other tool that can generate compatible output).

tautschnig force-pushed the memory-regression-test branch from 1d90a73 to eb94fce Compare April 17, 2018 23:52

Perform memory regression test in Travis/Ubuntu/cmake/g++ build

eb94fce

The CMake build configuration is now set to RelWithDebInfo to obtain usable function call names in the heap trace. As this yields different and larger binaries, ccache's cache size is increased to 2G for this stage.

tautschnig assigned thk123, peterschrammel and forejtv and unassigned tautschnig Apr 18, 2018

NathanJPhillips reviewed Apr 30, 2018

View reviewed changes

martin-cs approved these changes May 23, 2018

View reviewed changes

peterschrammel approved these changes Jun 3, 2018

View reviewed changes

tautschnig assigned tautschnig and unassigned thk123, peterschrammel and forejtv Jun 13, 2018

tautschnig added the blocker label Nov 10, 2018

tautschnig changed the title ~~Memory regression test~~ Memory regression test [blocks: #2035] Nov 10, 2018

TGWDB closed this May 19, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Memory regression test [blocks: #2035] #1971

Memory regression test [blocks: #2035] #1971

tautschnig commented Mar 25, 2018

chrisr-diffblue Mar 26, 2018

tautschnig Mar 26, 2018

chrisr-diffblue Mar 26, 2018

tautschnig Mar 26, 2018

chrisr-diffblue Mar 26, 2018

chrisr-diffblue Mar 26, 2018

tautschnig Mar 26, 2018

tautschnig commented Mar 26, 2018

chrisr-diffblue left a comment

tautschnig commented Mar 27, 2018

forejtv commented Apr 13, 2018

chrisr-diffblue commented Apr 13, 2018

tautschnig commented Apr 13, 2018

tautschnig commented Apr 18, 2018

NathanJPhillips left a comment

NathanJPhillips Apr 30, 2018

tautschnig Apr 30, 2018

chrisr-diffblue May 1, 2018

martin-cs left a comment

peterschrammel left a comment

TGWDB commented May 19, 2021

Memory regression test [blocks: #2035] #1971

Memory regression test [blocks: #2035] #1971

Conversation

tautschnig commented Mar 25, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Mar 26, 2018

chrisr-diffblue left a comment

Choose a reason for hiding this comment

tautschnig commented Mar 27, 2018

forejtv commented Apr 13, 2018

chrisr-diffblue commented Apr 13, 2018

tautschnig commented Apr 13, 2018

tautschnig commented Apr 18, 2018

NathanJPhillips left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

TGWDB commented May 19, 2021