Project

General

Profile

Feature #9535

Bug #6629: Used CIL is outdated

Increase memory limit for Frama-C (CIL)

Added by Evgeny Novikov 2 months ago. Updated about 2 months ago.

Status:
Closed
Priority:
Urgent
Category:
Tasks generation
Target version:
Start date:
03/13/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Unfortunately it seems that Frama-C (CIL) needs much more memory than previously used CIL. Maybe 1 GB instead of 300 MB will be enough to have the same results. Also we need to increase the default memory limit for deciding verification jobs.


Related issues

Related to Deductive Verification Tools for Linux Kernel - Feature #9538: Reduce memory consumption by Frama-C (CIL)Closed03/13/2019

Actions

History

#1

Updated by Evgeny Novikov 2 months ago

  • Related to Feature #9538: Reduce memory consumption by Frama-C (CIL) added
#2

Updated by Evgeny Novikov 2 months ago

Perhaps, we will not need this if #9538 will shoot.

#3

Updated by Evgeny Novikov 2 months ago

  • Status changed from New to Open

I did both in branch frama-c-cil. But in one case it did not help. Let's wait for #9538 since too greedy CIL is not good.

#4

Updated by Evgeny Novikov 2 months ago

  • Related to deleted (Feature #9538: Reduce memory consumption by Frama-C (CIL))
#5

Updated by Evgeny Novikov 2 months ago

  • Blocked by Feature #9538: Reduce memory consumption by Frama-C (CIL) added
#6

Updated by Evgeny Novikov 2 months ago

  • Blocked by deleted (Feature #9538: Reduce memory consumption by Frama-C (CIL))
#7

Updated by Evgeny Novikov 2 months ago

  • Related to Feature #9538: Reduce memory consumption by Frama-C (CIL) added
#8

Updated by Evgeny Novikov 2 months ago

  • Status changed from Open to Resolved

One more iteration helped. Unfortunately, Frama-C (CIL) needs very much RAM for merging some source files. At the moment the limit is 2 GB rather than 300 MB as it was for CIL. Job limits start from 3 GB and they are 5 GB even for jobs that have only 2 parallel task generators and one sub-job worker of course. Nevertheless for simple tests one can use much more aggressive parallelism.

#9

Updated by Evgeny Novikov 2 months ago

After Mikhail made considerable optimizations (#9538) I reduced the CIL memory limit from 2 GB to 1 GB. I didn't change job limits, since specified values seem to be much better.

#10

Updated by Evgeny Novikov about 2 months ago

  • Status changed from Resolved to Closed

I merged the branch to master in c082518.

Also available in: Atom PDF