Feature #8240
closedFix transformation of witnesses to error traces for multithreaded software
0%
Description
See description in #8234.
Partially there is likely a bug but mostly some new things should be supported.
Files
Updated by Evgeny Novikov almost 7 years ago
- Assignee set to Ilja Zakharov
Primarily Ilja developed code for dealing with threads, so it would be better if he will "fix" it.
Updated by Ilja Zakharov almost 7 years ago
- 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.
Updated by Pavel Andrianov almost 7 years ago
- File witness.struct_at76_priv__auth_mode.graphml witness.struct_at76_priv__auth_mode.graphml added
- Status changed from Feedback to Open
Update CPALockator output format. New example of witness attached. New revision of CPALockator: 25097.
Updated by Ilja Zakharov almost 7 years ago
- 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
Updated by Evgeny Novikov almost 7 years ago
- Assignee changed from Pavel Andrianov to Ilja Zakharov
Our issue tracker isn't intended for CPAchecker related issues.
Updated by Pavel Andrianov almost 7 years ago
My ant build does not use Werror, so I have not such failure. Nevertheless, I fixed the problem in rev. 25099.
Updated by Ilja Zakharov almost 7 years ago
- 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.
Updated by Pavel Andrianov almost 7 years ago
- Status changed from Feedback to Open
Disable workaround filter of output files. New revision is 25107.
Updated by Ilja Zakharov almost 7 years ago
- Status changed from Open to Feedback
Another one iteration of fixes.
Updated by Ilja Zakharov almost 7 years ago
- File unsafestruct_at76_priv__beacon_period report files.zip unsafestruct_at76_priv__beacon_period report files.zip added
- Assignee changed from Ilja Zakharov to Vladimir Gratinskiy
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.
Updated by Vladimir Gratinskiy almost 7 years ago
The bug in visualization was fixed in branch fix_8240.
Updated by Ilja Zakharov almost 7 years ago
- File unsafestruct_at76_priv__channel report files.zip unsafestruct_at76_priv__channel report files.zip added
- File unsafestruct_at76_priv__iw_mode report files.zip unsafestruct_at76_priv__iw_mode report files.zip added
It works but not always still. On that driver I got 11 unsafes and all except 2 can be visualized. See them in attachments.
Updated by Evgeny Novikov almost 7 years ago
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.
Updated by Pavel Andrianov almost 7 years ago
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.
Updated by Vladimir Gratinskiy almost 7 years ago
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.
Updated by Ilja Zakharov almost 7 years ago
- 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.
Updated by Evgeny Novikov almost 7 years ago
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.
Updated by Evgeny Novikov almost 7 years ago
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.
Updated by Ilja Zakharov almost 7 years ago
Updated by Evgeny Novikov almost 7 years ago
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.
Updated by Pavel Andrianov almost 7 years ago
- 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.
Updated by Vladimir Gratinskiy almost 7 years ago
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.
Updated by Pavel Andrianov almost 7 years ago
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?
Updated by Vladimir Gratinskiy almost 7 years ago
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.
Updated by Pavel Andrianov almost 7 years ago
Split thread creation into two actions (creation a thread and entering the corresponding function) is implemented in rev. 25248.
Updated by Ilja Zakharov almost 7 years ago
- Assignee changed from Vladimir Gratinskiy to Ilja Zakharov
Updated by Ilja Zakharov almost 7 years ago
- 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.
Updated by Evgeny Novikov over 6 years ago
- Status changed from Resolved to Closed
I merged the branch to master in b21a6ba5.