Project

General

Profile

Actions

Feature #9535

closed

Bug #6629: Used CIL is outdated

Increase memory limit for Frama-C (CIL)

Added by Evgeny Novikov about 5 years ago. Updated about 5 years 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 1 (0 open1 closed)

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

Actions
Actions #1

Updated by Evgeny Novikov about 5 years ago

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

Updated by Evgeny Novikov about 5 years ago

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

Actions #3

Updated by Evgeny Novikov about 5 years 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.

Actions #4

Updated by Evgeny Novikov about 5 years ago

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

Updated by Evgeny Novikov about 5 years ago

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

Updated by Evgeny Novikov about 5 years ago

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

Updated by Evgeny Novikov about 5 years ago

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

Updated by Evgeny Novikov about 5 years 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.

Actions #9

Updated by Evgeny Novikov about 5 years 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.

Actions #10

Updated by Evgeny Novikov about 5 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in c082518.

Actions

Also available in: Atom PDF