[[Concurrency Tool Comparison]]

== Model Description ==

The Wronglock model contains an error that is caused when two different kinds of threads do not obtain the same lock instance. One type of thread requests a lock on the field object of a class while another type of thread requests a lock on the class containing the field. 

Classes:4

SLOC: 38

== Summary Results Table ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | #wronglock (10,1)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4999 (4999) 1.00
| align="right"| 1.07s
| 115.71 (0.00)
| 77.86 (77.17)
|- bgcolor="white" |
| colspan=5 align="center" |  (1,1)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4999 (4999) 1.00
| align="right"| 1.07s
| 115.71 (0.00)
| 77.86 (77.17)
|-
| JPF Stateless Random Walk
| 10129 (4842) 0.48
| align="right"| 0.03s
| 2.94 (NA)
| 0.00 (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 1000 (323) 0.32
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (12) 0.12
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 1.47s
| 1058.00 (NA)
| 165.00 (165.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (1,1)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4998 (4998) 1.00
| align="right"| 0.84s
| 28.04 (0.00)
| 14.33 (14.16)
|-
| JPF Stateless Random Walk
| 10126 (694) 0.07
| align="right"| 0.55s
| 13.08 (NA)
| 0.00 (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 0.94s
| 198.00 (9.00)
| 22.00 (NA)
|-
| ConTest
| 1000 (110) 0.11
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (8) 0.08
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 65.00 (NA)
| 31.00 (31.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (1,10)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 5000 (5000) 1.00
| align="right"| 750.10s
| 11215820.05 (0.00)
| 59.84 (35.92)
|-
| JPF Stateless Random Walk
| 10128 (2027) 0.20
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 1000 (243) 0.24
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (11) 0.11
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 65.00 (NA)
| 31.00 (31.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (1,2)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.43s
| 183.05 (0.00)
| 25.92 (25.67)
|-
| JPF Stateless Random Walk
| 214 (33) 0.15
| align="right"| 0.09s
| 11.09 (NA)
| 0.00 (NA)
|-
| CHESS
| 1 (1) 1.00
| align="right"| 0.50s
| 3000.00 (100.00)
| 30.00 (NA)
|-
| ConTest
| 1000 (220) 0.22
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (7) 0.07
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 65.00 (NA)
| 31.00 (31.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (1,20)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4998 (1000) 0.20
| align="right"| 0.92s
| 41.58 (0.00)
| 40.58 (40.58)
|-
| JPF Stateless Random Walk
| 10128 (2063) 0.20
| align="right"| 0.01s
| 0.01 (NA)
| 0.00 (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 1000 (220) 0.22
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (11) 0.11
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 65.00 (NA)
| 31.00 (31.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (1,5)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 5.68s
| 29213.92 (0.00)
| 46.40 (33.47)
|-
| JPF Stateless Random Walk
| 201 (24) 0.12
| align="right"| 0.02s
| 1.83 (NA)
| 0.00 (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 1000 (230) 0.23
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (8) 0.08
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 65.00 (NA)
| 31.00 (31.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (1,6)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 16.46s
| 159284.08 (0.00)
| 53.34 (34.06)
|-
| JPF Stateless Random Walk
| 200 (28) 0.14
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 1000 (250) 0.25
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (9) 0.09
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 65.00 (NA)
| 31.00 (31.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (10,1)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4999 (4999) 1.00
| align="right"| 1.07s
| 115.71 (0.00)
| 77.86 (77.17)
|-
| JPF Stateless Random Walk
| 10129 (4842) 0.48
| align="right"| 0.03s
| 2.94 (NA)
| 0.00 (NA)
|-
| CHESS
| 1 (0) 0.00
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| ConTest
| 1000 (323) 0.32
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (12) 0.12
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 1.47s
| 1058.00 (NA)
| 165.00 (165.00)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (20,1)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 1.37s
| 1250.24 (0.00)
| 146.12 (145.05)
|- bgcolor="white" |
| colspan=5 align="center" | wronglock (5,5)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 1.52s
| 6603.42 (0.00)
| 80.39 (72.36)
|-
| JPF Stateless Random Walk
| 202 (93) 0.46
| align="right"| 0.01s
| 2.13 (NA)
| 0.00 (NA)
|-
| ConTest
| 1000 (510) 0.51
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| CalFuzzer
| 100 (29) 0.29
| align="right"| NA
| NA (NA)
| NA (NA)
|-
| JPF "Abstraction Guided Refinement"
| 1 (1) 1.00
| align="right"| 0.47s
| 361.00 (NA)
| 91.00 (91.00)
|}

==Chess==

* ChessBound=2
* ChessMonitorVolatiles=true

{| align=center | border=1 | -bgcolor=grey
! Wronglock Params !! Tests !! Found Error !! Time Taken !! Steps (Depth)
|- 
| 1,1 || 9     || Yes || 0.94 secs || 22
|-
| 1,2 || >=100 || Yes || 0.499 secs || 30
|- 
| 1,5 || >=668,000 || No || 3600.331 secs || 54
|-
| 1,6 || >=620,000 || No || 3603.967 secs || 62
|}

==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
! Wronglock Params !! Path Error Density
|- 
| 1,1 || 0.068
|-
| 1,10 || 0.200
|-
| 1,20 || 0.204
|-
| 10,1 || 0.478
|-
| 1,10 || 0.200
|}

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

|-
|(10,1)
| 4999 (4999) 100.00%
| align="right"| 1.07s
| 115.71 (0.00)
| 77.86 (77.17)
| align="right" | 1065.53
| align="right" | 1065.53
| align="right" | 77.86
| align="right" | 77.17
| align="right" | 95.24
| align="right" | 20.47
| align="right" | 0.80
| align="right" | 37.54
| align="right" | 16.54
| align="right" | 0.00
| align="right" | 13528.85
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 204.02
| align="right" | 204.02
|-
|(1,1)
| 4998 (4998) 100.00%
| align="right"| 0.84s
| 28.04 (0.00)
| 14.33 (14.16)
| align="right" | 835.85
| align="right" | 835.85
| align="right" | 14.33
| align="right" | 14.16
| align="right" | 23.85
| align="right" | 4.18
| align="right" | 1.93
| align="right" | 12.87
| align="right" | 7.76
| align="right" | 0.00
| align="right" | 13488.24
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 168.05
| align="right" | 168.05
|-
|(1,2)
| 100 (100) 100.00%
| align="right"| 0.43s
| 183.05 (0.00)
| 25.92 (25.67)
| align="right" | 429.97
| align="right" | 429.97
| align="right" | 25.92
| align="right" | 25.67
| align="right" | 103.49
| align="right" | 79.56
| align="right" | 1.41
| align="right" | 156.38
| align="right" | 75.92
| align="right" | 0.00
| align="right" | 21349.76
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 248.00
| align="right" | 248.00
|-
|(1,5)
| 100 (100) 100.00%
| align="right"| 5.68s
| 29213.92 (0.00)
| 46.40 (33.47)
| align="right" | 5683.89
| align="right" | 5583.89
| align="right" | 46.40
| align="right" | 33.47
| align="right" | 7557.23
| align="right" | 21656.69
| align="right" | 0.88
| align="right" | 29179.45
| align="right" | 7521.89
| align="right" | 0.00
| align="right" | 54645.12
| align="right" | 932096.00
| align="right" | 290.14
| align="right" | 269.05
| align="right" | 273.63
|-
|(1,6)
| 100 (100) 100.00%
| align="right"| 16.46s
| 159284.08 (0.00)
| 53.34 (34.06)
| align="right" | 16464.24
| align="right" | 3663.20
| align="right" | 53.34
| align="right" | 34.06
| align="right" | 32999.12
| align="right" | 126284.96
| align="right" | 0.86
| align="right" | 159249.02
| align="right" | 32963.22
| align="right" | 0.00
| align="right" | 91546.24
| align="right" | 932096.00
| align="right" | 34514.31
| align="right" | 270.38
| align="right" | 276.64
|-
|(20,1)
| 100 (100) 100.00%
| align="right"| 1.37s
| 1250.24 (0.00)
| 146.12 (145.05)
| align="right" | 1371.52
| align="right" | 1371.52
| align="right" | 146.12
| align="right" | 145.05
| align="right" | 375.75
| align="right" | 874.49
| align="right" | 0.83
| align="right" | 1104.19
| align="right" | 229.16
| align="right" | 0.00
| align="right" | 18414.08
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 244.00
| align="right" | 244.00
|-
|(1,10)
| 5000 (5000) 100.00%
| align="right"| 750.10s
| 11215820.05 (0.00)
| 59.84 (35.92)
| align="right" | 750095.95
| align="right" | 4111.95
| align="right" | 59.84
| align="right" | 35.92
| align="right" | 1463916.50
| align="right" | 9751903.55
| align="right" | 0.80
| align="right" | 11215783.12
| align="right" | 1463878.78
| align="right" | 0.00
| align="right" | 294585.37
| align="right" | 932096.00
| align="right" | 132550.75
| align="right" | 195.71
| align="right" | 195.93
|-
|(1,20)
| 4998 (1000) 20.01%
| align="right"| 0.92s
| 41.58 (0.00)
| 40.58 (40.58)
| align="right" | 919.08
| align="right" | 919.08
| align="right" | 40.58
| align="right" | 40.58
| align="right" | 41.58
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 16141.82
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 199.19
| align="right" | 199.19
|-
|(5,5)
| 100 (100) 100.00%
| align="right"| 1.52s
| 6603.42 (0.00)
| 80.39 (72.36)
| align="right" | 1520.25
| align="right" | 1520.25
| align="right" | 80.39
| align="right" | 72.36
| align="right" | 1704.33
| align="right" | 4899.09
| align="right" | 0.50
| align="right" | 6530.06
| align="right" | 1630.52
| align="right" | 0.00
| align="right" | 31015.04
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 291.57
| align="right" | 291.65
|-
|(10,1)
| 4999 (4999) 100.00%
| align="right"| 1.07s
| 115.71 (0.00)
| 77.86 (77.17)
| align="right" | 1065.53
| align="right" | 1065.53
| align="right" | 77.86
| align="right" | 77.17
| align="right" | 95.24
| align="right" | 20.47
| align="right" | 0.80
| align="right" | 37.54
| align="right" | 16.54
| align="right" | 0.00
| align="right" | 13528.85
| align="right" | 932096.00
| align="right" | 0.00
| align="right" | 204.02
| align="right" | 204.02
|}


==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
! Wronglock Params !! Path Error Density
|- 
| 1,1 || 0.11
|-
| 1,2 || 0.22
|-
| 1,5 || 0.23
|-
| 1,6 || 0.25
|-
| 5,5 || 0.51
|- 
| 1,10 || 0.243
|-
| 10,1 || 0.323
|- 
| 1,20 || 0.22
|}

==CalFuzzer==

* 100 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
! Wronglock Params !! Path Error Density
|- 
| 1,1 || 0.08
|- 
| 1,2 || 0.07
|- 
| 1,5 || 0.08
|- 
| 1,6 || 0.09
|-
| 5,5 || 0.29
|- 
| 1,10 || 0.11
|-
| 10,1 || 0.12
|- 
| 1,20 || 0.11
|}