Concurrency Tool Comparison

Model Description

The model contains a deadlock.

Classes: 4

SLOC: 51

Parameters: (#first, #second, #iter)

Summary Results Table

clean (1,1,12)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.54s 1742.56 (0.00) 161.30 (14.97)
JPF Stateless Random Walk 10125 (336) 0.03 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 0.93s 1800.00 (10.00) 180.00 (NA)
ConTest 1000 (30) 0.03 NA NA (NA) NA (NA)
clean (10,10,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 114 (110) 0.96 113.28s 1326102.90 (0.00) 221.93 (218.74)
JPF Stateless Random Walk 10129 (2928) 0.29 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 100 (0) 0.00 NA NA (NA) NA (NA)

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=false
Clean Params Tests Found Error Time Taken Steps (Depth)
1,1,12 10 Yes 0.93 secs 180
10,10,1 >=398,000 No 3604.715 secs 242

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.

Clean Params Path Error Density
1,1,12 0.033
10,10,1 0.289
  • 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,12) 100 (100) 100.00% 1.54s 1742.56 (0.00) 161.30 (14.97) 1539.79 1539.79 161.30 14.97 906.75 835.81 0.96 1726.59 889.82 0.00 17153.92 6990528.00 0.00 138.00 149.00
(10,10,1) 114 (110) 96.49% 113.28s 1326102.90 (0.00) 221.93 (218.74) 113278.95 3154.25 221.93 218.74 281078.65 1045024.25 0.60 1325883.16 280858.31 0.00 452811.64 6990528.00 163324.80 210.00 221.00

ConTest

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

path error density.

Clean Params Path Error Density
1,1,12 0.030
10,10,1 ? (not-halt or deadlock)

CalFuzzer

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

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