Klever

Evgeny Novikov wrote:

Initially they were erroneously added to master just because of corresponding branches hold too much useful and orthogonal features. So they should be just removed since there are too much problems in them.

In fact, branch 'new_format_of_strategies' (with a lot of fixes for all those "erroneously added" strategies and after conducting experiments) was not merged without any good reason, when it could take just a few minutes (see issues #7448, #7467). Now it will take a few weeks or maybe even more, because of multiple changes in both experimental branch and master (see issue #7800).

This was a global mistake and the only reason, why "there are too much problems" in those strategies in master now. We should try to avoid such mistakes in future.

Evgeny Novikov wrote:

Initially they were erroneously added to master just because of corresponding branches hold too much useful and orthogonal features.

This is not true.
For example, issues #7394 (added support of MPV) and #6779 (added support of old rules for MAV), which logically precedes to the issue #7448 (added support of old rules for MPV and some bugs were fixed), were merged, because they added more perspective methods and improved the whole system in general, but they did not hold anything useful only for basic sequential strategy. Thus it is still unclear, why issue #7448 and everything after it were not merged.

The only issue, which fits this description, is #7237, but it is much more earlier issue.

You should inspect output of "git log -p v0.1rc4..v0.1rc5" where the functionality I am talked about was merged to master. One will easily see that together with bad implementation of various advanced strategies that I had have to fix myself numerous times there are also numerous orthogonal improvements and fixes in rule specifications that were included by you in the branch with that implementation. It was too hard to separate them easily since we had the very strict and already shifted deadline. I was terribly upset that I had to merge this branch but I hadn't another chooise. Soon I will spend several hours to get rid of the bad implementation.

First, output of "git log -p v0.1rc4..v0.1rc5" shows merge for issue #7237, which was hard to perform only because corresponding branch was not merged at a time, when it was synchronized with master, because about 2 months were wasted on discussion about "ideal strategy", which should replace MAV/MEA/MPV etc., but nothing detailed was even suggested. Therefore, it rather were unsynchronized branches rather than a bad implementation.

fixes in rule specifications

There were a lot of bugs in rules at that time, and nobody else conducted experiments with them, so I had to fix those bugs. I do not see any reason, why those fixes should not be merged ASAP.

Second, branches for #7394, #6779 and #7448 were synchronized with master (at least at the time, they were created and suggested for merging). At that time they literally required several minutes for merge. And it does not explain, why only some branches were merged (without "much useful and orthogonal features" for basic strategy).

BTW, branches #7448 and #7467 were prepared and synchronized with master before the deadline and could (this actually were confirmed later) improve our results, but these issues were ignored.

I was terribly upset that I had to merge this branch

Then why make the same mistake and postpone more and more prepared and synchronized branches so it would be too hard to merge them?

Soon I will spend several hours to get rid of the bad implementation.

And if anyone will need to use MAV with some new features (for example, to generate tasks for SVCOMP), now it will be completely impossible.
That's great!

It wasn't merged because of nobody actually wanted them much

Why did we use MAV for our experiments then? I guess, it is more convenient to get results faster, isn't it?

nobody carefully reviewed them

Did anyone (at least) carefully reviewed error trace filters from master? I doubt. Nobody even tried to use them in practice. Then why are they in master?

MAV has much more tricky issues, e.g. all time heuristics

Do you even understand why all those heuristics were used? I doubt. Read my old documentation first at least, otherwise how can you review something, that you completely do not understand.

Until you will fix all of them nothing will be in master any more.

Then wait for verification results few times more, I am sure all our users will love it.

What is a pity. Dirk and his colleagues already specified their opinion about MAV, he isn't interested much both in it and in corresponding verification tasks in their original flavor. Added verification tasks aren't intended for finding violations of several properties - they almost the same as other ones.

What is a pity, that you do not understand the difference between CPAchecker (general verifier) and our system (which should also verify big number of modules against big number of rules) and that MAV is much more needed for us.

So, MAV wasn't merged to CPAchecker trunk yet and this likely won't happen ever

There are adequate reasons for it (like optimizations, which make sense only in MAV).

if you will do really necessary things

Can you list at least one adequate reason, why it was not merged at first? (synched, tested, documented branch after experiments)

Why it should seem strange that almost nobody accepts MAV and your other conceptions.

If you are everybody, that is really strange.
And if you do not accept MAV, please, suggest and implement a "new approach", which will show better results. So far I did not even see a suggestion.

One more fix of this is available in 372aecb to master. This commit fixes creating of Unknown reports for verifiers when resources aren't exhausted, e.g. parsing failures happen, and logs aren't created, that is usual for the production decision mode. This issue is especially unpleasant due to #7571 since instead of getting some error message that one can inspect one just get corrupted decision due to some component reports aren't finished.

Evgeny Novikov wrote:

e.g. parsing failures happen, and logs aren't created, that is usual for the production decision mode.

FYI, logs are created in case of parsing failure, so the real reason is different.

This issue is especially unpleasant due to #7571 since instead of getting some error message that one can inspect one just get corrupted decision due to some component reports aren't finished.

So commit https://forge.ispras.ru/projects/klever/repository/revisions/878f9747f20b416c7c2122523376aeb3c6e554de managed to break something.

Vitaly Mordan wrote:

Evgeny Novikov wrote:

e.g. parsing failures happen, and logs aren't created, that is usual for the production decision mode.

FYI, logs are created in case of parsing failure, so the real reason is different.

This issue is especially unpleasant due to #7571 since instead of getting some error message that one can inspect one just get corrupted decision due to some component reports aren't finished.

So commit https://forge.ispras.ru/projects/klever/repository/revisions/878f9747f20b416c7c2122523376aeb3c6e554de managed to break something.

It looks like you even didn't see what the recent 372aecb did as well as what I have done in branch fix-7617.

Core and its components do not create logs in case of the production decision mode. And this wasn't processed properly. My recent commit just fixed that.

It looks like you even didn't see what the recent 372aecb did as well as what I have done in branch fix-7617.

As I can see 372aecb fixes problems with logs for production mode. It has nothing to do with parsing fails.

Commit 878f974 (merge branch fix-7617) is the worst commit during our whole project. Anyone can count, that it threw away ~10 devoper-months (total time, that I spent on MAV in klever). Moreover you managed to remove some very hard to recreate elements (for example, common aspect, description of tests for MAV/MPV, support of different strategies in RSG (RSG is yet another example of your own "poorly established code"), option for uniting rules, etc.). Such elements will be hard to rewrite, because they require thorough testing and I cannot just copy them from my branch, since all formats were changed. Therefore, if we ever need those strategies, it will take months to restore them.
That is why now you will have to spent on average 5 times more time for your experiments even with more machines, therefore you will be able to run less experiments, to fix less bugs and will get worse results in the end. That is what you have done in 878f974.

Vitaly Mordan wrote:

It looks like you even didn't see what the recent 372aecb did as well as what I have done in branch fix-7617.

As I can see 372aecb fixes problems with logs for production mode. It has nothing to do with parsing fails.

https://forge.ispras.ru/issues/7617#note-10 - read this one more time. Then you will understand what I fixed.

Commit 878f974 (merge branch fix-7617) is the worst commit during our whole project. Anyone can count, that it threw away ~10 devoper-months (total time, that I spent on MAV in klever). Moreover you managed to remove some very hard to recreate elements (for example, common aspect, description of tests for MAV/MPV, support of different strategies in RSG (RSG is yet another example of your own "poorly established code"), option for uniting rules, etc.). Such elements will be hard to rewrite, because they require thorough testing and I cannot just copy them from my branch, since all formats were changed. Therefore, if we ever need those strategies, it will take months to restore them.
That is why now you will have to spent on average 5 times more time for your experiments even with more machines, therefore you will be able to run less experiments, to fix less bugs and will get worse results in the end. That is what you have done in 878f974.

Thank you for highlighting the most of noticeable things done. Now you understand what was done. Perhaps one day you will understand why it was done at last and what can/should be done later with all these abnormal verification tasks generation strategies to avoid mistakes from the past.

Evgeny Novikov wrote:

https://forge.ispras.ru/issues/7617#note-10 - read this one more time. Then you will understand what I fixed.

In any case, this is a small fix, which can be done in several minutes and cannot be compared with 878f974.

Perhaps one day you will understand why it was done at last

I think, this is well-known, since you specified yourself a lot of emotional, irrational and even false "reasons" (like you did not want to understand core ideas of MAV, you did not like automata for no reasons, you refused to review synched, tested, documented branch after experiments, "practical improvements weren't shown yet" - I guess you were sleeping when I presented it, and much more even less adequate "reasons").

what can/should be done later with all these abnormal verification tasks generation strategies to avoid mistakes from the past.

FYI, I do not need those strategies in master for my own experiments and was asking to merge them, because they add more perspective methods, which improves our system in general and can be useful for others (including you). Right now you will have to kill a lot of time for your own experiments because of 878f974.

Thank you for highlighting the most of noticeable things done.

Which is also one of the biggest fails in development of our system (after refusing to merge branch #7448, of course, which is the root of all these problems).