Klever

I suggest to allow to the user to specify 'CPU time limit per 1 rule specification', which will be the same for all strategies (multi-aspect verification with internal and external launches, on-the-fly specification decomposition, etc.).
There also should be instruction, which will tell to the user, that strategies will interpret this limit differently.

Most of the users will use basic options for complex strategies (such as 900 CPU seconds per one task and one property according to SV-COMP and a lot of internal MAV limits). But if the user wants to understand, how some strategy works, he must read corresponding documentation (or even papers), which will prevent him from forgetting, for example, to specify iteration time limit.
We should support both groups of users. Current implementation is more oriented to the second group.
I think, this feature will be more needed in the future, when we will implement more user-friendly way to set jobs, since now there is still no one button 'launch MAV', which sets all needed option.

Vitaly Mordan wrote:

I suggest to allow to the user to specify 'CPU time limit per 1 rule specification', which will be the same for all strategies (multi-aspect verification with internal and external launches, on-the-fly specification decomposition, etc.).

First. Why do you consider just CPU time? Why do you miss RAM and disk space? For users they are also very important.
Second. The suggested name isn't accurate since if I will verify 1000 modules this will be a limit for checking all these modules against one rule.

There also should be instruction, which will tell to the user, that strategies will interpret this limit differently.

This instruction is relevant for strategies rather than for the limit itself. Users can know nothing about various strategies but understand what do the limits mean very well (if it will be clearly implemented).

Evgeny Novikov wrote:

Vitaly Mordan wrote:
First. Why do you consider just CPU time? Why do you miss RAM and disk space? For users they are also very important.

Disk space cannot be limited now (and in near future).
RAM always should have the same limitation (per verification run, per verification task, per one rule, ...).
CPU time in this issue will mean something useful only for Separated strategy. Therefore, the user should not have any illusions about usefulness of this limit and the name of the limit should clearly state it.

Second. The suggested name isn't accurate since if I will verify 1000 modules this will be a limit for checking all these modules against one rule.

Then
CPU time limit PER 1 rule PER 1 module PER 1 entry point

There should be a CPU_TIME_LIMIT which has a meaning of a CPU limit PER 1 rule PER 1 module PER 1 entry point
There should be a guarantee:
In SBT: the task with one rule should not work more than CPU_TIME_LIMIT
In MAV: the task with N rules should not work more than N*CPU_TIME_LIMIT
MAV should do its best to provide not more than CPU_TIME_LIMIT for each rule.

Side note here, may be a topic for another ticket.

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

This feature was implemented in branch new_format_of_strategies.
Now resource limit per one task (or Quality of Service limit) means the same for all strategies.
Resource limitations for the whole task will be resolved in another issue (#7470).