Project

General

Profile

Actions
Copy link

Feature #8240

closed

Fix transformation of witnesses to error traces for multithreaded software

Added by Evgeny Novikov over 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Ilja Zakharov
Category:
Tasks generation
Target version:
0.2
Start date:
06/13/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

See description in #8234.

Partially there is likely a bug but mostly some new things should be supported.

Files

Download all files
witness.struct_at76_priv__auth_mode.graphml (1.61 MB) witness.struct_at76_priv__auth_mode.graphml Pavel Andrianov, 06/27/2017 12:48 PM
unsafestruct_at76_priv__beacon_period report files.zip (3.81 MB) unsafestruct_at76_priv__beacon_period report files.zip Ilja Zakharov, 07/04/2017 05:35 PM
unsafestruct_at76_priv__channel report files.zip (953 KB) unsafestruct_at76_priv__channel report files.zip Ilja Zakharov, 07/10/2017 11:34 AM
unsafestruct_at76_priv__iw_mode report files.zip (953 KB) unsafestruct_at76_priv__iw_mode report files.zip Ilja Zakharov, 07/10/2017 11:34 AM

Related issues 2 (0 open — 2 closed)

Blocks Klever - Feature #8234: Error traces comparison for racesClosedVladimir Gratinskiy06/05/201709/23/2017

Actions
Blocked by Klever - Feature #8271: Implement checks of the error trace format in CoreClosedIlja Zakharov07/04/2017

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov over 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.

Actions
Copy link
 #2

Updated by Ilja Zakharov over 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.

Actions
Copy link
 #3

Updated by Pavel Andrianov over 7 years ago

Update CPALockator output format. New example of witness attached. New revision of CPALockator: 25097.

Actions
Copy link
 #4

Updated by Ilja Zakharov over 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

Actions
Copy link
 #5

Updated by Evgeny Novikov over 7 years ago

  • Assignee changed from Pavel Andrianov to Ilja Zakharov

Our issue tracker isn't intended for CPAchecker related issues.

Actions
Copy link
 #6

Updated by Pavel Andrianov over 7 years ago

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

Actions
Copy link
 #7

Updated by Ilja Zakharov over 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.

Actions
Copy link
 #8

Updated by Pavel Andrianov over 7 years ago

  • Status changed from Feedback to Open

Disable workaround filter of output files. New revision is 25107.

Actions
Copy link
 #9

Updated by Ilja Zakharov over 7 years ago

  • Status changed from Open to Feedback

Another one iteration of fixes.

Actions
Copy link
 #10

Updated by Ilja Zakharov over 7 years ago

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.

Actions
Copy link
 #11

Updated by Vadim Mutilin over 7 years ago

Any news on the topic?

Actions
Copy link
 #12

Updated by Vladimir Gratinskiy over 7 years ago

The bug in visualization was fixed in branch fix_8240.

Actions
Copy link Download all files
 #13

Updated by Ilja Zakharov over 7 years ago

It works but not always still. On that driver I got 11 unsafes and all except 2 can be visualized. See them in attachments.

Actions
Copy link
 #14

Updated by Evgeny Novikov over 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.

Actions
Copy link
 #15

Updated by Pavel Andrianov over 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.

Actions
Copy link
 #16

Updated by Vladimir Gratinskiy over 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.

Actions
Copy link
 #17

Updated by Ilja Zakharov over 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.

Actions
Copy link
 #18

Updated by Evgeny Novikov over 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.

Actions
Copy link
 #19

Updated by Evgeny Novikov over 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.

Actions
Copy link
 #20

Updated by Ilja Zakharov over 7 years ago

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.

Actions
Copy link
 #21

Updated by Evgeny Novikov over 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.

Actions
Copy link
 #22

Updated by Pavel Andrianov over 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.

Actions
Copy link
 #23

Updated by Vladimir Gratinskiy over 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.

Actions
Copy link
 #24

Updated by Pavel Andrianov over 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?

Actions
Copy link
 #25

Updated by Vladimir Gratinskiy over 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.

Actions
Copy link
 #26

Updated by Pavel Andrianov over 7 years ago

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

Actions
Copy link
 #27

Updated by Ilja Zakharov over 7 years ago

  • Assignee changed from Vladimir Gratinskiy to Ilja Zakharov
Actions
Copy link
 #28

Updated by Ilja Zakharov over 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.

Actions
Copy link
 #29

Updated by Evgeny Novikov about 7 years ago

  • Target version set to 0.2
Actions
Copy link
 #30

Updated by Evgeny Novikov about 7 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in b21a6ba5.

Actions
Copy link

Also available in: Atom PDF