Differences

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

Link to this comparison view

vv-lab:piper [2015/02/18 22:57] (current)
egm created
Line 1: Line 1:
 +[[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 ==
 +
 +{| align=center | border=1
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,16,8)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 9995 (6) 0.00
 +| align="​right"​| 1.31s
 +| 325.50 (0.00)
 +| 324.50 (324.50)
 +|-
 +| JPF Stateless Random Walk
 +| 10125 (6) 0.00
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,2,2)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 150 (150) 1.00
 +| align="​right"​| 1.58s
 +| 2276.49 (0.00)
 +| 53.93 (40.53)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,4,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 150 (150) 1.00
 +| align="​right"​| 54.71s
 +| 838403.57 (0.00)
 +| 108.29 (81.40)
 +|-
 +| JPF Stateless Random Walk
 +| 10116 (289) 0.03
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 18.83s
 +| 628824.00 (3743.00)
 +| 168.00 (NA)
 +|-
 +| ConTest
 +| 1000 (11) 0.01
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,5,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 206.89s
 +| 3057202.80 (0.00)
 +| 126.45 (100.04)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,6,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (97) 0.97
 +| align="​right"​| 283.17s
 +| 3883492.16 (0.00)
 +| 143.87 (117.64)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,7,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (96) 0.96
 +| align="​right"​| 334.26s
 +| 4566700.58 (0.00)
 +| 160.06 (133.93)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,8,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 5000 (4770) 0.95
 +| align="​right"​| 301.58s
 +| 3755044.80 (0.00)
 +| 179.06 (151.94)
 +|-
 +| JPF Stateless Random Walk
 +| 10124 (850) 0.08
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 42.65s
 +| 1531872.00 (5319.00)
 +| 288.00 (NA)
 +|-
 +| ConTest
 +| 100 (11) 0.11
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,8,5)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 5025 (2866) 0.57
 +| align="​right"​| 1179.77s
 +| 14552031.67 (0.00)
 +| 184.68 (150.43)
 +|-
 +| JPF Stateless Random Walk
 +| 10124 (301) 0.03
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 12.86s
 +| 459936.00 (1597.00)
 +| 288.00 (NA)
 +|-
 +| ConTest
 +| 100 (1) 0.01
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,8,6)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 4987 (429) 0.09
 +| align="​right"​| 1329.92s
 +| 16186995.16 (0.00)
 +| 180.35 (146.60)
 +|-
 +| JPF Stateless Random Walk
 +| 10123 (83) 0.01
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 12.86s
 +| 459936.00 (1597.00)
 +| 288.00 (NA)
 +|-
 +| ConTest
 +| 100 (0) 0.00
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | piper (2,8,7)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 5186 (91) 0.02
 +| align="​right"​| 1487.44s
 +| 18341935.22 (0.00)
 +| 176.79 (143.89)
 +|-
 +| JPF Stateless Random Walk
 +| 10130 (17) 0.00
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 12.86s
 +| 459936.00 (1597.00)
 +| 288.00 (NA)
 +|-
 +| ConTest
 +| 100 (0) 0.00
 +| align="​right"​| NA
 +| NA (NA)
 +| NA (NA)
 +|}
 +==Chess==
 +
 +* ChessBound=2
 +* ChessMonitorVolatiles=false ​
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! 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. ​
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! 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
 +|}
 +
 +===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
 +
 +|-
 +|(2,7,4)
 +| 100 (96) 96.00%
 +| align="​right"​| 334.26s
 +| 4566700.58 (0.00)
 +| 160.06 (133.93)
 +| align="​right"​ | 334260.55
 +| align="​right"​ | 4928.19
 +| align="​right"​ | 160.06
 +| align="​right"​ | 133.93
 +| align="​right"​ | 871245.98
 +| align="​right"​ | 3695454.60
 +| align="​right"​ | 0.89
 +| align="​right"​ | 4566565.66
 +| align="​right"​ | 871110.17
 +| align="​right"​ | 0.00
 +| align="​right"​ | 1105157.33
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 420132.95
 +| align="​right"​ | 219.00
 +| align="​right"​ | 230.00
 +|-
 +|(2,16,8)
 +| 9995 (6) 0.06%
 +| align="​right"​| 1.31s
 +| 325.50 (0.00)
 +| 324.50 (324.50)
 +| align="​right"​ | 1306.17
 +| align="​right"​ | 1306.17
 +| align="​right"​ | 324.50
 +| align="​right"​ | 324.50
 +| align="​right"​ | 325.50
 +| align="​right"​ | 0.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 15488.00
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 327.00
 +| align="​right"​ | 338.00
 +|-
 +|(2,8,4)
 +| 5000 (4770) 95.40%
 +| align="​right"​| 301.58s
 +| 3755044.80 (0.00)
 +| 179.06 (151.94)
 +| align="​right"​ | 301575.26
 +| align="​right"​ | 4681.66
 +| align="​right"​ | 179.06
 +| align="​right"​ | 151.94
 +| align="​right"​ | 742889.64
 +| align="​right"​ | 3012155.16
 +| align="​right"​ | 0.92
 +| align="​right"​ | 3754891.86
 +| align="​right"​ | 742735.78
 +| align="​right"​ | 0.00
 +| align="​right"​ | 334799.17
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 158633.07
 +| align="​right"​ | 231.00
 +| align="​right"​ | 242.00
 +|-
 +|(2,8,5)
 +| 5025 (2866) 57.03%
 +| align="​right"​| 1179.77s
 +| 14552031.67 (0.00)
 +| 184.68 (150.43)
 +| align="​right"​ | 1179766.68
 +| align="​right"​ | 4888.26
 +| align="​right"​ | 184.68
 +| align="​right"​ | 150.43
 +| align="​right"​ | 3061014.77
 +| align="​right"​ | 11491016.91
 +| align="​right"​ | 0.96
 +| align="​right"​ | 14551880.24
 +| align="​right"​ | 3060862.38
 +| align="​right"​ | 0.00
 +| align="​right"​ | 413719.60
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 185184.04
 +| align="​right"​ | 231.00
 +| align="​right"​ | 242.00
 +|-
 +|(2,8,6)
 +| 4987 (429) 8.60%
 +| align="​right"​| 1329.92s
 +| 16186995.16 (0.00)
 +| 180.35 (146.60)
 +| align="​right"​ | 1329924.23
 +| align="​right"​ | 4499.45
 +| align="​right"​ | 180.35
 +| align="​right"​ | 146.60
 +| align="​right"​ | 3208115.95
 +| align="​right"​ | 12978879.21
 +| align="​right"​ | 0.92
 +| align="​right"​ | 16186847.55
 +| align="​right"​ | 3207967.42
 +| align="​right"​ | 0.00
 +| align="​right"​ | 403275.04
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 183196.31
 +| align="​right"​ | 231.00
 +| align="​right"​ | 242.00
 +|-
 +|(2,8,7)
 +| 5186 (91) 1.75%
 +| align="​right"​| 1487.44s
 +| 18341935.22 (0.00)
 +| 176.79 (143.89)
 +| align="​right"​ | 1487437.86
 +| align="​right"​ | 3733.93
 +| align="​right"​ | 176.79
 +| align="​right"​ | 143.89
 +| align="​right"​ | 3564384.73
 +| align="​right"​ | 14777550.49
 +| align="​right"​ | 0.85
 +| align="​right"​ | 18341790.33
 +| align="​right"​ | 3564238.99
 +| align="​right"​ | 0.00
 +| align="​right"​ | 384064.00
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 161049.68
 +| align="​right"​ | 231.00
 +| align="​right"​ | 242.00
 +|-
 +|(2,2,2)
 +| 150 (150) 100.00%
 +| align="​right"​| 1.58s
 +| 2276.49 (0.00)
 +| 53.93 (40.53)
 +| align="​right"​ | 1583.92
 +| align="​right"​ | 1583.92
 +| align="​right"​ | 53.93
 +| align="​right"​ | 40.53
 +| align="​right"​ | 995.87
 +| align="​right"​ | 1280.63
 +| align="​right"​ | 0.87
 +| align="​right"​ | 2234.96
 +| align="​right"​ | 953.46
 +| align="​right"​ | 0.00
 +| align="​right"​ | 18155.52
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 159.00
 +| align="​right"​ | 170.00
 +|-
 +|(2,4,4)
 +| 150 (150) 100.00%
 +| align="​right"​| 54.71s
 +| 838403.57 (0.00)
 +| 108.29 (81.40)
 +| align="​right"​ | 54711.95
 +| align="​right"​ | 4838.51
 +| align="​right"​ | 108.29
 +| align="​right"​ | 81.40
 +| align="​right"​ | 214919.68
 +| align="​right"​ | 623483.89
 +| align="​right"​ | 0.98
 +| align="​right"​ | 838321.17
 +| align="​right"​ | 214836.30
 +| align="​right"​ | 0.00
 +| align="​right"​ | 258444.80
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 105054.13
 +| align="​right"​ | 183.00
 +| align="​right"​ | 194.00
 +|-
 +|(2,5,4)
 +| 100 (100) 100.00%
 +| align="​right"​| 206.89s
 +| 3057202.80 (0.00)
 +| 126.45 (100.04)
 +| align="​right"​ | 206888.94
 +| align="​right"​ | 4791.95
 +| align="​right"​ | 126.45
 +| align="​right"​ | 100.04
 +| align="​right"​ | 657551.49
 +| align="​right"​ | 2399651.31
 +| align="​right"​ | 0.96
 +| align="​right"​ | 3057101.76
 +| align="​right"​ | 657449.49
 +| align="​right"​ | 0.00
 +| align="​right"​ | 874992.64
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 310137.28
 +| align="​right"​ | 195.00
 +| align="​right"​ | 206.00
 +|-
 +|(2,6,4)
 +| 100 (97) 97.00%
 +| align="​right"​| 283.17s
 +| 3883492.16 (0.00)
 +| 143.87 (117.64)
 +| align="​right"​ | 283174.82
 +| align="​right"​ | 4753.69
 +| align="​right"​ | 143.87
 +| align="​right"​ | 117.64
 +| align="​right"​ | 794850.54
 +| align="​right"​ | 3088641.63
 +| align="​right"​ | 0.93
 +| align="​right"​ | 3883373.53
 +| align="​right"​ | 794730.97
 +| align="​right"​ | 0.00
 +| align="​right"​ | 1154472.25
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 469754.15
 +| align="​right"​ | 207.00
 +| align="​right"​ | 218.00
 +|}
 +
 +
 +==ConTest==
 +
 +* 100 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
 +! 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