Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002262Frama-CPlug-in > wppublic2016-12-15 21:182016-12-16 11:56
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilitysometimes
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002262: more prover processes run than expected
DescriptionWhen I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
Steps To Reproducerun WP on example with a sufficiently large number of proof obligations that require more than one theorem prover
Additional InformationI 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.
TagsNo tags attached.
Attached Filespng file icon screen-shot.png [^] (345,355 bytes) 2016-12-16 10:08

- Relationships

-  Notes
(0006320)
correnson (manager)
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 (reporter)
2016-12-16 10:08

The screen shot shows that six provers are running. However, WP was started with '-wp-par 4'
(0006323)
correnson (manager)
2016-12-16 11:56

Thanks for the screenshot, this will help !

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker