https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692019-03-13T07:20:11ZOpen-Source ProjectsDeductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357532019-03-13T07:20:11ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Related to</strong> <i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed child" href="/issues/9535">Feature #9535</a>: Increase memory limit for Frama-C (CIL)</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357612019-03-13T12:22:55ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Related to</strong> deleted (<i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed child" href="/issues/9535">Feature #9535</a>: Increase memory limit for Frama-C (CIL)</i>)</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357622019-03-13T12:22:59ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Blocks</strong> <i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed child" href="/issues/9535">Feature #9535</a>: Increase memory limit for Frama-C (CIL)</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357752019-03-14T07:10:48ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6321">fvtp.tar.gz</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6321/fvtp.tar.gz">fvtp.tar.gz</a> added</li></ul><p>For the attached input source files Frama-C (CIL) needs more than 1 GB or RAM on the following command:<br /><pre>
toplevel.opt "-no-autoload-plugins" "-no-findlib" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_ib_media.abs-paths.trimmed.i" ".tmp_msg.abs-paths.trimmed.i" ".tmp_node.abs-paths.trimmed.i" ".tmp_handler.abs-paths.trimmed.i" ".tmp_bcast.abs-paths.trimmed.i" ".tmp_node_subscr.abs-paths.trimmed.i" ".tmp_ref.abs-paths.trimmed.i" ".tmp_discover.abs-paths.trimmed.i" ".tmp_port.abs-paths.trimmed.i" ".tmp_server.abs-paths.trimmed.i" ".tmp_net.abs-paths.trimmed.i" ".tmp_config.abs-paths.trimmed.i" ".tmp_socket.abs-paths.trimmed.i" ".tmp_name_distr.abs-paths.trimmed.i" ".tmp_core.abs-paths.trimmed.i" ".tmp_bearer.abs-paths.trimmed.i" ".tmp_log.abs-paths.trimmed.i" ".tmp_subscr.abs-paths.trimmed.i" ".tmp_link.abs-paths.trimmed.i" ".tmp_name_table.abs-paths.trimmed.i" ".tmp_sysctl.abs-paths.trimmed.i" ".tmp_eth_media.abs-paths.trimmed.i" ".tmp_netlink.abs-paths.trimmed.i" ".tmp_addr.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "spinlock.bk.abs-paths.trimmed.i" "bug kind funcs.trimmed.i"
</pre></p>
<p>CIL 1.5.1 needed less than 140 MB of RAM.</p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357842019-03-14T15:23:37ZMikhail Mandrykinmandrykin@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6325">screenshot-spacetime.png</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6325/screenshot-spacetime.png">screenshot-spacetime.png</a> added</li></ul><p>I tried to investigate the allocation profile of Frama-C on a subset of the attached files with <a href="https://caml.inria.fr/pub/docs/manual-ocaml/spacetime.html" class="external">Spacetime</a> (Spacetime incurs a very large memory overhead, so when the uninstrumented program takes ~1GB of RAM with spacetime it takes ~14GB and processing the collected profile takes more than 16GB and was unsuccessful on my machine, so I profiled for a small subset of files). Unfortunately, I couldn't discover any outstanding culprit. Here's an example of the profile:<br /><img src="https://forge.ispras.ru/attachments/download/6325/screenshot-spacetime.png" alt="" loading="lazy" /><br />The only suspicious blue stripe (in the center, the bottom one is for unknown allocation source, e.g. in the C bindings) is from varinfos (various data attached to variable definitions e.g. type, location, scope etc.), another light green stripe is from various locations i.e. source code location data attached to expressions, statements, variable definitions etc. Removing location information from expressions (CIL dosn't keep it and uses per-statement granularity) only reduces memory footprint by 100-200M on this set of files. There's also an option "<code>-agressive-merging</code>", which enables merging more similar function and composite type definitions and reduces memory consumption by ~50M in this case. But a larger gain in reducing the memory overhead can likely be achieved only by more drastic changes across the entire Frama-C codebase such as removing some data kept for variable definitions and functions, removing some internal caches etc.</p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357852019-03-14T15:39:14ZMikhail Mandrykinmandrykin@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6326">screenshot-spacetime2.png</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6326/screenshot-spacetime2.png">screenshot-spacetime2.png</a> added</li></ul><p>Another profile:<br /><img src="https://forge.ispras.ru/attachments/download/6326/screenshot-spacetime2.png" alt="" loading="lazy" /><br />Again, the widest stripes are for exprs (upper pale grayish violet), varinfos (lower pale grayish violet), locations (gray), statement chunks (in code blocks) (upper light gray) and call argument lists (lower light gray)</p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357892019-03-15T05:51:27ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Thank you for your investigations. I hope that this was a good experience for you!</p>
<p>Even initially I didn't expect much in this direction, so, I opened the issue with priority "High". Since it seems that optimizations cost much we should adopt the current state as is.</p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357902019-03-15T05:51:43ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Blocks</strong> deleted (<i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed child" href="/issues/9535">Feature #9535</a>: Increase memory limit for Frama-C (CIL)</i>)</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=357932019-03-15T05:51:49ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Related to</strong> <i><a class="issue tracker-4 status-5 priority-6 priority-high2 closed child" href="/issues/9535">Feature #9535</a>: Increase memory limit for Frama-C (CIL)</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=358012019-03-15T07:23:17ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6327">weaver.tar.gz</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6327/weaver.tar.gz">weaver.tar.gz</a> added</li></ul><p>My observation regarding this issue is that for most even quite large source files Frama-C (CIL) does not need very much memory (you can find examples attached to other issues), but in some cases it is very greedy. Surprisingly they all are Linux loadable kernel modules from file system and networking subsystems that have quite many source files (they are prefixed with ".tmp_" in source file archives). But the number of source files does not matter much. I attached another example with a driver having many source files as well, but it is from the sound subsystem and Frama-C (CIL) didn't need very much memory to process it. Thus, there are some specific things in sources for which Frama-C (CIL) consumes very much memory.</p>
<p>Frama-C (CIL) command for the attached archive:<br /><pre>
toplevel.opt "-no-autoload-plugins" "-no-findlib" "-machdep" "gcc_x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_emumpu401.abs-paths.i" ".tmp_emu10k1_main.abs-paths.i" ".tmp_p16v.abs-paths.i" ".tmp_emuproc.abs-paths.i" ".tmp_emu10k1_patch.abs-paths.i" ".tmp_emufx.abs-paths.i" ".tmp_irq.abs-paths.i" ".tmp_emu10k1_callback.abs-paths.i" ".tmp_emu10k1.abs-paths.i" ".tmp_io.abs-paths.i" ".tmp_emu10k1_synth.abs-paths.i" ".tmp_timer.abs-paths.i" ".tmp_voice.abs-paths.i" ".tmp_memory.abs-paths.i" ".tmp_emumixer.abs-paths.i" ".tmp_emupcm.abs-paths.i" "atomic.abs-paths.i" "dd.abs-paths.i" "spi.abs-paths.i" "err.abs-paths.i" "panic.abs-paths.i" "common.abs-paths.i" "slab.abs-paths.i" "memory.abs-paths.i" "gcc.abs-paths.i" "nondet.abs-paths.i" "reference memory.abs-paths.i" "environment_model.abs-paths.i" "spinlock.bk.abs-paths.i"
</pre></p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=358162019-03-15T18:15:29ZMikhail Mandrykinmandrykin@ispras.ru
<ul></ul>Actually it turned out to be possible to reduce memory consumption on this example down to ~500M by
<ul>
<li>using purely sequential handling of input files so that the CABS ASTs of the previous files can be collected by GC when handling succeeding files</li>
<li>removing unexported and unused function definitions (<code>static</code> and <code>inline</code>) local to a file earlier before merging</li>
</ul>
<p>Implemented these optimizations in <a href="https://forge.ispras.ru/projects/astraver/repository/framac/revisions/9c08d509dbb34ed39aeb2253fee9b57ab6749f26" class="external">9c08d509</a>. Sequential parsing is activated by option "<code>-no-annot</code>" that also deactivates annotation handling (specifications), I also used "<code>-aggressive-merging</code>" to further reduce the size of the resulting merged Cil file</p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=358192019-03-17T08:37:08ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Great! After your optimizations I could reduce the memory limit for Frama-C (CIL) from 2 GB back to 1 GB and we will not have many different memory issues in Klever.</p>
<p>Instead of awful 1.6 GB of RAM at Klever validation set, Frama-C (CIL) needs only 550 MB. This is still more than old CIL (170 MB) but not in an order.</p>
<p>Please, close the issue.</p> Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)https://forge.ispras.ru/issues/9538?journal_id=358322019-03-18T10:05:22ZMikhail Mandrykinmandrykin@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Closed</i></li></ul>