Concurrency Tool Comparison

Model Description

The model deadlocks because a wait() is enclosed within an if statement instead of a while statement.

Classes: 2

SLOC: 71

Parameters: (#seatRequests, #passengers, capacity)

Summary Results Table

piper (2,16,8)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 9995 (6) 0.00 1.31s 325.50 (0.00) 324.50 (324.50)
JPF Stateless Random Walk 10125 (6) 0.00 NA NA (NA) NA (NA)
piper (2,2,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 150 (150) 1.00 1.58s 2276.49 (0.00) 53.93 (40.53)
piper (2,4,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 150 (150) 1.00 54.71s 838403.57 (0.00) 108.29 (81.40)
JPF Stateless Random Walk 10116 (289) 0.03 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 18.83s 628824.00 (3743.00) 168.00 (NA)
ConTest 1000 (11) 0.01 NA NA (NA) NA (NA)
piper (2,5,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 206.89s 3057202.80 (0.00) 126.45 (100.04)
piper (2,6,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (97) 0.97 283.17s 3883492.16 (0.00) 143.87 (117.64)
piper (2,7,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (96) 0.96 334.26s 4566700.58 (0.00) 160.06 (133.93)
piper (2,8,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (4770) 0.95 301.58s 3755044.80 (0.00) 179.06 (151.94)
JPF Stateless Random Walk 10124 (850) 0.08 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 42.65s 1531872.00 (5319.00) 288.00 (NA)
ConTest 100 (11) 0.11 NA NA (NA) NA (NA)
piper (2,8,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5025 (2866) 0.57 1179.77s 14552031.67 (0.00) 184.68 (150.43)
JPF Stateless Random Walk 10124 (301) 0.03 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 12.86s 459936.00 (1597.00) 288.00 (NA)
ConTest 100 (1) 0.01 NA NA (NA) NA (NA)
piper (2,8,6)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4987 (429) 0.09 1329.92s 16186995.16 (0.00) 180.35 (146.60)
JPF Stateless Random Walk 10123 (83) 0.01 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 12.86s 459936.00 (1597.00) 288.00 (NA)
ConTest 100 (0) 0.00 NA NA (NA) NA (NA)
piper (2,8,7)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5186 (91) 0.02 1487.44s 18341935.22 (0.00) 176.79 (143.89)
JPF Stateless Random Walk 10130 (17) 0.00 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 12.86s 459936.00 (1597.00) 288.00 (NA)
ConTest 100 (0) 0.00 NA NA (NA) NA (NA)

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=false
AccountSubtype Params Tests Found Error Time Taken Steps (Depth)
2,4,4 3,743 Yes 18.829 secs 168
2,8,4 5,319 Yes 42.651 secs 288
2,8,5 1,597 Yes 12.855 secs 288
2,8,6 1,597 Yes 8.268 secs 288
2,8,7 1,597 Yes 8.221 secs 288

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.
Parameters Path Error Density
2,4,4 0.029
2,8,4 0.083
2,8,5 0.030
2,8,6 0.008
2,8,7 0.002
2,16,7 0.0006
  • 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
(2,7,4) 100 (96) 96.00% 334.26s 4566700.58 (0.00) 160.06 (133.93) 334260.55 4928.19 160.06 133.93 871245.98 3695454.60 0.89 4566565.66 871110.17 0.00 1105157.33 6990528.00 420132.95 219.00 230.00
(2,16,8) 9995 (6) 0.06% 1.31s 325.50 (0.00) 324.50 (324.50) 1306.17 1306.17 324.50 324.50 325.50 0.00 0.00 0.00 0.00 0.00 15488.00 932096.00 0.00 327.00 338.00
(2,8,4) 5000 (4770) 95.40% 301.58s 3755044.80 (0.00) 179.06 (151.94) 301575.26 4681.66 179.06 151.94 742889.64 3012155.16 0.92 3754891.86 742735.78 0.00 334799.17 932096.00 158633.07 231.00 242.00
(2,8,5) 5025 (2866) 57.03% 1179.77s 14552031.67 (0.00) 184.68 (150.43) 1179766.68 4888.26 184.68 150.43 3061014.77 11491016.91 0.96 14551880.24 3060862.38 0.00 413719.60 932096.00 185184.04 231.00 242.00
(2,8,6) 4987 (429) 8.60% 1329.92s 16186995.16 (0.00) 180.35 (146.60) 1329924.23 4499.45 180.35 146.60 3208115.95 12978879.21 0.92 16186847.55 3207967.42 0.00 403275.04 932096.00 183196.31 231.00 242.00
(2,8,7) 5186 (91) 1.75% 1487.44s 18341935.22 (0.00) 176.79 (143.89) 1487437.86 3733.93 176.79 143.89 3564384.73 14777550.49 0.85 18341790.33 3564238.99 0.00 384064.00 932096.00 161049.68 231.00 242.00
(2,2,2) 150 (150) 100.00% 1.58s 2276.49 (0.00) 53.93 (40.53) 1583.92 1583.92 53.93 40.53 995.87 1280.63 0.87 2234.96 953.46 0.00 18155.52 932096.00 0.00 159.00 170.00
(2,4,4) 150 (150) 100.00% 54.71s 838403.57 (0.00) 108.29 (81.40) 54711.95 4838.51 108.29 81.40 214919.68 623483.89 0.98 838321.17 214836.30 0.00 258444.80 932096.00 105054.13 183.00 194.00
(2,5,4) 100 (100) 100.00% 206.89s 3057202.80 (0.00) 126.45 (100.04) 206888.94 4791.95 126.45 100.04 657551.49 2399651.31 0.96 3057101.76 657449.49 0.00 874992.64 6990528.00 310137.28 195.00 206.00
(2,6,4) 100 (97) 97.00% 283.17s 3883492.16 (0.00) 143.87 (117.64) 283174.82 4753.69 143.87 117.64 794850.54 3088641.63 0.93 3883373.53 794730.97 0.00 1154472.25 6990528.00 469754.15 207.00 218.00

ConTest

  • 100 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
2,4,4 0.011 (1000 trials)
2,8,4 0.11
2,8,5 0.01
2,8,6 0.000
2,8,7 0.000

CalFuzzer

Not Applicable. The initial dynamic analysis does not finish within a time bound of 1 hour.

vv-lab/piper.txt · Last modified: 2015/02/18 22:57 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