Project

General

Profile

Actions

Bug #7175

closed

Potential hang of Klever

Added by Vitaly Mordan about 8 years ago. Updated almost 8 years ago.

Status:
Closed
Priority:
Immediate
Category:
*Abstract tasks generation
Target version:
-
Start date:
05/05/2016
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
3810fb2

Description

Sometimes Klever is hanging for a few minutes while solving verification tasks in the following way:

...
2016-05-05 01:39:51 (separated.py:149) SBK INFO> Status of verification task "11538" is "PROCESSING"
2016-05-05 01:39:52 (separated.py:149) SBK INFO> Status of verification task "11538" is "PROCESSING"
2016-05-05 01:39:53 (separated.py:149) SBK INFO> Status of verification task "11538" is "FINISHED"
2016-05-05 01:39:53 (separated.py:174) SBK INFO> Verification task was successfully decided
2016-05-05 01:39:53 (common.py:160) SBK INFO> Verification task decision status is "safe"
2016-05-05 01:39:53 (components.py:119) SBK INFO> Terminate child resources message queue
...
After a few minutes Klever starts to solve new verification tasks.

Note: SBK is ABKM


Files

avtg_log (408 KB) avtg_log Vitaly Mordan, 05/25/2016 04:39 PM
core_log (432 KB) core_log Vitaly Mordan, 05/25/2016 04:39 PM
vtg_log (45.5 KB) vtg_log Vitaly Mordan, 05/25/2016 04:39 PM
core_log (1.8 KB) core_log Vitaly Mordan, 05/30/2016 02:12 PM
avtg_log (1.12 KB) avtg_log Vitaly Mordan, 05/30/2016 02:12 PM
lkbce_log (815 Bytes) lkbce_log Vitaly Mordan, 05/30/2016 02:12 PM
vtg_log (285 Bytes) vtg_log Vitaly Mordan, 05/30/2016 02:12 PM
lkvog_log (5.42 MB) lkvog_log Vitaly Mordan, 05/30/2016 02:12 PM
avtg_log (2.51 KB) avtg_log Vitaly Mordan, 05/31/2016 06:04 PM
sa_log (23.4 KB) sa_log Vitaly Mordan, 05/31/2016 06:04 PM
emg_log (631 Bytes) emg_log Vitaly Mordan, 05/31/2016 06:04 PM
core_log (8.46 KB) core_log Vitaly Mordan, 05/31/2016 06:14 PM
log (3.07 MB) log Vitaly Mordan, 06/01/2016 07:00 PM

Related issues 3 (0 open3 closed)

Blocked by Klever - Feature #6615: Automatically push and pop abstract verification task descriptionClosedEvgeny Novikov01/29/2016

Actions
Blocks Klever - Feature #7432: Allow to verify all rule specifications together by using multi-aspect verificationClosedVitaly Mordan07/28/2016

Actions
Blocks Klever - Feature #7392: Support groupping of rule specifications to be checked togetherClosedEvgeny Novikov06/24/201606/24/2016

Actions
Actions #1

Updated by Vitaly Mordan about 8 years ago

One instance of CPAchecker is hanging for 1 day.

Actions #2

Updated by Vitaly Mordan about 8 years ago

It looks like it always happens after

<component> INFO> Terminate child resources message queue.

Actions #3

Updated by Evgeny Novikov about 8 years ago

  • Assignee deleted (Evgeny Novikov)

I don't see such behavior in master. It was likely introduced in branch mav and I am not responsible for that.

Actions #4

Updated by Evgeny Novikov almost 8 years ago

  • Category set to *Abstract tasks generation
  • Status changed from New to Feedback
  • Assignee set to Vitaly Mordan
  • Priority changed from Normal to Urgent

At the moment we have a suggestion that this hang may be related with the buggy implementation of queues provided by Python package multiprocessing. It is likely just for queues used for AVTG plugins to share abstract verification tasks.

Vitaly tries to use Manager queues. Let's see whether it will help.

Actions #5

Updated by Vitaly Mordan almost 8 years ago

This issue is still present with 2 Managers (AVTG and component).
Branch master (8f3282f9ea28c45eec8b56d3d75b032c9c4847cf).

Actions #6

Updated by Evgeny Novikov almost 8 years ago

Please, attach log files of Core, AVTG, VTG and corresponding ABKM that hangs.

Besides please try the last master since these hangs can be due to EMG could prepare some environment models for a very-very long time, thus VTG/ABKMs just have nothing to do.

Updated by Vitaly Mordan almost 8 years ago

ABKM log:

2016-05-25 12:59:29 (init.py:148) ABKM INFO> Status of verification task "97" is "PROCESSING"
2016-05-25 12:59:30 (init.py:148) ABKM INFO> Status of verification task "97" is "PROCESSING"
2016-05-25 12:59:31 (init.py:148) ABKM INFO> Status of verification task "97" is "PROCESSING"
2016-05-25 12:59:32 (init.py:148) ABKM INFO> Status of verification task "97" is "FINISHED"
2016-05-25 12:59:32 (init.py:173) ABKM INFO> Verification task was successfully decided
2016-05-25 12:59:32 (init.py:206) ABKM INFO> Verification task decision status is "unknown"
2016-05-25 12:59:32 (init.py:421) ABKM INFO> Remove verification task "97"
2016-05-25 12:59:32 (components.py:119) ABKM INFO> Terminate child resources message queue

I am using branch from master revision 8f3282f9ea28c45eec8b56d3d75b032c9c4847cf.
Master revision 9814cdfa4fe82b1b20fc43f6fcfcdee7eedfce1b fails on tests.

Actions #8

Updated by Evgeny Novikov almost 8 years ago

  • Status changed from Feedback to Rejected
  • Assignee deleted (Vitaly Mordan)

Yes, as I expected EMG likely hangs on module fs/cifs/cifs.ko (see the tail of the AVTG log).

You need to use at least v0.1rc1 that includes very many EMG performance fixes.

Why the last commit in master fails on tests? Where the appropriate issue?

Updated by Vitaly Mordan almost 8 years ago

This issue is still present with 2 Managers in the latest master.
Klever hangs after a few minutes of processing a task.

Actions #10

Updated by Evgeny Novikov almost 8 years ago

  • Status changed from Rejected to Feedback
  • Assignee set to Evgeny Novikov

Please, restart the job with a higher debugging level (e.g. with the development mode) and attach the RSG log file likely located in avtg/block/deadline-iosched.ko/linux:crypto:context2/rsg/log.

Updated by Vitaly Mordan almost 8 years ago

RSG component was not started (only SA and EMG).

Actions #12

Updated by Vitaly Mordan almost 8 years ago

Actions #13

Updated by Evgeny Novikov almost 8 years ago

It is very strange. Now it hangs immediately after the second AVTG plugin (EMG) starts. I didn't observe this behaviour anywhere. Perhaps you have some changes against the master branch. Please, revert all of them and try pure master.

Actions #14

Updated by Vitaly Mordan almost 8 years ago

I reverted the changes with Managers (2 Managers were added in AVTG and component in order to prevent such hangs) and so far could not reproduce this issue.
But now Klever hangs on tests, probably, in a similar way.

Actions #15

Updated by Evgeny Novikov almost 8 years ago

Through the attached log file I can't understand what hangs. Whether all tests passed and Core hangs at the end? Or it hangs somewhere in the middle? Please, attach at least log files of LKBCE, LKVOG, AVTG and VTG. Besides last log files of AVTG plugins and ABKM are welcome.

Actions #16

Updated by Evgeny Novikov almost 8 years ago

Moreover, one more time I would like to note that log level INFO can't help much when detecting issues. Use the DEBUG one.

Actions #17

Updated by Evgeny Novikov almost 8 years ago

  • Category deleted (*Abstract tasks generation)
  • Assignee deleted (Evgeny Novikov)
  • Priority changed from Urgent to Normal

No feedback during 5 days for the issue considered urgent. Besides it is still unknown where is the problem if so.

Actions #18

Updated by Evgeny Novikov almost 8 years ago

  • Category set to *Abstract tasks generation
  • Priority changed from Normal to Urgent

I also observed likely the same hang up when one of AVTG plugins infinitely waits for an abstract verification description from a corresponding message queue.

I think that this can be a race between AVTG plugins and AVTG itself that periodically checks that plugins put the updated abstract verification task description back to the same queue if they terminate successfully (but very-very rarely they can even be unstarted yet).

Instead of implementing more and more "advanced" checks I would like to #6615 that suggests completely another approach.

Actions #19

Updated by Evgeny Novikov almost 8 years ago

Please, try master after 911b496 - there this hang up was likely fixed.

Actions #20

Updated by Evgeny Novikov almost 8 years ago

  • Status changed from Feedback to Rejected

Several times all modules of the Linux kernel were verified against different rules. Thus the issue finally has gone.

Actions #21

Updated by Vitaly Mordan almost 8 years ago

  • Priority changed from Urgent to Immediate

This issue is still present in the latest master (3 big experiments failed).
Until it will be resolved all other big experiments are pointless.

Actions #22

Updated by Evgeny Novikov almost 8 years ago

  • Status changed from Rejected to Closed
  • Assignee set to Evgeny Novikov
  • Published in build set to 3810fb2

I hope that 3810fb2 finally fixes these issues since it eventually gets rid of queues for passing abstract verification task descriptions between AVTG and its plugins.

For other hang-ups open other issues please.

Actions

Also available in: Atom PDF