Project

General

Profile

Actions

Feature #9538

closed

Reduce memory consumption by Frama-C (CIL)

Added by Evgeny Novikov over 5 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
High
Start date:
03/13/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

As you can see at #9519 Frama-C (CIL) consumes much more memory that pure CIL. For normal use cases of Frama-C this does not matter, but in the CIL mode it is not welcome.


Files

fvtp.tar.gz (7.52 MB) fvtp.tar.gz Evgeny Novikov, 03/14/2019 10:07 AM
screenshot-spacetime.png (655 KB) screenshot-spacetime.png Mikhail Mandrykin, 03/14/2019 06:06 PM
screenshot-spacetime2.png (657 KB) screenshot-spacetime2.png Mikhail Mandrykin, 03/14/2019 06:34 PM
weaver.tar.gz (3.53 MB) weaver.tar.gz Evgeny Novikov, 03/15/2019 10:21 AM

Related issues 1 (0 open1 closed)

Related to Klever - Feature #9535: Increase memory limit for Frama-C (CIL)ClosedEvgeny Novikov03/13/2019

Actions
Actions #1

Updated by Evgeny Novikov over 5 years ago

  • Related to Feature #9535: Increase memory limit for Frama-C (CIL) added
Actions #2

Updated by Evgeny Novikov over 5 years ago

  • Related to deleted (Feature #9535: Increase memory limit for Frama-C (CIL))
Actions #3

Updated by Evgeny Novikov over 5 years ago

  • Blocks Feature #9535: Increase memory limit for Frama-C (CIL) added
Actions #4

Updated by Evgeny Novikov over 5 years ago

For the attached input source files Frama-C (CIL) needs more than 1 GB or RAM on the following command:

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" 

CIL 1.5.1 needed less than 140 MB of RAM.

Actions #5

Updated by Mikhail Mandrykin over 5 years ago

I tried to investigate the allocation profile of Frama-C on a subset of the attached files with Spacetime (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:

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 "-agressive-merging", 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.

Actions #6

Updated by Mikhail Mandrykin over 5 years ago

Another profile:

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)

Actions #7

Updated by Evgeny Novikov over 5 years ago

Thank you for your investigations. I hope that this was a good experience for you!

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.

Actions #8

Updated by Evgeny Novikov over 5 years ago

  • Blocks deleted (Feature #9535: Increase memory limit for Frama-C (CIL))
Actions #9

Updated by Evgeny Novikov over 5 years ago

  • Related to Feature #9535: Increase memory limit for Frama-C (CIL) added
Actions #10

Updated by Evgeny Novikov over 5 years ago

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.

Frama-C (CIL) command for the attached archive:

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" 

Actions #11

Updated by Mikhail Mandrykin over 5 years ago

Actually it turned out to be possible to reduce memory consumption on this example down to ~500M by
  • 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
  • removing unexported and unused function definitions (static and inline) local to a file earlier before merging

Implemented these optimizations in 9c08d509. Sequential parsing is activated by option "-no-annot" that also deactivates annotation handling (specifications), I also used "-aggressive-merging" to further reduce the size of the resulting merged Cil file

Actions #12

Updated by Evgeny Novikov over 5 years ago

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.

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.

Please, close the issue.

Actions #13

Updated by Mikhail Mandrykin over 5 years ago

  • Status changed from New to Closed
Actions

Also available in: Atom PDF