Two versions of a model that deadlocks. The deadlock is caused from a circular lock dependency.

Classes: 4

SLOC: 24

Parameters: (selector)

deadlockVersionA () | ||||

Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
---|---|---|---|---|

JPF “Randomized DFS” | 100 (100) 1.00 | 0.33s | 18.78 (0.00) | 12.29 (11.24) |

JPF Stateless Random Walk | 10142 (4571) 0.45 | NA | NA (NA) | NA (NA) |

deadlockVersionB () | ||||

Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
---|---|---|---|---|

JPF “Randomized DFS” | 100 (100) 1.00 | 0.27s | 6.44 (0.00) | 4.36 (4.00) |

JPF Stateless Random Walk | 10127 (3844) 0.38 | NA | NA (NA) | NA (NA) |

- ChessBound=2
- ChessMonitorVolatiles=false

Deadlock Params | Tests | Found Error | Time Taken | Steps (Depth) |
---|---|---|---|---|

1 | 10 | Yes | 0.94 secs | 20 |

Parameters | Time | Transitions | paths | Max Depth |
---|---|---|---|---|

1, 1 | .110 | 60 | 3 | 20 |

1 | .94 | 200 | 10 | 20 |

Parameters | Path Error Density |
---|---|

1 | 0.450 |

2 | 0.379 |

- 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 |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

() | 100 (100) 100.00% | 0.33s | 18.78 (0.00) | 12.29 (11.24) | 333.05 | 333.05 | 12.29 | 11.24 | 17.06 | 1.72 | 0.74 | 6.54 | 4.08 | 0.00 | 10630.40 | 6990528.00 | 0.00 | 128.00 | 128.00 |

() | 100 (100) 100.00% | 0.27s | 6.44 (0.00) | 4.36 (4.00) | 265.34 | 265.34 | 4.36 | 4.00 | 6.32 | 0.12 | 0.60 | 1.44 | 0.72 | 0.00 | 10154.88 | 6990528.00 | 0.00 | 122.00 | 122. |