Differences

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

Link to this comparison view

vv-lab:producerconsumer [2015/02/18 22:57] (current)
egm created
Line 1: Line 1:
 +[[Concurrency Tool Comparison]]
  
 +== Model Description == 
 +
 +A race condition in producer and consumer model. ​
 +
 +Classes: 8
 +
 +SLOC: 87
 +
 +Parameters: (#prod, #cons, #items)
 +
 +== Summary Results Table ==
 +
 +{| align=center | border=1
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (1,10,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 115 (84) 0.73
 +| align="​right"​| 86.11s
 +| 963174.08 (0.00)
 +| 121.87 (116.52)
 +|-
 +| JPF Stateless Random Walk
 +| 10125 (5434) 0.54
 +| align="​right"​| 1.22s
 +| 116.26 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (1,12,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 135 (93) 0.69
 +| align="​right"​| 146.54s
 +| 1677307.59 (0.00)
 +| 133.19 (128.74)
 +|-
 +| JPF Stateless Random Walk
 +| 10125 (5405) 0.53
 +| align="​right"​| 1.26s
 +| 126.19 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (1,16,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 4999 (2736) 0.55
 +| align="​right"​| 25.65s
 +| 283379.04 (0.00)
 +| 146.74 (145.98)
 +|-
 +| JPF Stateless Random Walk
 +| 10113 (5380) 0.53
 +| align="​right"​| 1.18s
 +| 146.01 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (1,8,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 115 (111) 0.97
 +| align="​right"​| 94.91s
 +| 1300588.95 (0.00)
 +| 113.86 (107.14)
 +|-
 +| JPF Stateless Random Walk
 +| 10122 (5389) 0.53
 +| align="​right"​| 1.10s
 +| 105.43 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (2,2,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 0.83s
 +| 120.42 (0.00)
 +| 99.09 (98.25)
 +|-
 +| JPF Stateless Random Walk
 +| 10124 (7760) 0.77
 +| align="​right"​| 1.11s
 +| 98.42 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (2,4,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 0.87s
 +| 120.46 (0.00)
 +| 110.75 (110.65)
 +|-
 +| JPF Stateless Random Walk
 +| 10126 (9680) 0.96
 +| align="​right"​| 1.13s
 +| 111.14 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (2,8,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 0.99s
 +| 593.74 (0.00)
 +| 135.70 (135.49)
 +|-
 +| JPF Stateless Random Walk
 +| 10126 (9799) 0.97
 +| align="​right"​| 1.11s
 +| 134.56 (NA)
 +| 0.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | producerconsumer (7,10,4)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 1.22s
 +| 370.09 (0.00)
 +| 369.09 (369.09)
 +|}
 +==Java Pathfinder==
 +===Stateless Random Walk===
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! Parameters !! Path Error Density
 +|-
 +| 1,8,4 || 0.532
 +|- 
 +| 1,10,4 || 0.537
 +|-
 +| 1,12,4 || 0.534
 +|-
 +| 1,16,4 || 0.531
 +|-
 +| 2,2,4 || 0.767
 +|-
 +| 2,2,4 || 0.956
 +|-
 +| 2,8,4 || 0.967
 +|}
 +
 +===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,12,4)
 +| 135 (93) 68.89%
 +| align="​right"​| 146.54s
 +| 1677307.59 (0.00)
 +| 133.19 (128.74)
 +| align="​right"​ | 146535.80
 +| align="​right"​ | 1531.52
 +| align="​right"​ | 133.19
 +| align="​right"​ | 128.74
 +| align="​right"​ | 235782.88
 +| align="​right"​ | 1441524.71
 +| align="​right"​ | 1.20
 +| align="​right"​ | 1677177.85
 +| align="​right"​ | 235652.94
 +| align="​right"​ | 0.00
 +| align="​right"​ | 306280.60
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 141235.20
 +| align="​right"​ | 237.00
 +| align="​right"​ | 237.00
 +|-
 +|(2,8,4)
 +| 100 (100) 100.00%
 +| align="​right"​| 0.99s
 +| 593.74 (0.00)
 +| 135.70 (135.49)
 +| align="​right"​ | 985.94
 +| align="​right"​ | 985.94
 +| align="​right"​ | 135.70
 +| align="​right"​ | 135.49
 +| align="​right"​ | 260.76
 +| align="​right"​ | 332.98
 +| align="​right"​ | 1.02
 +| align="​right"​ | 457.25
 +| align="​right"​ | 124.25
 +| align="​right"​ | 0.00
 +| align="​right"​ | 17381.76
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 225.07
 +| align="​right"​ | 225.07
 +|-
 +|(7,10,4)
 +| 100 (100) 100.00%
 +| align="​right"​| 1.22s
 +| 370.09 (0.00)
 +| 369.09 (369.09)
 +| align="​right"​ | 1217.91
 +| align="​right"​ | 1217.91
 +| align="​right"​ | 369.09
 +| align="​right"​ | 369.09
 +| align="​right"​ | 370.09
 +| align="​right"​ | 0.00
 +| align="​right"​ | 1.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 17490.56
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 253.02
 +| align="​right"​ | 261.46
 +|-
 +|(2,2,4)
 +| 100 (100) 100.00%
 +| align="​right"​| 0.83s
 +| 120.42 (0.00)
 +| 99.09 (98.25)
 +| align="​right"​ | 831.93
 +| align="​right"​ | 831.93
 +| align="​right"​ | 99.09
 +| align="​right"​ | 98.25
 +| align="​right"​ | 111.74
 +| align="​right"​ | 8.68
 +| align="​right"​ | 1.20
 +| align="​right"​ | 21.17
 +| align="​right"​ | 12.28
 +| align="​right"​ | 0.00
 +| align="​right"​ | 16512.00
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 200.93
 +| align="​right"​ | 200.93
 +|-
 +|(2,4,4)
 +| 100 (100) 100.00%
 +| align="​right"​| 0.87s
 +| 120.46 (0.00)
 +| 110.75 (110.65)
 +| align="​right"​ | 865.74
 +| align="​right"​ | 865.74
 +| align="​right"​ | 110.75
 +| align="​right"​ | 110.65
 +| align="​right"​ | 115.66
 +| align="​right"​ | 4.80
 +| align="​right"​ | 1.03
 +| align="​right"​ | 8.81
 +| align="​right"​ | 3.98
 +| align="​right"​ | 0.00
 +| align="​right"​ | 16368.00
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 0.00
 +| align="​right"​ | 209.02
 +| align="​right"​ | 209.02
 +|-
 +|(1,8,4)
 +| 115 (111) 96.52%
 +| align="​right"​| 94.91s
 +| 1300588.95 (0.00)
 +| 113.86 (107.14)
 +| align="​right"​ | 94906.75
 +| align="​right"​ | 3281.18
 +| align="​right"​ | 113.86
 +| align="​right"​ | 107.14
 +| align="​right"​ | 200326.51
 +| align="​right"​ | 1100262.43
 +| align="​right"​ | 1.49
 +| align="​right"​ | 1300480.80
 +| align="​right"​ | 200217.88
 +| align="​right"​ | 0.00
 +| align="​right"​ | 323747.17
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 108138.57
 +| align="​right"​ | 221.00
 +| align="​right"​ | 221.00
 +|-
 +|(1,16,4)
 +| 4999 (2736) 54.73%
 +| align="​right"​| 25.65s
 +| 283379.04 (0.00)
 +| 146.74 (145.98)
 +| align="​right"​ | 25645.56
 +| align="​right"​ | 1081.17
 +| align="​right"​ | 146.74
 +| align="​right"​ | 145.98
 +| align="​right"​ | 38927.38
 +| align="​right"​ | 244451.65
 +| align="​right"​ | 1.03
 +| align="​right"​ | 283232.06
 +| align="​right"​ | 38780.38
 +| align="​right"​ | 0.00
 +| align="​right"​ | 24845.89
 +| align="​right"​ | 932096.00
 +| align="​right"​ | 4041.29
 +| align="​right"​ | 253.00
 +| align="​right"​ | 253.00
 +|-
 +|(1,10,4)
 +| 115 (84) 73.04%
 +| align="​right"​| 86.11s
 +| 963174.08 (0.00)
 +| 121.87 (116.52)
 +| align="​right"​ | 86108.83
 +| align="​right"​ | 2191.33
 +| align="​right"​ | 121.87
 +| align="​right"​ | 116.52
 +| align="​right"​ | 138683.65
 +| align="​right"​ | 824490.43
 +| align="​right"​ | 1.30
 +| align="​right"​ | 963056.56
 +| align="​right"​ | 138565.83
 +| align="​right"​ | 0.00
 +| align="​right"​ | 209030.10
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 78466.30
 +| align="​right"​ | 229.00
 +| align="​right"​ | 229.00
 +|}
vv-lab/producerconsumer.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