[[Concurrency Tool Comparison]]

== Model Description ==

The model exhibits a deadlock caused from a cyclic lock acquisition by a set of threads. 

Classes: 3

SLOC: 66

Parameters: (numOfThreads)

== Summary Results Table ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | accountDeadlock (4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 337.76s
| 13341480.00 (111179.00)
| 120.00 (NA)
|-
| ConTest
| 1000 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | accountDeadlock (5)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 5063 (1684) 0.33
| align="right"| 479.82s
| 7386006.08 (0.00)
| 199.97 (114.10)
|-
| JPF Stateless Random Walk
| 10127 (780) 0.08
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 473.11s
| 20602893.00 (136443.00)
| 151.00 (NA)
|-
| ConTest
| 1000 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|}

''''*'''' Deterministic implementation

''''na'''' Data not output by tool (not available)

'''blank''' Not yet run

'''Hardness''' in a non-deterministic algorithm is the number of
trials that find an error divided by the total number of trials where a
trial is an independent run of the algorithm. For example, if 100
trials are run and 50 of those are successful in finding an error, then
the hardness is reported as 0.50 or 50%.  For deterministic algorithms
(or tools) hardness is either 1 (easy) or 0 (hard).  The time, transitions, and
depth are the average over the successful experiments for
non-deterministic algorithms.

==Chess==

* ChessBound=2
* ChessMonitorVolatiles=true

{| align=center | border=1 | -bgcolor=grey
! Account Params !! Tests !! Found Error !! Time Taken !! Steps (Depth)
|- 
| 4 || 272,034 || Yes (Deadlock) || 1554.581 secs || 176
|-
| 5 || 292,460 || Yes (Deadlock) || 1872.823 secs || 221
|}

* ChessMonitorVolatiles=false

{| align=center | border=1 | -bgcolor=grey
! Account Params !! Tests !! Found Error !! Time Taken !! Steps (Depth)
|- 
| 4 || 111,179 || Yes (Deadlock) || 337.757 secs || 120
|-
| 5 || 136,443 || Yes (Deadlock) || 473.11 secs || 151
|-
|}

==Java PathFinder==
===Stateless Random Walk===

Source is pathErr

* 10,000 Trials of Random Walk
* The ratio of the error discovery trials over the total number of trials is the 

{| 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
|-
|()
| 10127 (780) 7.70%
| align="right"| 0.00s
| 0.00 (0.00)
| 0.00 (0.00)
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
|}

===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). 

Source is error_analysis

{| 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 head objects
|-
|()
| 5063 (1684) 33.26%
| align="right"| 479.82s
| 7386006.08 (0.00)
| 199.97 (114.10)
| align="right" | 479819.03
| align="right" | 5020.64
| align="right" | 199.97
| align="right" | 114.10
| align="right" | 1665631.08
| align="right" | 5720375.00
| align="right" | 10.19
| align="right" | 7386005.08
| align="right" | 1665218.32
| align="right" | 1665218.32
| align="right" | 390486.19
| align="right" | 932096.00
| align="right" | 183307.65
| align="right" | 176.00
| align="right" | 180.98
|}

==ConTest==

* 1000 independent trials

* The ratio of the error discovery trials over the total number of trials is the 
path error density. 

{| align=center | border=1 | -bgcolor=grey
! Account Params !! Path Error Density
|- 
| 4 || 0.000
|- 
| 5 || 0.000
|}