search
Table of Contents
Model Description
The model is a concurrent linked list implementation that contains an atomicity violation.
Classes: 5
SLOC: 117
Parameters (#builders, maxSize, sync)
Summary Results Table
| linkedlist (4,100) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (100) 1.00 | 10.51s | 10031.57 (0.00) | 9993.02 (9990.94) |
| JPF Stateless Random Walk | 10157 (9988) 0.98 | 9.29s | 9937.49 (NA) | 0.00 (NA) |
CHESS
| Parameters | Time | Transitions | paths | Max Depth |
|---|---|---|---|---|
| 2, 20 | 3447 | 347600 | 400 | 869 |
| 4, 100 | 1450576 | 281497000 | 23000 | 12239 |
Java Pathfinder
Stateless Random Walk
| Parameters | Path Error Density |
|---|---|
| 4,100 | 0.984 |
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 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (4,100) | 100 (100) 100.00% | 10.51s | 10031.57 (0.00) | 9993.02 (9990.94) | 10510.54 | 5309.57 | 9993.02 | 9990.94 | 10014.32 | 17.25 | 1.02 | 39.63 | 22.36 | 0.00 | 78468.48 | 6990528.00 | 12790.96 | 388.80 | 388.80 |
