Feature #7800
closedFeature #7799: Integrate Ultimate Automizer as an alternative verification tool
Refactoring of VTG
0%
Description
To integrate new verification tool all common part of existing strategies should be separated from CPAchecker specific functionality.
Updated by Ilja Zakharov about 8 years ago
- Assignee changed from Ilja Zakharov to Vitaly Mordan
I have done some necessary first steps of the refactoring to be able to integrate another tool but still there are many things to be done in this directon to make code tidy and clear for understanding. The major issues:
- Distinguish private methods (__mymethod), private inheritable methods (_mymethod), public methods (mymethod)
- Even if init function is not used there should be a function with list of attributes introduced by the strategy. Like methods all attributes should be distinguished concerning privateness.
- Implement clear algorithms for strategies with clear set of methods that can be implemented by another strategies derived from common ones. If it is necessary to introduce an hierarchy of strategies than should be able to understand where a general algorithm of a strategy is implemented and which steps are overrode or implemented differently. Currently functionality is very distributed and one cannot observe particular steps of any strategy because each contain just set of methods and its really hard to understand who calls them because there are called from many different places.
- Submitting tasks and getting results from Bridge and work with the other reports should be extracted into separate libraries inside VTG.
- It is forbidden to use attributes or methods in abstract strategies if there are introduced or logically belong to strategies which are inherited from this one. I removed all .mea, .mav and the other attributes from common strategies, but inside CPAchecker strategies (for example separated) there are a lot of inaccurate code left.
Updated by Ilja Zakharov about 8 years ago
Current implementation is placed in ultimate-backend branch.
Updated by Vitaly Mordan about 8 years ago
The main question, which should be resolved before major refactoring, is what to do with other strategies (MAV, MEA, MPV, etc.). Currently they are all broken or incomplete in master, and I do not see any perspective for refactoring them as they are.
Therefore, I suggest to finally determine, if we even need those strategies in master.
If yes, then I will merge this branch with "new_format_of_strategies", which will make all strategies available. This may take some time. In the process of merging all suggestions from this issue also should be taken into account.
Otherwise if we do not require more efficient and more effective methods in master, I suggest to fully remove all strategies except so called "SBT/SBK" from master, which significantly simplify the process of refactoring.
Updated by Evgeny Novikov about 8 years ago
- Category changed from Infrastructure of Core to Tasks generation
- Assignee deleted (
Vitaly Mordan)
I suggest to remove all poorly established code from master and just support clear things that operate properly and reasonably. The only bad thing is that this will simplify components so that they will not allow to extend them even in the way that is available now. Perhaps this isn't very bad since eventually we can decide to give up experiments with multi-aspect verification and all its variants, for instance, if a more simpler, efficient and strong approach will be suggested instead.
Updated by Vitaly Mordan about 8 years ago
Evgeny Novikov wrote:
all poorly established code
Most likely, more experiments were conducted with that "poorly established code", than with other components, and thus it probably contains much less bugs, than other components in master.
Evgeny Novikov wrote:
The only bad thing is that this will simplify components so that they will not allow to extend them even in the way that is available now.
In other words, the master will degrade.
Evgeny Novikov wrote:
if a more simpler, efficient and strong approach will be suggested instead.
As someone who more or less knows this area, I doubt anything "more simpler, efficient and strong" will be suggested from nowhere.
Most likely, the main direction of development will be related with automata specifications, which are more clear (than instrumentation), more efficient, more effective, and more applicable to verifying several properties.
Therefore, our tool ignores more perspective methods for no reason.
Updated by Ilja Zakharov about 8 years ago
all poorly established code
I explicitly stated a list of drawbacks in VTG strategies code. Moreover, experiments with Ultimate Automizer showed that current architecture of this code is completely unclear and inextensible. Another question is how to fix it, but I doubt that implementation of new advanced features on this unstable basis is a good idea.
Most likely, the main direction of development will be related with automata specifications, which are more clear (than instrumentation), more efficient, more effective, and more applicable to verifying several properties.
Anyway current state of automata specifications cannot replace an existing main workflow and it cannot be used with the other verification tools. According to this this functionality can be considered at the moment as an additional and extending feature of VTG and its code should be separated and not mixed with the main one.
Updated by Vitaly Mordan about 8 years ago
I explicitly stated a list of drawbacks in VTG strategies code.
I completely agree, that VTG strategies code should be refactored (here I mean their full implementation in branch "new_format_of_strategies") and I can do it. But it does not mean, that corresponding algorithms (CMAV, MEA, MPV, SC), which showed very promising results, are "all poorly established". The main question is whether we need those algorithms (after refactoring) in master on not.
Anyway current state of automata specifications cannot replace an existing main workflow
All current rules can be formalized by automata specifications, and it was done long ago.
it cannot be used with the other verification tools.
Currently, yes, only CPAchecker supports automata specifications (as well as MAV and MEA). But first, before this issue, we supported only CPAchecker as verification tools.
Second, with the extension of multi-aspect verification ideas, it is possible, that more tools will start to support it in near future (potentially even new category in SVCOMP can be created).
From my point of view, even if one tool operates with more perspective methods and we state, that we fully support the tool, we need to support those methods as well. Of course, such methods should be available exclusively for corresponding verification tool (which is violated in current implementation and should be resolved during refactoring).
Updated by Evgeny Novikov almost 8 years ago
- Assignee set to Vitaly Mordan
- Priority changed from Normal to Low
After fixing of #7617 this issue will be relevant just for the specified experimental branch. Definitely it should be implemented there if we will want to merge this branch to master one day. Nevertheless I am absolutely not sure that we will decide this positively, so I don't see much sense to waste any resources on it while we always have issues of much more importance.
Updated by Evgeny Novikov over 7 years ago
- Assignee changed from Vitaly Mordan to Ilja Zakharov
- Target version set to 2.0
This issue likely will become irrelevant after refactoring.
Updated by Evgeny Novikov over 7 years ago
- Target version changed from 2.0 to 0.2
This considerable Core refactoring is always completed and it would be better to have it in master ASAP while Klever 1.0 will be devoted to great conceptual improvements.
Updated by Ilja Zakharov over 7 years ago
- Status changed from New to Resolved
Implemented in the core-refactoring branch.
Major refactoring is almost finished. There are a couple of problems left and some minor introduced but it is better to deal with them separately. The refactoring included scaling parallel tasks generation, verifier options separation, templates for setting heap and limits in the option configuration file, support of the UltimateAutomizer verifier, deletion of verification tasks files during the progress and deletion them from the server, reuse of EMG and SA plugins data to avoid extra calls of CIF and speed up tasks generation, separation of tasks processing into additional components and many other helpful improvements. So I think that it is time to merge this as it is merged with the latest master branch and it becomes each next time more difficult.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Resolved to Open
At the moment common attributes as well as verification objects aren't reported for unsafe/safe/unknown reports that is absolutely crucial for creating corresponding marks. The former should be likely reported for VTGVRP while the latter for RP.
Update CPAchecker SMG up to version smg_witness_for_ldv:25566 - this was done in master about month ago.
Also I suppose to at last introduce one more component level between VTG (former AVTG) and its plugins. Otherwise plugin reports for various verification objects and rule specifications are intermixed. This issue existed before this refactoring as well.
Updated by Evgeny Novikov over 7 years ago
Also you need to update preset unknown marks for ABKM, AVTG and VTG.
Updated by Evgeny Novikov over 7 years ago
I suppose to move coverage related parameters from the most high-level configuration, job.json, to configurations for particular rule specifications since this is closer to particular verifier capabilities. For instance, you can check together rule specifications while for some of them coverage cannot be produced.
Minor notes:- I don't understand why did you specified an XML namespace just for rule specification sync:race.
- I suggest to use more appropriate attribute name instead of expect several files. I think that this is about multiple error witnesses.
Updated by Ilja Zakharov over 7 years ago
- Status changed from Open to Resolved
Done all that you have requested in messages above. Check the new version, please.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Resolved to Open
A bug was introduced in this branch. At the moment failures of verification tasks generation plugins aren't reflected in resulting testing and validation tables.
All other mentioned below issues were fixed.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Resolved to Open
- If something wrong is with verifiers, e.g. I terminated them with a signal, then corresponding unknown reports are not children of verification reports - they are children of RP reports. This breaks preset unknown mark associations because of another component name.
- I suggest that a meta component VTGVRP is redundant. Initially I thought to introduce it to unite working directories of Verification Tasks Generator and Verification Results Processor which are very similar because of they start with corresponding verification objects and rule specifications. But that wasn't done and I'm not sure that we will do it ever.
- Both verification reports and their archives are now placed into working directories with ugly names. I suppose to use for them exactly the same names as were used before (some minor improvements are welcome) but create symlinks at corresponding paths to actual report and archive contents which is located in a dedicated directory now protected from removing before report uploading.
Other notes I mentioned directly in corresponding issues (#7803, #7924). For other related issues I didn't find any bugs. But I didn't play much with, say, verifier parameters and with integration of new static verification tools. Anyway at last we are moving forward in this direction.
Updated by Ilja Zakharov over 7 years ago
- Status changed from Open to Resolved
If something wrong is with verifiers, ...
Done.
I suggest that a meta component VTGVRP is redundant.
I prefer to keep it as is because there are a lot of common shared data between VTG and VRP such as queues and directories. It is better to create the queues in VTGVRP and show that the components reuse dirs because they do their job as siblings of the one component.
Both verification reports and their archives are now placed into working directories with ugly names
Names contain the same data as previously but an identifier, so names are not completely useless at least comparing with the recent situation. The reason for the identifier is that in the same working directories happen reports with ununique names because of running components in the same dirs. I can try to remove identifiers for symlinks in components dirs but I cannot guarantee that it will work and it will require quite a comprehensive testing to check because some time ago it did not work. Moreover, reports are technical files intended for developers mostly and there are a lot of other important work to do other than complaining about ugly names of temporary files.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Resolved to Open
Ilja Zakharov wrote:
I suggest that a meta component VTGVRP is redundant.
I prefer to keep it as is because there are a lot of common shared data between VTG and VRP such as queues and directories. It is better to create the queues in VTGVRP and show that the components reuse dirs because they do their job as siblings of the one component.
Queues between the top level components are shared by hooking a special function called before those components are launched. You can find an example at the beginning of core/core/lkbce/_init__.py_.
I don't see any directory reuse because of VTG and VRP seem to create working directories independently on each other. There is just one extra parent directory for VTGVRP. Note that source tree directories are also "shadowed" within working directories of LKBCE and LKVOG but you didn't put them into the VTGVRP working directory.
Indeed I think that it will be great from some point of view if we will put everything related into the corresponding working directories. For instance, put a verification object description within a directory corresponding to a module path and put everything related with rule specifications within corresponding subdirectories within that one. But let's do that cool feature one day later.
Thus, if you can get rid of a redundant component, please, do it!
Both verification reports and their archives are now placed into working directories with ugly names
Names contain the same data as previously but an identifier, so names are not completely useless at least comparing with the recent situation. The reason for the identifier is that in the same working directories happen reports with ununique names because of running components in the same dirs. I can try to remove identifiers for symlinks in components dirs but I cannot guarantee that it will work and it will require quite a comprehensive testing to check because some time ago it did not work. Moreover, reports are technical files intended for developers mostly and there are a lot of other important work to do other than complaining about ugly names of temporary files.
First of all names don't contain the same data. I can't distinguish, say, start and finish component reports since there is just a number of meaningless symbols and "report" in report names while before they were named like "start report" and "finish report".
Updated by Ilja Zakharov over 7 years ago
- Status changed from Open to Resolved
After another day of refactoring of the 'refactoring' I solved both issues. Now there is no VTGVRP and any data reuse between VTG and VRP except queues. For reports in component directories I have introduced cool and awesome names. Enjoy, I hope I have not introduced any additional bugs but it is worth checking.
P.S. To merge collateral branches for other core-related features intended for v0.2 an additional merge of this branch can be required.
Updated by Evgeny Novikov about 7 years ago
- Status changed from Resolved to Closed
After fixing several more issues I eventually merged the branch containing numerous cool improvements in Core to master in aec48ac1.