This shows you the differences between two versions of the page.
— |
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 | ||
+ | |} |