Concurrency Tool Comparison

Model Description

The benchmark contains a data race. There is a check whether the data race causes an inconsistency in the data values. When such an inconsistency is discovered an exception is raised. The benchmark contains two kinds of threads: setter and getterwhich is the source of the data race. The getter thread also checks for the inconsistency in the data values that are caused by the data race. As we increase the number of setter threads while keeping the getter thread constant, the semantic measure of the hardness in error discovery increases (i.e., get harder) as shown in Hardness for Explicit State Software Model Checking Benchmarks paper.

Classes: 4

SLOC: 44

Summary Results Table

reorder (1,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.78s 83.69 (0.00) 18.32 (15.64)
JPF Stateless Random Walk 10125 (307) 0.03 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 0.78s 95.00 (5.00) 19.00 (NA)
ConTest 1000 (61) 0.06 NA NA (NA) NA (NA)
CalFuzzer 100 (6) 0.06 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.67s 29.00 (NA) 12.00 (12.00)
reorder (1,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 16.61s 238450.80 (0.00) 52.94 (25.52)
JPF Stateless Random Walk 10128 (438) 0.04 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (285) 0.28 NA NA (NA) NA (NA)
CalFuzzer 100 (8) 0.08 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.67s 29.00 (NA) 12.00 (12.00)
reorder (10,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (4) 0.00 2414.82s 38022689.25 (0.00) 89.75 (65.25)
JPF Stateless Random Walk 10127 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
CalFuzzer 100 (9) 0.09 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 236.00 (NA) 30.00 (30.00)
reorder (2,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.61s 560.58 (0.00) 28.33 (21.24)
JPF Stateless Random Walk 1000 (2) 0.00 0.28s 27.50 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 0.44s 2600.00 (100.00) 26.00 (NA)
ConTest 1000 (23) 0.02 NA NA (NA) NA (NA)
CalFuzzer 100 (12) 0.12 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 44.00 (NA) 14.00 (14.00)
reorder (3,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.21s 3867.01 (0.00) 36.96 (27.26)
JPF Stateless Random Walk 1000 (1) 0.00 0.21s 39.00 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 8.55s 66000.00 (2000.00) 33.00 (NA)
ConTest 1000 (7) 0.01 NA NA (NA) NA (NA)
CalFuzzer 100 (11) 0.11 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 61.00 (NA) 16.00 (16.00)
reorder (3,3)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 24.10s 216430.64 (0.00) 57.72 (29.79)
CHESS 1 (1) 1.00 3454.61s 33516000.00 (684000.00) 49.00 (NA)
ConTest 1000 (20) 0.02 NA NA (NA) NA (NA)
CalFuzzer 100 (36) 0.36 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 61.00 (NA) 16.00 (16.00)
reorder (4,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 7.35s 33895.58 (0.00) 46.61 (34.29)
JPF Stateless Random Walk 1000 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 140.53s 1200000.00 (30000.00) 40.00 (NA)
ConTest 1000 (3) 0.00 NA NA (NA) NA (NA)
CalFuzzer 100 (12) 0.12 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 80.00 (NA) 18.00 (18.00)
reorder (4,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 19.46s 170146.30 (0.00) 56.39 (36.93)
JPF Stateless Random Walk 1000 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 2836.43s 26640000.00 (555000.00) 48.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
CalFuzzer 100 (10) 0.10 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 80.00 (NA) 18.00 (18.00)
reorder (5,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 9.98s 107466.97 (0.00) 49.72 (37.57)
JPF Stateless Random Walk 10128 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 2275.93s 20633000.00 (439000.00) 47.00 (NA)
ConTest 1000 (3) 0.00 NA NA (NA) NA (NA)
CalFuzzer 100 (12) 0.12 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 101.00 (NA) 20.00 (20.00)
reorder (5,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 85.43s 996758.65 (0.00) 65.17 (42.90)
JPF Stateless Random Walk 1000 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (10) 0.01 NA NA (NA) NA (NA)
CalFuzzer 100 (24) 0.24 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 101.00 (NA) 20.00 (20.00)
reorder (5,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 117 (2) 0.02 2206.74s 31429172.50 (0.00) 86.00 (44.00)
reorder (6,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 73.05s 833413.61 (0.00) 64.44 (46.18)
JPF Stateless Random Walk 1000 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
CalFuzzer 100 (10) 0.10 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 124.00 (NA) 22.00 (22.00)
reorder (7,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (5000) 1.00 213.90s 3586188.11 (0.00) 65.62 (48.65)
reorder (8,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (5000) 1.00 1225.99s 20078513.07 (0.00) 73.59 (54.07)
JPF Stateless Random Walk 10126 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
CalFuzzer 100 (10) 0.10 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 176.00 (NA) 26.00 (26.00)
reorder (9,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (593) 0.12 2497.98s 38704112.56 (0.00) 81.67 (59.64)
JPF Stateless Random Walk 10124 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (10) 0.01 NA NA (NA) NA (NA)
CalFuzzer 100 (10) 0.10 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.67s 205.00 (NA) 28.00 (28.00)

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=true
Reorder Params Paths Found Error Time Taken Steps (Depth)
1,1 5 Yes 0.78 secs 19
2,1 >=100 Yes 0.436 secs 26
3,1 >=2000 Yes 8.549 secs 33
4,1 >=30,000 Yes 140.526 secs 40
5,1 >=439,000 Yes 2275.930 secs 47
4,2 >= 555,000 Yes 2836.426 secs 48
3,3 >= 684,000 Yes 3454.611 secs 49
1,5 >= 708,000 No 3600.909 secs 51
6,1 >=652,000 No 3603.998 secs 54
5,2 >=602,000 No 3600.612 secs 55
8,1 >=579,000 No 3605.120 secs 68
9,1 >=538,000 No 3605.823 secs 75
10,1 >=499,000 No 3600.534 secs 82

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.
Reorder Params Path Error Density
1,1 0.030
1,5 0.043
5,1 0.0
8,1 0.0
9,1 0.0
10,1 0.0
  • 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
(1,1) 100 (100) 100.00% 0.78s 83.69 (0.00) 18.32 (15.64) 783.57 783.57 18.32 15.64 55.16 28.53 0.99 67.05 37.53 0.00 14001.28 6990528.00 0.00 174.00 174.00
(1,5) 100 (100) 100.00% 16.61s 238450.80 (0.00) 52.94 (25.52) 16608.03 5007.11 52.94 25.52 49151.07 189299.73 0.98 238424.28 49123.57 0.00 244161.92 6990528.00 80162.71 185.26 185.26
(8,1) 5000 (5000) 100.00% 1225.99s 20078513.07 (0.00) 73.59 (54.07) 1225990.15 5039.40 73.59 54.07 2874234.15 17204278.92 1.00 20078458.00 2874178.08 0.00 426544.46 932096.00 187472.32 202.00 202.00
(2,1) 100 (100) 100.00% 0.61s 560.58 (0.00) 28.33 (21.24) 613.41 613.41 28.33 21.24 255.66 304.92 1.00 538.34 233.00 0.00 22846.08 932096.00 0.00 252.46 252.46
(9,1) 5000 (593) 11.86% 2497.98s 38704112.56 (0.00) 81.67 (59.64) 2497980.25 5102.36 81.67 59.64 5223853.76 33480258.80 1.00 38704051.92 5223792.11 0.00 475022.89 932096.00 198919.75 206.00 206.00
(3,1) 100 (100) 100.00% 1.21s 3867.01 (0.00) 36.96 (27.26) 1211.19 1211.19 36.96 27.26 1285.54 2581.47 1.00 3838.75 1256.97 0.00 30968.96 932096.00 0.00 255.03 255.03
(3,3) 100 (100) 100.00% 24.10s 216430.64 (0.00) 57.72 (29.79) 24102.54 6396.58 57.72 29.79 47500.16 168930.48 1.00 216399.85 47468.86 0.00 111149.44 932096.00 48094.12 272.41 278.00
(4,1) 100 (100) 100.00% 7.35s 33895.58 (0.00) 46.61 (34.29) 7348.58 6948.40 46.61 34.29 9516.88 24378.70 1.00 33860.29 9481.27 0.00 61336.96 932096.00 879.70 274.16 274.16
(4,2) 100 (100) 100.00% 19.46s 170146.30 (0.00) 56.39 (36.93) 19455.02 4850.36 56.39 36.93 37562.55 132583.75 1.00 170108.37 37524.15 0.00 98801.92 932096.00 42491.61 279.55 279.93
(10,1) 5000 (4) 0.08% 2414.82s 38022689.25 (0.00) 89.75 (65.25) 2414821.25 3641.25 89.75 65.25 4947236.75 33075452.50 1.00 38022623.00 4947169.50 0.00 471712.00 932096.00 212632.75 210.00 210.00
(5,1) 100 (100) 100.00% 9.98s 107466.97 (0.00) 49.72 (37.57) 9984.68 4383.55 49.72 37.57 23411.50 84055.47 1.00 107428.40 23371.93 0.00 147628.80 6990528.00 45776.70 190.00 190.00
(5,2) 100 (100) 100.00% 85.43s 996758.65 (0.00) 65.17 (42.90) 85426.04 5003.09 65.17 42.90 184139.71 812618.94 1.00 996714.75 184095.52 0.00 155769.60 932096.00 45871.92 281.11 281.67
(5,5) 117 (2) 1.71% 2206.74s 31429172.50 (0.00) 86.00 (44.00) 2206738.50 2245.00 86.00 44.00 4352520.00 27076652.50 1.00 31429127.50 4352474.00 0.00 2576352.00 6990528.00 179173.00 201.00 201.00
(6,1) 100 (100) 100.00% 73.05s 833413.61 (0.00) 64.44 (46.18) 73054.57 4832.70 64.44 46.18 155272.79 678140.82 1.00 833366.43 155225.40 0.00 157378.56 932096.00 49872.47 280.73 280.73
(7,1) 5000 (5000) 100.00% 213.90s 3586188.11 (0.00) 65.62 (48.65) 213896.72 4963.18 65.62 48.65 579468.72 3006719.39 1.00 3586138.46 579418.07 0.00 369729.37 932096.00 172409.01 198.00 198.00

ConTest

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

path error density.

Reorder Params Path Error Density
1,1 0.061
2,1 0.023
3,1 0.007
4,1 0.003
5,1 0.003
6,1 0.000
1,5 0.285
4,2 0.00
3,3 0.02
5,2 0.01
8,1 0.00
9,1 0.01
10,1 0.00

CalFuzzer

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

path error density.

Reorder Params Path Error Density
1,1 0.06
2,1 0.12
3,1 0.11
4,1 0.12
4,2 0.10
5,1 0.12
3,3 0.36
6,1 0.10
5,2 0.24
1,5 0.08
8,1 0.10
9,1 0.10
10,1 0.09
vv-lab/reorder.txt · Last modified: 2015/02/18 22:59 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