[Javapathfinder-user] necessary locks

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

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