Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:clean [2015/02/18 22:54] (current)
egm created
Line 1: Line 1:
 +[[Concurrency Tool Comparison]]
  
 +== Model Description ==
 +
 +The model contains a deadlock.
 +
 +Classes: 4
 +
 +SLOC: 51
 +
 +Parameters: (#first, #second, #iter)
 +
 +== Summary Results Table ==
 +
 +{| align=center | border=1
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | clean (1,1,12)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 1.54s
 +| 1742.56 (0.00)
 +| 161.30 (14.97)
 +|-
 +| JPF Stateless Random Walk
 +| 10125 (336) 0.03
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 0.93s
 +| 1800.00 (10.00)
 +| 180.00 (NA)
 +|-
 +| ConTest
 +| 1000 (30) 0.03
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | clean (10,10,1)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 114 (110) 0.96
 +| align="​right"​| 113.28s
 +| 1326102.90 (0.00)
 +| 221.93 (218.74)
 +|-
 +| JPF Stateless Random Walk
 +| 10129 (2928) 0.29
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (0) 0.00
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| ConTest
 +| 100 (0) 0.00
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|}
 +
 +==Chess==
 +
 +* ChessBound=2
 +* ChessMonitorVolatiles=false
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! 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. ​
 +
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! Clean Params !! Path Error Density
 +|- 
 +| 1,1,12 || 0.033
 +|-
 +| 10,10,1 || 0.289
 +|}
 +
 +
 +
 +
 +===Stateful Randomized Depth-first search===
 +
 +* 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). ​
 +
 +{| align="​center"​ | border=1
 +|- bgcolor="​lightblue"​
 +! 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%
 +| align="​right"​| 1.54s
 +| 1742.56 (0.00)
 +| 161.30 (14.97)
 +| align="​right"​ | 1539.79
 +| align="​right"​ | 1539.79
 +| align="​right"​ | 161.30
 +| align="​right"​ | 14.97
 +| align="​right"​ | 906.75
 +| align="​right"​ | 835.81
 +| align="​right"​ | 0.96
 +| align="​right"​ | 1726.59
 +| align="​right"​ | 889.82
 +| align="​right"​ | 0.00
 +| align="​right"​ | 17153.92
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 138.00
 +| align="​right"​ | 149.00
 +|-
 +|(10,10,1)
 +| 114 (110) 96.49%
 +| align="​right"​| 113.28s
 +| 1326102.90 (0.00)
 +| 221.93 (218.74)
 +| align="​right"​ | 113278.95
 +| align="​right"​ | 3154.25
 +| align="​right"​ | 221.93
 +| align="​right"​ | 218.74
 +| align="​right"​ | 281078.65
 +| align="​right"​ | 1045024.25
 +| align="​right"​ | 0.60
 +| align="​right"​ | 1325883.16
 +| align="​right"​ | 280858.31
 +| align="​right"​ | 0.00
 +| align="​right"​ | 452811.64
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 163324.80
 +| align="​right"​ | 210.00
 +| align="​right"​ | 221.00
 +|}
 +
 +
 +
 +
 +==ConTest==
 +
 +* 1000 independent trials
 +
 +* The ratio of the error discovery trials over the total number of trials is the 
 +path error density. ​
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! 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