Klever

My ant build does not use Werror, so I have not such failure. Nevertheless, I fixed the problem in rev. 25099.

Any news on the topic?

The bug in visualization was fixed in branch fix_8240.

I suppose to make all related fixes and improvements in branch new-multithread-witness. Also I am wondering whether something useful should be taken from quite old branch feature_8234 there or it just should be deleted.

Evgeny Novikov wrote:

Also I am wondering whether something useful should be taken from quite old branch feature_8234 there or it just should be deleted.

In the corresponding ticket #8234 I placed my expectations about error comparison algorithm for multithreaded programs. That one, implemented in feature_8234 is not correct and should be modified. I do not know, is it useful for refactoring or should be completely rewritten.

The second error trace doesn't have return from function 28 (ldv_ieee80211_scenario_2).
It looks like:

(thread3) enter 27;
(thread3) enter 28;
(thread4)...WARNING
(thread3) return from 27;

I guess the first one has the same problem.

Pavel Andrianov wrote:

Evgeny Novikov wrote:

Also I am wondering whether something useful should be taken from quite old branch feature_8234 there or it just should be deleted.

In the corresponding ticket #8234 I placed my expectations about error comparison algorithm for multithreaded programs. That one, implemented in feature_8234 is not correct and should be modified. I do not know, is it useful for refactoring or should be completely rewritten.

So, I expect some comments from Vladimir regarding this issue.

Ilja Zakharov wrote:

This is quite strange, yes. And such edges exist in original witnesses. I think that CPAchecker also prints too many redundant edges with ldv_thread_create also.

After one more iteration I added #8234 as a blocker issue since otherwise we will spend more time finding out such the bugs even when implementing just this feature.

After one more iteration I added #8234 as a blocker issue since otherwise we will spend more time finding out such the bugs even when implementing just this feature.

You have meant #8271, right? I have done it and it detects the issue for Pavel.

Ilja Zakharov wrote:

After one more iteration I added #8234 as a blocker issue since otherwise we will spend more time finding out such the bugs even when implementing just this feature.

You have meant #8271, right? I have done it and it detects the issue for Pavel.

Yes, of course. This is great that we have it implemented now at last.

Pavel Andrianov wrote:

Vladimir Gratinskiy wrote:

The second error trace doesn't have return from function 28 (ldv_ieee80211_scenario_2).

it looks like:
(thread3) enter 27;
(thread3) threadsCreate(ldv_ieee80211_scenario_2), creates thread4 with enter 28;
(thread4)...WARNING
(thread3) return from 27;

Thus, return from 28 means the end of thread4 and is not present in trace. Seems, this is not an error, just the thread is switched (created) at the function entry.

Enter was in thread 3, so return must be there. After thread switched I return from every entered function in the previous thread. So the function ldv_ieee80211_scenario_2 should be in thread 4.

New idea is to divide the problem edge into the two ones: one creates a thread and the other enters the function

(thread3) enter 27;
(thread3) threadsCreate(ldv_ieee80211_scenario_2), creates thread4
(thread4) enter 28 (ldv_ieee80211_scenario_2)
(thread4)...WARNING
(thread3) return from 27;

Is it suitable?

Pavel Andrianov wrote:

New idea is to divide the problem edge into the two ones: one creates a thread and the other enters the function

(thread3) enter 27;
(thread3) threadsCreate(ldv_ieee80211_scenario_2), creates thread4
(thread4) enter 28 (ldv_ieee80211_scenario_2)
(thread4)...WARNING
(thread3) return from 27;

Is it suitable?

Yes.

Split thread creation into two actions (creation a thread and entering the corresponding function) is implemented in rev. 25248.