Frama-C Bug Tracking System - Frama-C
View Issue Details
0002262Frama-CPlug-in > wppublic2016-12-15 21:182016-12-16 11:56
jens 
correnson 
normalminorsometimes
assignedopen 
Frama-C 14-Silicon 
 
0002262: more prover processes run than expected
When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover
I am not sure this is related but: It happens from time to time that a proof obligations that is verified with '-wp-par 1' and given timeout T is not verified when using a greater number of processes and the same timeout T.
No tags attached.
png screen-shot.png (345,355) 2016-12-16 10:08
https://bts.frama-c.com/file_download.php?file_id=1128&type=bug
Issue History
2016-12-15 21:18jensNew Issue
2016-12-15 21:18jensStatusnew => assigned
2016-12-15 21:18jensAssigned To => correnson
2016-12-16 09:39corrensonNote Added: 0006320
2016-12-16 10:08jensNote Added: 0006321
2016-12-16 10:08jensFile Added: screen-shot.png
2016-12-16 11:56corrensonNote Added: 0006323

Notes
(0006320)
correnson   
2016-12-16 09:39   
This is a very strange behavior indeed. I never see that before and I can not even understand how it is possible. When using several theorem provers, we actually schedule several proof task in parallel, but only `-wp-par N` task are actually started simultaneously. Maybe some tasks are actually started on creation, rather that delayed until explicitly started by the scheduler. Thanks for the report. Regarding timeout, it is a known issue. Timeout is observed from the Frama-C scheduler point of view, not from each individual process. Hence, it is « shared » among the various processes running in parallel. Depending on how many cores are actually running provers, you might increase or decrease the global timeout. We plan to actually use a more process-based timeout control. We also plan to include memory control. But this requires system-dependent C-code routines.
(0006321)
jens   
2016-12-16 10:08   
The screen shot shows that six provers are running. However, WP was started with '-wp-par 4'
(0006323)
correnson   
2016-12-16 11:56   
Thanks for the screenshot, this will help !