jpf-concurrent - strange result

[Jan Jirout]

Hello,

Last few week I was working at java hobby project. It's thread safe java.util.Map implementation based on Lehman and Yao algorithm. Project is at https://github.com/jajir/jblinktree.

 

When I finish first implementation I started to think, how to prove that this implementation is thread safe. Later I found JPF and jpf-concurrent module. I created jfp maven module which is part of project at github. Regarding this I have question which I really don't understand. When I run test with disabled jfp-concurrent module test pass successfully, there are no errors. But when I enable jpf-concurrent than test fail with exception at ReentrantLock. 

I would like to ask if there is problem in my code or it's bug in some jpf or in any jpf module?

Thanks

jan

Console report:

====================================================== system under test

application: com/coroptis/TreeTest.java

====================================================== search started: 8/25/15 8:53 AM

Test is done

Test is done

====================================================== error #1

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)

at com.coroptis.jblinktree.JbTreeHelperImpl.insertToLeafNode(JbTreeHelperImpl.java:109)

at com.coroptis.jblinktree.JbTreeImpl.insert(JbTreeImpl.java:81)

at com.coroptis.jblinktree.JbTreeWrapper$1.execute(JbTreeWrapper.java:72)

at com.coroptis.jblinktree.JbTreeWrapper.saveExecution(JbTreeWrapper.java:168)

at com.coroptis.jblinktree.JbTreeWrapper.insert(JbTreeWrapper.java:68)

at com.coroptis.jblinktree.TreeMapImpl.put(TreeMapImpl.java:107)

at com.coroptis.TreeThread.run(TreeThread.java:28)

====================================================== snapshot #1

thread java.lang.Thread:{id:0,name:main,status:WAITING,priority:5,lockCount:0,suspendCount:0}

  waiting on: com.coroptis.TreeThread@2e4

  call stack:

at java.lang.Thread.join(Thread.java)

at com.coroptis.TreeTest.test4(TreeTest.java:27)

at com.coroptis.TreeTest.main(TreeTest.java:16)

thread com.coroptis.TreeThread:{id:1,name:tt1,status:RUNNING,priority:5,lockCount:0,suspendCount:0}

  call stack:

at com.coroptis.jblinktree.JbTreeWrapper.saveExecution(JbTreeWrapper.java:171)

at com.coroptis.jblinktree.JbTreeWrapper.insert(JbTreeWrapper.java:68)

at com.coroptis.jblinktree.TreeMapImpl.put(TreeMapImpl.java:107)

at com.coroptis.TreeThread.run(TreeThread.java:28)

thread com.coroptis.TreeThread:{id:2,name:tt2,status:RUNNING,priority:5,lockCount:0,suspendCount:0}

  call stack:

at java.util.concurrent.locks.ReentrantLock.nativeLock(ReentrantLock.java)

at java.util.concurrent.locks.ReentrantLock.lock(ReentrantLock.java:49)

at com.coroptis.jblinktree.NodeLocks.lockNode(NodeLocks.java:80)

at com.coroptis.jblinktree.NodeStoreImpl.lockNode(NodeStoreImpl.java:54)

at com.coroptis.jblinktree.NodeStoreImpl.getAndLock(NodeStoreImpl.java:73)

at com.coroptis.jblinktree.JbTreeImpl.remove(JbTreeImpl.java:97)

at com.coroptis.jblinktree.JbTreeWrapper$2.execute(JbTreeWrapper.java:84)

at com.coroptis.jblinktree.JbTreeWrapper.saveExecution(JbTreeWrapper.java:168)

at com.coroptis.jblinktree.JbTreeWrapper.remove(JbTreeWrapper.java:80)

at com.coroptis.jblinktree.TreeMapImpl.remove(TreeMapImpl.java:117)

at com.coroptis.TreeThread.run(TreeThread.java:30)

====================================================== results

error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.IllegalMonitorStateException  at java.ut..."

====================================================== statistics

elapsed time:       00:00:02

states:             new=136, visited=84, backtracked=200, end=2

search:             maxDepth=23, constraints hit=0

choice generators:  thread=136 (signal=0, lock=17, shared ref=60), data=0

heap:               new=4224, released=3489, max live=1024, gc-cycles=219

instructions:       518808

max memory:         123MB

loaded code:        classes=144, methods=2118

====================================================== search finished: 8/25/15 8:53 AM

[Nastaran Shafiei]

Hi Jan,

Unfortunately, jpf-concurrent is outdated. It has not been maintained during the past couple of years, and it also has a bug. One of the main porpuse for jpf-concurrent was to provide efficient exploration of conccurent programs through modeling the underlying java.util.concurrent library. Most of the support for Java Concurrency Utilities is part of jpf-core now. 

Thanks,

Nastaran

--

---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Jan Jirout]

Hello Nastaran,

thanks for your reply and explanation.

It's pity that jpf project and associated modules doesn't have corresponding popularity in java community. I believe that it's really great project.

thanks again and best reagards

Jan

--

---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/oj2cwSY9FTY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.