search
Table of Contents
Model Description
The model is designed to allocate and free blocks. The bug is manifested due a synchronization gap between two individually locked methods. Context-switching between these methods raises an Exception.
Classes: 3
SLOC: 85
Parameters: (blockSize, vectorSize, #runs)
Summary Results Table
| allocate (2,100,1,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (100) 1.00 | 7.67s | 78569.50 (0.00) | 78.29 (57.01) |
| allocate (2,100,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 7.67s | 78569.50 (0.00) | 78.29 (57.01) |
| CHESS | 1 (1) 1.00 | 1.00s | 216.00 (3.00) | 72.00 (NA) |
| allocate (2,20,1,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 3.08s | 13109.32 (0.00) | 75.57 (56.05) |
| allocate (2,20,4,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 2.93s | 15899.23 (0.00) | 264.60 (248.12) |
| allocate (8,20,1,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (99) 0.99 | 34.69s | 573020.90 (0.00) | 194.87 (154.32) |
Chess
- ChessBound=2
- ChessMonitorVolatiles=false
| AllocationVector Params | Tests | Found Error | Time Taken | Steps (Depth) |
|---|---|---|---|---|
| 2,100,1 | 3 | Yes | 0.4-1.0 secs | 72 |
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.
| Parameters | Path Error Density |
|---|---|
| 2,20,1 | 0.085 |
| 2,20,4 | 0.294 |
| 2,100,1 | 0.018 |
| 8,20,2 | 0.442 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (2,20,4,2) | 100 (100) 100.00% | 2.93s | 15899.23 (0.00) | 264.60 (248.12) | 2932.76 | 2631.07 | 264.60 | 248.12 | 5645.77 | 10253.46 | 0.77 | 15650.11 | 5395.88 | 0.00 | 46645.76 | 6990528.00 | 1592.21 | 225.68 | 225.68 |
| (8,20,1,2) | 100 (99) 99.00% | 34.69s | 573020.90 (0.00) | 194.87 (154.32) | 34692.74 | 3028.96 | 194.87 | 154.32 | 198205.85 | 374815.05 | 0.49 | 572865.58 | 198050.03 | 0.00 | 213983.03 | 6990528.00 | 53879.25 | 194.00 | 194.00 |
| (2,20,1,2) | 100 (100) 100.00% | 3.08s | 13109.32 (0.00) | 75.57 (56.05) | 3082.10 | 2982.10 | 75.57 | 56.05 | 4832.29 | 8277.03 | 0.90 | 13052.27 | 4774.34 | 0.00 | 37712.00 | 6990528.00 | 309.38 | 194.00 | 194.00 |
| (2,100,1,2) | 100 (100) 100.00% | 7.67s | 78569.50 (0.00) | 78.29 (57.01) | 7667.78 | 4665.67 | 78.29 | 57.01 | 28406.49 | 50163.01 | 0.98 | 78511.49 | 28347.50 | 0.00 | 122312.32 | 6990528.00 | 24170.40 | 194.00 | 194.00 |
