Feature #7470
closed
Add support for user-oriented time limit
Added by Evgeny Novikov over 8 years ago.
Updated over 6 years ago.
Description
Copied from https://forge.ispras.ru/issues/7453#note-6
A CPU limit PER 1 rule PER 1 module PER 1 entry point is not a resource limit but a kind of Quality of Service limit.
It represents in some implicit way a minimal limit for quality of verification.
The actual resource limit from user perspective is a time limit for the whole task (e.g. 1 day for analysis of all drivers for all rules). Currently, we set this limit to value "as soon as possible as long as QoS is achieved".
In general, resource limit and QoS limit can be set simultaneously, while one of them may have higher priority than another one.
Typically QoS limit would have higher priority.
Another observation. QoS limit is more important for massive tasks, while resource limit may be more important for small tasks (e.g. if you run verification task for weekend, there are no benefits to have results on Saturday evening, tools can spend one more day to achieve better results).
- Priority changed from High to Urgent
We need to think about this.
- Priority changed from Urgent to High
Let's postpone all advanced features since we have very much more important and obvious ones now.
- Subject changed from Add support for Quality of Service limit to Add support for user-oriented time limit
- Assignee set to Ilja Zakharov
- Priority changed from High to Urgent
- Target version set to 2.0
When abstracting from reliable experiments and benchmarks, this is an obvious feature for static verification of real software by real users.
Without no doubts this feature is closely related with #8149 which will be available since Klever 0.3.
- Target version changed from 2.0 to 1.1
This issue is not strictly bound with purposes of 2.0 that targets verification of C software.
- Status changed from New to Resolved
Implemented in 6614-speculative-scheduling.
- Status changed from Resolved to Open
Long-running instance showed that there is room for necessary improvement.
- Status changed from Open to Resolved
User oriented time limit is intended to solve as much tasks successfully as possible. It means that if a user has not enough time then he should consider reduce resources for tasks or reduce number of drivers or rules. But if he or she has more time then it is necessary for the solution then he can set option 'wall time limit' in job.json and set how much time it is safe to spend on solving the job. For instance, if the option is set to value 4 hours and Klever can solve all tasks in 3 hours it will spend an extra hour to solve timeout tasks.
Each timeout task will be solved with an increased CPU time limit. On each solution Klever will add 20% time more by default or a user can set an option 'min increaded limit' (float, to set increase step to 50% set the value '1.5').
Notice, that rescheduling of timeout tasks always happens when all tasks are solved at least once and there is enough time left to do rescheduling.
- Status changed from Resolved to Closed
CI doesn't test this, ditto I am. So, I just merged the branch to master in aa70aed85.
Also available in: Atom
PDF