vv-lab:producerconsumer [CS Wiki]

Differences

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

@@ 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