Re: [Javapathfinder-user] necessary locks

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

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=3Dgov.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=3Dgov.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=3D1317153&forum_i=
d=3D461881).
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_id=16845&op=CCk
> > _______________________________________________
> > Javapathfinder-user mailing list
> > Jav...@li...
> > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>
>
>