Project

General

Profile

Actions
Copy link

Bug #7037

closed

EMG became too greedy

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

Status:
Closed
Priority:
Immediate
Assignee:
Ilja Zakharov
Category:
Environment models
Target version:
-
Start date:
04/06/2016
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
3d22042

Description

Recent changes in EMG or/and environment model specifications likely from branch interface-categories-fixes leads to EMG started to consume much more memory. Before 1 GB was enough for Core including EMG to complete all jobs. Now 2 GB isn't enough sometimes and maybe there is not any reasonable memory limit for Core any more.

Particular cases:
  • From the validation set:
        {
      "Linux kernel": {
        "Git repository": {"commit": "44f694330e1e~"},
        "modules": ["net/sunrpc/sunrpc.ko"]
      },
      "rule specifications": ["linux:module"],
      "ideal verdict": "unsafe",
      "comment": "<a href='https://forge.ispras.ru/issues/6560'>Bug #6560</a>" 
    }
  • Module drivers/target/target_core_mod.ko of Linux 3.5 against rule specification linux:module. 2 GB was hit when EMG tried to generate states for at least about 60000 automata.

Since this issue breaks too much it should be fixed ASAP.

Please, ensure that after fixes at least the whole validation set will pass and the pointed particular module will be successfully verified given just 1 GB as it was before.

Actions
Copy link

Also available in: Atom PDF