Re: [Javapathfinder-user] necessary locks

[Dusty P. <bu...@gm...>]

On 24/11/05, Willem Visser <wv...@em...> wrote:
> Hi Dusty,
>
> Add a -show to the command line to see which options are being loaded. Yo=
u
> don't need to do a -c option if you add it to jpf.properties (it loads th=
at
> by default). Actually also add a +config.level=3Dconfig (I think this is =
the
> command) to the command line  and that will tell you where the properties
> gets loaded from.

Hi Willem,

I'm still having trouble detecting a race condition. I wrote a simple
test that looks like a race condition:
public class RaceCond {
    public int theInt;
    public static void main(String[] args) {
        RaceCond raceCond =3D new RaceCond();
        raceCond.theInt =3D 10;
        new t1(raceCond).start();
        new t2(raceCond).start();
  }
}
class t1 extends Thread {
    private RaceCond racer;
    public t1(RaceCond blah) {
        racer =3D blah;
    }
    public void run() {
        racer.theInt++;
    }
}

class t2 is the same as t1, but decrements the value instead.

So I put this in my jpf.properties:

   listener =3D gov.nasa.jpf.tools.RaceDetector

When I run it it tells me no errors found, although I think the class
above is an obvious race condition. Am I defining 'race condition' too
simply (I need something more complicated than above?) or am I not
implementing the listener correctly?

Sorry to keep pestering you with these questions. I think I understand
what JPF is doing, but not necessarily how to control it! :-D I've
been browsing through the sources to get a better understanding, but
there are still gaps in my knowledge to actually get started using it.

Thanks again,
Dusty