Static Datarace Analysis Unsound?

[Suvam Mukherjee]

Hi,

I have been experimenting with the static datarace detector in Chord. The analysis datarace-java seems to work fine on the datarace-test in the examples directory. However, it fails to detect any races in the following simple Java application:

Thread 1:

public class RacyThread1 extends Thread {

private Data d;

public RacyThread1(Data d)

{

this.d = d;

}

public void run()

{

while(true)

{

d.setData(10);

if(d.getData() != 10)

System.out.println("\nThread 1 observed value for x: " + d.getData());

}

}

}

Thread 2:

public class RacyThread2 extends Thread {

private Data d;

public RacyThread2(Data d)

{

this.d = d;

}

public void run()

{

while(true)

{

d.setData(20);

}

}

}

Main:

public class Driver {

/**

* @param args

*/

private static Data d;

public static void main(String[] args) throws InterruptedException {

// TODO Auto-generated method stub

d = new Data(0);

RacyThread1 t1 = new RacyThread1(d);

RacyThread2 t2 = new RacyThread2(d);

t1.start();

t2.start();

t1.join();

t2.join();

}

}

There is an obvious race between, for example, the read d.getData() in Thread 1 and d.setData(20) in Thread 2. Yet, when I run the datarace analysis using the following command:

java -cp chord-src-2.1/chord.jar -Dchord.work.dir=project -Dchord.run.analyses=datarace-java -Dchord.kobj.k=3 -Dchord.inst.ctxt.kind=co chord.project.Boot

both the datarace-by-fields and datarace-by-objects HTML turn out to be completely empty. Is the static datarace analysis in Chord unsound? Or am I making some mistake here?

Sincerely,

Suvam.

Programming Languages Lab,

Computer Science and Automation,

Indian Institute of Science, Bangalore.

[Mayur Naik]

Hi Suvam,

I tried the following command with Chord 2.1 and got the two races between getData and setData:

java -cp ./chord.jar -Dchord.work.dir=. -Dchord.run.analyses=datarace-java chord.project.Boot

The only difference is that I did not use these two options in your command: -Dchord.kobj.k=3 -Dchord.inst.ctxt.kind=co

Can you try this and see if you get the desired output?  The default datarace detector is unsound (but that does not seem to be the issue here).  You need to set these options to make it sound (modulo reflection):

chord.datarace.exclude.init=false (to enable reporting races in constructor methods)

chord.datarace.exclude.eqth=false (to enable reporting races between concrete threads that are mapped to the same abstract thread)

These options are explained in RelExcludeInitMethods.java and RelExcludeSameThread.java under src/chord/analyses/datarace/.

-- Mayur

--
You received this message because you are subscribed to the Google Groups "chord-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to chord-discus...@googlegroups.com.
To post to this group, send email to chord-...@googlegroups.com.
Visit this group at http://groups.google.com/group/chord-discuss.
For more options, visit https://groups.google.com/d/optout.

[Suvam Mukherjee]

Hi Mayur,

Thanks for the quick reply!

The command you suggested fixes the issue, and the races are correctly reported.

I had a few additional questions: suppose I create critical sections using volatile variables, as shown below:

volatile boolean flag; // global

Thread 1:

while ( flag == false) {}

//cs

flag = false;

Thread 2:

while ( flag == true) {}

//cs

flag = true

Then the datarace detector fails to detect the synchronisation, and reports races on the volatile variable, as well as on accesses in the critical sections. From your PLDI '06 paper, it seems this behaviour is to be expected. I was wondering if there are newer modifications to the race detector in Chord which supports this, and other synchronisation techniques (like non-syntactically scoped locking, where a.lock() is performed in one function, which calls some other function which performs a.unlock()).

Sincerely,

Suvam.

Programming Languages Lab,

Computer Science and Automation,

Indian Institute of Science, Bangalore.

[Mayur Naik]

Hi Suvam,

There are automated techniques that are more precise than Chord for the below scenario, but that do not scale to large programs.  One example is the Java PathFinder model checker that you could easily run on the below example.  I also believe that there is room to discover new techniques.

As this is an undecidable problem where false positives/negatives will be inevitable, we came up with a different approach to tackle this problem that will appear at FSE'15 (see http://www.cc.gatech.edu/~naik/pubs/fse15a.pdf).  Empirically speaking, this approach suppresses large numbers of false positives for a few false negatives.

Best,

-- Mayur

[Suvam Mukherjee]

Hi Mayur,

Thanks a lot! The paper looks really interesting.

Sincerely,

Suvam.

Programming Languages Lab,

Computer Science and Automation,

Indian Institute of Science, Bangalore.