Project

General

Profile

Feature #7470

Add support for user-oriented time limit

Added by Evgeny Novikov over 3 years ago. Updated over 1 year ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
-
Target version:
Start date:
08/15/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

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).


Related issues

Related to Klever - Feature #8446: Fix and improve progress reportingClosed10/10/2017

Actions
Has duplicate Klever - Feature #7471: Allow to specify resource limitations for the whole taskRejected08/08/201608/08/2016

Actions
Blocked by Klever - Feature #6614: Intellectual schedulingClosed01/29/2016

Actions

History

#1

Updated by Evgeny Novikov about 3 years ago

  • Priority changed from High to Urgent

We need to think about this.

#2

Updated by Evgeny Novikov almost 3 years ago

  • Priority changed from Urgent to High

Let's postpone all advanced features since we have very much more important and obvious ones now.

#3

Updated by Evgeny Novikov about 2 years ago

  • 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.

#4

Updated by Evgeny Novikov over 1 year ago

  • 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.

#5

Updated by Ilja Zakharov over 1 year ago

  • Status changed from New to Resolved

Implemented in 6614-speculative-scheduling.

#6

Updated by Ilja Zakharov over 1 year ago

  • Status changed from Resolved to Open

Long-running instance showed that there is room for necessary improvement.

#7

Updated by Ilja Zakharov over 1 year ago

  • Status changed from Open to Resolved

Fixed.

#8

Updated by Ilja Zakharov over 1 year ago

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.

#9

Updated by Evgeny Novikov over 1 year ago

  • 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