Feature #7448
closedAdd property automata for all rules
Added by Vitaly Mordan over 8 years ago. Updated over 4 years ago.
0%
Description
Without them it is impossible to evaluate all corresponding VTG strategies.
Moreover, most of property automata were implemented before.
Updated by Evgeny Novikov over 8 years ago
- Priority changed from Urgent to High
They aren't so important since they represent alternative experimental approach for developing rule specifications.
Updated by Vitaly Mordan over 8 years ago
- Status changed from New to Feedback
This feature was implemented in branch specification_automata.
Overall 30 new property automata were added or restored from LDV for all basic rule specifications. Now it is possible to use option 'property automaton' for RSG strategy for any rule specification.
In the course of this work, 150 rule specification was improved, in which countless pointer dereferences were (finally) removed.
Updated by Vitaly Mordan over 8 years ago
- Status changed from Feedback to Resolved
Updated by Vitaly Mordan over 8 years ago
- Status changed from Resolved to Open
In order to evaluate all strategies with property automata, a separated common aspect is required (without assume sections).
Updated by Vitaly Mordan over 8 years ago
- Status changed from Open to Resolved
Support of MPV-strategies along with tests has been added.
Updated by Evgeny Novikov over 8 years ago
This is an experimental branch for which practical improvements weren't shown yet while theoretically it is known that current automata have quite poor abilities for formalizing rules as well as they are supported by the only verification back-end, namely CPAchecker. Even good testing wasn't performed. In addition this feature request has the priority that is lower than the one of really significant features and bugs at the moment. Taking all this together means that there are no chances for this feature to be even reviewed and evaluated by anybody in near future.
The only thing that is absolutely obvious that changing any existing rule specifications can't be done in this branch. This should be done separately. In particular separate comparison of verification results should be provided.
Updated by Vitaly Mordan over 8 years ago
This is the best option to solve https://forge.ispras.ru/issues/7392.
It has 2 sets of new tests.
Comparison of new rule specification was provided.
It must be used in all experiments already.
Updated by Evgeny Novikov over 8 years ago
Vitaly Mordan wrote:
This is the best option to solve https://forge.ispras.ru/issues/7392.
Read again the topic, the description and comments for #7392.
It has 2 sets of new tests.
Tests usually show that something isn't complete shit. Nothing more. Moreover often hard test cases are missed or even specially excluded.
Comparison of new rule specification was provided.
I don't need comparison of rule specifications. I need comparison of verification results.
It must be used in all experiments already.
You are free to use this in experiments in your free time and on free resources.
Updated by Vitaly Mordan over 8 years ago
- Status changed from Resolved to Feedback
- Priority changed from High to Urgent
"Useless" automata in MPV could find all Unsafes as SBT do (which were lost in any static groups with MAV). Note, that MPV could process all basic 30 rules, whereas MAV with instrumentation could not handle 8-16 rules per group. MPV can handle large number of rules, because it creates different partitions for each module. For example, in module
drivers/net/ethernet/stmicro/stmmac/stmmac.ko
(in which MAV misses real bug due to internal time limit) MPV creates 2 groups: rules 10, 39, 43, 134 for separated verification, and the rest rules for simultaneous verification. Nobody will suggest such grouping in static, because usually rules 10 and 134 are considered to be much easier, than, for example, 32. But for this module this partition is optimal.
On the other hand, it will be much more convenient for the user to specify all rules and let some dynamic algorithm in verifier to group them, than create static groups (for example, if the user decide to make a new rule, in which group it should be placed?).
Therefore, priority of this feature rises. I suggest to use automata for other evaluations, because they can provide better results.
Updated by Evgeny Novikov over 8 years ago
- Priority changed from Urgent to High
We will consider this after really important things will be done.
Updated by Vitaly Mordan over 8 years ago
After resolving some issues, property automata operate exactly like instrumentation with small reduction of CPU time. Also they allow us to use MPV-strategies to verify multiple rules at once.
Currently there are several also important issues, which require this one, therefore I do not see any reasons to postpone it more and more. Otherwise, it will be very hard to merge it in master in a few weeks and we will lose much more time again (as it already was with MAV branch).
Updated by Vitaly Mordan almost 8 years ago
Evgeny Novikov wrote:
We will consider this after really important things will be done.
Is it possible, that there was not a few minutes in about five months to finally merge this branch? After it was thoroughly evaluated and results were presented.
Updated by Evgeny Novikov almost 8 years ago
- Priority changed from High to Normal
To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5, this time this branch will be merged to master just after it will be totally synced with it the required number of times, very well tested and most likely fixed, documented and *carefully reviewed by several people" (I expect numerous remarks after that, so you will need to fix as well). Of course, all orthogonal changes, e.g. fixes and improvements in rule specifications if so, should be considered and merged absolutely separately.
I reduce the priority of this issue in accordance with our plan to deal with really important tasks. I am sure that you will be able to do some of them.
Updated by Vitaly Mordan almost 8 years ago
To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5
This is absolutely incorrect (see https://forge.ispras.ru/issues/7617#note-6).
this branch will be merged to master just after it will be totally synced
It was synced already and was not merged before. Why?
very well tested and most likely fixed
It was tested before as well as basic strategy in master. Statement
Tests usually show that something isn't complete shit. Nothing more. Moreover often hard test cases are missed or even specially excluded.
means absolutely the same for any other component in master. For example, is there a test for error trace conversion functions, which operates with ~100Mb traces, in master? No. "Useless" filters from my branch could handle such traces. Can you give sumilar example for my branch?
documented
There is a documentation (about methods, not implementation), I did not change it much since summer. Anyone can comment there, so I could improve it.
*carefully reviewed by several people"
If so, then why this branch was not reviewed for the last few months?
Also this branch includes property automata. Who is going to review them? Or we do not need them, because they are too efficient?
Of course, all orthogonal changes, e.g. fixes and improvements in rule specifications if so, should be considered and merged absolutely separately
I merged a lot of fixes in this branch only because it was not merged in master for like half of the year.
When I prepared it for merge for the first time, it did not contain any orthogonal changes.
Thus, there was none adequate reasons, why it was not merged.
I reduce the priority of this issue in accordance with our plan to deal with really important tasks
Exactly the same was told several months ago (even in this issue). I guess one of such "important tasks" is to break and then to remove efficient and effective methods from VTG instead of fixing and refactoring them.
Updated by Evgeny Novikov almost 8 years ago
Vitaly Mordan wrote:
To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5
This is absolutely incorrect (see https://forge.ispras.ru/issues/7617#note-6).
Since your original statement is bad (https://forge.ispras.ru/issues/7617#note-7) all other notes don't need comments. The most of people have to spend their time doing really necessary things.
Updated by Vitaly Mordan almost 8 years ago
Evgeny Novikov wrote:
Vitaly Mordan wrote:
To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5
This is absolutely incorrect (see https://forge.ispras.ru/issues/7617#note-6).
Since your original statement is bad (https://forge.ispras.ru/issues/7617#note-7) all other notes don't need comments. The most of people have to spend their time doing really necessary things.
Since statement https://forge.ispras.ru/issues/7617#note-7 is far from being adequate (see https://forge.ispras.ru/issues/7617#note-8), real issues from this discussion are simple ignored.
Updated by Evgeny Novikov over 4 years ago
- Status changed from Feedback to Rejected