|Anonymous | Login | Signup for a new account||2019-08-17 13:52 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002262||Frama-C||Plug-in > wp||public||2016-12-15 21:18||2016-12-16 11:56|
|Product Version||Frama-C 14-Silicon|
|Target Version||Fixed in Version|
|Summary||0002262: more prover processes run than expected|
|Description||When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.|
|Steps To Reproduce||run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover|
|Additional Information||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.
|Tags||No tags attached.|
|Attached Files||screen-shot.png [^] (345,355 bytes) 2016-12-16 10:08|
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.
|The screen shot shows that six provers are running. However, WP was started with '-wp-par 4'|
|Thanks for the screenshot, this will help !|
|2016-12-15 21:18||jens||New Issue|
|2016-12-15 21:18||jens||Status||new => assigned|
|2016-12-15 21:18||jens||Assigned To||=> correnson|
|2016-12-16 09:39||correnson||Note Added: 0006320|
|2016-12-16 10:08||jens||Note Added: 0006321|
|2016-12-16 10:08||jens||File Added: screen-shot.png|
|2016-12-16 11:56||correnson||Note Added: 0006323|
|Copyright © 2000 - 2019 MantisBT Team|