Re: [Javapathfinder-user] necessary locks

[Willem V. <wv...@em...>]

Hi Dusty,

Add a -show to the command line to see which options are being loaded. You
don't need to do a -c option if you add it to jpf.properties (it loads that
by default). Actually also add a +config.level=config (I think this is the
command) to the command line  and that will tell you where the properties
gets loaded from.

To see progress you should add the SearchMonitor for sure.

Also if JPF seems to hang that can definitely be the 1.5 issue - it does go
into and endless loop if run on 1.5 library code. This will soon be fixed
but it is not yet in the CVS version.

Bye,
Willem

----- Original Message ----- 
From: "Dusty Phillips" <bu...@gm...>
To: <wv...@em...>
Cc: <Jav...@li...>
Sent: Wednesday, November 23, 2005 8:27 PM
Subject: Re: [Javapathfinder-user] necessary locks


> Hi Willem,
>
> Thanks for the advice. I can tell this is what I want, but I'm not
> sure how to make it work.
>
> I've created a jpf. properties and have added
> listener=gov.nasa.jpf.tools.RaceDetector to it. I pass this properties
> using jpf -c. Is that all I need to make it work? It doesn't seem to
> change anything one way or the other.
>
> Possibly on a related topic, I frequently run JPF and it doesn't
> terminate. I assume the state space is too big, but maybe there is
> another problem. I was wondering how I can tell if JPF is making
> progress. I tried adding a
> search.listener=gov.nasa.jpf.tools.SearchMonitor to my jpf.properties,
> but it doesn't seem to add any output. Is this not the tool I want?
>
> I read on the forum that Java 1.5 and BCEL were not playing well on
> July 13
(http://sourceforge.net/forum/forum.php?thread_id=1317153&forum_id=461881).
> Is this still the case? Would that be causing my problems?
>
> I think I'm just having trouble getting started here. :-)
>
> Thanks,
> Dusty
>
> On 21/11/05, Willem Visser <wv...@em...> wrote:
> > Hi Dusty,
> >
> > Use the RaceDetector listener in the tools directory - it will tell you
> > if there is a race violation possible on the queue without the locks.
> >
> > Bye,
> > Willem
> >
> > --
> > Willem C. Visser                 Automated Software Engineering Group
> > RIACS/NASA Ames Research Center            wv...@em...
> > M/S 269-2                                     http://ase.arc.nasa.gov
> > Moffett Field, CA 94035                (650)604-3515 fax 4036  rm 235
> >
> >
> > > -----Original Message-----
> > > From: jav...@li...
> > > [mailto:jav...@li...] On Behalf Of
> > > Dusty Phillips
> > > Sent: Saturday, November 19, 2005 2:00 PM
> > > To: Jav...@li...
> > > Subject: [Javapathfinder-user] necessary locks
> > >
> > > Hello,
> > >
> > > I'm just starting to understand how to use Java Pathfinder (got the
> > > cvs version working). So far I've been implementing a model and
> > > running it in JPF without writing extra properties or using the Verify
> > > class, though I intend to add these eventually.
> > >
> > > I was wondering if it would be possible using JPF to test whether or
> > > not a specific lock is needed. For example, I've implemented a
> > > concurrently accessible queue with synchronized methods for offering
> > > and polling objects. From the design of the rest of the model, I can't
> > > tell if this queue is ever actually accesed concurrently. I think that
> > > at worst, it may be written by one process while another process is
> > > reading it. Is there some way to write a property to test whether or
> > > not this happens?
> > >
> > > This isn't a deadlock issue, so I don't think the default deadlock
> > > property will do what I want. I'm not sure where to start when it
> > > comes to writing properties or otherwise customizing JPF.
> > >
> > > Thank you,
> > >
> > > Dusty
> > >
> > >
> > > -------------------------------------------------------
> > > This SF.Net email is sponsored by the JBoss Inc.  Get Certified Today
> > > Register for a JBoss Training Course.  Free Certification Exam
> > > for All Training Attendees Through End of 2005. For more info visit:
> > > http://ads.osdn.com/?ad_idv28&alloc_id845&opÌk
> > > _______________________________________________
> > > Javapathfinder-user mailing list
> > > Jav...@li...
> > > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
> >
> >
> >
>