Klever

It was shown, that grouping rules in some ‘optimal’ way significantly helps to reduce negative impact in MAV (overall speedup of MAV CPU time could be more than 15(!) times). Thus, the main question of this issue is to suggest a heuristic, which will help automatically to find such ‘optimal’ grouping.
Currently I suggest the following heuristics, which should be evaluated in order to resolve this issue:
1. Evaluate the number of files in Linux kernel modules, which uses corresponding for rule interfaces, thus we can evaluate the ‘complexity’ of each rule. Based on that, we can place in a group a lot of ‘simple’ rules.
2. Evaluate the number of ‘relevant’ modules, for which we can prepare corresponding verification tasks, for each rule. The ideal instrument for this is MPV (the support of which was implemented in #7448), which outputs information about relevant rules in statistics. This way will be much more accurate.
3. We should not forget about MPV strategies, which are indented to decompose the whole specification into a smaller groups in order to verify together in the optimal way (similar task). MPV implements some heuristics, which could be useful for this issue. Thus the user should not even think about decomposing a set of rules, it will be done automatically in a verifier.

Vitaly Mordan wrote:

It was shown, that grouping rules in some ‘optimal’ way significantly helps to reduce negative impact in MAV (overall speedup of MAV CPU time could be more than 15(!) times). Thus, the main question of this issue is to suggest a heuristic, which will help automatically to find such ‘optimal’ grouping.

Please, read this feature topic and description. There aren't such requirements as you pointed. So, open another issue for this research. Here just support for grouping rule specifications is assumed. I already implemented it in general and just wait for you when you at last finish decomposition of the common aspect and test this in various test cases.

BTW, the optimal grouping of rules will vary from one verification task to another (is it was shown on thousands of verification tasks in MPV), therefore there is no optimal ‘static’ groups. This means, that this issue even in theory cannot provide anything good in general case.

Vitaly Mordan wrote:

BTW, the optimal grouping of rules will vary from one verification task to another (is it was shown on thousands of verification tasks in MPV), therefore there is no optimal ‘static’ groups. This means, that this issue even in theory cannot provide anything good in general case.

Again, why did you decide that here some optimal grouping is assumed?
Of course your point that "this issue even in theory cannot provide anything good in general case" isn't valid from both scientific and practical point of views.

Any kind of "static" groups did not help to find lost 3 True Positives with MAV. Thus, from practical point of view, groups are pointless and we will need to use SBT for "complex" rules (at least 43, 39, 32) and verify with MAV the rest. Again groups cannot help with this (need to use different strategies), but good old "sub-jobs" already can do it.

Vitaly Mordan wrote:

Any kind of "static" groups did not help to find lost 3 True Positives with MAV. Thus, from practical point of view, groups are pointless and we will need to use SBT for "complex" rules (at least 43, 39, 32) and verify with MAV the rest. Again groups cannot help with this (need to use different strategies), but good old "sub-jobs" already can do it.

Sub-jobs can't be used in production. They are intended just for testing and validation sets. It isn't so crucial to loose some unsafes. One will be able to check rules one by one if needed anyway.

You can't implement this important feature for a week, thus I will do this by myself.

So, the best solution is to create sub-jobs internally (by means of AVTG).
For example, there is some heuristic grouping, which places in one group all "simple" rules and uses sub-job with MAV, and in another all "complex" rules, which are verified separately. Similar idea successfully is used (dynamically) in MPV strategy Relevance. With more-or-less good manual grouping this method will work as efficient as MPV for most tasks. We could start by placing 32, 39, 43, 132 rules in separated group, and the rest in MAV.

Vitaly Mordan wrote:

So, the best solution is to create sub-jobs internally (by means of AVTG).

Sub-jobs can't be created internally.

For example, there is some heuristic grouping, which places in one group all "simple" rules and uses sub-job with MAV, and in another all "complex" rules, which are verified separately. Similar idea successfully is used (dynamically) in MPV strategy Relevance. With more-or-less good manual grouping this method will work as efficient as MPV for most tasks. We could start by placing 32, 39, 43, 132 rules in separated group, and the rest in MAV.

Perhaps it has sense to switch to SBT from MAV automatically when there is the only rule specification in a group (this is an example of a very simple dynamic VTG strategy), although I expect that MAV should behave exactly as SBT if one rule specification is given. If not so, MAV isn't completed yet.

MAV with one rule is not even intended to be SBT due to several reasons:
1. MAV does a lot of additional work (checking internal time limits, tracking precisions, updating current information in external file for relaunches) and that is all overhead costs (same true for MPV).
2. MAV basic preset L1 (as well as L2 and L3) uses heuristic time limits, which does not make sense for SBT.
3. External MAV launch soon to be strictly limited to mu*<what_the_user_specified>, mu>1 (according with current instruction). Moreover, there will be no chance for user to change that new limit (and completely break MAV).
That is why it will be strictly forbidden to launch MAV or MPV with only one rule/assert (according with instruction). There are separated strategies (for both instrumentation and automata) for that.

Evgeny Novikov wrote:

Vitaly Mordan wrote:

So, the best solution is to create sub-jobs internally (by means of AVTG).

Sub-jobs can't be created internally.

I would say, this is exactly what this issue should resolve.

I expect that MAV should behave exactly as SBT if one rule specification is given

As far as I understood static grouping (and creation of subjob) is done and hence the issue is done.

Dynamic grouping is a separate topic which is not so high priority now.

Vadim Mutilin wrote:

[...]
I agree, but it looks like a separate issue.

Of course. Now the easiest way is to use MAV even for checking individual rule specifications.

As far as I understood static grouping (and creation of subjob) is done and hence the issue is done.

Not yet since Vitaly didn't complete and test it. I do this myself now. The most tedious work is to split the common aspect so that if some rule specifications are checked just relevant parts of the common aspect are invoked.

Dynamic grouping is a separate topic which is not so high priority now.

Yes, it is. We can allow users to completely switch off multi-aspect verification.