JavaPathfinder v6.0 (rev 652+) - (C) RIACS/NASA Ames Research Center


====================================================== system under test
application: AlarmClock/AlarmClock.java
arguments:   8 

====================================================== search started: 1/20/12 7:24 AM

====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field AlarmClock.MyLinkedList@146.size
  Clock0 at AlarmClock.MyLinkedList.removeElementAt(AlarmClock.java:295)
"  : putfield
  Client1 at AlarmClock.MyLinkedList.getLock(AlarmClock.java:339)
"  : getfield


====================================================== snapshot #1
thread AlarmClock.Clock:{id:1,name:Clock0,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  owned locks:AlarmClock.Monitor@142
  call stack:
	at AlarmClock.MyLinkedList.removeElementAt(AlarmClock.java:297)
	at AlarmClock.Monitor.tick(AlarmClock.java:145)
	at AlarmClock.Clock.run(AlarmClock.java:70)

thread AlarmClock.Client:{id:2,name:Client1,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:
	at AlarmClock.MyLinkedList.getLock(AlarmClock.java:339)
	at AlarmClock.Monitor.wakeme(AlarmClock.java:191)
	at AlarmClock.Client.run(AlarmClock.java:106)

thread AlarmClock.Client:{id:3,name:Client2,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread AlarmClock.Client:{id:4,name:Client3,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread AlarmClock.Client:{id:5,name:Client4,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread AlarmClock.Client:{id:6,name:Client5,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread AlarmClock.Client:{id:7,name:Client6,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread AlarmClock.Client:{id:8,name:Client7,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:

thread AlarmClock.Client:{id:9,name:Client8,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
  call stack:


====================================================== results
error #1: gov.nasa.jpf.listener.PreciseRaceDetector "race for field AlarmClock.MyLinkedList@146.size   ..."

====================================================== statistics
elapsed time:       00:31:27
states:             new=883094, visited=4246135, backtracked=5129183, end=84
search:             maxDepth=77, constraints hit=0
choice generators:  thread=883092 (signal=0, lock=663636, shared ref=133356), data=0
heap:               new=1810720, released=5340218, max live=411, gc-cycles=5129229
instructions:       59147809
max memory:         107MB
loaded code:        classes=91, methods=1374

====================================================== search finished: 1/20/12 7:55 AM