search
Differences
This shows you the differences between two versions of the page.
| — |
vv-lab:deadlock [2015/02/18 15:56] (current) egm created |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| + | [[Concurrency Tool Comparison]] | ||
| + | == Model Description== | ||
| + | Two versions of a model that deadlocks. The deadlock is caused from a circular lock dependency. | ||
| + | |||
| + | Classes: 4 | ||
| + | |||
| + | SLOC: 24 | ||
| + | |||
| + | Parameters: (selector) | ||
| + | |||
| + | == Summary Results Table == | ||
| + | |||
| + | === Version A === | ||
| + | {| align=center | border=1 | ||
| + | |- bgcolor="white" | | ||
| + | | colspan=5 align="center" | deadlockVersionA () | ||
| + | |- bgcolor="lightblue" | ||
| + | ! Tool | ||
| + | ! Trials (successful) | ||
| + | ! Time | ||
| + | ! Transition (paths) | ||
| + | ! Max Depth (error depth) | ||
| + | |- | ||
| + | | JPF "Randomized DFS" | ||
| + | | 100 (100) 1.00 | ||
| + | | align="right"| 0.33s | ||
| + | | 18.78 (0.00) | ||
| + | | 12.29 (11.24) | ||
| + | |- | ||
| + | | JPF Stateless Random Walk | ||
| + | | 10142 (4571) 0.45 | ||
| + | | align="right"| NA | ||
| + | | NA (NA) | ||
| + | | NA (NA) | ||
| + | |} | ||
| + | |||
| + | === Version B === | ||
| + | |||
| + | {| align=center | border=1 | ||
| + | |- bgcolor="white" | | ||
| + | | colspan=5 align="center" | deadlockVersionB () | ||
| + | |- bgcolor="lightblue" | ||
| + | ! Tool | ||
| + | ! Trials (successful) | ||
| + | ! Time | ||
| + | ! Transition (paths) | ||
| + | ! Max Depth (error depth) | ||
| + | |- | ||
| + | | JPF "Randomized DFS" | ||
| + | | 100 (100) 1.00 | ||
| + | | align="right"| 0.27s | ||
| + | | 6.44 (0.00) | ||
| + | | 4.36 (4.00) | ||
| + | |- | ||
| + | | JPF Stateless Random Walk | ||
| + | | 10127 (3844) 0.38 | ||
| + | | align="right"| NA | ||
| + | | NA (NA) | ||
| + | | NA (NA) | ||
| + | |} | ||
| + | |||
| + | ==Chess== | ||
| + | |||
| + | * ChessBound=2 | ||
| + | * ChessMonitorVolatiles=false | ||
| + | |||
| + | {| align=center | border=1 | -bgcolor=grey | ||
| + | ! Deadlock Params !! Tests !! Found Error !! Time Taken !! Steps (Depth) | ||
| + | |- | ||
| + | | 1 || 10 || Yes || 0.94 secs || 20 | ||
| + | |} | ||
| + | |||
| + | ==CHESS== | ||
| + | {| align=center | border=1 | | ||
| + | |- bgcolor="lightblue" | ||
| + | ! Parameters !! Time !! Transitions !! paths !! Max Depth | ||
| + | |- | ||
| + | | 1, 1 || .110 || 60 || 3 || 20 | ||
| + | |- | ||
| + | | 1 || .94 || 200 || 10 || 20 | ||
| + | |} | ||
| + | |||
| + | ==Java Pathfinder== | ||
| + | ===Stateless Random Walk=== | ||
| + | |||
| + | {| align=center | border=1 | -bgcolor=grey | ||
| + | ! Parameters !! Path Error Density | ||
| + | |- | ||
| + | | 1 || 0.450 | ||
| + | |- | ||
| + | | 2 || 0.379 | ||
| + | |} | ||
| + | |||
| + | ===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). | ||
| + | {| align="center" | border=1 | ||
| + | |- bgcolor="lightblue" | ||
| + | ! 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% | ||
| + | | align="right"| 0.33s | ||
| + | | 18.78 (0.00) | ||
| + | | 12.29 (11.24) | ||
| + | | align="right" | 333.05 | ||
| + | | align="right" | 333.05 | ||
| + | | align="right" | 12.29 | ||
| + | | align="right" | 11.24 | ||
| + | | align="right" | 17.06 | ||
| + | | align="right" | 1.72 | ||
| + | | align="right" | 0.74 | ||
| + | | align="right" | 6.54 | ||
| + | | align="right" | 4.08 | ||
| + | | align="right" | 0.00 | ||
| + | | align="right" | 10630.40 | ||
| + | | align="right" | 6990528.00 | ||
| + | | align="right" | 0.00 | ||
| + | | align="right" | 128.00 | ||
| + | | align="right" | 128.00 | ||
| + | |- | ||
| + | |() | ||
| + | | 100 (100) 100.00% | ||
| + | | align="right"| 0.27s | ||
| + | | 6.44 (0.00) | ||
| + | | 4.36 (4.00) | ||
| + | | align="right" | 265.34 | ||
| + | | align="right" | 265.34 | ||
| + | | align="right" | 4.36 | ||
| + | | align="right" | 4.00 | ||
| + | | align="right" | 6.32 | ||
| + | | align="right" | 0.12 | ||
| + | | align="right" | 0.60 | ||
| + | | align="right" | 1.44 | ||
| + | | align="right" | 0.72 | ||
| + | | align="right" | 0.00 | ||
| + | | align="right" | 10154.88 | ||
| + | | align="right" | 6990528.00 | ||
| + | | align="right" | 0.00 | ||
| + | | align="right" | 122.00 | ||
| + | | align="right" | 122. | ||
| + | |} | ||
