Concurrency Tool Comparison

Model Description

The benchmark contains an atomicity violation with two sequences of operations that need to be protected together but the implementation incorrectly protects the two sequence separately. The input parameters to the benchmark are two different types of threads (twoStagers and readers). The twoStage thread modifies the two separately protected sequences. When the reader thread reads the value of a shared variable between the two accesses by the twoStage thread then a bug is manifested (an exception is raised).

Classes: 5

SLOC: 52

Summary Results Table

twostage (1,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.61s 88.04 (0.00) 20.18 (18.51)
JPF Stateless Random Walk 10127 (430) 0.04 0.02s 0.94 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 0.94s 180.00 (9.00) 20.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 3.53s 30.00 (NA) 11.00 (11.00)
twostage (1,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.92s 2286.20 (0.00) 35.71 (29.10)
CHESS 1 (1) 1.00 0.55s 5800.00 (200.00) 29.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 4.53s 30.00 (NA) 11.00 (11.00)
twostage (1,3)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 13.16s 78273.12 (0.00) 50.59 (34.77)
CHESS 1 (1) 1.00 17.38s 228000.00 (6000.00) 38.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 30.00 (NA) 11.00 (11.00)
twostage (1,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 319.01s 3341784.11 (0.00) 73.96 (38.09)
JPF Stateless Random Walk 1000 (55) 0.06 0.43s 55.85 (NA) 0.00 (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 30.00 (NA) 11.00 (11.00)
twostage (1,7)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 150 (58) 0.39 615.22s 8442487.19 (0.00) 77.57 (46.53)
twostage (1,8)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 130 (29) 0.22 760.96s 8184336.48 (0.00) 72.31 (51.24)
twostage (10,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (0) 0.00 NA NA (NA) NA (NA)
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 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 246.00 (NA) 29.00 (29.00)
twostage (2,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.07s 1966.10 (0.00) 38.46 (30.08)
JPF Stateless Random Walk 1000 (10) 0.01 0.30s 30.20 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 0.52s 5800.00 (200.00) 29.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 3.53s 46.00 (NA) 13.00 (13.00)
twostage (2,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 2.41s 10223.50 (0.00) 45.72 (36.07)
CHESS 1 (1) 1.00 17.44s 228000.00 (6000.00) 38.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 3.53s 46.00 (NA) 13.00 (13.00)
twostage (2,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 518.46s 8968986.03 (0.00) 81.30 (46.71)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 46.00 (NA) 13.00 (13.00)
twostage (2,6)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 125 (36) 0.29 1666.94s 22273647.86 (0.00) 90.06 (50.17)
twostage (3,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 10.14s 56717.85 (0.00) 53.76 (40.57)
JPF Stateless Random Walk 1000 (1) 0.00 0.59s 49.00 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 16.64s 228000.00 (6000.00) 38.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 64.00 (NA) 15.00 (15.00)
twostage (3,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 106 (40) 0.38 1968.26s 32880318.60 (0.00) 90.78 (53.70)
twostage (4,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 30.84s 288171.90 (0.00) 68.06 (50.25)
JPF Stateless Random Walk 1000 (0) 0.00 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 754.66s 9400000.00 (200000.00) 47.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 84.00 (NA) 17.00 (17.00)
twostage (4,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 114 (27) 0.24 2106.31s 29409673.52 (0.00) 94.67 (59.85)
twostage (5,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 321.14s 3272083.66 (0.00) 81.82 (59.83)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 106.00 (NA) 19.00 (19.00)
twostage (5,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 97 (97) 1.00 459.54s 7977266.73 (0.00) 82.94 (59.40)
twostage (5,3)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 117 (33) 0.28 1751.81s 27545439.15 (0.00) 94.94 (63.45)
twostage (6,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (5000) 1.00 464.28s 7882244.02 (0.00) 83.00 (60.13)
JPF Stateless Random Walk 10128 (2) 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)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 130.00 (NA) 21.00 (21.00)
twostage (6,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 130 (37) 0.28 1616.85s 20977457.46 (0.00) 94.78 (65.76)
twostage (7,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (2299) 0.46 1815.53s 27704831.56 (0.00) 94.96 (67.75)
JPF Stateless Random Walk 10128 (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)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 156.00 (NA) 23.00 (23.00)
twostage (8,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (126) 0.03 2155.76s 32969192.09 (0.00) 105.46 (73.40)
JPF Stateless Random Walk 10200 (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)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 2.53s 184.00 (NA) 25.00 (25.00)

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=false
TwoStage Params Tests Found Error Time Taken Steps (Depth)
1,1 9 Yes 0.94 secs 20
1,2 >=200 Yes 0.546 secs 29
2,1 >=200 Yes 0.515 secs 29
2,2 >=6000 Yes 17.441 secs 38
1,3 >=6000 Yes 17.378 secs 38
3,1 >=6000 Yes 16.645 secs 38
4,1 >=200,000 Yes 754.655 secs 47
1,5 >=1,059,000 No 3602.282 secs 56
5,1 >=1,064,000 No 3602.422 secs 56
6,1 >=970,000 No 3604.022 secs 56
2,5 >=969,000 No 3600.35 secs 65
2,5 >=969,000 No 3600.35 secs 65
7,1 >=879,000 No 3601.205 secs 74
8,1 >=821,000 No 3602.135 secs 83
10,1 >=714,000 No 3600.206 secs 83

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.

TwoStage Params Path Error Density
1,1 0.043
2,2 0.022
2,5 0.028
6,1 0.0002
7,1 0.0
8,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
(6,1) 5000 (5000) 100.00% 464.28s 7882244.02 (0.00) 83.00 (60.13) 464282.52 5068.92 83.00 60.13 1586963.57 6295280.44 1.00 7882182.88 1586901.44 0.00 392921.75 932096.00 185330.38 193.00 193.00
(6,2) 130 (37) 28.46% 1616.85s 20977457.46 (0.00) 94.78 (65.76) 1616853.00 4244.54 94.78 65.76 4040281.35 16937176.11 1.00 20977390.70 4040213.59 0.00 2413953.73 6990528.00 1101639.38 197.03 197.03
(7,1) 5000 (2299) 45.98% 1815.53s 27704831.56 (0.00) 94.96 (67.75) 1815534.19 4892.96 94.96 67.75 5278666.49 22426165.07 1.00 27704762.81 5278596.74 0.00 477712.12 932096.00 202529.28 197.01 197.01
(1,1) 100 (100) 100.00% 0.61s 88.04 (0.00) 20.18 (18.51) 612.70 612.70 20.18 18.51 56.67 31.37 1.04 68.53 36.18 0.00 15553.28 6990528.00 0.00 173.08 173.08
(1,2) 100 (100) 100.00% 0.92s 2286.20 (0.00) 35.71 (29.10) 918.46 918.46 35.71 29.10 817.13 1469.07 0.93 2256.10 786.19 0.00 26549.76 932096.00 0.00 251.19 251.91
(1,3) 100 (100) 100.00% 13.16s 78273.12 (0.00) 50.59 (34.77) 13157.28 4255.89 50.59 34.77 25204.08 53069.04 0.99 78237.35 25167.32 0.00 79715.20 932096.00 27159.95 272.12 272.68
(1,5) 100 (100) 100.00% 319.01s 3341784.11 (0.00) 73.96 (38.09) 319014.62 4503.47 73.96 38.09 683349.85 2658434.26 0.92 3341745.02 683309.84 0.00 157665.92 932096.00 37416.00 278.52 279.90
(1,7) 150 (58) 38.67% 615.22s 8442487.19 (0.00) 77.57 (46.53) 615215.91 3348.79 77.57 46.53 1559333.97 6883153.22 0.83 8442439.66 1559285.60 0.00 1366030.34 6990528.00 525682.10 197.71 197.71
(1,8) 130 (29) 22.31% 760.96s 8184336.48 (0.00) 72.31 (51.24) 760962.59 3539.07 72.31 51.24 1453206.17 6731130.31 0.66 8184284.24 1453153.28 0.00 934430.90 6990528.00 446142.62 200.10 200.10
(8,1) 4999 (126) 2.52% 2155.76s 32969192.09 (0.00) 105.46 (73.40) 2155760.02 4799.94 105.46 73.40 6480559.25 26488632.84 1.00 32969117.69 6480483.85 0.00 505722.92 932096.00 223251.82 201.00 201.00
(2,1) 100 (100) 100.00% 1.07s 1966.10 (0.00) 38.46 (30.08) 1067.09 1067.09 38.46 30.08 746.72 1219.38 0.99 1935.02 715.23 0.00 25803.52 932096.00 0.00 244.46 249.10
(2,2) 100 (100) 100.00% 2.41s 10223.50 (0.00) 45.72 (36.07) 2406.28 2406.28 45.72 36.07 3300.70 6922.80 0.99 10186.43 3262.64 0.00 31480.96 6990528.00 0.00 181.12 181.12
(2,5) 100 (100) 100.00% 518.46s 8968986.03 (0.00) 81.30 (46.71) 518462.59 4775.78 81.30 46.71 1759759.44 7209226.59 0.97 8968938.32 1759710.76 0.00 1726579.20 6990528.00 635963.42 194.39 194.39
(2,6) 125 (36) 28.80% 1666.94s 22273647.86 (0.00) 90.06 (50.17) 1666940.14 3480.08 90.06 50.17 4105668.44 18167979.42 0.94 22273596.69 4105616.33 0.00 2283043.56 6990528.00 1147659.22 198.64 198.64
(3,1) 100 (100) 100.00% 10.14s 56717.85 (0.00) 53.76 (40.57) 10142.53 4741.55 53.76 40.57 19029.75 37688.10 1.00 56676.28 18987.84 0.00 72305.28 932096.00 17963.74 262.42 267.70
(3,5) 106 (40) 37.74% 1968.26s 32880318.60 (0.00) 90.78 (53.70) 1968262.65 4380.48 90.78 53.70 6079980.10 26800338.50 0.90 32880263.90 6079924.50 0.00 2392500.80 6990528.00 1167632.68 198.28 198.28
(10,1) 4999 (0) 0.00%
(4,1) 100 (100) 100.00% 30.84s 288171.90 (0.00) 68.06 (50.25) 30844.89 4437.01 68.06 50.25 74878.02 213293.88 1.00 288120.65 74826.56 0.00 117380.48 932096.00 49747.98 264.73 271.05
(4,4) 114 (27) 23.68% 2106.31s 29409673.52 (0.00) 94.67 (59.85) 2106310.30 3547.56 94.67 59.85 5589241.56 23820431.96 1.00 29409612.67 5589179.70 0.00 2646885.93 6990528.00 1270640.63 197.26 197.26
(5,1) 100 (100) 100.00% 321.14s 3272083.66 (0.00) 81.82 (59.83) 321144.06 4221.71 81.82 59.83 697572.24 2574511.42 1.00 3272022.83 697511.08 0.00 177150.08 932096.00 40599.68 270.29 275.65
(5,2) 97 (97) 100.00% 459.54s 7977266.73 (0.00) 82.94 (59.40) 459535.48 4536.60 82.94 59.40 1601368.30 6375898.43 1.00 7977206.33 1601306.90 0.00 1789834.56 6990528.00 663180.38 193.01 193.01
(5,3) 117 (33) 28.21% 1751.81s 27545439.15 (0.00) 94.94 (63.45) 1751814.09 4889.55 94.94 63.45 5290511.58 22254927.58 1.00 27545374.70 5290446.12 0.00 2647683.88 6990528.00 1311998.91 197.24 197.24

ConTest

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

path error density.

TwoStage Params Path Error Density
1,1 0.000
2,1 0.000
3,1 0.000
4,1 0.000
5,1 0.000
6,1 0.000
1,5 0.000
1,2 0.000
2,2 0.000
1,3 0.000
2,5 0.000
7,1 0.000
8,1 0.000
10,1 0.000

CalFuzzer

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

vv-lab/two-stage.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