search
Table of Contents
Model Description
A readers writers example that contains a race condition.
Classes: 6
SLOC: 103
Parameters (checkForDeadlock)
Summary Results Table
| rwN () | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 118 (94) 0.80 | 1.27s | 575.14 (0.00) | 574.14 (574.14) |
| JPF Stateless Random Walk | 10181 (7820) 0.77 | NA | NA (NA) | NA (NA) |
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.
No Exception Check
| Parameters | Path Error Density |
|---|---|
| default | 0.076 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (N) | 118 (94) 79.66% | 1.27s | 575.14 (0.00) | 574.14 (574.14) | 1269.11 | 1269.11 | 574.14 | 574.14 | 575.14 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 17960.17 | 6990528.00 | 0.00 | 156.69 | 173.64 |
CHESS
| Parameters | Time | Transitions | paths | Max Depth |
|---|---|---|---|---|
| 2, 2, 100 | 391329 | 67920000 | 24000 | 2830 |
