Concurrency Tool Comparison

Model Description

The model manifests a data race when a set of thread reads from a shared variable while another thread is writing to the same object.

Classes: 6

SLOC: 91

Parameters: (#PersonalAccounts, #BusinessAccounts)

Summary Results Table

  1. accountsubtype (20,1)

|- bgcolor=“lightblue”

Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (3) 0.00 74.91s 626362.67 (0.00) 621.00 (580.33)
accountsubtype (1,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.01s 122.36 (0.00) 64.71 (61.16)
CHESS 1 (1) 1.00 0.34s 5280.00 (60.00) 88.00 (NA)
ConTest 1000 (13) 0.01 NA NA (NA) NA (NA)
CalFuzzer 1000 (730) 0.73 NA NA (NA) NA (NA)
accountsubtype (1,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
CHESS 1 (1) 1.00 4.85s 116100.00 (900.00) 129.00 (NA)
ConTest 1000 (80) 0.08 NA NA (NA) NA (NA)
CalFuzzer 1000 (1000) 1.00 NA NA (NA) NA (NA)
accountsubtype (10,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (931) 0.19 211.03s 2437012.58 (0.00) 328.01 (312.45)
JPF Stateless Random Walk 10124 (815) 0.08 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (13) 0.01 NA NA (NA) NA (NA)
CalFuzzer 1000 (720) 0.72 NA NA (NA) NA (NA)
accountsubtype (11,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (584) 0.12 286.22s 3179153.11 (0.00) 356.39 (340.48)
JPF Stateless Random Walk 10116 (531) 0.05 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
CalFuzzer 1000 (680) 0.68 NA NA (NA) NA (NA)
accountsubtype (2,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
CHESS 1 (1) 1.00 64.58s 1596000.00 (12000.00) 133.00 (NA)
ConTest 1000 (15) 0.02 NA NA (NA) NA (NA)
CalFuzzer 1000 (680) 0.68 NA NA (NA) NA (NA)
accountsubtype (2,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.17s 359.13 (0.00) 135.38 (132.10)
accountsubtype (20,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (3) 0.00 74.91s 626362.67 (0.00) 621.00 (580.33)
JPF Stateless Random Walk 10126 (2) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
CalFuzzer 1000 (670) 0.67 NA NA (NA) NA (NA)
accountsubtype (5,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (10) 0.01 NA NA (NA) NA (NA)
CalFuzzer 1000 (660) 0.66 NA NA (NA) NA (NA)
accountsubtype (5,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
ConTest 1000 (270) 0.27 NA NA (NA) NA (NA)
CalFuzzer 1000 (1000) 1.00 NA NA (NA) NA (NA)
accountsubtype (8,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (1986) 0.40 256.71s 3154370.20 (0.00) 271.04 (257.72)
JPF Stateless Random Walk 10126 (1538) 0.15 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (12) 0.01 NA NA (NA) NA (NA)
CalFuzzer 1000 (700) 0.70 NA NA (NA) NA (NA)
accountsubtype (8,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (4957) 0.99 27.88s 316964.83 (0.00) 312.38 (304.05)
JPF Stateless Random Walk 10126 (5168) 0.51 NA NA (NA) NA (NA)
ConTest 1000 (110) 0.11 NA NA (NA) NA (NA)
CalFuzzer 1000 (1000) 1.00 NA NA (NA) NA (NA)
accountsubtype (8,8)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (5000) 1.00 1.50s 1206.08 (0.00) 557.65 (557.25)
JPF Stateless Random Walk 10127 (9942) 0.98 NA NA (NA) NA (NA)
ConTest 1000 (380) 0.38 NA NA (NA) NA (NA)
CalFuzzer 1000 (1000) 1.00 NA NA (NA) NA (NA)
accountsubtype (9,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (1422) 0.28 285.10s 3369017.81 (0.00) 300.13 (284.94)
JPF Stateless Random Walk 10124 (1068) 0.11 NA NA (NA) NA (NA)
ConTest 1000 (12) 0.01 NA NA (NA) NA (NA)
CalFuzzer 1000 (700) 0.70 NA NA (NA) NA (NA)

'*' Deterministic implementation

'-' No data to report as tool failed to find error

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

blank Not yet run

Hardness

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.

Transitions

  • CHESS: computed as the number of paths times the depth
  • JPF: computed as the number of states plus the number of revisited states

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=true
AccountSubtype Params Tests Found Error Time Taken Steps (Depth)
1,1 >=60 Yes 0.343 secs 88
1,2 >=900 Yes 4.852 secs 129
2,1 >=12,000 Yes 64.584 secs 133
5,1 >=491,000 No 3600.456 secs 268
8,1 >-391,000 No 3601.423 secs 403
10,1 >=673,000 No 7209.165 secs 493

Java PathFinder

Stateless Random Walk

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) 10124 (815) 8.05% 1.28s 316.91 (0.00) 0.00 (0.00) 1282.34 1282.34 0.00 0.00 316.91 0.00 0.00 0.00 0.00 0.00 12371.24 932096.00 0.00 228.00 228.00
(11,1) 10116 (531) 5.25% 1.27s 344.37 (0.00) 0.00 (0.00) 1271.48 1271.48 0.00 0.00 344.37 0.00 0.00 0.00 0.00 0.00 12780.60 932096.00 0.00 235.00 235.00
(8,1) 10126 (1538) 15.19% 0.91s 261.14 (0.00) 0.00 (0.00) 910.58 910.58 0.00 0.00 261.14 0.00 0.00 0.00 0.00 0.00 14698.82 932096.00 0.00 214.00 214.00
(8,2) 10126 (5168) 51.04% 1.30s 309.53 (0.00) 0.00 (0.00) 1303.24 1303.24 0.00 0.00 309.53 0.00 0.00 0.00 0.00 0.00 11760.11 932096.00 0.00 221.00 221.00
(8,8) 10127 (9942) 98.17% 1.76s 557.81 (0.00) 0.00 (0.00) 1757.50 1757.50 0.00 0.00 557.81 0.00 0.00 0.00 0.00 0.00 16175.35 932096.00 0.00 263.00 263.00
(20,1) 10126 (2) 0.02% 2.61s 590.50 (0.00) 0.00 (0.00) 2606.00 2606.00 0.00 0.00 590.50 0.00 0.00 0.00 0.00 0.00 20352.00 932096.00 0.00 298.00 298.00
(9,1) 10124 (1068) 10.55% 1.23s 289.09 (0.00) 0.00 (0.00) 1230.36 1230.36 0.00 0.00 289.09 0.00 0.00 0.00 0.00 0.00 12467.72 932096.00 0.00 221.00 221.00
  • 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).

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) 5000 (931) 18.62% 211.03s 2437012.58 (0.00) 328.01 (312.45) 211031.46 3032.36 328.01 312.45 432510.58 2004502.00 1.56 2436699.13 432196.58 0.00 156919.20 932096.00 63601.53 248.00 248.00
(20,1) 5000 (3) 0.06% 74.91s 626362.67 (0.00) 621.00 (580.33) 74906.67 4906.67 621.00 580.33 131921.33 494441.33 1.67 625781.33 131339.33 0.00 248981.33 932096.00 153579.33 318.00 318.00
(11,1) 4999 (584) 11.68% 286.22s 3179153.11 (0.00) 356.39 (340.48) 286218.75 3170.55 356.39 340.48 554758.12 2624395.00 1.52 3178811.63 554416.11 0.00 162449.64 932096.00 66486.34 255.00 255.00
(1,1) 100 (100) 100.00% 1.01s 122.36 (0.00) 64.71 (61.16) 1006.42 1006.42 64.71 61.16 97.66 24.70 1.56 60.20 34.94 0.00 16581.12 6990528.00 0.00 185.00 185.00
(8,1) 5000 (1986) 39.72% 256.71s 3154370.20 (0.00) 271.04 (257.72) 256712.01 3167.19 271.04 257.72 556990.73 2597379.47 1.62 3154111.48 556731.40 0.00 167893.78 932096.00 72185.19 234.00 234.00
(8,2) 5000 (4957) 99.14% 27.88s 316964.83 (0.00) 312.38 (304.05) 27881.65 2204.46 312.38 304.05 55864.49 261100.34 1.48 316659.78 55558.96 0.00 56404.08 932096.00 14745.03 241.00 241.00
(8,8) 5000 (5000) 100.00% 1.50s 1206.08 (0.00) 557.65 (557.25) 1495.24 1441.24 557.65 557.25 709.95 496.14 1.02 647.83 151.68 0.00 17889.01 932096.00 151.20 283.00 283.00
(20,1) 5000 (3) 0.06% 74.91s 626362.67 (0.00) 621.00 (580.33) 74906.67 4906.67 621.00 580.33 131921.33 494441.33 1.67 625781.33 131339.33 0.00 248981.33 932096.00 153579.33 318.00 318.00
(2,2) 100 (100) 100.00% 1.17s 359.13 (0.00) 135.38 (132.10) 1171.33 1171.33 135.38 132.10 224.98 134.15 1.37 226.03 91.51 0.00 16812.80 6990528.00 0.00 199.00 199.00
(9,1) 4999 (1422) 28.45% 285.10s 3369017.81 (0.00) 300.13 (284.94) 285097.42 3288.38 300.13 284.94 589956.73 2779061.08 1.61 3368731.87 589670.18 0.00 175321.11 932096.00 75030.19 241.00 241.00

ConTest

  • 100 to 1000 independent trials
  • The ratio of the error discovery trials over the total number of trials is the

path error density.

AccountSubtype Params Path Error Density
1,1 0.013
2,1 0.015
1,2 0.08
5,1 0.01
5,5 0.27
8,1 0.012
9,1 0.012
8,2 0.11
8,8 0.38
10,1 0.013
11,1 0.000
20,1 0.000

CalFuzzer

  • 100 to 1000 independent trials
  • The ratio of the error discovery trials over the total number of trials is the

path error density.

AccountSubtype Params Path Error Density
1,1 0.73
2,1 0.68
1,2 1.00
5,1 0.66
5,5 1.00
8,1 0.70
9,1 0.70
8,2 1.00
8,8 1.00
10,1 0.72
11,1 0.68
20,1 0.67
vv-lab/accountsubtype.txt · Last modified: 2015/02/18 22:52 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