Project

General

Profile

Actions
Copy link

Feature #9535

closed

Bug #6629: Used CIL is outdated

Increase memory limit for Frama-C (CIL)

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

Status:
Closed
Priority:
Urgent
Assignee:
Evgeny Novikov
Category:
Tasks generation
Target version:
3.0
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 open — 1 closed)

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

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Actions
Copy link
 #3

Updated by Evgeny Novikov over 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
Copy link
 #4

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 5 years ago

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

Updated by Evgeny Novikov over 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
Copy link
 #9

Updated by Evgeny Novikov over 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
Copy link
 #10

Updated by Evgeny Novikov over 5 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in c082518.

Actions
Copy link

Also available in: Atom PDF