Bug #7175
closedPotential hang of Klever
Added by Vitaly Mordan about 8 years ago. Updated almost 8 years ago.
0%
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 |
Updated by Vitaly Mordan about 8 years ago
One instance of CPAchecker is hanging for 1 day.
Updated by Vitaly Mordan about 8 years ago
It looks like it always happens after
<component> INFO> Terminate child resources message queue.
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.
Updated by Evgeny Novikov about 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.
Updated by Vitaly Mordan about 8 years ago
This issue is still present with 2 Managers (AVTG and component).
Branch master (8f3282f9ea28c45eec8b56d3d75b032c9c4847cf).
Updated by Evgeny Novikov about 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 about 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.
Updated by Evgeny Novikov about 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 about 8 years ago
- File avtg_log avtg_log added
- File core_log core_log added
- File lkbce_log lkbce_log added
- File lkvog_log lkvog_log added
- File vtg_log vtg_log added
This issue is still present with 2 Managers in the latest master.
Klever hangs after a few minutes of processing a task.
Updated by Evgeny Novikov about 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 about 8 years ago
RSG component was not started (only SA and EMG).
Updated by Evgeny Novikov about 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.
Updated by Vitaly Mordan about 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.
Updated by Evgeny Novikov about 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.
Updated by Evgeny Novikov about 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.
Updated by Evgeny Novikov about 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.
Updated by Evgeny Novikov about 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.
Updated by Evgeny Novikov about 8 years ago
Please, try master after 911b496 - there this hang up was likely fixed.
Updated by Evgeny Novikov about 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.
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.
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.