Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002205Frama-CPlug-in > wppublic2016-02-01 20:352016-02-04 12:29
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in Version 
Summary0002205: zombie processes (again)
DescriptionThis is related #2154 and #2132. I have updated my Frama-C installation under OS X with a patch provided by Loïc Correnson. The situation has improved in the sense that my system is not so sluggish anymore but there still a substantial number of zombie processes: 86 (before the patch I counted 111 for the same example).
TagsNo tags attached.
Attached Files? file icon command.ml [^] (8,927 bytes) 2016-02-02 20:19 [Show Content]
? file icon command.mli [^] (5,915 bytes) 2016-02-02 20:19 [Show Content]
? file icon task.ml [^] (16,581 bytes) 2016-02-02 20:19 [Show Content]
? file icon task.mli [^] (8,951 bytes) 2016-02-02 20:19 [Show Content]

- Relationships

-  Notes
(0006144)
correnson (manager)
2016-02-02 09:18

Just to check, could you share your patched Command and Task modules from Frama-C kernel ?
(0006145)
jens (reporter)
2016-02-02 20:24

I have attached them (I had received them from you per email 27.11.2015)
(0006146)
jens (reporter)
2016-02-02 20:25
edited on: 2016-02-02 20:26

Here some output of 'ps' while running Frama-C/WP jens 50320 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50306 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50142 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50307 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50334 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50335 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50327 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50321 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50328 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50128 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50313 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50314 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50299 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50300 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50285 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50286 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50078 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50234 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50235 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50070 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50227 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50228 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50062 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50177 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50178 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50170 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50171 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50163 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50164 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50156 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50157 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50149 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50150 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50143 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50135 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50136 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50121 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50122 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50114 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50115 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50107 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50108 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50080 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (coqtop.opt) jens 50100 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50072 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (coqtop.opt) jens 50101 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50064 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (coqtop.opt) jens 50093 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50094 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50086 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (why3prove) jens 50087 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50079 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 50071 0,0 0,0 0 0 s000 Z+ 8:17pm 0:00.00 (alt-ergo) jens 49976 0,0 0,0 0 0 s000 Z+ 8:16pm 0:00.00 (coqtop.opt) jens 49745 0,0 0,0 0 0 s000 Z+ 8:16pm 0:00.00 (why3prove) jens 49747 0,0 0,0 0 0 s000 Z+ 8:16pm 0:00.00 (coqtop.opt) jens 49746 0,0 0,0 0 0 s000 Z+ 8:16pm 0:00.00 (alt-ergo) jens 49524 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (why3prove) jens 49550 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (coqtop.opt) jens 49542 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (coqtop.opt) jens 49534 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (coqtop.opt) jens 49526 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (coqtop.opt) jens 49548 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (why3prove) jens 49549 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (alt-ergo) jens 49540 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (why3prove) jens 49541 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (alt-ergo) jens 49532 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (why3prove) jens 49533 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (alt-ergo) jens 49525 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (alt-ergo) jens 49321 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (alt-ergo) jens 49322 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (coqtop.opt) jens 49320 0,0 0,0 0 0 s000 Z+ 8:15pm 0:00.00 (why3prove)
(0006152)
correnson (manager)
2016-02-04 12:29

Thanks Jens for the output. I identified the problem, which is due to a race between parallel run of several provers. I'm working on a new patch.

- Issue History
Date Modified Username Field Change
2016-02-01 20:35 jens New Issue
2016-02-01 20:35 jens Status new => assigned
2016-02-01 20:35 jens Assigned To => correnson
2016-02-02 09:18 correnson Note Added: 0006144
2016-02-02 09:18 correnson Status assigned => feedback
2016-02-02 20:19 jens File Added: command.ml
2016-02-02 20:19 jens File Added: command.mli
2016-02-02 20:19 jens File Added: task.ml
2016-02-02 20:19 jens File Added: task.mli
2016-02-02 20:24 jens Note Added: 0006145
2016-02-02 20:24 jens Status feedback => assigned
2016-02-02 20:25 jens Note Added: 0006146
2016-02-02 20:26 jens Note Edited: 0006146 View Revisions
2016-02-04 12:29 correnson Note Added: 0006152
2016-02-04 12:29 correnson Status assigned => confirmed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker