[[Concurrency Tool Comparison]]

== Model Description ==

The model contains a deadlock.

Classes: 4

SLOC: 51

Parameters: (#first, #second, #iter)

== Summary Results Table ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | clean (1,1,12)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 1.54s
| 1742.56 (0.00)
| 161.30 (14.97)
|-
| JPF Stateless Random Walk
| 10125 (336) 0.03
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 0.93s
| 1800.00 (10.00)
| 180.00 (NA)
|-
| ConTest
| 1000 (30) 0.03
| align="right"| NA
| NA (NA)
| NA (NA)
|- bgcolor="white" |
| colspan=5 align="center" | clean (10,10,1)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 114 (110) 0.96
| align="right"| 113.28s
| 1326102.90 (0.00)
| 221.93 (218.74)
|-
| JPF Stateless Random Walk
| 10129 (2928) 0.29
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 100 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|}

==Chess==

* ChessBound=2
* ChessMonitorVolatiles=false

{| align=center | border=1 | -bgcolor=grey
! Clean Params !! Tests !! Found Error !! Time Taken !! Steps (Depth)
|- 
| 1,1,12 || 10 || Yes  || 0.93 secs || 180
|-
| 10,10,1 || >=398,000 || No || 3604.715 secs || 242
|}

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

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


{| align=center | border=1 | -bgcolor=grey
! Clean Params !! Path Error Density
|- 
| 1,1,12 || 0.033
|-
| 10,10,1 || 0.289
|}




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

|-
|(1,1,12)
| 100 (100) 100.00%
| align="right"| 1.54s
| 1742.56 (0.00)
| 161.30 (14.97)
| align="right" | 1539.79
| align="right" | 1539.79
| align="right" | 161.30
| align="right" | 14.97
| align="right" | 906.75
| align="right" | 835.81
| align="right" | 0.96
| align="right" | 1726.59
| align="right" | 889.82
| align="right" | 0.00
| align="right" | 17153.92
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 138.00
| align="right" | 149.00
|-
|(10,10,1)
| 114 (110) 96.49%
| align="right"| 113.28s
| 1326102.90 (0.00)
| 221.93 (218.74)
| align="right" | 113278.95
| align="right" | 3154.25
| align="right" | 221.93
| align="right" | 218.74
| align="right" | 281078.65
| align="right" | 1045024.25
| align="right" | 0.60
| align="right" | 1325883.16
| align="right" | 280858.31
| align="right" | 0.00
| align="right" | 452811.64
| align="right" | 6990528.00
| align="right" | 163324.80
| align="right" | 210.00
| align="right" | 221.00
|}




==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
! Clean Params !! Path Error Density
|- 
| 1,1,12 || 0.030
|-
| 10,10,1 || ? (not-halt or deadlock)
|}

==CalFuzzer==

Not Applicable. The initial dynamic analysis does not find any input
target locations.