Feature #7392
closedSupport groupping of rule specifications to be checked together
Added by Vitaly Mordan almost 8 years ago. Updated almost 8 years ago.
0%
Description
Experiments show that some rule specifications can be checked together quite efficiently that is with much less resources and without considerable changes in obtained verification verdicts. That is why we need a way to specify manually such groups of rules.
In addition it is suggested to create just one big default common aspect and mark its parts by identifiers of rules or groups of rules.
Therefore, the user only specifies rules to check and the strategy, common aspect is added automatically in optimal way.
Thus, common aspect should be similar to the following:
#ifdef __REQUIREMENT_GROUP_68_69
around: call(struct urb *usb_alloc_urb(.., gfp_t flags, ..))
{
struct urb *res = ldv_linux_usb_urb_usb_alloc_urb();
ldv_assume(!ldv_is_err(res));
ldv_linux_alloc_irq_check_alloc_flags(flags);
ldv_linux_alloc_spin_lock_check_alloc_flags(flags);
ldv_linux_alloc_usb_lock_check_alloc_flags(flags);
return res;
}
#endif
Updated by Evgeny Novikov almost 8 years ago
- Category changed from Program fragments generation to *Abstract tasks generation
- Status changed from New to Open
- Assignee changed from Vitaly Mordan to Evgeny Novikov
- Priority changed from Low to Urgent
We need this at least to have easy way to experiment with various subsets of rules to be verified together. Then it can be helpful to specify default such groups.
I hope that this all is related just with generation of abstract verification tasks and nothing else should take care about this.
Updated by Evgeny Novikov almost 8 years ago
- Subject changed from Implement smart usage of common aspect to Support groupping of rule specifications to be checked together
- Description updated (diff)
Updated by Evgeny Novikov almost 8 years ago
- Published in build set to rule-spec-groups
I implemented all the required support in tools and added several examples of grouping rule specifications and getting relevant parts of common aspect in branch rule-spec-groups.
Vitaly needs to try this, specify more/proper groups and test altogether expressively.
Updated by Vitaly Mordan almost 8 years ago
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.
Updated by Evgeny Novikov almost 8 years ago
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.
Updated by Vitaly Mordan almost 8 years ago
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.
Updated by Evgeny Novikov almost 8 years ago
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.
Updated by Vitaly Mordan almost 8 years ago
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.
Updated by Evgeny Novikov almost 8 years ago
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.
Updated by Vitaly Mordan almost 8 years ago
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.
Updated by Evgeny Novikov almost 8 years ago
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.
Updated by Vitaly Mordan almost 8 years ago
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.
Updated by Vitaly Mordan almost 8 years ago
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.
Updated by Vadim Mutilin almost 8 years ago
I expect that MAV should behave exactly as SBT if one rule specification is given
I agree, but it looks like a separate issue.
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.
Updated by Evgeny Novikov almost 8 years ago
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.
Updated by Evgeny Novikov almost 8 years ago
- Status changed from Open to Closed
- Published in build changed from rule-spec-groups to 52b9229
I completed the branch and merge it to master in 52b9229.