JPF is tool for static code analysis. I tried to use it for proving that code is thread safe. In multiple thread environment is problem with JVM 'state explosion'. When JPF try to examine all possible JVM states in multiple thread environment number of possible states grow exorbitantly. As documentation say this problem could be solved with module jpf-concurrent.
Because I didn't find guide how to install it here is simple guide.
Prerequisites
- linux/unix system, in my case it's Mac OSX
- Installed mercurial SCM
- Installed Apache ANT
- Installed jpf-core
Installation steps
- Go to directory where is jpf-core installed. In my case it's directory '/Users/jan/projects/jpf/'
- Checkout project
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-concurrent
- Build jpf-concurrent project
ant
- Edit your site property file. In my case is at '/Users/jan/.jpf/site.properties'. Add there following section:
# concurrent extension jpf-concurrent = ${jpf.home}/jpf-concurrent extensions+=,${jpf-concurrent}
[EDIT] - After some time of using jpf-concurrent project I had following problem:
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty java.lang.IllegalMonitorStateException at java.util.concurrent.locks.ReentrantLock.unlock(gov.nasa.jpf.concurrent.peers.JPF_java_util_concurrent_locks_ReentrantLock) at com.coroptis.jblinktree.NodeLocks.unlockNode(NodeLocks.java:96) at com.coroptis.jblinktree.NodeStoreImpl.unlockNode(NodeStoreImpl.java:59)
I contacted Nastaran Shafiei via google group, he is creator of jpf-concurrent. He told me, that jpf-concurrent module is outdated and no longer supported. So I removed jpf-concurrent module and path finder start work fine.
