Project

General

Profile

Feature #8240

Fix transformation of witnesses to error traces for multithreaded software

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

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Tasks generation
Target version:
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


Related issues

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

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

Actions

History

#1

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

#2

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

#3

Updated by Pavel Andrianov over 3 years ago

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

#4

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

#5

Updated by Evgeny Novikov about 3 years ago

  • Assignee changed from Pavel Andrianov to Ilja Zakharov

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

#6

Updated by Pavel Andrianov about 3 years ago

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

#7

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

#8

Updated by Pavel Andrianov about 3 years ago

  • Status changed from Feedback to Open

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

#9

Updated by Ilja Zakharov about 3 years ago

  • Status changed from Open to Feedback

Another one iteration of fixes.

#10

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

#11

Updated by Vadim Mutilin about 3 years ago

Any news on the topic?

#12

Updated by Vladimir Gratinskiy about 3 years ago

The bug in visualization was fixed in branch fix_8240.

#13

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

#14

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

#15

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

#16

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

#17

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

#18

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

#19

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

#20

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

#21

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

#22

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

#23

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

#24

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

#25

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

#26

Updated by Pavel Andrianov about 3 years ago

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

#27

Updated by Ilja Zakharov about 3 years ago

  • Assignee changed from Vladimir Gratinskiy to Ilja Zakharov
#28

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

#29

Updated by Evgeny Novikov about 3 years ago

  • Target version set to 0.2
#30

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in b21a6ba5.

Also available in: Atom PDF