Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:wronglock [2015/02/18 23:01] (current)
egm created
Line 1: Line 1:
 +[[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
 +|}
vv-lab/wronglock.txt ยท Last modified: 2015/02/18 23:01 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0