The model manifests a data race when a set of thread reads from a shared variable while another thread is writing to the same object.
Classes: 3
SLOC: 66
Parameters: (numOfThreads)
accountException (5) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
---|---|---|---|---|
JPF “Randomized DFS” | 5047 (4495) 0.89 | 686.37s | 10536186.70 (0.00) | 197.68 (190.32) |
JPF Stateless Random Walk | 10120 (5555) 0.55 | NA | NA (NA) | NA (NA) |
'*' Deterministic implementation
'na' Data not output by tool (not available)
blank Not yet run
Hardness in a non-deterministic algorithm is the number of trials that find an error divided by the total number of trials where a trial is an independent run of the algorithm. For example, if 100 trials are run and 50 of those are successful in finding an error, then the hardness is reported as 0.50 or 50%. For deterministic algorithms(or tools) hardness is either 1 (easy) or 0 (hard). The time, transitions, and depth are the average over the successful experiments for non-deterministic algorithms.
Account Params | Tests | Found Error | Time Taken | Steps (Depth) |
---|
Account Params | Tests | Found Error | Time Taken | Steps (Depth) |
---|
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 |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
(5) | 10120 (5555) 54.89% | 0.77s | 191.92 (0.00) | 0.00 (0.00) | 771.03 | 771.03 | 0.00 | 0.00 | 191.92 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 12249.84 | 932096.00 | 0.00 | 176.00 | 176.00 |
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 |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
(5) | 5047 (4495) 89.06% | 686.37s | 10536186.70 (0.00) | 197.68 (190.32) | 686374.56 | 3958.51 | 197.68 | 190.32 | 2152801.11 | 8383385.59 | 1.74 | 10536185.70 | 2152264.23 | 2152264.23 | 297339.23 | 932096.00 | 130452.48 | 196.00 | 196.00 |
path error density.
Account Params | Path Error Density |
---|---|
4 | 0.000 |
5 | 0.000 |