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