Project

General

Profile

Feature #6614

Intellectual scheduling

Added by Evgeny Novikov over 3 years ago. Updated 12 months ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Scheduling
Target version:
Start date:
01/29/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Sometimes scheduling can be done more intellectually, e.g. we can try to solve more tasks with initially lower memory limits and re-solve them one or more times (there can be an option) if they meet memory limit. Since it depends on specifics of verification tasks to be solved (e.g. testing verification tasks require very few resources while complicated rule specifications likely require the most of them) it is better to implement this scheduling within VTG.


Related issues

Related to Klever - Feature #9167: Track speculative wall and CPU timeNew07/26/2018

Actions
Blocks Klever - Feature #7470: Add support for user-oriented time limitClosed08/15/2016

Actions
Blocked by Klever - Feature #8489: Show computational resources consumed by verifier in tables with safes/unsafes/verification unknownsClosed10/10/201710/27/2017

Actions

History

#1

Updated by Evgeny Novikov over 2 years ago

  • Description updated (diff)
  • Category changed from Scheduling to Tasks generation
  • Priority changed from Normal to Urgent
#2

Updated by Evgeny Novikov about 2 years ago

  • Assignee set to Ilja Zakharov
#3

Updated by Evgeny Novikov about 2 years ago

Let's do it together with #6608.

#4

Updated by Evgeny Novikov about 2 years ago

  • Assignee deleted (Ilja Zakharov)
  • Priority changed from Urgent to High

There are too many very high priority issues. This one can be done after really important features will be supported.

#5

Updated by Evgeny Novikov almost 2 years ago

  • Category deleted (Tasks generation)
#6

Updated by Ilja Zakharov almost 2 years ago

  • Priority changed from High to Urgent
  • Target version set to 2.0

Rising the priority since it is related to #7470 and blocks it.

#7

Updated by Evgeny Novikov over 1 year ago

  • Assignee set to Ilja Zakharov

I am not sure that this feature should be fully implemented together with #7470, although they definitely should be based on the same ground.

#8

Updated by Evgeny Novikov over 1 year ago

  • Description updated (diff)
  • Subject changed from Speculative scheduling to Intellectual scheduling
#9

Updated by Ilja Zakharov over 1 year ago

  • Category set to Scheduling
#10

Updated by Evgeny Novikov about 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.

#11

Updated by Ilja Zakharov about 1 year ago

Implemented in 6614-speculative-scheduling.

#12

Updated by Ilja Zakharov about 1 year ago

  • Status changed from New to Resolved
#13

Updated by Evgeny Novikov 12 months ago

  • Related to Feature #9167: Track speculative wall and CPU time added
#14

Updated by Evgeny Novikov 12 months ago

  • Status changed from Resolved to Closed

Tests passed demonstrating a very-very small change in total wall time. So, I merged the branch to master in aa70aed85.

Let's wait for very rapid verification tasks generation or/and quite complicated verification tasks when speculative scheduling will allow to win much time!

Also available in: Atom PDF