[[Concurrency Tool Comparison]]
== Model Description==

Two versions of a model that deadlocks. The deadlock is caused from a circular lock dependency. 

Classes: 4

SLOC: 24

Parameters: (selector)

== Summary Results Table ==

=== Version A ===
{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | deadlockVersionA ()
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.33s
| 18.78 (0.00)
| 12.29 (11.24)
|-
| JPF Stateless Random Walk
| 10142 (4571) 0.45
| align="right"| NA
| NA (NA)
| NA (NA)
|}

=== Version B ===

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | deadlockVersionB ()
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.27s
| 6.44 (0.00)
| 4.36 (4.00)
|-
| JPF Stateless Random Walk
| 10127 (3844) 0.38
| align="right"| NA
| NA (NA)
| NA (NA)
|}

==Chess==

* ChessBound=2
* ChessMonitorVolatiles=false

{| align=center | border=1 | -bgcolor=grey
! Deadlock Params !! Tests !! Found Error !! Time Taken !! Steps (Depth)
|- 
| 1 || 10     || Yes || 0.94 secs || 20
|}

==CHESS==
{| align=center | border=1 |
|- bgcolor="lightblue"
! Parameters !! Time !!  Transitions !!  paths !!  Max Depth
|-
| 1, 1 || .110 ||  60 ||  3 ||  20
|-
| 1 || .94 || 200 || 10 || 20
|}

==Java Pathfinder==
===Stateless Random Walk===

{| align=center | border=1 | -bgcolor=grey
! Parameters !! Path Error Density
|- 
| 1 || 0.450
|-
| 2 || 0.379
|}

===Stateful Randomized Depth-first search===

* 100 randomized depth-first search trial, where each trial is time-bounded at
one hour. A total of 100 computation hours dedicated in discovering the error. 

* 2 MB of RAM allocated on each machine

* The Error Discovering Trials is the number of trials that discovered an error
among the initially launched trials (100). 
{| align="center" | border=1
|- bgcolor="lightblue"
! Parameters
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
!  abs time (ms)
!  rel. time (ms)
!  search depth
!  errorDepth
!  new states
!  revisited states
!  end states
!  backtracks
!  processed states
!  restored states
!  total memory (kB)
!  max total memory
!  free memory (kB)
!  heap objects
!  max heap objects

|-
|()
| 100 (100) 100.00%
| align="right"| 0.33s
| 18.78 (0.00)
| 12.29 (11.24)
| align="right" | 333.05
| align="right" | 333.05
| align="right" | 12.29
| align="right" | 11.24
| align="right" | 17.06
| align="right" | 1.72
| align="right" | 0.74
| align="right" | 6.54
| align="right" | 4.08
| align="right" | 0.00
| align="right" | 10630.40
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 128.00
| align="right" | 128.00
|-
|()
| 100 (100) 100.00%
| align="right"| 0.27s
| 6.44 (0.00)
| 4.36 (4.00)
| align="right" | 265.34
| align="right" | 265.34
| align="right" | 4.36
| align="right" | 4.00
| align="right" | 6.32
| align="right" | 0.12
| align="right" | 0.60
| align="right" | 1.44
| align="right" | 0.72
| align="right" | 0.00
| align="right" | 10154.88
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 122.00
| align="right" | 122.
|}