Feature #8240
closed
Fix transformation of witnesses to error traces for multithreaded software
Added by Evgeny Novikov almost 8 years ago.
Updated over 7 years ago.
Category:
Tasks generation
Description
See description in #8234.
Partially there is likely a bug but mostly some new things should be supported.
Files
- Assignee set to Ilja Zakharov
Primarily Ilja developed code for dealing with threads, so it would be better if he will "fix" it.
- Status changed from New to Feedback
Expect new example of witness from Pavel. Then I will add support of thread identifiers and edges with thread creating.
Update CPALockator output format. New example of witness attached. New revision of CPALockator: 25097.
- Assignee changed from Ilja Zakharov to Pavel Andrianov
I cannot build CPAchecker from this revision (and from the next too):
[depend] Deleted 191 out of date files in 0 seconds
[javac] Compiling 592 source files to /work/zakharov/src/cpachecker/bin
[javac] /work/zakharov/src/cpachecker/src/org/sosy_lab/cpachecker/cpa/usage/KleverErrorTracePrinter.java:91: warning: [BoxedPrimitiveConstructor] valueOf or autoboxing provides better time and space performance
[javac] usedThreadIds.add(new Integer(nextThread));
[javac] ^
[javac] (see http://errorprone.info/bugpattern/BoxedPrimitiveConstructor)
[javac] Did you mean 'usedThreadIds.add(Integer.valueOf(nextThread));'?
[javac] error: warnings found and -Werror specified
[javac] 1 error
[javac] 1 warning
- Assignee changed from Pavel Andrianov to Ilja Zakharov
Our issue tracker isn't intended for CPAchecker related issues.
My ant build does not use Werror, so I have not such failure. Nevertheless, I fixed the problem in rev. 25099.
- Status changed from Open to Feedback
As I cannot run your example directly, I tried to generate witnesses myself. It occurs that the witnesses do not contain threads and in some sense there are spurious.
- Status changed from Feedback to Open
Disable workaround filter of output files. New revision is 25107.
- Status changed from Open to Feedback
Another one iteration of fixes.
Seems Bridge cannot visualize error trace with both threads interleaving and actions. I tried to no set actions and it works, but something goes wrong if I add actions to the same error trace. From my point of view, actions are set properly, but I cannot prove this. Vladimir, can you check out this attached example and either fix the visualizer or explain why it cannot be visualized?
Note, that in this example there is a point with a sudden switch to a different thread (which is correct for an error path with several threads) and this should cause a problem.
The bug in visualization was fixed in branch fix_8240.
It works but not always still. On that driver I got 11 unsafes and all except 2 can be visualized. See them in attachments.
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.
- Assignee changed from Vladimir Gratinskiy to Pavel Andrianov
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.
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.
- Status changed from Feedback to Open
- Assignee changed from Pavel Andrianov to Vladimir Gratinskiy
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.
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.
- Assignee changed from Vladimir Gratinskiy to Ilja Zakharov
- Status changed from Open to Resolved
Seems that it finally works (many thanks to all involved developers and their tremendous efforts!).
All fixes including fix_8240, checks for #8271 and recent merged master are available in branch "new-multithread-witness".
I wish Pavel would check it out and prove more examples working until it is merged to master.
- Target version set to 0.2
- Status changed from Resolved to Closed
I merged the branch to master in b21a6ba5.
Also available in: Atom
PDF